diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 100 |
1 files changed, 32 insertions, 68 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8db8eadd5..f6b1d08bf 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -91,23 +91,25 @@ namespace prop { /* -------------------------------------------------------------------------- */ namespace smt { - /** - * Representation of a defined function. We keep these around in - * SmtEngine to permit expanding definitions late (and lazily), to - * support getValue() over defined functions, to support user output - * in terms of defined functions, etc. - */ - class DefinedFunction; - - struct SmtEngineStatistics; - class SmtEnginePrivate; - class SmtScope; - class ProcessAssertions; - - ProofManager* currentProofManager(); - - struct CommandCleanup; - typedef context::CDList<Command*, CommandCleanup> CommandList; +/** Subsolvers */ +class AbductionSolver; +/** + * Representation of a defined function. We keep these around in + * SmtEngine to permit expanding definitions late (and lazily), to + * support getValue() over defined functions, to support user output + * in terms of defined functions, etc. + */ +class DefinedFunction; + +struct SmtEngineStatistics; +class SmtEnginePrivate; +class SmtScope; +class ProcessAssertions; + +ProofManager* currentProofManager(); + +struct CommandCleanup; +typedef context::CDList<Command*, CommandCleanup> CommandList; }/* CVC4::smt namespace */ /* -------------------------------------------------------------------------- */ @@ -508,7 +510,7 @@ class CVC4_PUBLIC SmtEngine * * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - Expr expandDefinitions(const Expr& e); + Node expandDefinitions(const Node& e); /** * Get the assigned value of an expr (only if immediately preceded by a SAT @@ -660,10 +662,10 @@ class CVC4_PUBLIC SmtEngine * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd); + bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd); /** Same as above, but without user-provided grammar restrictions */ - bool getAbduct(const Expr& conj, Expr& abd); + bool getAbduct(const Node& conj, Node& abd); /** * Get list of quantified formulas that were instantiated on the last call @@ -898,6 +900,13 @@ class CVC4_PUBLIC SmtEngine /** Get the resource manager of this SMT engine */ ResourceManager* getResourceManager(); + + /** + * Get expanded assertions. + * + * Return the set of assertions, after expanding definitions. + */ + std::vector<Expr> getExpandedAssertions(); /* ....................................................................... */ private: /* ....................................................................... */ @@ -994,7 +1003,7 @@ class CVC4_PUBLIC SmtEngine * with the abduct and the goal is UNSAT. If these criteria are not met, an * internal error is thrown. */ - void checkAbduct(Expr a); + void checkAbduct(Node a); /** * Postprocess a value for output to the user. Involves doing things @@ -1111,30 +1120,12 @@ class CVC4_PUBLIC SmtEngine 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 -------------------------------------------------------------- */ /** Solver instance that owns this SmtEngine instance. */ @@ -1171,35 +1162,8 @@ class CVC4_PUBLIC SmtEngine /** 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; + /** The solver for abduction queries */ + std::unique_ptr<smt::AbductionSolver> d_abductSolver; /** * The assertion list (before any conversion) for supporting |