GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_engine.h Lines: 47 47 100.0 %
Date: 2021-03-23 Branches: 103 368 28.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_engine.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The theory engine
13
 **
14
 ** The theory engine.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY_ENGINE_H
20
#define CVC4__THEORY_ENGINE_H
21
22
#include <memory>
23
#include <vector>
24
25
#include "base/check.h"
26
#include "context/cdhashmap.h"
27
#include "expr/node.h"
28
#include "options/theory_options.h"
29
#include "theory/atom_requests.h"
30
#include "theory/engine_output_channel.h"
31
#include "theory/interrupted.h"
32
#include "theory/rewriter.h"
33
#include "theory/sort_inference.h"
34
#include "theory/theory.h"
35
#include "theory/theory_preprocessor.h"
36
#include "theory/trust_node.h"
37
#include "theory/trust_substitutions.h"
38
#include "theory/uf/equality_engine.h"
39
#include "theory/valuation.h"
40
#include "util/hash.h"
41
#include "util/statistics_registry.h"
42
#include "util/unsafe_interrupt_exception.h"
43
44
namespace CVC4 {
45
46
class ResourceManager;
47
class OutputManager;
48
class TheoryEngineProofGenerator;
49
50
/**
51
 * A pair of a theory and a node. This is used to mark the flow of
52
 * propagations between theories.
53
 */
54
504450920
struct NodeTheoryPair {
55
  Node d_node;
56
  theory::TheoryId d_theory;
57
  size_t d_timestamp;
58
72987730
  NodeTheoryPair(TNode n, theory::TheoryId t, size_t ts = 0)
59
72987730
      : d_node(n), d_theory(t), d_timestamp(ts)
60
  {
61
72987730
  }
62
50304306
  NodeTheoryPair() : d_theory(theory::THEORY_LAST), d_timestamp() {}
63
  // Comparison doesn't take into account the timestamp
64
87965661
  bool operator == (const NodeTheoryPair& pair) const {
65
87965661
    return d_node == pair.d_node && d_theory == pair.d_theory;
66
  }
67
};/* struct NodeTheoryPair */
68
69
struct NodeTheoryPairHashFunction {
70
  NodeHashFunction hashFunction;
71
  // Hash doesn't take into account the timestamp
72
163548269
  size_t operator()(const NodeTheoryPair& pair) const {
73
163548269
    uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node));
74
163548269
    return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash));
75
  }
76
};/* struct NodeTheoryPairHashFunction */
77
78
79
/* Forward declarations */
80
namespace theory {
81
class TheoryModel;
82
class CombinationEngine;
83
class SharedSolver;
84
class DecisionManager;
85
class RelevanceManager;
86
87
}/* CVC4::theory namespace */
88
89
namespace prop {
90
class PropEngine;
91
}
92
93
/**
94
 * This is essentially an abstraction for a collection of theories.  A
95
 * TheoryEngine provides services to a PropEngine, making various
96
 * T-solvers look like a single unit to the propositional part of
97
 * CVC4.
98
 */
99
class TheoryEngine {
100
101
  /** Shared terms database can use the internals notify the theories */
102
  friend class SharedTermsDatabase;
103
  friend class theory::EngineOutputChannel;
104
  friend class theory::CombinationEngine;
105
  friend class theory::SharedSolver;
106
107
  /** Associated PropEngine engine */
108
  prop::PropEngine* d_propEngine;
109
110
  /** Our context */
111
  context::Context* d_context;
112
113
  /** Our user context */
114
  context::UserContext* d_userContext;
115
116
  /**
117
   * A table of from theory IDs to theory pointers. Never use this table
118
   * directly, use theoryOf() instead.
119
   */
120
  theory::Theory* d_theoryTable[theory::THEORY_LAST];
121
122
  /**
123
   * A collection of theories that are "active" for the current run.
124
   * This set is provided by the user (as a logic string, say, in SMT-LIBv2
125
   * format input), or else by default it's all-inclusive.  This is important
126
   * because we can optimize for single-theory runs (no sharing), can reduce
127
   * the cost of walking the DAG on registration, etc.
128
   */
129
  const LogicInfo& d_logicInfo;
130
  /** The separation logic location and data types */
131
  TypeNode d_sepLocType;
132
  TypeNode d_sepDataType;
133
134
  /** Reference to the output manager of the smt engine */
135
  OutputManager& d_outMgr;
136
137
  //--------------------------------- new proofs
138
  /** Proof node manager used by this theory engine, if proofs are enabled */
139
  ProofNodeManager* d_pnm;
140
  /** The lazy proof object
141
   *
142
   * This stores instructions for how to construct proofs for all theory lemmas.
143
   */
144
  std::shared_ptr<LazyCDProof> d_lazyProof;
145
  /** The proof generator */
146
  std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
147
  //--------------------------------- end new proofs
148
  /** The combination manager we are using */
149
  std::unique_ptr<theory::CombinationEngine> d_tc;
150
  /** The shared solver of the above combination engine. */
151
  theory::SharedSolver* d_sharedSolver;
152
  /** The quantifiers engine, which is owned by the quantifiers theory */
153
  theory::QuantifiersEngine* d_quantEngine;
154
  /**
155
   * The decision manager
156
   */
157
  std::unique_ptr<theory::DecisionManager> d_decManager;
158
  /** The relevance manager */
159
  std::unique_ptr<theory::RelevanceManager> d_relManager;
160
161
  /** are we in eager model building mode? (see setEagerModelBuilding). */
162
  bool d_eager_model_building;
163
164
  /**
165
   * Output channels for individual theories.
166
   */
167
  theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
168
169
  /**
170
   * Are we in conflict.
171
   */
172
  context::CDO<bool> d_inConflict;
173
174
  /**
175
   * Are we in "SAT mode"? In this state, the user can query for the model.
176
   * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB
177
   * standard, version 2.6.
178
   */
179
  bool d_inSatMode;
180
181
  /**
182
   * Called by the theories to notify of a conflict.
183
   *
184
   * @param conflict The trust node containing the conflict and its proof
185
   * generator (if it exists),
186
   * @param theoryId The theory that sent the conflict
187
   */
188
  void conflict(theory::TrustNode conflict, theory::TheoryId theoryId);
189
190
  /**
191
   * Debugging flag to ensure that shutdown() is called before the
192
   * destructor.
193
   */
194
  bool d_hasShutDown;
195
196
  /**
197
   * True if a theory has notified us of incompleteness (at this
198
   * context level or below).
199
   */
200
  context::CDO<bool> d_incomplete;
201
202
  /**
203
   * Called by the theories to notify that the current branch is incomplete.
204
   */
205
3047
  void setIncomplete(theory::TheoryId theory) {
206
3047
    d_incomplete = true;
207
3047
  }
208
209
  /**
210
   * Mapping of propagations from recievers to senders.
211
   */
212
  typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap;
213
  PropagationMap d_propagationMap;
214
215
  /**
216
   * Timestamp of propagations
217
   */
218
  context::CDO<size_t> d_propagationMapTimestamp;
219
220
  /**
221
   * Literals that are propagated by the theory. Note that these are TNodes.
222
   * The theory can only propagate nodes that have an assigned literal in the
223
   * SAT solver and are hence referenced in the SAT solver.
224
   */
225
  context::CDList<TNode> d_propagatedLiterals;
226
227
  /**
228
   * The index of the next literal to be propagated by a theory.
229
   */
230
  context::CDO<unsigned> d_propagatedLiteralsIndex;
231
232
  /**
233
   * Called by the output channel to propagate literals and facts
234
   * @return false if immediate conflict
235
   */
236
  bool propagate(TNode literal, theory::TheoryId theory);
237
238
  /**
239
   * Internal method to call the propagation routines and collect the
240
   * propagated literals.
241
   */
242
  void propagate(theory::Theory::Effort effort);
243
244
  /**
245
   * A variable to mark if we added any lemmas.
246
   */
247
  bool d_lemmasAdded;
248
249
  /**
250
   * A variable to mark if the OutputChannel was "used" by any theory
251
   * since the start of the last check.  If it has been, we require
252
   * a FULL_EFFORT check before exiting and reporting SAT.
253
   *
254
   * See the documentation for the needCheck() function, below.
255
   */
256
  bool d_outputChannelUsed;
257
258
  /** Atom requests from lemmas */
259
  AtomRequests d_atomRequests;
260
261
  /**
262
   * Adds a new lemma, returning its status.
263
   * @param node the lemma
264
   * @param p the properties of the lemma.
265
   * @param atomsTo the theory that atoms of the lemma should be sent to
266
   * @param from the theory that sent the lemma
267
   */
268
  void lemma(theory::TrustNode node,
269
             theory::LemmaProperty p,
270
             theory::TheoryId atomsTo = theory::THEORY_LAST,
271
             theory::TheoryId from = theory::THEORY_LAST);
272
273
  /** Enusre that the given atoms are send to the given theory */
274
  void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
275
276
  /** sort inference module */
277
  std::unique_ptr<theory::SortInference> d_sortInfer;
278
279
  /** Time spent in theory combination */
280
  TimerStat d_combineTheoriesTime;
281
282
  Node d_true;
283
  Node d_false;
284
285
  /** Whether we were just interrupted (or not) */
286
  bool d_interrupted;
287
  ResourceManager* d_resourceManager;
288
289
 public:
290
  /** Constructs a theory engine */
291
  TheoryEngine(context::Context* context,
292
               context::UserContext* userContext,
293
               ResourceManager* rm,
294
               const LogicInfo& logic,
295
               OutputManager& outMgr,
296
               ProofNodeManager* pnm);
297
298
  /** Destroys a theory engine */
299
  ~TheoryEngine();
300
301
  void interrupt();
302
303
  /** "Spend" a resource during a search or preprocessing.*/
304
  void spendResource(ResourceManager::Resource r);
305
306
  /**
307
   * Adds a theory. Only one theory per TheoryId can be present, so if
308
   * there is another theory it will be deleted.
309
   */
310
  template <class TheoryClass>
311
116997
  inline void addTheory(theory::TheoryId theoryId)
312
  {
313
116997
    Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
314
116997
    d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
315
233994
    d_theoryTable[theoryId] = new TheoryClass(d_context,
316
                                              d_userContext,
317
116997
                                              *d_theoryOut[theoryId],
318
                                              theory::Valuation(this),
319
                                              d_logicInfo,
320
                                              d_pnm);
321
350991
    theory::Rewriter::registerTheoryRewriter(
322
350991
        theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
323
116997
  }
324
325
9029
  void setPropEngine(prop::PropEngine* propEngine)
326
  {
327
9029
    d_propEngine = propEngine;
328
9029
  }
329
330
  /**
331
   * Called when all initialization of options/logic is done, after theory
332
   * objects have been created.
333
   *
334
   * This initializes the quantifiers engine, the "official" equality engines
335
   * of each theory as required, and the model and model builder utilities.
336
   */
337
  void finishInit();
338
339
  /**
340
   * Get a pointer to the underlying propositional engine.
341
   */
342
3149477
  inline prop::PropEngine* getPropEngine() const {
343
3149477
    return d_propEngine;
344
  }
345
346
  /** Get the proof node manager */
347
  ProofNodeManager* getProofNodeManager() const;
348
349
  /**
350
   * Get a pointer to the underlying sat context.
351
   */
352
42042
  context::Context* getSatContext() const { return d_context; }
353
354
  /**
355
   * Get a pointer to the underlying user context.
356
   */
357
12902
  context::UserContext* getUserContext() const { return d_userContext; }
358
359
  /**
360
   * Get a pointer to the underlying quantifiers engine.
361
   */
362
12544
  theory::QuantifiersEngine* getQuantifiersEngine() const {
363
12544
    return d_quantEngine;
364
  }
365
  /**
366
   * Get a pointer to the underlying decision manager.
367
   */
368
  theory::DecisionManager* getDecisionManager() const
369
  {
370
    return d_decManager.get();
371
  }
372
373
 private:
374
  /**
375
   * Queue of nodes for pre-registration.
376
   */
377
  std::queue<TNode> d_preregisterQueue;
378
379
  /**
380
   * Boolean flag denoting we are in pre-registration.
381
   */
382
  bool d_inPreregister;
383
384
  /**
385
   * Did the theories get any new facts since the last time we called
386
   * check()
387
   */
388
  context::CDO<bool> d_factsAsserted;
389
390
  /**
391
   * Assert the formula to the given theory.
392
   * @param assertion the assertion to send (not necesserily normalized)
393
   * @param original the assertion as it was sent in from the propagating theory
394
   * @param toTheoryId the theory to assert to
395
   * @param fromTheoryId the theory that sent it
396
   */
397
  void assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
398
399
  /**
400
   * Marks a theory propagation from a theory to a theory where a
401
   * theory could be the THEORY_SAT_SOLVER for literals coming from
402
   * or being propagated to the SAT solver. If the receiving theory
403
   * already recieved the literal, the method returns false, otherwise
404
   * it returns true.
405
   *
406
   * @param assertion the normalized assertion being sent
407
   * @param originalAssertion the actual assertion that was sent
408
   * @param toTheoryId the theory that is on the receiving end
409
   * @param fromTheoryId the theory that sent the assertion
410
   * @return true if a new assertion, false if theory already got it
411
   */
412
  bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
413
414
  /**
415
   * Computes the explanation by traversing the propagation graph and
416
   * asking relevant theories to explain the propagations. Initially
417
   * the explanation vector should contain only the element (node, theory)
418
   * where the node is the one to be explained, and the theory is the
419
   * theory that sent the literal.
420
   */
421
  theory::TrustNode getExplanation(
422
      std::vector<NodeTheoryPair>& explanationVector);
423
424
  /** Are proofs enabled? */
425
  bool isProofEnabled() const;
426
427
 public:
428
  /**
429
   * Preprocess rewrite equality, called by the preprocessor to rewrite
430
   * equalities appearing in the input.
431
   */
432
  theory::TrustNode ppRewriteEquality(TNode eq);
433
  /** Notify (preprocessed) assertions. */
434
  void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
435
436
  /** Return whether or not we are incomplete (in the current context). */
437
5953
  inline bool isIncomplete() const { return d_incomplete; }
438
439
  /**
440
   * Returns true if we need another round of checking.  If this
441
   * returns true, check(FULL_EFFORT) _must_ be called by the
442
   * propositional layer before reporting SAT.
443
   *
444
   * This is especially necessary for incomplete theories that lazily
445
   * output some lemmas on FULL_EFFORT check (e.g. quantifier reasoning
446
   * outputing quantifier instantiations).  In such a case, a lemma can
447
   * be asserted that is simplified away (perhaps it's already true).
448
   * However, we must maintain the invariant that, if a theory uses the
449
   * OutputChannel, it implicitly requests that another check(FULL_EFFORT)
450
   * be performed before exit, even if no new facts are on its fact queue,
451
   * as it might decide to further instantiate some lemmas, precluding
452
   * a SAT response.
453
   */
454
4217141
  inline bool needCheck() const {
455
4217141
    return d_outputChannelUsed || d_lemmasAdded;
456
  }
457
  /**
458
   * Is the literal lit (possibly) critical for satisfying the input formula in
459
   * the current context? This call is applicable only during collectModelInfo
460
   * or during LAST_CALL effort.
461
   */
462
  bool isRelevant(Node lit) const;
463
  /**
464
   * This is called at shutdown time by the SmtEngine, just before
465
   * destruction.  It is important because there are destruction
466
   * ordering issues between PropEngine and Theory.
467
   */
468
  void shutdown();
469
470
  /**
471
   * Solve the given literal with a theory that owns it. The proof of tliteral
472
   * is carried in the trust node. The proof added to substitutionOut should
473
   * take this proof into account (when proofs are enabled).
474
   */
475
  theory::Theory::PPAssertStatus solve(
476
      theory::TrustNode tliteral,
477
      theory::TrustSubstitutionMap& substitutionOut);
478
479
  /**
480
   * Preregister a Theory atom with the responsible theory (or
481
   * theories).
482
   */
483
  void preRegister(TNode preprocessed);
484
485
  /**
486
   * Assert the formula to the appropriate theory.
487
   * @param node the assertion
488
   */
489
  void assertFact(TNode node);
490
491
  /**
492
   * Check all (currently-active) theories for conflicts.
493
   * @param effort the effort level to use
494
   */
495
  void check(theory::Theory::Effort effort);
496
497
  /**
498
   * Calls ppStaticLearn() on all theories, accumulating their
499
   * combined contributions in the "learned" builder.
500
   */
501
  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
502
503
  /**
504
   * Calls presolve() on all theories and returns true
505
   * if one of the theories discovers a conflict.
506
   */
507
  bool presolve();
508
509
   /**
510
   * Calls postsolve() on all theories.
511
   */
512
  void postsolve();
513
514
  /**
515
   * Calls notifyRestart() on all active theories.
516
   */
517
  void notifyRestart();
518
519
11805775
  void getPropagatedLiterals(std::vector<TNode>& literals) {
520
19981346
    for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) {
521
8175571
      Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl;
522
8175571
      literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]);
523
    }
524
3630204
  }
525
526
  /**
527
   * Returns the next decision request, or null if none exist. The next
528
   * decision request is a literal that this theory engine prefers the SAT
529
   * solver to make as its next decision. Decision requests are managed by
530
   * the decision manager d_decManager.
531
   */
532
  Node getNextDecisionRequest();
533
534
  bool properConflict(TNode conflict) const;
535
536
  /**
537
   * Returns an explanation of the node propagated to the SAT solver.
538
   */
539
  theory::TrustNode getExplanation(TNode node);
540
541
  /**
542
   * Get the pointer to the model object used by this theory engine.
543
   */
544
  theory::TheoryModel* getModel();
545
  /**
546
   * Get the current model for the current set of assertions. This method
547
   * should only be called immediately after a satisfiable or unknown
548
   * response to a check-sat call, and only if produceModels is true.
549
   *
550
   * If the model is not already built, this will cause this theory engine
551
   * to build the model.
552
   *
553
   * If the model is not available (for instance, if the last call to check-sat
554
   * was interrupted), then this returns the null pointer.
555
   */
556
  theory::TheoryModel* getBuiltModel();
557
  /**
558
   * This forces the model maintained by the combination engine to be built
559
   * if it has not been done so already. This should be called only during a
560
   * last call effort check after theory combination is run.
561
   *
562
   * @return true if the model was successfully built (possibly prior to this
563
   * call).
564
   */
565
  bool buildModel();
566
  /** set eager model building
567
   *
568
   * If this method is called, then this TheoryEngine will henceforth build
569
   * its model immediately after every satisfiability check that results
570
   * in a satisfiable or unknown result. The motivation for this mode is to
571
   * accomodate API users that get the model object from the TheoryEngine,
572
   * where we want to ensure that this model is always valid.
573
   * TODO (#2648): revisit this.
574
   */
575
25
  void setEagerModelBuilding() { d_eager_model_building = true; }
576
577
  /**
578
   * Get the theory associated to a given Node.
579
   *
580
   * @returns the theory, or NULL if the TNode is
581
   * of built-in type.
582
   */
583
2205440
  inline theory::Theory* theoryOf(TNode node) const {
584
2205440
    return d_theoryTable[theory::Theory::theoryOf(node)];
585
  }
586
587
  /**
588
   * Get the theory associated to a the given theory id.
589
   *
590
   * @returns the theory
591
   */
592
40132445
  inline theory::Theory* theoryOf(theory::TheoryId theoryId) const {
593
40132445
    Assert(theoryId < theory::THEORY_LAST);
594
40132445
    return d_theoryTable[theoryId];
595
  }
596
597
1580198
  inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
598
1580198
    return d_logicInfo.isTheoryEnabled(theoryId);
599
  }
600
  /** get the logic info used by this theory engine */
601
  const LogicInfo& getLogicInfo() const;
602
  /** get the separation logic heap types */
603
  bool getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const;
604
605
  /**
606
   * Declare heap. This is used for separation logics to set the location
607
   * and data types. It should be called only once, and before any separation
608
   * logic constraints are asserted to this theory engine.
609
   */
610
  void declareSepHeap(TypeNode locT, TypeNode dataT);
611
612
  /**
613
   * Returns the equality status of the two terms, from the theory
614
   * that owns the domain type.  The types of a and b must be the same.
615
   */
616
  theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
617
618
  /**
619
   * Returns the value that a theory that owns the type of var currently
620
   * has (or null if none);
621
   */
622
  Node getModelValue(TNode var);
623
624
  /**
625
   * Forwards an entailment check according to the given theoryOfMode.
626
   * See theory.h for documentation on entailmentCheck().
627
   */
628
  std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
629
630
 private:
631
632
  /** Dump the assertions to the dump */
633
  void dumpAssertions(const char* tag);
634
635
  /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
636
public:
637
4736
 theory::SortInference* getSortInference() { return d_sortInfer.get(); }
638
639
 /** Prints the assertions to the debug stream */
640
 void printAssertions(const char* tag);
641
642
private:
643
644
  std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
645
646
 public:
647
  /** Set user attribute.
648
   *
649
   * This function is called when an attribute is set by a user.  In SMT-LIBv2
650
   * this is done via the syntax (! n :attr)
651
   */
652
  void setUserAttribute(const std::string& attr,
653
                        Node n,
654
                        const std::vector<Node>& node_values,
655
                        const std::string& str_value);
656
657
  /** Handle user attribute.
658
   *
659
   * Associates theory t with the attribute attr.  Theory t will be
660
   * notified whenever an attribute of name attr is set.
661
   */
662
  void handleUserAttribute(const char* attr, theory::Theory* t);
663
664
  /**
665
   * Check that the theory assertions are satisfied in the model.
666
   * This function is called from the smt engine's checkModel routine.
667
   */
668
  void checkTheoryAssertionsWithModel(bool hardFailure);
669
};/* class TheoryEngine */
670
671
}/* CVC4 namespace */
672
673
#endif /* CVC4__THEORY_ENGINE_H */