CVC3  2.4.1
theory.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory.h
4  * \brief Generic API for Theories plus methods commonly used by theories
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Sat Nov 30 23:30:15 2002
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__include__theory_h_
23 #define _cvc3__include__theory_h_
24 
25 #include "expr_stream.h"
26 #include "common_proof_rules.h"
27 #include "cdlist.h"
28 
29 namespace CVC3 {
30 
31 class TheoryCore;
32 class Theorem;
33 class Type;
34 
35 /************************************************************************/
36 /*!
37  *\defgroup Theories Theories
38  *\ingroup VC
39  *\brief Theories
40  *@{
41  */
42 /***********************************************************************/
43 
44 /*****************************************************************************/
45 /*!
46  *\anchor Theory
47  *\class Theory
48  *\brief Base class for theories
49  *
50  * Author: Clark Barrett
51  *
52  * Created: Thu Jan 30 16:37:56 2003
53  *
54  * This is an abstract class which all theories should inherit from. In
55  * addition to providing an abstract theory interface, it provides access
56  * functions to core functionality. However, in order to avoid duplicating the
57  * data structures which implement this functionality, all the functionality is
58  * stored in a separate class (which actually derives from this one) called
59  * TheoryCore. These two classes work closely together to provide the core
60  * functionality.
61  */
62 /*****************************************************************************/
63 
64 class Theory {
65  friend class TheoryCore;
66 private:
68  TheoryCore* d_theoryCore; //!< Provides the core functionality
69  CommonProofRules* d_commonRules; //!< Commonly used proof rules
70  std::string d_name; //!< Name of the theory (for debugging)
71 
72  //! Private default constructor.
73  /*! Everyone besides TheoryCore has to use the public constructor
74  which sets up all the provided functionality automatically.
75  */
76  Theory(void);
77 
78 protected:
79  bool d_theoryUsed; //! Whether theory has been used (for smtlib translator)
80 
81 public:
82  //! Exposed constructor.
83  /*! Note that each instance of Theory must have a name (mostly for
84  debugging purposes). */
85  Theory(TheoryCore* theoryCore, const std::string& name);
86  //! Destructor
87  virtual ~Theory(void);
88 
89  //! Access to ExprManager
90  ExprManager* getEM() { return d_em; }
91 
92  //! Get a pointer to theoryCore
94 
95  //! Get a pointer to common proof rules
97 
98  //! Get the name of the theory (for debugging purposes)
99  const std::string& getName() const { return d_name; }
100 
101  //! Set the "used" flag on this theory (for smtlib translator)
102  virtual void setUsed() { d_theoryUsed = true; }
103  //! Get whether theory has been used (for smtlib translator)
104  virtual bool theoryUsed() { return d_theoryUsed; }
105 
106  /***************************************************************************/
107  /*!
108  *\defgroup Theory_API Abstract Theory Interface
109  *\anchor theory_api
110  *\ingroup Theories
111  *\brief Abstract Theory Interface
112  *
113  * These are the theory-specific methods which provide the decision procedure
114  * functionality for a new theory. At the very least, a theory must
115  * implement the checkSat method. The other methods can be used to make the
116  * implementation more convenient. For more information on this API, see
117  * Clark Barrett's PhD dissertation and \ref theory_api_howto.
118  *@{
119  */
120  /***************************************************************************/
121 
122  //! Notify theory of a new shared term
123  /*! When a term e associated with theory i occurs as a child of an expression
124  associated with theory j, the framework calls i->addSharedTerm(e) and
125  j->addSharedTerm(e)
126  */
127  virtual void addSharedTerm(const Expr& e) {}
128 
129  //! Assert a new fact to the decision procedure
130  /*! Each fact that makes it into the core framework is assigned to exactly
131  one theory: the theory associated with that fact. assertFact is called to
132  inform the theory that a new fact has been assigned to the theory.
133  */
134  virtual void assertFact(const Theorem& e) = 0;
135 
136  //! Check for satisfiability in the theory
137  /*! \param fullEffort when it is false, checkSat can do as much or
138  as little work as it likes, though simple inferences and checks for
139  consistency should be done to increase efficiency. If fullEffort is true,
140  checkSat must check whether the set of facts given by assertFact together
141  with the arrangement of shared terms (provided by addSharedTerm) induced by
142  the global find database equivalence relation are satisfiable. If
143  satisfiable, checkSat does nothing.
144 
145  If satisfiability can be acheived by merging some of the shared terms, a new
146  fact must be enqueued using enqueueFact (this fact need not be a literal).
147  If there is no way to make things satisfiable, setInconsistent must be called.
148  */
149  virtual void checkSat(bool fullEffort) = 0;
150 
151  //! Theory-specific rewrite rules.
152  /*! By default, rewrite just returns a reflexive theorem stating that the
153  input expression is equivalent to itself. However, rewrite is allowed to
154  return any theorem which describes how the input expression is equivalent
155  to some new expression. rewrite should be used to perform simplifications,
156  normalization, and any other preprocessing on theory-specific expressions
157  that needs to be done.
158  */
159  virtual Theorem rewrite(const Expr& e) { return reflexivityRule(e); }
160 
161  //! Theory-specific preprocessing
162  /*! This gets called each time a new assumption or query is preprocessed.
163  By default it does nothing. */
164  virtual Theorem theoryPreprocess(const Expr& e) { return reflexivityRule(e); }
165 
166  //! Set up the term e for call-backs when e or its children change.
167  /*! setup is called once for each expression associated with the theory. It
168  is typically used to setup theory-specific data for an expression and to
169  add call-back information for use with update.
170  \sa update
171  */
172  virtual void setup(const Expr& e) {}
173 
174  //! Notify a theory of a new equality
175  /*! update is a call-back used by the notify mechanism of the core theory.
176  It works as follows. When an equation t1 = t2 makes it into the core
177  framework, the two find equivalence classes for t1 and t2 are merged. The
178  result is that t2 is the new equivalence class representative and t1 is no
179  longer an equivalence class representative. When this happens, the notify
180  list of t1 is traversed. Notify list entries consist of a theory and an
181  expression d. For each entry (i,d), i->update(e, d) is called, where e is
182  the theorem corresponding to the equality t1=t2.
183 
184  To add the entry (i,d) to a term t1's notify list, a call must be made to
185  t1.addNotify(i,d). This is typically done in setup.
186 
187  \sa setup
188  */
189  virtual void update(const Theorem& e, const Expr& d) {}
190 
191  //! An optional solver.
192  /*! The solve method can be used to implement a Shostak-style solver. Since
193  solvers do not in general combine, the following technique is used. One
194  theory is designated as the primary solver (in our case, it is the theory
195  of arithmetic). For each equation that enters the core framework, the
196  primary solver is called to ensure that the equation is in solved form with
197  respect to the primary theory.
198 
199  After the primary solver, the solver for the theory associated with the
200  equation is called. This solver can do whatever it likes, as long as the
201  result is still in solved form with respect to the primary solver. This is
202  a slight generalization of what is described in my (Clark)'s PhD thesis.
203  */
204  virtual Theorem solve(const Theorem& e) { return e; }
205  //! A debug check used by the primary solver
206  virtual void checkAssertEqInvariant(const Theorem& e) { }
207 
208  /////////////////////////////////
209  // Extensions to original API: //
210  /////////////////////////////////
211 
212  //! Recursive simplification step
213  /*!
214  * INVARIANT: the result is a Theorem(e=e'), where e' is a fully
215  * simplified version of e. To simplify subexpressions recursively,
216  * call simplify() function.
217  *
218  * This theory-specific method is called when the simplifier
219  * descends top-down into the expression. Normally, every kid is
220  * simplified recursively, and the results are combined into the new
221  * parent with the same operator (Op). This functionality is
222  * provided with the default implementation.
223  *
224  * However, in some expressions some kids may not matter in the
225  * result, and can be skipped. For instance, if the first kid in a
226  * long AND simplifies to FALSE, then the entire expression
227  * simplifies to FALSE, and the remaining kids do not need to be
228  * simplified.
229  *
230  * This call is a chance for a DP to provide these types of
231  * optimizations during the top-down phase of simplification.
232  */
233  virtual Theorem simplifyOp(const Expr& e);
234 
235  //! Check that e is a valid Type expr
236  virtual void checkType(const Expr& e)
237  { throw Exception("Cannot construct type from expr: "+e.toString()); }
238 
239  //! Compute information related to finiteness of types
240  /*! Used by the TypeComputer defined in TheoryCore (theories should not call this
241  * funtion directly -- they should use the methods in Type instead). Each theory
242  * should implement this if it contains any types that could be non-infinite.
243  *
244  * 1. Returns Cardinality of the type (finite, infinite, or unknown)
245  * 2. If cardinality = finite and enumerate is true,
246  * sets e to the nth element of the type if it can
247  * sets e to NULL if n is out of bounds or if unable to compute nth element
248  * 3. If cardinality = finite and computeSize is true,
249  * sets n to the size of the type if it can
250  * sets n to 0 otherwise
251  */
253  bool enumerate, bool computeSize)
254  { return CARD_INFINITE; }
255 
256  //! Compute and store the type of e
257  /*!
258  * \param e is the expression whose type is computed.
259  *
260  * This function computes the type of the top-level operator of e,
261  * and recurses into children using getType(), if necessary.
262  */
263  virtual void computeType(const Expr& e) {}
264  //! Compute the base type of the top-level operator of an arbitrary type
265  virtual Type computeBaseType(const Type& tp) { return tp; }
266  /*! @brief Theory specific computation of the subtyping predicate for
267  * type t applied to the expression e.
268  */
269  /*! By default returns true. Each theory needs to compute subtype predicates
270  * for the types associated with it. So, for example, the theory of records
271  * will take a record type [# f1: T1, f2: T2 #] and an expression e
272  * and will return the subtyping predicate for e, namely:
273  * computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2)
274  */
275  virtual Expr computeTypePred(const Type& t, const Expr& e)
276  { return e.getEM()->trueExpr(); }
277  //! Compute and cache the TCC of e.
278  /*!
279  * \param e is an expression (term or formula). This function
280  * computes the TCC of e which is true iff the expression is defined.
281  *
282  * This function computes the TCC or predicate of the top-level
283  * operator of e, and recurses into children using getTCC(), if
284  * necessary.
285  *
286  * The default implementation is to compute TCCs recursively for all
287  * children, and return their conjunction.
288  */
289  virtual Expr computeTCC(const Expr& e);
290 
291  //! Theory-specific parsing implemented by the DP
292  virtual Expr parseExprOp(const Expr& e) { return e; }
293 
294  //! Theory-specific pretty-printing.
295  /*! By default, print the top node in AST, and resume
296  pretty-printing the children. The same call e.print(os) can be
297  used in DP-specific printers to use AST printing for the given
298  node. In fact, it is strongly recommended to add e.print(os) as
299  the default for all the cases/kinds that are not handled by the
300  particular pretty-printer.
301  */
302  virtual ExprStream& print(ExprStream& os, const Expr& e) {
303  return e.printAST(os);
304  }
305 
306  //! Add variables from 'e' to 'v' for constructing a concrete model
307  /*! If e is already of primitive type, do NOT add it to v. */
308  virtual void computeModelTerm(const Expr& e, std::vector<Expr>& v);
309  //! Process disequalities from the arrangement for model generation
310  virtual void refineCounterExample() {}
311  //! Assign concrete values to basic-type variables in v
312  virtual void computeModelBasic(const std::vector<Expr>& v) {}
313  //! Compute the value of a compound variable from the more primitive ones
314  /*! The more primitive variables for e are already assigned concrete
315  * values, and are available through getModelValue().
316  *
317  * The new value for e must be assigned using assignValue() method.
318  *
319  * \param e is the compound type expression to assign a value;
320  *
321  * \param vars are the variables actually assigned. Normally, 'e'
322  * is the only element of vars. However, e.g. in the case of
323  * uninterpreted functions, assigning 'f' means assigning all
324  * relevant applications of 'f' to constant values (f(0), f(5),
325  * etc.). Such applications might not be known before the model is
326  * constructed (they may be of the form f(x), f(y+z), etc., where
327  * x,y,z are still unassigned).
328  *
329  * Populating 'vars' is an opportunity for a DP to change the set of
330  * top-level "variables" to assign, if needed. In particular, it
331  * may drop 'e' from the model entirely, if it is already a concrete
332  * value by itself.
333  */
334  virtual void computeModel(const Expr& e, std::vector<Expr>& vars) {
335  assignValue(find(e));
336  vars.push_back(e);
337  }
338 
339  //! Receives all the type predicates for the types of the given theory
340  /*! Type predicates may be expensive to enqueue eagerly, and DPs may
341  choose to postpone them, or transform them to something more
342  efficient. By default, the asserted type predicate is
343  immediately enqueued as a new fact.
344 
345  Note: Used only by bitvector theory.
346 
347  \param e is the expression for which the type predicate is computed
348  \param pred is the predicate theorem P(e)
349  */
350  virtual void assertTypePred(const Expr& e, const Theorem& pred)
351  { enqueueFact(pred); }
352 
353  //! Theory-specific rewrites for atomic formulas
354  /*! The intended use is to convert complex atomic formulas into an
355  * equivalent Boolean combination of simpler formulas. Such
356  * conversion may be harmful for algebraic rewrites, and is not
357  * always desirable to have in rewrite() method.
358  *
359  * Note: Used only by bitvector theory and rewriteLiteral in core.
360  *
361  * However, if rewrite() alone cannot solve the problem, and the SAT
362  * solver needs to be envoked, these additional rewrites may ease
363  * the job for the SAT solver.
364  */
365  virtual Theorem rewriteAtomic(const Expr& e) { return reflexivityRule(e); }
366 
367  //! Notification of conflict
368  /*!
369  * Decision procedures implement this method when they want to be
370  * notified about a conflict.
371  *
372  * Note: Used only by quantifier theory
373  *
374  * \param thm is the theorem of FALSE given to setInconsistent()
375  */
376  virtual void notifyInconsistent(const Theorem& thm) { }
377 
378  virtual void registerAtom(const Expr& e, const Theorem& thm);
379 
380  //! Theory-specific registration of atoms
381  /*!
382  * If a theory wants to implement its own theory propagation, it
383  * should implement this method and use it to collect all atoms
384  * that the core is interested in. If the theory can deduce the atom
385  * or its negation, it should do so (using enqueueFact).
386  */
387  virtual void registerAtom(const Expr& e) { }
388 
389 
390 #ifdef _CVC3_DEBUG_MODE
391  //! Theory-specific debug function
392  virtual void debug(int i) { }
393  //! help function, as debug(int i). yeting
394  virtual int help(int i) { return 9999 ;} ;
395 #endif
396 
397  /*@}*/ // End of Theory_API group
398 
399  /***************************************************************************/
400  /*!
401  *\name Core Framework Functionality
402  * These methods provide convenient access to core functionality for the
403  * benefit of decision procedures.
404  *@{
405  */
406  /***************************************************************************/
407 
408  //! Check if the current context is inconsistent
409  virtual bool inconsistent();
410  //! Make the context inconsistent; The formula proved by e must FALSE.
411  virtual void setInconsistent(const Theorem& e);
412 
413  //! Mark the current decision branch as possibly incomplete
414  /*!
415  * This should be set when a decision procedure uses an incomplete
416  * algorithm, and cannot guarantee satisfiability after the final
417  * checkSat() call with full effort. An example would be
418  * instantiation of universal quantifiers.
419  *
420  * A decision procedure can provide a reason for incompleteness,
421  * which will be reported back to the user.
422  */
423  virtual void setIncomplete(const std::string& reason);
424 
425  //! Simplify a term e and return a Theorem(e==e')
426  /*! \sa simplifyExpr() */
427  virtual Theorem simplify(const Expr& e);
428  //! Simplify a term e w.r.t. the current context
429  /*! \sa simplify */
431  { return simplify(e).getRHS(); }
432 
433  //! Submit a derived fact to the core from a decision procedure
434  /*! \param e is the Theorem for the new fact
435  */
436  virtual void enqueueFact(const Theorem& e);
437  virtual void enqueueSE(const Theorem& e);
438 
439  //! Handle new equalities (usually asserted through addFact)
440  /*!
441  * INVARIANT: the Theorem 'e' is an equality e1==e2, where e2 is
442  * i-leaf simplified in the current context, or a conjunction of
443  * such equalities.
444  *
445  */
446  virtual void assertEqualities(const Theorem& e);
447 
448  //! Parse the generic expression.
449  /*! This method should be used in parseExprOp() for recursive calls
450  * to subexpressions, and is the method called by the command
451  * processor.
452  */
453  virtual Expr parseExpr(const Expr& e);
454 
455  //! Assigns t a concrete value val. Used in model generation.
456  virtual void assignValue(const Expr& t, const Expr& val);
457  //! Record a derived assignment to a variable (LHS).
458  virtual void assignValue(const Theorem& thm);
459 
460  /*@}*/ // End of Core Framework Functionality
461 
462  /***************************************************************************/
463  /*!
464  *\name Theory Helper Methods
465  * These methods provide basic functionality needed by all theories.
466  *@{
467  */
468  /***************************************************************************/
469 
470  //! Register new kinds with the given theory
471  void registerKinds(Theory* theory, std::vector<int>& kinds);
472  //! Unregister kinds for a theory
473  void unregisterKinds(Theory* theory, std::vector<int>& kinds);
474  //! Register a new theory
475  void registerTheory(Theory* theory, std::vector<int>& kinds,
476  bool hasSolver=false);
477  //! Unregister a theory
478  void unregisterTheory(Theory* theory, std::vector<int>& kinds,
479  bool hasSolver);
480 
481  //! Return the number of registered theories
482  int getNumTheories();
483 
484  //! Test whether a kind maps to any theory
485  bool hasTheory(int kind);
486  //! Return the theory associated with a kind
487  Theory* theoryOf(int kind);
488  //! Return the theory associated with a type
489  Theory* theoryOf(const Type& e);
490  //! Return the theory associated with an Expr
491  Theory* theoryOf(const Expr& e);
492 
493  //! Return the theorem that e is equal to its find
494  Theorem find(const Expr& e);
495  //! Return the find as a reference: expr must have a find
496  const Theorem& findRef(const Expr& e);
497 
498  //! Return find-reduced version of e
499  Theorem findReduce(const Expr& e);
500  //! Return true iff e is find-reduced
501  bool findReduced(const Expr& e);
502  //! Return the find of e, or e if it has no find
503  inline Expr findExpr(const Expr& e)
504  { return e.hasFind() ? find(e).getRHS() : e; }
505 
506  //! Compute the TCC of e, or the subtyping predicate, if e is a type
507  Expr getTCC(const Expr& e);
508  //! Compute (or look up in cache) the base type of e and return the result
509  Type getBaseType(const Expr& e);
510  //! Compute the base type from an arbitrary type
511  Type getBaseType(const Type& tp);
512  //! Calls the correct theory to compute a type predicate
513  Expr getTypePred(const Type& t, const Expr& e);
514 
515  //! Update the children of the term e
516  /*! When a decision procedure receives a call to update() because a
517  child of a term 'e' has changed, this method can be called to
518  compute the new value of 'e'.
519  \sa update
520  */
521  Theorem updateHelper(const Expr& e);
522  //! Setup a term for congruence closure (must have sig and rep attributes)
523  void setupCC(const Expr& e);
524  //! Update a term w.r.t. congruence closure (must be setup with setupCC())
525  void updateCC(const Theorem& e, const Expr& d);
526  //! Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
527  Theorem rewriteCC(const Expr& e);
528 
529  /*! @brief Calls the correct theory to get all of the terms that
530  need to be assigned values in the concrete model */
531  void getModelTerm(const Expr& e, std::vector<Expr>& v);
532  //! Fetch the concrete assignment to the variable during model generation
533  Theorem getModelValue(const Expr& e);
534 
535  //! Suggest a splitter to the SearchEngine
536  void addSplitter(const Expr& e, int priority = 0);
537 
538  //! Add a global lemma
539  void addGlobalLemma(const Theorem& thm, int priority = 0);
540 
541  /*@}*/ // End of Theory Helper Methods
542 
543  /***************************************************************************/
544  /*!
545  *\name Core Testers
546  *@{
547  */
548  /***************************************************************************/
549 
550  //! Test if e is an i-leaf term for the current theory
551  /*! A term 'e' is an i-leaf for a theory 'i', if it is a variable,
552  or 'e' belongs to a different theory. This definition makes sense
553  for a larger term which by itself belongs to the current theory
554  'i', but (some of) its children are variables or belong to
555  different theories. */
556  bool isLeaf(const Expr& e) { return e.isVar() || theoryOf(e) != this; }
557 
558  //! Test if e1 is an i-leaf in e2
559  /*! \sa isLeaf */
560  bool isLeafIn(const Expr& e1, const Expr& e2);
561 
562  //! Test if all i-leaves of e are simplified
563  /*! \sa isLeaf */
564  bool leavesAreSimp(const Expr& e);
565 
566  /*@}*/ // End of Core Testers
567 
568  /***************************************************************************/
569  /*!
570  *\name Common Type and Expr Methods
571  *@{
572  */
573  /***************************************************************************/
574 
575  //! Return BOOLEAN type
577 
578  //! Return FALSE Expr
579  const Expr& falseExpr() { return d_em->falseExpr(); }
580 
581  //! Return TRUE Expr
582  const Expr& trueExpr() { return d_em->trueExpr(); }
583 
584  //! Create a new variable given its name and type
585  /*! Add the variable to the database for resolving IDs in parseExpr
586  */
587  Expr newVar(const std::string& name, const Type& type);
588  //! Create a new named expression given its name, type, and definition
589  /*! Add the definition to the database for resolving IDs in parseExpr
590  */
591  Expr newVar(const std::string& name, const Type& type, const Expr& def);
592 
593  //! Create a new uninterpreted function
594  /*! Add the definition to the database for resolving IDs in parseExpr
595  */
596  Op newFunction(const std::string& name, const Type& type,
597  bool computeTransClosure);
598 
599  //! Look up a function by name.
600  /*! Returns the function and sets type to the type of the function if it
601  * exists. If not, returns a NULL Op object.
602  */
603  Op lookupFunction(const std::string& name, Type* type);
604 
605  //! Create a new defined function
606  /*! Add the definition to the database for resolving IDs in parseExpr
607  */
608  Op newFunction(const std::string& name, const Type& type, const Expr& def);
609 
610  //! Create and add a new bound variable to the stack, for parseExprOp().
611  /*!
612  * The stack is popped automatically upon return from the
613  * parseExprOp() which used this method.
614  *
615  * Bound variable names may repeat, in which case the latest
616  * declaration takes precedence.
617  */
618  Expr addBoundVar(const std::string& name, const Type& type);
619  //! Create and add a new bound named def to the stack, for parseExprOp().
620  /*!
621  * The stack is popped automatically upon return from the
622  * parseExprOp() which used this method.
623  *
624  * Bound variable names may repeat, in which case the latest
625  * declaration takes precedence.
626  *
627  * The type may be Null, but 'def' must always be a valid Expr
628  */
629  Expr addBoundVar(const std::string& name, const Type& type, const Expr& def);
630 
631  /*! @brief Lookup variable and return it and its type. Return NULL Expr if
632  it doesn't exist yet. */
633  Expr lookupVar(const std::string& name, Type* type);
634 
635  //! Create a new uninterpreted type with the given name
636  /*! Add the name to the global variable database d_globals
637  */
638  Type newTypeExpr(const std::string& name);
639  //! Lookup type by name. Return Null if no such type exists.
640  Type lookupTypeExpr(const std::string& name);
641  //! Create a new type abbreviation with the given name
642  Type newTypeExpr(const std::string& name, const Type& def);
643 
644  //! Create a new subtype expression
645  Type newSubtypeExpr(const Expr& pred, const Expr& witness);
646 
647  //! Resolve an identifier, for use in parseExprOp()
648  /*!
649  * First, search the bound variable stack, and if the name is not
650  * found, search the global constant and type declarations.
651  *
652  * \return an expression to use in place of the identifier, or Null
653  * if cannot resolve the name.
654  */
655  Expr resolveID(const std::string& name);
656 
657  //! Install name as a new identifier associated with Expr e
658  void installID(const std::string& name, const Expr& e);
659 
660  Theorem typePred(const Expr& e);
661 
662  /*@}*/ // End of Common Type and Expr Methods
663 
664  /***************************************************************************/
665  /*!
666  *\name Commonly Used Proof Rules
667  *\anchor theory_api_core_proof_rules
668  *@{
669  */
670  /***************************************************************************/
671 
672  //! ==> a == a
674  { return d_commonRules->reflexivityRule(a); }
675 
676  //! a1 == a2 ==> a2 == a1
677  Theorem symmetryRule(const Theorem& a1_eq_a2)
678  { return d_commonRules->symmetryRule(a1_eq_a2); }
679 
680  //! (a1 == a2) & (a2 == a3) ==> (a1 == a3)
682  const Theorem& a2_eq_a3)
683  { return d_commonRules->transitivityRule(a1_eq_a2, a2_eq_a3); }
684 
685  //! (c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
687  const std::vector<Theorem>& thms)
688  { return d_commonRules->substitutivityRule(op, thms); }
689 
690  //! Special case for unary operators
692  const Theorem& t)
693  { return d_commonRules->substitutivityRule(e, t); }
694 
695  //! Special case for binary operators
697  const Theorem& t1,
698  const Theorem& t2)
699  { return d_commonRules->substitutivityRule(e, t1, t2); }
700 
701  //! Optimized: only positions which changed are included
703  const std::vector<unsigned>& changed,
704  const std::vector<Theorem>& thms)
705  { return d_commonRules->substitutivityRule(e, changed, thms); }
706 
707  //! Optimized: only a single position changed
709  int changed,
710  const Theorem& thm)
711  { return d_commonRules->substitutivityRule(e, changed, thm); }
712 
713  //! e1 AND (e1 IFF e2) ==> e2
714  Theorem iffMP(const Theorem& e1, const Theorem& e1_iff_e2) {
715  return d_commonRules->iffMP(e1, e1_iff_e2);
716  }
717 
718  //! ==> AND(e1,e2) IFF [simplified expr]
719  Theorem rewriteAnd(const Expr& e) {
720  return d_commonRules->rewriteAnd(e);
721  }
722 
723  //! ==> OR(e1,...,en) IFF [simplified expr]
724  Theorem rewriteOr(const Expr& e) {
725  return d_commonRules->rewriteOr(e);
726  }
727 
728  //! Derived rule for rewriting ITE
729  Theorem rewriteIte(const Expr& e);
730 
731  //! Derived rule to create a new name for an expression
732  Theorem renameExpr(const Expr& e);
733 
734  /*@}*/ // End of Commonly Used Proof Rules
735 
736 
737 };
738 
739 /*@}*/ // End of group Theories
740 
741 }
742 
743 #endif
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
Definition: theory.cpp:119
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
Definition: theory.cpp:519
TheoryCore * d_theoryCore
Provides the core functionality.
Definition: theory.h:68
virtual void setUsed()
Set the "used" flag on this theory (for smtlib translator)
Definition: theory.h:102
virtual Theorem rewriteAtomic(const Expr &e)
Theory-specific rewrites for atomic formulas.
Definition: theory.h:365
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
Definition: expr.cpp:400
TheoryCore * theoryCore()
Get a pointer to theoryCore.
Definition: theory.h:93
bool leavesAreSimp(const Expr &e)
Test if all i-leaves of e are simplified.
Definition: theory.cpp:557
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Definition: theory.h:312
Theorem typePred(const Expr &e)
Return BOOLEAN type.
Definition: theory.cpp:918
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
Definition: theory.cpp:148
bool isLeafIn(const Expr &e1, const Expr &e2)
Test if e1 is an i-leaf in e2.
Definition: theory.cpp:546
ExprManager * getEM() const
Definition: expr.h:1156
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
bool isLeaf(const Expr &e)
Test if e is an i-leaf term for the current theory.
Definition: theory.h:556
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
Definition: theory.cpp:142
virtual void setInconsistent(const Theorem &e)
Make the context inconsistent; The formula proved by e must FALSE.
Definition: theory.cpp:103
virtual void setIncomplete(const std::string &reason)
Mark the current decision branch as possibly incomplete.
Definition: theory.cpp:112
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
Definition: theory.cpp:459
Theorem substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2)
Special case for binary operators.
Definition: theory.h:696
bool hasTheory(int kind)
Test whether a kind maps to any theory.
Definition: theory.cpp:247
Type newSubtypeExpr(const Expr &pred, const Expr &witness)
Create a new subtype expression.
Definition: theory.cpp:816
std::string d_name
Name of the theory (for debugging)
Definition: theory.h:70
Expr resolveID(const std::string &name)
Resolve an identifier, for use in parseExprOp()
Definition: theory.cpp:887
virtual Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
Definition: theory.h:275
MS C++ specific settings.
Definition: type.h:42
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
Definition: theory.cpp:128
Base class for theories.
Definition: theory.h:64
virtual Theorem rewriteAnd(const Expr &e)=0
==> AND(e1,e2) IFF [simplified expr]
virtual void enqueueSE(const Theorem &e)
Check if the current context is inconsistent.
Definition: theory.cpp:134
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
Definition: theory.h:252
void unregisterTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver)
Unregister a theory.
Definition: theory.cpp:224
Theorem substitutivityRule(const Expr &e, int changed, const Theorem &thm)
Optimized: only a single position changed.
Definition: theory.h:708
virtual Theorem reflexivityRule(const Expr &a)=0
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
Definition: theory.h:719
bool hasFind() const
Definition: expr.h:1232
void registerKinds(Theory *theory, std::vector< int > &kinds)
Register new kinds with the given theory.
Definition: theory.cpp:177
virtual void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Definition: theory.h:172
virtual void checkType(const Expr &e)
Check that e is a valid Type expr.
Definition: theory.h:236
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Definition: theory.cpp:203
virtual ~Theory(void)
Destructor.
Definition: theory.cpp:44
Theorem renameExpr(const Expr &e)
Derived rule to create a new name for an expression.
Definition: theory.cpp:935
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
Definition: theory.h:714
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
Definition: theory.cpp:162
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
Definition: theory.h:96
Type lookupTypeExpr(const std::string &name)
Lookup type by name. Return Null if no such type exists.
Definition: theory.cpp:805
Op newFunction(const std::string &name, const Type &type, bool computeTransClosure)
Create a new uninterpreted function.
Definition: theory.cpp:647
void addGlobalLemma(const Theorem &thm, int priority=0)
Add a global lemma.
Definition: theory.cpp:157
bool d_theoryUsed
Definition: theory.h:79
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory.cpp:81
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
Theorem rewriteCC(const Expr &e)
Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
Definition: theory.cpp:512
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
virtual void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Definition: theory.h:334
Expr newVar(const std::string &name, const Type &type)
Create a new variable given its name and type.
Definition: theory.cpp:569
void unregisterKinds(Theory *theory, std::vector< int > &kinds)
Unregister kinds for a theory.
Definition: theory.cpp:190
virtual void computeType(const Expr &e)
Compute and store the type of e.
Definition: theory.h:263
virtual void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Definition: theory.h:127
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Definition: theory.h:292
const Expr & falseExpr()
FALSE Expr.
Definition: expr_manager.h:278
virtual void registerAtom(const Expr &e)
Theory-specific registration of atoms.
Definition: theory.h:387
virtual void assertFact(const Theorem &e)=0
Assert a new fact to the decision procedure.
Theorem substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)
Optimized: only positions which changed are included.
Definition: theory.h:702
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
Expr simplifyExpr(const Expr &e)
Simplify a term e w.r.t. the current context.
Definition: theory.h:430
const Expr & getRHS() const
Definition: theorem.cpp:246
const std::string & getName() const
Get the name of the theory (for debugging purposes)
Definition: theory.h:99
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
Definition: theory.h:503
const Theorem & findRef(const Expr &e)
Return the find as a reference: expr must have a find.
Definition: theory.cpp:295
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Definition: theory.cpp:541
Type newTypeExpr(const std::string &name)
Create a new uninterpreted type with the given name.
Definition: theory.cpp:790
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
Definition: theory.cpp:406
const Expr & trueExpr()
TRUE Expr.
Definition: expr_manager.h:280
const Expr & falseExpr()
Return FALSE Expr.
Definition: theory.h:579
const Expr & trueExpr()
Return TRUE Expr.
Definition: theory.h:582
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
Definition: theory.cpp:709
virtual ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Definition: theory.h:302
Expression Manager.
Definition: expr_manager.h:58
virtual Type computeBaseType(const Type &tp)
Compute the base type of the top-level operator of an arbitrary type.
Definition: theory.h:265
virtual void assertTypePred(const Expr &e, const Theorem &pred)
Receives all the type predicates for the types of the given theory.
Definition: theory.h:350
void installID(const std::string &name, const Expr &e)
Install name as a new identifier associated with Expr e.
Definition: theory.cpp:910
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
virtual void checkSat(bool fullEffort)=0
Check for satisfiability in the theory.
void getModelTerm(const Expr &e, std::vector< Expr > &v)
Calls the correct theory to get all of the terms that need to be assigned values in the concrete mode...
Definition: theory.cpp:527
virtual Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Definition: theory.h:159
virtual Theorem solve(const Theorem &e)
An optional solver.
Definition: theory.h:204
Theorem updateHelper(const Expr &e)
Update the children of the term e.
Definition: theory.cpp:417
virtual void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
Definition: theory.h:206
virtual bool theoryUsed()
Get whether theory has been used (for smtlib translator)
Definition: theory.h:104
Op lookupFunction(const std::string &name, Type *type)
Look up a function by name.
Definition: theory.cpp:697
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Definition: theory.cpp:383
void updateCC(const Theorem &e, const Expr &d)
Update a term w.r.t. congruence closure (must be setup with setupCC())
Definition: theory.cpp:473
virtual void refineCounterExample()
Process disequalities from the arrangement for model generation.
Definition: theory.h:310
virtual Theorem simplifyOp(const Expr &e)
Recursive simplification step.
Definition: theory.cpp:53
bool findReduced(const Expr &e)
Return true iff e is find-reduced.
Definition: theory.cpp:357
Theorem findReduce(const Expr &e)
Return find-reduced version of e.
Definition: theory.cpp:327
int getNumTheories()
Return the number of registered theories.
Definition: theory.cpp:241
virtual bool inconsistent()
Check if the current context is inconsistent.
Definition: theory.cpp:97
virtual void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Definition: theory.cpp:47
Type boolType()
Return BOOLEAN type.
Definition: theory.h:576
bool isVar() const
Definition: expr.h:1005
virtual void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Definition: theory.h:189
virtual Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0
(same for IFF)
ExprManager * d_em
Definition: theory.h:67
Expr getTCC(const Expr &e)
Compute the TCC of e, or the subtyping predicate, if e is a type.
Definition: theory.cpp:367
virtual void registerAtom(const Expr &e, const Theorem &thm)
Definition: theory.cpp:91
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
Theorem rewriteIte(const Expr &e)
Derived rule for rewriting ITE.
Definition: theory.cpp:923
virtual Theorem theoryPreprocess(const Expr &e)
Theory-specific preprocessing.
Definition: theory.h:164
Theorem reflexivityRule(const Expr &a)
==> a == a
Definition: theory.h:673
Theorem rewriteOr(const Expr &e)
==> OR(e1,...,en) IFF [simplified expr]
Definition: theory.h:724
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Definition: theory.h:686
CommonProofRules * d_commonRules
Commonly used proof rules.
Definition: theory.h:69
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
Expr lookupVar(const std::string &name, Type *type)
Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Definition: theory.cpp:776
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Definition: theory.cpp:252
virtual void notifyInconsistent(const Theorem &thm)
Notification of conflict.
Definition: theory.h:376
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
Definition: theory.cpp:310
virtual Theorem symmetryRule(const Theorem &a1_eq_a2)=0
(same for IFF)
virtual Theorem rewriteOr(const Expr &e)=0
==> OR(e1,...,en) IFF [simplified expr]
Theory(void)
Private default constructor.
Definition: theory.cpp:33
static Type typeBool(ExprManager *em)
Definition: type.h:73
Theorem substitutivityRule(const Expr &e, const Theorem &t)
Special case for unary operators.
Definition: theory.h:691
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
Definition: theory.h:677