CVC3  2.4.1
theory_core.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_core.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Thu Jan 30 16:58:05 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__theory_core_h_
22 #define _cvc3__include__theory_core_h_
23 
24 #include <queue>
25 #include "theory.h"
26 #include "cdmap.h"
27 #include "statistics.h"
28 #include <string>
29 #include "notifylist.h"
30 #include <vector>
31 #include <utility>
32 //#include "expr_transform.h"
33 
34 namespace CVC3 {
35 
36 class ExprTransform;
37 // class Statistics;
38 class CoreProofRules;
39 class Translator;
40 
41 /*****************************************************************************/
42 /*!
43  *\class TheoryCore
44  *\ingroup Theories
45  *\brief This theory handles the built-in logical connectives plus equality.
46  * It also handles the registration and cooperation among all other theories.
47  *
48  * Author: Clark Barrett
49  *
50  * Created: Sat Feb 8 14:54:05 2003
51  */
52 /*****************************************************************************/
53 class TheoryCore :public Theory {
54  friend class Theory;
55 
56  //! Context manager
58 
59  //! Theorem manager
61 
62  //! Core proof rules
64 
65  //! Reference to command line flags
66  const CLFlags& d_flags;
67 
68  //! Reference to statistics
70 
71  //! PrettyPrinter (we own it)
73 
74  //! Type Computer
76 
77  //! Expr Transformer
79 
80  //! Translator
82 
83  //! Assertion queue
84  std::queue<Theorem> d_queue;
85  //! Queue of facts to be sent to the SearchEngine
86  std::vector<Theorem> d_queueSE;
87 
88  //! Inconsistent flag
90  //! The set of reasons for incompleteness (empty when we are complete)
92 
93  //! Proof of inconsistent
95  //! List of all active terms in the system (for quantifier instantiation)
97  //! Map from active terms to theorems that introduced those terms
98 
100  // CDMap<Expr, Theorem> d_termTheorems;
101 
102  //! List of all active non-equality atomic formulas in the system (for quantifier instantiation)
104  //! List of variables that were created up to this point
105  std::vector<Expr> d_vars;
106  //! Database of declared identifiers
107  std::map<std::string, Expr> d_globals;
108  //! Bound variable stack: a vector of pairs <name, var>
109  std::vector<std::pair<std::string, Expr> > d_boundVarStack;
110  //! Map for bound vars
112  //! Top-level cache for parser
113  // This cache is only used when there are no bound variables
115  //! Alternative cache for parser when not at top-level
116  // This cache used when there are bound variables - and it is cleared
117  // every time the bound variable stack changes
119  //! Current cache being used for parser
121  //! Cache for tcc's
123 
124  //! Array of registered theories
125  std::vector<Theory*> d_theories;
126 
127  //! Array mapping kinds to theories
129 
130  //! The theory which has the solver (if any)
132 
133  //! Mapping of compound type variables to simpler types (model generation)
135  //! Mapping of intermediate variables to their values
137  //! List of basic variables (temporary storage for model generation)
138  std::vector<Expr> d_basicModelVars;
139  //! Mapping of basic variables to simplified expressions (temp. storage)
140  /*! There may be some vars which simplify to something else; we save
141  * those separately, and keep only those which simplify to
142  * themselves. Once the latter vars are assigned, we'll re-simplify
143  * the former variables and use the results as concrete values.
144  */
146 
147  //! Command line flag whether to simplify in place
148  const bool* d_simplifyInPlace;
149  //! Which recursive simplifier to use
151 
152  //! Resource limit (0==unlimited, 1==no more resources, >=2 - available).
153  /*! Currently, it is the number of enqueued facts. Once the
154  * resource is exhausted, the remaining facts will be dropped, and
155  * an incomplete flag is set.
156  */
157  unsigned d_resourceLimit;
158 
159  //! Time limit (0==unlimited, >0==total available cpu time in seconds).
160  /*! Currently, if exhausted processFactQueue will not perform any more
161  * reasoning with FULL effor and an incomplete flag is set.
162  */
163  unsigned d_timeBase;
164  unsigned d_timeLimit;
165 
169  bool d_inPP;
170 
171  IF_DEBUG(ExprMap<bool> d_simpStack;)
172 
173 
174  //! So we get notified every time there's a pop
175  friend class CoreNotifyObj;
178  public:
180  : ContextNotifyObj(context), d_theoryCore(tc) {}
181  void notify() { d_theoryCore->getEM()->invalidateSimpCache(); }
182  };
184 
185  //! List of implied literals, based on registered atomic formulas of interest
187 
188  //! Next index in d_impliedLiterals that has not yet been fetched
190 
191  //! List of theorems from calls to update()
192  // These are stored here until the equality lists are finished and then
193  // processed by processUpdates()
194  std::vector<Theorem> d_update_thms;
195 
196  //! List of data accompanying above theorems from calls to update()
197  std::vector<Expr> d_update_data;
198 
199  //! Notify list that gets processed on every equality
201 
202  //! Whether we are in the middle of doing updates
203  unsigned d_inUpdate;
204 
205  //! The set of named expressions to evaluate on a GET_ASSIGNMENT request
206  std::vector< std::pair<Expr, Expr> > d_assignment;
207 
208 public:
209  /***************************************************************************/
210  /*!
211  *\class CoreSatAPI
212  *\brief Interface class for callbacks to SAT from Core
213  *
214  * Author: Clark Barrett
215  *
216  * Created: Mon Dec 5 18:42:15 2005
217  */
218  /***************************************************************************/
219  class CoreSatAPI {
220  public:
222  virtual ~CoreSatAPI() {}
223  //! Add a new lemma derived by theory core
224  virtual void addLemma(const Theorem& thm, int priority = 0,
225  bool atBottomScope = false) = 0;
226  //! Add an assumption to the set of assumptions in the current context
227  /*! Assumptions have the form e |- e */
228  virtual Theorem addAssumption(const Expr& assump) = 0;
229  //! Suggest a splitter to the Sat engine
230  /*! \param e is a literal.
231  * \param priority is between -10 and 10. A priority above 0 indicates
232  * that the splitter should be favored. A priority below 0 indicates that
233  * the splitter should be delayed.
234  */
235  virtual void addSplitter(const Expr& e, int priority) = 0;
236  //! Check the validity of e in the current context
237  virtual bool check(const Expr& e) = 0;
238  };
239 private:
241 
242 private:
243  //! Private method to get a new theorem producer.
244  /*! This method is used ONLY by the TheoryCore constructor. The
245  only reason to have this method is to separate the trusted part of
246  the constructor into a separate .cpp file (Alternative is to make
247  the entire constructer trusted, which is not very safe).
248  Method is implemented in core_theorem_producer.cpp */
250 
251  // Helper functions
252 
253  //! Effort level for processFactQueue
254  /*! LOW means just process facts, don't call theory checkSat methods
255  NORMAL means call theory checkSat methods without full effort
256  FULL means call theory checkSat methods with full effort
257  */
258  typedef enum {
262  } EffortLevel;
263 
264  //! A helper function for addFact()
265  /*! Returns true if lemmas were added to search engine, false otherwise */
266  bool processFactQueue(EffortLevel effort = NORMAL);
267  //! Process a notify list triggered as a result of new theorem e
268  void processNotify(const Theorem& e, NotifyList* L);
269  //! Transitive composition of other rewrites with the above
270  Theorem rewriteCore(const Theorem& e);
271  //! Helper for registerAtom
272  void setupSubFormulas(const Expr& s, const Expr& e, const Theorem& thm);
273  //! Process updates recorded by calls to update()
274  void processUpdates();
275  /*! @brief The assumptions for e must be in H or phi. "Core" added
276  * to avoid conflict with theory interface function name
277  */
278  void assertFactCore(const Theorem& e);
279  //! Process a newly derived formula
280  void assertFormula(const Theorem& e);
281  //! Check that lhs and rhs of thm have same base type
282  IF_DEBUG(void checkRewriteType(const Theorem& thm);)
283  /*! @brief Returns phi |= e = rewriteCore(e). "Core" added to avoid
284  conflict with theory interface function name */
285  Theorem rewriteCore(const Expr& e);
286 
287  //! Set the find pointer of an atomic formula and notify SearchEngine
288  /*! \param thm is a Theorem(phi) or Theorem(NOT phi), where phi is
289  * an atomic formula to get a find pointer to TRUE or FALSE,
290  * respectively.
291  */
292  void setFindLiteral(const Theorem& thm);
293  //! Core rewrites for literals (NOT and EQ)
294  Theorem rewriteLitCore(const Expr& e);
295  //! Enqueue a fact to be sent to the SearchEngine
296  // void enqueueSE(const Theorem& thm);//yeting
297  //! Fetch the concrete assignment to the variable during model generation
298  Theorem getModelValue(const Expr& e);
299 
300  //! An auxiliary recursive function to process COND expressions into ITE
301  Expr processCond(const Expr& e, int i);
302 
303  //! Return true if no special parsing is required for this kind
304  bool isBasicKind(int kind);
305 
306  //! Helper check functions for solve
307  void checkEquation(const Theorem& thm);
308  //! Helper check functions for solve
309  void checkSolved(const Theorem& thm);
310 
311  // Time limit exhausted
312  bool timeLimitReached();
313 
314  //! Print an expression in the shared subset of SMT-LIB v1/v2
315  //! Should only be called if os.lang() is SMTLIB_LANG or SMTLIB_V2_LANG.
317 
318 
319 public:
320  //! Constructor
322  TheoremManager* tm, Translator* tr,
323  const CLFlags& flags,
324  Statistics& statistics);
325  //! Destructor
326  ~TheoryCore();
327 
328  //! Request a unit of resource
329  /*! It will be subtracted from the resource limit.
330  *
331  * \return true if resource unit is granted, false if no more
332  * resources available.
333  */
334  void getResource() {
335  getStatistics().counter("resource")++;
336  if (d_resourceLimit > 1) d_resourceLimit--;
337  }
338 
339  //! Register a SatAPI for TheoryCore
340  void registerCoreSatAPI(CoreSatAPI* coreSatAPI) { d_coreSatAPI = coreSatAPI; }
341 
342  //! Register a callback for every equality
343  void addNotifyEq(Theory* t, const Expr& e) { d_notifyEq.add(t, e); }
344 
345  //! Call theory-specific preprocess routines
347 
348  ContextManager* getCM() const { return d_cm; }
349  TheoremManager* getTM() const { return d_tm; }
350  const CLFlags& getFlags() const { return d_flags; }
351  Statistics& getStatistics() const { return d_statistics; }
353  CoreProofRules* getCoreRules() const { return d_rules; }
354  Translator* getTranslator() const { return d_translator; }
355 
356  //! Access to tcc cache (needed by theory_bitvector)
358 
359  //! Get list of terms
360  const CDList<Expr>& getTerms() { return d_terms; }
361 
362  int getCurQuantLevel();
363 
364  //! Set the flag for the preprocessor
365  void setInPP() { d_inPP = true; }
366  void clearInPP() { d_inPP = false; }
367 
368  //! Get theorem which was responsible for introducing this term
369  Theorem getTheoremForTerm(const Expr& e);
370  //! Get quantification level at which this term was introduced
371  unsigned getQuantLevelForTerm(const Expr& e);
372  //! Get list of predicates
374  //! Whether updates are being processed
375  bool inUpdate() { return d_inUpdate > 0; }
376  //! Whether its OK to add new facts (for use in rewrites)
377  bool okToEnqueue()
378  { return d_inAddFact || d_inCheckSATCore || d_inRegisterAtom || d_inPP; }
379 
380  // Implementation of Theory API
381  /*! Variables of uninterpreted types may be sent here, and they
382  should be ignored. */
383  void addSharedTerm(const Expr& e) { }
384  void assertFact(const Theorem& e);
385  void checkSat(bool fullEffort) { }
386  Theorem rewrite(const Expr& e);
387  /*! Only Boolean constants (TRUE and FALSE) and variables of
388  uninterpreted types should appear here (they come from records and
389  tuples). Just ignore them. */
390  void setup(const Expr& e) { }
391  void update(const Theorem& e, const Expr& d);
392  Theorem solve(const Theorem& e);
393 
394  Theorem simplifyOp(const Expr& e);
395  void checkType(const Expr& e);
397  bool enumerate, bool computeSize);
398  void computeType(const Expr& e);
399  Type computeBaseType(const Type& t);
400  Expr computeTCC(const Expr& e);
401  Expr computeTypePred(const Type& t,const Expr& e);
402  Expr parseExprOp(const Expr& e);
403  ExprStream& print(ExprStream& os, const Expr& e);
404 
405  //! Calls for other theories to add facts to refine a coutnerexample.
406  void refineCounterExample();
407  bool refineCounterExample(Theorem& thm);
408  void computeModelBasic(const std::vector<Expr>& v);
409 
410  // User-level API methods
411 
412  /*! @brief Add a new assertion to the core from the user or a SAT
413  solver. Do NOT use it in a decision procedure; use
414  enqueueFact(). */
415  /*! \sa enqueueFact */
416  void addFact(const Theorem& e);
417 
418  //! Top-level simplifier
419  Theorem simplify(const Expr& e);
420 
421  //! Check if the current context is inconsistent
422  bool inconsistent() { return d_inconsistent ; }
423  //! Get the proof of inconsistency for the current context
424  /*! \return Theorem(FALSE) */
426  /*! @brief To be called by SearchEngine when it believes the context
427  * is satisfiable.
428  *
429  * \return true if definitely consistent or inconsistent and false if
430  * consistency is unknown.
431  */
432  bool checkSATCore();
433 
434  //! Check if the current decision branch is marked as incomplete
435  bool incomplete() { return d_incomplete.size() > 0 ; }
436  //! Check if the branch is incomplete, and return the reasons (strings)
437  bool incomplete(std::vector<std::string>& reasons);
438 
439  //! Register an atomic formula of interest.
440  /*! If e or its negation is later deduced, we will add the implied
441  literal to d_impliedLiterals */
442  void registerAtom(const Expr& e, const Theorem& thm);
443 
444  //! Return the next implied literal (NULL Theorem if none)
446 
447  //! Return total number of implied literals
448  unsigned numImpliedLiterals() { return d_impliedLiterals.size(); }
449 
450  //! Return an implied literal by index
451  Theorem getImpliedLiteralByIndex(unsigned index);
452 
453  //! Parse the generic expression.
454  /*! This method should be used in parseExprOp() for recursive calls
455  * to subexpressions, and is the method called by the command
456  * processor.
457  */
458  Expr parseExpr(const Expr& e);
459  //! Top-level call to parseExpr, clears the bound variable stack.
460  /*! Use it in VCL instead of parseExpr(). */
461  Expr parseExprTop(const Expr& e) {
462  d_boundVarStack.clear();
463  d_parseCache = &d_parseCacheTop;
464  return parseExpr(e);
465  }
466 
467  //! Assign t a concrete value val. Used in model generation.
468  void assignValue(const Expr& t, const Expr& val);
469  //! Record a derived assignment to a variable (LHS).
470  void assignValue(const Theorem& thm);
471 
472  //! Adds expression to var database
473  void addToVarDB(const Expr & e);
474  //! Split compound vars into basic type variables
475  /*! The results are saved in d_basicModelVars and
476  * d_simplifiedModelVars. Also, add new basic vars as shared terms
477  * whenever their type belongs to a different theory than the term
478  * itself.
479  */
480  void collectBasicVars();
481  //! Calls theory specific computeModel, results are placed in map
482  void buildModel(ExprMap<Expr>& m);
483  bool buildModel(Theorem& thm);
484  //! Recursively build a compound-type variable assignment for e
485  void collectModelValues(const Expr& e, ExprMap<Expr>& m);
486 
487  //! Set the resource limit (0==unlimited).
488  void setResourceLimit(unsigned limit) { d_resourceLimit = limit; }
489  //! Get the resource limit
490  unsigned getResourceLimit() { return d_resourceLimit; }
491  //! Return true if resources are exhausted
492  bool outOfResources() { return d_resourceLimit == 1; }
493 
494  //! Initialize base time used for !setTimeLimit
495  void initTimeLimit();
496 
497  //! Set the time limit in seconds (0==unlimited).
498  void setTimeLimit(unsigned limit);
499 
500  //! Called by search engine
501  Theorem rewriteLiteral(const Expr& e);
502 
503  //! Get the value of all :named terms
505 
506  //! Get the value of an arbitrary formula or term
507  Expr getValue(Expr e);
508 
509 private:
510  // Methods provided for benefit of theories. Access is made available through theory.h
511 
512  //! Assert a system of equations (1 or more).
513  /*! e is either a single equation, or a conjunction of equations
514  */
515  void assertEqualities(const Theorem& e);
516 
517  //! Mark the branch as incomplete
518  void setIncomplete(const std::string& reason);
519 
520  //! Return a theorem for the type predicate of e
521  /*! Note: used only by theory_arith */
522  Theorem typePred(const Expr& e);
523 
524 public:
525  // TODO: These should be private
526  //! Enqueue a new fact
527  /*! not private because used in search_fast.cpp */
528  void enqueueFact(const Theorem& e);
529  void enqueueSE(const Theorem& thm);//yeting
530  // Must provide proof of inconsistency
531  /*! not private because used in search_fast.cpp */
532  void setInconsistent(const Theorem& e);
533 
534  //! Setup additional terms within a theory-specific setup().
535  /*! not private because used in theory_bitvector.cpp */
536  void setupTerm(const Expr& e, Theory* i, const Theorem& thm);
537 
538 
539 };
540 
541 //! Printing NotifyList class
542 std::ostream& operator<<(std::ostream& os, const NotifyList& l);
543 
544 }
545 
546 #endif
CDO< bool > d_inconsistent
Inconsistent flag.
Definition: theory_core.h:89
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
void setupTerm(const Expr &e, Theory *i, const Theorem &thm)
Setup additional terms within a theory-specific setup().
Theory * d_solver
The theory which has the solver (if any)
Definition: theory_core.h:131
std::hash_map< Expr, Theorem > d_termTheorems
Map from active terms to theorems that introduced those terms.
Definition: theory_core.h:99
const bool * d_simplifyInPlace
Command line flag whether to simplify in place.
Definition: theory_core.h:148
EffortLevel
Effort level for processFactQueue.
Definition: theory_core.h:258
CDList< Expr > d_terms
List of all active terms in the system (for quantifier instantiation)
Definition: theory_core.h:96
Data structure of expressions in CVC3.
Definition: expr.h:133
void assertFormula(const Theorem &e)
Process a newly derived formula.
void computeType(const Expr &e)
Compute and store the type of e.
ExprHashMap< Theorem > d_varAssignments
Mapping of intermediate variables to their values.
Definition: theory_core.h:136
TheoremManager * getTM() const
Definition: theory_core.h:349
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
CoreProofRules * createProofRules(TheoremManager *tm)
Private method to get a new theorem producer.
unsigned d_timeBase
Time limit (0==unlimited, >0==total available cpu time in seconds).
Definition: theory_core.h:163
Expr processCond(const Expr &e, int i)
An auxiliary recursive function to process COND expressions into ITE.
const CLFlags & getFlags() const
Definition: theory_core.h:350
void enqueueFact(const Theorem &e)
Enqueue a new fact.
CoreProofRules * d_rules
Core proof rules.
Definition: theory_core.h:63
ExprMap< Expr > & tccCache()
Access to tcc cache (needed by theory_bitvector)
Definition: theory_core.h:357
void addToVarDB(const Expr &e)
Adds expression to var database.
const CDList< Expr > & getPredicates()
Get list of predicates.
Definition: theory_core.h:373
TheoryCore(ContextManager *cm, ExprManager *em, TheoremManager *tm, Translator *tr, const CLFlags &flags, Statistics &statistics)
Constructor.
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
const CLFlags & d_flags
Reference to command line flags.
Definition: theory_core.h:66
void registerCoreSatAPI(CoreSatAPI *coreSatAPI)
Register a SatAPI for TheoryCore.
Definition: theory_core.h:340
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Definition: theory_core.h:385
void setupSubFormulas(const Expr &s, const Expr &e, const Theorem &thm)
Helper for registerAtom.
void setIncomplete(const std::string &reason)
Mark the branch as incomplete.
MS C++ specific settings.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
TheoremManager * d_tm
Theorem manager.
Definition: theory_core.h:60
ContextManager * d_cm
Context manager.
Definition: theory_core.h:57
virtual void addLemma(const Theorem &thm, int priority=0, bool atBottomScope=false)=0
Add a new lemma derived by theory core.
CDList< Theorem > d_impliedLiterals
List of implied literals, based on registered atomic formulas of interest.
Definition: theory_core.h:186
void initTimeLimit()
Initialize base time used for !setTimeLimit.
ExprMap< Expr > d_tccCache
Cache for tcc's.
Definition: theory_core.h:122
void enqueueSE(const Theorem &thm)
Check if the current context is inconsistent.
Translator * getTranslator() const
Definition: theory_core.h:354
std::vector< std::pair< std::string, Expr > > d_boundVarStack
Bound variable stack: a vector of pairs
Definition: theory_core.h:109
Expr parseExpr(const Expr &e)
Parse the generic expression.
bool incomplete()
Check if the current decision branch is marked as incomplete.
Definition: theory_core.h:435
virtual bool check(const Expr &e)=0
Check the validity of e in the current context.
Theorem simplifyOp(const Expr &e)
Recursive simplification step.
bool inconsistent()
Check if the current context is inconsistent.
Definition: theory_core.h:422
Theorem rewriteLiteral(const Expr &e)
Called by search engine.
Description: Counters and flags for collecting run-time statistics.
unsigned getQuantLevelForTerm(const Expr &e)
Get quantification level at which this term was introduced.
Theorem callTheoryPreprocess(const Expr &e)
Call theory-specific preprocess routines.
bool inUpdate()
Whether updates are being processed.
Definition: theory_core.h:375
CDMap< std::string, bool > d_incomplete
The set of reasons for incompleteness (empty when we are complete)
Definition: theory_core.h:91
std::vector< Theory * > d_theories
Array of registered theories.
Definition: theory_core.h:125
bool checkSATCore()
To be called by SearchEngine when it believes the context is satisfiable.
ExprTransform * d_exprTrans
Expr Transformer.
Definition: theory_core.h:78
CoreProofRules * getCoreRules() const
Definition: theory_core.h:353
std::map< std::string, Expr > d_globals
Database of declared identifiers.
Definition: theory_core.h:107
Theorem getModelValue(const Expr &e)
Enqueue a fact to be sent to the SearchEngine.
std::hash_map< int, Theory * > d_theoryMap
Array mapping kinds to theories.
Definition: theory_core.h:128
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Theorem getImpliedLiteralByIndex(unsigned index)
Return an implied literal by index.
void setInPP()
Set the flag for the preprocessor.
Definition: theory_core.h:365
void getResource()
Request a unit of resource.
Definition: theory_core.h:334
std::vector< Theorem > d_update_thms
List of theorems from calls to update()
Definition: theory_core.h:194
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
NotifyList d_notifyEq
Notify list that gets processed on every equality.
Definition: theory_core.h:200
ExprHashMap< Theorem > d_simplifiedModelVars
Mapping of basic variables to simplified expressions (temp. storage)
Definition: theory_core.h:145
void assignValue(const Expr &t, const Expr &val)
Assign t a concrete value val. Used in model generation.
Theorem simplify(const Expr &e)
Top-level simplifier.
virtual void addSplitter(const Expr &e, int priority)=0
Suggest a splitter to the Sat engine.
void refineCounterExample()
Calls for other theories to add facts to refine a coutnerexample.
ExprTransform * getExprTrans() const
Definition: theory_core.h:352
ExprMap< Expr > * d_parseCache
Current cache being used for parser.
Definition: theory_core.h:120
Abstract class for computing expr type.
Definition: expr_manager.h:183
Expr getAssignment()
Get the value of all :named terms.
Statistics & d_statistics
Reference to statistics.
Definition: theory_core.h:69
const CDList< Expr > & getTerms()
Get list of terms.
Definition: theory_core.h:360
StatCounter counter(const std::string &name)
Definition: statistics.h:163
CoreSatAPI * d_coreSatAPI
Definition: theory_core.h:240
Theorem(TheoryCore::* d_currentRecursiveSimplifier)(const Expr &)
Which recursive simplifier to use.
Definition: theory_core.h:150
ExprManager::TypeComputer * d_typeComputer
Type Computer.
Definition: theory_core.h:75
Theorem getImpliedLiteral(void)
Return the next implied literal (NULL Theorem if none)
void add(Theory *t, const Expr &e)
Definition: notifylist.h:40
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
unsigned d_inUpdate
Whether we are in the middle of doing updates.
Definition: theory_core.h:203
void collectModelValues(const Expr &e, ExprMap< Expr > &m)
Recursively build a compound-type variable assignment for e.
void assertFactCore(const Theorem &e)
The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface funct...
CDO< Theorem > d_incThm
Proof of inconsistent.
Definition: theory_core.h:94
size_t size() const
Definition: cdmap.h:171
Theorem rewriteCore(const Theorem &e)
Transitive composition of other rewrites with the above.
void collectBasicVars()
Split compound vars into basic type variables.
Interface class for callbacks to SAT from Core.
Definition: theory_core.h:219
#define IF_DEBUG(code)
Definition: debug.h:406
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
void addSharedTerm(const Expr &e)
Definition: theory_core.h:383
Expression Manager.
Definition: expr_manager.h:58
std::hash_map< std::string, Expr > d_boundVarMap
Map for bound vars.
Definition: theory_core.h:111
unsigned size() const
Definition: cdlist.h:64
void addNotifyEq(Theory *t, const Expr &e)
Register a callback for every equality.
Definition: theory_core.h:343
std::vector< Expr > d_basicModelVars
List of basic variables (temporary storage for model generation)
Definition: theory_core.h:138
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
void checkEquation(const Theorem &thm)
Helper check functions for solve.
CDO< unsigned > d_impliedLiteralsIdx
Next index in d_impliedLiterals that has not yet been fetched.
Definition: theory_core.h:189
Expr getValue(Expr e)
Get the value of an arbitrary formula or term.
void registerAtom(const Expr &e, const Theorem &thm)
Register an atomic formula of interest.
void checkType(const Expr &e)
Check that e is a valid Type expr.
void setInconsistent(const Theorem &e)
bool processFactQueue(EffortLevel effort=NORMAL)
A helper function for addFact()
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
void setResourceLimit(unsigned limit)
Set the resource limit (0==unlimited).
Definition: theory_core.h:488
ContextManager * getCM() const
Definition: theory_core.h:348
unsigned d_timeLimit
Definition: theory_core.h:164
Translator * d_translator
Translator.
Definition: theory_core.h:81
void setup(const Expr &e)
Definition: theory_core.h:390
ExprStream & printSmtLibShared(ExprStream &os, const Expr &e)
Generic API for Theories plus methods commonly used by theories.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
CoreNotifyObj d_notifyObj
Definition: theory_core.h:183
void processUpdates()
Process updates recorded by calls to update()
Theorem getTheoremForTerm(const Expr &e)
Get theorem which was responsible for introducing this term.
ExprHashMap< std::vector< Expr > > d_varModelMap
Mapping of compound type variables to simpler types (model generation)
Definition: theory_core.h:134
CoreNotifyObj(TheoryCore *tc, Context *context)
Definition: theory_core.h:179
Theorem typePred(const Expr &e)
Return a theorem for the type predicate of e.
bool outOfResources()
Return true if resources are exhausted.
Definition: theory_core.h:492
Theorem inconsistentThm()
Get the proof of inconsistency for the current context.
Definition: theory_core.h:425
void assertEqualities(const Theorem &e)
Assert a system of equations (1 or more).
ExprMap< Expr > d_parseCacheTop
Top-level cache for parser.
Definition: theory_core.h:114
std::vector< Theorem > d_queueSE
Queue of facts to be sent to the SearchEngine.
Definition: theory_core.h:86
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
Definition: expr_manager.h:341
CDList< Expr > d_predicates
List of all active non-equality atomic formulas in the system (for quantifier instantiation) ...
Definition: theory_core.h:103
std::queue< Theorem > d_queue
Assertion queue.
Definition: theory_core.h:84
unsigned d_resourceLimit
Resource limit (0==unlimited, 1==no more resources, >=2 - available).
Definition: theory_core.h:157
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
void processNotify(const Theorem &e, NotifyList *L)
Process a notify list triggered as a result of new theorem e.
unsigned numImpliedLiterals()
Return total number of implied literals.
Definition: theory_core.h:448
PrettyPrinter * d_printer
PrettyPrinter (we own it)
Definition: theory_core.h:72
bool okToEnqueue()
Whether its OK to add new facts (for use in rewrites)
Definition: theory_core.h:377
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
Definition: expr.cpp:35
Expr parseExprTop(const Expr &e)
Top-level call to parseExpr, clears the bound variable stack.
Definition: theory_core.h:461
void setFindLiteral(const Theorem &thm)
Set the find pointer of an atomic formula and notify SearchEngine.
~TheoryCore()
Destructor.
std::vector< Expr > d_vars
List of variables that were created up to this point.
Definition: theory_core.h:105
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
void update(const Theorem &e, const Expr &d)
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Theorem solve(const Theorem &e)
std::vector< std::pair< Expr, Expr > > d_assignment
The set of named expressions to evaluate on a GET_ASSIGNMENT request.
Definition: theory_core.h:206
ExprMap< Expr > d_parseCacheOther
Alternative cache for parser when not at top-level.
Definition: theory_core.h:118
virtual Theorem addAssumption(const Expr &assump)=0
Add an assumption to the set of assumptions in the current context.
std::vector< Expr > d_update_data
List of data accompanying above theorems from calls to update()
Definition: theory_core.h:197
Abstract API to a pretty-printer for Expr.
Statistics & getStatistics() const
Definition: theory_core.h:351
bool isBasicKind(int kind)
Return true if no special parsing is required for this kind.
void buildModel(ExprMap< Expr > &m)
Calls theory specific computeModel, results are placed in map.
Theorem rewriteLitCore(const Expr &e)
Core rewrites for literals (NOT and EQ)
unsigned getResourceLimit()
Get the resource limit.
Definition: theory_core.h:490
void checkSolved(const Theorem &thm)
Helper check functions for solve.
void setTimeLimit(unsigned limit)
Set the time limit in seconds (0==unlimited).