diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
commit | d6b37239a2e525e7878d3bb0b4372a8dabc340a9 (patch) | |
tree | 3db6b54c8b5873db1e6c91b1577d431d74632c66 /src/smt/smt_engine.h | |
parent | 7a059452ebf5729723f610da9258a47007e38253 (diff) |
additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7272762d8..d6940f09f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -26,6 +26,7 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "context/cdmap_forward.h" +#include "context/cdset_forward.h" #include "util/result.h" #include "util/model.h" #include "util/sexpr.h" @@ -88,6 +89,8 @@ class CVC4_PUBLIC SmtEngine { DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList<Expr> AssertionList; + /** The type of our internal assignment set */ + typedef context::CDSet<Node, NodeHashFunction> AssignmentSet; /** Our Context */ context::Context* d_context; @@ -112,6 +115,11 @@ class CVC4_PUBLIC SmtEngine { AssertionList* d_assertionList; /** + * List of items for which to retrieve values using getAssignment(). + */ + AssignmentSet* d_assignments; + + /** * Whether or not we have added any * assertions/declarations/definitions since the last checkSat/query * (and therefore we're not responsible for an assignment). @@ -229,7 +237,18 @@ public: * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. */ - Expr getValue(Expr e) throw(ModalException, AssertionException); + Expr getValue(const Expr& e) throw(ModalException, AssertionException); + + /** + * 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) throw(AssertionException); /** * Get the assignment (only if immediately preceded by a SAT or |