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
#define __CVC4__CONTEXT__CDSET_H
#include "context/context.h"
+#include "context/cdset_forward.h"
#include "context/cdmap.h"
#include "util/Assert.h"
--- /dev/null
+/********************* */
+/*! \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 */
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) :
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() {
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;
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;
#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"
#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"
using namespace CVC4::parser;
using namespace CVC4::main;
-static Result lastResult;
-
namespace CVC4 {
namespace main {
struct Options options;
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
// 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){
} 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();
- }
- }
}
}
#include <signal.h>
#include "util/exception.h"
-#include "util/options.h"
+#include "smt/options.h"
#include "util/Assert.h"
#include "util/stats.h"
$cmd = seq;
}
}
+ | /* get-assignment */
+ GET_ASSIGNMENT_TOK
+ { cmd = new GetAssignmentCommand; }
| /* assertion */
ASSERT_TOK term[expr]
{ cmd = new AssertCommand(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;
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';
#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>
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;
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;
}
}
}
printSatisfyingAssignment();
}
- Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl;
+ Debug("prop") << "PropEngine::checkSat() => "
+ << (result ? "true" : "false") << endl;
return Result(result ? Result::SAT : Result::UNSAT);
}
Debug("prop") << "pop()" << endl;
}
-}/* prop namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#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 {
};/* class PropEngine */
-}/* prop namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* __CVC4__PROP_ENGINE_H */
// 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
smt_engine.h \
noninteractive_exception.h \
bad_option_exception.h \
- no_such_function_exception.h
+ no_such_function_exception.h \
+ options.h
--- /dev/null
+/********************* */
+/*! \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 */
#include <vector>
#include <string>
+#include <sstream>
#include "smt/smt_engine.h"
#include "smt/modal_exception.h"
#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"
d_decisionEngine(NULL),
d_theoryEngine(NULL),
d_propEngine(NULL),
+ d_definedFunctions(NULL),
d_assertionList(NULL),
+ d_assignments(NULL),
d_haveAdditions(false),
d_status() {
shutdown();
+ if(d_assignments != NULL) {
+ d_assignments->deleteSelf();
+ }
+
if(d_assertionList != NULL) {
d_assertionList->deleteSelf();
}
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();
} 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();
}
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
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)
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
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()
#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"
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;
*/
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
* 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
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;
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;
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; }
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());
}
/**
/**
* 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
#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"
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;
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) { }
#include "expr/attribute.h"
#include "theory/theory.h"
#include "expr/node_builder.h"
+#include "smt/options.h"
#include <vector>
#include <list>
}
}
+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,
#include "theory/arrays/theory_arrays.h"
#include "theory/bv/theory_bv.h"
-#include "util/options.h"
#include "util/stats.h"
namespace CVC4 {
/**
* 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;
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);
}
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);
}
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);
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);
}
hash.h \
bool.h \
model.h \
- options.h \
output.cpp \
output.h \
result.h \
+ result.cpp \
unique_id.h \
configuration.h \
configuration_private.h \
+++ /dev/null
-/********************* */
-/*! \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 or equivalent) tuning parameters.
- **
- ** Global (command-line or equivalent) tuning parameters.
- **/
-
-#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 support SmtEngine::getAssignment() for this run. */
- 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 */
--- /dev/null
+/********************* */
+/*! \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 */
#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
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 */
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;
SExpr(const std::string& value) :
d_isAtom(true),
- d_value(value) {
+ d_stringValue(value) {
}
SExpr(const std::vector<SExpr> children) :
inline const std::string SExpr::getValue() const {
AlwaysAssert( d_isAtom );
- return d_value;
+ return d_stringValue;
}
inline const std::vector<SExpr> SExpr::getChildren() const {
-% EXPECT: VALID
+% EXPECT: valid
x : REAL;
y : REAL;
-% EXPECT: VALID
+% EXPECT: valid
x : REAL;
y : REAL;
z : REAL;
-% EXPECT: VALID
+% EXPECT: valid
x : REAL;
y : REAL;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of AND, <=>, NOT.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
p : BOOLEAN;
q : BOOLEAN;
r : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
a:BOOLEAN;
b:BOOLEAN;
ASSERT(a);
%% This test borrowed from CVC3 regressions, bug15.cvc
-% EXPECT: VALID
+% EXPECT: valid
x : REAL;
y : REAL;
f : REAL -> REAL;
-% EXPECT: VALID
+% EXPECT: valid
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
-% EXPECT: UNSAT
+% EXPECT: unsat
% EXIT: 20
x, y : REAL;
CHECKSAT (NOT (x = IF TRUE THEN x ELSE y ENDIF));
a, b, c: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
% EXIT: 20
a, b, c: BOOLEAN;
-% EXPECT: INVALID
+% EXPECT: invalid
QUERY NOT c AND b;
% EXIT: 10
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
a, b, c: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY (a => b) <=> (NOT a OR b);
% EXIT: 20
a, b, c: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY TRUE XOR FALSE;
% EXIT: 20
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of AND and NOT.
A, B: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of XOR and AND.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of comparisons and booleans
x , y, z: INT;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of comparisons and plus/minus
x, y, z: INT;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of function application and =
T : TYPE;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right associativity of <=>
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of <=> and =>.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right associativity of =>
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of <=> and =>.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of => and OR.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of AND and NOT.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of = and NOT.
A, B: INT;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of => and OR.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of OR and XOR.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of plus/minus and mult/divide
a, b, c, d, e: INT;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of XOR and AND.
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for left associativity of XOR
A, B, C: BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
% Simple test for right precedence of OR and XOR.
A, B, C: BOOLEAN;
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
ASSERT x0 OR NOT x3;
ASSERT x3 OR x2;
ASSERT x1 AND NOT x1;
-% EXPECT: VALID
+% EXPECT: valid
QUERY x2;
% EXIT: 20
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
ASSERT (x OR y);
ASSERT NOT (x OR y);
-% EXPECT: VALID
+% EXPECT: valid
QUERY FALSE;
% EXIT: 20
-% 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;
-% EXPECT: VALID
+% EXPECT: valid
P,Q:BOOLEAN;
ASSERT (P OR Q);
QUERY (P OR Q);
-% EXPECT: VALID
+% EXPECT: valid
A: TYPE;
B: TYPE;
x, y: A;
-% EXPECT: INVALID
+% EXPECT: invalid
A: TYPE;
B: TYPE;
x, y: A;
-% EXPECT: VALID
+% EXPECT: valid
A: TYPE;
B: TYPE;
x, y: A;
-% EXPECT: INVALID
+% EXPECT: invalid
A: TYPE;
B: TYPE;
x, y: A;
-% EXPECT: INVALID
+% EXPECT: invalid
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a OR (b OR c) <=> (a OR b) OR c;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a AND (b AND c) <=> (a AND b) AND c;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a OR b <=> b OR a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a AND b <=> b AND a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a OR (a AND b) <=> a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a AND (a OR b) <=> a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a OR NOT a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a AND NOT a <=> FALSE;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a OR a <=> a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a AND a <=> a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a OR FALSE <=> a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a AND TRUE <=> a;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a OR TRUE <=> TRUE;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY a AND FALSE <=> FALSE;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY NOT FALSE <=> TRUE;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY NOT TRUE <=> FALSE;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY NOT (a OR b) <=> NOT a AND NOT b;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY NOT (a AND b) <=> NOT a OR NOT b;
% EXIT: 20
a, b, c : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
QUERY NOT NOT a <=> a;
% EXIT: 20
-% EXPECT: VALID
+% EXPECT: valid
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
-% EXPECT: VALID
+% EXPECT: valid
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
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'"
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'"
#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;
#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;
#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;
projects / cvc5.git / commitdiff