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