CVC3
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) {}
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()
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();
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