GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory.h Lines: 75 97 77.3 %
Date: 2021-03-23 Branches: 70 170 41.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
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 Base of the theory interface.
13
 **
14
 ** Base of the theory interface.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__THEORY_H
20
#define CVC4__THEORY__THEORY_H
21
22
#include <iosfwd>
23
#include <set>
24
#include <string>
25
#include <unordered_set>
26
27
#include "context/cdlist.h"
28
#include "context/cdo.h"
29
#include "context/context.h"
30
#include "expr/node.h"
31
#include "options/theory_options.h"
32
#include "theory/assertion.h"
33
#include "theory/care_graph.h"
34
#include "theory/logic_info.h"
35
#include "theory/skolem_lemma.h"
36
#include "theory/theory_id.h"
37
#include "theory/trust_node.h"
38
#include "theory/valuation.h"
39
#include "util/statistics_registry.h"
40
#include "util/stats_timer.h"
41
42
namespace CVC4 {
43
44
class ProofNodeManager;
45
class TheoryEngine;
46
47
namespace theory {
48
49
class DecisionManager;
50
struct EeSetupInfo;
51
class OutputChannel;
52
class QuantifiersEngine;
53
class TheoryInferenceManager;
54
class TheoryModel;
55
class TheoryRewriter;
56
class TheoryState;
57
class TrustSubstitutionMap;
58
59
namespace eq {
60
  class EqualityEngine;
61
}/* CVC4::theory::eq namespace */
62
63
/**
64
 * Base class for T-solvers.  Abstract DPLL(T).
65
 *
66
 * This is essentially an interface class.  The TheoryEngine has
67
 * pointers to Theory.  Note that only one specific Theory type (e.g.,
68
 * TheoryUF) can exist per NodeManager, because of how the
69
 * RegisteredAttr works.  (If you need multiple instances of the same
70
 * theory, you'll have to write a multiplexed theory that dispatches
71
 * all calls to them.)
72
 *
73
 * NOTE: A Theory has a special way of being initialized. The owner of a Theory
74
 * is either:
75
 *
76
 * (A) Using Theory as a standalone object, not associated with a TheoryEngine.
77
 * In this case, simply call the public initialization method
78
 * (Theory::finishInitStandalone).
79
 *
80
 * (B) TheoryEngine, which determines how the Theory acts in accordance with
81
 * its theory combination policy. We require the following steps in order:
82
 * (B.1) Get information about whether the theory wishes to use an equality
83
 * eninge, and more specifically which equality engine notifications the Theory
84
 * would like to be notified of (Theory::needsEqualityEngine).
85
 * (B.2) Set the equality engine of the theory (Theory::setEqualityEngine),
86
 * which we refer to as the "official equality engine" of this Theory. The
87
 * equality engine passed to the theory must respect the contract(s) specified
88
 * by the equality engine setup information (EeSetupInfo) returned in the
89
 * previous step.
90
 * (B.3) Set the other required utilities including setQuantifiersEngine and
91
 * setDecisionManager.
92
 * (B.4) Call the private initialization method (Theory::finishInit).
93
 *
94
 * Initialization of the second form happens during TheoryEngine::finishInit,
95
 * after the quantifiers engine and model objects have been set up.
96
 */
97
class Theory {
98
  friend class ::CVC4::TheoryEngine;
99
100
 private:
101
  // Disallow default construction, copy, assignment.
102
  Theory() = delete;
103
  Theory(const Theory&) = delete;
104
  Theory& operator=(const Theory&) = delete;
105
106
  /** An integer identifying the type of the theory. */
107
  TheoryId d_id;
108
109
  /** The SAT search context for the Theory. */
110
  context::Context* d_satContext;
111
112
  /** The user level assertion context for the Theory. */
113
  context::UserContext* d_userContext;
114
115
  /** Information about the logic we're operating within. */
116
  const LogicInfo& d_logicInfo;
117
118
  /**
119
   * The assertFact() queue.
120
   *
121
   * These can not be TNodes as some atoms (such as equalities) are sent
122
   * across theories without being stored in a global map.
123
   */
124
  context::CDList<Assertion> d_facts;
125
126
  /** Index into the head of the facts list */
127
  context::CDO<unsigned> d_factsHead;
128
129
  /** Indices for splitting on the shared terms. */
130
  context::CDO<unsigned> d_sharedTermsIndex;
131
132
  /** The care graph the theory will use during combination. */
133
  CareGraph* d_careGraph;
134
135
  /** Pointer to the decision manager. */
136
  DecisionManager* d_decManager;
137
138
 protected:
139
  /** Name of this theory instance. Along with the TheoryId this should provide
140
   * an unique string identifier for each instance of a Theory class. We need
141
   * this to ensure unique statistics names over multiple theory instances. */
142
  std::string d_instanceName;
143
144
  // === STATISTICS ===
145
  /** time spent in check calls */
146
  TimerStat d_checkTime;
147
  /** time spent in theory combination */
148
  TimerStat d_computeCareGraphTime;
149
150
  /**
151
   * The only method to add suff to the care graph.
152
   */
153
  void addCarePair(TNode t1, TNode t2);
154
155
  /**
156
   * The function should compute the care graph over the shared terms.
157
   * The default function returns all the pairs among the shared variables.
158
   */
159
  virtual void computeCareGraph();
160
161
  /**
162
   * A list of shared terms that the theory has.
163
   */
164
  context::CDList<TNode> d_sharedTerms;
165
166
  /**
167
   * Construct a Theory.
168
   *
169
   * The pair <id, instance> is assumed to uniquely identify this Theory
170
   * w.r.t. the SmtEngine.
171
   */
172
  Theory(TheoryId id,
173
         context::Context* satContext,
174
         context::UserContext* userContext,
175
         OutputChannel& out,
176
         Valuation valuation,
177
         const LogicInfo& logicInfo,
178
         ProofNodeManager* pnm,
179
         std::string instance = "");  // taking : No default.
180
181
  /**
182
   * This is called at shutdown time by the TheoryEngine, just before
183
   * destruction.  It is important because there are destruction
184
   * ordering issues between PropEngine and Theory (based on what
185
   * hard-links to Nodes are outstanding).  As the fact queue might be
186
   * nonempty, we ensure here that it's clear.  If you overload this,
187
   * you must make an explicit call here to this->Theory::shutdown()
188
   * too.
189
   */
190
71934
  virtual void shutdown() { }
191
192
  /**
193
   * The output channel for the Theory.
194
   */
195
  OutputChannel* d_out;
196
197
  /**
198
   * The valuation proxy for the Theory to communicate back with the
199
   * theory engine (and other theories).
200
   */
201
  Valuation d_valuation;
202
  /**
203
   * Pointer to the official equality engine of this theory, which is owned by
204
   * the equality engine manager of TheoryEngine.
205
   */
206
  eq::EqualityEngine* d_equalityEngine;
207
  /**
208
   * The official equality engine, if we allocated it.
209
   */
210
  std::unique_ptr<eq::EqualityEngine> d_allocEqualityEngine;
211
  /**
212
   * The theory state, which contains contexts, valuation, and equality engine.
213
   * Notice the theory is responsible for memory management of this class.
214
   */
215
  TheoryState* d_theoryState;
216
  /**
217
   * The theory inference manager. This is a wrapper around the equality
218
   * engine and the output channel. It ensures that the output channel and
219
   * the equality engine are used properly.
220
   */
221
  TheoryInferenceManager* d_inferManager;
222
223
  /**
224
   * Pointer to the quantifiers engine (or NULL, if quantifiers are not
225
   * supported or not enabled). Not owned by the theory.
226
   */
227
  QuantifiersEngine* d_quantEngine;
228
229
  /** Pointer to proof node manager */
230
  ProofNodeManager* d_pnm;
231
232
  /**
233
   * Are proofs enabled?
234
   *
235
   * They are considered enabled if the ProofNodeManager is non-null.
236
   */
237
  bool proofsEnabled() const;
238
239
  /**
240
   * Returns the next assertion in the assertFact() queue.
241
   *
242
   * @return the next assertion in the assertFact() queue
243
   */
244
  inline Assertion get();
245
246
174179
  const LogicInfo& getLogicInfo() const {
247
174179
    return d_logicInfo;
248
  }
249
250
  /**
251
   * Set separation logic heap. This is called when the location and data
252
   * types for separation logic are determined. This should be called at
253
   * most once, before solving.
254
   *
255
   * This currently should be overridden by the separation logic theory only.
256
   */
257
1444
  virtual void declareSepHeap(TypeNode locT, TypeNode dataT) {}
258
259
  /**
260
   * The theory that owns the uninterpreted sort.
261
   */
262
  static TheoryId s_uninterpretedSortOwner;
263
264
  void printFacts(std::ostream& os) const;
265
  void debugPrintFacts() const;
266
267
  /** is legal elimination
268
   *
269
   * Returns true if x -> val is a legal elimination of variable x. This is
270
   * useful for ppAssert, when x = val is an entailed equality. This function
271
   * determines whether indeed x can be eliminated from the problem via the
272
   * substituion x -> val.
273
   *
274
   * The following criteria imply that x -> val is *not* a legal elimination:
275
   * (1) If x is contained in val,
276
   * (2) If the type of val is not a subtype of the type of x,
277
   * (3) If val contains an operator that cannot be evaluated, and produceModels
278
   * is true. For example, x -> sqrt(2) is not a legal elimination if we
279
   * are producing models. This is because we care about the value of x, and
280
   * its value must be computed (approximated) by the non-linear solver.
281
   */
282
  bool isLegalElimination(TNode x, TNode val);
283
  //--------------------------------- private initialization
284
  /**
285
   * Called to set the official equality engine. This should be done by
286
   * TheoryEngine only.
287
   */
288
  void setEqualityEngine(eq::EqualityEngine* ee);
289
  /** Called to set the quantifiers engine. */
290
  void setQuantifiersEngine(QuantifiersEngine* qe);
291
  /** Called to set the decision manager. */
292
  void setDecisionManager(DecisionManager* dm);
293
  /**
294
   * Finish theory initialization.  At this point, options and the logic
295
   * setting are final, the master equality engine and quantifiers
296
   * engine (if any) are initialized, and the official equality engine of this
297
   * theory has been assigned.  This base class implementation
298
   * does nothing. This should be called by TheoryEngine only.
299
   */
300
8997
  virtual void finishInit() {}
301
  //--------------------------------- end private initialization
302
303
  /**
304
   * This method is called to notify a theory that the node n should
305
   * be considered a "shared term" by this theory. This does anything
306
   * theory-specific concerning the fact that n is now marked as a shared
307
   * term, which is done in addition to explicitly storing n as a shared
308
   * term and adding it as a trigger term in the equality engine of this
309
   * class (see addSharedTerm).
310
   */
311
  virtual void notifySharedTerm(TNode n);
312
313
 public:
314
  //--------------------------------- initialization
315
  /**
316
   * @return The theory rewriter associated with this theory.
317
   */
318
  virtual TheoryRewriter* getTheoryRewriter() = 0;
319
  /**
320
   * Returns true if this theory needs an equality engine for checking
321
   * satisfiability.
322
   *
323
   * If this method returns true, then the equality engine manager will
324
   * initialize its equality engine field via setEqualityEngine above during
325
   * TheoryEngine::finishInit, prior to calling finishInit for this theory.
326
   *
327
   * Additionally, if this method returns true, then this method is required to
328
   * update the argument esi with instructions for initializing and setting up
329
   * notifications from its equality engine, which is commonly done with
330
   * a notifications class (eq::EqualityEngineNotify).
331
   */
332
  virtual bool needsEqualityEngine(EeSetupInfo& esi);
333
  /**
334
   * Finish theory initialization, standalone version. This is used to
335
   * initialize this class if it is not associated with a theory engine.
336
   * This allocates the official equality engine of this Theory and then
337
   * calls the finishInit method above.
338
   */
339
  void finishInitStandalone();
340
  //--------------------------------- end initialization
341
342
  /**
343
   * Return the ID of the theory responsible for the given type.
344
   */
345
50515566
  static inline TheoryId theoryOf(TypeNode typeNode) {
346
50515566
    Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
347
    TheoryId id;
348
50515566
    if (typeNode.getKind() == kind::TYPE_CONSTANT) {
349
36674973
      id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
350
    } else {
351
13840593
      id = kindToTheoryId(typeNode.getKind());
352
    }
353
50515566
    if (id == THEORY_BUILTIN) {
354
2828191
      Trace("theory::internal") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
355
2828191
      return s_uninterpretedSortOwner;
356
    }
357
47687375
    return id;
358
  }
359
360
  /**
361
   * Returns the ID of the theory responsible for the given node.
362
   */
363
  static TheoryId theoryOf(options::TheoryOfMode mode, TNode node);
364
365
  /**
366
   * Returns the ID of the theory responsible for the given node.
367
   */
368
158797440
  static inline TheoryId theoryOf(TNode node) {
369
317605985
    return theoryOf(options::theoryOfMode(), node);
370
  }
371
372
  /**
373
   * Set the owner of the uninterpreted sort.
374
   */
375
8997
  static void setUninterpretedSortOwner(TheoryId theory) {
376
8997
    s_uninterpretedSortOwner = theory;
377
8997
  }
378
379
  /**
380
   * Get the owner of the uninterpreted sort.
381
   */
382
  static TheoryId getUninterpretedSortOwner() {
383
    return s_uninterpretedSortOwner;
384
  }
385
386
  /**
387
   * Checks if the node is a leaf node of this theory
388
   */
389
343844
  inline bool isLeaf(TNode node) const {
390
343844
    return node.getNumChildren() == 0 || theoryOf(node) != d_id;
391
  }
392
393
  /**
394
   * Checks if the node is a leaf node of a theory.
395
   */
396
179542761
  inline static bool isLeafOf(TNode node, TheoryId theoryId) {
397
179542761
    return node.getNumChildren() == 0 || theoryOf(node) != theoryId;
398
  }
399
400
  /** Returns true if the assertFact queue is empty*/
401
50490669
  bool done() const { return d_factsHead == d_facts.size(); }
402
  /**
403
   * Destructs a Theory.
404
   */
405
  virtual ~Theory();
406
407
  /**
408
   * Subclasses of Theory may add additional efforts.  DO NOT CHECK
409
   * equality with one of these values (e.g. if STANDARD xxx) but
410
   * rather use range checks (or use the helper functions below).
411
   * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
412
   * with FULL_EFFORT.
413
   */
414
  enum Effort
415
  {
416
    /**
417
     * Standard effort where theory need not do anything
418
     */
419
    EFFORT_STANDARD = 50,
420
    /**
421
     * Full effort requires the theory make sure its assertions are satisfiable
422
     * or not
423
     */
424
    EFFORT_FULL = 100,
425
    /**
426
     * Last call effort, called after theory combination has completed with
427
     * no lemmas and a model is available.
428
     */
429
    EFFORT_LAST_CALL = 200
430
  }; /* enum Effort */
431
432
4
  static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
433
4
    { return e >= EFFORT_STANDARD; }
434
4
  static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION
435
4
    { return e >= EFFORT_STANDARD && e <  EFFORT_FULL; }
436
34349375
  static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
437
34349375
    { return e == EFFORT_FULL; }
438
439
  /**
440
   * Get the id for this Theory.
441
   */
442
19754844
  TheoryId getId() const {
443
19754844
    return d_id;
444
  }
445
446
  /**
447
   * Get the SAT context associated to this Theory.
448
   */
449
4190076
  context::Context* getSatContext() const {
450
4190076
    return d_satContext;
451
  }
452
453
  /**
454
   * Get the context associated to this Theory.
455
   */
456
139002
  context::UserContext* getUserContext() const {
457
139002
    return d_userContext;
458
  }
459
460
  /**
461
   * Get the output channel associated to this theory.
462
   */
463
117797
  OutputChannel& getOutputChannel() {
464
117797
    return *d_out;
465
  }
466
467
  /**
468
   * Get the valuation associated to this theory.
469
   */
470
34458
  Valuation& getValuation() {
471
34458
    return d_valuation;
472
  }
473
474
  /** Get the equality engine being used by this theory. */
475
  eq::EqualityEngine* getEqualityEngine();
476
477
  /**
478
   * Get the quantifiers engine associated to this theory.
479
   */
480
217330
  QuantifiersEngine* getQuantifiersEngine() {
481
217330
    return d_quantEngine;
482
  }
483
484
  /** Get the decision manager associated to this theory. */
485
12208
  DecisionManager* getDecisionManager() { return d_decManager; }
486
487
  /**
488
   * @return The theory state associated with this theory.
489
   */
490
  TheoryState* getTheoryState() { return d_theoryState; }
491
492
  /**
493
   * @return The theory inference manager associated with this theory.
494
   */
495
  TheoryInferenceManager* getInferenceManager() { return d_inferManager; }
496
497
  /**
498
   * Expand definitions in the term node. This returns a term that is
499
   * equivalent to node. It wraps this term in a TrustNode of kind
500
   * TrustNodeKind::REWRITE. If node is unchanged by this method, the
501
   * null TrustNode may be returned. This is an optimization to avoid
502
   * constructing the trivial equality (= node node) internally within
503
   * TrustNode.
504
   *
505
   * The purpose of this method is typically to eliminate the operators in node
506
   * that are syntax sugar that cannot otherwise be eliminated during rewriting.
507
   * For example, division relies on the introduction of an uninterpreted
508
   * function for the divide-by-zero case, which we do not introduce with
509
   * the rewriter, since this function may be cached in a non-global fashion.
510
   *
511
   * Some theories have kinds that are effectively definitions and should be
512
   * expanded before they are handled.  Definitions allow a much wider range of
513
   * actions than the normal forms given by the rewriter. However no
514
   * assumptions can be made about subterms having been expanded or rewritten.
515
   * Where possible rewrite rules should be used, definitions should only be
516
   * used when rewrites are not possible, for example in handling
517
   * under-specified operations using partially defined functions.
518
   *
519
   * Some theories like sets use expandDefinition as a "context
520
   * independent preRegisterTerm".  This is required for cases where
521
   * a theory wants to be notified about a term before preprocessing
522
   * and simplification but doesn't necessarily want to rewrite it.
523
   */
524
5699
  virtual TrustNode expandDefinition(Node node)
525
  {
526
    // by default, do nothing
527
5699
    return TrustNode::null();
528
  }
529
530
  /**
531
   * Pre-register a term.  Done one time for a Node per SAT context level.
532
   */
533
  virtual void preRegisterTerm(TNode);
534
535
  /**
536
   * Assert a fact in the current context.
537
   */
538
15156934
  void assertFact(TNode assertion, bool isPreregistered) {
539
30313868
    Trace("theory") << "Theory<" << getId() << ">::assertFact["
540
30313868
                    << d_satContext->getLevel() << "](" << assertion << ", "
541
15156934
                    << (isPreregistered ? "true" : "false") << ")" << std::endl;
542
15156934
    d_facts.push_back(Assertion(assertion, isPreregistered));
543
15156934
  }
544
545
  /** Add shared term to the theory. */
546
  void addSharedTerm(TNode node);
547
548
  /**
549
   * Return the current theory care graph. Theories should overload
550
   * computeCareGraph to do the actual computation, and use addCarePair to add
551
   * pairs to the care graph.
552
   */
553
  void getCareGraph(CareGraph* careGraph);
554
555
  /**
556
   * Return the status of two terms in the current context. Should be
557
   * implemented in sub-theories to enable more efficient theory-combination.
558
   */
559
  virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
560
561
  /**
562
   * Return the model value of the give shared term (or null if not available).
563
   *
564
   * TODO (project #39): this method is likely to become deprecated.
565
   */
566
1718
  virtual Node getModelValue(TNode var) { return Node::null(); }
567
568
  /** T-propagate new literal assignments in the current context. */
569
573701
  virtual void propagate(Effort level = EFFORT_FULL) {}
570
571
  /**
572
   * Return an explanation for the literal represented by parameter n
573
   * (which was previously propagated by this theory).
574
   */
575
  virtual TrustNode explain(TNode n)
576
  {
577
    Unimplemented() << "Theory " << identify()
578
                    << " propagated a node but doesn't implement the "
579
                       "Theory::explain() interface!";
580
    return TrustNode::null();
581
  }
582
583
  //--------------------------------- check
584
  /**
585
   * Does this theory wish to be called to check at last call effort? This is
586
   * the case for any theory that wishes to run when a model is available.
587
   */
588
61682
  virtual bool needsCheckLastEffort() { return false; }
589
  /**
590
   * Check the current assignment's consistency.
591
   *
592
   * An implementation of check() is required to either:
593
   * - return a conflict on the output channel,
594
   * - be interrupted,
595
   * - throw an exception
596
   * - or call get() until done() is true.
597
   *
598
   * The standard method for check consists of a loop that processes the entire
599
   * fact queue when preCheck returns false. It makes four theory-specific
600
   * callbacks, (preCheck, postCheck, preNotifyFact, notifyFact) as described
601
   * below. It asserts each fact to the official equality engine when
602
   * preNotifyFact returns false.
603
   *
604
   * Theories that use this check method must use an official theory
605
   * state object (d_theoryState).
606
   */
607
  void check(Effort level = EFFORT_FULL);
608
  /**
609
   * Pre-check, called before the fact queue of the theory is processed.
610
   * If this method returns false, then the theory will process its fact
611
   * queue. If this method returns true, then the theory has indicated
612
   * its check method should finish immediately.
613
   */
614
  virtual bool preCheck(Effort level = EFFORT_FULL);
615
  /**
616
   * Post-check, called after the fact queue of the theory is processed.
617
   */
618
  virtual void postCheck(Effort level = EFFORT_FULL);
619
  /**
620
   * Pre-notify fact, return true if the theory processed it. If this
621
   * method returns false, then the atom will be added to the equality engine
622
   * of the theory and notifyFact will be called with isInternal=false.
623
   *
624
   * Theories that implement check but do not use official equality
625
   * engines should always return true for this method.
626
   *
627
   * @param atom The atom
628
   * @param polarity Its polarity
629
   * @param fact The original literal that was asserted
630
   * @param isPrereg Whether the assertion is preregistered
631
   * @param isInternal Whether the origin of the fact was internal. If this
632
   * is false, the fact was asserted via the fact queue of the theory.
633
   * @return true if the theory completely processed this fact, i.e. it does
634
   * not need to assert the fact to its equality engine.
635
   */
636
  virtual bool preNotifyFact(
637
      TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal);
638
  /**
639
   * Notify fact, called immediately after the fact was pushed into the
640
   * equality engine.
641
   *
642
   * @param atom The atom
643
   * @param polarity Its polarity
644
   * @param fact The original literal that was asserted.
645
   * @param isInternal Whether the origin of the fact was internal. If this
646
   * is false, the fact was asserted via the fact queue of the theory.
647
   */
648
  virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal);
649
  //--------------------------------- end check
650
651
  //--------------------------------- collect model info
652
  /**
653
   * Get all relevant information in this theory regarding the current
654
   * model.  This should be called after a call to check( FULL_EFFORT )
655
   * for all theories with no conflicts and no lemmas added.
656
   *
657
   * This method returns true if and only if the equality engine of m is
658
   * consistent as a result of this call.
659
   *
660
   * The standard method for collectModelInfo computes the relevant terms,
661
   * asserts the theory's equality engine to the model (if necessary) and
662
   * then calls computeModelValues.
663
   *
664
   * TODO (project #39): this method should be non-virtual, once all theories
665
   * conform to the new standard, delete, move to model manager distributed.
666
   */
667
  virtual bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet);
668
  /**
669
   * Compute terms that are not necessarily part of the assertions or
670
   * shared terms that should be considered relevant, add them to termSet.
671
   */
672
  virtual void computeRelevantTerms(std::set<Node>& termSet);
673
  /**
674
   * Collect model values, after equality information is added to the model.
675
   * The argument termSet is the set of relevant terms returned by
676
   * computeRelevantTerms.
677
   */
678
  virtual bool collectModelValues(TheoryModel* m,
679
                                  const std::set<Node>& termSet);
680
  /** if theories want to do something with model after building, do it here */
681
11388
  virtual void postProcessModel( TheoryModel* m ){ }
682
  //--------------------------------- end collect model info
683
684
  //--------------------------------- preprocessing
685
  /**
686
   * Statically learn from assertion "in," which has been asserted
687
   * true at the top level.  The theory should only add (via
688
   * ::operator<< or ::append()) to the "learned" builder---it should
689
   * *never* clear it.  It is a conjunction to add to the formula at
690
   * the top-level and may contain other theories' contributions.
691
   */
692
  virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned) { }
693
694
  enum PPAssertStatus {
695
    /** Atom has been solved  */
696
    PP_ASSERT_STATUS_SOLVED,
697
    /** Atom has not been solved */
698
    PP_ASSERT_STATUS_UNSOLVED,
699
    /** Atom is inconsistent */
700
    PP_ASSERT_STATUS_CONFLICT
701
  };
702
703
  /**
704
   * Given a literal and its proof generator (encapsulated by trust node tin),
705
   * add the solved substitutions to the map, if any. The method should return
706
   * true if the literal can be safely removed from the input problem.
707
   *
708
   * Note that tin has trude node kind LEMMA. Its proof generator should be
709
   * take into account when adding a substitution to outSubstitutions when
710
   * proofs are enabled.
711
   */
712
  virtual PPAssertStatus ppAssert(TrustNode tin,
713
                                  TrustSubstitutionMap& outSubstitutions);
714
715
  /**
716
   * Given a term of the theory coming from the input formula or
717
   * from a lemma generated during solving, this method can be overridden in a
718
   * theory implementation to rewrite the term into an equivalent form.
719
   *
720
   * This method returns a TrustNode of kind TrustNodeKind::REWRITE, which
721
   * carries information about the proof generator for the rewrite, which can
722
   * be the null TrustNode if n is unchanged.
723
   *
724
   * Notice this method is used both in the "theory rewrite equalities"
725
   * preprocessing pass, where n is an equality from the input formula,
726
   * and in theory preprocessing, where n is a (non-equality) term occurring
727
   * in the input or generated in a lemma.
728
   *
729
   * @param n the node to preprocess-rewrite.
730
   * @param lems a set of lemmas that should be added as a consequence of
731
   * preprocessing n. These are in the form of "skolem lemmas". For example,
732
   * calling this method on (div x n), we return a trust node proving:
733
   *   (= (div x n) k_div)
734
   * for fresh skolem k, and add the skolem lemma for k that indicates that
735
   * it is the division of x and n.
736
   *
737
   * Note that ppRewrite should not return WITNESS terms, since the internal
738
   * calculus works in "original forms" and not "witness forms".
739
   */
740
122299
  virtual TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
741
  {
742
122299
    return TrustNode::null();
743
  }
744
745
  /**
746
   * Notify preprocessed assertions. Called on new assertions after
747
   * preprocessing before they are asserted to theory engine.
748
   */
749
113850
  virtual void ppNotifyAssertions(const std::vector<Node>& assertions) {}
750
  //--------------------------------- end preprocessing
751
752
  /**
753
   * A Theory is called with presolve exactly one time per user
754
   * check-sat.  presolve() is called after preregistration,
755
   * rewriting, and Boolean propagation, (other theories'
756
   * propagation?), but the notified Theory has not yet had its
757
   * check() or propagate() method called.  A Theory may empty its
758
   * assertFact() queue using get().  A Theory can raise conflicts,
759
   * add lemmas, and propagate literals during presolve().
760
   *
761
   * NOTE: The presolve property must be added to the kinds file for
762
   * the theory.
763
   */
764
  virtual void presolve() { }
765
766
  /**
767
   * A Theory is called with postsolve exactly one time per user
768
   * check-sat.  postsolve() is called after the query has completed
769
   * (regardless of whether sat, unsat, or unknown), and after any
770
   * model-querying related to the query has been performed.
771
   * After this call, the theory will not get another check() or
772
   * propagate() call until presolve() is called again.  A Theory
773
   * cannot raise conflicts, add lemmas, or propagate literals during
774
   * postsolve().
775
   */
776
  virtual void postsolve() { }
777
778
  /**
779
   * Notification sent to the theory wheneven the search restarts.
780
   * Serves as a good time to do some clean-up work, and you can
781
   * assume you're at DL 0 for the purposes of Contexts.  This function
782
   * should not use the output channel.
783
   */
784
  virtual void notifyRestart() { }
785
786
  /**
787
   * Identify this theory (for debugging, dynamic configuration,
788
   * etc..)
789
   */
790
  virtual std::string identify() const = 0;
791
792
  /** Set user attribute
793
    * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
794
    *  via the syntax (! n :attr)
795
    */
796
  virtual void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) {
797
    Unimplemented() << "Theory " << identify()
798
                    << " doesn't support Theory::setUserAttribute interface";
799
  }
800
801
  typedef context::CDList<Assertion>::const_iterator assertions_iterator;
802
803
  /**
804
   * Provides access to the facts queue, primarily intended for theory
805
   * debugging purposes.
806
   *
807
   * @return the iterator to the beginning of the fact queue
808
   */
809
174377
  assertions_iterator facts_begin() const {
810
174377
    return d_facts.begin();
811
  }
812
813
  /**
814
   * Provides access to the facts queue, primarily intended for theory
815
   * debugging purposes.
816
   *
817
   * @return the iterator to the end of the fact queue
818
   */
819
820030
  assertions_iterator facts_end() const {
820
820030
    return d_facts.end();
821
  }
822
  /**
823
   * Whether facts have been asserted to this theory.
824
   *
825
   * @return true iff facts have been asserted to this theory.
826
   */
827
5393
  bool hasFacts() { return !d_facts.empty(); }
828
829
  /** Return total number of facts asserted to this theory */
830
43943
  size_t numAssertions() {
831
43943
    return d_facts.size();
832
  }
833
834
  typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
835
836
  /**
837
   * Provides access to the shared terms, primarily intended for theory
838
   * debugging purposes.
839
   *
840
   * @return the iterator to the beginning of the shared terms list
841
   */
842
171211
  shared_terms_iterator shared_terms_begin() const {
843
171211
    return d_sharedTerms.begin();
844
  }
845
846
  /**
847
   * Provides access to the facts queue, primarily intended for theory
848
   * debugging purposes.
849
   *
850
   * @return the iterator to the end of the shared terms list
851
   */
852
187979
  shared_terms_iterator shared_terms_end() const {
853
187979
    return d_sharedTerms.end();
854
  }
855
856
857
  /**
858
   * This is a utility function for constructing a copy of the currently shared terms
859
   * in a queriable form.  As this is
860
   */
861
  std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
862
863
  /**
864
   * This allows the theory to be queried for whether a literal, lit, is
865
   * entailed by the theory.  This returns a pair of a Boolean and a node E.
866
   *
867
   * If the Boolean is true, then E is a formula that entails lit and E is propositionally
868
   * entailed by the assertions to the theory.
869
   *
870
   * If the Boolean is false, it is "unknown" if lit is entailed and E may be
871
   * any node.
872
   *
873
   * The literal lit is either an atom a or (not a), which must belong to the theory:
874
   *   There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
875
   *
876
   * There are NO assumptions that a or the subterms of a have been
877
   * preprocessed in any form.  This includes ppRewrite, rewriting,
878
   * preregistering, registering, definition expansion or ITE removal!
879
   *
880
   * Theories are free to limit the amount of effort they use and so may
881
   * always opt to return "unknown".  Both "unknown" and "not entailed",
882
   * may return for E a non-boolean Node (e.g. Node::null()).  (There is no explicit output
883
   * for the negation of lit is entailed.)
884
   *
885
   * If lit is theory valid, the return result may be the Boolean constant
886
   * true for E.
887
   *
888
   * If lit is entailed by multiple assertions on the theory's getFact()
889
   * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
890
   * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
891
   *
892
   * If lit is entailed by a single assertion on the theory's getFact()
893
   * queue, say a, this may return E=a.
894
   *
895
   * The theory may always return false!
896
   *
897
   * Theories may not touch their output stream during an entailment check.
898
   *
899
   * @param  lit     a literal belonging to the theory.
900
   * @return         a pair <b,E> s.t. if b is true, then a formula E such that
901
   * E |= lit in the theory.
902
   */
903
  virtual std::pair<bool, Node> entailmentCheck(TNode lit);
904
};/* class Theory */
905
906
std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
907
908
909
14759579
inline theory::Assertion Theory::get() {
910
14759579
  Assert(!done()) << "Theory::get() called with assertion queue empty!";
911
912
  // Get the assertion
913
14759579
  Assertion fact = d_facts[d_factsHead];
914
14759579
  d_factsHead = d_factsHead + 1;
915
916
14759579
  Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
917
918
14759579
  return fact;
919
}
920
921
inline std::ostream& operator<<(std::ostream& out,
922
                                const CVC4::theory::Theory& theory) {
923
  return out << theory.identify();
924
}
925
926
inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertStatus status) {
927
  switch (status) {
928
  case theory::Theory::PP_ASSERT_STATUS_SOLVED:
929
    out << "SOLVE_STATUS_SOLVED"; break;
930
  case theory::Theory::PP_ASSERT_STATUS_UNSOLVED:
931
    out << "SOLVE_STATUS_UNSOLVED"; break;
932
  case theory::Theory::PP_ASSERT_STATUS_CONFLICT:
933
    out << "SOLVE_STATUS_CONFLICT"; break;
934
  default:
935
    Unhandled();
936
  }
937
  return out;
938
}
939
940
}/* CVC4::theory namespace */
941
}/* CVC4 namespace */
942
943
#endif /* CVC4__THEORY__THEORY_H */