fix some Java compatibility-layer interface problems; also fix some Mac OS X build issues

2 files changed, 86 insertions, 6 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 83c33c7ab..16169c10a 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -225,6 +225,10 @@ Expr::Expr(const Expr& e) : CVC4::Expr(e) {
 Expr::Expr(const CVC4::Expr& e) : CVC4::Expr(e) {
 }
 
+Expr::Expr(const CVC4::Kind k) : CVC4::Expr() {
+  *this = getEM()->operatorOf(k);
+}
+
 Expr Expr::eqExpr(const Expr& right) const {
   return getEM()->mkExpr(CVC4::kind::EQUAL, *this, right);
 }
@@ -321,6 +325,22 @@ bool Expr::isString() const {
   return false;
 }
 
+bool Expr::isBoundVar() const {
+  Unimplemented();
+}
+
+bool Expr::isLambda() const {
+  Unimplemented();
+}
+
+bool Expr::isClosure() const {
+  Unimplemented();
+}
+
+bool Expr::isQuantifier() const {
+  Unimplemented();
+}
+
 bool Expr::isApply() const {
   return hasOperator();
 }
@@ -404,7 +424,7 @@ std::vector< std::vector<Expr> > Expr::getTriggers() const {
 }
 
 ExprManager* Expr::getEM() const {
-  return getExprManager();
+  return reinterpret_cast<ExprManager*>(getExprManager());
 }
 
 std::vector<Expr> Expr::getKids() const {
@@ -709,7 +729,7 @@ ValidityChecker::ValidityChecker() :
   d_clflags(new CLFlags()),
   d_options() {
   setUpOptions(d_options, *d_clflags);
-  d_em = new CVC4::ExprManager(d_options);
+  d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options));
   d_smt = new CVC4::SmtEngine(d_em);
   d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
 }
@@ -718,7 +738,7 @@ ValidityChecker::ValidityChecker(const CLFlags& clflags) :
   d_clflags(new CLFlags(clflags)),
   d_options() {
   setUpOptions(d_options, *d_clflags);
-  d_em = new CVC4::ExprManager(d_options);
+  d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options));
   d_smt = new CVC4::SmtEngine(d_em);
   d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
 }
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index beef53006..eae8412cf 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -82,6 +82,20 @@
 
 namespace CVC3 {
 
+const CVC4::Kind EQ = CVC4::kind::EQUAL;
+const CVC4::Kind LE = CVC4::kind::LEQ;
+const CVC4::Kind GE = CVC4::kind::GEQ;
+const CVC4::Kind DIVIDE = CVC4::kind::DIVISION;
+const CVC4::Kind BVLT = CVC4::kind::BITVECTOR_ULT;
+const CVC4::Kind BVLE = CVC4::kind::BITVECTOR_ULE;
+const CVC4::Kind BVGT = CVC4::kind::BITVECTOR_UGT;
+const CVC4::Kind BVGE = CVC4::kind::BITVECTOR_UGE;
+const CVC4::Kind BVPLUS = CVC4::kind::BITVECTOR_PLUS;
+const CVC4::Kind BVSUB = CVC4::kind::BITVECTOR_SUB;
+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);
 
 //! Different types of command line flags
@@ -227,10 +241,11 @@ public:
 
 };/* class CLFlags */
 
+class ExprManager;
 class Context;
 class Proof {};
+class Theorem {};
 
-using CVC4::ExprManager;
 using CVC4::InputLanguage;
 using CVC4::Integer;
 using CVC4::Rational;
@@ -318,6 +333,7 @@ public:
   Expr();
   Expr(const Expr& e);
   Expr(const CVC4::Expr& e);
+  Expr(CVC4::Kind k);
 
   // Compound expression constructors
   Expr eqExpr(const Expr& right) const;
@@ -348,12 +364,40 @@ public:
   bool isTrue() const;
   bool isBoolConst() const;
   bool isVar() const;
+  bool isBoundVar() const;
   bool isString() const;
+  bool isSymbol() const;
+  bool isTerm() const;
+  bool isType() const;
+  bool isClosure() const;
+  bool isQuantifier() const;
+  bool isForall() const;
+  bool isExists() const;
+  bool isLambda() const;
   bool isApply() const;
   bool isTheorem() const;
   bool isConstant() const;
   bool isRawList() const;
 
+  bool isAtomic() const;
+  bool isAtomicFormula() const;
+  bool isAbsAtomicFormula() const;
+  bool isLiteral() const;
+  bool isAbsLiteral() const;
+  bool isBoolConnective() const;
+  bool isPropLiteral() const;
+  bool isPropAtom() const;
+
+  const std::string& getName() const;
+  const std::string& getUid() const;
+
+  const std::string& getString() const;
+  const std::vector<Expr>& getVars() const;
+  const Expr& getExistential() const;
+  int getBoundIndex() const;
+  const Expr& getBody() const;
+  const Theorem& getTheorem() const;
+
   bool isEq() const;
   bool isNot() const;
   bool isAnd() const;
@@ -366,7 +410,7 @@ public:
   bool isRational() const;
   bool isSkolem() const;
 
-  Rational getRational() const;
+  const Rational& getRational() const;
 
   Op mkOp() const;
   Op getOp() const;
@@ -407,8 +451,24 @@ public:
   //! Look up the current type. Do not recursively compute (i.e. may be NULL)
   Type lookupType() const;
 
+  //! Pretty-print the expression
+  void pprint() const;
+  //! Pretty-print without dagifying
+  void pprintnodag() const;
+
 };/* class CVC3::Expr */
 
+bool isArrayLiteral(const Expr&);
+
+class ExprManager : public CVC4::ExprManager {
+public:
+  const std::string& getKindName(int kind);
+  //! Get the input language for printing
+  InputLanguage getInputLang() const;
+  //! Get the output language for printing
+  InputLanguage getOutputLang() const;
+};/* class CVC3::ExprManager */
+
 typedef CVC4::StatisticsRegistry Statistics;
 
 #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4
@@ -464,7 +524,7 @@ class CVC4_PUBLIC ValidityChecker {
 
   CLFlags* d_clflags;
   CVC4::Options d_options;
-  CVC4::ExprManager* d_em;
+  CVC3::ExprManager* d_em;
   CVC4::SmtEngine* d_smt;
   CVC4::parser::Parser* d_parserContext;