Model generation for arith, boolean, and uf theories via

(get-value ...) SMT-LIBv2 command.  As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work).  Closes bug #213.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index c33982ddc..7eb903180 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -114,6 +114,14 @@ public:
   Result checkSat();
 
   /**
+   * Get the value of a boolean variable.
+   *
+   * @return mkConst<true>, mkConst<false>, or Node::null() if
+   * unassigned.
+   */
+  Node getValue(TNode node);
+
+  /**
    * Push the context level.
    */
   void push();