Lemmas on demand work, push-pop, some cleanup.

9 files changed, 26 insertions, 119 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index af3457550..837837cd6 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -12,8 +12,6 @@ libutil_la_SOURCES = \
 	Makefile.in \
 	congruence_closure.h \
 	debug.h \
-	decision_engine.cpp \
-	decision_engine.h \
 	exception.h \
 	hash.h \
 	bool.h \
@@ -29,7 +27,6 @@ libutil_la_SOURCES = \
 	rational.h \
 	integer.h \
 	bitvector.h \
-	bitvector.cpp \
 	gmp_util.h \
 	sexpr.h \
 	stats.h \
@@ -44,12 +41,10 @@ BUILT_SOURCES = \
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \
-	integer_cln_imp.cpp \
 	rational_cln_imp.cpp
 endif
 if CVC4_GMP_IMP
 libutil_la_SOURCES += \
-	integer_gmp_imp.cpp \
 	rational_gmp_imp.cpp
 endif
 
@@ -57,11 +52,9 @@ EXTRA_DIST = \
 	rational_cln_imp.h \
 	integer_cln_imp.h \
 	rational_cln_imp.cpp \
-	integer_cln_imp.cpp \
 	rational_gmp_imp.h \
 	integer_gmp_imp.h \
 	rational_gmp_imp.cpp \
-	integer_gmp_imp.cpp \
 	rational.h.in \
 	integer.h.in \
 	tls.h.in
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
deleted file mode 100644
index 8ea95e1c9..000000000
--- a/src/util/bitvector.cpp
+++ /dev/null
@@ -1,32 +0,0 @@
-/*********************                                                        */
-/*! \file bitvector.cpp
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): taking
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "bitvector.h"
-
-namespace CVC4 {
-
-std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
-  return os << bv.toString();
-}
-
-std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
-  return os << "[" << bv.high << ":" << bv.low << "]";
-}
-
-}/* CVC4 namespace */
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index edf4e987d..51239cbbb 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -245,8 +245,13 @@ struct UnsignedHashStrategy {
   }
 };
 
-std::ostream& operator <<(std::ostream& os, const BitVector& bv);
-std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv);
+inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
+  return os << bv.toString();
+}
+
+inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
+  return os << "[" << bv.high << ":" << bv.low << "]";
+}
 
 }/* CVC4 namespace */
 
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
deleted file mode 100644
index 692520257..000000000
--- a/src/util/integer_cln_imp.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                                        */
-/*! \file integer_cln_imp.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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 A multiprecision rational constant.
- **
- ** A multiprecision rational constant.
- ** This stores the rational as a pair of multiprecision integers,
- ** one for the numerator and one for the denominator.
- ** The number is always stored so that the gcd of the numerator and denominator
- ** is 1.  (This is referred to as referred to as canonical form in GMP's
- ** literature.) A consquence is that that the numerator and denominator may be
- ** different than the values used to construct the Rational.
- **/
-
-#include "cvc4autoconfig.h"
-#include "util/integer.h"
-
-#ifndef CVC4_CLN_IMP
-#  error "This source should only ever be built if CVC4_CLN_IMP is on !"
-#endif /* CVC4_CLN_IMP */
-
-using namespace CVC4;
-
-std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
-  return os << n.toString();
-}
-
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index ee256867a..21f6c7581 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -228,7 +228,9 @@ struct IntegerHashStrategy {
   }
 };/* struct IntegerHashStrategy */
 
-std::ostream& operator<<(std::ostream& os, const Integer& n);
+inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
+  return os << n.toString();
+}
 
 }/* CVC4 namespace */
 
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
deleted file mode 100644
index 1c2bd7ccd..000000000
--- a/src/util/integer_gmp_imp.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                                        */
-/*! \file integer_gmp_imp.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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 A multiprecision rational constant.
- **
- ** A multiprecision rational constant.
- ** This stores the rational as a pair of multiprecision integers,
- ** one for the numerator and one for the denominator.
- ** The number is always stored so that the gcd of the numerator and denominator
- ** is 1.  (This is referred to as referred to as canonical form in GMP's
- ** literature.) A consquence is that that the numerator and denominator may be
- ** different than the values used to construct the Rational.
- **/
-
-#include "cvc4autoconfig.h"
-#include "util/integer.h"
-
-#ifndef CVC4_GMP_IMP
-#  error "This source should only ever be built if CVC4_GMP_IMP is on !"
-#endif /* CVC4_GMP_IMP */
-
-using namespace CVC4;
-
-std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
-  return os << n.toString();
-}
-
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 44f460559..72a653545 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -164,7 +164,9 @@ struct IntegerHashStrategy {
   }
 };/* struct IntegerHashStrategy */
 
-std::ostream& operator<<(std::ostream& os, const Integer& n);
+inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
+  return os << n.toString();
+}
 
 }/* CVC4 namespace */
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index dbfed887d..8f26d9376 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -66,7 +66,8 @@ static const string optionsDescription = "\
    --no-interactive       do not run interactively\n\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
-   --lazy-definition-expansion expand define-fun lazily\n";
+   --lazy-definition-expansion expand define-fun lazily\n\
+   --incremental          enable incremental solving\n";
 
 static const string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
@@ -119,6 +120,7 @@ enum OptionValue {
   NO_TYPE_CHECKING,
   LAZY_TYPE_CHECKING,
   EAGER_TYPE_CHECKING,
+  INCREMENTAL
 };/* enum OptionValue */
 
 /**
@@ -174,6 +176,7 @@ static struct option cmdlineOptions[] = {
   { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING},
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING},
   { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
+  { "incremental", no_argument, NULL, INCREMENTAL},
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -367,6 +370,10 @@ throw(OptionException) {
       earlyTypeChecking = true;
       break;
 
+    case INCREMENTAL:
+      incrementalSolving = true;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/util/options.h b/src/util/options.h
index 60c8f2a1a..1eca0d499 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -126,6 +126,9 @@ struct CVC4_PUBLIC Options {
   /** Whether we do typechecking at Expr creation time. */
   bool earlyTypeChecking;
 
+  /** Whether incemental solving (push/pop) */
+  bool incrementalSolving;
+
   Options() :
     binary_name(),
     statistics(false),
@@ -147,7 +150,8 @@ struct CVC4_PUBLIC Options {
     produceModels(false),
     produceAssignments(false),
     typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
-    earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
+    earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
+    incrementalSolving(false) {
   }
 
   /**