Merging some cleanup work:

* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed

17 files changed, 42 insertions, 53 deletions

diff --git a/NEWS b/NEWS
index 9d4b5452d..e792564ba 100644
--- a/NEWS
+++ b/NEWS
@@ -6,15 +6,16 @@ Changes since 1.0
 * tuple and record support in the compatibility library
 * user patterns are now supported in the SMT-LIBv1.2 parser
 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
-* Win32 support via mingw
+* Win32-building support via mingw
 * for printing commands as they're invoked from the driver, you now need
   verbosity of 3 or higher (e.g. -vvv) instead of verbosity 1 or higher (-v).
   This allows tracing the solver's activities without having too much output.
-* multiline support in interactive mode
+* multiline input support in interactive mode
 * To make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
   use -q.  Previously, this would silence all output (including "sat" or
   "unsat") as well.  Now, single -q silences messages and warnings, and
   double -qq silences all output (except on exception or signal).
 * Boolean term support in datatypes
+* numerous bug fixes, usability improvements, and build system improvements
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 20 Mar 2013 20:03:50 -0400
+-- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 26 Mar 2013 15:17:52 -0400
diff --git a/configure.ac b/configure.ac
index b8127592f..33bdb5128 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1179,7 +1179,7 @@ AC_SUBST(MAN_DATE)
 AC_CONFIG_FILES([
   Makefile.builds
   Makefile]
-  m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^src/prop/cryptominisat/' | sort | sed 's,\.am$,,'])
+  m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | sort | sed 's,\.am$,,'])
 )
 
 if test $cvc4_has_threads = yes; then
@@ -1206,8 +1206,6 @@ CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
 
-# AC_CONFIG_SUBDIRS([src/prop/cryptominisat])
-
 AC_OUTPUT
 
 # Final information to the user
diff --git a/contrib/spellcheck b/contrib/spellcheck
index 4aa210a50..20cbd82d9 100755
--- a/contrib/spellcheck
+++ b/contrib/spellcheck
@@ -2,7 +2,7 @@
 
 dir="$(dirname "$0")"
 
-find src \( -name '*.cpp' -o -name '*.h' \) \! -path 'src/prop/minisat/*' \! -path 'src/prop/bvminisat/*' \! -path 'src/prop/cryptominisat/*' \! -path 'src/parser/*/generated/*' |
+find src \( -name '*.cpp' -o -name '*.h' \) \! -path 'src/prop/minisat/*' \! -path 'src/prop/bvminisat/*' \! -path 'src/parser/*/generated/*' |
   while read f; do
     misspelled_words=`
     $dir/extract-strings-and-comments $f |
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 4811a4bbe..f7ce15f6c 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -34,7 +34,7 @@
 # the license.)
 #
 
-my $excluded_directories = '^(minisat|bvminisat|cryptominisat|CVS|generated)$';
+my $excluded_directories = '^(minisat|bvminisat|CVS|generated)$';
 my $excluded_paths = '^(src/parser/antlr_input_imports.cpp|src/bindings/compat/.*)$';
 
 # Years of copyright for the template.  E.g., the string
diff --git a/library_versions b/library_versions
index 657c13cd8..f5f3daef7 100644
--- a/library_versions
+++ b/library_versions
@@ -47,3 +47,4 @@
 1\.0 libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0
 1\.0\.1-prerelease libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0
 1\.1-prerelease libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0
+1\.1 libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 4d9cbc60d..b436bad7c 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -45,7 +45,7 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
 
 ${typerules}
 
-#line 46 "${template}"
+#line 49 "${template}"
 
   default:
     Debug("getType") << "FAILURE" << std::endl;
@@ -68,7 +68,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
   switch(n.getKind()) {
 ${construles}
 
-#line 69 "${template}"
+#line 72 "${template}"
 
   default:;
   }
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index 0527b7f1a..bb26feef3 100644
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -34,7 +34,7 @@ namespace main {
 
 class CommandExecutorPortfolio : public CommandExecutor {
 
-  // These shall be created/deleted during initalization
+  // These shall be created/deleted during initialization
   std::vector<ExprManager*> d_exprMgrs;
   const unsigned d_numThreads;   // Currently const, but designed so it is
                                  // not too hard to support this changing
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2b909a9a9..d4448787f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -254,7 +254,7 @@ class SmtEnginePrivate : public NodeManagerListener {
    * A map of AbsractValues to their actual constants.  Only used if
    * options::abstractValues() is on.
    */
-  theory::SubstitutionMap d_abstractValueMap;
+  SubstitutionMap d_abstractValueMap;
 
   /**
    * A mapping of all abstract values (actual value |-> abstract) that
@@ -489,7 +489,7 @@ public:
 
   /**
    * Return the uinterpreted function symbol corresponding to division-by-zero
-   * for this particular bit-wdith
+   * for this particular bit-width
    * @param k should be UREM or UDIV
    * @param width
    *
@@ -695,7 +695,7 @@ void SmtEngine::finalOptionsAreSet() {
     setLogicInternal();
   }
 
-  // finish initalization, creat the prop engine, etc.
+  // finish initialization, create the prop engine, etc.
   finishInit();
 
   AlwaysAssert( d_propEngine->getAssertionLevel() == 0,
@@ -815,11 +815,11 @@ void SmtEngine::setLogicInternal() throw() {
   d_logic.lock();
 
   // may need to force uninterpreted functions to be on for non-linear
-  if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) ||
-      d_logic.isTheoryEnabled(theory::THEORY_BV)) &&
-     !d_logic.isTheoryEnabled(theory::THEORY_UF)){
+  if(((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ||
+      d_logic.isTheoryEnabled(THEORY_BV)) &&
+     !d_logic.isTheoryEnabled(THEORY_UF)){
     d_logic = d_logic.getUnlockedCopy();
-    d_logic.enableTheory(theory::THEORY_UF);
+    d_logic.enableTheory(THEORY_UF);
     d_logic.lock();
   }
 
@@ -1030,7 +1030,7 @@ void SmtEngine::setLogicInternal() throw() {
   }
 
   // Non-linear arithmetic does not support models
-  if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+  if (d_logic.isTheoryEnabled(THEORY_ARITH) &&
       !d_logic.isLinear()) {
     if (options::produceModels()) {
       Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl;
@@ -1042,8 +1042,8 @@ void SmtEngine::setLogicInternal() throw() {
     }
   }
 
-  //datatypes theory should assign values to all datatypes terms if logic is quantified
-  if (d_logic.isQuantified() && d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+  // datatypes theory should assign values to all datatypes terms if logic is quantified
+  if (d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
     if( !options::dtForceAssignment.wasSetByUser() ){
       options::dtForceAssignment.set(true);
     }
@@ -1800,7 +1800,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     for( SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin(); pos != d_topLevelSubstitutions.end(); ++pos) {
       Node n = (*pos).first;
       Node v = (*pos).second;
-      Trace("model") << "Add substitution : " << n << " " << v << std::endl;
+      Trace("model") << "Add substitution : " << n << " " << v << endl;
       m->addSubstitution( n, v );
     }
   }
@@ -2395,7 +2395,7 @@ bool SmtEnginePrivate::simplifyAssertions()
           // miplib rewrites aren't safe in incremental mode
           ! options::incrementalSolving() &&
           // only useful in arith
-          d_smt.d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+          d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
           // we add new assertions and need this (in practice, this
           // restriction only disables miplib processing during
           // re-simplification, which we don't expect to be useful anyway)
@@ -2654,16 +2654,16 @@ void SmtEnginePrivate::processAssertions() {
         switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
         case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
         case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
-          if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) {
+          if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) {
             d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-            d_smt.d_logic.enableTheory(theory::THEORY_BV);
+            d_smt.d_logic.enableTheory(THEORY_BV);
             d_smt.d_logic.lock();
           }
           break;
         case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
-          if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+          if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
             d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-            d_smt.d_logic.enableTheory(theory::THEORY_DATATYPES);
+            d_smt.d_logic.enableTheory(THEORY_DATATYPES);
             d_smt.d_logic.lock();
           }
           break;
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index 499d362a9..ec4b223cf 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -30,7 +30,7 @@ const ReasonId CVC4::theory::bv::AxiomReasonId = -2;
 
 
 bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
-  Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; 
+  Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; 
 
   TermId id_a = registerTerm(a);
   TermId id_b = registerTerm(b);
@@ -121,7 +121,7 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
   while (!queue.empty()) {
     TermId current = queue.top();
     queue.pop();
-    Debug("bv-inequality-internal") << "InequalityGraph::processQueue proceessing " << getTermNode(current) << "\n";
+    Debug("bv-inequality-internal") << "InequalityGraph::processQueue processing " << getTermNode(current) << "\n";
   
     BitVector current_value = getValue(current);
   
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 2ea92635e..ca22f29b6 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -208,12 +208,13 @@ public:
    */
   virtual void spendResource() throw() {}
 
-  /** Handle user attribute
-    *   Associates theory t with the attribute attr.  Theory t will be
-    *   notifed whenever an attribute of name attr is set on a node.
-    *   This can happen through, for example, the SMT LIB v2 language.
-    */
-  virtual void handleUserAttribute( const char* attr, Theory* t ){}
+  /**
+   * Handle user attribute.
+   * Associates theory t with the attribute attr.  Theory t will be
+   * notified whenever an attribute of name attr is set on a node.
+   * This can happen through, for example, the SMT-LIBv2 language.
+   */
+  virtual void handleUserAttribute(const char* attr, Theory* t) {}
 
 };/* class OutputChannel */
 
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 0b4f2654b..187587227 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -31,7 +31,7 @@ namespace theory {
 class QuantRelevance
 {
 private:
-  /** for computing relavance */
+  /** for computing relevance */
   bool d_computeRel;
   /** map from quantifiers to symbols they contain */
   std::map< Node, std::vector< Node > > d_syms;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 6bfea5c44..e232a382e 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -212,7 +212,7 @@ private:
   std::map< TNode, std::vector< TNode > > d_var_contains;
   /** triggers for each operator */
   std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
-  /** helper for is intance of */
+  /** helper for is instance of */
   bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
 public:
   /** compute var contains */
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 45f161143..016abb2ac 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -291,7 +291,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
       d_subtermsToEvaluate[result] = t.getNumChildren();
       for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
 	if (isConstant(getNodeId(t[i]))) {
-	  Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluatates " << t[i] << std::endl;
+	  Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl;
 	  subtermEvaluates(result);
 	}
       }
@@ -390,7 +390,7 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) {
 }
 
 void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) {
-  Debug("equality") << d_name << "::eq::mergePredicats(" << p << "," << q << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::mergePredicates(" << p << "," << q << ")" << std::endl;
   assertEqualityInternal(p, q, reason);
   propagate();
 }
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 2373c7f9a..34cb2443f 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -727,7 +727,7 @@ public:
   }
 
   /**
-   * Returns true if this kind is used for congruencce closure + evaluation of constants.
+   * Returns true if this kind is used for congruence closure + evaluation of constants.
    */
   bool isInterpretedFunctionKind(Kind fun) const {
     return d_congruenceKindsInterpreted.tst(fun);
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index f993b941b..9caa8b1f1 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -282,7 +282,7 @@ enum FunctionApplicationType {
 struct FunctionApplication {
   /** Type of application */
   FunctionApplicationType type;
-  /** The actuall application elements */
+  /** The actual application elements */
   EqualityNodeId a, b;
 
   /** Construct an application */
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 85d49f921..9a7878066 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -174,10 +174,6 @@ public:
   /** 
    * Returns the Integer obtained by setting the ith bit of the
    * current Integer to 1. 
-   * 
-   * @param bit 
-   * 
-   * @return 
    */
   Integer setBit(uint32_t i) const {
     mpz_class res = d_value;
diff --git a/test/regress/regress0/simple.smt2 b/test/regress/regress0/simple.smt2
deleted file mode 100644
index c1f65e565..000000000
--- a/test/regress/regress0/simple.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-(set-info :source "contrived")
-(set-info :smt-lib-version 2.0)
-(set-info :category "check")
-(set-info :status unsat)
-(set-logic QF_UF)
-(set-info :notes |This benchmark simply checks that SMT-LIB v2 can be parsed.|)
-(set-info :difficulty 0.000)
-(exit)