diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/compat | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/Makefile | 4 | ||||
-rw-r--r-- | src/compat/Makefile.am | 50 | ||||
-rw-r--r-- | src/compat/cvc3_compat.cpp | 1886 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 1465 |
4 files changed, 3405 insertions, 0 deletions
diff --git a/src/compat/Makefile b/src/compat/Makefile new file mode 100644 index 000000000..675bd8827 --- /dev/null +++ b/src/compat/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = src/compat + +include $(topdir)/Makefile.subdir diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am new file mode 100644 index 000000000..905eaa6c4 --- /dev/null +++ b/src/compat/Makefile.am @@ -0,0 +1,50 @@ +# LIBCVC4COMPAT_VERSION (-version-info) is in the form current:revision:age +# +# current - +# increment if interfaces have been added, removed or changed +# revision - +# increment if source code has changed +# set to zero if current is incremented +# age - +# increment if interfaces have been added +# set to zero if interfaces have been removed +# or changed +# +LIBCVC4COMPAT_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@ + +AM_CPPFLAGS = \ + -D__BUILDING_CVC4COMPATLIB \ + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +if CVC4_BUILD_LIBCOMPAT + +nobase_lib_LTLIBRARIES = libcvc4compat.la +if HAVE_CXXTESTGEN +noinst_LTLIBRARIES = libcvc4compat_noinst.la +endif + +libcvc4compat_la_LDFLAGS = \ + -version-info $(LIBCVC4COMPAT_VERSION) +libcvc4compat_noinst_la_LDFLAGS = + +libcvc4compat_la_LIBADD = \ + @builddir@/../lib/libreplacements.la +libcvc4compat_noinst_la_LIBADD = \ + @builddir@/../lib/libreplacements.la + +libcvc4compat_la_SOURCES = \ + cvc3_compat.h \ + cvc3_compat.cpp + +libcvc4compat_noinst_la_SOURCES = \ + cvc3_compat.h \ + cvc3_compat.cpp + +else + +EXTRA_DIST = \ + cvc3_compat.h \ + cvc3_compat.cpp + +endif diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp new file mode 100644 index 000000000..99cf4e84b --- /dev/null +++ b/src/compat/cvc3_compat.cpp @@ -0,0 +1,1886 @@ +/********************* */ +/*! \file cvc3_compat.cpp + ** \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, 2011 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 CVC3 compatibility layer for CVC4 + ** + ** CVC3 compatibility layer for CVC4. + **/ + +#include "compat/cvc3_compat.h" + +#include "expr/kind.h" +#include "expr/command.h" + +#include "util/rational.h" +#include "util/integer.h" +#include "util/bitvector.h" + +#include "parser/parser.h" +#include "parser/parser_builder.h" + +#include <iostream> +#include <string> +#include <sstream> + +using namespace std; + +namespace CVC3 { + +std::string int2string(int n) { + std::ostringstream ss; + ss << n; + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, CLFlagType clft) { + switch(clft) { + case CLFLAG_NULL: out << "CLFLAG_NULL"; + case CLFLAG_BOOL: out << "CLFLAG_BOOL"; + case CLFLAG_INT: out << "CLFLAG_INT"; + case CLFLAG_STRING: out << "CLFLAG_STRING"; + case CLFLAG_STRVEC: out << "CLFLAG_STRVEC"; + default: out << "CLFlagType!UNKNOWN"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, QueryResult qr) { + switch(qr) { + case SATISFIABLE: out << "SATISFIABLE/INVALID"; break; + case UNSATISFIABLE: out << "VALID/UNSATISFIABLE"; break; + case ABORT: out << "ABORT"; break; + case UNKNOWN: out << "UNKNOWN"; break; + default: out << "QueryResult!UNKNOWN"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, FormulaValue fv) { + switch(fv) { + case TRUE_VAL: out << "TRUE_VAL"; break; + case FALSE_VAL: out << "FALSE_VAL"; break; + case UNKNOWN_VAL: out << "UNKNOWN_VAL"; break; + default: out << "FormulaValue!UNKNOWN"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, CVC3CardinalityKind c) { + switch(c) { + case CARD_FINITE: out << "CARD_FINITE"; break; + case CARD_INFINITE: out << "CARD_INFINITE"; break; + case CARD_UNKNOWN: out << "CARD_UNKNOWN"; break; + default: out << "CVC3CardinalityKind!UNKNOWN"; + } + + return out; +} + +static string toString(CLFlagType clft) { + stringstream sstr; + sstr << clft; + return sstr.str(); +} + +bool operator==(const Cardinality& c, CVC3CardinalityKind d) { + switch(d) { + case CARD_FINITE: + return c.isFinite(); + case CARD_INFINITE: + return c.isInfinite(); + case CARD_UNKNOWN: + return c.isUnknown(); + } + + Unhandled(d); +} + +bool operator==(CVC3CardinalityKind d, const Cardinality& c) { + return c == d; +} + +bool operator!=(const Cardinality& c, CVC3CardinalityKind d) { + return !(c == d); +} + +bool operator!=(CVC3CardinalityKind d, const Cardinality& c) { + return !(c == d); +} + +Type::Type() : + CVC4::Type() { +} + +Type::Type(const CVC4::Type& type) : + CVC4::Type(type) { +} + +Type::Type(const Type& type) : + CVC4::Type(type) { +} + +Expr Type::getExpr() const { + Unimplemented(); +} + +int Type::arity() const { + return isSort() ? CVC4::SortType(*this).getParamTypes().size() : 0; +} + +Type Type::operator[](int i) const { + return Type(CVC4::Type(CVC4::SortType(*this).getParamTypes()[i])); +} + +bool Type::isBool() const { + return isBoolean(); +} + +bool Type::isSubtype() const { + return false; +} + +Cardinality Type::card() const { + return getCardinality(); +} + +Expr Type::enumerateFinite(Unsigned n) const { + Unimplemented(); +} + +Unsigned Type::sizeFinite() const { + return getCardinality().getFiniteCardinality().getUnsignedLong(); +} + +Type Type::typeBool(ExprManager* em) { + return Type(CVC4::Type(em->booleanType())); +} + +Type Type::funType(const std::vector<Type>& typeDom, + const Type& typeRan) { + const vector<CVC4::Type>& dom = + *reinterpret_cast<const vector<CVC4::Type>*>(&typeDom); + return Type(typeRan.getExprManager()->mkFunctionType(dom, typeRan)); +} + +Type Type::funType(const Type& typeRan) const { + return Type(getExprManager()->mkFunctionType(*this, typeRan)); +} + +Expr::Expr() : CVC4::Expr() { +} + +Expr::Expr(const Expr& e) : CVC4::Expr(e) { +} + +Expr::Expr(const CVC4::Expr& e) : CVC4::Expr(e) { +} + +Expr Expr::eqExpr(const Expr& right) const { + return getEM()->mkExpr(CVC4::kind::EQUAL, *this, right); +} + +Expr Expr::notExpr() const { + return getEM()->mkExpr(CVC4::kind::NOT, *this); +} + +Expr Expr::negate() const { + // avoid double-negatives + return (getKind() == CVC4::kind::NOT) ? + (*this)[0] : + Expr(getEM()->mkExpr(CVC4::kind::NOT, *this)); +} + +Expr Expr::andExpr(const Expr& right) const { + return getEM()->mkExpr(CVC4::kind::AND, *this, right); +} + +Expr Expr::orExpr(const Expr& right) const { + return getEM()->mkExpr(CVC4::kind::OR, *this, right); +} + +Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { + return getEM()->mkExpr(CVC4::kind::ITE, *this, thenpart, elsepart); +} + +Expr Expr::iffExpr(const Expr& right) const { + return getEM()->mkExpr(CVC4::kind::IFF, *this, right); +} + +Expr Expr::impExpr(const Expr& right) const { + return getEM()->mkExpr(CVC4::kind::IMPLIES, *this, right); +} + +Expr Expr::xorExpr(const Expr& right) const { + return getEM()->mkExpr(CVC4::kind::XOR, *this, right); +} + +Expr Expr::substExpr(const std::vector<Expr>& oldTerms, + const std::vector<Expr>& newTerms) const { + const vector<CVC4::Expr>& o = + *reinterpret_cast<const vector<CVC4::Expr>*>(&oldTerms); + const vector<CVC4::Expr>& n = + *reinterpret_cast<const vector<CVC4::Expr>*>(&newTerms); + + return Expr(substitute(o, n)); +} + +Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const { + const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n = + *reinterpret_cast<const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew); + + return Expr(substitute(o2n)); +} + +Expr Expr::operator!() const { + return notExpr(); +} + +Expr Expr::operator&&(const Expr& right) const { + return andExpr(right); +} + +Expr Expr::operator||(const Expr& right) const { + return orExpr(right); +} + +size_t Expr::hash(const Expr& e) { + return CVC4::ExprHashFunction()(e); +} + +size_t Expr::hash() const { + return CVC4::ExprHashFunction()(*this); +} + +bool Expr::isFalse() const { + return getKind() == CVC4::kind::CONST_BOOLEAN && !getConst<bool>(); +} + +bool Expr::isTrue() const { + return getKind() == CVC4::kind::CONST_BOOLEAN && getConst<bool>(); +} + +bool Expr::isBoolConst() const { + return getKind() == CVC4::kind::CONST_BOOLEAN; +} + +bool Expr::isVar() const { + return isVariable(); +} + +bool Expr::isEq() const { + return getKind() == CVC4::kind::EQUAL; +} + +bool Expr::isNot() const { + return getKind() == CVC4::kind::NOT; +} + +bool Expr::isAnd() const { + return getKind() == CVC4::kind::AND; +} + +bool Expr::isOr() const { + return getKind() == CVC4::kind::OR; +} + +bool Expr::isITE() const { + return getKind() == CVC4::kind::ITE; +} + +bool Expr::isIff() const { + return getKind() == CVC4::kind::IFF; +} + +bool Expr::isImpl() const { + return getKind() == CVC4::kind::IMPLIES; +} + +bool Expr::isXor() const { + return getKind() == CVC4::kind::XOR; +} + +bool Expr::isRational() const { + return getKind() == CVC4::kind::CONST_RATIONAL; +} + +bool Expr::isSkolem() const { + return getKind() == CVC4::kind::SKOLEM; +} + +std::vector< std::vector<Expr> > Expr::getTriggers() const { + return vector< vector<Expr> >(); +} + +ExprManager* Expr::getEM() const { + return getExprManager(); +} + +std::vector<Expr> Expr::getKids() const { + vector<CVC4::Expr> v = getChildren(); + return *reinterpret_cast<vector<Expr>*>(&v); +} + +ExprIndex Expr::getIndex() const { + return getId(); +} + +int Expr::arity() const { + return getNumChildren(); +} + +Expr Expr::unnegate() const { + return isNot() ? Expr((*this)[0]) : *this; +} + +bool Expr::isInitialized() const { + return !isNull(); +} + +Type Expr::getType() const { + return Type(this->CVC4::Expr::getType()); +} + +Type Expr::lookupType() const { + return getType(); +} + +Expr Expr::operator[](int i) const { + return Expr(this->CVC4::Expr::operator[](i)); +} + +CLFlag::CLFlag(bool b, const std::string& help, bool display) : + d_tp(CLFLAG_BOOL) { + d_data.b = b; +} + +CLFlag::CLFlag(int i, const std::string& help, bool display) : + d_tp(CLFLAG_INT) { + d_data.i = i; +} + +CLFlag::CLFlag(const std::string& s, const std::string& help, bool display) : + d_tp(CLFLAG_STRING) { + d_data.s = new string(s); +} + +CLFlag::CLFlag(const char* s, const std::string& help, bool display) : + d_tp(CLFLAG_STRING) { + d_data.s = new string(s); +} + +CLFlag::CLFlag(const std::vector<std::pair<std::string,bool> >& sv, + const std::string& help, bool display) : + d_tp(CLFLAG_STRVEC) { + d_data.sv = new vector<pair<string, bool> >(sv); +} + +CLFlag::CLFlag() : + d_tp(CLFLAG_NULL) { +} + +CLFlag::CLFlag(const CLFlag& f) : + d_tp(f.d_tp) { + switch(d_tp) { + case CLFLAG_STRING: + d_data.s = new string(*f.d_data.s); + break; + case CLFLAG_STRVEC: + d_data.sv = new vector<pair<string, bool> >(*f.d_data.sv); + break; + default: + d_data = f.d_data; + } +} + +CLFlag::~CLFlag() { + switch(d_tp) { + case CLFLAG_STRING: + delete d_data.s; + break; + case CLFLAG_STRVEC: + delete d_data.sv; + break; + default: + ; // nothing to do + } +} + +CLFlag& CLFlag::operator=(const CLFlag& f) { + if(this == &f) { + // self-assignment + return *this; + } + + // try to preserve the existing heap objects if possible + if(d_tp == f.d_tp) { + switch(d_tp) { + case CLFLAG_STRING: + *d_data.s = *f.d_data.s; + break; + case CLFLAG_STRVEC: + *d_data.sv = *f.d_data.sv; + break; + default: + d_data = f.d_data; + } + } else { + switch(d_tp) { + case CLFLAG_STRING: + delete d_data.s; + break; + case CLFLAG_STRVEC: + delete d_data.sv; + break; + default: + ; // nothing to do here + } + + switch(f.d_tp) { + case CLFLAG_STRING: + d_data.s = new string(*f.d_data.s); + break; + case CLFLAG_STRVEC: + d_data.sv = new vector<pair<string, bool> >(*f.d_data.sv); + break; + default: + d_data = f.d_data; + } + } + d_tp = f.d_tp; + return *this; +} + +CLFlag& CLFlag::operator=(bool b) { + CheckArgument(d_tp == CLFLAG_BOOL, this); + d_data.b = b; + return *this; +} + +CLFlag& CLFlag::operator=(int i) { + CheckArgument(d_tp == CLFLAG_INT, this); + d_data.i = i; + return *this; +} + +CLFlag& CLFlag::operator=(const std::string& s) { + CheckArgument(d_tp == CLFLAG_STRING, this); + *d_data.s = s; + return *this; +} + +CLFlag& CLFlag::operator=(const char* s) { + CheckArgument(d_tp == CLFLAG_STRING, this); + *d_data.s = s; + return *this; +} + +CLFlag& CLFlag::operator=(const std::pair<std::string, bool>& p) { + CheckArgument(d_tp == CLFLAG_STRVEC, this); + d_data.sv->push_back(p); + return *this; +} + +CLFlag& CLFlag::operator=(const std::vector<std::pair<std::string, bool> >& sv) { + CheckArgument(d_tp == CLFLAG_STRVEC, this); + *d_data.sv = sv; + return *this; +} + +CLFlagType CLFlag::getType() const { + return d_tp; +} + +bool CLFlag::modified() const { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +bool CLFlag::display() const { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +const bool& CLFlag::getBool() const { + CheckArgument(d_tp == CLFLAG_BOOL, this); + return d_data.b; +} + +const int& CLFlag::getInt() const { + CheckArgument(d_tp == CLFLAG_INT, this); + return d_data.i; +} + +const std::string& CLFlag::getString() const { + CheckArgument(d_tp == CLFLAG_STRING, this); + return *d_data.s; +} + +const std::vector<std::pair<std::string, bool> >& CLFlag::getStrVec() const { + CheckArgument(d_tp == CLFLAG_STRVEC, this); + return *d_data.sv; +} + +const std::string& CLFlag::getHelp() const { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void CLFlags::addFlag(const std::string& name, const CLFlag& f) { + d_map[name] = f; +} + +size_t CLFlags::countFlags(const std::string& name) const { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +size_t CLFlags::countFlags(const std::string& name, + std::vector<std::string>& names) const { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +const CLFlag& CLFlags::getFlag(const std::string& name) const { + FlagMap::const_iterator i = d_map.find(name); + CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + return (*i).second; +} + +const CLFlag& CLFlags::operator[](const std::string& name) const { + return getFlag(name); +} + +void CLFlags::setFlag(const std::string& name, const CLFlag& f) { + FlagMap::iterator i = d_map.find(name); + CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CheckArgument((*i).second.getType() == f.getType(), f, + "Command-line flag `%s' has type %s, but caller tried to set to a %s.", + name.c_str(), + toString((*i).second.getType()).c_str(), + toString(f.getType()).c_str()); + (*i).second = f; +} + +void CLFlags::setFlag(const std::string& name, bool b) { + FlagMap::iterator i = d_map.find(name); + CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + (*i).second = b; +} + +void CLFlags::setFlag(const std::string& name, int i) { + FlagMap::iterator it = d_map.find(name); + CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported."); + (*it).second = i; +} + +void CLFlags::setFlag(const std::string& name, const std::string& s) { + FlagMap::iterator i = d_map.find(name); + CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + (*i).second = s; +} + +void CLFlags::setFlag(const std::string& name, const char* s) { + FlagMap::iterator i = d_map.find(name); + CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + (*i).second = s; +} + +void CLFlags::setFlag(const std::string& name, const std::pair<std::string, bool>& p) { + FlagMap::iterator i = d_map.find(name); + CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + (*i).second = p; +} + +void CLFlags::setFlag(const std::string& name, + const std::vector<std::pair<std::string, bool> >& sv) { + FlagMap::iterator i = d_map.find(name); + CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + (*i).second = sv; +} + +ValidityChecker::ValidityChecker() : + d_clflags(new CLFlags()), + d_em(), + d_smt(&d_em) { +} + +ValidityChecker::ValidityChecker(const CLFlags& clflags) : + d_clflags(new CLFlags(clflags)), + d_em(), + d_smt(&d_em) { +} + +ValidityChecker::~ValidityChecker() { + delete d_clflags; +} + +CLFlags& ValidityChecker::getFlags() const { + return *d_clflags; +} + +void ValidityChecker::reprocessFlags() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +CLFlags ValidityChecker::createFlags() { + CLFlags flags; + + // We expect the user to type cvc3 -h to get help, which will set + // the "help" flag to false; that's why it's initially true. + + // Overall system control flags + flags.addFlag("timeout", CLFlag(0, "Kill cvc3 process after given number of seconds (0==no limit)")); + flags.addFlag("stimeout", CLFlag(0, "Set time resource limit in tenths of seconds for a query(0==no limit)")); + flags.addFlag("resource", CLFlag(0, "Set finite resource limit (0==no limit)")); + flags.addFlag("mm", CLFlag("chunks", "Memory manager (chunks, malloc)")); + + // Information printing flags + flags.addFlag("help",CLFlag(true, "print usage information and exit")); + flags.addFlag("unsupported",CLFlag(true, "print usage for old/unsupported/experimental options")); + flags.addFlag("version",CLFlag(true, "print version information and exit")); + flags.addFlag("interactive", CLFlag(false, "Interactive mode")); + flags.addFlag("stats", CLFlag(false, "Print run-time statistics")); + flags.addFlag("seed", CLFlag(1, "Set the seed for random sequence")); + flags.addFlag("printResults", CLFlag(true, "Print results of interactive commands.")); + flags.addFlag("dump-log", CLFlag("", "Dump API call log in CVC3 input " + "format to given file " + "(off when file name is \"\")")); + flags.addFlag("parse-only", CLFlag(false,"Parse the input, then exit.")); + + //Translation related flags + flags.addFlag("expResult", CLFlag("", "For smtlib translation. Give the expected result", false)); + flags.addFlag("category", CLFlag("unknown", "For smtlib translation. Give the category", false)); + flags.addFlag("translate", CLFlag(false, "Produce a complete translation from " + "the input language to output language. ")); + flags.addFlag("real2int", CLFlag(false, "When translating, convert reals to integers.", false)); + flags.addFlag("convertArith", CLFlag(false, "When translating, try to rewrite arith terms into smt-lib subset", false)); + flags.addFlag("convert2diff", CLFlag("", "When translating, try to force into difference logic. Legal values are int and real.", false)); + flags.addFlag("iteLiftArith", CLFlag(false, "For translation. If true, ite's are lifted out of arith exprs.", false)); + flags.addFlag("convertArray", CLFlag(false, "For translation. If true, arrays are converted to uninterpreted functions if possible.", false)); + flags.addFlag("combineAssump", CLFlag(false, "For translation. If true, assumptions are combined into the query.", false)); + flags.addFlag("convert2array", CLFlag(false, "For translation. If true, try to convert to array-only theory", false)); + flags.addFlag("convertToBV",CLFlag(0, "For translation. Set to nonzero to convert ints to bv's of that length", false)); + flags.addFlag("convert-eq-iff",CLFlag(false, "Convert equality on Boolean expressions to iff.", false)); + flags.addFlag("preSimplify",CLFlag(false, "Simplify each assertion or query before translating it", false)); + flags.addFlag("dump-tcc", CLFlag(false, "Compute and dump TCC only")); + flags.addFlag("trans-skip-pp", CLFlag(false, "Skip preprocess step in translation module", false)); + flags.addFlag("trans-skip-difficulty", CLFlag(false, "Leave out difficulty attribute during translation to SMT v2.0", false)); + flags.addFlag("promote", CLFlag(true, "Promote undefined logic combinations to defined logic combinations during translation to SMT", false)); + + // Parser related flags + flags.addFlag("old-func-syntax",CLFlag(false, "Enable parsing of old-style function syntax", false)); + + // Pretty-printing related flags + flags.addFlag("dagify-exprs", + CLFlag(true, "Print expressions with sharing as DAGs")); + flags.addFlag("lang", CLFlag("presentation", "Input language " + "(presentation, smt, smt2, internal)")); + flags.addFlag("output-lang", CLFlag("", "Output language " + "(presentation, smtlib, simplify, internal, lisp, tptp, spass)")); + flags.addFlag("indent", CLFlag(false, "Print expressions with indentation")); + flags.addFlag("width", CLFlag(80, "Suggested line width for printing")); + flags.addFlag("print-depth", CLFlag(-1, "Max. depth to print expressions ")); + flags.addFlag("print-assump", CLFlag(false, "Print assumptions in Theorems ")); + + // Search Engine (SAT) related flags + flags.addFlag("sat",CLFlag("minisat", "choose a SAT solver to use " + "(sat, minisat)")); + flags.addFlag("de",CLFlag("dfs", "choose a decision engine to use " + "(dfs, sat)")); + + // Proofs and Assumptions + flags.addFlag("proofs", CLFlag(false, "Produce proofs")); + flags.addFlag("check-proofs", CLFlag(false, "Check proofs on-the-fly")); + flags.addFlag("minimizeClauses", CLFlag(false, "Use brute-force minimization of clauses", false)); + flags.addFlag("dynack", CLFlag(false, "Use dynamic Ackermannization", false)); + flags.addFlag("smart-clauses", CLFlag(true, "Learn multiple clauses per conflict")); + // Core framework switches + flags.addFlag("tcc", CLFlag(false, "Check TCCs for each ASSERT and QUERY")); + flags.addFlag("cnf", CLFlag(true, "Convert top-level Boolean formulas to CNF", false)); + flags.addFlag("ignore-cnf-vars", CLFlag(false, "Do not split on aux. CNF vars (with +cnf)", false)); + flags.addFlag("orig-formula", CLFlag(false, "Preserve the original formula with +cnf (for splitter heuristics)", false)); + flags.addFlag("liftITE", CLFlag(false, "Eagerly lift all ITE exprs")); + flags.addFlag("iflift", CLFlag(false, "Translate if-then-else terms to CNF (with +cnf)", false)); + flags.addFlag("circuit", CLFlag(false, "With +cnf, use circuit propagation", false)); + flags.addFlag("un-ite-ify", CLFlag(false, "Unconvert ITE expressions", false)); + flags.addFlag("ite-cond-simp", + CLFlag(false, "Replace ITE condition by TRUE/FALSE in subexprs", false)); + flags.addFlag("preprocess", CLFlag(true, "Preprocess queries")); + flags.addFlag("pp-pushneg", CLFlag(false, "Push negation in preprocessor")); + flags.addFlag("pp-bryant", CLFlag(false, "Enable Bryant algorithm for UF", false)); + flags.addFlag("pp-budget", CLFlag(0, "Budget for new preprocessing step", false)); + flags.addFlag("pp-care", CLFlag(true, "Enable care-set preprocessing step", false)); + flags.addFlag("simp-and", CLFlag(false, "Rewrite x&y to x&y[x/true]", false)); + flags.addFlag("simp-or", CLFlag(false, "Rewrite x|y to x|y[x/false]", false)); + flags.addFlag("pp-batch", CLFlag(false, "Ignore assumptions until query, then process all at once")); + + // Negate the query when translate into tptp + flags.addFlag("negate-query", CLFlag(true, "Negate the query when translate into TPTP format"));; + + // Concrete model generation (counterexamples) flags + flags.addFlag("counterexample", CLFlag(false, "Dump counterexample if formula is invalid or satisfiable")); + flags.addFlag("model", CLFlag(false, "Dump model if formula is invalid or satisfiable")); + flags.addFlag("unknown-check-model", CLFlag(false, "Try to generate model if formula is unknown")); + flags.addFlag("applications", CLFlag(true, "Add relevant function applications and array accesses to the concrete countermodel")); + // Debugging flags (only for the debug build) + // #ifdef _CVC3_DEBUG_MODE + vector<pair<string,bool> > sv; + flags.addFlag("trace", CLFlag(sv, "Tracing. Multiple flags add up.")); + flags.addFlag("dump-trace", CLFlag("", "Dump debugging trace to " + "given file (off when file name is \"\")")); + // #endif + // DP-specific flags + + // Arithmetic + flags.addFlag("arith-new",CLFlag(false, "Use new arithmetic dp", false)); + flags.addFlag("arith3",CLFlag(false, "Use old arithmetic dp that works well with combined theories", false)); + flags.addFlag("var-order", + CLFlag(false, "Use simple variable order in arith", false)); + flags.addFlag("ineq-delay", CLFlag(0, "Accumulate this many inequalities before processing (-1 for don't process until necessary)")); + + flags.addFlag("nonlinear-sign-split", CLFlag(true, "Whether to split on the signs of nontrivial nonlinear terms")); + + flags.addFlag("grayshadow-threshold", CLFlag(-1, "Ignore gray shadows bigger than this (makes solver incomplete)")); + flags.addFlag("pathlength-threshold", CLFlag(-1, "Ignore gray shadows bigger than this (makes solver incomplete)")); + + // Arrays + flags.addFlag("liftReadIte", CLFlag(true, "Lift read of ite")); + + //for LFSC stuff, disable Tseitin CNF conversion, by Yeting + flags.addFlag("cnf-formula", CLFlag(false, "The input must be in CNF. This option automatically enables '-de sat' and disable preprocess")); + + //for LFSC print out, by Yeting + //flags.addFlag("lfsc", CLFlag(false, "the input is already in CNF. This option automatically enables -de sat and disable -preprocess")); + + // for LFSC print, allows different modes by Liana + flags.addFlag("lfsc-mode", + CLFlag(0, "lfsc mode 0: off, 1:normal, 2:cvc3-mimic etc.")); + + + // Quantifiers + flags.addFlag("max-quant-inst", CLFlag(200, "The maximum number of" + " naive instantiations")); + + flags.addFlag("quant-new", + CLFlag(true, "If this option is false, only naive instantiation is called")); + + flags.addFlag("quant-lazy", CLFlag(false, "Instantiate lazily", false)); + + flags.addFlag("quant-sem-match", + CLFlag(false, "Attempt to match semantically when instantiating", false)); + +// flags.addFlag("quant-const-match", +// CLFlag(true, "When matching semantically, only match with constants", false)); + + flags.addFlag("quant-complete-inst", + CLFlag(false, "Try complete instantiation heuristic. +pp-batch will be automatically enabled")); + + flags.addFlag("quant-max-IL", + CLFlag(100, "The maximum Instantiation Level allowed")); + + flags.addFlag("quant-inst-lcache", + CLFlag(true, "Cache instantiations")); + + flags.addFlag("quant-inst-gcache", + CLFlag(false, "Cache instantiations", false)); + + flags.addFlag("quant-inst-tcache", + CLFlag(false, "Cache instantiations", false)); + + + flags.addFlag("quant-inst-true", + CLFlag(true, "Ignore true instantiations")); + + flags.addFlag("quant-pullvar", + CLFlag(false, "Pull out vars", false)); + + flags.addFlag("quant-score", + CLFlag(true, "Use instantiation level")); + + flags.addFlag("quant-polarity", + CLFlag(false, "Use polarity ", false)); + + flags.addFlag("quant-eqnew", + CLFlag(true, "Use new equality matching")); + + flags.addFlag("quant-max-score", + CLFlag(0, "Maximum initial dynamic score")); + + flags.addFlag("quant-trans3", + CLFlag(true, "Use trans heuristic")); + + flags.addFlag("quant-trans2", + CLFlag(true, "Use trans2 heuristic")); + + flags.addFlag("quant-naive-num", + CLFlag(1000, "Maximum number to call naive instantiation")); + + flags.addFlag("quant-naive-inst", + CLFlag(true, "Use naive instantiation")); + + flags.addFlag("quant-man-trig", + CLFlag(true, "Use manual triggers")); + + flags.addFlag("quant-gfact", + CLFlag(false, "Send facts to core directly", false)); + + flags.addFlag("quant-glimit", + CLFlag(1000, "Limit for gfacts", false)); + + flags.addFlag("print-var-type", //by yeting, as requested by Sascha Boehme for proofs + CLFlag(false, "Print types for bound variables")); + + // Bitvectors + flags.addFlag("bv32-flag", + CLFlag(false, "assume that all bitvectors are 32bits with no overflow", false)); + + // Uninterpreted Functions + flags.addFlag("trans-closure", + CLFlag(false,"enables transitive closure of binary relations", false)); + + // Datatypes + flags.addFlag("dt-smartsplits", + CLFlag(true, "enables smart splitting in datatype theory", false)); + flags.addFlag("dt-lazy", + CLFlag(false, "lazy splitting on datatypes", false)); + + return flags; +} + +ValidityChecker* ValidityChecker::create(const CLFlags& flags) { + return new ValidityChecker(flags); +} + +ValidityChecker* ValidityChecker::create() { + return new ValidityChecker(createFlags()); +} + +Type ValidityChecker::boolType() { + return d_em.booleanType(); +} + +Type ValidityChecker::realType() { + return d_em.realType(); +} + +Type ValidityChecker::intType() { + return d_em.integerType(); +} + +Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::tupleType(const Type& type0, const Type& type1) { + vector<CVC4::Type> types; + types.push_back(type0); + types.push_back(type1); + return d_em.mkTupleType(types); +} + +Type ValidityChecker::tupleType(const Type& type0, const Type& type1, const Type& type2) { + vector<CVC4::Type> types; + types.push_back(type0); + types.push_back(type1); + types.push_back(type2); + return d_em.mkTupleType(types); +} + +Type ValidityChecker::tupleType(const std::vector<Type>& types) { + const vector<CVC4::Type>& v = + *reinterpret_cast<const vector<CVC4::Type>*>(&types); + return Type(d_em.mkTupleType(v)); +} + +Type ValidityChecker::recordType(const std::string& field, const Type& type) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::recordType(const std::string& field0, const Type& type0, + const std::string& field1, const Type& type1) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::recordType(const std::string& field0, const Type& type0, + const std::string& field1, const Type& type1, + const std::string& field2, const Type& type2) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::recordType(const std::vector<std::string>& fields, + const std::vector<Type>& types) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::dataType(const std::string& name, + const std::string& constructor, + const std::vector<std::string>& selectors, + const std::vector<Expr>& types) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::dataType(const std::string& name, + const std::vector<std::string>& constructors, + const std::vector<std::vector<std::string> >& selectors, + const std::vector<std::vector<Expr> >& types) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::dataType(const std::vector<std::string>& names, + const std::vector<std::vector<std::string> >& constructors, + const std::vector<std::vector<std::vector<std::string> > >& selectors, + const std::vector<std::vector<std::vector<Expr> > >& types, + std::vector<Type>& returnTypes) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) { + return d_em.mkArrayType(typeIndex, typeData); +} + +Type ValidityChecker::bitvecType(int n) { + CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size"); + return d_em.mkBitVectorType(n); +} + +Type ValidityChecker::funType(const Type& typeDom, const Type& typeRan) { + return d_em.mkFunctionType(typeDom, typeRan); +} + +Type ValidityChecker::funType(const std::vector<Type>& typeDom, const Type& typeRan) { + const vector<CVC4::Type>& dom = + *reinterpret_cast<const vector<CVC4::Type>*>(&typeDom); + return Type(d_em.mkFunctionType(dom, typeRan)); +} + +Type ValidityChecker::createType(const std::string& typeName) { + return d_em.mkSort(typeName); +} + +Type ValidityChecker::createType(const std::string& typeName, const Type& def) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::lookupType(const std::string& typeName) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +ExprManager* ValidityChecker::getEM() { + return &d_em; +} + +Expr ValidityChecker::varExpr(const std::string& name, const Type& type) { + return d_em.mkVar(name, type); +} + +Expr ValidityChecker::varExpr(const std::string& name, const Type& type, + const Expr& def) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::lookupVar(const std::string& name, Type* type) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::getType(const Expr& e) { + return d_em.getType(e); +} + +Type ValidityChecker::getBaseType(const Expr& e) { + Type t = d_em.getType(e); + return t.isInteger() ? Type(d_em.realType()) : t; +} + +Type ValidityChecker::getBaseType(const Type& t) { + return t.isInteger() ? Type(d_em.realType()) : t; +} + +Expr ValidityChecker::getTypePred(const Type&t, const Expr& e) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::stringExpr(const std::string& str) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::idExpr(const std::string& name) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::listExpr(const std::vector<Expr>& kids) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::listExpr(const Expr& e1) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::listExpr(const std::string& op, + const std::vector<Expr>& kids) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1, + const Expr& e2) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1, + const Expr& e2, const Expr& e3) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::printExpr(const Expr& e) { + printExpr(e, Message()); +} + +void ValidityChecker::printExpr(const Expr& e, std::ostream& os) { + Expr::setdepth::Scope sd(os, -1); + Expr::printtypes::Scope pt(os, false); + Expr::setlanguage::Scope sl(os, d_em.getOptions()->outputLanguage); + os << e; +} + +Expr ValidityChecker::parseExpr(const Expr& e) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::parseType(const Expr& e) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::importExpr(const Expr& e) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Type ValidityChecker::importType(const Type& t) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::cmdsFromString(const std::string& s, InputLanguage lang) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::exprFromString(const std::string& e) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::trueExpr() { + return d_em.mkConst(true); +} + +Expr ValidityChecker::falseExpr() { + return d_em.mkConst(false); +} + +Expr ValidityChecker::notExpr(const Expr& child) { + return d_em.mkExpr(CVC4::kind::NOT, child); +} + +Expr ValidityChecker::andExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::AND, left, right); +} + +Expr ValidityChecker::andExpr(const std::vector<Expr>& children) { + const vector<CVC4::Expr>& v = + *reinterpret_cast<const vector<CVC4::Expr>*>(&children); + return d_em.mkExpr(CVC4::kind::AND, v); +} + +Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::OR, left, right); +} + +Expr ValidityChecker::orExpr(const std::vector<Expr>& children) { + const vector<CVC4::Expr>& v = + *reinterpret_cast<const vector<CVC4::Expr>*>(&children); + return d_em.mkExpr(CVC4::kind::OR, v); +} + +Expr ValidityChecker::impliesExpr(const Expr& hyp, const Expr& conc) { + return d_em.mkExpr(CVC4::kind::IMPLIES, hyp, conc); +} + +Expr ValidityChecker::iffExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::IFF, left, right); +} + +Expr ValidityChecker::eqExpr(const Expr& child0, const Expr& child1) { + return d_em.mkExpr(CVC4::kind::EQUAL, child0, child1); +} + +Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart, + const Expr& elsepart) { + return d_em.mkExpr(CVC4::kind::ITE, ifpart, thenpart, elsepart); +} + +Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) { + const vector<CVC4::Expr>& v = + *reinterpret_cast<const vector<CVC4::Expr>*>(&children); + return d_em.mkExpr(CVC4::kind::DISTINCT, v); +} + +Op ValidityChecker::createOp(const std::string& name, const Type& type) { + return d_em.mkVar(name, type); +} + +Op ValidityChecker::createOp(const std::string& name, const Type& type, + const Expr& def) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Op ValidityChecker::lookupOp(const std::string& name, Type* type) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::funExpr(const Op& op, const Expr& child) { + return d_em.mkExpr(CVC4::kind::APPLY_UF, op, child); +} + +Expr ValidityChecker::funExpr(const Op& op, const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::APPLY_UF, op, left, right); +} + +Expr ValidityChecker::funExpr(const Op& op, const Expr& child0, + const Expr& child1, const Expr& child2) { + return d_em.mkExpr(CVC4::kind::APPLY_UF, op, child0, child1, child2); +} + +Expr ValidityChecker::funExpr(const Op& op, const std::vector<Expr>& children) { + vector<CVC4::Expr> opkids; + opkids.push_back(op); + opkids.insert(opkids.end(), children.begin(), children.end()); + return d_em.mkExpr(CVC4::kind::APPLY_UF, opkids); +} + +bool ValidityChecker::addPairToArithOrder(const Expr& smaller, const Expr& bigger) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::ratExpr(int n, int d) { + return d_em.mkConst(Rational(n, d)); +} + +Expr ValidityChecker::ratExpr(const std::string& n, const std::string& d, int base) { + return d_em.mkConst(Rational(n + '/' + d, base)); +} + +Expr ValidityChecker::ratExpr(const std::string& n, int base) { + return d_em.mkConst(Rational(n, base)); +} + +Expr ValidityChecker::uminusExpr(const Expr& child) { + return d_em.mkExpr(CVC4::kind::UMINUS, child); +} + +Expr ValidityChecker::plusExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::PLUS, left, right); +} + +Expr ValidityChecker::plusExpr(const std::vector<Expr>& children) { + const vector<CVC4::Expr>& v = + *reinterpret_cast<const vector<CVC4::Expr>*>(&children); + return d_em.mkExpr(CVC4::kind::PLUS, v); +} + +Expr ValidityChecker::minusExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::MINUS, left, right); +} + +Expr ValidityChecker::multExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::MULT, left, right); +} + +Expr ValidityChecker::powExpr(const Expr& x, const Expr& n) { + return d_em.mkExpr(CVC4::kind::POW, x, n); +} + +Expr ValidityChecker::divideExpr(const Expr& numerator, + const Expr& denominator) { + return d_em.mkExpr(CVC4::kind::DIVISION, numerator, denominator); +} + +Expr ValidityChecker::ltExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::LT, left, right); +} + +Expr ValidityChecker::leExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::LEQ, left, right); +} + +Expr ValidityChecker::gtExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::GT, left, right); +} + +Expr ValidityChecker::geExpr(const Expr& left, const Expr& right) { + return d_em.mkExpr(CVC4::kind::GEQ, left, right); +} + +Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, + const std::string& field1, const Expr& expr1) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, + const std::string& field1, const Expr& expr1, + const std::string& field2, const Expr& expr2) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields, + const std::vector<Expr>& exprs) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field, + const Expr& newValue) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::readExpr(const Expr& array, const Expr& index) { + return d_em.mkExpr(CVC4::kind::SELECT, array, index); +} + +Expr ValidityChecker::writeExpr(const Expr& array, const Expr& index, + const Expr& newValue) { + return d_em.mkExpr(CVC4::kind::STORE, array, index, newValue); +} + +Expr ValidityChecker::newBVConstExpr(const std::string& s, int base) { + return d_em.mkConst(CVC4::BitVector(s, base)); +} + +Expr ValidityChecker::newBVConstExpr(const std::vector<bool>& bits) { + Integer value = 0; + for(vector<bool>::const_iterator i = bits.begin(); i != bits.end(); ++i) { + value *= 2; + value += *i ? 1 : 0; + } + return d_em.mkConst(CVC4::BitVector(bits.size(), value)); +} + +Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { + // implementation based on CVC3's TheoryBitvector::newBVConstExpr() + + CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: " + "not an integer: `%s'", r.toString().c_str()); + CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " + "len = %d", len); + + string s(r.toString(2)); + size_t strsize = s.size(); + size_t length = len; + Expr res; + if(length > 0 && length != strsize) { + //either (length > strsize) or (length < strsize) + if(length < strsize) { + s = s.substr(strsize - length, length); + } else { + string zeros(""); + for(size_t i = 0, pad = length - strsize; i < pad; ++i) + zeros += "0"; + s = zeros + s; + } + } + + return newBVConstExpr(s, 2); +} + +Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, t2); +} + +Expr ValidityChecker::newConcatExpr(const std::vector<Expr>& kids) { + const vector<CVC4::Expr>& v = + *reinterpret_cast<const vector<CVC4::Expr>*>(&kids); + return d_em.mkExpr(CVC4::kind::BITVECTOR_CONCAT, v); +} + +Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int low) { + CheckArgument(e.getType().isBitVector(), e, "can only bvextract from a bitvector, not a `%s'", e.getType().toString().c_str()); + CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low); + CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low); + CheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), hi, "bitvector is of size %u, extraction [%d:%d] is off-the-end", CVC4::BitVectorType(e.getType()).getSize(), hi, low); + return d_em.mkExpr(CVC4::kind::BITVECTOR_EXTRACT, + d_em.mkConst(CVC4::BitVectorExtract(hi, low)), e); +} + +Expr ValidityChecker::newBVNegExpr(const Expr& t1) { + // CVC3's BVNEG => SMT-LIBv2 bvnot + CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_NOT, t1); +} + +Expr ValidityChecker::newBVAndExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_AND, t1, t2); +} + +Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) { + // BVAND is not N-ary + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_OR, t1, t2); +} + +Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) { + // BVOR is not N-ary + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_XOR, t1, t2); +} + +Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) { + // BVXOR is not N-ary + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_XNOR, t1, t2); +} + +Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) { + // BVXNOR is not N-ary + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_NAND, t1, t2); +} + +Expr ValidityChecker::newBVNorExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_NOR, t1, t2); +} + +Expr ValidityChecker::newBVCompExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_COMP, t1, t2); +} + +Expr ValidityChecker::newBVLTExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_ULT, t1, t2); +} + +Expr ValidityChecker::newBVLEExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_ULE, t1, t2); +} + +Expr ValidityChecker::newBVSLTExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_SLT, t1, t2); +} + +Expr ValidityChecker::newBVSLEExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_SLE, t1, t2); +} + +Expr ValidityChecker::newSXExpr(const Expr& t1, int len) { + CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(len >= 0, len, "must sx by a positive integer"); + CheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_SIGN_EXTEND, + d_em.mkConst(CVC4::BitVectorSignExtend(len)), t1); +} + +Expr ValidityChecker::newBVUminusExpr(const Expr& t1) { + // CVC3's BVUMINUS => SMT-LIBv2 bvneg + CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_NEG, t1); +} + +Expr ValidityChecker::newBVSubExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2); +} + +Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector<Expr>& k) { + // BVPLUS is not N-ary + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str()); + Expr e = d_em.mkExpr(CVC4::kind::BITVECTOR_PLUS, t1, t2); + unsigned size = CVC4::BitVectorType(e.getType()).getSize(); + CheckArgument(numbits > 0, numbits, + "argument must be positive integer, not %u", numbits); + CheckArgument(unsigned(numbits) == size, numbits, + "argument must match computed size of bitvector sum: " + "passed size == %u, computed size == %u", numbits, size); + return e; +} + +Expr ValidityChecker::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str()); + Expr e = d_em.mkExpr(CVC4::kind::BITVECTOR_MULT, t1, t2); + unsigned size = CVC4::BitVectorType(e.getType()).getSize(); + CheckArgument(numbits > 0, numbits, + "argument must be positive integer, not %u", numbits); + CheckArgument(unsigned(numbits) == size, numbits, + "argument must match computed size of bitvector product: " + "passed size == %u, computed size == %u", numbits, size); + return e; +} + +Expr ValidityChecker::newBVUDivExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_UDIV, t1, t2); +} + +Expr ValidityChecker::newBVURemExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_UREM, t1, t2); +} + +Expr ValidityChecker::newBVSDivExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_SDIV, t1, t2); +} + +Expr ValidityChecker::newBVSRemExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_SREM, t1, t2); +} + +Expr ValidityChecker::newBVSModExpr(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_SMOD, t1, t2); +} + +Expr ValidityChecker::newFixedLeftShiftExpr(const Expr& t1, int r) { + CheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r); + // Defined in: + // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit + return d_em.mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, d_em.mkConst(CVC4::BitVector(r))); +} + +Expr ValidityChecker::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r) { + CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r); + // just turn it into a BVSHL + return d_em.mkExpr(CVC4::kind::BITVECTOR_SHL, t1, d_em.mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r)))); +} + +Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { + CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r); + // Defined in: + // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit + // Should be equivalent to a BVLSHR; just turn it into that. + return d_em.mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, d_em.mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r)))); +} + +Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_SHL, t1, t2); +} + +Expr ValidityChecker::newBVLSHR(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, t2); +} + +Expr ValidityChecker::newBVASHR(const Expr& t1, const Expr& t2) { + CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + return d_em.mkExpr(CVC4::kind::BITVECTOR_ASHR, t1, t2); +} + +Rational ValidityChecker::computeBVConst(const Expr& e) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) { + const vector<CVC4::Expr>& v = + *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs); + return d_em.mkExpr(CVC4::kind::TUPLE, v); +} + +Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, + const Expr& newValue) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& arg) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Expr& arg) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& uid, + const Type& type) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body, + const Expr& trigger) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body, + const std::vector<Expr>& triggers) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body, + const std::vector<std::vector<Expr> >& triggers) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::setTriggers(const Expr& e, const std::vector<std::vector<Expr> > & triggers) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::setTriggers(const Expr& e, const std::vector<Expr>& triggers) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::setTrigger(const Expr& e, const Expr& trigger) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::existsExpr(const std::vector<Expr>& vars, const Expr& body) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Op ValidityChecker::lambdaExpr(const std::vector<Expr>& vars, const Expr& body) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Op ValidityChecker::transClosure(const Op& op) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::simulateExpr(const Expr& f, const Expr& s0, + const std::vector<Expr>& inputs, + const Expr& n) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::setResourceLimit(unsigned limit) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::setTimeLimit(unsigned limit) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::assertFormula(const Expr& e) { + d_smt.assertFormula(CVC4::BoolExpr(e)); +} + +void ValidityChecker::registerAtom(const Expr& e) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::getImpliedLiteral() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::simplify(const Expr& e) { + return d_smt.simplify(e); +} + +static QueryResult cvc4resultToCvc3result(CVC4::Result r) { + switch(r.isSat()) { + case CVC4::Result::SAT: + return SATISFIABLE; + case CVC4::Result::UNSAT: + return UNSATISFIABLE; + default: + ; + } + + switch(r.isValid()) { + case CVC4::Result::VALID: + return VALID; + case CVC4::Result::INVALID: + return INVALID; + default: + return UNKNOWN; + } +} + +QueryResult ValidityChecker::query(const Expr& e) { + return cvc4resultToCvc3result(d_smt.query(CVC4::BoolExpr(e))); +} + +QueryResult ValidityChecker::checkUnsat(const Expr& e) { + return cvc4resultToCvc3result(d_smt.checkSat(CVC4::BoolExpr(e))); +} + +QueryResult ValidityChecker::checkContinue() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +QueryResult ValidityChecker::restart(const Expr& e) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::returnFromCheck() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) { + CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); + vector<CVC4::Expr> v = d_smt.getAssertions(); + assumptions.swap(*reinterpret_cast<vector<Expr>*>(&v)); +} + +void ValidityChecker::getInternalAssumptions(std::vector<Expr>& assumptions) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::getAssumptions(std::vector<Expr>& assumptions) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::getAssumptionsUsed(std::vector<Expr>& assumptions) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::getProofQuery() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::getCounterExample(std::vector<Expr>& assumptions, + bool inOrder) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::getConcreteModel(ExprMap<Expr>& m) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +QueryResult ValidityChecker::tryModelGeneration() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +FormulaValue ValidityChecker::value(const Expr& e) { + CheckArgument(e.getType() == d_em.booleanType(), e, "argument must be a formula"); + return d_smt.getValue(e).getConst<bool>() ? TRUE_VAL : FALSE_VAL; +} + +bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +bool ValidityChecker::inconsistent() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +bool ValidityChecker::incomplete() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +bool ValidityChecker::incomplete(std::vector<std::string>& reasons) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Proof ValidityChecker::getProof() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::getTCC() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::getAssumptionsTCC(std::vector<Expr>& assumptions) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Proof ValidityChecker::getProofTCC() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Expr ValidityChecker::getClosure() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Proof ValidityChecker::getProofClosure() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +int ValidityChecker::stackLevel() { + return d_smt.getStackLevel(); +} + +void ValidityChecker::push() { + d_smt.push(); +} + +void ValidityChecker::pop() { + d_smt.pop(); +} + +void ValidityChecker::popto(int stackLevel) { + CheckArgument(stackLevel >= 0, stackLevel, + "Cannot pop to a negative stack level %u", stackLevel); + CheckArgument(unsigned(stackLevel) <= d_smt.getStackLevel(), stackLevel, + "Cannot pop to a level higher than the current one! " + "At level %u, user requested level %d", + d_smt.getStackLevel(), stackLevel); + while(unsigned(stackLevel) < d_smt.getStackLevel()) { + pop(); + } +} + +int ValidityChecker::scopeLevel() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::pushScope() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::popScope() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::poptoScope(int scopeLevel) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +Context* ValidityChecker::getCurrentContext() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::reset() { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +void ValidityChecker::logAnnotation(const Expr& annot) { + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +} + +static void doCommands(CVC4::parser::Parser* parser, CVC4::SmtEngine& smt, CVC4::Options& opts) { + while(CVC4::Command* cmd = parser->nextCommand()) { + if(opts.verbosity >= 0) { + cmd->invoke(&smt, *opts.out); + } else { + cmd->invoke(&smt); + } + delete cmd; + } +} + +void ValidityChecker::loadFile(const std::string& fileName, + InputLanguage lang, + bool interactive, + bool calledFromParser) { + CVC4::Options opts = *d_em.getOptions(); + opts.inputLanguage = lang; + opts.interactive = interactive; + CVC4::parser::ParserBuilder parserBuilder(&d_em, fileName, opts); + CVC4::parser::Parser* parser = parserBuilder.build(); + doCommands(parser, d_smt, opts); + delete parser; +} + +void ValidityChecker::loadFile(std::istream& is, + InputLanguage lang, + bool interactive) { + CVC4::Options opts = *d_em.getOptions(); + opts.inputLanguage = lang; + opts.interactive = interactive; + CVC4::parser::ParserBuilder parserBuilder(&d_em, "[stream]", opts); + CVC4::parser::Parser* parser = parserBuilder.withStreamInput(is).build(); + doCommands(parser, d_smt, opts); + delete parser; +} + +Statistics& ValidityChecker::getStatistics() { + return *d_smt.getStatisticsRegistry(); +} + +void ValidityChecker::printStatistics() { + Message() << d_smt.getStatisticsRegistry(); +} + +}/* CVC3 namespace */ diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h new file mode 100644 index 000000000..36c5c0f6a --- /dev/null +++ b/src/compat/cvc3_compat.h @@ -0,0 +1,1465 @@ +/********************* */ +/*! \file cvc3_compat.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, 2011 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 CVC3 compatibility layer for CVC4 + ** + ** CVC3 compatibility layer for CVC4. This version was derived from + ** the following CVS revisions of the following files in CVC3. If + ** those files have a later revision, then this file might be out of + ** date. + ** + ** src/include/vc.h 1.36 + ** src/include/expr.h 1.39 + ** src/include/command_line_flags.h 1.3 + ** src/include/queryresult.h 1.2 + ** src/include/formula_value.h 1.1 + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CVC3_COMPAT_H +#define __CVC4__CVC3_COMPAT_H + +// keep the CVC3 include guard also +#if defined(_cvc3__include__vc_h_) || \ + defined(_cvc3__expr_h_) || \ + defined(_cvc3__command_line_flags_h_) || \ + defined(_cvc3__include__queryresult_h_) || \ + defined(_cvc3__include__formula_value_h_) + +#error "A CVC3 header file was included before CVC4's cvc3_compat.h header. Please include cvc3_compat.h rather than any CVC3 headers." + +#else + +// define these so the files are skipped if the user #includes them too +#define _cvc3__expr_h_ +#define _cvc3__include__vc_h_ +#define _cvc3__command_line_flags_h_ +#define _cvc3__include__queryresult_h_ +#define _cvc3__include__formula_value_h_ + +#include "expr/expr_manager.h" +#include "expr/expr.h" +#include "expr/type.h" + +#include "smt/smt_engine.h" + +#include "util/rational.h" +#include "util/integer.h" + +#include "util/exception.h" +#include "util/hash.h" + +#include <stdlib.h> +#include <map> +#include <utility> + +// some #defines that CVC3 exported to userspace :( +#ifdef CVC4_DEBUG +# define DebugAssert(cond, ...) Assert(cond, "CVC3-style assertion failed"); +# define IF_DEBUG(x) x +#else +# define DebugAssert(...) +# define IF_DEBUG(x) +#endif +#define FatalAssert(cond, ...) AlwaysAssert(cond, "CVC3-style assertion failed"); + +//class CInterface; + +namespace CVC3 { + +std::string int2string(int n); + +//! Different types of command line flags +typedef enum { + CLFLAG_NULL, + CLFLAG_BOOL, + CLFLAG_INT, + CLFLAG_STRING, + CLFLAG_STRVEC //!< Vector of pair<string, bool> +} CLFlagType; + +std::ostream& operator<<(std::ostream& out, CLFlagType clft); + +/*! + Class CLFlag (for Command Line Flag) + + Author: Sergey Berezin + + Date: Fri May 30 14:10:48 2003 + + This class implements a data structure to hold a value of a single + command line flag. +*/ +class CLFlag { + //! Type of the argument + CLFlagType d_tp; + //! The argument + union { + bool b; + int i; + std::string* s; + std::vector<std::pair<std::string,bool> >* sv; + } d_data; + +public: + + //! Constructor for a boolean flag + CLFlag(bool b, const std::string& help, bool display = true); + //! Constructor for an integer flag + CLFlag(int i, const std::string& help, bool display = true); + //! Constructor for a string flag + CLFlag(const std::string& s, const std::string& help, bool display = true); + //! Constructor for a string flag from char* + CLFlag(const char* s, const std::string& help, bool display = true); + //! Constructor for a vector flag + CLFlag(const std::vector<std::pair<std::string,bool> >& sv, + const std::string& help, bool display = true); + //! Default constructor + CLFlag(); + //! Copy constructor + CLFlag(const CLFlag& f); + //! Destructor + ~CLFlag(); + + //! Assignment from another flag + CLFlag& operator=(const CLFlag& f); + //! Assignment of a boolean value + /*! The flag must already have the right type */ + CLFlag& operator=(bool b); + //! Assignment of an integer value + /*! The flag must already have the right type */ + CLFlag& operator=(int i); + //! Assignment of a string value + /*! The flag must already have a string type. */ + CLFlag& operator=(const std::string& s); + //! Assignment of an string value from char* + /*! The flag must already have a string type. */ + CLFlag& operator=(const char* s); + //! Assignment of a string value with a boolean tag to a vector flag + /*! The flag must already have a vector type. The pair of + <string,bool> will be appended to the vector. */ + CLFlag& operator=(const std::pair<std::string,bool>& p); + //! Assignment of a vector value + /*! The flag must already have a vector type. */ + CLFlag& operator=(const std::vector<std::pair<std::string,bool> >& sv); + + // Accessor methods + //! Return the type of the flag + CLFlagType getType() const; + /*! @brief Return true if the flag was modified from the default + value (e.g. set on the command line) */ + bool modified() const; + //! Return true if flag should be displayed in regular help + bool display() const; + + // The value accessors return a reference. For the system-wide + // flags, this reference will remain valid throughout the run of the + // program, even if the flag's value changes. So, the reference can + // be cached, and the value can be checked directly (which is more + // efficient). + const bool& getBool() const; + + const int& getInt() const; + + const std::string& getString() const; + + const std::vector<std::pair<std::string,bool> >& getStrVec() const; + + const std::string& getHelp() const; + +};/* class CLFlag */ + +/////////////////////////////////////////////////////////////////////// +// Class CLFlag (for Command Line Flag) +// +// Author: Sergey Berezin +// Date: Fri May 30 14:10:48 2003 +// +// Database of command line flags. +/////////////////////////////////////////////////////////////////////// + +class CLFlags { + typedef std::map<std::string, CLFlag> FlagMap; + FlagMap d_map; + +public: + // Public methods + // Add a new flag. The name must be a complete flag name. + void addFlag(const std::string& name, const CLFlag& f); + // Count how many flags match the name prefix + size_t countFlags(const std::string& name) const; + // Match the name prefix and add all the matching names to the vector + size_t countFlags(const std::string& name, + std::vector<std::string>& names) const; + // Retrieve an existing flag. The 'name' must be a full name of an + // existing flag. + const CLFlag& getFlag(const std::string& name) const; + + const CLFlag& operator[](const std::string& name) const; + + // Setting the flag to a new value, but preserving the help string. + // The 'name' prefix must uniquely resolve to an existing flag. + void setFlag(const std::string& name, const CLFlag& f); + + // Variants of setFlag for all the types + void setFlag(const std::string& name, bool b); + void setFlag(const std::string& name, int i); + void setFlag(const std::string& name, const std::string& s); + void setFlag(const std::string& name, const char* s); + void setFlag(const std::string& name, const std::pair<std::string, bool>& p); + void setFlag(const std::string& name, + const std::vector<std::pair<std::string, bool> >& sv); + +};/* class CLFlags */ + +class Context; +class Proof {}; + +using CVC4::ExprManager; +using CVC4::InputLanguage; +using CVC4::Rational; +using CVC4::Integer; +using CVC4::Exception; +using CVC4::Cardinality; +using namespace CVC4::kind; + +typedef size_t ExprIndex; +typedef CVC4::TypeCheckingException TypecheckException; +typedef size_t Unsigned; + +static const int READ = ::CVC4::kind::SELECT; +static const int WRITE = ::CVC4::kind::STORE; + +// CVC4 has a more sophisticated Cardinality type; +// but we can support comparison against CVC3's more +// coarse-grained Cardinality. +enum CVC3CardinalityKind { + CARD_FINITE, + CARD_INFINITE, + CARD_UNKNOWN +};/* enum CVC3CardinalityKind */ + +std::ostream& operator<<(std::ostream& out, CVC3CardinalityKind c); + +bool operator==(const Cardinality& c, CVC3CardinalityKind d); +bool operator==(CVC3CardinalityKind d, const Cardinality& c); +bool operator!=(const Cardinality& c, CVC3CardinalityKind d); +bool operator!=(CVC3CardinalityKind d, const Cardinality& c); + +class Expr; + +template <class T> +class ExprMap : public std::map<Expr, T> { +};/* class ExprMap<T> */ + +template <class T> +class ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> { +public: + void insert(Expr a, Expr b); +};/* class ExprHashMap<T> */ + +class Type : public CVC4::Type { +public: + Type(); + Type(const CVC4::Type& type); + Type(const Type& type); + Expr getExpr() const; + + // Reasoning about children + int arity() const; + Type operator[](int i) const; + + // Core testers + bool isBool() const; + bool isSubtype() const; + //! Return cardinality of type + Cardinality card() const; + //! Return nth (starting with 0) element in a finite type + /*! Returns NULL Expr if unable to compute nth element + */ + Expr enumerateFinite(Unsigned n) const; + //! Return size of a finite type; returns 0 if size cannot be determined + Unsigned sizeFinite() const; + + // Core constructors + static Type typeBool(ExprManager* em); + static Type funType(const std::vector<Type>& typeDom, const Type& typeRan); + Type funType(const Type& typeRan) const; + +};/* class CVC3::Type */ + +/** + * Expr class for CVC3 compatibility layer. + * + * This class is identical to (and convertible to/from) a CVC4 Expr, + * except that a few additional functions are supported to provide + * naming compatibility with CVC3. + */ +class Expr : public CVC4::Expr { +public: + Expr(); + Expr(const Expr& e); + Expr(const CVC4::Expr& e); + + // Compound expression constructors + Expr eqExpr(const Expr& right) const; + Expr notExpr() const; + Expr negate() const; // avoid double-negatives + Expr andExpr(const Expr& right) const; + Expr orExpr(const Expr& right) const; + Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const; + Expr iffExpr(const Expr& right) const; + Expr impExpr(const Expr& right) const; + Expr xorExpr(const Expr& right) const; + + Expr substExpr(const std::vector<Expr>& oldTerms, + const std::vector<Expr>& newTerms) const; + Expr substExpr(const ExprHashMap<Expr>& oldToNew) const; + + Expr operator!() const; + Expr operator&&(const Expr& right) const; + Expr operator||(const Expr& right) const; + + static size_t hash(const Expr& e); + + size_t hash() const; + + // Core expression testers + + bool isFalse() const; + bool isTrue() const; + bool isBoolConst() const; + bool isVar() const; + + bool isEq() const; + bool isNot() const; + bool isAnd() const; + bool isOr() const; + bool isITE() const; + bool isIff() const; + bool isImpl() const; + bool isXor() const; + + bool isRational() const; + bool isSkolem() const; + + //! Get the manual triggers of the closure Expr + std::vector< std::vector<Expr> > getTriggers() const; + + // Get the expression manager. The expression must be non-null. + ExprManager* getEM() const; + + // Return a ref to the vector of children. + std::vector<Expr> getKids() const; + + // Get the index field + ExprIndex getIndex() const; + + // Return the number of children. Note, that an application of a + // user-defined function has the arity of that function (the number + // of arguments), and the function name itself is part of the + // operator. + int arity() const; + + // Return the ith child. As with arity, it's also the ith argument + // in function application. + Expr operator[](int i) const; + + //! Remove leading NOT if any + Expr unnegate() const; + + // Check if Expr is not Null + bool isInitialized() const; + + //! Get the type. Recursively compute if necessary + Type getType() const; + //! Look up the current type. Do not recursively compute (i.e. may be NULL) + Type lookupType() const; + +};/* class CVC3::Expr */ + +typedef Expr Op; +typedef CVC4::StatisticsRegistry Statistics; + +#define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4 +#define SMTLIB_LANG ::CVC4::language::input::LANG_SMTLIB +#define SMTLIB_V2_LANG ::CVC4::language::input::LANG_SMTLIB_V2 +#define AST_LANG ::CVC4::language::input::LANG_AST + +/*****************************************************************************/ +/* + * Type for result of queries. VALID and UNSATISFIABLE are treated as + * equivalent, as are SATISFIABLE and INVALID. + */ +/*****************************************************************************/ +typedef enum QueryResult { + SATISFIABLE = 0, + INVALID = 0, + VALID = 1, + UNSATISFIABLE = 1, + ABORT, + UNKNOWN +} QueryResult; + +std::ostream& operator<<(std::ostream& out, QueryResult qr); + +/*****************************************************************************/ +/* + * Type for truth value of formulas. + */ +/*****************************************************************************/ +typedef enum FormulaValue { + TRUE_VAL, + FALSE_VAL, + UNKNOWN_VAL +} FormulaValue; + +std::ostream& operator<<(std::ostream& out, FormulaValue fv); + +/*****************************************************************************/ +/*! + *\class ValidityChecker + *\brief CVC3 API (compatibility layer for CVC4) + * + * All terms and formulas are represented as expressions using the Expr class. + * The notion of a context is also important. A context is a "background" set + * of formulas which are assumed to be true or false. Formulas can be added to + * the context explicitly, using assertFormula, or they may be added as part of + * processing a query command. At any time, the current set of formulas making + * up the context can be retrieved using getAssumptions. + */ +/*****************************************************************************/ +class CVC4_PUBLIC ValidityChecker { + + CLFlags* d_clflags; + CVC4::ExprManager d_em; + CVC4::SmtEngine d_smt; + + ValidityChecker(const CLFlags& clflags); + +public: + //! Constructor + ValidityChecker(); + //! Destructor + virtual ~ValidityChecker(); + + //! Return the set of command-line flags + /*! The flags are returned by reference, and if modified, will have an + immediate effect on the subsequent commands. Note that not all flags will + have such an effect; some flags are used only at initialization time (like + "sat"), and therefore, will not take effect if modified after + ValidityChecker is created. + */ + virtual CLFlags& getFlags() const; + //! Force reprocessing of all flags + virtual void reprocessFlags(); + + /***************************************************************************/ + /* + * Static methods + */ + /***************************************************************************/ + + //! Create the set of command line flags with default values; + /*! + \return the set of flags by value + */ + static CLFlags createFlags(); + //! Create an instance of ValidityChecker + /*! + \param flags is the set of command line flags. + */ + static ValidityChecker* create(const CLFlags& flags); + //! Create an instance of ValidityChecker using default flag values. + static ValidityChecker* create(); + + /***************************************************************************/ + /*! + *\name Type-related methods + * Methods for creating and looking up types + *\sa class Type + *@{ + */ + /***************************************************************************/ + + // Basic types + virtual Type boolType(); //!< Create type BOOLEAN + + virtual Type realType(); //!< Create type REAL + + virtual Type intType(); //!< Create type INT + + //! Create a subrange type [l..r] + /*! l and r can be Null; l=Null represents minus infinity, r=Null is + * plus infinity. + */ + virtual Type subrangeType(const Expr& l, const Expr& r); + + //! Creates a subtype defined by the given predicate + /*! + * \param pred is a predicate taking one argument of type T and returning + * Boolean. The resulting type is a subtype of T whose elements x are those + * satisfying the predicate pred(x). + * + * \param witness is an expression of type T for which pred holds (if a Null + * expression is passed as a witness, cvc will try to prove \f$\exists x. pred(x))\f$. + * if the witness check fails, a TypecheckException is thrown. + */ + virtual Type subtypeType(const Expr& pred, const Expr& witness); + + // Tuple types + //! 2-element tuple + virtual Type tupleType(const Type& type0, const Type& type1); + + //! 3-element tuple + virtual Type tupleType(const Type& type0, const Type& type1, + const Type& type2); + //! n-element tuple (from a vector of types) + virtual Type tupleType(const std::vector<Type>& types); + + // Record types + //! 1-element record + virtual Type recordType(const std::string& field, const Type& type); + + //! 2-element record + /*! Fields will be sorted automatically */ + virtual Type recordType(const std::string& field0, const Type& type0, + const std::string& field1, const Type& type1); + //! 3-element record + /*! Fields will be sorted automatically */ + virtual Type recordType(const std::string& field0, const Type& type0, + const std::string& field1, const Type& type1, + const std::string& field2, const Type& type2); + //! n-element record (fields and types must be of the same length) + /*! Fields will be sorted automatically */ + virtual Type recordType(const std::vector<std::string>& fields, + const std::vector<Type>& types); + + // Datatypes + + //! Single datatype, single constructor + /*! The types are either type exressions (obtained from a type with + * getExpr()) or string expressions containing the name of (one of) the + * dataType(s) being defined. */ + virtual Type dataType(const std::string& name, + const std::string& constructor, + const std::vector<std::string>& selectors, + const std::vector<Expr>& types); + + //! Single datatype, multiple constructors + /*! The types are either type exressions (obtained from a type with + * getExpr()) or string expressions containing the name of (one of) the + * dataType(s) being defined. */ + virtual Type dataType(const std::string& name, + const std::vector<std::string>& constructors, + const std::vector<std::vector<std::string> >& selectors, + const std::vector<std::vector<Expr> >& types); + + //! Multiple datatypes + /*! The types are either type exressions (obtained from a type with + * getExpr()) or string expressions containing the name of (one of) the + * dataType(s) being defined. */ + virtual void dataType(const std::vector<std::string>& names, + const std::vector<std::vector<std::string> >& constructors, + const std::vector<std::vector<std::vector<std::string> > >& selectors, + const std::vector<std::vector<std::vector<Expr> > >& types, + std::vector<Type>& returnTypes); + + //! Create an array type (ARRAY typeIndex OF typeData) + virtual Type arrayType(const Type& typeIndex, const Type& typeData); + + //! Create a bitvector type of length n + virtual Type bitvecType(int n); + + //! Create a function type typeDom -> typeRan + virtual Type funType(const Type& typeDom, const Type& typeRan); + + //! Create a function type (t1,t2,...,tn) -> typeRan + virtual Type funType(const std::vector<Type>& typeDom, const Type& typeRan); + + //! Create named user-defined uninterpreted type + virtual Type createType(const std::string& typeName); + + //! Create named user-defined interpreted type (type abbreviation) + virtual Type createType(const std::string& typeName, const Type& def); + + //! Lookup a user-defined (uninterpreted) type by name. Returns Null if none. + virtual Type lookupType(const std::string& typeName); + + /*@}*/ // End of Type-related methods + + /***************************************************************************/ + /*! + *\name General Expr methods + *\sa class Expr + *\sa class ExprManager + *@{ + */ + /***************************************************************************/ + + //! Return the ExprManager + virtual ExprManager* getEM(); + + //! Create a variable with a given name and type + /*! + \param name is the name of the variable + \param type is its type. The type cannot be a function type. + \return an Expr representation of a new variable + */ + virtual Expr varExpr(const std::string& name, const Type& type); + + //! Create a variable with a given name, type, and value + virtual Expr varExpr(const std::string& name, const Type& type, + const Expr& def); + + //! Get the variable associated with a name, and its type + /*! + \param name is the variable name + \param type is where the type value is returned + + \return a variable by the name. If there is no such Expr, a NULL \ + Expr is returned. + */ + virtual Expr lookupVar(const std::string& name, Type* type); + + //! Get the type of the Expr. + virtual Type getType(const Expr& e); + + //! Get the largest supertype of the Expr. + virtual Type getBaseType(const Expr& e); + + //! Get the largest supertype of the Type. + virtual Type getBaseType(const Type& t); + + //! Get the subtype predicate + virtual Expr getTypePred(const Type&t, const Expr& e); + + //! Create a string Expr + virtual Expr stringExpr(const std::string& str); + + //! Create an ID Expr + virtual Expr idExpr(const std::string& name); + + //! Create a list Expr + /*! Intermediate representation for DP-specific expressions. + * Normally, the first element of the list is a string Expr + * representing an operator, and the rest of the list are the + * arguments. For example, + * + * kids.push_back(vc->stringExpr("PLUS")); + * kids.push_back(x); // x and y are previously created Exprs + * kids.push_back(y); + * Expr lst = vc->listExpr(kids); + * + * Or, alternatively (using its overloaded version): + * + * Expr lst = vc->listExpr("PLUS", x, y); + * + * or + * + * vector<Expr> summands; + * summands.push_back(x); summands.push_back(y); ... + * Expr lst = vc->listExpr("PLUS", summands); + */ + virtual Expr listExpr(const std::vector<Expr>& kids); + + //! Overloaded version of listExpr with one argument + virtual Expr listExpr(const Expr& e1); + + //! Overloaded version of listExpr with two arguments + virtual Expr listExpr(const Expr& e1, const Expr& e2); + + //! Overloaded version of listExpr with three arguments + virtual Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3); + + //! Overloaded version of listExpr with string operator and many arguments + virtual Expr listExpr(const std::string& op, + const std::vector<Expr>& kids); + + //! Overloaded version of listExpr with string operator and one argument + virtual Expr listExpr(const std::string& op, const Expr& e1); + + //! Overloaded version of listExpr with string operator and two arguments + virtual Expr listExpr(const std::string& op, const Expr& e1, + const Expr& e2); + + //! Overloaded version of listExpr with string operator and three arguments + virtual Expr listExpr(const std::string& op, const Expr& e1, + const Expr& e2, const Expr& e3); + + //! Prints e to the standard output + virtual void printExpr(const Expr& e); + + //! Prints e to the given ostream + virtual void printExpr(const Expr& e, std::ostream& os); + + //! Parse an expression using a Theory-specific parser + virtual Expr parseExpr(const Expr& e); + + //! Parse a type expression using a Theory-specific parser + virtual Type parseType(const Expr& e); + + //! Import the Expr from another instance of ValidityChecker + /*! When expressions need to be passed among several instances of + * ValidityChecker, they need to be explicitly imported into the + * corresponding instance using this method. The return result is + * an identical expression that belongs to the current instance of + * ValidityChecker, and can be safely used as part of more complex + * expressions from the same instance. + */ + virtual Expr importExpr(const Expr& e); + + //! Import the Type from another instance of ValidityChecker + /*! \sa getType() */ + virtual Type importType(const Type& t); + + //! Parse a sequence of commands from a presentation language string + virtual void cmdsFromString(const std::string& s, + InputLanguage lang = PRESENTATION_LANG); + + //! Parse an expression from a presentation language string + virtual Expr exprFromString(const std::string& e); + + /*@}*/ // End of General Expr Methods + + /***************************************************************************/ + /*! + *\name Core expression methods + * Methods for manipulating core expressions + * + * Except for equality and ite, the children provided as arguments must be of + * type Boolean. + *@{ + */ + /***************************************************************************/ + + //! Return TRUE Expr + virtual Expr trueExpr(); + + //! Return FALSE Expr + virtual Expr falseExpr(); + + //! Create negation + virtual Expr notExpr(const Expr& child); + + //! Create 2-element conjunction + virtual Expr andExpr(const Expr& left, const Expr& right); + + //! Create n-element conjunction + virtual Expr andExpr(const std::vector<Expr>& children); + + //! Create 2-element disjunction + virtual Expr orExpr(const Expr& left, const Expr& right); + + //! Create n-element disjunction + virtual Expr orExpr(const std::vector<Expr>& children); + + //! Create Boolean implication + virtual Expr impliesExpr(const Expr& hyp, const Expr& conc); + + //! Create left IFF right (boolean equivalence) + virtual Expr iffExpr(const Expr& left, const Expr& right); + + //! Create an equality expression. + /*! + The two children must have the same type, and cannot be of type + Boolean. + */ + virtual Expr eqExpr(const Expr& child0, const Expr& child1); + + //! Create IF ifpart THEN thenpart ELSE elsepart ENDIF + /*! + \param ifpart must be of type Boolean. + \param thenpart and \param elsepart must have the same type, which will + also be the type of the ite expression. + */ + virtual Expr iteExpr(const Expr& ifpart, const Expr& thenpart, + const Expr& elsepart); + + /** + * Create an expression asserting that all the children are different. + * @param children the children to be asserted different + */ + virtual Expr distinctExpr(const std::vector<Expr>& children); + + /*@}*/ // End of Core expression methods + + /***************************************************************************/ + /*! + *\name User-defined (uninterpreted) function methods + * Methods for manipulating uninterpreted function expressions + *@{ + */ + /***************************************************************************/ + + //! Create a named uninterpreted function with a given type + /*! + \param name is the new function's name (as ID Expr) + \param type is a function type ( [range -> domain] ) + */ + virtual Op createOp(const std::string& name, const Type& type); + + //! Create a named user-defined function with a given type + virtual Op createOp(const std::string& name, const Type& type, + const Expr& def); + + //! Get the Op associated with a name, and its type + /*! + \param name is the operator name + \param type is where the type value is returned + + \return an Op by the name. If there is no such Op, a NULL \ + Op is returned. + */ + virtual Op lookupOp(const std::string& name, Type* type); + + //! Unary function application (op must be of function type) + virtual Expr funExpr(const Op& op, const Expr& child); + + //! Binary function application (op must be of function type) + virtual Expr funExpr(const Op& op, const Expr& left, const Expr& right); + + //! Ternary function application (op must be of function type) + virtual Expr funExpr(const Op& op, const Expr& child0, + const Expr& child1, const Expr& child2); + + //! n-ary function application (op must be of function type) + virtual Expr funExpr(const Op& op, const std::vector<Expr>& children); + + /*@}*/ // End of User-defined (uninterpreted) function methods + + /***************************************************************************/ + /*! + *\name Arithmetic expression methods + * Methods for manipulating arithmetic expressions + * + * These functions create arithmetic expressions. The children provided + * as arguments must be of type Real. + *@{ + */ + /***************************************************************************/ + + /*! + * Add the pair of variables to the variable ordering for aritmetic solving. + * Terms that are not arithmetic will be ignored. + * \param smaller the smaller variable + * \param bigger the bigger variable + */ + virtual bool addPairToArithOrder(const Expr& smaller, const Expr& bigger); + + //! Create a rational number with numerator n and denominator d. + /*! + \param n the numerator + \param d the denominator, cannot be 0. + */ + virtual Expr ratExpr(int n, int d = 1); + + //! Create a rational number with numerator n and denominator d. + /*! + Here n and d are given as strings. They are converted to + arbitrary-precision integers according to the given base. + */ + virtual Expr ratExpr(const std::string& n, const std::string& d, int base); + + //! Create a rational from a single string. + /*! + \param n can be a string containing an integer, a pair of integers + "nnn/ddd", or a number in the fixed or floating point format. + \param base is the base in which to interpret the string. + */ + virtual Expr ratExpr(const std::string& n, int base = 10); + + //! Unary minus. + virtual Expr uminusExpr(const Expr& child); + + //! Create 2-element sum (left + right) + virtual Expr plusExpr(const Expr& left, const Expr& right); + + //! Create n-element sum + virtual Expr plusExpr(const std::vector<Expr>& children); + + //! Make a difference (left - right) + virtual Expr minusExpr(const Expr& left, const Expr& right); + + //! Create a product (left * right) + virtual Expr multExpr(const Expr& left, const Expr& right); + + //! Create a power expression (x ^ n); n must be integer + virtual Expr powExpr(const Expr& x, const Expr& n); + + //! Create expression x / y + virtual Expr divideExpr(const Expr& numerator, const Expr& denominator); + + //! Create (left < right) + virtual Expr ltExpr(const Expr& left, const Expr& right); + + //! Create (left <= right) + virtual Expr leExpr(const Expr& left, const Expr& right); + + //! Create (left > right) + virtual Expr gtExpr(const Expr& left, const Expr& right); + + //! Create (left >= right) + virtual Expr geExpr(const Expr& left, const Expr& right); + + /*@}*/ // End of Arithmetic expression methods + + /***************************************************************************/ + /*! + *\name Record expression methods + * Methods for manipulating record expressions + *@{ + */ + /***************************************************************************/ + + //! Create a 1-element record value (# field := expr #) + /*! Fields will be sorted automatically */ + virtual Expr recordExpr(const std::string& field, const Expr& expr); + + //! Create a 2-element record value (# field0 := expr0, field1 := expr1 #) + /*! Fields will be sorted automatically */ + virtual Expr recordExpr(const std::string& field0, const Expr& expr0, + const std::string& field1, const Expr& expr1); + + //! Create a 3-element record value (# field_i := expr_i #) + /*! Fields will be sorted automatically */ + virtual Expr recordExpr(const std::string& field0, const Expr& expr0, + const std::string& field1, const Expr& expr1, + const std::string& field2, const Expr& expr2); + + //! Create an n-element record value (# field_i := expr_i #) + /*! + * \param fields + * \param exprs must be the same length as fields + * + * Fields will be sorted automatically + */ + virtual Expr recordExpr(const std::vector<std::string>& fields, + const std::vector<Expr>& exprs); + + //! Create record.field (field selection) + /*! Create an expression representing the selection of a field from + a record. */ + virtual Expr recSelectExpr(const Expr& record, const std::string& field); + + //! Record update; equivalent to "record WITH .field := newValue" + /*! Notice the `.' before field in the presentation language (and + the comment above); this is to distinguish it from datatype + update. + */ + virtual Expr recUpdateExpr(const Expr& record, const std::string& field, + const Expr& newValue); + + /*@}*/ // End of Record expression methods + + /***************************************************************************/ + /*! + *\name Array expression methods + * Methods for manipulating array expressions + *@{ + */ + /***************************************************************************/ + + //! Create an expression array[index] (array access) + /*! Create an expression for the value of array at the given index */ + virtual Expr readExpr(const Expr& array, const Expr& index); + + //! Array update; equivalent to "array WITH index := newValue" + virtual Expr writeExpr(const Expr& array, const Expr& index, + const Expr& newValue); + + /*@}*/ // End of Array expression methods + + /***************************************************************************/ + /*! + *\name Bitvector expression methods + * Methods for manipulating bitvector expressions + *@{ + */ + /***************************************************************************/ + + // Bitvector constants + // From a string of digits in a given base + virtual Expr newBVConstExpr(const std::string& s, int base = 2); + // From a vector of bools + virtual Expr newBVConstExpr(const std::vector<bool>& bits); + // From a rational: bitvector is of length 'len', or the min. needed length when len=0. + virtual Expr newBVConstExpr(const Rational& r, int len = 0); + + // Concat and extract + virtual Expr newConcatExpr(const Expr& t1, const Expr& t2); + virtual Expr newConcatExpr(const std::vector<Expr>& kids); + virtual Expr newBVExtractExpr(const Expr& e, int hi, int low); + + // Bitwise Boolean operators: Negation, And, Nand, Or, Nor, Xor, Xnor + virtual Expr newBVNegExpr(const Expr& t1); + + virtual Expr newBVAndExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVAndExpr(const std::vector<Expr>& kids); + + virtual Expr newBVOrExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVOrExpr(const std::vector<Expr>& kids); + + virtual Expr newBVXorExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVXorExpr(const std::vector<Expr>& kids); + + virtual Expr newBVXnorExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVXnorExpr(const std::vector<Expr>& kids); + + virtual Expr newBVNandExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVNorExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVCompExpr(const Expr& t1, const Expr& t2); + + // Unsigned bitvector inequalities + virtual Expr newBVLTExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVLEExpr(const Expr& t1, const Expr& t2); + + // Signed bitvector inequalities + virtual Expr newBVSLTExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVSLEExpr(const Expr& t1, const Expr& t2); + + // Sign-extend t1 to a total of len bits + virtual Expr newSXExpr(const Expr& t1, int len); + + // Bitvector arithmetic: unary minus, plus, subtract, multiply + virtual Expr newBVUminusExpr(const Expr& t1); + virtual Expr newBVSubExpr(const Expr& t1, const Expr& t2); + //! 'numbits' is the number of bits in the result + virtual Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k); + virtual Expr newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2); + virtual Expr newBVMultExpr(int numbits, + const Expr& t1, const Expr& t2); + + virtual Expr newBVUDivExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVURemExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVSDivExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVSRemExpr(const Expr& t1, const Expr& t2); + virtual Expr newBVSModExpr(const Expr& t1, const Expr& t2); + + // Left shift by r bits: result is old size + r bits + virtual Expr newFixedLeftShiftExpr(const Expr& t1, int r); + // Left shift by r bits: result is same size as t1 + virtual Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r); + // Logical right shift by r bits: result is same size as t1 + virtual Expr newFixedRightShiftExpr(const Expr& t1, int r); + // Left shift with shift parameter an arbitrary bit-vector expr + virtual Expr newBVSHL(const Expr& t1, const Expr& t2); + // Logical right shift with shift parameter an arbitrary bit-vector expr + virtual Expr newBVLSHR(const Expr& t1, const Expr& t2); + // Arithmetic right shift with shift parameter an arbitrary bit-vector expr + virtual Expr newBVASHR(const Expr& t1, const Expr& t2); + // Get value of BV Constant + virtual Rational computeBVConst(const Expr& e); + + /*@}*/ // End of Bitvector expression methods + + /***************************************************************************/ + /*! + *\name Other expression methods + * Methods for manipulating other kinds of expressions + *@{ + */ + /***************************************************************************/ + + //! Tuple expression + virtual Expr tupleExpr(const std::vector<Expr>& exprs); + + //! Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5) + virtual Expr tupleSelectExpr(const Expr& tuple, int index); + + //! Tuple update; equivalent to "tuple WITH index := newValue" + virtual Expr tupleUpdateExpr(const Expr& tuple, int index, + const Expr& newValue); + + //! Datatype constructor expression + virtual Expr datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args); + + //! Datatype selector expression + virtual Expr datatypeSelExpr(const std::string& selector, const Expr& arg); + + //! Datatype tester expression + virtual Expr datatypeTestExpr(const std::string& constructor, const Expr& arg); + + //! Create a bound variable with a given name, unique ID (uid) and type + /*! + \param name is the name of the variable + \param uid is the unique ID (a string), which must be unique for + each variable + \param type is its type. The type cannot be a function type. + \return an Expr representation of a new variable + */ + virtual Expr boundVarExpr(const std::string& name, + const std::string& uid, + const Type& type); + + //! Universal quantifier + virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body); + //! Universal quantifier with a trigger + virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body, + const Expr& trigger); + //! Universal quantifier with a set of triggers. + virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body, + const std::vector<Expr>& triggers); + //! Universal quantifier with a set of multi-triggers. + virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body, + const std::vector<std::vector<Expr> >& triggers); + + //! Set triggers for quantifier instantiation + /*! + * \param e the expression for which triggers are being set. + * \param triggers Each item in triggers is a vector of Expr containing one + * or more patterns. A pattern is a term or Atomic predicate sub-expression + * of e. A vector containing more than one pattern is treated as a + * multi-trigger. Patterns will be matched in the order they occur in + * the vector. + */ + virtual void setTriggers(const Expr& e, const std::vector<std::vector<Expr> > & triggers); + //! Set triggers for quantifier instantiation (no multi-triggers) + virtual void setTriggers(const Expr& e, const std::vector<Expr>& triggers); + //! Set a single trigger for quantifier instantiation + virtual void setTrigger(const Expr& e, const Expr& trigger); + //! Set a single multi-trigger for quantifier instantiation + virtual void setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger); + + //! Existential quantifier + virtual Expr existsExpr(const std::vector<Expr>& vars, const Expr& body); + + //! Lambda-expression + virtual Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body); + + //! Transitive closure of a binary predicate + virtual Op transClosure(const Op& op); + + //! Symbolic simulation expression + /*! + * \param f is the next state function (LAMBDA-expression) + * \param s0 is the initial state + * \param inputs is the vector of LAMBDA-expressions representing + * the sequences of inputs to f + * \param n is a constant, the number of cycles to run the simulation. + */ + virtual Expr simulateExpr(const Expr& f, const Expr& s0, + const std::vector<Expr>& inputs, + const Expr& n); + + /*@}*/ // End of Other expression methods + + /***************************************************************************/ + /*! + *\name Validity checking methods + * Methods related to validity checking + * + * This group includes methods for asserting formulas, checking + * validity in the given logical context, manipulating the scope + * level of the context, etc. + *@{ + */ + /***************************************************************************/ + + //! Set the resource limit (0==unlimited, 1==exhausted). + /*! Currently, the limit is the total number of processed facts. */ + virtual void setResourceLimit(unsigned limit); + + //! Set a time limit in tenth of a second, + /*! counting the cpu time used by the current process from now on. + * Currently, when the limit is reached, cvc3 tries to quickly + * terminate, probably with the status unknown. + */ + virtual void setTimeLimit(unsigned limit); + + //! Assert a new formula in the current context. + /*! This creates the assumption e |- e. The formula must have Boolean type. + */ + virtual void assertFormula(const Expr& e); + + //! Register an atomic formula of interest. + /*! Registered atoms are tracked by the decision procedures. If one of them + is deduced to be true or false, it is added to a list of implied literals. + Implied literals can be retrieved with the getImpliedLiteral function */ + virtual void registerAtom(const Expr& e); + + //! Return next literal implied by last assertion. Null Expr if none. + /*! Returned literals are either registered atomic formulas or their negation + */ + virtual Expr getImpliedLiteral(); + + //! Simplify e with respect to the current context + virtual Expr simplify(const Expr& e); + + //! Check validity of e in the current context. + /*! If it returns VALID, the scope and context are the same + * as when called. If it returns INVALID, the context will be one which + * falsifies the query. If it returns UNKNOWN, the context will falsify the + * query, but the context may be inconsistent. Finally, if it returns + * ABORT, the context will be one which satisfies as much as possible. + * + * \param e is the queried formula + */ + virtual QueryResult query(const Expr& e); + + //! Check satisfiability of the expr in the current context. + /*! Equivalent to query(!e) */ + virtual QueryResult checkUnsat(const Expr& e); + + //! Get the next model + /*! This method should only be called after a query which returns + INVALID. Its return values are as for query(). */ + virtual QueryResult checkContinue(); + + //! Restart the most recent query with e as an additional assertion. + /*! This method should only be called after a query which returns + INVALID. Its return values are as for query(). */ + virtual QueryResult restart(const Expr& e); + + //! Returns to context immediately before last invalid query. + /*! This method should only be called after a query which returns false. + */ + virtual void returnFromCheck(); + + //! Get assumptions made by the user in this and all previous contexts. + /*! User assumptions are created either by calls to assertFormula or by a + * call to query. In the latter case, the negated query is added as an + * assumption. + * \param assumptions should be empty on entry. + */ + virtual void getUserAssumptions(std::vector<Expr>& assumptions); + + //! Get assumptions made internally in this and all previous contexts. + /*! Internal assumptions are literals assumed by the sat solver. + * \param assumptions should be empty on entry. + */ + virtual void getInternalAssumptions(std::vector<Expr>& assumptions); + + //! Get all assumptions made in this and all previous contexts. + /*! \param assumptions should be empty on entry. + */ + virtual void getAssumptions(std::vector<Expr>& assumptions); + + //! Returns the set of assumptions used in the proof of queried formula. + /*! It returns a subset of getAssumptions(). If the last query was false + * or there has not yet been a query, it does nothing. + * NOTE: this functionality is not supported yet + * \param assumptions should be empty on entry. + */ + virtual void getAssumptionsUsed(std::vector<Expr>& assumptions); + + virtual Expr getProofQuery(); + + + //! Return the internal assumptions that make the queried formula false. + /*! This method should only be called after a query which returns + false. It will try to return the simplest possible subset of + the internal assumptions sufficient to make the queried expression + false. + \param assumptions should be empty on entry. + \param inOrder if true, returns the assumptions in the order they + were made. This is slightly more expensive than inOrder = false. + */ + virtual void getCounterExample(std::vector<Expr>& assumptions, + bool inOrder=true); + + //! Will assign concrete values to all user created variables + /*! This function should only be called after a query which return false. + */ + virtual void getConcreteModel(ExprMap<Expr> & m); + + //! If the result of the last query was UNKNOWN try to actually build the model + //! to verify the result. + /*! This function should only be called after a query which return unknown. + */ + virtual QueryResult tryModelGeneration(); + + //:ALEX: returns the current truth value of a formula + // returns UNKNOWN_VAL if e is not associated + // with a boolean variable in the SAT module, + // i.e. if its value can not determined without search. + virtual FormulaValue value(const Expr& e); + + //! Returns true if the current context is inconsistent. + /*! Also returns a minimal set of assertions used to determine the + inconsistency. + \param assumptions should be empty on entry. + */ + virtual bool inconsistent(std::vector<Expr>& assumptions); + + //! Returns true if the current context is inconsistent. + virtual bool inconsistent(); + + //! Returns true if the invalid result from last query() is imprecise + /*! + * Some decision procedures in CVC are incomplete (quantifier + * elimination, non-linear arithmetic, etc.). If any incomplete + * features were used during the last query(), and the result is + * "invalid" (query() returns false), then this result is + * inconclusive. It means that the system gave up the search for + * contradiction at some point. + */ + virtual bool incomplete(); + + //! Returns true if the invalid result from last query() is imprecise + /*! + * \sa incomplete() + * + * The argument is filled with the reasons for incompleteness (they + * are intended to be shown to the end user). + */ + virtual bool incomplete(std::vector<std::string>& reasons); + + //! Returns the proof term for the last proven query + /*! If there has not been a successful query, it should return a NULL proof + */ + virtual Proof getProof(); + + //! Returns the TCC of the last assumption or query + /*! Returns Null if no assumptions or queries were performed. */ + virtual Expr getTCC(); + + //! Return the set of assumptions used in the proof of the last TCC + virtual void getAssumptionsTCC(std::vector<Expr>& assumptions); + + //! Returns the proof of TCC of the last assumption or query + /*! Returns Null if no assumptions or queries were performed. */ + virtual Proof getProofTCC(); + + //! After successful query, return its closure |- Gamma => phi + /*! Turn a valid query Gamma |- phi into an implication + * |- Gamma => phi. + * + * Returns Null if last query was invalid. + */ + virtual Expr getClosure(); + + //! Construct a proof of the query closure |- Gamma => phi + /*! Returns Null if last query was Invalid. */ + virtual Proof getProofClosure(); + + /*@}*/ // End of Validity checking methods + + /***************************************************************************/ + /*! + *\name Context methods + * Methods for manipulating contexts + * + * Contexts support stack-based push and pop. There are two + * separate notions of the current context stack. stackLevel(), push(), + * pop(), and popto() work with the user-level notion of the stack. + * + * scopeLevel(), pushScope(), popScope(), and poptoScope() work with + * the internal stack which is more fine-grained than the user + * stack. + * + * Do not use the scope methods unless you know what you are doing. + * *@{ + */ + /***************************************************************************/ + + //! Returns the current stack level. Initial level is 0. + virtual int stackLevel(); + + //! Checkpoint the current context and increase the scope level + virtual void push(); + + //! Restore the current context to its state at the last checkpoint + virtual void pop(); + + //! Restore the current context to the given stackLevel. + /*! + \param stackLevel should be greater than or equal to 0 and less + than or equal to the current scope level. + */ + virtual void popto(int stackLevel); + + //! Returns the current scope level. Initially, the scope level is 1. + virtual int scopeLevel(); + + /*! @brief Checkpoint the current context and increase the + * <strong>internal</strong> scope level. Do not use unless you + * know what you're doing! + */ + virtual void pushScope(); + + /*! @brief Restore the current context to its state at the last + * <strong>internal</strong> checkpoint. Do not use unless you know + * what you're doing! + */ + virtual void popScope(); + + //! Restore the current context to the given scopeLevel. + /*! + \param scopeLevel should be less than or equal to the current scope level. + + If scopeLevel is less than 1, then the current context is reset + and the scope level is set to 1. + */ + virtual void poptoScope(int scopeLevel); + + //! Get the current context + virtual Context* getCurrentContext(); + + //! Destroy and recreate validity checker: resets everything except for flags + virtual void reset(); + + //! Add an annotation to the current script - prints annot when translating + virtual void logAnnotation(const Expr& annot); + + /*@}*/ // End of Context methods + + /***************************************************************************/ + /*! + *\name Reading files + * Methods for reading external files + *@{ + */ + /***************************************************************************/ + + //! Read and execute the commands from a file given by name ("" means stdin) + virtual void loadFile(const std::string& fileName, + InputLanguage lang = PRESENTATION_LANG, + bool interactive = false, + bool calledFromParser = false); + + //! Read and execute the commands from a stream + virtual void loadFile(std::istream& is, + InputLanguage lang = PRESENTATION_LANG, + bool interactive = false); + + /*@}*/ // End of methods for reading files + + /***************************************************************************/ + /*! + *\name Reporting Statistics + * Methods for collecting and reporting run-time statistics + *@{ + */ + /***************************************************************************/ + + //! Get statistics object + virtual Statistics& getStatistics(); + + //! Print collected statistics to stdout + virtual void printStatistics(); + + /*@}*/ // End of Statistics Methods + +};/* class ValidityChecker */ + +template <class T> +void ExprHashMap<T>::insert(Expr a, Expr b) { + (*this)[a] = b; +} + +}/* CVC3 namespace */ + +#endif /* _cvc3__include__vc_h_ */ +#endif /* __CVC4__CVC3_COMPAT_H */ |