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, 15 insertions, 0 deletions

diff --git a/src/util/result.h b/src/util/result.h
index ccc36973d..f1f6ae1c2 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -86,6 +86,21 @@ public:
   }
   enum UnknownExplanation whyUnknown();
 
+  inline bool operator==(Result r) {
+    if(d_which != r.d_which) {
+      return false;
+    }
+    if(d_which == TYPE_SAT) {
+      return d_sat == r.d_sat;
+    }
+    if(d_which == TYPE_VALIDITY) {
+      return d_validity == r.d_validity;
+    }
+    return false;
+  }
+  inline bool operator!=(Result r) {
+    return !(*this == r);
+  }
   inline Result asSatisfiabilityResult() const;
   inline Result asValidityResult() const;