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 57 ContextManager* d_cm; 58 59 //! Theorem manager 60 TheoremManager* d_tm; 61 62 //! Core proof rules 63 CoreProofRules* d_rules; 64 65 //! Reference to command line flags 66 const CLFlags& d_flags; 67 68 //! Reference to statistics 69 Statistics& d_statistics; 70 71 //! PrettyPrinter (we own it) 72 PrettyPrinter* d_printer; 73 74 //! Type Computer 75 ExprManager::TypeComputer* d_typeComputer; 76 77 //! Expr Transformer 78 ExprTransform* d_exprTrans; 79 80 //! Translator 81 Translator* d_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 89 CDO<bool> d_inconsistent; 90 //! The set of reasons for incompleteness (empty when we are complete) 91 CDMap<std::string, bool> d_incomplete; 92 93 //! Proof of inconsistent 94 CDO<Theorem> d_incThm; 95 //! List of all active terms in the system (for quantifier instantiation) 96 CDList<Expr> d_terms; 97 //! Map from active terms to theorems that introduced those terms 98 99 std::hash_map<Expr, Theorem> d_termTheorems; 100 // CDMap<Expr, Theorem> d_termTheorems; 101 102 //! List of all active non-equality atomic formulas in the system (for quantifier instantiation) 103 CDList<Expr> d_predicates; 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 111 std::hash_map<std::string, Expr> d_boundVarMap; 112 //! Top-level cache for parser 113 // This cache is only used when there are no bound variables 114 ExprMap<Expr> d_parseCacheTop; 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 118 ExprMap<Expr> d_parseCacheOther; 119 //! Current cache being used for parser 120 ExprMap<Expr>* d_parseCache; 121 //! Cache for tcc's 122 ExprMap<Expr> d_tccCache; 123 124 //! Array of registered theories 125 std::vector<Theory*> d_theories; 126 127 //! Array mapping kinds to theories 128 std::hash_map<int, Theory*> d_theoryMap; 129 130 //! The theory which has the solver (if any) 131 Theory* d_solver; 132 133 //! Mapping of compound type variables to simpler types (model generation) 134 ExprHashMap<std::vector<Expr> > d_varModelMap; 135 //! Mapping of intermediate variables to their values 136 ExprHashMap<Theorem> d_varAssignments; 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 */ 145 ExprHashMap<Theorem> d_simplifiedModelVars; 146 147 //! Command line flag whether to simplify in place 148 const bool* d_simplifyInPlace; 149 //! Which recursive simplifier to use 150 Theorem (TheoryCore::*d_currentRecursiveSimplifier)(const Expr&); 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 166 bool d_inCheckSATCore; 167 bool d_inAddFact; 168 bool d_inRegisterAtom; 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; 176 class CoreNotifyObj :public ContextNotifyObj { 177 TheoryCore* d_theoryCore; 178 public: CoreNotifyObj(TheoryCore * tc,Context * context)179 CoreNotifyObj(TheoryCore* tc, Context* context) 180 : ContextNotifyObj(context), d_theoryCore(tc) {} notify()181 void notify() { d_theoryCore->getEM()->invalidateSimpCache(); } 182 }; 183 CoreNotifyObj d_notifyObj; 184 185 //! List of implied literals, based on registered atomic formulas of interest 186 CDList<Theorem> d_impliedLiterals; 187 188 //! Next index in d_impliedLiterals that has not yet been fetched 189 CDO<unsigned> d_impliedLiteralsIdx; 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 200 NotifyList d_notifyEq; 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: CoreSatAPI()221 CoreSatAPI() {} ~CoreSatAPI()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: 240 CoreSatAPI* d_coreSatAPI; 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 */ 249 CoreProofRules* createProofRules(TheoremManager* tm); 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 { 259 LOW, 260 NORMAL, 261 FULL 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. 316 ExprStream& printSmtLibShared(ExprStream& os, const Expr& e); 317 318 319 public: 320 //! Constructor 321 TheoryCore(ContextManager* cm, ExprManager* em, 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 */ getResource()334 void getResource() { 335 getStatistics().counter("resource")++; 336 if (d_resourceLimit > 1) d_resourceLimit--; 337 } 338 339 //! Register a SatAPI for TheoryCore registerCoreSatAPI(CoreSatAPI * coreSatAPI)340 void registerCoreSatAPI(CoreSatAPI* coreSatAPI) { d_coreSatAPI = coreSatAPI; } 341 342 //! Register a callback for every equality addNotifyEq(Theory * t,const Expr & e)343 void addNotifyEq(Theory* t, const Expr& e) { d_notifyEq.add(t, e); } 344 345 //! Call theory-specific preprocess routines 346 Theorem callTheoryPreprocess(const Expr& e); 347 getCM()348 ContextManager* getCM() const { return d_cm; } getTM()349 TheoremManager* getTM() const { return d_tm; } getFlags()350 const CLFlags& getFlags() const { return d_flags; } getStatistics()351 Statistics& getStatistics() const { return d_statistics; } getExprTrans()352 ExprTransform* getExprTrans() const { return d_exprTrans; } getCoreRules()353 CoreProofRules* getCoreRules() const { return d_rules; } getTranslator()354 Translator* getTranslator() const { return d_translator; } 355 356 //! Access to tcc cache (needed by theory_bitvector) tccCache()357 ExprMap<Expr>& tccCache() { return d_tccCache; } 358 359 //! Get list of terms getTerms()360 const CDList<Expr>& getTerms() { return d_terms; } 361 362 int getCurQuantLevel(); 363 364 //! Set the flag for the preprocessor setInPP()365 void setInPP() { d_inPP = true; } clearInPP()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 getPredicates()373 const CDList<Expr>& getPredicates() { return d_predicates; } 374 //! Whether updates are being processed inUpdate()375 bool inUpdate() { return d_inUpdate > 0; } 376 //! Whether its OK to add new facts (for use in rewrites) okToEnqueue()377 bool okToEnqueue() 378 { return d_inAddFact || d_inCheckSATCore || d_inRegisterAtom || d_inPP; } 379 380 // Implementation of Theory API 381 /*! Variables of uninterpreted types may be sent here, and they 382 should be ignored. */ addSharedTerm(const Expr & e)383 void addSharedTerm(const Expr& e) { } 384 void assertFact(const Theorem& e); checkSat(bool fullEffort)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. */ setup(const Expr & e)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); 396 Cardinality finiteTypeInfo(Expr& e, Unsigned& n, 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 inconsistent()422 bool inconsistent() { return d_inconsistent ; } 423 //! Get the proof of inconsistency for the current context 424 /*! \return Theorem(FALSE) */ inconsistentThm()425 Theorem inconsistentThm() { return d_incThm; } 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 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) 445 Theorem getImpliedLiteral(void); 446 447 //! Return total number of implied literals numImpliedLiterals()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(). */ parseExprTop(const Expr & e)461 Expr parseExprTop(const Expr& e) { 462 d_boundVarStack.clear(); 463 d_parseCache = &d_parseCacheTop; 464 return parseExpr(e); 465 } 466 467 //! Assign t a concrete value val. Used in model generation. 468 void assignValue(const Expr& t, const Expr& val); 469 //! Record a derived assignment to a variable (LHS). 470 void assignValue(const Theorem& thm); 471 472 //! Adds expression to var database 473 void addToVarDB(const Expr & e); 474 //! Split compound vars into basic type variables 475 /*! The results are saved in d_basicModelVars and 476 * d_simplifiedModelVars. Also, add new basic vars as shared terms 477 * whenever their type belongs to a different theory than the term 478 * itself. 479 */ 480 void collectBasicVars(); 481 //! Calls theory specific computeModel, results are placed in map 482 void buildModel(ExprMap<Expr>& m); 483 bool buildModel(Theorem& thm); 484 //! Recursively build a compound-type variable assignment for e 485 void collectModelValues(const Expr& e, ExprMap<Expr>& m); 486 487 //! Set the resource limit (0==unlimited). setResourceLimit(unsigned limit)488 void setResourceLimit(unsigned limit) { d_resourceLimit = limit; } 489 //! Get the resource limit getResourceLimit()490 unsigned getResourceLimit() { return d_resourceLimit; } 491 //! Return true if resources are exhausted outOfResources()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 504 Expr getAssignment(); 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 547