fixes to the compatibility layer; this fixes the broken system test

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<ExprManager*>(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<ExprManager*>(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<string, bool>
 } 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<std::string, CLFlag> 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 T>
-class ExprMap : public std::map<Expr, T> {
+class CVC4_PUBLIC ExprMap : public std::map<Expr, T> {
 };/* class ExprMap<T> */
 
 template <class T>
-class ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> {
+class CVC4_PUBLIC ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> {
 public:
   void insert(Expr a, Expr b);
 };/* class ExprHashMap<T> */
 
-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<Expr> d_exprTypeMapRemove;
+  unsigned d_stackLevel;
 
   friend class Type; // to reach in to d_exprTypeMapRemove