diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-08-13 18:20:59 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-13 18:20:59 -0700 |
commit | 5c97514836a18ddb0d00041c013445f2b93efd25 (patch) | |
tree | 9e31882399c31d87f9228db5cb1b256701d2ba81 | |
parent | 01e84d511e40604b01328b1e96ecdbe2b818b3c3 (diff) |
SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 1118 |
2 files changed, 574 insertions, 546 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 762b21fd8..27ee446fe 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -849,8 +849,8 @@ class SmtEnginePrivate : public NodeManagerListener { SmtEngine::SmtEngine(ExprManager* em) : d_context(new Context()), - d_userLevels(), d_userContext(new UserContext()), + d_userLevels(), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), d_decisionEngine(NULL), diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f032d202a..eba73c380 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -65,19 +65,27 @@ class Model; class LogicRequest; class StatisticsRegistry; +/* -------------------------------------------------------------------------- */ + namespace context { class Context; class UserContext; }/* CVC4::context namespace */ +/* -------------------------------------------------------------------------- */ + namespace preprocessing { class PreprocessingPassContext; } +/* -------------------------------------------------------------------------- */ + namespace prop { class PropEngine; }/* CVC4::prop namespace */ +/* -------------------------------------------------------------------------- */ + namespace smt { /** * Representation of a defined function. We keep these around in @@ -98,6 +106,8 @@ namespace smt { typedef context::CDList<Command*, CommandCleanup> CommandList; }/* CVC4::smt namespace */ +/* -------------------------------------------------------------------------- */ + namespace theory { class TheoryModel; }/* CVC4::theory namespace */ @@ -113,345 +123,10 @@ namespace theory { // // The CNF conversion can go on in PropEngine. -class CVC4_PUBLIC SmtEngine { - - /** The type of our internal map of defined functions */ - typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction> - DefinedFunctionMap; - /** The type of our internal assertion list */ - typedef context::CDList<Expr> AssertionList; - /** The type of our internal assignment set */ - typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet; - /** The types for the recursive function definitions */ - typedef context::CDList<Node> NodeList; - - /** Expr manager context */ - context::Context* d_context; - - /** The context levels of user pushes */ - std::vector<int> d_userLevels; - /** User level context */ - context::UserContext* d_userContext; - - /** Our expression manager */ - ExprManager* d_exprManager; - /** Our internal expression/node manager */ - NodeManager* d_nodeManager; - /** The decision engine */ - DecisionEngine* d_decisionEngine; - /** The theory engine */ - TheoryEngine* d_theoryEngine; - /** The propositional engine */ - prop::PropEngine* d_propEngine; - /** The proof manager */ - ProofManager* d_proofManager; - /** An index of our defined functions */ - DefinedFunctionMap* d_definedFunctions; - /** The SMT engine subsolver - * - * This is a separate copy of the SMT engine which is used for making - * calls that cannot be answered by this copy of the SMT engine. An example - * of invoking this subsolver is the get-abduct command, where we wish to - * solve a sygus conjecture based on the current assertions. In particular, - * consider the input: - * (assert A) - * (get-abduct B) - * In the copy of the SMT engine where these commands are issued, we maintain - * A in the assertion stack. To solve the abduction problem, instead of - * modifying the assertion stack to remove A and add the sygus conjecture - * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the - * assertion stack unchaged. This copy of the SMT engine can be further - * queried for information regarding further solutions. - */ - std::unique_ptr<SmtEngine> d_subsolver; - /** - * If applicable, the function-to-synthesize that the subsolver is solving - * for. This is used for the get-abduct command. - */ - Expr d_sssf; - /** - * The conjecture of the current abduction problem. This expression is only - * valid while we are in mode SMT_MODE_ABDUCT. - */ - Expr d_abdConj; - /** recursive function definition abstractions for --fmf-fun */ - std::map< Node, TypeNode > d_fmfRecFunctionsAbs; - std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; - NodeList* d_fmfRecFunctionsDefined; - - /** - * The assertion list (before any conversion) for supporting - * getAssertions(). Only maintained if in interactive mode. - */ - AssertionList* d_assertionList; - - /** - * The list of assumptions from the previous call to checkSatisfiability. - * Note that if the last call to checkSatisfiability was a validity check, - * i.e., a call to query(a1, ..., an), then d_assumptions contains one single - * assumption ~(a1 AND ... AND an). - */ - std::vector<Expr> d_assumptions; - - /** - * List of items for which to retrieve values using getAssignment(). - */ - AssignmentSet* d_assignments; - - /** - * A list of commands that should be in the Model globally (i.e., - * regardless of push/pop). Only maintained if produce-models option - * is on. - */ - std::vector<Command*> d_modelGlobalCommands; - - /** - * A list of commands that should be in the Model locally (i.e., - * it is context-dependent on push/pop). Only maintained if - * produce-models option is on. - */ - smt::CommandList* d_modelCommands; - - /** - * A vector of declaration commands waiting to be dumped out. - * Once the SmtEngine is fully initialized, we'll dump them. - * This ensures the declarations come after the set-logic and - * any necessary set-option commands are dumped. - */ - std::vector<Command*> d_dumpCommands; - - /** - * A vector of command definitions to be imported in the new - * SmtEngine when checking unsat-cores. - */ - std::vector<Command*> d_defineCommands; - - /** - * The logic we're in. - */ - LogicInfo d_logic; - - /** - * Keep a copy of the original option settings (for reset()). - */ - Options d_originalOptions; - - /** whether this is an internal subsolver */ - bool d_isInternalSubsolver; - - /** - * Number of internal pops that have been deferred. - */ - unsigned d_pendingPops; - - /** - * Whether or not this SmtEngine is fully initialized (post-construction). - * This post-construction initialization is automatically triggered by the - * use of the SmtEngine; e.g. when the first formula is asserted, a call - * to simplify() is issued, a scope is pushed, etc. - */ - bool d_fullyInited; - - /** - * Whether or not a query() or checkSat() has already been made through - * this SmtEngine. If true, and incrementalSolving is false, then - * attempting an additional query() or checkSat() will fail with a - * ModalException. - */ - bool d_queryMade; - - /** - * Internal status flag to indicate whether we've sent a theory - * presolve() notification and need to match it with a postsolve(). - */ - bool d_needPostsolve; - - /* - * Whether to call theory preprocessing during simplification - on - * by default* but gets turned off if arithRewriteEq is on - */ - bool d_earlyTheoryPP; - - /* - * Whether we did a global negation of the formula. - */ - bool d_globalNegation; - - /** - * Most recent result of last checkSat/query or (set-info :status). - */ - Result d_status; - - /** - * The expected status of the next satisfiability check. - */ - Result d_expectedStatus; - - /** - * The current mode of the solver, see Figure 4.1 on page 52 of the - * SMT-LIB version 2.6 standard - * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf - */ - enum SmtMode - { - // the initial state of the solver - SMT_MODE_START, - // normal state of the solver, after assert/push/pop/declare/define - SMT_MODE_ASSERT, - // immediately after a check-sat returning "sat" or "unknown" - SMT_MODE_SAT, - // immediately after a check-sat returning "unsat" - SMT_MODE_UNSAT, - // immediately after a successful call to get-abduct - SMT_MODE_ABDUCT - }; - SmtMode d_smtMode; - - /** - * The input file name (if any) or the name set through setInfo (if any) - */ - std::string d_filename; - - /** - * Verbosity of various commands. - */ - std::map<std::string, Integer> d_commandVerbosity; - - - /** ReplayStream for the solver. */ - ExprStream* d_replayStream; - - /** - * A private utility class to SmtEngine. - */ - smt::SmtEnginePrivate* d_private; - - /** - * Check that a generated proof (via getProof()) checks. - */ - void checkProof(); - - /** - * Internal method to get an unsatisfiable core (only if immediately preceded - * by an UNSAT or VALID query). Only permitted if CVC4 was built with - * unsat-core support and produce-unsat-cores is on. Does not dump the - * command. - */ - UnsatCore getUnsatCoreInternal(); - - /** - * Check that an unsatisfiable core is indeed unsatisfiable. - */ - void checkUnsatCore(); - - /** - * Check that a generated Model (via getModel()) actually satisfies - * all user assertions. - */ - void checkModel(bool hardFailure = true); - - /** - * Check that a solution to a synthesis conjecture is indeed a solution. - * - * The check is made by determining if the negation of the synthesis - * conjecture in which the functions-to-synthesize have been replaced by the - * synthesized solutions, which is a quantifier-free formula, is - * unsatisfiable. If not, then the found solutions are wrong. - */ - void checkSynthSolution(); - /** - * Check that a solution to an abduction conjecture is indeed a solution. - * - * The check is made by determining that the assertions conjoined with the - * solution to the abduction problem (a) is SAT, and the assertions conjoined - * with the abduct and the goal is UNSAT. If these criteria are not met, an - * internal error is thrown. - */ - void checkAbduct(Expr a); - - /** - * Postprocess a value for output to the user. Involves doing things - * like turning datatypes back into tuples, length-1-bitvectors back - * into booleans, etc. - */ - Node postprocess(TNode n, TypeNode expectedType) const; - - /** - * This is something of an "init" procedure, but is idempotent; call - * as often as you like. Should be called whenever the final options - * and logic for the problem are set (at least, those options that are - * not permitted to change after assertions and queries are made). - */ - void finalOptionsAreSet(); - - /** - * Apply heuristics settings and other defaults. Done once, at - * finishInit() time. - */ - void setDefaults(); - - /** - * Sets that the problem has been extended. This sets the smt mode of the - * solver to SMT_MODE_ASSERT, and clears the list of assumptions from the - * previous call to checkSatisfiability. - */ - void setProblemExtended(); - - /** - * Create theory engine, prop engine, decision engine. Called by - * finalOptionsAreSet() - */ - void finishInit(); - - /** - * This is called by the destructor, just before destroying the - * PropEngine, TheoryEngine, and DecisionEngine (in that order). It - * is important because there are destruction ordering issues - * between PropEngine and Theory. - */ - void shutdown(); - - /** - * Full check of consistency in current context. Returns true iff - * consistent. - */ - Result check(); - - /** - * Quick check of consistency in current context: calls - * processAssertionList() then look for inconsistency (based only on - * that). - */ - Result quickCheck(); - /** get the model, if it is available and return a pointer to it - * - * This ensures that the model is currently available, which means that - * CVC4 is producing models, and is in "SAT mode", otherwise an exception - * is thrown. - * - * The flag c is used for giving an error message to indicate the context - * this method was called. - */ - theory::TheoryModel* getAvailableModel(const char* c) const; - - /** - * Fully type-check the argument, and also type-check that it's - * actually Boolean. - */ - void ensureBoolean(const Expr& e) /* throw(TypeCheckingException) */; - - void internalPush(); - - void internalPop(bool immediate = false); - - void doPendingPops(); - - /** - * Internally handle the setting of a logic. This function should always - * be called when d_logic is updated. - */ - void setLogicInternal() /* throw() */; +/* -------------------------------------------------------------------------- */ +class CVC4_PUBLIC SmtEngine +{ // TODO (Issue #1096): Remove this friend relationship. friend class ::CVC4::preprocessing::PreprocessingPassContext; friend class ::CVC4::smt::SmtEnginePrivate; @@ -459,83 +134,16 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::BooleanTermConverter; friend ProofManager* ::CVC4::smt::currentProofManager(); friend class ::CVC4::LogicRequest; - // to access d_modelCommands - friend class ::CVC4::Model; + friend class ::CVC4::Model; // to access d_modelCommands friend class ::CVC4::theory::TheoryModel; - StatisticsRegistry* d_statisticsRegistry; - - smt::SmtEngineStatistics* d_stats; - - /** Container for the lemma input and output channels for this SmtEngine.*/ - LemmaChannels* d_channels; - - /** - * Add to Model command. This is used for recording a command - * that should be reported during a get-model call. - */ - void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations"); - - // disallow copy/assignment - SmtEngine(const SmtEngine&) = delete; - SmtEngine& operator=(const SmtEngine&) = delete; - - //check satisfiability (for query and check-sat) - Result checkSatisfiability(const Expr& assumption, - bool inUnsatCore, - bool isQuery); - Result checkSatisfiability(const std::vector<Expr>& assumptions, - bool inUnsatCore, - bool isQuery); - - /** - * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is - * the function that the formal argument list is for. This method is used - * as a helper function when defining (recursive) functions. - */ - void debugCheckFormals(const std::vector<Expr>& formals, Expr func); - - /** - * Checks whether formula is a valid function body for func whose formal - * argument list is stored in formals. This method is - * used as a helper function when defining (recursive) functions. - */ - void debugCheckFunctionBody(Expr formula, - const std::vector<Expr>& formals, - Expr func); - /** get abduct internal - * - * Gets the next abduct from the internal subsolver d_subsolver. If - * successful, this method returns true and sets abd to that abduct. - * - * This method assumes d_subsolver has been initialized to do abduction - * problems. - */ - bool getAbductInternal(Expr& abd); - - /** - * Helper method to obtain both the heap and nil from the solver. Returns a - * std::pair where the first element is the heap expression and the second - * element is the nil expression. - */ - std::pair<Expr, Expr> getSepHeapAndNilExpr(); - - /** get expanded assertions - * - * Returns the set of assertions, after expanding definitions. - */ - std::vector<Expr> getExpandedAssertions(); - + /* ....................................................................... */ public: + /* ....................................................................... */ - /** - * Construct an SmtEngine with the given expression manager. - */ - SmtEngine(ExprManager* em) /* throw() */; - - /** - * Destruct the SMT engine. - */ + /** Construct an SmtEngine with the given expression manager. */ + SmtEngine(ExprManager* em); + /** Destruct the SMT engine. */ ~SmtEngine(); /** @@ -546,48 +154,44 @@ class CVC4_PUBLIC SmtEngine { */ bool isFullyInited() { return d_fullyInited; } - /** - * Return the user context level. - */ + /** Return the user context level. */ size_t getNumUserLevels() { return d_userLevels.size(); } /** * Set the logic of the script. + * @throw ModalException, LogicException */ - void setLogic( - const std::string& logic) /* throw(ModalException, LogicException) */; + void setLogic(const std::string& logic); /** * Set the logic of the script. + * @throw ModalException, LogicException */ - void setLogic(const char* logic) /* throw(ModalException, LogicException) */; + void setLogic(const char* logic); /** * Set the logic of the script. + * @throw ModalException */ - void setLogic(const LogicInfo& logic) /* throw(ModalException) */; + void setLogic(const LogicInfo& logic); - /** - * Get the logic information currently set - */ + /** Get the logic information currently set. */ LogicInfo getLogicInfo() const; /** * Set information about the script executing. + * @throw OptionException, ModalException */ - void setInfo(const std::string& key, const CVC4::SExpr& value) - /* throw(OptionException, ModalException) */; + void setInfo(const std::string& key, const CVC4::SExpr& value); - /** - * Query information about the SMT environment. - */ + /** Query information about the SMT environment. */ CVC4::SExpr getInfo(const std::string& key) const; /** * Set an aspect of the current SMT execution environment. + * @throw OptionException, ModalException */ - void setOption(const std::string& key, const CVC4::SExpr& value) - /* throw(OptionException, ModalException) */; + void setOption(const std::string& key, const CVC4::SExpr& value); /** Set is internal subsolver. * @@ -598,10 +202,11 @@ class CVC4_PUBLIC SmtEngine { */ void setIsInternalSubsolver(); - /** sets the input name */ + /** set the input name */ void setFilename(std::string filename); /** return the input name (if any) */ std::string getFilename() const; + /** * Get the model (only if immediately preceded by a SAT * or INVALID query). Only permitted if produce-models is on. @@ -634,21 +239,17 @@ class CVC4_PUBLIC SmtEngine { */ Result blockModelValues(const std::vector<Expr>& exprs); - /** - * When using separation logic, obtain the expression for the heap. - */ + /** When using separation logic, obtain the expression for the heap. */ Expr getSepHeapExpr(); - /** - * When using separation logic, obtain the expression for nil. - */ + /** When using separation logic, obtain the expression for nil. */ Expr getSepNilExpr(); /** * Get an aspect of the current SMT execution environment. + * @throw OptionException */ - CVC4::SExpr getOption(const std::string& key) const - /* throw(OptionException) */; + CVC4::SExpr getOption(const std::string& key) const; /** * Define function func in the current context to be: @@ -665,10 +266,11 @@ class CVC4_PUBLIC SmtEngine { const std::vector<Expr>& formals, Expr formula); - /** is defined function */ + /** Return true if given expression is a defined function. */ bool isDefinedFunction(Expr func); - /** Define functions recursive + /** + * Define functions recursive * * For each i, this constrains funcs[i] in the current context to be: * (lambda (formals[i]) formulas[i]) @@ -685,15 +287,13 @@ class CVC4_PUBLIC SmtEngine { void defineFunctionsRec(const std::vector<Expr>& funcs, const std::vector<std::vector<Expr> >& formals, const std::vector<Expr>& formulas); - - /** Define function recursive - * + /** + * Define function recursive * Same as above, but for a single function. */ void defineFunctionRec(Expr func, const std::vector<Expr>& formals, Expr formula); - /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for @@ -701,29 +301,30 @@ class CVC4_PUBLIC SmtEngine { * immediately determined to be inconsistent. This version * takes a Boolean flag to determine whether to include this asserted * formula in an unsat core (if one is later requested). + * + * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - Result assertFormula(const Expr& e, bool inUnsatCore = true) - /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ - ; + Result assertFormula(const Expr& e, bool inUnsatCore = true); /** * Check validity of an expression with respect to the current set * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. + * + * @throw Exception */ - Result query(const Expr& assumption = Expr(), - bool inUnsatCore = true) /* throw(Exception) */; - Result query(const std::vector<Expr>& assumptions, - bool inUnsatCore = true) /* throw(Exception) */; + Result query(const Expr& assumption = Expr(), bool inUnsatCore = true); + Result query(const std::vector<Expr>& assumptions, bool inUnsatCore = true); /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. + * + * @throw Exception */ - Result checkSat(const Expr& assumption = Expr(), - bool inUnsatCore = true) /* throw(Exception) */; + Result checkSat(const Expr& assumption = Expr(), bool inUnsatCore = true); Result checkSat(const std::vector<Expr>& assumptions, - bool inUnsatCore = true) /* throw(Exception) */; + bool inUnsatCore = true); /** * Returns a set of so-called "failed" assumptions. @@ -737,15 +338,18 @@ class CVC4_PUBLIC SmtEngine { */ std::vector<Expr> getUnsatAssumptions(void); - /*------------------- sygus commands ------------------*/ + /*---------------------------- sygus commands ---------------------------*/ - /** adds a variable declaration + /** + * Add variable declaration. * * Declared SyGuS variables may be used in SyGuS constraints, in which they * are assumed to be universally quantified. */ void declareSygusVar(const std::string& id, Expr var, Type type); - /** stores information for debugging sygus invariants setup + + /** + * Store information for debugging sygus invariants setup. * * Since in SyGuS the commands "declare-primed-var" are not necessary for * building invariant constraints, we only use them to check that the number @@ -753,7 +357,9 @@ class CVC4_PUBLIC SmtEngine { * invariant-to-synthesize. */ void declareSygusPrimedVar(const std::string& id, Type type); - /** adds a function variable declaration + + /** + * Add a function variable declaration. * * Is SyGuS semantics declared functions are treated in the same manner as * declared variables, i.e. as universally quantified (function) variables @@ -761,7 +367,9 @@ class CVC4_PUBLIC SmtEngine { * which a function is being synthesized. */ void declareSygusFunctionVar(const std::string& id, Expr var, Type type); - /** adds a function-to-synthesize declaration + + /** + * Add a function-to-synthesize declaration. * * The given type may not correspond to the actual function type but to a * datatype encoding the syntax restrictions for the @@ -780,9 +388,12 @@ class CVC4_PUBLIC SmtEngine { Type type, bool isInv, const std::vector<Expr>& vars); - /** adds a regular sygus constraint */ + + /** Add a regular sygus constraint.*/ void assertSygusConstraint(Expr constraint); - /** adds an invariant constraint + + /** + * Add an invariant constraint. * * Invariant constraints are not explicitly declared: they are given in terms * of the invariant-to-synthesize, the pre condition, transition relation and @@ -813,10 +424,12 @@ class CVC4_PUBLIC SmtEngine { * * in which f1...fn are the functions-to-synthesize, v1...vm are the declared * universal variables and F is the set of declared constraints. + * + * @throw Exception */ - Result checkSynth() /* throw(Exception) */; + Result checkSynth(); - /*------------------- end of sygus commands-------------*/ + /*------------------------- end of sygus commands ------------------------*/ /** * Simplify a formula without doing "much" work. Does not involve @@ -824,31 +437,30 @@ class CVC4_PUBLIC SmtEngine { * definitions, assertions, and the current partial model, if one * has been constructed. It also involves theory normalization. * + * @throw TypeCheckingException, LogicException, UnsafeInterruptException + * * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? */ - Expr simplify( - const Expr& - e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ - ; + Expr simplify(const Expr& e); /** * Expand the definitions in a term or formula. No other * simplification or normalization is done. + * + * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - Expr expandDefinitions( - const Expr& - e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ - ; + Expr expandDefinitions(const Expr& e); /** * Get the assigned value of an expr (only if immediately preceded * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. + * + * @throw ModalException, TypeCheckingException, LogicException, + * UnsafeInterruptException */ - Expr getValue(const Expr& e) const - /* throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) */ - ; + Expr getValue(const Expr& e) const; /** * Same as getValue but for a vector of expressions @@ -883,18 +495,17 @@ class CVC4_PUBLIC SmtEngine { */ const Proof& getProof(); - /** - * Print all instantiations made by the quantifiers module. - */ - void printInstantiations( std::ostream& out ); + /** Print all instantiations made by the quantifiers module. */ + void printInstantiations(std::ostream& out); /** - * Print solution for synthesis conjectures found by ce_guided_instantiation module + * Print solution for synthesis conjectures found by counter-example guided + * instantiation module. */ - void printSynthSolution( std::ostream& out ); + void printSynthSolution(std::ostream& out); /** - * Get synth solution + * Get synth solution. * * This function adds entries to sol_map that map functions-to-synthesize with * their solutions, for all active conjectures. This should be called @@ -951,13 +562,14 @@ class CVC4_PUBLIC SmtEngine { * extended command get-qe-disjunct, which can be used * for incrementally computing the result of a * quantifier elimination. - * + * * The argument strict is whether to output * warnings, such as when an unexpected logic is used. + * + * throw@ Exception */ - Expr doQuantifierElimination(const Expr& e, - bool doFull, - bool strict = true) /* throw(Exception) */; + Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true); + /** * This method asks this SMT engine to find an abduct with respect to the * current assertion stack (call it A) and the conjecture (call it B). @@ -971,19 +583,17 @@ class CVC4_PUBLIC SmtEngine { * corresponding sygus problem for generating such a solution. */ bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd); + /** Same as above, but without user-provided grammar restrictions */ bool getAbduct(const Expr& conj, Expr& abd); - /** - * Get list of quantified formulas that were instantiated - */ - void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ); - - /** - * Get instantiations - */ - void getInstantiations( Expr q, std::vector< Expr >& insts ); - void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ); + /** Get list of quantified formulas that were instantiated. */ + void getInstantiatedQuantifiedFormulas(std::vector<Expr>& qs); + + /** Get instantiations. */ + void getInstantiations(Expr q, std::vector<Expr>& insts); + void getInstantiationTermVectors(Expr q, + std::vector<std::vector<Expr> >& tvecs); /** * Get an unsatisfiable core (only if immediately preceded by an @@ -1000,12 +610,13 @@ class CVC4_PUBLIC SmtEngine { /** * Push a user-level context. + * throw@ ModalException, LogicException, UnsafeInterruptException */ - void - push() /* throw(ModalException, LogicException, UnsafeInterruptException) */; + void push(); /** * Pop a user-level context. Throws an exception if nothing to pop. + * @throw ModalException */ void pop(); @@ -1014,19 +625,19 @@ class CVC4_PUBLIC SmtEngine { * recreated. The result is as if newly constructed (so it still * retains the same options structure and ExprManager). */ - void reset() /* throw() */; + void reset(); - /** - * Reset all assertions, global declarations, etc. - */ - void resetAssertions() /* throw() */; + /** Reset all assertions, global declarations, etc. */ + void resetAssertions(); /** * Interrupt a running query. This can be called from another thread * or from a signal handler. Throws a ModalException if the SmtEngine * isn't currently in a query. + * + * @throw ModalException */ - void interrupt() /* throw(ModalException) */; + void interrupt(); /** * Set a resource limit for SmtEngine operations. This is like a time @@ -1100,9 +711,7 @@ class CVC4_PUBLIC SmtEngine { */ unsigned long getResourceUsage() const; - /** - * Get the current millisecond count for this SmtEngine. - */ + /** Get the current millisecond count for this SmtEngine. */ unsigned long getTimeUsage() const; /** @@ -1110,43 +719,36 @@ class CVC4_PUBLIC SmtEngine { * according to the currently-set cumulative resource limit. If there * is not a cumulative resource limit set, this function throws a * ModalException. + * + * @throw ModalException */ - unsigned long getResourceRemaining() const /* throw(ModalException) */; + unsigned long getResourceRemaining() const; /** * Get the remaining number of milliseconds that can be consumed by * this SmtEngine according to the currently-set cumulative time limit. * If there is not a cumulative resource limit set, this function * throws a ModalException. + * + * @throw ModalException */ - unsigned long getTimeRemaining() const /* throw(ModalException) */; + unsigned long getTimeRemaining() const; - /** - * Permit access to the underlying ExprManager. - */ - ExprManager* getExprManager() const { - return d_exprManager; - } + /** Permit access to the underlying ExprManager. */ + ExprManager* getExprManager() const { return d_exprManager; } - /** - * Export statistics from this SmtEngine. - */ - Statistics getStatistics() const /* throw() */; + /** Export statistics from this SmtEngine. */ + Statistics getStatistics() const; - /** - * Get the value of one named statistic from this SmtEngine. - */ - SExpr getStatistic(std::string name) const /* throw() */; + /** Get the value of one named statistic from this SmtEngine. */ + SExpr getStatistic(std::string name) const; - /** - * Flush statistic from this SmtEngine. Safe to use in a signal handler. - */ + /** Flush statistic from this SmtEngine. Safe to use in a signal handler. */ void safeFlushStatistics(int fd) const; - /** - * Returns the most recent result of checkSat/query or (set-info :status). - */ - Result getStatusOfLastCommand() const /* throw() */ { return d_status; } + /** Returns the most recent result of checkSat/query or (set-info :status). */ + Result getStatusOfLastCommand() const { return d_status; } + /** * Set user attribute. * This function is called when an attribute is set by a user. @@ -1157,18 +759,19 @@ class CVC4_PUBLIC SmtEngine { const std::vector<Expr>& expr_values, const std::string& str_value); - /** - * Set print function in model - */ + /** Set print function in model. */ void setPrintFuncInModel(Expr f, bool p); - - /** Throws a ModalException if the SmtEngine has been fully initialized. */ - void beforeSearch() /* throw(ModalException) */; + /** + * Check and throw a ModalException if the SmtEngine has been fully + * initialized. + * + * throw@ ModalException + */ + void beforeSearch(); LemmaChannels* channels() { return d_channels; } - /** * Expermintal feature: Sets the sequence of decisions. * This currently requires very fine grained knowledge about literal @@ -1176,20 +779,445 @@ class CVC4_PUBLIC SmtEngine { */ void setReplayStream(ExprStream* exprStream); - /** get expression name - * Returns true if e has an expression name in the current context. - * If it returns true, the name of e is stored in name. - */ + /** + * Get expression name. + * + * Return true if given expressoion has a name in the current context. + * If it returns true, the name of expression 'e' is stored in 'name'. + */ bool getExpressionName(Expr e, std::string& name) const; - /** set expression name - * Sets the expression name of e to name. - * This information is user-context-dependent. - * If e already has a name, it is overwritten. - */ + /** + * Set name of given expression 'e' to 'name'. + * + * This information is user-context-dependent. + * If 'e' already has a name, it is overwritten. + */ void setExpressionName(Expr e, const std::string& name); -};/* class SmtEngine */ + /* ....................................................................... */ + private: + /* ....................................................................... */ + + /** The type of our internal map of defined functions */ + typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction> + DefinedFunctionMap; + /** The type of our internal assertion list */ + typedef context::CDList<Expr> AssertionList; + /** The type of our internal assignment set */ + typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet; + /** The types for the recursive function definitions */ + typedef context::CDList<Node> NodeList; + + /** + * The current mode of the solver, see Figure 4.1 on page 52 of the + * SMT-LIB version 2.6 standard + * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf + */ + enum SmtMode + { + // the initial state of the solver + SMT_MODE_START, + // normal state of the solver, after assert/push/pop/declare/define + SMT_MODE_ASSERT, + // immediately after a check-sat returning "sat" or "unknown" + SMT_MODE_SAT, + // immediately after a check-sat returning "unsat" + SMT_MODE_UNSAT, + // immediately after a successful call to get-abduct + SMT_MODE_ABDUCT + }; + + // disallow copy/assignment + SmtEngine(const SmtEngine&) = delete; + SmtEngine& operator=(const SmtEngine&) = delete; + + /** + * Check that a generated proof (via getProof()) checks. + */ + void checkProof(); + + /** + * Internal method to get an unsatisfiable core (only if immediately preceded + * by an UNSAT or VALID query). Only permitted if CVC4 was built with + * unsat-core support and produce-unsat-cores is on. Does not dump the + * command. + */ + UnsatCore getUnsatCoreInternal(); + + /** + * Check that an unsatisfiable core is indeed unsatisfiable. + */ + void checkUnsatCore(); + + /** + * Check that a generated Model (via getModel()) actually satisfies + * all user assertions. + */ + void checkModel(bool hardFailure = true); + + /** + * Check that a solution to a synthesis conjecture is indeed a solution. + * + * The check is made by determining if the negation of the synthesis + * conjecture in which the functions-to-synthesize have been replaced by the + * synthesized solutions, which is a quantifier-free formula, is + * unsatisfiable. If not, then the found solutions are wrong. + */ + void checkSynthSolution(); + /** + * Check that a solution to an abduction conjecture is indeed a solution. + * + * The check is made by determining that the assertions conjoined with the + * solution to the abduction problem (a) is SAT, and the assertions conjoined + * with the abduct and the goal is UNSAT. If these criteria are not met, an + * internal error is thrown. + */ + void checkAbduct(Expr a); + + /** + * Postprocess a value for output to the user. Involves doing things + * like turning datatypes back into tuples, length-1-bitvectors back + * into booleans, etc. + */ + Node postprocess(TNode n, TypeNode expectedType) const; + + /** + * This is something of an "init" procedure, but is idempotent; call + * as often as you like. Should be called whenever the final options + * and logic for the problem are set (at least, those options that are + * not permitted to change after assertions and queries are made). + */ + void finalOptionsAreSet(); + + /** + * Apply heuristics settings and other defaults. Done once, at + * finishInit() time. + */ + void setDefaults(); + + /** + * Sets that the problem has been extended. This sets the smt mode of the + * solver to SMT_MODE_ASSERT, and clears the list of assumptions from the + * previous call to checkSatisfiability. + */ + void setProblemExtended(); + + /** + * Create theory engine, prop engine, decision engine. Called by + * finalOptionsAreSet() + */ + void finishInit(); + + /** + * This is called by the destructor, just before destroying the + * PropEngine, TheoryEngine, and DecisionEngine (in that order). It + * is important because there are destruction ordering issues + * between PropEngine and Theory. + */ + void shutdown(); + + /** + * Full check of consistency in current context. Returns true iff + * consistent. + */ + Result check(); + + /** + * Quick check of consistency in current context: calls + * processAssertionList() then look for inconsistency (based only on + * that). + */ + Result quickCheck(); + + /** + * Get the model, if it is available and return a pointer to it + * + * This ensures that the model is currently available, which means that + * CVC4 is producing models, and is in "SAT mode", otherwise an exception + * is thrown. + * + * The flag c is used for giving an error message to indicate the context + * this method was called. + */ + theory::TheoryModel* getAvailableModel(const char* c) const; + + /** + * Fully type-check the argument, and also type-check that it's + * actually Boolean. + * + * throw@ TypeCheckingException + */ + void ensureBoolean(const Expr& e); + + void internalPush(); + + void internalPop(bool immediate = false); + + void doPendingPops(); + + /** + * Internally handle the setting of a logic. This function should always + * be called when d_logic is updated. + */ + void setLogicInternal(); + + /** + * Add to Model command. This is used for recording a command + * that should be reported during a get-model call. + */ + void addToModelCommandAndDump(const Command& c, + uint32_t flags = 0, + bool userVisible = true, + const char* dumpTag = "declarations"); + + /* Check satisfiability (used for query and check-sat). */ + Result checkSatisfiability(const Expr& assumption, + bool inUnsatCore, + bool isQuery); + Result checkSatisfiability(const std::vector<Expr>& assumptions, + bool inUnsatCore, + bool isQuery); + + /** + * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is + * the function that the formal argument list is for. This method is used + * as a helper function when defining (recursive) functions. + */ + void debugCheckFormals(const std::vector<Expr>& formals, Expr func); + + /** + * Checks whether formula is a valid function body for func whose formal + * argument list is stored in formals. This method is + * used as a helper function when defining (recursive) functions. + */ + void debugCheckFunctionBody(Expr formula, + const std::vector<Expr>& formals, + Expr func); + /** + * Get abduct internal. + * + * Get the next abduct from the internal subsolver d_subsolver. If + * successful, this method returns true and sets abd to that abduct. + * + * This method assumes d_subsolver has been initialized to do abduction + * problems. + */ + bool getAbductInternal(Expr& abd); + + /** + * Helper method to obtain both the heap and nil from the solver. Returns a + * std::pair where the first element is the heap expression and the second + * element is the nil expression. + */ + std::pair<Expr, Expr> getSepHeapAndNilExpr(); + + /** + * Get expanded assertions. + * + * Return the set of assertions, after expanding definitions. + */ + std::vector<Expr> getExpandedAssertions(); + + /* Members -------------------------------------------------------------- */ + + /** Expr manager context */ + context::Context* d_context; + /** User level context */ + context::UserContext* d_userContext; + /** The context levels of user pushes */ + std::vector<int> d_userLevels; + + /** Our expression manager */ + ExprManager* d_exprManager; + /** Our internal expression/node manager */ + NodeManager* d_nodeManager; + /** The decision engine */ + + DecisionEngine* d_decisionEngine; + /** The theory engine */ + TheoryEngine* d_theoryEngine; + /** The propositional engine */ + prop::PropEngine* d_propEngine; + + /** The proof manager */ + ProofManager* d_proofManager; + + /** An index of our defined functions */ + DefinedFunctionMap* d_definedFunctions; + + /** The SMT engine subsolver + * + * This is a separate copy of the SMT engine which is used for making + * calls that cannot be answered by this copy of the SMT engine. An example + * of invoking this subsolver is the get-abduct command, where we wish to + * solve a sygus conjecture based on the current assertions. In particular, + * consider the input: + * (assert A) + * (get-abduct B) + * In the copy of the SMT engine where these commands are issued, we maintain + * A in the assertion stack. To solve the abduction problem, instead of + * modifying the assertion stack to remove A and add the sygus conjecture + * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the + * assertion stack unchaged. This copy of the SMT engine can be further + * queried for information regarding further solutions. + */ + std::unique_ptr<SmtEngine> d_subsolver; + + /** + * If applicable, the function-to-synthesize that the subsolver is solving + * for. This is used for the get-abduct command. + */ + Expr d_sssf; + + /** + * The conjecture of the current abduction problem. This expression is only + * valid while we are in mode SMT_MODE_ABDUCT. + */ + Expr d_abdConj; + + /** recursive function definition abstractions for --fmf-fun */ + std::map<Node, TypeNode> d_fmfRecFunctionsAbs; + std::map<Node, std::vector<Node> > d_fmfRecFunctionsConcrete; + NodeList* d_fmfRecFunctionsDefined; + + /** + * The assertion list (before any conversion) for supporting + * getAssertions(). Only maintained if in interactive mode. + */ + AssertionList* d_assertionList; + + /** + * The list of assumptions from the previous call to checkSatisfiability. + * Note that if the last call to checkSatisfiability was a validity check, + * i.e., a call to query(a1, ..., an), then d_assumptions contains one single + * assumption ~(a1 AND ... AND an). + */ + std::vector<Expr> d_assumptions; + + /** + * List of items for which to retrieve values using getAssignment(). + */ + AssignmentSet* d_assignments; + + /** + * A list of commands that should be in the Model globally (i.e., + * regardless of push/pop). Only maintained if produce-models option + * is on. + */ + std::vector<Command*> d_modelGlobalCommands; + + /** + * A list of commands that should be in the Model locally (i.e., + * it is context-dependent on push/pop). Only maintained if + * produce-models option is on. + */ + smt::CommandList* d_modelCommands; + + /** + * A vector of declaration commands waiting to be dumped out. + * Once the SmtEngine is fully initialized, we'll dump them. + * This ensures the declarations come after the set-logic and + * any necessary set-option commands are dumped. + */ + std::vector<Command*> d_dumpCommands; + + /** + * A vector of command definitions to be imported in the new + * SmtEngine when checking unsat-cores. + */ + std::vector<Command*> d_defineCommands; + + /** + * The logic we're in. + */ + LogicInfo d_logic; + + /** + * Keep a copy of the original option settings (for reset()). + */ + Options d_originalOptions; + + /** Whether this is an internal subsolver. */ + bool d_isInternalSubsolver; + + /** + * Number of internal pops that have been deferred. + */ + unsigned d_pendingPops; + + /** + * Whether or not this SmtEngine is fully initialized (post-construction). + * This post-construction initialization is automatically triggered by the + * use of the SmtEngine; e.g. when the first formula is asserted, a call + * to simplify() is issued, a scope is pushed, etc. + */ + bool d_fullyInited; + + /** + * Whether or not a query() or checkSat() has already been made through + * this SmtEngine. If true, and incrementalSolving is false, then + * attempting an additional query() or checkSat() will fail with a + * ModalException. + */ + bool d_queryMade; + + /** + * Internal status flag to indicate whether we've sent a theory + * presolve() notification and need to match it with a postsolve(). + */ + bool d_needPostsolve; + + /* + * Whether to call theory preprocessing during simplification - on + * by default* but gets turned off if arithRewriteEq is on + */ + bool d_earlyTheoryPP; + + /* + * Whether we did a global negation of the formula. + */ + bool d_globalNegation; + + /** + * Most recent result of last checkSat/query or (set-info :status). + */ + Result d_status; + + /** + * The expected status of the next satisfiability check. + */ + Result d_expectedStatus; + + SmtMode d_smtMode; + + /** + * The input file name (if any) or the name set through setInfo (if any) + */ + std::string d_filename; + + /** + * Verbosity of various commands. + */ + std::map<std::string, Integer> d_commandVerbosity; + + /** ReplayStream for the solver. */ + ExprStream* d_replayStream; + + /** + * A private utility class to SmtEngine. + */ + smt::SmtEnginePrivate* d_private; + + StatisticsRegistry* d_statisticsRegistry; + + smt::SmtEngineStatistics* d_stats; + + /** Container for the lemma input and output channels for this SmtEngine.*/ + LemmaChannels* d_channels; +}; /* class SmtEngine */ + +/* -------------------------------------------------------------------------- */ }/* CVC4 namespace */ |