cvc3 compatibility layer; and another libantlr3c v3.4 incompatibility fix

10 files changed, 98 insertions, 45 deletions

diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index e35ec5e67..e14527ede 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -136,7 +136,7 @@ python.lo: python.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $<
 python.cpp:
 ocaml.cpp:
-python.lo: ruby.cpp
+ruby.lo: ruby.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $<
 ruby.cpp:
 tcl.cpp:
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 955f3a1f4..96c0933d8 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -596,10 +596,10 @@ mainCommand[CVC4::Command*& cmd]
     { cmd = new SetOptionCommand(s, sexpr); }
 
     /* push / pop */
-  | PUSH_TOK k=numeral?
-    { cmd = REPEAT_COMMAND(k, PushCommand()); }
-  | POP_TOK k=numeral?
-    { cmd = REPEAT_COMMAND(k, PopCommand()); }
+  | PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); }
+               | { cmd = new PushCommand(); } )
+  | POP_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PopCommand()); }
+              | { cmd = new PopCommand(); } )
   | POPTO_TOK k=numeral?
     { UNSUPPORTED("POPTO command"); }
 
diff --git a/src/parser/parser.i b/src/parser/parser.i
index dd52bfcda..5e10973d4 100644
--- a/src/parser/parser.i
+++ b/src/parser/parser.i
@@ -12,8 +12,8 @@ namespace CVC4 {
   class ParserExprStream : public CVC4::ExprStream {
     Parser* d_parser;
   public:
-    ExprStream(Parser* parser) : d_parser(parser) {}
-    ~ExprStream() { delete d_parser; }
+    ParserExprStream(Parser* parser) : d_parser(parser) {}
+    ~ParserExprStream() { delete d_parser; }
     Expr nextExpr() { return d_parser->nextExpression(); }
   };/* class Parser::ExprStream */
 
diff --git a/src/util/cardinality.i b/src/util/cardinality.i
index 760f746c0..82f67382b 100644
--- a/src/util/cardinality.i
+++ b/src/util/cardinality.i
@@ -20,4 +20,32 @@
 %ignore CVC4::operator<<(std::ostream&, const Cardinality&);
 %ignore CVC4::operator<<(std::ostream&, Cardinality::Beth);
 
+  class Beth {
+    Integer d_index;
+
+  public:
+    Beth(const Integer& beth) : d_index(beth) {
+      CheckArgument(beth >= 0, beth,
+                    "Beth index must be a nonnegative integer, not %s.",
+                    beth.toString().c_str());
+    }
+
+    const Integer& getNumber() const throw() {
+      return d_index;
+    }
+  };/* class Cardinality::Beth */
+
+  class Unknown {
+  public:
+    Unknown() throw() {}
+    ~Unknown() throw() {}
+  };/* class Cardinality::Unknown */
+
 %include "util/cardinality.h"
+
+%{
+namespace CVC4 {
+  typedef CVC4::Cardinality::Beth Beth;
+  typedef CVC4::Cardinality::Unknown Unknown;
+}
+%}
diff --git a/src/util/datatype.i b/src/util/datatype.i
index b62033e17..fe696029d 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -1,8 +1,5 @@
 %{
 #include "util/datatype.h"
-namespace CVC4 {
-//typedef CVC4::Datatype::Constructor DatatypeConstructor;
-}
 %}
 
 namespace CVC4 {
@@ -33,6 +30,11 @@ namespace CVC4 {
 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const;
 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const;
 
+%rename(beginConst) CVC4::Constructor::begin() const;
+%rename(endConst) CVC4::Constructor::end() const;
+
+%rename(getArg) CVC4::Constructor::operator[](size_t) const;
+
 %ignore CVC4::operator<<(std::ostream&, const Datatype&);
 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
@@ -226,7 +228,6 @@ namespace CVC4 {
     const Arg& operator[](size_t index) const;
 
   };/* class Datatype::Constructor */
-}
 
   class SelfType {
   };/* class Datatype::SelfType */
@@ -245,6 +246,7 @@ namespace CVC4 {
     inline UnresolvedType(std::string name);
     inline std::string getName() const throw();
   };/* class Datatype::UnresolvedType */
+}
 
 %{
 namespace CVC4 {
diff --git a/src/util/integer.i b/src/util/integer.i
index 4aaa532a7..bad6b196f 100644
--- a/src/util/integer.i
+++ b/src/util/integer.i
@@ -4,6 +4,7 @@
 
 %ignore CVC4::Integer::Integer(int);
 %ignore CVC4::Integer::Integer(unsigned int);
+%ignore CVC4::Integer::Integer(const std::string&);
 
 %rename(assign) CVC4::Integer::operator=(const Integer&);
 %rename(equals) CVC4::Integer::operator==(const Integer&) const;
diff --git a/src/util/output.i b/src/util/output.i
index 10653c2f8..b9c0e32ee 100644
--- a/src/util/output.i
+++ b/src/util/output.i
@@ -11,4 +11,22 @@
 %ignore CVC4::null_os;
 %ignore CVC4::DumpC::dump_cout;
 
+%ignore operator<<;
+%ignore on(std::string);
+%ignore isOn(std::string);
+%ignore off(std::string);
+%ignore printf(std::string, const char*, ...);
+%ignore operator()(std::string);
+
+%ignore CVC4::ScopedDebug::ScopedDebug(std::string);
+%ignore CVC4::ScopedDebug::ScopedDebug(std::string, bool);
+
+%ignore CVC4::ScopedTrace::ScopedTrace(std::string);
+%ignore CVC4::ScopedTrace::ScopedTrace(std::string, bool);
+
+%rename(getostream) operator std::ostream&;
+%rename(getCVC4ostream) operator CVC4ostream;
+%rename(get) operator();
+%rename(ok) operator bool;
+
 %include "util/output.h"
diff --git a/src/util/rational.i b/src/util/rational.i
index 512d3ea50..135302c66 100644
--- a/src/util/rational.i
+++ b/src/util/rational.i
@@ -6,6 +6,7 @@
 %ignore CVC4::Rational::Rational(unsigned int);
 %ignore CVC4::Rational::Rational(int, int);
 %ignore CVC4::Rational::Rational(unsigned int, unsigned int);
+%ignore CVC4::Rational::Rational(const std::string&);
 
 %rename(assign) CVC4::Rational::operator=(const Rational&);
 %rename(equals) CVC4::Rational::operator==(const Rational&) const;
diff --git a/src/util/stats.h b/src/util/stats.h
index 3a2847512..e955a7d28 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -45,8 +45,6 @@ class ExprManager;
 
 class CVC4_PUBLIC Stat;
 
-inline std::ostream& operator<<(std::ostream& os, const timespec& t);
-
 /**
  * The main statistics registry.  This registry maintains the list of
  * currently active statistics and is able to "flush" them all.
@@ -643,12 +641,14 @@ inline bool operator>=(const timespec& a, const timespec& b) {
 }
 
 /** Output a timespec on an output stream. */
+inline std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& os, const timespec& t) {
   // assumes t.tv_nsec is in range
   return os << t.tv_sec << "."
             << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec;
 }
 
+class CVC4_PUBLIC CodeTimer;
 
 /**
  * A timer statistic.  The timer can be started and stopped
@@ -666,27 +666,7 @@ class CVC4_PUBLIC TimerStat : public BackedStat< timespec > {
 
 public:
 
-  /**
-   * Utility class to make it easier to call stop() at the end of a
-   * code block.  When constructed, it starts the timer.  When
-   * destructed, it stops the timer.
-   */
-  class CodeTimer {
-    TimerStat& d_timer;
-
-    /** Private copy constructor undefined (no copy permitted). */
-    CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED;
-    /** Private assignment operator undefined (no copy permitted). */
-    CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED;
-
-  public:
-    CodeTimer(TimerStat& timer) : d_timer(timer) {
-      d_timer.start();
-    }
-    ~CodeTimer() {
-      d_timer.stop();
-    }
-  };/* class TimerStat::CodeTimer */
+  typedef CVC4::CodeTimer CodeTimer;
 
   /**
    * Construct a timer statistic with the given name.  Newly-constructed
@@ -713,6 +693,29 @@ public:
 
 
 /**
+ * Utility class to make it easier to call stop() at the end of a
+ * code block.  When constructed, it starts the timer.  When
+ * destructed, it stops the timer.
+ */
+class CVC4_PUBLIC CodeTimer {
+  TimerStat& d_timer;
+
+  /** Private copy constructor undefined (no copy permitted). */
+  CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED;
+  /** Private assignment operator undefined (no copy permitted). */
+  CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED;
+
+public:
+  CodeTimer(TimerStat& timer) : d_timer(timer) {
+    d_timer.start();
+  }
+  ~CodeTimer() {
+    d_timer.stop();
+  }
+};/* class CodeTimer */
+
+
+/**
  * To use a statistic, you need to declare it, initialize it in your
  * constructor, register it in your constructor, and deregister it in
  * your destructor.  Instead, this macro does it all for you (and
diff --git a/src/util/stats.i b/src/util/stats.i
index 48828cb7e..5d3b81d4d 100644
--- a/src/util/stats.i
+++ b/src/util/stats.i
@@ -2,20 +2,20 @@
 #include "util/stats.h"
 %}
 
-%ignore CVC4::operator<<(std::ostream&, const ::timespec&);
+%ignore CVC4::operator<<(std::ostream&, const timespec&);
 
 %rename(increment) CVC4::IntStat::operator++();
 %rename(plusAssign) CVC4::IntStat::operator+=(int64_t);
 
-%rename(plusAssign) CVC4::operator+=(::timespec&, const ::timespec&);
-%rename(minusAssign) CVC4::operator-=(::timespec&, const ::timespec&);
-%rename(plus) CVC4::operator+(const ::timespec&, const ::timespec&);
-%rename(minus) CVC4::operator-(const ::timespec&, const ::timespec&);
-%rename(equals) CVC4::operator==(const ::timespec&, const ::timespec&);
-%ignore CVC4::operator!=(const ::timespec&, const ::timespec&);
-%rename(less) CVC4::operator<(const ::timespec&, const ::timespec&);
-%rename(lessEqual) CVC4::operator<=(const ::timespec&, const ::timespec&);
-%rename(greater) CVC4::operator>(const ::timespec&, const ::timespec&);
-%rename(greaterEqual) CVC4::operator>=(const ::timespec&, const ::timespec&);
+%rename(plusAssign) CVC4::operator+=(timespec&, const timespec&);
+%rename(minusAssign) CVC4::operator-=(timespec&, const timespec&);
+%rename(plus) CVC4::operator+(const timespec&, const timespec&);
+%rename(minus) CVC4::operator-(const timespec&, const timespec&);
+%rename(equals) CVC4::operator==(const timespec&, const timespec&);
+%ignore CVC4::operator!=(const timespec&, const timespec&);
+%rename(less) CVC4::operator<(const timespec&, const timespec&);
+%rename(lessEqual) CVC4::operator<=(const timespec&, const timespec&);
+%rename(greater) CVC4::operator>(const timespec&, const timespec&);
+%rename(greaterEqual) CVC4::operator>=(const timespec&, const timespec&);
 
 %include "util/stats.h"