diff options
97 files changed, 762 insertions, 353 deletions
diff --git a/configure.ac b/configure.ac index ced90d56f..de6b3a427 100644 --- a/configure.ac +++ b/configure.ac @@ -67,7 +67,7 @@ if test -z "${CFLAGS+set}"; then CFLAGS=; fi if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi # on by default -AM_MAINTAINER_MODE +AM_MAINTAINER_MODE([enable]) # turn off static lib building by default AC_ENABLE_SHARED diff --git a/src/context/cdset.h b/src/context/cdset.h index 47848c26f..268c3127b 100644 --- a/src/context/cdset.h +++ b/src/context/cdset.h @@ -22,6 +22,7 @@ #define __CVC4__CONTEXT__CDSET_H #include "context/context.h" +#include "context/cdset_forward.h" #include "context/cdmap.h" #include "util/Assert.h" diff --git a/src/context/cdset_forward.h b/src/context/cdset_forward.h new file mode 100644 index 000000000..135db8751 --- /dev/null +++ b/src/context/cdset_forward.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file cdset_forward.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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 This is a forward declaration header to declare the CDSet<> + ** template + ** + ** This is a forward declaration header to declare the CDSet<> + ** template. It's useful if you want to forward-declare CDSet<> + ** without including the full cdset.h header, for example, in a + ** public header context. + ** + ** For CDSet<> in particular, it's difficult to forward-declare it + ** yourself, becase it has a default template argument. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CONTEXT__CDSET_FORWARD_H +#define __CVC4__CONTEXT__CDSET_FORWARD_H + +namespace __gnu_cxx { + template <class Key> class hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template <class V, class HashFcn = __gnu_cxx::hash<V> > + class CDSet; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDSET_FORWARD_H */ diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 15fea22da..38193a75b 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -240,6 +240,28 @@ void DefineFunctionCommand::toStream(std::ostream& out) const { out << "], << " << d_formula << " >> )"; } +/* class DefineFunctionCommand */ + +DefineNamedFunctionCommand::DefineNamedFunctionCommand(Expr func, + const std::vector<Expr>& formals, + Expr formula) : + DefineFunctionCommand(func, formals, formula) { +} + +void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) { + this->DefineFunctionCommand::invoke(smtEngine); + if(d_func.getType().isBoolean()) { + smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, + d_func)); + } +} + +void DefineNamedFunctionCommand::toStream(std::ostream& out) const { + out << "DefineNamedFunction( "; + this->DefineFunctionCommand::toStream(out); + out << " )"; +} + /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) : @@ -262,6 +284,27 @@ void GetValueCommand::toStream(std::ostream& out) const { out << "GetValue( << " << d_term << " >> )"; } +/* class GetAssignmentCommand */ + +GetAssignmentCommand::GetAssignmentCommand() { +} + +void GetAssignmentCommand::invoke(SmtEngine* smtEngine) { + d_result = smtEngine->getAssignment(); +} + +SExpr GetAssignmentCommand::getResult() const { + return d_result; +} + +void GetAssignmentCommand::printResult(std::ostream& out) const { + out << d_result << endl; +} + +void GetAssignmentCommand::toStream(std::ostream& out) const { + out << "GetAssignment()"; +} + /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() { 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; diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 8faaefac4..57aa84a57 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -29,7 +29,7 @@ #include "util/exception.h" #include "util/configuration.h" #include "util/output.h" -#include "util/options.h" +#include "smt/options.h" #include "util/language.h" #include "expr/expr.h" diff --git a/src/main/main.cpp b/src/main/main.cpp index 7fd866112..f78637d82 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -33,7 +33,7 @@ #include "util/Assert.h" #include "util/configuration.h" #include "util/output.h" -#include "util/options.h" +#include "smt/options.h" #include "util/result.h" #include "util/stats.h" @@ -42,8 +42,6 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -static Result lastResult; - namespace CVC4 { namespace main { struct Options options; @@ -203,20 +201,15 @@ int runCvc4(int argc, char* argv[]) { delete cmd; } - Result asSatResult = lastResult.asSatisfiabilityResult(); + string result = smt.getInfo(":status").getValue(); int returnValue; - switch(asSatResult.isSAT()) { - - case Result::SAT: + if(result == "sat") { returnValue = 10; - break; - case Result::UNSAT: + } else if(result == "unsat") { returnValue = 20; - break; - default: + } else { returnValue = 0; - break; } #ifdef CVC4_COMPETITION_MODE @@ -228,7 +221,7 @@ int runCvc4(int argc, char* argv[]) { // Remove the parser delete parser; - ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult); + ReferenceStat< Result > s_statSatResult("sat/unsat", result); StatisticsRegistry::registerStat(&s_statSatResult); if(options.statistics){ @@ -259,15 +252,5 @@ void doCommand(SmtEngine& smt, Command* cmd) { } else { cmd->invoke(&smt); } - - QueryCommand *qc = dynamic_cast<QueryCommand*>(cmd); - if(qc != NULL) { - lastResult = qc->getResult(); - } else { - CheckSatCommand *csc = dynamic_cast<CheckSatCommand*>(cmd); - if(csc != NULL) { - lastResult = csc->getResult(); - } - } } } diff --git a/src/main/util.cpp b/src/main/util.cpp index 760bd5258..70cb85c93 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -24,7 +24,7 @@ #include <signal.h> #include "util/exception.h" -#include "util/options.h" +#include "smt/options.h" #include "util/Assert.h" #include "util/stats.h" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ddfd1804e..f549d2148 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -248,6 +248,9 @@ command returns [CVC4::Command* cmd] $cmd = seq; } } + | /* get-assignment */ + GET_ASSIGNMENT_TOK + { cmd = new GetAssignmentCommand; } | /* assertion */ ASSERT_TOK term[expr] { cmd = new AssertCommand(expr); } @@ -400,7 +403,7 @@ term[CVC4::Expr& expr] Expr func = PARSER_STATE->mkFunction(name, expr.getType()); // bind name to expr with define-fun Command* c = - new DefineFunctionCommand(func, std::vector<Expr>(), expr); + new DefineNamedFunctionCommand(func, std::vector<Expr>(), expr); PARSER_STATE->preemptCommand(c); } else { std::stringstream ss; @@ -585,6 +588,7 @@ DECLARE_SORT_TOK : 'declare-sort'; DEFINE_FUN_TOK : 'define-fun'; DEFINE_SORT_TOK : 'define-sort'; GET_VALUE_TOK : 'get-value'; +GET_ASSIGNMENT_TOK : 'get-assignment'; GET_ASSERTIONS_TOK : 'get-assertions'; EXIT_TOK : 'exit'; ITE_TOK : 'ite'; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 961a18bdb..de60b5f7d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -24,7 +24,7 @@ #include "util/decision_engine.h" #include "util/Assert.h" #include "util/output.h" -#include "util/options.h" +#include "smt/options.h" #include "util/result.h" #include <utility> @@ -93,9 +93,11 @@ void PropEngine::assertLemma(TNode node) { void PropEngine::printSatisfyingAssignment(){ - const CnfStream::TranslationCache& transCache = d_cnfStream->getTranslationCache(); + const CnfStream::TranslationCache& transCache = + d_cnfStream->getTranslationCache(); Debug("prop-value") << "Literal | Value | Expr" << endl - << "---------------------------------------------------------" << endl; + << "----------------------------------------" + << "-----------------" << endl; for(CnfStream::TranslationCache::const_iterator i = transCache.begin(), end = transCache.end(); i != end; @@ -105,8 +107,7 @@ void PropEngine::printSatisfyingAssignment(){ if(!sign(l)) { Node n = curr.first; SatLiteralValue value = d_satSolver->value(l); - Debug("prop-value") << /*setw(4) << */ "'" << l << "' " /*<< setw(4)*/ << value << " " << n - << endl; + Debug("prop-value") << "'" << l << "' " << value << " " << n << endl; } } } @@ -126,7 +127,8 @@ Result PropEngine::checkSat() { printSatisfyingAssignment(); } - Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl; + Debug("prop") << "PropEngine::checkSat() => " + << (result ? "true" : "false") << endl; return Result(result ? Result::SAT : Result::UNSAT); } @@ -154,5 +156,5 @@ void PropEngine::pop() { Debug("prop") << "pop()" << endl; } -}/* prop namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 7eb903180..1dada2e69 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,12 +25,12 @@ #include "expr/node.h" #include "util/result.h" -#include "util/options.h" #include "util/decision_engine.h" namespace CVC4 { class TheoryEngine; +class Options; namespace prop { @@ -133,7 +133,7 @@ public: };/* class PropEngine */ -}/* prop namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* __CVC4__PROP_ENGINE_H */ diff --git a/src/prop/sat.h b/src/prop/sat.h index 776895b4c..a335b733b 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -25,9 +25,9 @@ // Optional blocks below will be unconditionally included #define __CVC4_USE_MINISAT -#include "util/options.h" #include "util/stats.h" #include "theory/theory.h" +#include "smt/options.h" #ifdef __CVC4_USE_MINISAT 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/util/options.h b/src/smt/options.h index af254dabf..7ddaf5d4d 100644 --- a/src/util/options.h +++ b/src/smt/options.h @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Global (command-line or equivalent) tuning parameters. + ** \brief Global (command-line, set-option, ...) parameters for SMT. ** - ** Global (command-line or equivalent) tuning parameters. + ** Global (command-line, set-option, ...) parameters for SMT. **/ #include "cvc4_public.h" @@ -89,7 +89,7 @@ struct CVC4_PUBLIC Options { /** Whether we support SmtEngine::getAssignment() for this run. */ bool produceAssignments; - /** Whether we support SmtEngine::getAssignment() for this run. */ + /** Whether we do typechecking at Expr creation time. */ bool earlyTypeChecking; Options() : 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 diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h index 0b21eedae..181508c54 100644 --- a/src/theory/shared_data.h +++ b/src/theory/shared_data.h @@ -51,8 +51,8 @@ namespace theory { class SharedData : public context::ContextObj { private: /** - * Bit-vector representation of list of theories needing to be notified if - * this shared term is no longer the representative + * Bit-vector representation of list of theories needing to be + * notified if this shared term is no longer the representative */ uint64_t d_theories; @@ -72,25 +72,29 @@ private: SharedData* d_proofNext; /** - * In order to precisely reconstruct the equality that justifies this node - * being equal to the node at d_proofNext, we need to know whether this edge - * has been switched. Value is meaningless at the proof root. + * In order to precisely reconstruct the equality that justifies + * this node being equal to the node at d_proofNext, we need to know + * whether this edge has been switched. Value is meaningless at the + * proof root. */ bool d_edgeReversed; /** - * The theory that can explain the equality of this node and the node at - * d_proofNext. Not valid if this is proof root. + * The theory that can explain the equality of this node and the + * node at d_proofNext. Not valid if this is proof root. */ theory::Theory* d_explainingTheory; /** - * This is a pointer back to the node associated with this SharedData object. + * This is a pointer back to the node associated with this + * SharedData object. * * The following invariant should be maintained: - * (n.getAttribute(SharedAttr()))->d_rep == n - * i.e. rep is equal to the node that maps to the SharedData using SharedAttr. * + * (n.getAttribute(SharedAttr()))->d_rep == n + * + * i.e. rep is equal to the node that maps to the SharedData using + * SharedAttr. */ TNode d_rep; @@ -133,8 +137,8 @@ public: void setSize(unsigned size) { makeCurrent(); d_size = size; } /** - * Returns the find pointer of the SharedData. - * If this is the representative of the equivalence class, then getFind() == this + * Returns the find pointer of the SharedData. If this is the + * representative of the equivalence class, then getFind() == this */ SharedData* getFind() const { return d_find; } @@ -169,13 +173,15 @@ public: void setEdgeReversed(bool value) { makeCurrent(); d_edgeReversed = value; } /** - * Get the original equality that created the link from this node to the next - * proof node. + * Get the original equality that created the link from this node to + * the next proof node. */ Node getEquality() const { return d_edgeReversed - ? NodeManager::currentNM()->mkNode(kind::EQUAL, d_proofNext->getRep(), d_rep) - : NodeManager::currentNM()->mkNode(kind::EQUAL, d_rep, d_proofNext->getRep()); + ? NodeManager::currentNM()->mkNode(kind::EQUAL, + d_proofNext->getRep(), d_rep) + : NodeManager::currentNM()->mkNode(kind::EQUAL, + d_rep, d_proofNext->getRep()); } /** @@ -186,7 +192,10 @@ public: /** * Set the explaining theory */ - void setExplainingTheory(theory::Theory* t) { makeCurrent(); d_explainingTheory = t; } + void setExplainingTheory(theory::Theory* t) { + makeCurrent(); + d_explainingTheory = t; + } /** * Get the shared term associated with this data diff --git a/src/theory/shared_term_manager.h b/src/theory/shared_term_manager.h index 49bd447d7..7263ac93a 100644 --- a/src/theory/shared_term_manager.h +++ b/src/theory/shared_term_manager.h @@ -21,6 +21,9 @@ #ifndef __CVC4__SHARED_TERM_MANAGER_H #define __CVC4__SHARED_TERM_MANAGER_H +#include <set> +#include <vector> + #include "expr/node.h" #include "theory/shared_data.h" @@ -50,18 +53,20 @@ class SharedTermManager { context::Context* d_context; /** - * List of all theories indexed by theory id (built by calls to registerTheory) + * List of all theories indexed by theory id (built by calls to + * registerTheory()) */ std::vector<theory::Theory*> d_theories; /** - * Private method to find equivalence class representative in union-find data - * structure. + * Private method to find equivalence class representative in + * union-find data structure. */ SharedData* find(SharedData* pData) const; /** - * Helper function for explain: add all reasons for equality at pData to set s + * Helper function for explain: add all reasons for equality at + * pData to set s */ void collectExplanations(SharedData* pData, std::set<Node>& s) const; @@ -77,27 +82,30 @@ public: void registerTheory(theory::Theory* th); /** - * Called by theory engine to indicate that node n is shared by theories - * parent and child. + * Called by theory engine to indicate that node n is shared by + * theories parent and child. */ void addTerm(TNode n, theory::Theory* parent, theory::Theory* child); /** - * Called by theory engine or theories to notify the shared term manager that - * two terms are equal. + * Called by theory engine or theories to notify the shared term + * manager that two terms are equal. * * @param eq the equality between shared terms - * @param thReason the theory that knows why, NULL means it's a SAT assertion + * @param thReason the theory that knows why, NULL means it's a SAT + * assertion */ void addEq(TNode eq, theory::Theory* thReason = NULL); /** - * Called by theory engine or theories to notify the shared term manager that - * two terms are disequal. + * Called by theory engine or theories to notify the shared term + * manager that two terms are disequal. * - * @param eq the equality between shared terms whose negation now holds - * @param thReason the theory that knows why, NULL means it's a SAT assertion + * @param eq the equality between shared terms whose negation now + * holds + * @param thReason the theory that knows why, NULL means it's a SAT + * assertion */ void addDiseq(TNode eq, theory::Theory* thReason = NULL) { } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 388167e00..384e2fdd6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -21,6 +21,7 @@ #include "expr/attribute.h" #include "theory/theory.h" #include "expr/node_builder.h" +#include "smt/options.h" #include <vector> #include <list> @@ -116,6 +117,57 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { } } +TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) : + d_propEngine(NULL), + d_theoryOut(this, ctxt), + d_hasShutDown(false), + d_statistics() { + + d_sharedTermManager = new SharedTermManager(this, ctxt); + + d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut); + d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut); + switch(opts->uf_implementation) { + case Options::TIM: + d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut); + break; + case Options::MORGAN: + d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut); + break; + default: + Unhandled(opts->uf_implementation); + } + d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut); + d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); + d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut); + + d_sharedTermManager->registerTheory(d_builtin); + d_sharedTermManager->registerTheory(d_bool); + d_sharedTermManager->registerTheory(d_uf); + d_sharedTermManager->registerTheory(d_arith); + d_sharedTermManager->registerTheory(d_arrays); + d_sharedTermManager->registerTheory(d_bv); + + d_theoryOfTable.registerTheory(d_builtin); + d_theoryOfTable.registerTheory(d_bool); + d_theoryOfTable.registerTheory(d_uf); + d_theoryOfTable.registerTheory(d_arith); + d_theoryOfTable.registerTheory(d_arrays); + d_theoryOfTable.registerTheory(d_bv); +} + +TheoryEngine::~TheoryEngine() { + Assert(d_hasShutDown); + + delete d_bv; + delete d_arrays; + delete d_arith; + delete d_uf; + delete d_bool; + delete d_builtin; + + delete d_sharedTermManager; +} Theory* TheoryEngine::theoryOf(TypeNode t) { // FIXME: we don't yet have a Type-to-Theory map. When we do, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0eaf61055..2d056af28 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -36,7 +36,6 @@ #include "theory/arrays/theory_arrays.h" #include "theory/bv/theory_bv.h" -#include "util/options.h" #include "util/stats.h" namespace CVC4 { @@ -202,57 +201,12 @@ public: /** * Construct a theory engine. */ - TheoryEngine(context::Context* ctxt, const Options* opts) : - d_propEngine(NULL), - d_theoryOut(this, ctxt), - d_hasShutDown(false), - d_statistics() { - - d_sharedTermManager = new SharedTermManager(this, ctxt); - - d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut); - d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut); - switch(opts->uf_implementation) { - case Options::TIM: - d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut); - break; - case Options::MORGAN: - d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut); - break; - default: - Unhandled(opts->uf_implementation); - } - d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut); - d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); - d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut); - - d_sharedTermManager->registerTheory(d_builtin); - d_sharedTermManager->registerTheory(d_bool); - d_sharedTermManager->registerTheory(d_uf); - d_sharedTermManager->registerTheory(d_arith); - d_sharedTermManager->registerTheory(d_arrays); - d_sharedTermManager->registerTheory(d_bv); - - d_theoryOfTable.registerTheory(d_builtin); - d_theoryOfTable.registerTheory(d_bool); - d_theoryOfTable.registerTheory(d_uf); - d_theoryOfTable.registerTheory(d_arith); - d_theoryOfTable.registerTheory(d_arrays); - d_theoryOfTable.registerTheory(d_bv); - } - - ~TheoryEngine() { - Assert(d_hasShutDown); - - delete d_bv; - delete d_arrays; - delete d_arith; - delete d_uf; - delete d_bool; - delete d_builtin; + TheoryEngine(context::Context* ctxt, const Options* opts); - delete d_sharedTermManager; - } + /** + * Destroy a theory engine. + */ + ~TheoryEngine(); SharedTermManager* getSharedTermManager() { return d_sharedTermManager; diff --git a/src/util/Assert.h b/src/util/Assert.h index dbbdfe9b7..5bb2e830f 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -163,7 +163,7 @@ public: va_list args; va_start(args, fmt); construct("Illegal argument detected", - ( std::string(argDesc) + " invalid" ).c_str(), + ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), function, file, line, fmt, args); va_end(args); } @@ -172,7 +172,7 @@ public: const char* file, unsigned line) : AssertionException() { construct("Illegal argument detected", - ( std::string(argDesc) + " invalid" ).c_str(), + ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), function, file, line); } @@ -183,7 +183,7 @@ public: va_list args; va_start(args, fmt); construct("Illegal argument detected", - ( std::string(argDesc) + " invalid; expected " + + ( std::string("`") + argDesc + "' is a bad argument; expected " + condStr + " to hold" ).c_str(), function, file, line, fmt, args); va_end(args); @@ -194,7 +194,7 @@ public: unsigned line) : AssertionException() { construct("Illegal argument detected", - ( std::string(argDesc) + " invalid; expected " + + ( std::string("`") + argDesc + "' is a bad argument; expected " + condStr + " to hold" ).c_str(), function, file, line); } diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 02315143d..61c0bf885 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -18,10 +18,10 @@ libutil_la_SOURCES = \ hash.h \ bool.h \ model.h \ - options.h \ output.cpp \ output.h \ result.h \ + result.cpp \ unique_id.h \ configuration.h \ configuration_private.h \ diff --git a/src/util/result.cpp b/src/util/result.cpp new file mode 100644 index 000000000..b8f34f47f --- /dev/null +++ b/src/util/result.cpp @@ -0,0 +1,210 @@ +/********************* */ +/*! \file result.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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 Encapsulation of the result of a query. + ** + ** Encapsulation of the result of a query. + **/ + +#include <iostream> +#include <algorithm> +#include <string> +#include <cctype> + +#include "util/result.h" +#include "util/Assert.h" + +using namespace std; + +namespace CVC4 { + +Result::Result(const string& instr) : + d_sat(SAT_UNKNOWN), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON) { + string s = instr; + transform(s.begin(), s.end(), s.begin(), ::tolower); + if(s == "sat" || s == "satisfiable") { + d_which = TYPE_SAT; + d_sat = SAT; + } else if(s == "unsat" || s == "unsatisfiable") { + d_which = TYPE_SAT; + d_sat = UNSAT; + } else if(s == "valid") { + d_which = TYPE_VALIDITY; + d_validity = VALID; + } else if(s == "invalid") { + d_which = TYPE_VALIDITY; + d_validity = INVALID; + } else if(s == "unknown") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + } else if(s == "incomplete") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = INCOMPLETE; + } else if(s == "timeout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = TIMEOUT; + } else if(s == "memout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = MEMOUT; + } else { + IllegalArgument(s, "expected satisfiability/validity result, " + "instead got `%s'", s.c_str()); + } +} + +bool Result::operator==(const Result& r) const { + if(d_which != r.d_which) { + return false; + } + if(d_which == TYPE_SAT) { + return d_sat == r.d_sat && + ( d_sat != SAT_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation ); + } + if(d_which == TYPE_VALIDITY) { + return d_validity == r.d_validity && + ( d_validity != VALIDITY_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation ); + } + return false; +} + +Result Result::asSatisfiabilityResult() const { + if(d_which == TYPE_SAT) { + return *this; + } + + Assert(d_which == TYPE_VALIDITY); + + switch(d_validity) { + + case INVALID: + return Result(SAT); + + case VALID: + return Result(UNSAT); + + case VALIDITY_UNKNOWN: + return Result(SAT_UNKNOWN, d_unknownExplanation); + + default: + Unhandled(d_validity); + } +} + +Result Result::asValidityResult() const { + if(d_which == TYPE_VALIDITY) { + return *this; + } + + Assert(d_which == TYPE_SAT); + + switch(d_sat) { + + case SAT: + return Result(INVALID); + + case UNSAT: + return Result(VALID); + + case SAT_UNKNOWN: + return Result(VALIDITY_UNKNOWN, d_unknownExplanation); + + default: + Unhandled(d_sat); + } +} + +string Result::toString() const { + stringstream ss; + ss << *this; + return ss.str(); +} + +ostream& operator<<(ostream& out, enum Result::Sat s) { + switch(s) { + case Result::UNSAT: out << "UNSAT"; break; + case Result::SAT: out << "SAT"; break; + case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; + default: Unhandled(s); + } + return out; +} + +ostream& operator<<(ostream& out, enum Result::Validity v) { + switch(v) { + case Result::INVALID: out << "INVALID"; break; + case Result::VALID: out << "VALID"; break; + case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; + default: Unhandled(v); + } + return out; +} + +ostream& operator<<(ostream& out, + enum Result::UnknownExplanation e) { + switch(e) { + case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break; + case Result::INCOMPLETE: out << "INCOMPLETE"; break; + case Result::TIMEOUT: out << "TIMEOUT"; break; + case Result::MEMOUT: out << "MEMOUT"; break; + case Result::OTHER: out << "OTHER"; break; + case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; + default: Unhandled(e); + } + return out; +} + +ostream& operator<<(ostream& out, const Result& r) { + if(r.d_which == Result::TYPE_SAT) { + switch(r.d_sat) { + case Result::UNSAT: + out << "unsat"; + break; + case Result::SAT: + out << "sat"; + break; + case Result::SAT_UNKNOWN: + out << "unknown"; + if(r.whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << r.whyUnknown() << ")"; + } + break; + } + } else { + switch(r.d_validity) { + case Result::INVALID: + out << "invalid"; + break; + case Result::VALID: + out << "valid"; + break; + case Result::VALIDITY_UNKNOWN: + out << "unknown"; + if(r.whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << r.whyUnknown() << ")"; + } + break; + } + } + + return out; +}/* operator<<(ostream&, const Result&) */ + +}/* CVC4 namespace */ diff --git a/src/util/result.h b/src/util/result.h index f1f6ae1c2..fc2fa4522 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -21,20 +21,29 @@ #ifndef __CVC4__RESULT_H #define __CVC4__RESULT_H +#include <iostream> +#include <string> + +#include "util/Assert.h" + namespace CVC4 { -// TODO: perhaps best to templatize Result on its Kind (SAT/Validity), -// but this requires doing the same for Prover and needs discussion. +// TODO: either templatize Result on its Kind (Sat/Validity) or subclass. +// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back +// into the SmtEngine that produced the Result? +// TODO: make unconstructible except by SmtEngine? That would ensure that +// any Result in the system is bona fide. -// TODO: subclass to provide models, etc. This is really just -// intended as a three-valued response code. +class Result; + +std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; /** - * Three-valued, immutable SMT result, with optional explanation. + * Three-valued SMT result, with optional explanation. */ class CVC4_PUBLIC Result { public: - enum SAT { + enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 @@ -50,121 +59,95 @@ public: REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT, - BAIL, - OTHER + MEMOUT, + OTHER, + UNKNOWN_REASON }; private: - enum SAT d_sat; + enum Sat d_sat; enum Validity d_validity; enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which; + enum UnknownExplanation d_unknownExplanation; - friend std::ostream& CVC4::operator<<(std::ostream& out, Result r); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Result& r); public: Result() : d_sat(SAT_UNKNOWN), d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_NONE) { + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON) { } - Result(enum SAT s) : + Result(enum Sat s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_SAT) { + d_which(TYPE_SAT), + d_unknownExplanation(UNKNOWN_REASON) { + CheckArgument(s != SAT_UNKNOWN, + "Must provide a reason for satisfiability being unknown"); } Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), - d_which(TYPE_VALIDITY) { + d_which(TYPE_VALIDITY), + d_unknownExplanation(UNKNOWN_REASON) { + CheckArgument(v != VALIDITY_UNKNOWN, + "Must provide a reason for validity being unknown"); + } + Result(enum Sat s, enum UnknownExplanation unknownExplanation) : + d_sat(s), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_SAT), + d_unknownExplanation(unknownExplanation) { + CheckArgument(s == SAT_UNKNOWN, + "improper use of unknown-result constructor"); + } + Result(enum Validity v, enum UnknownExplanation unknownExplanation) : + d_sat(SAT_UNKNOWN), + d_validity(v), + d_which(TYPE_VALIDITY), + d_unknownExplanation(unknownExplanation) { + CheckArgument(v == VALIDITY_UNKNOWN, + "improper use of unknown-result constructor"); } + Result(const std::string& s); - enum SAT isSAT() { + enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } - enum Validity isValid() { + enum Validity isValid() const { return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; } - 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; - -};/* class Result */ - -inline Result Result::asSatisfiabilityResult() const { - if(d_which == TYPE_SAT) { - return *this; - } - - switch(d_validity) { - - case INVALID: - return Result(SAT); - - case VALID: - return Result(UNSAT); - - case VALIDITY_UNKNOWN: - return Result(SAT_UNKNOWN); - - default: - Unhandled(d_validity); + bool isUnknown() const { + return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } -} - -inline Result Result::asValidityResult() const { - if(d_which == TYPE_VALIDITY) { - return *this; + enum UnknownExplanation whyUnknown() const { + AlwaysAssert( isUnknown(), + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); + return d_unknownExplanation; } - switch(d_sat) { - - case SAT: - return Result(INVALID); + bool operator==(const Result& r) const; + inline bool operator!=(const Result& r) const; + Result asSatisfiabilityResult() const; + Result asValidityResult() const; - case UNSAT: - return Result(VALID); + std::string toString() const; - case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN); +};/* class Result */ - default: - Unhandled(d_sat); - } +inline bool Result::operator!=(const Result& r) const { + return !(*this == r); } -inline std::ostream& operator<<(std::ostream& out, Result r) { - if(r.d_which == Result::TYPE_SAT) { - switch(r.d_sat) { - case Result::UNSAT: out << "UNSAT"; break; - case Result::SAT: out << "SAT"; break; - case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; - } - } else { - switch(r.d_validity) { - case Result::INVALID: out << "INVALID"; break; - case Result::VALID: out << "VALID"; break; - case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; - } - } - - return out; -} +std::ostream& operator<<(std::ostream& out, + enum Result::Sat s) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + enum Result::Validity v) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + enum Result::UnknownExplanation e) CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 9821664bd..376a8a224 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -38,7 +38,7 @@ class CVC4_PUBLIC SExpr { bool d_isAtom; /** The value of an atomic S-expression. */ - std::string d_value; + std::string d_stringValue; /** The children of a list S-expression. */ std::vector<SExpr> d_children; @@ -50,7 +50,7 @@ public: SExpr(const std::string& value) : d_isAtom(true), - d_value(value) { + d_stringValue(value) { } SExpr(const std::vector<SExpr> children) : @@ -80,7 +80,7 @@ inline bool SExpr::isAtom() const { inline const std::string SExpr::getValue() const { AlwaysAssert( d_isAtom ); - return d_value; + return d_stringValue; } inline const std::vector<SExpr> SExpr::getChildren() const { diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc index 5b4a33bed..d153464e1 100644 --- a/test/regress/regress0/arith/arith.01.cvc +++ b/test/regress/regress0/arith/arith.01.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x : REAL; y : REAL; diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc index a2c93da46..76a7a4338 100644 --- a/test/regress/regress0/arith/arith.02.cvc +++ b/test/regress/regress0/arith/arith.02.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x : REAL; y : REAL; z : REAL; diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc index 96af458f0..007adf1d6 100644 --- a/test/regress/regress0/arith/arith.03.cvc +++ b/test/regress/regress0/arith/arith.03.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x : REAL; y : REAL; diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc index d0205116c..cdfb3a09f 100644 --- a/test/regress/regress0/boolean-prec.cvc +++ b/test/regress/regress0/boolean-prec.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of AND, <=>, NOT. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index eeac40c9f..fe3450c27 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid p : BOOLEAN; q : BOOLEAN; r : BOOLEAN; diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc index c6d79a4ab..394f89e51 100644 --- a/test/regress/regress0/bug32.cvc +++ b/test/regress/regress0/bug32.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid a:BOOLEAN; b:BOOLEAN; ASSERT(a); diff --git a/test/regress/regress0/cvc3-bug15.cvc b/test/regress/regress0/cvc3-bug15.cvc index aaebeebd6..371374078 100644 --- a/test/regress/regress0/cvc3-bug15.cvc +++ b/test/regress/regress0/cvc3-bug15.cvc @@ -1,5 +1,5 @@ %% This test borrowed from CVC3 regressions, bug15.cvc -% EXPECT: VALID +% EXPECT: valid x : REAL; y : REAL; f : REAL -> REAL; diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index 07bfa392c..64231aaf5 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress0/ite.cvc b/test/regress/regress0/ite.cvc index 0a3e7535a..5094c997d 100644 --- a/test/regress/regress0/ite.cvc +++ b/test/regress/regress0/ite.cvc @@ -1,4 +1,4 @@ -% EXPECT: UNSAT +% EXPECT: unsat % EXIT: 20 x, y : REAL; CHECKSAT (NOT (x = IF TRUE THEN x ELSE y ENDIF)); diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc index 5348cf7e4..9a247d2c6 100644 --- a/test/regress/regress0/logops.01.cvc +++ b/test/regress/regress0/logops.01.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); % EXIT: 20 diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc index 4a8539fae..105cc7685 100644 --- a/test/regress/regress0/logops.02.cvc +++ b/test/regress/regress0/logops.02.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: INVALID +% EXPECT: invalid QUERY NOT c AND b; % EXIT: 10 diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc index 6b5f34613..65126699c 100644 --- a/test/regress/regress0/logops.03.cvc +++ b/test/regress/regress0/logops.03.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); % EXIT: 20 diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc index 6e7aa1f5e..258307e8c 100644 --- a/test/regress/regress0/logops.04.cvc +++ b/test/regress/regress0/logops.04.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY (a => b) <=> (NOT a OR b); % EXIT: 20 diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc index 14e2c887a..b7308870e 100644 --- a/test/regress/regress0/logops.05.cvc +++ b/test/regress/regress0/logops.05.cvc @@ -1,5 +1,5 @@ a, b, c: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY TRUE XOR FALSE; % EXIT: 20 diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc index 0de37db83..547633bf1 100644 --- a/test/regress/regress0/precedence/and-not.cvc +++ b/test/regress/regress0/precedence/and-not.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of AND and NOT. A, B: BOOLEAN; diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc index 7b29bb95e..dfc03bf22 100644 --- a/test/regress/regress0/precedence/and-xor.cvc +++ b/test/regress/regress0/precedence/and-xor.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of XOR and AND. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/bool-cmp.cvc b/test/regress/regress0/precedence/bool-cmp.cvc index ef1345cc1..d19ab9aae 100644 --- a/test/regress/regress0/precedence/bool-cmp.cvc +++ b/test/regress/regress0/precedence/bool-cmp.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of comparisons and booleans x , y, z: INT; diff --git a/test/regress/regress0/precedence/cmp-plus.cvc b/test/regress/regress0/precedence/cmp-plus.cvc index af2823fcf..aff12548f 100644 --- a/test/regress/regress0/precedence/cmp-plus.cvc +++ b/test/regress/regress0/precedence/cmp-plus.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of comparisons and plus/minus x, y, z: INT; diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc index e85b4a3e6..f207071b3 100644 --- a/test/regress/regress0/precedence/eq-fun.cvc +++ b/test/regress/regress0/precedence/eq-fun.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of function application and = T : TYPE; diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc index b92354753..a496ccf16 100644 --- a/test/regress/regress0/precedence/iff-assoc.cvc +++ b/test/regress/regress0/precedence/iff-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right associativity of <=> A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc index 0115fc319..ee2e2479f 100644 --- a/test/regress/regress0/precedence/iff-implies.cvc +++ b/test/regress/regress0/precedence/iff-implies.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of <=> and =>. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc index d465df313..b87038a99 100644 --- a/test/regress/regress0/precedence/implies-assoc.cvc +++ b/test/regress/regress0/precedence/implies-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right associativity of => A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc index f8c813ceb..4a2aa18a8 100644 --- a/test/regress/regress0/precedence/implies-iff.cvc +++ b/test/regress/regress0/precedence/implies-iff.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of <=> and =>. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc index 24edb4ecd..266daae40 100644 --- a/test/regress/regress0/precedence/implies-or.cvc +++ b/test/regress/regress0/precedence/implies-or.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of => and OR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc index 8c849a0d9..048d971b4 100644 --- a/test/regress/regress0/precedence/not-and.cvc +++ b/test/regress/regress0/precedence/not-and.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of AND and NOT. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc index 6d712d43d..cf4a0e4a5 100644 --- a/test/regress/regress0/precedence/not-eq.cvc +++ b/test/regress/regress0/precedence/not-eq.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of = and NOT. A, B: INT; diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc index d91f79dc8..13f3a316e 100644 --- a/test/regress/regress0/precedence/or-implies.cvc +++ b/test/regress/regress0/precedence/or-implies.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of => and OR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc index 47cc87c76..4e19be584 100644 --- a/test/regress/regress0/precedence/or-xor.cvc +++ b/test/regress/regress0/precedence/or-xor.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of OR and XOR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/plus-mult.cvc b/test/regress/regress0/precedence/plus-mult.cvc index ecd34f583..9300ae6c4 100644 --- a/test/regress/regress0/precedence/plus-mult.cvc +++ b/test/regress/regress0/precedence/plus-mult.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of plus/minus and mult/divide a, b, c, d, e: INT; diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc index ba3f48a7f..950c8ee94 100644 --- a/test/regress/regress0/precedence/xor-and.cvc +++ b/test/regress/regress0/precedence/xor-and.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of XOR and AND. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc index 27911332c..a356f9b3a 100644 --- a/test/regress/regress0/precedence/xor-assoc.cvc +++ b/test/regress/regress0/precedence/xor-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for left associativity of XOR A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc index 2b4436937..837e4c575 100644 --- a/test/regress/regress0/precedence/xor-or.cvc +++ b/test/regress/regress0/precedence/xor-or.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of OR and XOR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc index fe6235981..110984083 100644 --- a/test/regress/regress0/queries0.cvc +++ b/test/regress/regress0/queries0.cvc @@ -2,10 +2,10 @@ a, b: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY (a AND b) OR NOT (a AND b); -% EXPECT: INVALID +% EXPECT: invalid QUERY (a OR b); % EXIT: 10 diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc index a0bff6c5a..4a16dcbe3 100644 --- a/test/regress/regress0/simple.cvc +++ b/test/regress/regress0/simple.cvc @@ -3,6 +3,6 @@ ASSERT x1 OR NOT x0; ASSERT x0 OR NOT x3; ASSERT x3 OR x2; ASSERT x1 AND NOT x1; -% EXPECT: VALID +% EXPECT: valid QUERY x2; % EXIT: 20 diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc index fe17e0b53..dc316a9fb 100644 --- a/test/regress/regress0/smallcnf.cvc +++ b/test/regress/regress0/smallcnf.cvc @@ -4,7 +4,7 @@ ASSERT NOT a OR NOT b; ASSERT c OR b OR a; ASSERT b OR NOT a; ASSERT a OR NOT b OR c; -% EXPECT: INVALID +% EXPECT: invalid QUERY FALSE; % EXIT: 10 diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc index 2fa1e23ba..f777e517e 100644 --- a/test/regress/regress0/test11.cvc +++ b/test/regress/regress0/test11.cvc @@ -3,6 +3,6 @@ x, y : BOOLEAN; ASSERT (x OR y); ASSERT NOT (x OR y); -% EXPECT: VALID +% EXPECT: valid QUERY FALSE; % EXIT: 20 diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc index a3d63b497..25245f36a 100644 --- a/test/regress/regress0/test12.cvc +++ b/test/regress/regress0/test12.cvc @@ -1,33 +1,33 @@ -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: VALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: VALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: INVALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: valid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: valid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: invalid +% EXPECT: valid +% EXPECT: valid +% EXPECT: valid A: TYPE; P_1: BOOLEAN; P_2: BOOLEAN; diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc index 64c2011a4..0cf587bca 100644 --- a/test/regress/regress0/test9.cvc +++ b/test/regress/regress0/test9.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid P,Q:BOOLEAN; ASSERT (P OR Q); QUERY (P OR Q); diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc index 84b8b8a8d..141cc11fb 100644 --- a/test/regress/regress0/uf/simple.01.cvc +++ b/test/regress/regress0/uf/simple.01.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc index 21d3e3cee..3a72ce71a 100644 --- a/test/regress/regress0/uf/simple.02.cvc +++ b/test/regress/regress0/uf/simple.02.cvc @@ -1,4 +1,4 @@ -% EXPECT: INVALID +% EXPECT: invalid A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc index 476c6cd4a..e0079c826 100644 --- a/test/regress/regress0/uf/simple.03.cvc +++ b/test/regress/regress0/uf/simple.03.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc index c9675588d..649accd21 100644 --- a/test/regress/regress0/uf/simple.04.cvc +++ b/test/regress/regress0/uf/simple.04.cvc @@ -1,4 +1,4 @@ -% EXPECT: INVALID +% EXPECT: invalid A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc index a44b028a2..1b35efd7d 100644 --- a/test/regress/regress0/uf20-03.cvc +++ b/test/regress/regress0/uf20-03.cvc @@ -1,4 +1,4 @@ -% EXPECT: INVALID +% EXPECT: invalid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc index 7b6835469..3833bb85f 100644 --- a/test/regress/regress0/wiki.01.cvc +++ b/test/regress/regress0/wiki.01.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR (b OR c) <=> (a OR b) OR c; % EXIT: 20 diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc index 9fd4f8fb7..a431f9b22 100644 --- a/test/regress/regress0/wiki.02.cvc +++ b/test/regress/regress0/wiki.02.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND (b AND c) <=> (a AND b) AND c; % EXIT: 20 diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc index 63c1029b4..65acbb438 100644 --- a/test/regress/regress0/wiki.03.cvc +++ b/test/regress/regress0/wiki.03.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR b <=> b OR a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc index 77fa0059b..bcd724c8d 100644 --- a/test/regress/regress0/wiki.04.cvc +++ b/test/regress/regress0/wiki.04.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND b <=> b AND a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index cb7140bcc..9469a9902 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR (a AND b) <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc index 6c69ca4bc..64663e459 100644 --- a/test/regress/regress0/wiki.06.cvc +++ b/test/regress/regress0/wiki.06.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND (a OR b) <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc index a0281d04b..85de76be7 100644 --- a/test/regress/regress0/wiki.07.cvc +++ b/test/regress/regress0/wiki.07.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); % EXIT: 20 diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc index ddf0f328c..cedf3dba0 100644 --- a/test/regress/regress0/wiki.08.cvc +++ b/test/regress/regress0/wiki.08.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); % EXIT: 20 diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc index f97021910..ded0edd5a 100644 --- a/test/regress/regress0/wiki.09.cvc +++ b/test/regress/regress0/wiki.09.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR NOT a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc index da8a1a9c3..dd1e7031a 100644 --- a/test/regress/regress0/wiki.10.cvc +++ b/test/regress/regress0/wiki.10.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND NOT a <=> FALSE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc index 4d7c3c130..61e404338 100644 --- a/test/regress/regress0/wiki.11.cvc +++ b/test/regress/regress0/wiki.11.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR a <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc index c932892c8..b73b0357b 100644 --- a/test/regress/regress0/wiki.12.cvc +++ b/test/regress/regress0/wiki.12.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND a <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc index 3ad4fd4ab..6ae844616 100644 --- a/test/regress/regress0/wiki.13.cvc +++ b/test/regress/regress0/wiki.13.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR FALSE <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc index 454cf442c..228a5af4f 100644 --- a/test/regress/regress0/wiki.14.cvc +++ b/test/regress/regress0/wiki.14.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND TRUE <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc index 81a13f798..b78e2cb80 100644 --- a/test/regress/regress0/wiki.15.cvc +++ b/test/regress/regress0/wiki.15.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR TRUE <=> TRUE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc index bd13faf11..0282c59af 100644 --- a/test/regress/regress0/wiki.16.cvc +++ b/test/regress/regress0/wiki.16.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND FALSE <=> FALSE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc index 48949f89f..5d3b7629b 100644 --- a/test/regress/regress0/wiki.17.cvc +++ b/test/regress/regress0/wiki.17.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT FALSE <=> TRUE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc index 8959d34a6..a34ceeef8 100644 --- a/test/regress/regress0/wiki.18.cvc +++ b/test/regress/regress0/wiki.18.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT TRUE <=> FALSE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc index 11366526b..38c557514 100644 --- a/test/regress/regress0/wiki.19.cvc +++ b/test/regress/regress0/wiki.19.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT (a OR b) <=> NOT a AND NOT b; % EXIT: 20 diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc index 5ef534bb0..cd166f956 100644 --- a/test/regress/regress0/wiki.20.cvc +++ b/test/regress/regress0/wiki.20.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT (a AND b) <=> NOT a OR NOT b; % EXIT: 20 diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc index bcd7146fb..a8fbafbc1 100644 --- a/test/regress/regress0/wiki.21.cvc +++ b/test/regress/regress0/wiki.21.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT NOT a <=> a; % EXIT: 20 diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress1/hole7.cvc index 5ff290f62..150c39e38 100644 --- a/test/regress/regress1/hole7.cvc +++ b/test/regress/regress1/hole7.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress1/hole8.cvc index d0f974619..fb9206aa0 100644 --- a/test/regress/regress1/hole8.cvc +++ b/test/regress/regress1/hole8.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress2/hole9.cvc index e631444d3..e9bd543ef 100644 --- a/test/regress/regress2/hole9.cvc +++ b/test/regress/regress2/hole9.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress3/hole10.cvc index 661e3ef4b..ba29355db 100644 --- a/test/regress/regress3/hole10.cvc +++ b/test/regress/regress3/hole10.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/run_regression b/test/regress/run_regression index ebef82cf1..614f02f0f 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -52,10 +52,10 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *:status *sat' "$benchmark" &>/dev/null; then - expected_output=SAT + expected_output=sat expected_exit_status=10 elif grep '^ *:status *unsat' "$benchmark" &>/dev/null; then - expected_output=UNSAT + expected_output=unsat expected_exit_status=20 else error "cannot determine status of \`$benchmark'" @@ -80,10 +80,10 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *(set-info *:status *sat' "$benchmark" &>/dev/null; then - expected_output=SAT + expected_output=sat expected_exit_status=10 elif grep '^ *(set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_output=UNSAT + expected_output=unsat expected_exit_status=20 else error "cannot determine status of \`$benchmark'" diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index ee3d9c200..b340beb50 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -30,7 +30,7 @@ #include "prop/prop_engine.h" #include "prop/sat.h" #include "smt/smt_engine.h" -#include "util/options.h" +#include "smt/options.h" #include "util/decision_engine.h" using namespace CVC4; diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index a9b902dea..3e7a9f523 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -31,7 +31,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" -#include "util/options.h" +#include "smt/options.h" #include "util/Assert.h" using namespace CVC4; diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 0920fbd56..965857684 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -35,7 +35,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" -#include "util/options.h" +#include "smt/options.h" #include "util/Assert.h" using namespace CVC4; |