CVC3

theory_core.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_core.h
00004  *
00005  * Author: Clark Barrett
00006  *
00007  * Created: Thu Jan 30 16:58:05 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  *
00016  * <hr>
00017  *
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__include__theory_core_h_
00022 #define _cvc3__include__theory_core_h_
00023 
00024 #include <queue>
00025 #include "theory.h"
00026 #include "cdmap.h"
00027 #include "statistics.h"
00028 #include <string>
00029 #include "notifylist.h"
00030 #include <vector>
00031 #include <utility>
00032 //#include "expr_transform.h"
00033 
00034 namespace CVC3 {
00035 
00036 class ExprTransform;
00037 // class Statistics;
00038 class CoreProofRules;
00039 class Translator;
00040 
00041 /*****************************************************************************/
00042 /*!
00043  *\class TheoryCore
00044  *\ingroup Theories
00045  *\brief This theory handles the built-in logical connectives plus equality.
00046  * It also handles the registration and cooperation among all other theories.
00047  *
00048  * Author: Clark Barrett
00049  *
00050  * Created: Sat Feb 8 14:54:05 2003
00051  */
00052 /*****************************************************************************/
00053 class TheoryCore :public Theory {
00054   friend class Theory;
00055 
00056   //! Context manager
00057   ContextManager* d_cm;
00058 
00059   //! Theorem manager
00060   TheoremManager* d_tm;
00061 
00062   //! Core proof rules
00063   CoreProofRules* d_rules;
00064 
00065   //! Reference to command line flags
00066   const CLFlags& d_flags;
00067 
00068   //! Reference to statistics
00069   Statistics& d_statistics;
00070 
00071   //! PrettyPrinter (we own it)
00072   PrettyPrinter* d_printer;
00073 
00074   //! Type Computer
00075   ExprManager::TypeComputer* d_typeComputer;
00076 
00077   //! Expr Transformer
00078   ExprTransform* d_exprTrans;
00079 
00080   //! Translator
00081   Translator* d_translator;
00082 
00083   //! Assertion queue
00084   std::queue<Theorem> d_queue;
00085   //! Queue of facts to be sent to the SearchEngine
00086   std::vector<Theorem> d_queueSE;
00087 
00088   //! Inconsistent flag
00089   CDO<bool> d_inconsistent;
00090   //! The set of reasons for incompleteness (empty when we are complete)
00091   CDMap<std::string, bool> d_incomplete;
00092 
00093   //! Proof of inconsistent
00094   CDO<Theorem> d_incThm;
00095   //! List of all active terms in the system (for quantifier instantiation)
00096   CDList<Expr> d_terms;
00097   //! Map from active terms to theorems that introduced those terms
00098 
00099   std::hash_map<Expr, Theorem> d_termTheorems;
00100   //  CDMap<Expr, Theorem> d_termTheorems;
00101 
00102   //! List of all active non-equality atomic formulas in the system (for quantifier instantiation)
00103   CDList<Expr> d_predicates;
00104   //! List of variables that were created up to this point
00105   std::vector<Expr> d_vars;
00106   //! Database of declared identifiers
00107   std::map<std::string, Expr> d_globals;
00108   //! Bound variable stack: a vector of pairs <name, var>
00109   std::vector<std::pair<std::string, Expr> > d_boundVarStack;
00110   //! Map for bound vars
00111   std::hash_map<std::string, Expr> d_boundVarMap;
00112   //! Top-level cache for parser
00113   // This cache is only used when there are no bound variables
00114   ExprMap<Expr> d_parseCacheTop;
00115   //! Alternative cache for parser when not at top-level
00116   // This cache used when there are bound variables - and it is cleared
00117   // every time the bound variable stack changes
00118   ExprMap<Expr> d_parseCacheOther;
00119   //! Current cache being used for parser
00120   ExprMap<Expr>* d_parseCache;
00121   //! Cache for tcc's
00122   ExprMap<Expr> d_tccCache;
00123 
00124   //! Array of registered theories
00125   std::vector<Theory*> d_theories;
00126 
00127   //! Array mapping kinds to theories
00128   std::hash_map<int, Theory*> d_theoryMap;
00129 
00130   //! The theory which has the solver (if any)
00131   Theory* d_solver;
00132 
00133   //! Mapping of compound type variables to simpler types (model generation)
00134   ExprHashMap<std::vector<Expr> > d_varModelMap;
00135   //! Mapping of intermediate variables to their values
00136   ExprHashMap<Theorem> d_varAssignments;
00137   //! List of basic variables (temporary storage for model generation)
00138   std::vector<Expr> d_basicModelVars;
00139   //! Mapping of basic variables to simplified expressions (temp. storage)
00140   /*! There may be some vars which simplify to something else; we save
00141    * those separately, and keep only those which simplify to
00142    * themselves.  Once the latter vars are assigned, we'll re-simplify
00143    * the former variables and use the results as concrete values.
00144   */
00145   ExprHashMap<Theorem> d_simplifiedModelVars;
00146 
00147   //! Command line flag whether to simplify in place
00148   const bool* d_simplifyInPlace;
00149   //! Which recursive simplifier to use
00150   Theorem (TheoryCore::*d_currentRecursiveSimplifier)(const Expr&);
00151 
00152   //! Resource limit (0==unlimited, 1==no more resources, >=2 - available).
00153   /*! Currently, it is the number of enqueued facts.  Once the
00154    * resource is exhausted, the remaining facts will be dropped, and
00155    * an incomplete flag is set.
00156    */
00157   unsigned d_resourceLimit;
00158 
00159   //! Time limit (0==unlimited, >0==total available cpu time in seconds).
00160   /*! Currently, if exhausted processFactQueue will not perform any more
00161    * reasoning with FULL effor and an incomplete flag is set.
00162    */
00163   unsigned d_timeBase;
00164   unsigned d_timeLimit;
00165 
00166   bool d_inCheckSATCore;
00167   bool d_inAddFact;
00168   bool d_inRegisterAtom;
00169   bool d_inPP;
00170 
00171   IF_DEBUG(ExprMap<bool> d_simpStack;)
00172 
00173 
00174   //! So we get notified every time there's a pop
00175   friend class CoreNotifyObj;
00176   class CoreNotifyObj :public ContextNotifyObj {
00177     TheoryCore* d_theoryCore;
00178   public:
00179     CoreNotifyObj(TheoryCore* tc, Context* context)
00180       : ContextNotifyObj(context), d_theoryCore(tc) {}
00181     void notify() { d_theoryCore->getEM()->invalidateSimpCache(); }
00182   };
00183   CoreNotifyObj d_notifyObj;
00184 
00185   //! List of implied literals, based on registered atomic formulas of interest
00186   CDList<Theorem> d_impliedLiterals;
00187 
00188   //! Next index in d_impliedLiterals that has not yet been fetched
00189   CDO<unsigned> d_impliedLiteralsIdx;
00190 
00191   //! List of theorems from calls to update()
00192   // These are stored here until the equality lists are finished and then
00193   // processed by processUpdates()
00194   std::vector<Theorem> d_update_thms;
00195 
00196   //! List of data accompanying above theorems from calls to update()
00197   std::vector<Expr> d_update_data;
00198 
00199   //! Notify list that gets processed on every equality
00200   NotifyList d_notifyEq;
00201 
00202   //! Whether we are in the middle of doing updates
00203   unsigned d_inUpdate;
00204 
00205   //! The set of named expressions to evaluate on a GET_ASSIGNMENT request
00206   std::vector< std::pair<Expr, Expr> > d_assignment;
00207 
00208 public:
00209   /***************************************************************************/
00210   /*!
00211    *\class CoreSatAPI
00212    *\brief Interface class for callbacks to SAT from Core
00213    *
00214    * Author: Clark Barrett
00215    *
00216    * Created: Mon Dec  5 18:42:15 2005
00217    */
00218   /***************************************************************************/
00219   class CoreSatAPI {
00220   public:
00221     CoreSatAPI() {}
00222     virtual ~CoreSatAPI() {}
00223     //! Add a new lemma derived by theory core
00224     virtual void addLemma(const Theorem& thm, int priority = 0,
00225                           bool atBottomScope = false) = 0;
00226     //! Add an assumption to the set of assumptions in the current context
00227     /*! Assumptions have the form e |- e */
00228     virtual Theorem addAssumption(const Expr& assump) = 0;
00229     //! Suggest a splitter to the Sat engine
00230     /*! \param e is a literal.
00231      * \param priority is between -10 and 10.  A priority above 0 indicates
00232      * that the splitter should be favored.  A priority below 0 indicates that
00233      * the splitter should be delayed.
00234      */
00235     virtual void addSplitter(const Expr& e, int priority) = 0;
00236     //! Check the validity of e in the current context
00237     virtual bool check(const Expr& e) = 0;
00238   };
00239 private:
00240   CoreSatAPI* d_coreSatAPI;
00241 
00242 private:
00243   //! Private method to get a new theorem producer.
00244   /*! This method is used ONLY by the TheoryCore constructor.  The
00245     only reason to have this method is to separate the trusted part of
00246     the constructor into a separate .cpp file (Alternative is to make
00247     the entire constructer trusted, which is not very safe).
00248     Method is implemented in core_theorem_producer.cpp  */
00249   CoreProofRules* createProofRules(TheoremManager* tm);
00250 
00251   // Helper functions
00252 
00253   //! Effort level for processFactQueue
00254   /*! LOW means just process facts, don't call theory checkSat methods
00255       NORMAL means call theory checkSat methods without full effort
00256       FULL means call theory checkSat methods with full effort
00257   */
00258   typedef enum {
00259     LOW,
00260     NORMAL,
00261     FULL
00262   } EffortLevel;
00263 
00264   //! A helper function for addFact()
00265   /*! Returns true if lemmas were added to search engine, false otherwise */
00266   bool processFactQueue(EffortLevel effort = NORMAL);
00267   //! Process a notify list triggered as a result of new theorem e
00268   void processNotify(const Theorem& e, NotifyList* L);
00269   //! Transitive composition of other rewrites with the above
00270   Theorem rewriteCore(const Theorem& e);
00271   //! Helper for registerAtom
00272   void setupSubFormulas(const Expr& s, const Expr& e, const Theorem& thm);
00273   //! Process updates recorded by calls to update()
00274   void processUpdates();
00275   /*! @brief The assumptions for e must be in H or phi.  "Core" added
00276    * to avoid conflict with theory interface function name
00277    */
00278   void assertFactCore(const Theorem& e);
00279   //! Process a newly derived formula
00280   void assertFormula(const Theorem& e);
00281   //! Check that lhs and rhs of thm have same base type
00282   IF_DEBUG(void checkRewriteType(const Theorem& thm);)
00283   /*! @brief Returns phi |= e = rewriteCore(e).  "Core" added to avoid
00284     conflict with theory interface function name */
00285   Theorem rewriteCore(const Expr& e);
00286 
00287   //! Set the find pointer of an atomic formula and notify SearchEngine
00288   /*! \param thm is a Theorem(phi) or Theorem(NOT phi), where phi is
00289    * an atomic formula to get a find pointer to TRUE or FALSE,
00290    * respectively.
00291    */
00292   void setFindLiteral(const Theorem& thm);
00293   //! Core rewrites for literals (NOT and EQ)
00294   Theorem rewriteLitCore(const Expr& e);
00295   //! Enqueue a fact to be sent to the SearchEngine
00296   //  void enqueueSE(const Theorem& thm);//yeting
00297   //! Fetch the concrete assignment to the variable during model generation
00298   Theorem getModelValue(const Expr& e);
00299 
00300   //! An auxiliary recursive function to process COND expressions into ITE
00301   Expr processCond(const Expr& e, int i);
00302 
00303   //! Return true if no special parsing is required for this kind
00304   bool isBasicKind(int kind);
00305 
00306   //! Helper check functions for solve
00307   void checkEquation(const Theorem& thm);
00308   //! Helper check functions for solve
00309   void checkSolved(const Theorem& thm);
00310 
00311   // Time limit exhausted
00312   bool timeLimitReached();
00313 
00314   //! Print an expression in the shared subset of SMT-LIB v1/v2
00315   //! Should only be called if os.lang() is SMTLIB_LANG or SMTLIB_V2_LANG.
00316   ExprStream& printSmtLibShared(ExprStream& os, const Expr& e);
00317 
00318 
00319 public:
00320   //! Constructor
00321   TheoryCore(ContextManager* cm, ExprManager* em,
00322              TheoremManager* tm, Translator* tr,
00323              const CLFlags& flags,
00324              Statistics& statistics);
00325   //! Destructor
00326   ~TheoryCore();
00327 
00328   //! Request a unit of resource
00329   /*! It will be subtracted from the resource limit.
00330    *
00331    * \return true if resource unit is granted, false if no more
00332    * resources available.
00333    */
00334   void getResource() {
00335       getStatistics().counter("resource")++;
00336       if (d_resourceLimit > 1) d_resourceLimit--;
00337   }
00338 
00339   //! Register a SatAPI for TheoryCore
00340   void registerCoreSatAPI(CoreSatAPI* coreSatAPI) { d_coreSatAPI = coreSatAPI; }
00341 
00342   //! Register a callback for every equality
00343   void addNotifyEq(Theory* t, const Expr& e) { d_notifyEq.add(t, e); }
00344 
00345   //! Call theory-specific preprocess routines
00346   Theorem callTheoryPreprocess(const Expr& e);
00347 
00348   ContextManager* getCM() const { return d_cm; }
00349   TheoremManager* getTM() const { return d_tm; }
00350   const CLFlags& getFlags() const { return d_flags; }
00351   Statistics& getStatistics() const { return d_statistics; }
00352   ExprTransform* getExprTrans() const { return d_exprTrans; }
00353   CoreProofRules* getCoreRules() const { return d_rules; }
00354   Translator* getTranslator() const { return d_translator; }
00355 
00356   //! Access to tcc cache (needed by theory_bitvector)
00357   ExprMap<Expr>& tccCache() { return d_tccCache; }
00358 
00359   //! Get list of terms
00360   const CDList<Expr>& getTerms() { return d_terms; }
00361 
00362   int getCurQuantLevel();
00363 
00364   //! Set the flag for the preprocessor
00365   void setInPP() { d_inPP = true; }
00366   void clearInPP() { d_inPP = false; }
00367 
00368   //! Get theorem which was responsible for introducing this term
00369   Theorem getTheoremForTerm(const Expr& e);
00370   //! Get quantification level at which this term was introduced
00371   unsigned getQuantLevelForTerm(const Expr& e);
00372   //! Get list of predicates
00373   const CDList<Expr>& getPredicates() { return d_predicates; }
00374   //! Whether updates are being processed
00375   bool inUpdate() { return d_inUpdate > 0; }
00376   //! Whether its OK to add new facts (for use in rewrites)
00377   bool okToEnqueue()
00378     { return d_inAddFact || d_inCheckSATCore || d_inRegisterAtom || d_inPP; }
00379 
00380   // Implementation of Theory API
00381   /*! Variables of uninterpreted types may be sent here, and they
00382     should be ignored. */
00383   void addSharedTerm(const Expr& e) { }
00384   void assertFact(const Theorem& e);
00385   void checkSat(bool fullEffort) { }
00386   Theorem rewrite(const Expr& e);
00387   /*! Only Boolean constants (TRUE and FALSE) and variables of
00388     uninterpreted types should appear here (they come from records and
00389     tuples).  Just ignore them. */
00390   void setup(const Expr& e) { }
00391   void update(const Theorem& e, const Expr& d);
00392   Theorem solve(const Theorem& e);
00393 
00394   Theorem simplifyOp(const Expr& e);
00395   void checkType(const Expr& e);
00396   Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00397                              bool enumerate, bool computeSize);
00398   void computeType(const Expr& e);
00399   Type computeBaseType(const Type& t);
00400   Expr computeTCC(const Expr& e);
00401   Expr computeTypePred(const Type& t,const Expr& e);
00402   Expr parseExprOp(const Expr& e);
00403   ExprStream& print(ExprStream& os, const Expr& e);
00404 
00405   //! Calls for other theories to add facts to refine a coutnerexample.
00406   void refineCounterExample();
00407   bool refineCounterExample(Theorem& thm);
00408   void computeModelBasic(const std::vector<Expr>& v);
00409 
00410   // User-level API methods
00411 
00412   /*! @brief Add a new assertion to the core from the user or a SAT
00413     solver.  Do NOT use it in a decision procedure; use
00414     enqueueFact(). */
00415   /*! \sa enqueueFact */
00416   void addFact(const Theorem& e);
00417 
00418   //! Top-level simplifier
00419   Theorem simplify(const Expr& e);
00420 
00421   //! Check if the current context is inconsistent
00422   bool inconsistent() { return d_inconsistent ; }
00423   //! Get the proof of inconsistency for the current context
00424   /*! \return Theorem(FALSE) */
00425   Theorem inconsistentThm() { return d_incThm; }
00426   /*! @brief To be called by SearchEngine when it believes the context
00427    * is satisfiable.
00428    *
00429    * \return true if definitely consistent or inconsistent and false if
00430    * consistency is unknown.
00431    */
00432   bool checkSATCore();
00433 
00434   //! Check if the current decision branch is marked as incomplete
00435   bool incomplete() { return d_incomplete.size() > 0 ; }
00436   //! Check if the branch is incomplete, and return the reasons (strings)
00437   bool incomplete(std::vector<std::string>& reasons);
00438 
00439   //! Register an atomic formula of interest.
00440   /*! If e or its negation is later deduced, we will add the implied
00441       literal to d_impliedLiterals */
00442   void registerAtom(const Expr& e, const Theorem& thm);
00443 
00444   //! Return the next implied literal (NULL Theorem if none)
00445   Theorem getImpliedLiteral(void);
00446 
00447   //! Return total number of implied literals
00448   unsigned numImpliedLiterals() { return d_impliedLiterals.size(); }
00449 
00450   //! Return an implied literal by index
00451   Theorem getImpliedLiteralByIndex(unsigned index);
00452 
00453   //! Parse the generic expression.
00454   /*! This method should be used in parseExprOp() for recursive calls
00455    *  to subexpressions, and is the method called by the command
00456    *  processor.
00457    */
00458   Expr parseExpr(const Expr& e);
00459   //! Top-level call to parseExpr, clears the bound variable stack.
00460   /*! Use it in VCL instead of parseExpr(). */
00461   Expr parseExprTop(const Expr& e) {
00462     d_boundVarStack.clear();
00463     d_parseCache = &d_parseCacheTop;
00464     return parseExpr(e);
00465   }
00466 
00467   //! Assign t a concrete value val.  Used in model generation.
00468   void assignValue(const Expr& t, const Expr& val);
00469   //! Record a derived assignment to a variable (LHS).
00470   void assignValue(const Theorem& thm);
00471 
00472   //! Adds expression to var database
00473   void addToVarDB(const Expr & e);
00474   //! Split compound vars into basic type variables
00475   /*! The results are saved in d_basicModelVars and
00476    *  d_simplifiedModelVars.  Also, add new basic vars as shared terms
00477    *  whenever their type belongs to a different theory than the term
00478    *  itself.
00479    */
00480   void collectBasicVars();
00481   //! Calls theory specific computeModel, results are placed in map
00482   void buildModel(ExprMap<Expr>& m);
00483   bool buildModel(Theorem& thm);
00484   //! Recursively build a compound-type variable assignment for e
00485   void collectModelValues(const Expr& e, ExprMap<Expr>& m);
00486 
00487   //! Set the resource limit (0==unlimited).
00488   void setResourceLimit(unsigned limit) { d_resourceLimit = limit; }
00489   //! Get the resource limit
00490   unsigned getResourceLimit() { return d_resourceLimit; }
00491   //! Return true if resources are exhausted
00492   bool outOfResources() { return d_resourceLimit == 1; }
00493 
00494   //! Initialize base time used for !setTimeLimit
00495   void initTimeLimit();
00496 
00497   //! Set the time limit in seconds (0==unlimited).
00498   void setTimeLimit(unsigned limit);
00499 
00500   //! Called by search engine
00501   Theorem rewriteLiteral(const Expr& e);
00502 
00503   //! Get the value of all :named terms
00504   Expr getAssignment();
00505 
00506   //! Get the value of an arbitrary formula or term
00507   Expr getValue(Expr e);
00508 
00509 private:
00510   // Methods provided for benefit of theories.  Access is made available through theory.h
00511 
00512   //! Assert a system of equations (1 or more).
00513   /*! e is either a single equation, or a conjunction of equations
00514    */
00515   void assertEqualities(const Theorem& e);
00516 
00517   //! Mark the branch as incomplete
00518   void setIncomplete(const std::string& reason);
00519 
00520   //! Return a theorem for the type predicate of e
00521   /*! Note: used only by theory_arith */
00522   Theorem typePred(const Expr& e);
00523 
00524 public:
00525   // TODO: These should be private
00526   //! Enqueue a new fact
00527   /*! not private because used in search_fast.cpp */
00528   void enqueueFact(const Theorem& e);
00529   void enqueueSE(const Theorem& thm);//yeting
00530   // Must provide proof of inconsistency
00531   /*! not private because used in search_fast.cpp */
00532   void setInconsistent(const Theorem& e);
00533 
00534   //! Setup additional terms within a theory-specific setup().
00535   /*! not private because used in theory_bitvector.cpp */
00536   void setupTerm(const Expr& e, Theory* i, const Theorem& thm);
00537 
00538 
00539 };
00540 
00541 //! Printing NotifyList class
00542 std::ostream& operator<<(std::ostream& os, const NotifyList& l);
00543 
00544 }
00545 
00546 #endif