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

diff --git a/src/expr/command.h b/src/expr/command.h
index 4c74cfd6c..172ddea86 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -122,6 +122,20 @@ public:
   void toStream(std::ostream& out) const;
 };/* class DefineFunctionCommand */
 
+/**
+ * This differs from DefineFunctionCommand only in that it instructs
+ * the SmtEngine to "remember" this function for later retrieval with
+ * getAssignment().  Used for :named attributes in SMT-LIBv2.
+ */
+class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
+public:
+  DefineNamedFunctionCommand(Expr func,
+                             const std::vector<Expr>& formals,
+                             Expr formula);
+  void invoke(SmtEngine* smtEngine);
+  void toStream(std::ostream& out) const;
+};/* class DefineNamedFunctionCommand */
+
 class CVC4_PUBLIC CheckSatCommand : public Command {
 protected:
   BoolExpr d_expr;
@@ -158,6 +172,17 @@ public:
   void toStream(std::ostream& out) const;
 };/* class GetValueCommand */
 
+class CVC4_PUBLIC GetAssignmentCommand : public Command {
+protected:
+  SExpr d_result;
+public:
+  GetAssignmentCommand();
+  void invoke(SmtEngine* smtEngine);
+  SExpr getResult() const;
+  void printResult(std::ostream& out) const;
+  void toStream(std::ostream& out) const;
+};/* class GetAssignmentCommand */
+
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 protected:
   std::string d_result;