From 85a8d1bf09f91a041caa1723b30fe9f9ebf571f8 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 6 Sep 2012 20:05:20 +0000 Subject: [PATCH] fixes to the compatibility layer; this fixes the broken system test --- src/compat/cvc3_compat.cpp | 21 ++++++++++----- src/compat/cvc3_compat.h | 53 +++++++++++++++++++------------------- 2 files changed, 42 insertions(+), 32 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index fafc8ccb2..4e884a9ab 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -761,6 +761,7 @@ ValidityChecker::ValidityChecker() : d_smt(NULL), d_parserContext(NULL), d_exprTypeMapRemove(), + d_stackLevel(0), d_constructors(), d_selectors() { d_em = reinterpret_cast(new CVC4::ExprManager(d_options)); @@ -779,6 +780,7 @@ ValidityChecker::ValidityChecker(const CLFlags& clflags) : d_smt(NULL), d_parserContext(NULL), d_exprTypeMapRemove(), + d_stackLevel(0), d_constructors(), d_selectors() { d_em = reinterpret_cast(new CVC4::ExprManager(d_options)); @@ -2228,19 +2230,29 @@ Proof ValidityChecker::getProofClosure() { } int ValidityChecker::stackLevel() { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return d_stackLevel; } void ValidityChecker::push() { + ++d_stackLevel; d_smt->push(); } void ValidityChecker::pop() { d_smt->pop(); + --d_stackLevel; } void ValidityChecker::popto(int stackLevel) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + CheckArgument(stackLevel >= 0, stackLevel, + "Cannot pop to a negative stack level %d", stackLevel); + CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel, + "Cannot pop to a stack level higher than the current one! " + "At stack level %u, user requested stack level %d", + d_stackLevel, stackLevel); + while(unsigned(stackLevel) < d_stackLevel) { + pop(); + } } int ValidityChecker::scopeLevel() { @@ -2257,15 +2269,12 @@ void ValidityChecker::popScope() { void ValidityChecker::poptoScope(int scopeLevel) { CheckArgument(scopeLevel >= 0, scopeLevel, - "Cannot pop to a negative scope level %u", scopeLevel); + "Cannot pop to a negative scope level %d", scopeLevel); CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(), scopeLevel, "Cannot pop to a scope level higher than the current one! " "At scope level %u, user requested scope level %d", d_parserContext->getDeclarationLevel(), scopeLevel); - CheckArgument(scopeLevel <= d_parserContext->getDeclarationLevel(), - scopeLevel, - "Cannot pop to a higher scope level"); while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) { popScope(); } diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 83465775b..39f6658ad 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -96,10 +96,10 @@ const CVC4::Kind BVCONST = CVC4::kind::CONST_BITVECTOR; const CVC4::Kind EXTRACT = CVC4::kind::BITVECTOR_EXTRACT; const CVC4::Kind CONCAT = CVC4::kind::BITVECTOR_CONCAT; -std::string int2string(int n); +std::string int2string(int n) CVC4_PUBLIC; //! Different types of command line flags -typedef enum { +typedef enum CVC4_PUBLIC { CLFLAG_NULL, CLFLAG_BOOL, CLFLAG_INT, @@ -107,7 +107,7 @@ typedef enum { CLFLAG_STRVEC //!< Vector of pair } CLFlagType; -std::ostream& operator<<(std::ostream& out, CLFlagType clft); +std::ostream& operator<<(std::ostream& out, CLFlagType clft) CVC4_PUBLIC; /*! Class CLFlag (for Command Line Flag) @@ -119,7 +119,7 @@ std::ostream& operator<<(std::ostream& out, CLFlagType clft); This class implements a data structure to hold a value of a single command line flag. */ -class CLFlag { +class CVC4_PUBLIC CLFlag { //! Type of the argument CLFlagType d_tp; //! The argument @@ -207,7 +207,7 @@ public: // Database of command line flags. /////////////////////////////////////////////////////////////////////// -class CLFlags { +class CVC4_PUBLIC CLFlags { typedef std::map FlagMap; FlagMap d_map; @@ -241,10 +241,10 @@ public: };/* class CLFlags */ -class ExprManager; -class Context; -class Proof {}; -class Theorem {}; +class CVC4_PUBLIC ExprManager; +class CVC4_PUBLIC Context; +class CVC4_PUBLIC Proof {}; +class CVC4_PUBLIC Theorem {}; using CVC4::InputLanguage; using CVC4::Integer; @@ -263,32 +263,32 @@ 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 { +enum CVC4_PUBLIC CVC3CardinalityKind { CARD_FINITE, CARD_INFINITE, CARD_UNKNOWN };/* enum CVC3CardinalityKind */ -std::ostream& operator<<(std::ostream& out, CVC3CardinalityKind c); +std::ostream& operator<<(std::ostream& out, CVC3CardinalityKind c) CVC4_PUBLIC; -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); +bool operator==(const Cardinality& c, CVC3CardinalityKind d) CVC4_PUBLIC; +bool operator==(CVC3CardinalityKind d, const Cardinality& c) CVC4_PUBLIC; +bool operator!=(const Cardinality& c, CVC3CardinalityKind d) CVC4_PUBLIC; +bool operator!=(CVC3CardinalityKind d, const Cardinality& c) CVC4_PUBLIC; -class Expr; +class CVC4_PUBLIC Expr; template -class ExprMap : public std::map { +class CVC4_PUBLIC ExprMap : public std::map { };/* class ExprMap */ template -class ExprHashMap : public std::hash_map { +class CVC4_PUBLIC ExprHashMap : public std::hash_map { public: void insert(Expr a, Expr b); };/* class ExprHashMap */ -class Type : public CVC4::Type { +class CVC4_PUBLIC Type : public CVC4::Type { public: Type(); Type(const CVC4::Type& type); @@ -318,7 +318,7 @@ public: };/* class CVC3::Type */ -class Expr; +class CVC4_PUBLIC Expr; typedef Expr Op; /** @@ -328,7 +328,7 @@ typedef Expr Op; * except that a few additional functions are supported to provide * naming compatibility with CVC3. */ -class Expr : public CVC4::Expr { +class CVC4_PUBLIC Expr : public CVC4::Expr { public: Expr(); Expr(const Expr& e); @@ -458,9 +458,9 @@ public: };/* class CVC3::Expr */ -bool isArrayLiteral(const Expr&); +bool isArrayLiteral(const Expr&) CVC4_PUBLIC; -class ExprManager : public CVC4::ExprManager { +class CVC4_PUBLIC ExprManager : public CVC4::ExprManager { public: const std::string& getKindName(int kind); //! Get the input language for printing @@ -483,7 +483,7 @@ typedef CVC4::StatisticsRegistry Statistics; * equivalent, as are SATISFIABLE and INVALID. */ /*****************************************************************************/ -typedef enum QueryResult { +typedef enum CVC4_PUBLIC QueryResult { SATISFIABLE = 0, INVALID = 0, VALID = 1, @@ -500,13 +500,13 @@ std::string QueryResultToString(QueryResult query_result); * Type for truth value of formulas. */ /*****************************************************************************/ -typedef enum FormulaValue { +typedef enum CVC4_PUBLIC FormulaValue { TRUE_VAL, FALSE_VAL, UNKNOWN_VAL } FormulaValue; -std::ostream& operator<<(std::ostream& out, FormulaValue fv); +std::ostream& operator<<(std::ostream& out, FormulaValue fv) CVC4_PUBLIC; /*****************************************************************************/ /*! @@ -531,6 +531,7 @@ class CVC4_PUBLIC ValidityChecker { CVC4::SmtEngine* d_smt; CVC4::parser::Parser* d_parserContext; std::vector d_exprTypeMapRemove; + unsigned d_stackLevel; friend class Type; // to reach in to d_exprTypeMapRemove -- 2.30.2