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

4 files changed, 259 insertions, 30 deletions

diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 319b25576..8878448d5 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -10,4 +10,5 @@ libsmt_la_SOURCES = \
 	smt_engine.h \
 	noninteractive_exception.h \
 	bad_option_exception.h \
-	no_such_function_exception.h
+	no_such_function_exception.h \
+	options.h
diff --git a/src/smt/options.h b/src/smt/options.h
new file mode 100644
index 000000000..7ddaf5d4d
--- /dev/null
+++ b/src/smt/options.h
@@ -0,0 +1,136 @@
+/*********************                                                        */
+/*! \file options.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Global (command-line, set-option, ...) parameters for SMT.
+ **
+ ** Global (command-line, set-option, ...) parameters for SMT.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__OPTIONS_H
+#define __CVC4__OPTIONS_H
+
+#ifdef CVC4_DEBUG
+#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
+#else /* CVC4_DEBUG */
+#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
+#endif /* CVC4_DEBUG */
+
+#include <iostream>
+#include <string>
+
+#include "util/language.h"
+
+namespace CVC4 {
+
+struct CVC4_PUBLIC Options {
+
+  std::string binary_name;
+
+  bool statistics;
+
+  std::ostream *out;
+  std::ostream *err;
+
+  /* -1 means no output */
+  /* 0 is normal (and default) -- warnings only */
+  /* 1 is warnings + notices so the user doesn't get too bored */
+  /* 2 is chatty, giving statistical things etc. */
+  /* with 3, the solver is slowed down by all the scrolling */
+  int verbosity;
+
+  /** The input language */
+  InputLanguage inputLanguage;
+
+  /** Enumeration of UF implementation choices */
+  typedef enum { TIM, MORGAN } UfImplementation;
+
+  /** Which implementation of uninterpreted function theory to use */
+  UfImplementation uf_implementation;
+
+  /** Should we exit after parsing? */
+  bool parseOnly;
+
+  /** Should the parser do semantic checks? */
+  bool semanticChecks;
+
+  /** Should the parser memory-map file input? */
+  bool memoryMap;
+
+  /** Should we strictly enforce the language standard while parsing? */
+  bool strictParsing;
+
+  /** Should we expand function definitions lazily? */
+  bool lazyDefinitionExpansion;
+
+  /** Whether we're in interactive mode or not */
+  bool interactive;
+
+  /**
+   * Whether we're in interactive mode (or not) due to explicit user
+   * setting (if false, we inferred the proper default setting).
+   */
+  bool interactiveSetByUser;
+
+  /** Whether we support SmtEngine::getValue() for this run. */
+  bool produceModels;
+
+  /** Whether we support SmtEngine::getAssignment() for this run. */
+  bool produceAssignments;
+
+  /** Whether we do typechecking at Expr creation time. */
+  bool earlyTypeChecking;
+
+  Options() :
+    binary_name(),
+    statistics(false),
+    out(0),
+    err(0),
+    verbosity(0),
+    inputLanguage(language::input::LANG_AUTO),
+    uf_implementation(MORGAN),
+    parseOnly(false),
+    semanticChecks(true),
+    memoryMap(false),
+    strictParsing(false),
+    lazyDefinitionExpansion(false),
+    interactive(false),
+    interactiveSetByUser(false),
+    produceModels(false),
+    produceAssignments(false),
+    earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
+  }
+};/* struct Options */
+
+inline std::ostream& operator<<(std::ostream& out,
+                                Options::UfImplementation uf) {
+  switch(uf) {
+  case Options::TIM:
+    out << "TIM";
+    break;
+  case Options::MORGAN:
+    out << "MORGAN";
+    break;
+  default:
+    out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
+#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
+
+#endif /* __CVC4__OPTIONS_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index edf49c7ac..3d6f304b5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -18,6 +18,7 @@
 
 #include <vector>
 #include <string>
+#include <sstream>
 
 #include "smt/smt_engine.h"
 #include "smt/modal_exception.h"
@@ -30,7 +31,7 @@
 #include "expr/node_builder.h"
 #include "util/output.h"
 #include "util/exception.h"
-#include "util/options.h"
+#include "smt/options.h"
 #include "util/configuration.h"
 #include "prop/prop_engine.h"
 #include "theory/theory_engine.h"
@@ -120,7 +121,9 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
   d_decisionEngine(NULL),
   d_theoryEngine(NULL),
   d_propEngine(NULL),
+  d_definedFunctions(NULL),
   d_assertionList(NULL),
+  d_assignments(NULL),
   d_haveAdditions(false),
   d_status() {
 
@@ -152,6 +155,10 @@ SmtEngine::~SmtEngine() {
 
   shutdown();
 
+  if(d_assignments != NULL) {
+    d_assignments->deleteSelf();
+  }
+
   if(d_assertionList != NULL) {
     d_assertionList->deleteSelf();
   }
@@ -183,15 +190,7 @@ void SmtEngine::setInfo(const string& key, const SExpr& value)
       throw BadOptionException("argument to (set-info :status ..) must be "
                                "`sat' or `unsat' or `unknown'");
     }
-    if(s == "sat") {
-      d_status = Result::SAT;
-    } else if(s == "unsat") {
-      d_status = Result::UNSAT;
-    } else if(s == "unknown") {
-      d_status = Result::SAT_UNKNOWN;
-    } else {
-      Unreachable();
-    }
+    d_status = Result(s);
     return;
   }
   throw BadOptionException();
@@ -220,19 +219,16 @@ SExpr SmtEngine::getInfo(const string& key) const
   } else if(key == ":authors") {
     return Configuration::about();
   } else if(key == ":status") {
-    enum Result::SAT status = d_status.asSatisfiabilityResult().isSAT();
-    switch(status) {
-    case Result::SAT:
-      return SExpr("sat");
-    case Result::UNSAT:
-      return SExpr("unsat");
-    case Result::SAT_UNKNOWN:
-      return SExpr("unknown");
-    default:
-      Unhandled(status);
-    }
+    return d_status.asSatisfiabilityResult().toString();
   } else if(key == ":reason-unknown") {
-    throw BadOptionException();
+    if(d_status.isUnknown()) {
+      stringstream ss;
+      ss << d_status.whyUnknown();
+      return ss.str();
+    } else {
+      throw ModalException("Can't get-info :reason-unknown when the "
+                           "last result wasn't unknown!");
+    }
   } else {
     throw BadOptionException();
   }
@@ -241,8 +237,31 @@ SExpr SmtEngine::getInfo(const string& key) const
 void SmtEngine::setOption(const string& key, const SExpr& value)
   throw(BadOptionException) {
   Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
-  // FIXME implement me
-  throw BadOptionException();
+  if(key == ":print-success") {
+    throw BadOptionException();
+  } else if(key == ":expand-definitions") {
+    throw BadOptionException();
+  } else if(key == ":interactive-mode") {
+    throw BadOptionException();
+  } else if(key == ":produce-proofs") {
+    throw BadOptionException();
+  } else if(key == ":produce-unsat-cores") {
+    throw BadOptionException();
+  } else if(key == ":produce-models") {
+    throw BadOptionException();
+  } else if(key == ":produce-assignments") {
+    throw BadOptionException();
+  } else if(key == ":regular-output-channel") {
+    throw BadOptionException();
+  } else if(key == ":diagnostic-output-channel") {
+    throw BadOptionException();
+  } else if(key == ":random-seed") {
+    throw BadOptionException();
+  } else if(key == ":verbosity") {
+    throw BadOptionException();
+  } else {
+    throw BadOptionException();
+  }
 }
 
 SExpr SmtEngine::getOption(const string& key) const
@@ -386,7 +405,7 @@ Result SmtEngine::check() {
 
 Result SmtEngine::quickCheck() {
   Debug("smt") << "SMT quickCheck()" << endl;
-  return Result(Result::VALIDITY_UNKNOWN);
+  return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK);
 }
 
 void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
@@ -454,7 +473,7 @@ Expr SmtEngine::simplify(const Expr& e) {
   Unimplemented();
 }
 
-Expr SmtEngine::getValue(Expr e)
+Expr SmtEngine::getValue(const Expr& e)
   throw(ModalException, AssertionException) {
   Assert(e.getExprManager() == d_exprManager);
   Type type = e.getType(true);// ensure expr is type-checked at this point
@@ -494,19 +513,73 @@ Expr SmtEngine::getValue(Expr e)
   return Expr(d_exprManager, new Node(resultNode));
 }
 
+bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Type type = e.getType(true);
+  // must be Boolean
+  CheckArgument( type.isBoolean(), e,
+                 "expected Boolean-typed variable or function application "
+                 "in addToAssignment()" );
+  Node n = e.getNode();
+  // must be an APPLY of a zero-ary defined function, or a variable
+  CheckArgument( ( ( n.getKind() == kind::APPLY &&
+                     ( d_definedFunctions->find(n.getOperator()) !=
+                       d_definedFunctions->end() ) &&
+                     n.getNumChildren() == 0 ) ||
+                   n.getMetaKind() == kind::metakind::VARIABLE ), e,
+                 "expected variable or defined-function application "
+                 "in addToAssignment(),\ngot %s", e.toString().c_str() );
+  if(!d_options->interactive || !d_options->produceAssignments) {
+    return false;
+  }
+  if(d_assignments == NULL) {
+    d_assignments = new(true) AssignmentSet(d_context);
+  }
+  d_assignments->insert(n);
+
+  return true;
+}
+
 SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Debug("smt") << "SMT getAssignment()" << endl;
   if(!d_options->produceAssignments) {
     const char* msg =
-      "Cannot get the current assignment when produce-assignments option is off.";
+      "Cannot get the current assignment when "
+      "produce-assignments option is off.";
     throw ModalException(msg);
   }
   // TODO also check that the last query was sat/unknown, without intervening
   // assertions
 
   NodeManagerScope nms(d_nodeManager);
+  vector<SExpr> sexprs;
+  TypeNode boolType = d_nodeManager->booleanType();
+  for(AssignmentSet::const_iterator i = d_assignments->begin(),
+        iend = d_assignments->end();
+      i != iend;
+      ++i) {
+    Assert((*i).getType() == boolType);
 
-  Unimplemented();
+    Node n = SmtEnginePrivate::preprocess(*this, *i);
+
+    Debug("smt") << "--- getting value of " << n << endl;
+    Node resultNode = d_theoryEngine->getValue(n);
+
+    // type-check the result we got
+    Assert(resultNode.isNull() || resultNode.getType(true) == boolType);
+
+    vector<SExpr> v;
+    if((*i).getKind() == kind::APPLY) {
+      Assert((*i).getNumChildren() == 0);
+      v.push_back((*i).getOperator().toString());
+    } else {
+      Assert((*i).getMetaKind() == kind::metakind::VARIABLE);
+      v.push_back((*i).toString());
+    }
+    v.push_back(resultNode.toString());
+    sexprs.push_back(v);
+  }
+  return SExpr(sexprs);
 }
 
 vector<Expr> SmtEngine::getAssertions()
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