diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
commit | d6b37239a2e525e7878d3bb0b4372a8dabc340a9 (patch) | |
tree | 3db6b54c8b5873db1e6c91b1577d431d74632c66 /src/smt | |
parent | 7a059452ebf5729723f610da9258a47007e38253 (diff) |
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
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 3 | ||||
-rw-r--r-- | src/smt/options.h | 136 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 129 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 21 |
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 |