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

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