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

diff --git a/NEWS b/NEWS
index 9d4b5452d63244dece04b6ed51d86f05e1cafdc9..e792564baec0f6e0c0dae718559ee2649090e7aa 100644 (file)
--- 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 b8127592fecbeca2003b2db186f1c1f10088ef55..33bdb51285ef3667e31416b7211e1265cf9e4010 100644 (file)
--- 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 4aa210a508e7f894a171ed27c563d1c748c0d43f..20cbd82d905b2685634d7ff3411fd701c9d20b5b 100755 (executable)
--- 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 4811a4bbe04afd0692823e3f3607e569ee3fff9a..f7ce15f6c7bd6c63c34a9bec150dd17c9e5b86c7 100755 (executable)
--- 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 657c13cd8be9aaf908256ed1ac74c21979104f53..f5f3daef78a85689c4387b3a93b65b959ef3d837 100644 (file)
--- 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 4d9cbc60d863ef8cf8458ea01c097336b4c2e888..b436bad7c7c7e296a5804db343dd1afcc41d11e8 100644 (file)
--- 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 0527b7f1af7ed5f5fc57a7d46c379f2af3960a17..bb26feef3080168b49861c786cf46198584d5110 100644 (file)
--- 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 2b909a9a917e275ffe32f8ccc832e028b5d233e6..d4448787fa35c9456fd49882aa793d6f345828c8 100644 (file)
--- 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 499d362a96c72c0b52c1c71160927586ccd6d156..ec4b223cff4b1bc4d03440faa4b8b7f598b9c6e0 100644 (file)
--- 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 2ea92635eb22c1825d28b73b96eba470f31a7a1c..ca22f29b6b4235d26ad09b9851bc4c8f7073ef1e 100644 (file)
--- 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 0b4f2654b7fdeaefe6b39e8a7950e6de00d24c6f..187587227ad45c9655e35c1bac91568899420236 100644 (file)
--- 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 6bfea5c44931232561501c0d197ab7fd5c38146f..e232a382ede6064dc8712c211b911d6bda7aabf1 100644 (file)
--- 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 45f161143e0444c63e6e17d9339b6517ae725013..016abb2ac69addebae58b674ff899e1fc5d53e94 100644 (file)
--- 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 2373c7f9aace3f3981331b09e0c709e76c920635..34cb2443f94d4c88e29059dbf01efcf1007075a4 100644 (file)
--- 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 f993b941b75a05fa7998059beefb0cab6a60d8f9..9caa8b1f12a9912e427960544aede2058d1b892b 100644 (file)
--- 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 85d49f9210a6a0b7125c4816f20b7cca48d50172..9a78780664050710fc0504d1778b9488d5e3bade 100644 (file)
--- 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 (file)
index c1f65e5..0000000
--- 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)