1 /********************* */ 2 /*! \file smt_engine.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Andrew Reynolds, Haniel Barbosa 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief SmtEngine: the main public entry point of libcvc4. 13 ** 14 ** SmtEngine: the main public entry point of libcvc4. 15 **/ 16 17 #include "cvc4_public.h" 18 19 #ifndef __CVC4__SMT_ENGINE_H 20 #define __CVC4__SMT_ENGINE_H 21 22 #include <string> 23 #include <vector> 24 25 #include "base/modal_exception.h" 26 #include "context/cdhashmap_forward.h" 27 #include "context/cdhashset_forward.h" 28 #include "context/cdlist_forward.h" 29 #include "expr/expr.h" 30 #include "expr/expr_manager.h" 31 #include "expr/expr_stream.h" 32 #include "options/options.h" 33 #include "proof/unsat_core.h" 34 #include "smt/logic_exception.h" 35 #include "smt_util/lemma_channels.h" 36 #include "theory/logic_info.h" 37 #include "util/hash.h" 38 #include "util/proof.h" 39 #include "util/result.h" 40 #include "util/sexpr.h" 41 #include "util/statistics.h" 42 #include "util/unsafe_interrupt_exception.h" 43 44 // In terms of abstraction, this is below (and provides services to) 45 // ValidityChecker and above (and requires the services of) 46 // PropEngine. 47 48 namespace CVC4 { 49 50 template <bool ref_count> class NodeTemplate; 51 typedef NodeTemplate<true> Node; 52 typedef NodeTemplate<false> TNode; 53 struct NodeHashFunction; 54 55 class Command; 56 class GetModelCommand; 57 58 class SmtEngine; 59 class DecisionEngine; 60 class TheoryEngine; 61 62 class ProofManager; 63 64 class Model; 65 class LogicRequest; 66 class StatisticsRegistry; 67 68 namespace context { 69 class Context; 70 class UserContext; 71 }/* CVC4::context namespace */ 72 73 namespace preprocessing { 74 class PreprocessingPassContext; 75 } 76 77 namespace prop { 78 class PropEngine; 79 }/* CVC4::prop namespace */ 80 81 namespace smt { 82 /** 83 * Representation of a defined function. We keep these around in 84 * SmtEngine to permit expanding definitions late (and lazily), to 85 * support getValue() over defined functions, to support user output 86 * in terms of defined functions, etc. 87 */ 88 class DefinedFunction; 89 90 struct SmtEngineStatistics; 91 class SmtEnginePrivate; 92 class SmtScope; 93 class BooleanTermConverter; 94 95 ProofManager* currentProofManager(); 96 97 struct CommandCleanup; 98 typedef context::CDList<Command*, CommandCleanup> CommandList; 99 }/* CVC4::smt namespace */ 100 101 namespace theory { 102 class TheoryModel; 103 }/* CVC4::theory namespace */ 104 105 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the 106 // hood): use a type parameter and have check() delegate, or subclass 107 // SmtEngine and override check()? 108 // 109 // Probably better than that is to have a configuration object that 110 // indicates which passes are desired. The configuration occurs 111 // elsewhere (and can even occur at runtime). A simple "pass manager" 112 // of sorts determines check()'s behavior. 113 // 114 // The CNF conversion can go on in PropEngine. 115 116 class CVC4_PUBLIC SmtEngine { 117 118 /** The type of our internal map of defined functions */ 119 typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction> 120 DefinedFunctionMap; 121 /** The type of our internal assertion list */ 122 typedef context::CDList<Expr> AssertionList; 123 /** The type of our internal assignment set */ 124 typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet; 125 /** The types for the recursive function definitions */ 126 typedef context::CDList<Node> NodeList; 127 128 /** Expr manager context */ 129 context::Context* d_context; 130 131 /** The context levels of user pushes */ 132 std::vector<int> d_userLevels; 133 /** User level context */ 134 context::UserContext* d_userContext; 135 136 /** Our expression manager */ 137 ExprManager* d_exprManager; 138 /** Our internal expression/node manager */ 139 NodeManager* d_nodeManager; 140 /** The decision engine */ 141 DecisionEngine* d_decisionEngine; 142 /** The theory engine */ 143 TheoryEngine* d_theoryEngine; 144 /** The propositional engine */ 145 prop::PropEngine* d_propEngine; 146 /** The proof manager */ 147 ProofManager* d_proofManager; 148 /** An index of our defined functions */ 149 DefinedFunctionMap* d_definedFunctions; 150 /** recursive function definition abstractions for --fmf-fun */ 151 std::map< Node, TypeNode > d_fmfRecFunctionsAbs; 152 std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; 153 NodeList* d_fmfRecFunctionsDefined; 154 155 /** 156 * The assertion list (before any conversion) for supporting 157 * getAssertions(). Only maintained if in interactive mode. 158 */ 159 AssertionList* d_assertionList; 160 161 /** 162 * The list of assumptions from the previous call to checkSatisfiability. 163 * Note that if the last call to checkSatisfiability was a validity check, 164 * i.e., a call to query(a1, ..., an), then d_assumptions contains one single 165 * assumption ~(a1 AND ... AND an). 166 */ 167 std::vector<Expr> d_assumptions; 168 169 /** 170 * List of items for which to retrieve values using getAssignment(). 171 */ 172 AssignmentSet* d_assignments; 173 174 /** 175 * A list of commands that should be in the Model globally (i.e., 176 * regardless of push/pop). Only maintained if produce-models option 177 * is on. 178 */ 179 std::vector<Command*> d_modelGlobalCommands; 180 181 /** 182 * A list of commands that should be in the Model locally (i.e., 183 * it is context-dependent on push/pop). Only maintained if 184 * produce-models option is on. 185 */ 186 smt::CommandList* d_modelCommands; 187 188 /** 189 * A vector of declaration commands waiting to be dumped out. 190 * Once the SmtEngine is fully initialized, we'll dump them. 191 * This ensures the declarations come after the set-logic and 192 * any necessary set-option commands are dumped. 193 */ 194 std::vector<Command*> d_dumpCommands; 195 196 /** 197 * A vector of command definitions to be imported in the new 198 * SmtEngine when checking unsat-cores. 199 */ 200 std::vector<Command*> d_defineCommands; 201 202 /** 203 * The logic we're in. 204 */ 205 LogicInfo d_logic; 206 207 /** 208 * Keep a copy of the original option settings (for reset()). 209 */ 210 Options d_originalOptions; 211 212 /** whether this is an internal subsolver */ 213 bool d_isInternalSubsolver; 214 215 /** 216 * Number of internal pops that have been deferred. 217 */ 218 unsigned d_pendingPops; 219 220 /** 221 * Whether or not this SmtEngine is fully initialized (post-construction). 222 * This post-construction initialization is automatically triggered by the 223 * use of the SmtEngine; e.g. when the first formula is asserted, a call 224 * to simplify() is issued, a scope is pushed, etc. 225 */ 226 bool d_fullyInited; 227 228 /** 229 * Whether or not we have added any assertions/declarations/definitions, 230 * or done push/pop, since the last checkSat/query, and therefore we're 231 * not responsible for models or proofs. 232 */ 233 bool d_problemExtended; 234 235 /** 236 * Whether or not a query() or checkSat() has already been made through 237 * this SmtEngine. If true, and incrementalSolving is false, then 238 * attempting an additional query() or checkSat() will fail with a 239 * ModalException. 240 */ 241 bool d_queryMade; 242 243 /** 244 * Internal status flag to indicate whether we've sent a theory 245 * presolve() notification and need to match it with a postsolve(). 246 */ 247 bool d_needPostsolve; 248 249 /* 250 * Whether to call theory preprocessing during simplification - on 251 * by default* but gets turned off if arithRewriteEq is on 252 */ 253 bool d_earlyTheoryPP; 254 255 /* 256 * Whether we did a global negation of the formula. 257 */ 258 bool d_globalNegation; 259 260 /** 261 * Most recent result of last checkSat/query or (set-info :status). 262 */ 263 Result d_status; 264 265 /** 266 * The input file name (if any) or the name set through setInfo (if any) 267 */ 268 std::string d_filename; 269 270 /** 271 * Verbosity of various commands. 272 */ 273 std::map<std::string, Integer> d_commandVerbosity; 274 275 276 /** ReplayStream for the solver. */ 277 ExprStream* d_replayStream; 278 279 /** 280 * A private utility class to SmtEngine. 281 */ 282 smt::SmtEnginePrivate* d_private; 283 284 /** 285 * Check that a generated proof (via getProof()) checks. 286 */ 287 void checkProof(); 288 289 /** 290 * Internal method to get an unsatisfiable core (only if immediately preceded 291 * by an UNSAT or VALID query). Only permitted if CVC4 was built with 292 * unsat-core support and produce-unsat-cores is on. Does not dump the 293 * command. 294 */ 295 UnsatCore getUnsatCoreInternal(); 296 297 /** 298 * Check that an unsatisfiable core is indeed unsatisfiable. 299 */ 300 void checkUnsatCore(); 301 302 /** 303 * Check that a generated Model (via getModel()) actually satisfies 304 * all user assertions. 305 */ 306 void checkModel(bool hardFailure = true); 307 308 /** 309 * Check that a solution to a synthesis conjecture is indeed a solution. 310 * 311 * The check is made by determining if the negation of the synthesis 312 * conjecture in which the functions-to-synthesize have been replaced by the 313 * synthesized solutions, which is a quantifier-free formula, is 314 * unsatisfiable. If not, then the found solutions are wrong. 315 */ 316 void checkSynthSolution(); 317 318 /** 319 * Postprocess a value for output to the user. Involves doing things 320 * like turning datatypes back into tuples, length-1-bitvectors back 321 * into booleans, etc. 322 */ 323 Node postprocess(TNode n, TypeNode expectedType) const; 324 325 /** 326 * This is something of an "init" procedure, but is idempotent; call 327 * as often as you like. Should be called whenever the final options 328 * and logic for the problem are set (at least, those options that are 329 * not permitted to change after assertions and queries are made). 330 */ 331 void finalOptionsAreSet(); 332 333 /** 334 * Apply heuristics settings and other defaults. Done once, at 335 * finishInit() time. 336 */ 337 void setDefaults(); 338 339 /** 340 * Sets d_problemExtended to the given value. 341 * If d_problemExtended is set to true, the list of assumptions from the 342 * previous call to checkSatisfiability is cleared. 343 */ 344 void setProblemExtended(bool value); 345 346 /** 347 * Create theory engine, prop engine, decision engine. Called by 348 * finalOptionsAreSet() 349 */ 350 void finishInit(); 351 352 /** 353 * This is called by the destructor, just before destroying the 354 * PropEngine, TheoryEngine, and DecisionEngine (in that order). It 355 * is important because there are destruction ordering issues 356 * between PropEngine and Theory. 357 */ 358 void shutdown(); 359 360 /** 361 * Full check of consistency in current context. Returns true iff 362 * consistent. 363 */ 364 Result check(); 365 366 /** 367 * Quick check of consistency in current context: calls 368 * processAssertionList() then look for inconsistency (based only on 369 * that). 370 */ 371 Result quickCheck(); 372 373 /** 374 * Fully type-check the argument, and also type-check that it's 375 * actually Boolean. 376 */ 377 void ensureBoolean(const Expr& e) /* throw(TypeCheckingException) */; 378 379 void internalPush(); 380 381 void internalPop(bool immediate = false); 382 383 void doPendingPops(); 384 385 /** 386 * Internally handle the setting of a logic. This function should always 387 * be called when d_logic is updated. 388 */ 389 void setLogicInternal() /* throw() */; 390 391 // TODO (Issue #1096): Remove this friend relationship. 392 friend class ::CVC4::preprocessing::PreprocessingPassContext; 393 friend class ::CVC4::smt::SmtEnginePrivate; 394 friend class ::CVC4::smt::SmtScope; 395 friend class ::CVC4::smt::BooleanTermConverter; 396 friend ProofManager* ::CVC4::smt::currentProofManager(); 397 friend class ::CVC4::LogicRequest; 398 // to access d_modelCommands 399 friend class ::CVC4::Model; 400 friend class ::CVC4::theory::TheoryModel; 401 402 StatisticsRegistry* d_statisticsRegistry; 403 404 smt::SmtEngineStatistics* d_stats; 405 406 /** Container for the lemma input and output channels for this SmtEngine.*/ 407 LemmaChannels* d_channels; 408 409 /** 410 * Add to Model command. This is used for recording a command 411 * that should be reported during a get-model call. 412 */ 413 void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations"); 414 415 // disallow copy/assignment 416 SmtEngine(const SmtEngine&) = delete; 417 SmtEngine& operator=(const SmtEngine&) = delete; 418 419 //check satisfiability (for query and check-sat) 420 Result checkSatisfiability(const Expr& assumption, 421 bool inUnsatCore, 422 bool isQuery); 423 Result checkSatisfiability(const std::vector<Expr>& assumptions, 424 bool inUnsatCore, 425 bool isQuery); 426 427 /** 428 * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is 429 * the function that the formal argument list is for. This method is used 430 * as a helper function when defining (recursive) functions. 431 */ 432 void debugCheckFormals(const std::vector<Expr>& formals, Expr func); 433 434 /** 435 * Checks whether formula is a valid function body for func whose formal 436 * argument list is stored in formals. This method is 437 * used as a helper function when defining (recursive) functions. 438 */ 439 void debugCheckFunctionBody(Expr formula, 440 const std::vector<Expr>& formals, 441 Expr func); 442 443 /** 444 * Helper method to obtain both the heap and nil from the solver. Returns a 445 * std::pair where the first element is the heap expression and the second 446 * element is the nil expression. 447 */ 448 std::pair<Expr, Expr> getSepHeapAndNilExpr(); 449 450 public: 451 452 /** 453 * Construct an SmtEngine with the given expression manager. 454 */ 455 SmtEngine(ExprManager* em) /* throw() */; 456 457 /** 458 * Destruct the SMT engine. 459 */ 460 ~SmtEngine(); 461 462 /** 463 * Return true if this SmtEngine is fully initialized (post-construction). 464 * This post-construction initialization is automatically triggered by the 465 * use of the SmtEngine; e.g. when the first formula is asserted, a call 466 * to simplify() is issued, a scope is pushed, etc. 467 */ isFullyInited()468 bool isFullyInited() { return d_fullyInited; } 469 470 /** 471 * Set the logic of the script. 472 */ 473 void setLogic( 474 const std::string& logic) /* throw(ModalException, LogicException) */; 475 476 /** 477 * Set the logic of the script. 478 */ 479 void setLogic(const char* logic) /* throw(ModalException, LogicException) */; 480 481 /** 482 * Set the logic of the script. 483 */ 484 void setLogic(const LogicInfo& logic) /* throw(ModalException) */; 485 486 /** 487 * Get the logic information currently set 488 */ 489 LogicInfo getLogicInfo() const; 490 491 /** 492 * Set information about the script executing. 493 */ 494 void setInfo(const std::string& key, const CVC4::SExpr& value) 495 /* throw(OptionException, ModalException) */; 496 497 /** 498 * Query information about the SMT environment. 499 */ 500 CVC4::SExpr getInfo(const std::string& key) const; 501 502 /** 503 * Set an aspect of the current SMT execution environment. 504 */ 505 void setOption(const std::string& key, const CVC4::SExpr& value) 506 /* throw(OptionException, ModalException) */; 507 508 /** Set is internal subsolver. 509 * 510 * This function is called on SmtEngine objects that are created internally. 511 * It is used to mark that this SmtEngine should not perform preprocessing 512 * passes that rephrase the input, such as --sygus-rr-synth-input or 513 * --sygus-abduct. 514 */ 515 void setIsInternalSubsolver(); 516 517 /** sets the input name */ 518 void setFilename(std::string filename); 519 /** return the input name (if any) */ 520 std::string getFilename() const; 521 /** 522 * Get the model (only if immediately preceded by a SAT 523 * or INVALID query). Only permitted if CVC4 was built with model 524 * support and produce-models is on. 525 */ 526 Model* getModel(); 527 528 /** 529 * When using separation logic, obtain the expression for the heap. 530 */ 531 Expr getSepHeapExpr(); 532 533 /** 534 * When using separation logic, obtain the expression for nil. 535 */ 536 Expr getSepNilExpr(); 537 538 /** 539 * Get an aspect of the current SMT execution environment. 540 */ 541 CVC4::SExpr getOption(const std::string& key) const 542 /* throw(OptionException) */; 543 544 /** 545 * Define function func in the current context to be: 546 * (lambda (formals) formula) 547 * This adds func to the list of defined functions, which indicates that 548 * all occurrences of func should be expanded during expandDefinitions. 549 * This method expects input such that: 550 * - func : a variable of function type that expects the arguments in 551 * formals, 552 * - formals : a list of BOUND_VARIABLE expressions, 553 * - formula does not contain func. 554 */ 555 void defineFunction(Expr func, 556 const std::vector<Expr>& formals, 557 Expr formula); 558 559 /** is defined function */ 560 bool isDefinedFunction(Expr func); 561 562 /** Define functions recursive 563 * 564 * For each i, this constrains funcs[i] in the current context to be: 565 * (lambda (formals[i]) formulas[i]) 566 * where formulas[i] may contain variables from funcs. Unlike defineFunction 567 * above, we do not add funcs[i] to the set of defined functions. Instead, 568 * we consider funcs[i] to be a free uninterpreted function, and add: 569 * forall formals[i]. f(formals[i]) = formulas[i] 570 * to the set of assertions in the current context. 571 * This method expects input such that for each i: 572 * - func[i] : a variable of function type that expects the arguments in 573 * formals[i], and 574 * - formals[i] : a list of BOUND_VARIABLE expressions. 575 */ 576 void defineFunctionsRec(const std::vector<Expr>& funcs, 577 const std::vector<std::vector<Expr> >& formals, 578 const std::vector<Expr>& formulas); 579 580 /** Define function recursive 581 * 582 * Same as above, but for a single function. 583 */ 584 void defineFunctionRec(Expr func, 585 const std::vector<Expr>& formals, 586 Expr formula); 587 588 /** 589 * Add a formula to the current context: preprocess, do per-theory 590 * setup, use processAssertionList(), asserting to T-solver for 591 * literals and conjunction of literals. Returns false if 592 * immediately determined to be inconsistent. This version 593 * takes a Boolean flag to determine whether to include this asserted 594 * formula in an unsat core (if one is later requested). 595 */ 596 Result assertFormula(const Expr& e, bool inUnsatCore = true) 597 /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ 598 ; 599 600 /** 601 * Check validity of an expression with respect to the current set 602 * of assertions by asserting the query expression's negation and 603 * calling check(). Returns valid, invalid, or unknown result. 604 */ 605 Result query(const Expr& assumption = Expr(), 606 bool inUnsatCore = true) /* throw(Exception) */; 607 Result query(const std::vector<Expr>& assumptions, 608 bool inUnsatCore = true) /* throw(Exception) */; 609 610 /** 611 * Assert a formula (if provided) to the current context and call 612 * check(). Returns sat, unsat, or unknown result. 613 */ 614 Result checkSat(const Expr& assumption = Expr(), 615 bool inUnsatCore = true) /* throw(Exception) */; 616 Result checkSat(const std::vector<Expr>& assumptions, 617 bool inUnsatCore = true) /* throw(Exception) */; 618 619 /** 620 * Returns a set of so-called "failed" assumptions. 621 * 622 * The returned set is a subset of the set of assumptions of a previous 623 * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability 624 * with this set of failed assumptions still produces an unsat answer. 625 * 626 * Note that the returned set of failed assumptions is not necessarily 627 * minimal. 628 */ 629 std::vector<Expr> getUnsatAssumptions(void); 630 631 /*------------------- sygus commands ------------------*/ 632 633 /** adds a variable declaration 634 * 635 * Declared SyGuS variables may be used in SyGuS constraints, in which they 636 * are assumed to be universally quantified. 637 */ 638 void declareSygusVar(const std::string& id, Expr var, Type type); 639 /** stores information for debugging sygus invariants setup 640 * 641 * Since in SyGuS the commands "declare-primed-var" are not necessary for 642 * building invariant constraints, we only use them to check that the number 643 * of variables declared corresponds to the number of arguments of the 644 * invariant-to-synthesize. 645 */ 646 void declareSygusPrimedVar(const std::string& id, Type type); 647 /** adds a function variable declaration 648 * 649 * Is SyGuS semantics declared functions are treated in the same manner as 650 * declared variables, i.e. as universally quantified (function) variables 651 * which can occur in the SyGuS constraints that compose the conjecture to 652 * which a function is being synthesized. 653 */ 654 void declareSygusFunctionVar(const std::string& id, Expr var, Type type); 655 /** adds a function-to-synthesize declaration 656 * 657 * The given type may not correspond to the actual function type but to a 658 * datatype encoding the syntax restrictions for the 659 * function-to-synthesize. In this case this information is stored to be used 660 * during solving. 661 * 662 * vars contains the arguments of the function-to-synthesize. These variables 663 * are also stored to be used during solving. 664 * 665 * isInv determines whether the function-to-synthesize is actually an 666 * invariant. This information is necessary if we are dumping a command 667 * corresponding to this declaration, so that it can be properly printed. 668 */ 669 void declareSynthFun(const std::string& id, 670 Expr func, 671 Type type, 672 bool isInv, 673 const std::vector<Expr>& vars); 674 /** adds a regular sygus constraint */ 675 void assertSygusConstraint(Expr constraint); 676 /** adds an invariant constraint 677 * 678 * Invariant constraints are not explicitly declared: they are given in terms 679 * of the invariant-to-synthesize, the pre condition, transition relation and 680 * post condition. The actual constraint is built based on the inputs of these 681 * place holder predicates : 682 * 683 * PRE(x) -> INV(x) 684 * INV() ^ TRANS(x, x') -> INV(x') 685 * INV(x) -> POST(x) 686 * 687 * The regular and primed variables are retrieved from the declaration of the 688 * invariant-to-synthesize. 689 */ 690 void assertSygusInvConstraint(const Expr& inv, 691 const Expr& pre, 692 const Expr& trans, 693 const Expr& post); 694 /** 695 * Assert a synthesis conjecture to the current context and call 696 * check(). Returns sat, unsat, or unknown result. 697 * 698 * The actual synthesis conjecture is built based on the previously 699 * communicated information to this module (universal variables, defined 700 * functions, functions-to-synthesize, and which constraints compose it). The 701 * built conjecture is a higher-order formula of the form 702 * 703 * exists f1...fn . forall v1...vm . F 704 * 705 * in which f1...fn are the functions-to-synthesize, v1...vm are the declared 706 * universal variables and F is the set of declared constraints. 707 */ 708 Result checkSynth() /* throw(Exception) */; 709 710 /*------------------- end of sygus commands-------------*/ 711 712 /** 713 * Simplify a formula without doing "much" work. Does not involve 714 * the SAT Engine in the simplification, but uses the current 715 * definitions, assertions, and the current partial model, if one 716 * has been constructed. It also involves theory normalization. 717 * 718 * @todo (design) is this meant to give an equivalent or an 719 * equisatisfiable formula? 720 */ 721 Expr simplify( 722 const Expr& 723 e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ 724 ; 725 726 /** 727 * Expand the definitions in a term or formula. No other 728 * simplification or normalization is done. 729 */ 730 Expr expandDefinitions( 731 const Expr& 732 e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ 733 ; 734 735 /** 736 * Get the assigned value of an expr (only if immediately preceded 737 * by a SAT or INVALID query). Only permitted if the SmtEngine is 738 * set to operate interactively and produce-models is on. 739 */ 740 Expr getValue(const Expr& e) const 741 /* throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) */ 742 ; 743 744 /** 745 * Add a function to the set of expressions whose value is to be 746 * later returned by a call to getAssignment(). The expression 747 * should be a Boolean zero-ary defined function or a Boolean 748 * variable. Rather than throwing a ModalException on modal 749 * failures (not in interactive mode or not producing assignments), 750 * this function returns true if the expression was added and false 751 * if this request was ignored. 752 */ 753 bool addToAssignment(const Expr& e); 754 755 /** 756 * Get the assignment (only if immediately preceded by a SAT or 757 * INVALID query). Only permitted if the SmtEngine is set to 758 * operate interactively and produce-assignments is on. 759 */ 760 std::vector<std::pair<Expr, Expr> > getAssignment(); 761 762 /** 763 * Get the last proof (only if immediately preceded by an UNSAT 764 * or VALID query). Only permitted if CVC4 was built with proof 765 * support and produce-proofs is on. 766 * 767 * The Proof object is owned by this SmtEngine until the SmtEngine is 768 * destroyed. 769 */ 770 const Proof& getProof(); 771 772 /** 773 * Print all instantiations made by the quantifiers module. 774 */ 775 void printInstantiations( std::ostream& out ); 776 777 /** 778 * Print solution for synthesis conjectures found by ce_guided_instantiation module 779 */ 780 void printSynthSolution( std::ostream& out ); 781 782 /** 783 * Get synth solution 784 * 785 * This function adds entries to sol_map that map functions-to-synthesize with 786 * their solutions, for all active conjectures. This should be called 787 * immediately after the solver answers unsat for sygus input. 788 * 789 * Specifically, given a sygus conjecture of the form 790 * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn ) 791 * where x1...xn are second order bound variables, we map each xi to 792 * lambda term in sol_map such that 793 * forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn ) 794 * is a valid formula. 795 */ 796 void getSynthSolutions(std::map<Expr, Expr>& sol_map); 797 798 /** 799 * Do quantifier elimination. 800 * 801 * This function takes as input a quantified formula e 802 * of the form: 803 * Q x1...xn. P( x1...xn, y1...yn ) 804 * where P( x1...xn, y1...yn ) is a quantifier-free 805 * formula in a logic that supports quantifier elimination. 806 * Currently, the only logics supported by quantifier 807 * elimination is LRA and LIA. 808 * 809 * This function returns a formula ret such that, given 810 * the current set of formulas A asserted to this SmtEngine : 811 * 812 * If doFull = true, then 813 * - ( A ^ e ) and ( A ^ ret ) are equivalent 814 * - ret is quantifier-free formula containing 815 * only free variables in y1...yn. 816 * 817 * If doFull = false, then 818 * - (A ^ e) => (A ^ ret) if Q is forall or 819 * (A ^ ret) => (A ^ e) if Q is exists, 820 * - ret is quantifier-free formula containing 821 * only free variables in y1...yn, 822 * - If Q is exists, let A^Q_n be the formula 823 * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n 824 * where for each i=1,...n, formula ret^Q_i 825 * is the result of calling doQuantifierElimination 826 * for e with the set of assertions A^Q_{i-1}. 827 * Similarly, if Q is forall, then let A^Q_n be 828 * A ^ ret^Q_1 ^ ... ^ ret^Q_n 829 * where ret^Q_i is the same as above. 830 * In either case, we have that ret^Q_j will 831 * eventually be true or false, for some finite j. 832 * 833 * The former feature is quantifier elimination, and 834 * is run on invocations of the smt2 extended command get-qe. 835 * The latter feature is referred to as partial quantifier 836 * elimination, and is run on invocations of the smt2 837 * extended command get-qe-disjunct, which can be used 838 * for incrementally computing the result of a 839 * quantifier elimination. 840 * 841 * The argument strict is whether to output 842 * warnings, such as when an unexpected logic is used. 843 */ 844 Expr doQuantifierElimination(const Expr& e, 845 bool doFull, 846 bool strict = true) /* throw(Exception) */; 847 848 /** 849 * Get list of quantified formulas that were instantiated 850 */ 851 void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ); 852 853 /** 854 * Get instantiations 855 */ 856 void getInstantiations( Expr q, std::vector< Expr >& insts ); 857 void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ); 858 859 /** 860 * Get an unsatisfiable core (only if immediately preceded by an 861 * UNSAT or VALID query). Only permitted if CVC4 was built with 862 * unsat-core support and produce-unsat-cores is on. 863 */ 864 UnsatCore getUnsatCore(); 865 866 /** 867 * Get the current set of assertions. Only permitted if the 868 * SmtEngine is set to operate interactively. 869 */ 870 std::vector<Expr> getAssertions(); 871 872 /** 873 * Push a user-level context. 874 */ 875 void 876 push() /* throw(ModalException, LogicException, UnsafeInterruptException) */; 877 878 /** 879 * Pop a user-level context. Throws an exception if nothing to pop. 880 */ 881 void pop(); 882 883 /** 884 * Completely reset the state of the solver, as though destroyed and 885 * recreated. The result is as if newly constructed (so it still 886 * retains the same options structure and ExprManager). 887 */ 888 void reset() /* throw() */; 889 890 /** 891 * Reset all assertions, global declarations, etc. 892 */ 893 void resetAssertions() /* throw() */; 894 895 /** 896 * Interrupt a running query. This can be called from another thread 897 * or from a signal handler. Throws a ModalException if the SmtEngine 898 * isn't currently in a query. 899 */ 900 void interrupt() /* throw(ModalException) */; 901 902 /** 903 * Set a resource limit for SmtEngine operations. This is like a time 904 * limit, but it's deterministic so that reproducible results can be 905 * obtained. Currently, it's based on the number of conflicts. 906 * However, please note that the definition may change between different 907 * versions of CVC4 (as may the number of conflicts required, anyway), 908 * and it might even be different between instances of the same version 909 * of CVC4 on different platforms. 910 * 911 * A cumulative and non-cumulative (per-call) resource limit can be 912 * set at the same time. A call to setResourceLimit() with 913 * cumulative==true replaces any cumulative resource limit currently 914 * in effect; a call with cumulative==false replaces any per-call 915 * resource limit currently in effect. Time limits can be set in 916 * addition to resource limits; the SmtEngine obeys both. That means 917 * that up to four independent limits can control the SmtEngine 918 * at the same time. 919 * 920 * When an SmtEngine is first created, it has no time or resource 921 * limits. 922 * 923 * Currently, these limits only cause the SmtEngine to stop what its 924 * doing when the limit expires (or very shortly thereafter); no 925 * heuristics are altered by the limits or the threat of them expiring. 926 * We reserve the right to change this in the future. 927 * 928 * @param units the resource limit, or 0 for no limit 929 * @param cumulative whether this resource limit is to be a cumulative 930 * resource limit for all remaining calls into the SmtEngine (true), or 931 * whether it's a per-call resource limit (false); the default is false 932 */ 933 void setResourceLimit(unsigned long units, bool cumulative = false); 934 935 /** 936 * Set a time limit for SmtEngine operations. 937 * 938 * A cumulative and non-cumulative (per-call) time limit can be 939 * set at the same time. A call to setTimeLimit() with 940 * cumulative==true replaces any cumulative time limit currently 941 * in effect; a call with cumulative==false replaces any per-call 942 * time limit currently in effect. Resource limits can be set in 943 * addition to time limits; the SmtEngine obeys both. That means 944 * that up to four independent limits can control the SmtEngine 945 * at the same time. 946 * 947 * Note that the cumulative timer only ticks away when one of the 948 * SmtEngine's workhorse functions (things like assertFormula(), 949 * query(), checkSat(), and simplify()) are running. Between calls, 950 * the timer is still. 951 * 952 * When an SmtEngine is first created, it has no time or resource 953 * limits. 954 * 955 * Currently, these limits only cause the SmtEngine to stop what its 956 * doing when the limit expires (or very shortly thereafter); no 957 * heuristics are altered by the limits or the threat of them expiring. 958 * We reserve the right to change this in the future. 959 * 960 * @param millis the time limit in milliseconds, or 0 for no limit 961 * @param cumulative whether this time limit is to be a cumulative 962 * time limit for all remaining calls into the SmtEngine (true), or 963 * whether it's a per-call time limit (false); the default is false 964 */ 965 void setTimeLimit(unsigned long millis, bool cumulative = false); 966 967 /** 968 * Get the current resource usage count for this SmtEngine. This 969 * function can be used to ascertain reasonable values to pass as 970 * resource limits to setResourceLimit(). 971 */ 972 unsigned long getResourceUsage() const; 973 974 /** 975 * Get the current millisecond count for this SmtEngine. 976 */ 977 unsigned long getTimeUsage() const; 978 979 /** 980 * Get the remaining resources that can be consumed by this SmtEngine 981 * according to the currently-set cumulative resource limit. If there 982 * is not a cumulative resource limit set, this function throws a 983 * ModalException. 984 */ 985 unsigned long getResourceRemaining() const /* throw(ModalException) */; 986 987 /** 988 * Get the remaining number of milliseconds that can be consumed by 989 * this SmtEngine according to the currently-set cumulative time limit. 990 * If there is not a cumulative resource limit set, this function 991 * throws a ModalException. 992 */ 993 unsigned long getTimeRemaining() const /* throw(ModalException) */; 994 995 /** 996 * Permit access to the underlying ExprManager. 997 */ getExprManager()998 ExprManager* getExprManager() const { 999 return d_exprManager; 1000 } 1001 1002 /** 1003 * Export statistics from this SmtEngine. 1004 */ 1005 Statistics getStatistics() const /* throw() */; 1006 1007 /** 1008 * Get the value of one named statistic from this SmtEngine. 1009 */ 1010 SExpr getStatistic(std::string name) const /* throw() */; 1011 1012 /** 1013 * Flush statistic from this SmtEngine. Safe to use in a signal handler. 1014 */ 1015 void safeFlushStatistics(int fd) const; 1016 1017 /** 1018 * Returns the most recent result of checkSat/query or (set-info :status). 1019 */ getStatusOfLastCommand()1020 Result getStatusOfLastCommand() const /* throw() */ { return d_status; } 1021 /** 1022 * Set user attribute. 1023 * This function is called when an attribute is set by a user. 1024 * In SMT-LIBv2 this is done via the syntax (! expr :attr) 1025 */ 1026 void setUserAttribute(const std::string& attr, 1027 Expr expr, 1028 const std::vector<Expr>& expr_values, 1029 const std::string& str_value); 1030 1031 /** 1032 * Set print function in model 1033 */ 1034 void setPrintFuncInModel(Expr f, bool p); 1035 1036 1037 /** Throws a ModalException if the SmtEngine has been fully initialized. */ 1038 void beforeSearch() /* throw(ModalException) */; 1039 channels()1040 LemmaChannels* channels() { return d_channels; } 1041 1042 1043 /** 1044 * Expermintal feature: Sets the sequence of decisions. 1045 * This currently requires very fine grained knowledge about literal 1046 * translation. 1047 */ 1048 void setReplayStream(ExprStream* exprStream); 1049 1050 /** get expression name 1051 * Returns true if e has an expression name in the current context. 1052 * If it returns true, the name of e is stored in name. 1053 */ 1054 bool getExpressionName(Expr e, std::string& name) const; 1055 1056 /** set expression name 1057 * Sets the expression name of e to name. 1058 * This information is user-context-dependent. 1059 * If e already has a name, it is overwritten. 1060 */ 1061 void setExpressionName(Expr e, const std::string& name); 1062 1063 };/* class SmtEngine */ 1064 1065 }/* CVC4 namespace */ 1066 1067 #endif /* __CVC4__SMT_ENGINE_H */ 1068