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
typedef context::CDList<Command*, CommandCleanup> CommandList;
}/* CVC4::smt namespace */
+/* -------------------------------------------------------------------------- */
+
namespace theory {
class TheoryModel;
}/* CVC4::theory namespace */
//
// 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;
+class CVC4_PUBLIC SmtEngine
+{
+ // TODO (Issue #1096): Remove this friend relationship.
+ friend class ::CVC4::preprocessing::PreprocessingPassContext;
+ friend class ::CVC4::smt::SmtEnginePrivate;
+ friend class ::CVC4::smt::SmtScope;
+ friend class ::CVC4::smt::BooleanTermConverter;
+ friend ProofManager* ::CVC4::smt::currentProofManager();
+ friend class ::CVC4::LogicRequest;
+ friend class ::CVC4::Model; // to access d_modelCommands
+ friend class ::CVC4::theory::TheoryModel;
- /** Expr manager context */
- context::Context* d_context;
+ /* ....................................................................... */
+ public:
+ /* ....................................................................... */
- /** The context levels of user pushes */
- std::vector<int> d_userLevels;
- /** User level context */
- context::UserContext* d_userContext;
+ /** Construct an SmtEngine with the given expression manager. */
+ SmtEngine(ExprManager* em);
+ /** Destruct the SMT engine. */
+ ~SmtEngine();
- /** 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.
+ * Return true if 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.
*/
- Expr d_sssf;
+ bool isFullyInited() { return d_fullyInited; }
+
+ /** Return the user context level. */
+ size_t getNumUserLevels() { return d_userLevels.size(); }
+
/**
- * The conjecture of the current abduction problem. This expression is only
- * valid while we are in mode SMT_MODE_ABDUCT.
+ * Set the logic of the script.
+ * @throw ModalException, LogicException
*/
- 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;
+ void setLogic(const std::string& logic);
/**
- * The assertion list (before any conversion) for supporting
- * getAssertions(). Only maintained if in interactive mode.
+ * Set the logic of the script.
+ * @throw ModalException, LogicException
*/
- AssertionList* d_assertionList;
+ void setLogic(const char* logic);
/**
- * 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).
+ * Set the logic of the script.
+ * @throw ModalException
*/
- std::vector<Expr> d_assumptions;
+ void setLogic(const LogicInfo& logic);
+
+ /** Get the logic information currently set. */
+ LogicInfo getLogicInfo() const;
/**
- * List of items for which to retrieve values using getAssignment().
+ * Set information about the script executing.
+ * @throw OptionException, ModalException
*/
- AssignmentSet* d_assignments;
+ void setInfo(const std::string& key, const CVC4::SExpr& value);
+
+ /** Query information about the SMT environment. */
+ CVC4::SExpr getInfo(const std::string& key) const;
/**
- * 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.
+ * Set an aspect of the current SMT execution environment.
+ * @throw OptionException, ModalException
*/
- std::vector<Command*> d_modelGlobalCommands;
+ void setOption(const std::string& key, const CVC4::SExpr& value);
+
+ /** Set is internal subsolver.
+ *
+ * This function is called on SmtEngine objects that are created internally.
+ * It is used to mark that this SmtEngine should not perform preprocessing
+ * passes that rephrase the input, such as --sygus-rr-synth-input or
+ * --sygus-abduct.
+ */
+ void setIsInternalSubsolver();
+
+ /** set the input name */
+ void setFilename(std::string filename);
+ /** return the input name (if any) */
+ std::string getFilename() const;
/**
- * 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.
+ * Get the model (only if immediately preceded by a SAT
+ * or INVALID query). Only permitted if produce-models is on.
*/
- smt::CommandList* d_modelCommands;
+ Model* getModel();
/**
- * 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.
+ * Block the current model. Can be called only if immediately preceded by
+ * a SAT or INVALID query. Only permitted if produce-models is on, and the
+ * block-models option is set to a mode other than "none".
+ *
+ * This adds an assertion to the assertion stack that blocks the current
+ * model based on the current options configured by CVC4.
+ *
+ * The return value has the same meaning as that of assertFormula.
*/
- std::vector<Command*> d_dumpCommands;
+ Result blockModel();
/**
- * A vector of command definitions to be imported in the new
- * SmtEngine when checking unsat-cores.
+ * Block the current model values of (at least) the values in exprs.
+ * Can be called only if immediately preceded by a SAT or INVALID query. Only
+ * permitted if produce-models is on, and the block-models option is set to a
+ * mode other than "none".
+ *
+ * This adds an assertion to the assertion stack of the form:
+ * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
+ * where M0 ... Mn are the current model values of exprs[0] ... exprs[n].
+ *
+ * The return value has the same meaning as that of assertFormula.
*/
- std::vector<Command*> d_defineCommands;
+ Result blockModelValues(const std::vector<Expr>& exprs);
+
+ /** When using separation logic, obtain the expression for the heap. */
+ Expr getSepHeapExpr();
+
+ /** When using separation logic, obtain the expression for nil. */
+ Expr getSepNilExpr();
/**
- * The logic we're in.
+ * Get an aspect of the current SMT execution environment.
+ * @throw OptionException
*/
- LogicInfo d_logic;
+ CVC4::SExpr getOption(const std::string& key) const;
/**
- * Keep a copy of the original option settings (for reset()).
+ * Define function func in the current context to be:
+ * (lambda (formals) formula)
+ * This adds func to the list of defined functions, which indicates that
+ * all occurrences of func should be expanded during expandDefinitions.
+ * This method expects input such that:
+ * - func : a variable of function type that expects the arguments in
+ * formals,
+ * - formals : a list of BOUND_VARIABLE expressions,
+ * - formula does not contain func.
*/
- Options d_originalOptions;
+ void defineFunction(Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula);
- /** whether this is an internal subsolver */
- bool d_isInternalSubsolver;
+ /** Return true if given expression is a defined function. */
+ bool isDefinedFunction(Expr func);
/**
- * Number of internal pops that have been deferred.
+ * Define functions recursive
+ *
+ * For each i, this constrains funcs[i] in the current context to be:
+ * (lambda (formals[i]) formulas[i])
+ * where formulas[i] may contain variables from funcs. Unlike defineFunction
+ * above, we do not add funcs[i] to the set of defined functions. Instead,
+ * we consider funcs[i] to be a free uninterpreted function, and add:
+ * forall formals[i]. f(formals[i]) = formulas[i]
+ * to the set of assertions in the current context.
+ * This method expects input such that for each i:
+ * - func[i] : a variable of function type that expects the arguments in
+ * formals[i], and
+ * - formals[i] : a list of BOUND_VARIABLE expressions.
*/
- unsigned d_pendingPops;
-
+ void defineFunctionsRec(const std::vector<Expr>& funcs,
+ const std::vector<std::vector<Expr> >& formals,
+ const std::vector<Expr>& formulas);
/**
- * 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.
+ * Define function recursive
+ * Same as above, but for a single function.
*/
- bool d_fullyInited;
-
+ void defineFunctionRec(Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula);
/**
- * 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.
+ * Add a formula to the current context: preprocess, do per-theory
+ * setup, use processAssertionList(), asserting to T-solver for
+ * literals and conjunction of literals. Returns false if
+ * 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
*/
- bool d_queryMade;
+ Result assertFormula(const Expr& e, bool inUnsatCore = true);
/**
- * Internal status flag to indicate whether we've sent a theory
- * presolve() notification and need to match it with a postsolve().
+ * 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
*/
- bool d_needPostsolve;
+ Result query(const Expr& assumption = Expr(), bool inUnsatCore = true);
+ Result query(const std::vector<Expr>& assumptions, bool inUnsatCore = true);
- /*
- * Whether to call theory preprocessing during simplification - on
- * by default* but gets turned off if arithRewriteEq is on
+ /**
+ * Assert a formula (if provided) to the current context and call
+ * check(). Returns sat, unsat, or unknown result.
+ *
+ * @throw Exception
*/
- bool d_earlyTheoryPP;
+ Result checkSat(const Expr& assumption = Expr(), bool inUnsatCore = true);
+ Result checkSat(const std::vector<Expr>& assumptions,
+ bool inUnsatCore = true);
- /*
- * Whether we did a global negation of the formula.
+ /**
+ * Returns a set of so-called "failed" assumptions.
+ *
+ * The returned set is a subset of the set of assumptions of a previous
+ * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability
+ * with this set of failed assumptions still produces an unsat answer.
+ *
+ * Note that the returned set of failed assumptions is not necessarily
+ * minimal.
*/
- bool d_globalNegation;
+ std::vector<Expr> getUnsatAssumptions(void);
+
+ /*---------------------------- sygus commands ---------------------------*/
/**
- * Most recent result of last checkSat/query or (set-info :status).
+ * Add variable declaration.
+ *
+ * Declared SyGuS variables may be used in SyGuS constraints, in which they
+ * are assumed to be universally quantified.
*/
- Result d_status;
+ void declareSygusVar(const std::string& id, Expr var, Type type);
/**
- * The expected status of the next satisfiability check.
+ * 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
+ * of variables declared corresponds to the number of arguments of the
+ * invariant-to-synthesize.
*/
- Result d_expectedStatus;
+ void declareSygusPrimedVar(const std::string& id, Type type);
/**
- * 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
+ * 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
+ * which can occur in the SyGuS constraints that compose the conjecture to
+ * which a function is being synthesized.
*/
- 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;
+ void declareSygusFunctionVar(const std::string& id, Expr var, Type type);
/**
- * The input file name (if any) or the name set through setInfo (if any)
+ * 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
+ * function-to-synthesize. In this case this information is stored to be used
+ * during solving.
+ *
+ * vars contains the arguments of the function-to-synthesize. These variables
+ * are also stored to be used during solving.
+ *
+ * isInv determines whether the function-to-synthesize is actually an
+ * invariant. This information is necessary if we are dumping a command
+ * corresponding to this declaration, so that it can be properly printed.
*/
- std::string d_filename;
+ void declareSynthFun(const std::string& id,
+ Expr func,
+ Type type,
+ bool isInv,
+ const std::vector<Expr>& vars);
+
+ /** Add a regular sygus constraint.*/
+ void assertSygusConstraint(Expr constraint);
/**
- * Verbosity of various commands.
+ * 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
+ * post condition. The actual constraint is built based on the inputs of these
+ * place holder predicates :
+ *
+ * PRE(x) -> INV(x)
+ * INV() ^ TRANS(x, x') -> INV(x')
+ * INV(x) -> POST(x)
+ *
+ * The regular and primed variables are retrieved from the declaration of the
+ * invariant-to-synthesize.
*/
- std::map<std::string, Integer> d_commandVerbosity;
-
+ void assertSygusInvConstraint(const Expr& inv,
+ const Expr& pre,
+ const Expr& trans,
+ const Expr& post);
+ /**
+ * Assert a synthesis conjecture to the current context and call
+ * check(). Returns sat, unsat, or unknown result.
+ *
+ * The actual synthesis conjecture is built based on the previously
+ * communicated information to this module (universal variables, defined
+ * functions, functions-to-synthesize, and which constraints compose it). The
+ * built conjecture is a higher-order formula of the form
+ *
+ * exists f1...fn . forall v1...vm . F
+ *
+ * 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();
- /** ReplayStream for the solver. */
- ExprStream* d_replayStream;
+ /*------------------------- end of sygus commands ------------------------*/
/**
- * A private utility class to SmtEngine.
+ * Simplify a formula without doing "much" work. Does not involve
+ * the SAT Engine in the simplification, but uses the current
+ * 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?
*/
- smt::SmtEnginePrivate* d_private;
+ Expr simplify(const Expr& e);
/**
- * Check that a generated proof (via getProof()) checks.
+ * Expand the definitions in a term or formula. No other
+ * simplification or normalization is done.
+ *
+ * @throw TypeCheckingException, LogicException, UnsafeInterruptException
*/
- void checkProof();
+ Expr expandDefinitions(const Expr& e);
/**
- * 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.
+ * 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
*/
- UnsatCore getUnsatCoreInternal();
+ Expr getValue(const Expr& e) const;
/**
- * Check that an unsatisfiable core is indeed unsatisfiable.
+ * Same as getValue but for a vector of expressions
*/
- void checkUnsatCore();
+ std::vector<Expr> getValues(const std::vector<Expr>& exprs);
/**
- * Check that a generated Model (via getModel()) actually satisfies
- * all user assertions.
+ * Add a function to the set of expressions whose value is to be
+ * later returned by a call to getAssignment(). The expression
+ * should be a Boolean zero-ary defined function or a Boolean
+ * variable. Rather than throwing a ModalException on modal
+ * failures (not in interactive mode or not producing assignments),
+ * this function returns true if the expression was added and false
+ * if this request was ignored.
*/
- void checkModel(bool hardFailure = true);
+ bool addToAssignment(const Expr& e);
/**
- * 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.
+ * Get the assignment (only if immediately preceded by a SAT or
+ * INVALID query). Only permitted if the SmtEngine is set to
+ * operate interactively and produce-assignments is on.
*/
- void checkSynthSolution();
+ std::vector<std::pair<Expr, Expr> > getAssignment();
+
/**
- * Check that a solution to an abduction conjecture is indeed a solution.
+ * Get the last proof (only if immediately preceded by an UNSAT
+ * or VALID query). Only permitted if CVC4 was built with proof
+ * support and produce-proofs is on.
*
- * 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.
+ * The Proof object is owned by this SmtEngine until the SmtEngine is
+ * destroyed.
*/
- void checkAbduct(Expr a);
+ const Proof& getProof();
+
+ /** Print all instantiations made by the quantifiers module. */
+ void printInstantiations(std::ostream& out);
/**
- * Postprocess a value for output to the user. Involves doing things
- * like turning datatypes back into tuples, length-1-bitvectors back
- * into booleans, etc.
+ * Print solution for synthesis conjectures found by counter-example guided
+ * instantiation module.
*/
- Node postprocess(TNode n, TypeNode expectedType) const;
+ void printSynthSolution(std::ostream& out);
/**
- * 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).
+ * 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
+ * immediately after the solver answers unsat for sygus input.
+ *
+ * Specifically, given a sygus conjecture of the form
+ * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn )
+ * where x1...xn are second order bound variables, we map each xi to
+ * lambda term in sol_map such that
+ * forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn )
+ * is a valid formula.
*/
- void finalOptionsAreSet();
+ void getSynthSolutions(std::map<Expr, Expr>& sol_map);
/**
- * Apply heuristics settings and other defaults. Done once, at
- * finishInit() time.
+ * Do quantifier elimination.
+ *
+ * This function takes as input a quantified formula e
+ * of the form:
+ * Q x1...xn. P( x1...xn, y1...yn )
+ * where P( x1...xn, y1...yn ) is a quantifier-free
+ * formula in a logic that supports quantifier elimination.
+ * Currently, the only logics supported by quantifier
+ * elimination is LRA and LIA.
+ *
+ * This function returns a formula ret such that, given
+ * the current set of formulas A asserted to this SmtEngine :
+ *
+ * If doFull = true, then
+ * - ( A ^ e ) and ( A ^ ret ) are equivalent
+ * - ret is quantifier-free formula containing
+ * only free variables in y1...yn.
+ *
+ * If doFull = false, then
+ * - (A ^ e) => (A ^ ret) if Q is forall or
+ * (A ^ ret) => (A ^ e) if Q is exists,
+ * - ret is quantifier-free formula containing
+ * only free variables in y1...yn,
+ * - If Q is exists, let A^Q_n be the formula
+ * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
+ * where for each i=1,...n, formula ret^Q_i
+ * is the result of calling doQuantifierElimination
+ * for e with the set of assertions A^Q_{i-1}.
+ * Similarly, if Q is forall, then let A^Q_n be
+ * A ^ ret^Q_1 ^ ... ^ ret^Q_n
+ * where ret^Q_i is the same as above.
+ * In either case, we have that ret^Q_j will
+ * eventually be true or false, for some finite j.
+ *
+ * The former feature is quantifier elimination, and
+ * is run on invocations of the smt2 extended command get-qe.
+ * The latter feature is referred to as partial quantifier
+ * elimination, and is run on invocations of the smt2
+ * 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
*/
- void setDefaults();
+ Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true);
/**
- * 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.
+ * 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).
+ * If this method returns true, then abd is set to a formula C such that
+ * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
+ *
+ * The argument grammarType is a sygus datatype type that encodes the syntax
+ * restrictions on the shape of possible solutions.
+ *
+ * This method invokes a separate copy of the SMT engine for solving the
+ * corresponding sygus problem for generating such a solution.
*/
- void setProblemExtended();
+ 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);
/**
- * Create theory engine, prop engine, decision engine. Called by
- * finalOptionsAreSet()
+ * 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.
*/
- void finishInit();
+ UnsatCore getUnsatCore();
/**
- * 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.
+ * Get the current set of assertions. Only permitted if the
+ * SmtEngine is set to operate interactively.
*/
- void shutdown();
+ std::vector<Expr> getAssertions();
/**
- * Full check of consistency in current context. Returns true iff
- * consistent.
+ * Push a user-level context.
+ * throw@ ModalException, LogicException, UnsafeInterruptException
*/
- Result check();
+ void push();
/**
- * Quick check of consistency in current context: calls
- * processAssertionList() then look for inconsistency (based only on
- * that).
+ * Pop a user-level context. Throws an exception if nothing to pop.
+ * @throw ModalException
*/
- 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.
+ void pop();
+
+ /**
+ * Completely reset the state of the solver, as though destroyed and
+ * recreated. The result is as if newly constructed (so it still
+ * retains the same options structure and ExprManager).
+ */
+ void reset();
+
+ /** 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.
*
- * The flag c is used for giving an error message to indicate the context
- * this method was called.
+ * @throw ModalException
*/
- theory::TheoryModel* getAvailableModel(const char* c) const;
+ void interrupt();
/**
- * Fully type-check the argument, and also type-check that it's
- * actually Boolean.
+ * Set a resource limit for SmtEngine operations. This is like a time
+ * limit, but it's deterministic so that reproducible results can be
+ * obtained. Currently, it's based on the number of conflicts.
+ * However, please note that the definition may change between different
+ * versions of CVC4 (as may the number of conflicts required, anyway),
+ * and it might even be different between instances of the same version
+ * of CVC4 on different platforms.
+ *
+ * A cumulative and non-cumulative (per-call) resource limit can be
+ * set at the same time. A call to setResourceLimit() with
+ * cumulative==true replaces any cumulative resource limit currently
+ * in effect; a call with cumulative==false replaces any per-call
+ * resource limit currently in effect. Time limits can be set in
+ * addition to resource limits; the SmtEngine obeys both. That means
+ * that up to four independent limits can control the SmtEngine
+ * at the same time.
+ *
+ * When an SmtEngine is first created, it has no time or resource
+ * limits.
+ *
+ * Currently, these limits only cause the SmtEngine to stop what its
+ * doing when the limit expires (or very shortly thereafter); no
+ * heuristics are altered by the limits or the threat of them expiring.
+ * We reserve the right to change this in the future.
+ *
+ * @param units the resource limit, or 0 for no limit
+ * @param cumulative whether this resource limit is to be a cumulative
+ * resource limit for all remaining calls into the SmtEngine (true), or
+ * whether it's a per-call resource limit (false); the default is false
*/
- void ensureBoolean(const Expr& e) /* throw(TypeCheckingException) */;
+ void setResourceLimit(unsigned long units, bool cumulative = false);
- void internalPush();
+ /**
+ * Set a time limit for SmtEngine operations.
+ *
+ * A cumulative and non-cumulative (per-call) time limit can be
+ * set at the same time. A call to setTimeLimit() with
+ * cumulative==true replaces any cumulative time limit currently
+ * in effect; a call with cumulative==false replaces any per-call
+ * time limit currently in effect. Resource limits can be set in
+ * addition to time limits; the SmtEngine obeys both. That means
+ * that up to four independent limits can control the SmtEngine
+ * at the same time.
+ *
+ * Note that the cumulative timer only ticks away when one of the
+ * SmtEngine's workhorse functions (things like assertFormula(),
+ * query(), checkSat(), and simplify()) are running. Between calls,
+ * the timer is still.
+ *
+ * When an SmtEngine is first created, it has no time or resource
+ * limits.
+ *
+ * Currently, these limits only cause the SmtEngine to stop what its
+ * doing when the limit expires (or very shortly thereafter); no
+ * heuristics are altered by the limits or the threat of them expiring.
+ * We reserve the right to change this in the future.
+ *
+ * @param millis the time limit in milliseconds, or 0 for no limit
+ * @param cumulative whether this time limit is to be a cumulative
+ * time limit for all remaining calls into the SmtEngine (true), or
+ * whether it's a per-call time limit (false); the default is false
+ */
+ void setTimeLimit(unsigned long millis, bool cumulative = false);
- void internalPop(bool immediate = false);
+ /**
+ * Get the current resource usage count for this SmtEngine. This
+ * function can be used to ascertain reasonable values to pass as
+ * resource limits to setResourceLimit().
+ */
+ unsigned long getResourceUsage() const;
- void doPendingPops();
+ /** Get the current millisecond count for this SmtEngine. */
+ unsigned long getTimeUsage() const;
/**
- * Internally handle the setting of a logic. This function should always
- * be called when d_logic is updated.
+ * Get the remaining resources that can be consumed by this 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
*/
- void setLogicInternal() /* throw() */;
+ unsigned long getResourceRemaining() const;
- // TODO (Issue #1096): Remove this friend relationship.
- friend class ::CVC4::preprocessing::PreprocessingPassContext;
- friend class ::CVC4::smt::SmtEnginePrivate;
- friend class ::CVC4::smt::SmtScope;
- 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::theory::TheoryModel;
+ /**
+ * 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;
- StatisticsRegistry* d_statisticsRegistry;
+ /** Permit access to the underlying ExprManager. */
+ ExprManager* getExprManager() const { return d_exprManager; }
- smt::SmtEngineStatistics* d_stats;
+ /** Export statistics from this SmtEngine. */
+ Statistics getStatistics() const;
- /** Container for the lemma input and output channels for this SmtEngine.*/
- LemmaChannels* d_channels;
+ /** 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. */
+ void safeFlushStatistics(int fd) const;
+
+ /** Returns the most recent result of checkSat/query or (set-info :status). */
+ Result getStatusOfLastCommand() const { return d_status; }
/**
- * Add to Model command. This is used for recording a command
- * that should be reported during a get-model call.
+ * Set user attribute.
+ * This function is called when an attribute is set by a user.
+ * In SMT-LIBv2 this is done via the syntax (! expr :attr)
*/
- 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;
+ void setUserAttribute(const std::string& attr,
+ Expr expr,
+ const std::vector<Expr>& expr_values,
+ const std::string& str_value);
- //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);
+ /** Set print function in model. */
+ void setPrintFuncInModel(Expr f, bool p);
/**
- * 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.
+ * Check and throw a ModalException if the SmtEngine has been fully
+ * initialized.
+ *
+ * throw@ ModalException
*/
- void debugCheckFormals(const std::vector<Expr>& formals, Expr func);
+ void beforeSearch();
+
+ LemmaChannels* channels() { return d_channels; }
/**
- * 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.
+ * Expermintal feature: Sets the sequence of decisions.
+ * This currently requires very fine grained knowledge about literal
+ * translation.
*/
- bool getAbductInternal(Expr& abd);
+ void setReplayStream(ExprStream* exprStream);
/**
- * 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.
+ * 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'.
*/
- std::pair<Expr, Expr> getSepHeapAndNilExpr();
+ bool getExpressionName(Expr e, std::string& name) const;
- /** get expanded assertions
+ /**
+ * Set name of given expression 'e' to 'name'.
*
- * Returns the set of assertions, after expanding definitions.
+ * This information is user-context-dependent.
+ * If 'e' already has a name, it is overwritten.
*/
- std::vector<Expr> getExpandedAssertions();
+ void setExpressionName(Expr e, const std::string& name);
- public:
+ /* ....................................................................... */
+ 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;
/**
- * Construct an SmtEngine with the given expression manager.
+ * 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
*/
- SmtEngine(ExprManager* em) /* throw() */;
+ 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;
/**
- * Destruct the SMT engine.
+ * Check that a generated proof (via getProof()) checks.
*/
- ~SmtEngine();
+ void checkProof();
/**
- * Return true if 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.
+ * 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.
*/
- bool isFullyInited() { return d_fullyInited; }
+ UnsatCore getUnsatCoreInternal();
/**
- * Return the user context level.
+ * Check that an unsatisfiable core is indeed unsatisfiable.
*/
- size_t getNumUserLevels() { return d_userLevels.size(); }
+ void checkUnsatCore();
/**
- * Set the logic of the script.
+ * Check that a generated Model (via getModel()) actually satisfies
+ * all user assertions.
*/
- void setLogic(
- const std::string& logic) /* throw(ModalException, LogicException) */;
+ void checkModel(bool hardFailure = true);
/**
- * Set the logic of the script.
+ * 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 setLogic(const char* logic) /* throw(ModalException, LogicException) */;
-
+ void checkSynthSolution();
/**
- * Set the logic of the script.
+ * 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 setLogic(const LogicInfo& logic) /* throw(ModalException) */;
+ void checkAbduct(Expr a);
/**
- * Get the logic information currently set
+ * Postprocess a value for output to the user. Involves doing things
+ * like turning datatypes back into tuples, length-1-bitvectors back
+ * into booleans, etc.
*/
- LogicInfo getLogicInfo() const;
+ Node postprocess(TNode n, TypeNode expectedType) const;
/**
- * Set information about the script executing.
+ * 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 setInfo(const std::string& key, const CVC4::SExpr& value)
- /* throw(OptionException, ModalException) */;
+ void finalOptionsAreSet();
/**
- * Query information about the SMT environment.
+ * Apply heuristics settings and other defaults. Done once, at
+ * finishInit() time.
*/
- CVC4::SExpr getInfo(const std::string& key) const;
+ void setDefaults();
/**
- * Set an aspect of the current SMT execution environment.
- */
- void setOption(const std::string& key, const CVC4::SExpr& value)
- /* throw(OptionException, ModalException) */;
-
- /** Set is internal subsolver.
- *
- * This function is called on SmtEngine objects that are created internally.
- * It is used to mark that this SmtEngine should not perform preprocessing
- * passes that rephrase the input, such as --sygus-rr-synth-input or
- * --sygus-abduct.
- */
- void setIsInternalSubsolver();
-
- /** sets 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.
- */
- Model* getModel();
-
- /**
- * Block the current model. Can be called only if immediately preceded by
- * a SAT or INVALID query. Only permitted if produce-models is on, and the
- * block-models option is set to a mode other than "none".
- *
- * This adds an assertion to the assertion stack that blocks the current
- * model based on the current options configured by CVC4.
- *
- * The return value has the same meaning as that of assertFormula.
- */
- Result blockModel();
-
- /**
- * Block the current model values of (at least) the values in exprs.
- * Can be called only if immediately preceded by a SAT or INVALID query. Only
- * permitted if produce-models is on, and the block-models option is set to a
- * mode other than "none".
- *
- * This adds an assertion to the assertion stack of the form:
- * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
- * where M0 ... Mn are the current model values of exprs[0] ... exprs[n].
- *
- * The return value has the same meaning as that of assertFormula.
- */
- Result blockModelValues(const std::vector<Expr>& exprs);
-
- /**
- * When using separation logic, obtain the expression for the heap.
- */
- Expr getSepHeapExpr();
-
- /**
- * When using separation logic, obtain the expression for nil.
- */
- Expr getSepNilExpr();
-
- /**
- * Get an aspect of the current SMT execution environment.
+ * 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.
*/
- CVC4::SExpr getOption(const std::string& key) const
- /* throw(OptionException) */;
+ void setProblemExtended();
/**
- * Define function func in the current context to be:
- * (lambda (formals) formula)
- * This adds func to the list of defined functions, which indicates that
- * all occurrences of func should be expanded during expandDefinitions.
- * This method expects input such that:
- * - func : a variable of function type that expects the arguments in
- * formals,
- * - formals : a list of BOUND_VARIABLE expressions,
- * - formula does not contain func.
- */
- void defineFunction(Expr func,
- const std::vector<Expr>& formals,
- Expr formula);
-
- /** is defined function */
- bool isDefinedFunction(Expr func);
-
- /** Define functions recursive
- *
- * For each i, this constrains funcs[i] in the current context to be:
- * (lambda (formals[i]) formulas[i])
- * where formulas[i] may contain variables from funcs. Unlike defineFunction
- * above, we do not add funcs[i] to the set of defined functions. Instead,
- * we consider funcs[i] to be a free uninterpreted function, and add:
- * forall formals[i]. f(formals[i]) = formulas[i]
- * to the set of assertions in the current context.
- * This method expects input such that for each i:
- * - func[i] : a variable of function type that expects the arguments in
- * formals[i], and
- * - formals[i] : a list of BOUND_VARIABLE expressions.
- */
- void defineFunctionsRec(const std::vector<Expr>& funcs,
- const std::vector<std::vector<Expr> >& formals,
- const std::vector<Expr>& formulas);
-
- /** Define function recursive
- *
- * Same as above, but for a single function.
+ * Create theory engine, prop engine, decision engine. Called by
+ * finalOptionsAreSet()
*/
- void defineFunctionRec(Expr func,
- const std::vector<Expr>& formals,
- Expr formula);
+ void finishInit();
/**
- * Add a formula to the current context: preprocess, do per-theory
- * setup, use processAssertionList(), asserting to T-solver for
- * literals and conjunction of literals. Returns false if
- * 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).
+ * 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.
*/
- Result assertFormula(const Expr& e, bool inUnsatCore = true)
- /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
- ;
+ void shutdown();
/**
- * 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.
+ * Full check of consistency in current context. Returns true iff
+ * consistent.
*/
- Result query(const Expr& assumption = Expr(),
- bool inUnsatCore = true) /* throw(Exception) */;
- Result query(const std::vector<Expr>& assumptions,
- bool inUnsatCore = true) /* throw(Exception) */;
+ Result check();
/**
- * Assert a formula (if provided) to the current context and call
- * check(). Returns sat, unsat, or unknown result.
+ * Quick check of consistency in current context: calls
+ * processAssertionList() then look for inconsistency (based only on
+ * that).
*/
- Result checkSat(const Expr& assumption = Expr(),
- bool inUnsatCore = true) /* throw(Exception) */;
- Result checkSat(const std::vector<Expr>& assumptions,
- bool inUnsatCore = true) /* throw(Exception) */;
+ Result quickCheck();
/**
- * Returns a set of so-called "failed" assumptions.
+ * Get the model, if it is available and return a pointer to it
*
- * The returned set is a subset of the set of assumptions of a previous
- * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability
- * with this set of failed assumptions still produces an unsat answer.
- *
- * Note that the returned set of failed assumptions is not necessarily
- * minimal.
- */
- std::vector<Expr> getUnsatAssumptions(void);
-
- /*------------------- sygus commands ------------------*/
-
- /** adds a 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
- *
- * Since in SyGuS the commands "declare-primed-var" are not necessary for
- * building invariant constraints, we only use them to check that the number
- * of variables declared corresponds to the number of arguments of the
- * invariant-to-synthesize.
- */
- void declareSygusPrimedVar(const std::string& id, Type type);
- /** adds 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
- * which can occur in the SyGuS constraints that compose the conjecture to
- * which a function is being synthesized.
- */
- void declareSygusFunctionVar(const std::string& id, Expr var, Type type);
- /** adds 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
- * function-to-synthesize. In this case this information is stored to be used
- * during solving.
- *
- * vars contains the arguments of the function-to-synthesize. These variables
- * are also stored to be used during solving.
- *
- * isInv determines whether the function-to-synthesize is actually an
- * invariant. This information is necessary if we are dumping a command
- * corresponding to this declaration, so that it can be properly printed.
- */
- void declareSynthFun(const std::string& id,
- Expr func,
- Type type,
- bool isInv,
- const std::vector<Expr>& vars);
- /** adds a regular sygus constraint */
- void assertSygusConstraint(Expr constraint);
- /** adds 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
- * post condition. The actual constraint is built based on the inputs of these
- * place holder predicates :
- *
- * PRE(x) -> INV(x)
- * INV() ^ TRANS(x, x') -> INV(x')
- * INV(x) -> POST(x)
- *
- * The regular and primed variables are retrieved from the declaration of the
- * invariant-to-synthesize.
- */
- void assertSygusInvConstraint(const Expr& inv,
- const Expr& pre,
- const Expr& trans,
- const Expr& post);
- /**
- * Assert a synthesis conjecture to the current context and call
- * check(). Returns sat, unsat, or unknown result.
- *
- * The actual synthesis conjecture is built based on the previously
- * communicated information to this module (universal variables, defined
- * functions, functions-to-synthesize, and which constraints compose it). The
- * built conjecture is a higher-order formula of the form
- *
- * exists f1...fn . forall v1...vm . F
+ * 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.
*
- * in which f1...fn are the functions-to-synthesize, v1...vm are the declared
- * universal variables and F is the set of declared constraints.
+ * The flag c is used for giving an error message to indicate the context
+ * this method was called.
*/
- Result checkSynth() /* throw(Exception) */;
-
- /*------------------- end of sygus commands-------------*/
+ theory::TheoryModel* getAvailableModel(const char* c) const;
/**
- * Simplify a formula without doing "much" work. Does not involve
- * the SAT Engine in the simplification, but uses the current
- * definitions, assertions, and the current partial model, if one
- * has been constructed. It also involves theory normalization.
+ * Fully type-check the argument, and also type-check that it's
+ * actually Boolean.
*
- * @todo (design) is this meant to give an equivalent or an
- * equisatisfiable formula?
+ * throw@ TypeCheckingException
*/
- Expr simplify(
- const Expr&
- e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
- ;
+ void ensureBoolean(const Expr& e);
- /**
- * Expand the definitions in a term or formula. No other
- * simplification or normalization is done.
- */
- Expr expandDefinitions(
- const Expr&
- e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
- ;
-
- /**
- * 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.
- */
- Expr getValue(const Expr& e) const
- /* throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) */
- ;
-
- /**
- * Same as getValue but for a vector of expressions
- */
- std::vector<Expr> getValues(const std::vector<Expr>& exprs);
+ void internalPush();
- /**
- * Add a function to the set of expressions whose value is to be
- * later returned by a call to getAssignment(). The expression
- * should be a Boolean zero-ary defined function or a Boolean
- * variable. Rather than throwing a ModalException on modal
- * failures (not in interactive mode or not producing assignments),
- * this function returns true if the expression was added and false
- * if this request was ignored.
- */
- bool addToAssignment(const Expr& e);
+ void internalPop(bool immediate = false);
- /**
- * Get the assignment (only if immediately preceded by a SAT or
- * INVALID query). Only permitted if the SmtEngine is set to
- * operate interactively and produce-assignments is on.
- */
- std::vector<std::pair<Expr, Expr> > getAssignment();
+ void doPendingPops();
/**
- * Get the last proof (only if immediately preceded by an UNSAT
- * or VALID query). Only permitted if CVC4 was built with proof
- * support and produce-proofs is on.
- *
- * The Proof object is owned by this SmtEngine until the SmtEngine is
- * destroyed.
+ * Internally handle the setting of a logic. This function should always
+ * be called when d_logic is updated.
*/
- const Proof& getProof();
+ void setLogicInternal();
/**
- * Print all instantiations made by the quantifiers module.
+ * Add to Model command. This is used for recording a command
+ * that should be reported during a get-model call.
*/
- void printInstantiations( std::ostream& out );
+ void addToModelCommandAndDump(const Command& c,
+ uint32_t flags = 0,
+ bool userVisible = true,
+ const char* dumpTag = "declarations");
- /**
- * Print solution for synthesis conjectures found by ce_guided_instantiation module
- */
- void printSynthSolution( std::ostream& out );
+ /* 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);
/**
- * 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
- * immediately after the solver answers unsat for sygus input.
- *
- * Specifically, given a sygus conjecture of the form
- * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn )
- * where x1...xn are second order bound variables, we map each xi to
- * lambda term in sol_map such that
- * forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn )
- * is a valid formula.
+ * 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 getSynthSolutions(std::map<Expr, Expr>& sol_map);
+ void debugCheckFormals(const std::vector<Expr>& formals, Expr func);
/**
- * Do quantifier elimination.
- *
- * This function takes as input a quantified formula e
- * of the form:
- * Q x1...xn. P( x1...xn, y1...yn )
- * where P( x1...xn, y1...yn ) is a quantifier-free
- * formula in a logic that supports quantifier elimination.
- * Currently, the only logics supported by quantifier
- * elimination is LRA and LIA.
- *
- * This function returns a formula ret such that, given
- * the current set of formulas A asserted to this SmtEngine :
- *
- * If doFull = true, then
- * - ( A ^ e ) and ( A ^ ret ) are equivalent
- * - ret is quantifier-free formula containing
- * only free variables in y1...yn.
- *
- * If doFull = false, then
- * - (A ^ e) => (A ^ ret) if Q is forall or
- * (A ^ ret) => (A ^ e) if Q is exists,
- * - ret is quantifier-free formula containing
- * only free variables in y1...yn,
- * - If Q is exists, let A^Q_n be the formula
- * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
- * where for each i=1,...n, formula ret^Q_i
- * is the result of calling doQuantifierElimination
- * for e with the set of assertions A^Q_{i-1}.
- * Similarly, if Q is forall, then let A^Q_n be
- * A ^ ret^Q_1 ^ ... ^ ret^Q_n
- * where ret^Q_i is the same as above.
- * In either case, we have that ret^Q_j will
- * eventually be true or false, for some finite j.
- *
- * The former feature is quantifier elimination, and
- * is run on invocations of the smt2 extended command get-qe.
- * The latter feature is referred to as partial quantifier
- * elimination, and is run on invocations of the smt2
- * 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.
+ * 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.
*/
- Expr doQuantifierElimination(const Expr& e,
- bool doFull,
- bool strict = true) /* throw(Exception) */;
- /**
- * 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).
- * If this method returns true, then abd is set to a formula C such that
- * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
+ void debugCheckFunctionBody(Expr formula,
+ const std::vector<Expr>& formals,
+ Expr func);
+ /**
+ * Get abduct internal.
*
- * The argument grammarType is a sygus datatype type that encodes the syntax
- * restrictions on the shape of possible solutions.
+ * Get the next abduct from the internal subsolver d_subsolver. If
+ * successful, this method returns true and sets abd to that abduct.
*
- * This method invokes a separate copy of the SMT engine for solving the
- * corresponding sygus problem for generating such a solution.
+ * This method assumes d_subsolver has been initialized to do abduction
+ * problems.
*/
- 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);
+ bool getAbductInternal(Expr& abd);
/**
- * Get list of quantified formulas that were instantiated
+ * 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.
*/
- void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs );
-
+ std::pair<Expr, Expr> getSepHeapAndNilExpr();
+
/**
- * Get instantiations
+ * Get expanded assertions.
+ *
+ * Return the set of assertions, after expanding definitions.
*/
- void getInstantiations( Expr q, std::vector< Expr >& insts );
- void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs );
+ std::vector<Expr> getExpandedAssertions();
- /**
- * 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.
+ /* 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.
*/
- UnsatCore getUnsatCore();
+ std::unique_ptr<SmtEngine> d_subsolver;
/**
- * Get the current set of assertions. Only permitted if the
- * SmtEngine is set to operate interactively.
+ * If applicable, the function-to-synthesize that the subsolver is solving
+ * for. This is used for the get-abduct command.
*/
- std::vector<Expr> getAssertions();
+ Expr d_sssf;
/**
- * Push a user-level context.
+ * The conjecture of the current abduction problem. This expression is only
+ * valid while we are in mode SMT_MODE_ABDUCT.
*/
- void
- push() /* throw(ModalException, LogicException, UnsafeInterruptException) */;
+ 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;
/**
- * Pop a user-level context. Throws an exception if nothing to pop.
+ * The assertion list (before any conversion) for supporting
+ * getAssertions(). Only maintained if in interactive mode.
*/
- void pop();
+ AssertionList* d_assertionList;
/**
- * Completely reset the state of the solver, as though destroyed and
- * recreated. The result is as if newly constructed (so it still
- * retains the same options structure and ExprManager).
+ * 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).
*/
- void reset() /* throw() */;
+ std::vector<Expr> d_assumptions;
/**
- * Reset all assertions, global declarations, etc.
+ * List of items for which to retrieve values using getAssignment().
*/
- void resetAssertions() /* throw() */;
+ AssignmentSet* d_assignments;
/**
- * 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.
+ * 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.
*/
- void interrupt() /* throw(ModalException) */;
+ std::vector<Command*> d_modelGlobalCommands;
/**
- * Set a resource limit for SmtEngine operations. This is like a time
- * limit, but it's deterministic so that reproducible results can be
- * obtained. Currently, it's based on the number of conflicts.
- * However, please note that the definition may change between different
- * versions of CVC4 (as may the number of conflicts required, anyway),
- * and it might even be different between instances of the same version
- * of CVC4 on different platforms.
- *
- * A cumulative and non-cumulative (per-call) resource limit can be
- * set at the same time. A call to setResourceLimit() with
- * cumulative==true replaces any cumulative resource limit currently
- * in effect; a call with cumulative==false replaces any per-call
- * resource limit currently in effect. Time limits can be set in
- * addition to resource limits; the SmtEngine obeys both. That means
- * that up to four independent limits can control the SmtEngine
- * at the same time.
- *
- * When an SmtEngine is first created, it has no time or resource
- * limits.
- *
- * Currently, these limits only cause the SmtEngine to stop what its
- * doing when the limit expires (or very shortly thereafter); no
- * heuristics are altered by the limits or the threat of them expiring.
- * We reserve the right to change this in the future.
- *
- * @param units the resource limit, or 0 for no limit
- * @param cumulative whether this resource limit is to be a cumulative
- * resource limit for all remaining calls into the SmtEngine (true), or
- * whether it's a per-call resource limit (false); the default is false
+ * 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.
*/
- void setResourceLimit(unsigned long units, bool cumulative = false);
+ smt::CommandList* d_modelCommands;
/**
- * Set a time limit for SmtEngine operations.
- *
- * A cumulative and non-cumulative (per-call) time limit can be
- * set at the same time. A call to setTimeLimit() with
- * cumulative==true replaces any cumulative time limit currently
- * in effect; a call with cumulative==false replaces any per-call
- * time limit currently in effect. Resource limits can be set in
- * addition to time limits; the SmtEngine obeys both. That means
- * that up to four independent limits can control the SmtEngine
- * at the same time.
- *
- * Note that the cumulative timer only ticks away when one of the
- * SmtEngine's workhorse functions (things like assertFormula(),
- * query(), checkSat(), and simplify()) are running. Between calls,
- * the timer is still.
- *
- * When an SmtEngine is first created, it has no time or resource
- * limits.
- *
- * Currently, these limits only cause the SmtEngine to stop what its
- * doing when the limit expires (or very shortly thereafter); no
- * heuristics are altered by the limits or the threat of them expiring.
- * We reserve the right to change this in the future.
- *
- * @param millis the time limit in milliseconds, or 0 for no limit
- * @param cumulative whether this time limit is to be a cumulative
- * time limit for all remaining calls into the SmtEngine (true), or
- * whether it's a per-call time limit (false); the default is false
+ * 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.
*/
- void setTimeLimit(unsigned long millis, bool cumulative = false);
+ std::vector<Command*> d_dumpCommands;
/**
- * Get the current resource usage count for this SmtEngine. This
- * function can be used to ascertain reasonable values to pass as
- * resource limits to setResourceLimit().
+ * A vector of command definitions to be imported in the new
+ * SmtEngine when checking unsat-cores.
*/
- unsigned long getResourceUsage() const;
+ std::vector<Command*> d_defineCommands;
/**
- * Get the current millisecond count for this SmtEngine.
+ * The logic we're in.
*/
- unsigned long getTimeUsage() const;
+ LogicInfo d_logic;
/**
- * Get the remaining resources that can be consumed by this SmtEngine
- * according to the currently-set cumulative resource limit. If there
- * is not a cumulative resource limit set, this function throws a
- * ModalException.
+ * Keep a copy of the original option settings (for reset()).
*/
- unsigned long getResourceRemaining() const /* throw(ModalException) */;
+ Options d_originalOptions;
+
+ /** Whether this is an internal subsolver. */
+ bool d_isInternalSubsolver;
/**
- * 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.
+ * Number of internal pops that have been deferred.
*/
- unsigned long getTimeRemaining() const /* throw(ModalException) */;
+ unsigned d_pendingPops;
/**
- * Permit access to the underlying ExprManager.
+ * 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.
*/
- ExprManager* getExprManager() const {
- return d_exprManager;
- }
+ bool d_fullyInited;
/**
- * Export statistics from this SmtEngine.
+ * 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.
*/
- Statistics getStatistics() const /* throw() */;
+ bool d_queryMade;
/**
- * Get the value of one named statistic from this SmtEngine.
+ * Internal status flag to indicate whether we've sent a theory
+ * presolve() notification and need to match it with a postsolve().
*/
- SExpr getStatistic(std::string name) const /* throw() */;
+ bool d_needPostsolve;
- /**
- * Flush statistic from this SmtEngine. Safe to use in a signal handler.
+ /*
+ * Whether to call theory preprocessing during simplification - on
+ * by default* but gets turned off if arithRewriteEq is on
*/
- void safeFlushStatistics(int fd) const;
+ bool d_earlyTheoryPP;
- /**
- * Returns the most recent result of checkSat/query or (set-info :status).
+ /*
+ * Whether we did a global negation of the formula.
*/
- Result getStatusOfLastCommand() const /* throw() */ { return d_status; }
+ bool d_globalNegation;
+
/**
- * Set user attribute.
- * This function is called when an attribute is set by a user.
- * In SMT-LIBv2 this is done via the syntax (! expr :attr)
+ * Most recent result of last checkSat/query or (set-info :status).
*/
- void setUserAttribute(const std::string& attr,
- Expr expr,
- const std::vector<Expr>& expr_values,
- const std::string& str_value);
+ Result d_status;
/**
- * Set print function in model
+ * The expected status of the next satisfiability check.
*/
- void setPrintFuncInModel(Expr f, bool p);
+ Result d_expectedStatus;
+ SmtMode d_smtMode;
- /** Throws a ModalException if the SmtEngine has been fully initialized. */
- void beforeSearch() /* throw(ModalException) */;
+ /**
+ * The input file name (if any) or the name set through setInfo (if any)
+ */
+ std::string d_filename;
- LemmaChannels* channels() { return d_channels; }
+ /**
+ * Verbosity of various commands.
+ */
+ std::map<std::string, Integer> d_commandVerbosity;
+ /** ReplayStream for the solver. */
+ ExprStream* d_replayStream;
/**
- * Expermintal feature: Sets the sequence of decisions.
- * This currently requires very fine grained knowledge about literal
- * translation.
+ * A private utility class to SmtEngine.
*/
- void setReplayStream(ExprStream* exprStream);
+ smt::SmtEnginePrivate* d_private;
- /** 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.
- */
- bool getExpressionName(Expr e, std::string& name) const;
+ StatisticsRegistry* d_statisticsRegistry;
- /** 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.
- */
- void setExpressionName(Expr e, const std::string& name);
+ smt::SmtEngineStatistics* d_stats;
+
+ /** Container for the lemma input and output channels for this SmtEngine.*/
+ LemmaChannels* d_channels;
+}; /* class SmtEngine */
-};/* class SmtEngine */
+/* -------------------------------------------------------------------------- */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff