Some cleanup and copyright updating

* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles

diff --git a/COPYING b/COPYING
index 5016b3fbd82848de7921c9508add7d22a7d24e1d..38196791a05179705c892c796853ea42ece6587d 100644 (file)
--- a/COPYING
+++ b/COPYING
@@ -1,5 +1,5 @@
-CVC4 is copyright (C) 2009, 2010, 2011, 2012 New York University and
-The University of Iowa.  All rights reserved.
+CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013 New York University
+and The University of Iowa.  All rights reserved.
 
 CVC4 is open-source; distribution is under the terms of the modified BSD
 license.  However, certain builds of CVC4 link against GPLed libraries,
@@ -19,7 +19,7 @@ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Fri, 04 Feb 2011 14:56:41 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  Mon, 28 Jan 2013 17:22:36 -0500
 
 CVC4 incorporates MiniSat code, excluded from the above copyright.
 See src/sat/minisat.  Its copyright:

diff --git a/contrib/configure-in-place b/contrib/configure-in-place
index 9da584d36f9d6d12c385771a736848e709eb425e..81517cfe43546f1d73a9eec6ec4efefb8ba8bcce 100755 (executable)
--- a/contrib/configure-in-place
+++ b/contrib/configure-in-place
@@ -1,8 +1,8 @@
-#!/bin/sh
+#!/bin/bash -ex
 #
 # configure-in-place
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010, 2011  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # usage: configure-in-place [ arguments... ]
 #
@@ -10,9 +10,9 @@
 # should be invoked).
 #
 
-if [ -e .svn ]; then
+if [ -e .git ] && ! [ x"$1" = x-f ]; then
   echo
-  echo "DO NOT USE THIS IN SUBVERSION WORKING DIRECTORIES!"
+  echo "DO NOT USE THIS IN GIT WORKING DIRECTORIES!"
   echo
   echo "You might accidentally commit Makefiles in the source directories"
   echo "improperly, since they exist in the source directory for"
@@ -21,6 +21,10 @@ if [ -e .svn ]; then
   exit 1
 fi
 
+if [ x"$1" = x-f ]; then
+  shift
+fi
+
 ./configure "$@"
-. builds/current
-builds/$(CURRENT_BUILD)/config.status
+CURRENT_BUILD="$(grep '^CURRENT_BUILD *= *' builds/current | awk 'BEGIN {FS=" *= *"} {print$2}')"
+builds/$CURRENT_BUILD/config.status

diff --git a/contrib/mac-build b/contrib/mac-build
index 834191a0c7f246f0d44920c4e44c6d8a31acdf97..2501b667d3354f4ef78821a10a09762b407c4059 100755 (executable)
--- a/contrib/mac-build
+++ b/contrib/mac-build
@@ -16,6 +16,7 @@ if [ $# -ne 0 ]; then
   echo "MacPorts must be installed (but this script installs prerequisite port" >&2
   echo "packages for CVC4).  If this script is successful, it prints a configure" >&2
   echo "line that you can use to configure CVC4." >&2
+  exit 1
 fi
 
 function reporterror {

diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index d45a8ad16f59b416bf65cf337257ea68860e2dd2..0af8da640a756f9e51ddc7ba69ac0c94104fa0b7 100644 (file)
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file Combination.cpp
+/*! \file Combination.java
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none

diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index 0c84eda80c86a9d2af3848d6f6cd1b045c178855..74e2fcf289b3a3d4f894f013630f3f69f865ff1e 100644 (file)
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -392,7 +392,7 @@ class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj {
    * If the key is a TNode and the backing (the hard node reference)
    * for the key in another data structure removes the key at the same context
    * the ref count could drop to 0.  The key would then not be eligible to be
-   * hashed. Getting the order right with a guarentee is to hard.
+   * hashed. Getting the order right with a guarantee is too hard.
    */
 
   BOOST_STATIC_ASSERT(sizeof(Data) == 0);

diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
index 5f090341d8c2997aad052cdbbe6e6e80e761fe2a..2d2020a16ad8b84d0ad939aa992b54b3619fd4f1 100644 (file)
--- a/src/context/cdtrail_hashmap.h
+++ b/src/context/cdtrail_hashmap.h
@@ -540,7 +540,7 @@ public:
     return d_trailMap->find(k);
   }
 
-  /** Returns an iterator to the begining of the map.  */
+  /** Returns an iterator to the beginning of the map.  */
   const_iterator begin() const{
     return d_trailMap->begin();
   }
@@ -561,7 +561,7 @@ class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj {
    * If the key is a TNode and the backing (the hard node reference)
    * for the key in another data structure removes the key at the same context
    * the ref count could drop to 0.  The key would then not be eligible to be
-   * hashed. Getting the order right with a guarentee is to hard.
+   * hashed. Getting the order right with a guarantee is too hard.
    */
 
   BOOST_STATIC_ASSERT(sizeof(Data) == 0);

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 9e8add7520168020dc92a3f85bdb183f1b35ced6..08a3e49d0472527773de636a67869de7bc8d5969 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -96,7 +96,7 @@ bool DecisionEngine::isRelevant(SatVariable var)
 
 SatValue DecisionEngine::getPolarity(SatVariable var)
 {
-  Debug("decision") << "getPolariry(" << var <<")" << std::endl;
+  Debug("decision") << "getPolarity(" << var <<")" << std::endl;
   if(d_relevancyStrategy != NULL) {
     Assert(isRelevant(var));
     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );

diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index a3c0d168475f94b2ca5c6a25378391c6d740e4ef..a2fda44fe07b4b6754ed36ccd3b4f40846d2852d 100644 (file)
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Decision stategy
+ ** \brief Decision strategy
  **
  ** Decision strategy
  **/

diff --git a/src/expr/command.h b/src/expr/command.h
index 342aec5fff017666f091772ef8d7f742b4eb7342..9877044fb41141fee66dbe6e1b4ceb5a27de4409 100644 (file)
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -401,7 +401,7 @@ public:
 
 /**
  * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
- *  via the syntax (! expr :atrr)
+ *  via the syntax (! expr :attr)
  */
 class CVC4_PUBLIC SetUserAttributeCommand : public Command {
 protected:

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 5134d561e5ce86af756682ae1a8edf1e38a0300b..ca89dfc91910728b277eeb39371a3ca55cfcc5bc 100755 (executable)
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -2,7 +2,7 @@
 #
 # mkexpr
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create {expr,expr_manager}.{h,cpp}
 # from template files and a list of theory kinds.  Basically it just
@@ -15,7 +15,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -23,7 +23,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This file automatically generated by:
  **

diff --git a/src/expr/mkkind b/src/expr/mkkind
index 786d6187b328d052700739e6b92e51f3d688c434..f8432466dd7943336d4efb95b7ceda6b0c6fa490 100755 (executable)
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -2,7 +2,7 @@
 #
 # mkkind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create kind.h (and also
 # type_properties.h) from a template and a list of theory kinds.
@@ -14,7 +14,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -22,7 +22,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **

diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 47ffc77f9a3bc50b0518c9ff5631ffe019f2987d..160a74eac106c071a208b5b46e6994f7aee7d6c9 100755 (executable)
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -2,7 +2,7 @@
 #
 # mkmetakind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create metakind.h from a template
 # and a list of theory kinds.
@@ -17,13 +17,14 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 cat <<EOF
 /*********************                                                        */
 /** metakind.h
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 0632cb3f9947fb9997eb9942d1aae0de85f41e7f..fa6c4c260915cb5830d2269c6cb7cd0e28dada18 100755 (executable)
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -2,7 +2,7 @@
 #
 # mkoptions
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2011-2012  The CVC4 Project
+# Copyright (c) 2011-2013  The CVC4 Project
 #
 # The purpose of this script is to create options.{h,cpp}
 # from template files and a list of options.
@@ -12,7 +12,7 @@
 #   mkoptions (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+
 #
 
-copyright=2011-2012
+copyright=2011-2013
 
 me=$(basename "$0")
 
@@ -1314,7 +1314,8 @@ function output_module {
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This file automatically generated by:
  **
@@ -1496,7 +1497,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This file automatically generated by:
  **

diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 904f9a7fa43749fc61e445055c4fc037fa5bf188..6a6ae8609536b8c0ca7b796bad0a6d8911d26660 100644 (file)
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -512,7 +512,7 @@ static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
 }
 
 
-/// Return a string that represents the name assoicated with the input source
+/// Return a string that represents the name associated with the input source
 ///
 /// /param[in] is The ANTLR3_INT_STREAM interface that is representing this token stream.
 ///

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1af4799beb779bd0f095a1bc7b627e23bc36f868..b8ec160e8e1ccc85fe4f9b03de930c181e3ce500 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -416,10 +416,8 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @header {
 /**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/

diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index e3c36cf91ac9f6f8278642e62379aeaa7c1d431f..f8331c899470ca4c137874d6f483a2ea32846772 100644 (file)
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -1,3 +1,4 @@
+/* *******************                                                        */
 /*! \file Smt1.g
  ** \verbatim
  ** Original author: cconway
@@ -30,10 +31,8 @@ options {
 
 @header {
 /**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6486660914eb8736bb5b81a4fa543d63a4adb43c..1ee288aa41d472b395c542a64973df62a9eea7f0 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -31,10 +31,8 @@ options {
 
 @header {
 /**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/

diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 62ed3363238602f7c576928b1a855797d47ca006..62959c7661fda88a2253dcbe471ae1481bcada6b 100644 (file)
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -41,7 +41,7 @@ class Smt2Input : public AntlrInput {
   /** The ANTLR3 SMT2 lexer for the input. */
   pSmt2Lexer d_pSmt2Lexer;
 
-  /** The ANTLR3 CVC parser for the input. */
+  /** The ANTLR3 SMT2 parser for the input. */
   pSmt2Parser d_pSmt2Parser;
 
   /**

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 2180255ca39682f3fe8760add270837b9dc3d0c2..ec6868c5b6f4f8b3b910aff67e2bf0f9097caeaf 100644 (file)
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -32,10 +32,8 @@ options {
 
 @header {
 /**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 1e40ea63f920c7fd5ce68d5b3f244358104848ca..59b1d205b3d565e0dc948c7d44eb7a7c1206b5b2 100644 (file)
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -151,7 +151,7 @@ void Tptp::includeFile(std::string fileName){
 
   if( d_tptpDir.empty() ){
     parseError("Couldn't open included file: " + fileName
-               + " at " + currentDirFileName + " and the TPTP directory is not specified (environnement variable TPTP)");
+               + " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)");
   };
 
   std::string tptpDirFileName = d_tptpDir + fileName;

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 324988585c3168f95711f6375e966ff6966c60e0..ccbde6e80bdafa4d5c282635072a54e5fd3940e7 100644 (file)
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -160,8 +160,8 @@ protected:
    * Does a depth first search on removed literals and adds the literals
    * to be removed in the proper order to the stack. 
    * 
-   * @param lit the literal we are recusing on
-   * @param removedSet the previously computed set of redundantant literals
+   * @param lit the literal we are recursing on
+   * @param removedSet the previously computed set of redundant literals
    * @param removeStack the stack of literals in reverse order of resolution
    */
   void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);

diff --git a/src/prop/bvminisat/Makefile b/src/prop/bvminisat/Makefile
new file mode 100644 (file)
index 0000000..7188801
--- /dev/null
+++ b/src/prop/bvminisat/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/prop/bvminisat
+
+include $(topdir)/Makefile.subdir

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ca65ab1dfc2be35dc1d701ff5adf62f78607bd3e..6b0d953ddf66380690285ff74f9aa017d27f36ca 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -424,7 +424,7 @@ public:
   }
 
   void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) {
-    std::string id = n.getAttribute(expr::VarNameAttr());
+    string id = n.getAttribute(expr::VarNameAttr());
     DeclareFunctionCommand c(id,
                              n.toExpr(),
                              n.getType().toType());
@@ -541,8 +541,6 @@ public:
 
 }/* namespace CVC4::smt */
 
-using namespace CVC4::smt;
-
 SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_context(em->getContext()),
   d_userLevels(),
@@ -658,17 +656,17 @@ void SmtEngine::finalOptionsAreSet() {
 
   if(options::checkModels()) {
     if(! options::produceModels()) {
-      Notice() << "SmtEngine: turning on produce-models to support check-model" << std::endl;
+      Notice() << "SmtEngine: turning on produce-models to support check-model" << endl;
       setOption("produce-models", SExpr("true"));
     }
     if(! options::interactive()) {
-      Notice() << "SmtEngine: turning on interactive-mode to support check-model" << std::endl;
+      Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl;
       setOption("interactive-mode", SExpr("true"));
     }
   }
 
   if(options::produceAssignments() && !options::produceModels()) {
-    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << std::endl;
+    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
     setOption("produce-models", SExpr("true"));
   }
 
@@ -819,15 +817,15 @@ void SmtEngine::setLogicInternal() throw() {
   // by default, symmetry breaker is on only for QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
     bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
-    Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
+    Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
     options::ufSymmetryBreaker.set(qf_uf);
   }
   // by default, nonclausal simplification is off for QF_SAT and for quantifiers
   if(! options::simplificationMode.wasSetByUser()) {
     bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
     bool quantifiers = d_logic.isQuantified();
-    Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << std::endl;
-    //simplifaction=none works better for SMT LIB benchmarks with quantifiers, not others
+    Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << endl;
+    //simplification=none works better for SMT LIB benchmarks with quantifiers, not others
     //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
     options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
   }
@@ -843,14 +841,14 @@ void SmtEngine::setLogicInternal() throw() {
     bool iteSimp = !d_logic.isQuantified() &&
       ((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areRealsUsed()) ||
        (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV)));
-    Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
+    Trace("smt") << "setting ite simplification to " << iteSimp << endl;
     options::doITESimp.set(iteSimp);
   }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV));
-    Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
+    Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
     options::repeatSimp.set(repeatSimp);
   }
   // Turn on unconstrained simplification for QF_AUFBV
@@ -859,24 +857,24 @@ void SmtEngine::setLogicInternal() throw() {
     //    bool uncSimp = false && !qf_sat && !options::incrementalSolving();
     bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::checkModels() &&
       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
-    Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
+    Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl;
     options::unconstrainedSimp.set(uncSimp);
   }
   // Unconstrained simp currently does *not* support model generation
   if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) {
     if (options::produceModels()) {
-      Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << std::endl;
+      Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::checkModels()) {
-      Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << std::endl;
+      Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl;
       setOption("check-models", SExpr("false"));
     }
   }
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! options::arithRewriteEq.wasSetByUser()) {
     bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified();
-    Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
+    Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << endl;
     options::arithRewriteEq.set(arithRewriteEq);
   }
   if(!  options::arithHeuristicPivots.wasSetByUser()) {
@@ -888,7 +886,7 @@ void SmtEngine::setLogicInternal() throw() {
         heuristicPivots = 0;
       }
     }
-    Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots << std::endl;
+    Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots << endl;
     options::arithHeuristicPivots.set(heuristicPivots);
   }
   if(! options::arithPivotThreshold.wasSetByUser()){
@@ -898,7 +896,7 @@ void SmtEngine::setLogicInternal() throw() {
         pivotThreshold = 16;
       }
     }
-    Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold << std::endl;
+    Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold << endl;
     options::arithPivotThreshold.set(pivotThreshold);
   }
   if(! options::arithStandardCheckVarOrderPivots.wasSetByUser()){
@@ -906,7 +904,7 @@ void SmtEngine::setLogicInternal() throw() {
     if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
       varOrderPivots = 200;
     }
-    Trace("smt") << "setting arithStandardCheckVarOrderPivots  " << varOrderPivots << std::endl;
+    Trace("smt") << "setting arithStandardCheckVarOrderPivots  " << varOrderPivots << endl;
     options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
   }
   // Turn off early theory preprocessing if arithRewriteEq is on
@@ -965,7 +963,7 @@ void SmtEngine::setLogicInternal() throw() {
         ? true : false
       );
 
-    Trace("smt") << "setting decision mode to " << decMode << std::endl;
+    Trace("smt") << "setting decision mode to " << decMode << endl;
     options::decisionMode.set(decMode);
     options::decisionStopOnly.set(stoponly);
   }
@@ -973,7 +971,7 @@ void SmtEngine::setLogicInternal() throw() {
   //for finite model finding
   if( ! options::instWhenMode.wasSetByUser()){
     if( options::fmfInstEngine() ){
-      Trace("smt") << "setting inst when mode to LAST_CALL" << std::endl;
+      Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
       options::instWhenMode.set( INST_WHEN_LAST_CALL );
     }
   }
@@ -986,11 +984,11 @@ void SmtEngine::setLogicInternal() throw() {
   }
   else if (options::minisatUseElim()) {
     if (options::produceModels()) {
-      Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << std::endl;
+      Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::checkModels()) {
-      Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << std::endl;
+      Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl;
       setOption("check-models", SExpr("false"));
     }
   }
@@ -1005,11 +1003,11 @@ void SmtEngine::setLogicInternal() throw() {
   if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
       !d_logic.isLinear()) {
     if (options::produceModels()) {
-      Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl;
+      Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::checkModels()) {
-      Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl;
+      Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl;
       setOption("check-models", SExpr("false"));
     }
   }
@@ -1030,7 +1028,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
     if(key == "status") {
-      std::string s = value.getValue();
+      string s = value.getValue();
       BenchmarkStatus status =
         (s == "sat") ? SMT_SATISFIABLE :
           ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN);
@@ -1210,7 +1208,7 @@ void SmtEngine::defineFunction(Expr func,
   // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
   // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
   // d_haveAdditions = true;
-  Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << std::endl;
+  Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << endl;
   d_definedFunctions->insert(funcNode, def);
 }
 
@@ -1220,7 +1218,7 @@ Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) {
   if (k == kind::BITVECTOR_UDIV) {
     if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
       // lazily create the function symbols
-      std::ostringstream os;
+      ostringstream os;
       os << "BVUDivByZero_" << width;
       Node divByZero = nm->mkSkolem(os.str(),
                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
@@ -1231,7 +1229,7 @@ Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) {
   }
   else if (k == kind::BITVECTOR_UREM) {
     if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
-      std::ostringstream os;
+      ostringstream os;
       os << "BVURemByZero_" << width;
       Node divByZero = nm->mkSkolem(os.str(),
                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
@@ -1271,7 +1269,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
     if(i != d_smt.d_definedFunctions->end()) {
       // replacement must be closed
       if((*i).second.getFormals().size() > 0) {
-        throw TypeCheckingException(n.toExpr(), std::string("Defined function requires arguments: `") + n.toString() + "'");
+        throw TypeCheckingException(n.toExpr(), string("Defined function requires arguments: `") + n.toString() + "'");
       }
       // don't bother putting in the cache
       return (*i).second.getFormula();
@@ -1300,9 +1298,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
     break;
   }
 
- case kind::BITVECTOR_UDIV:
- case kind::BITVECTOR_UREM: {
-   node = expandBVDivByZero(node);
+  case kind::BITVECTOR_UDIV:
+  case kind::BITVECTOR_UREM: {
+    node = expandBVDivByZero(node);
     break;
   }
   case kind::DIVISION: {
@@ -1374,7 +1372,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       Debug("expand") << "     : \"" << name << "\"" << endl;
     }
     if(i == d_smt.d_definedFunctions->end()) {
-      throw TypeCheckingException(n.toExpr(), std::string("Undefined function: `") + func.toString() + "'");
+      throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
     }
     if(Debug.isOn("expand")) {
       Debug("expand") << " defn: " << def.getFunction() << endl
@@ -1443,16 +1441,16 @@ static bool containsQuantifiers(Node n) {
 }
 
 Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
-  Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << std::endl;
+  Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
   if( n.getKind()==kind::NOT ){
     Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs );
     return nn.negate();
   }else if( n.getKind()==kind::FORALL ){
     if( polarity ){
-      std::vector< Node > children;
+      vector< Node > children;
       children.push_back( n[0] );
       //add children to current scope
-      std::vector< Node > fvss;
+      vector< Node > fvss;
       fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
       for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
         fvss.push_back( n[0][i] );
@@ -1468,13 +1466,13 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
       //process body
       Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs );
       //now, substitute skolems for the variables
-      std::vector< TypeNode > argTypes;
+      vector< TypeNode > argTypes;
       for( int i=0; i<(int)fvs.size(); i++ ){
         argTypes.push_back( fvs[i].getType() );
       }
       //calculate the variables and substitution
-      std::vector< Node > vars;
-      std::vector< Node > subs;
+      vector< Node > vars;
+      vector< Node > subs;
       for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
         vars.push_back( n[0][i] );
       }
@@ -1487,7 +1485,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
           TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
           Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
           //DOTHIS: set attribute on op, marking that it should not be selected as trigger
-          std::vector< Node > funcArgs;
+          vector< Node > funcArgs;
           funcArgs.push_back( op );
           funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
           subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) );
@@ -1527,7 +1525,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
         return preSkolemizeQuantifiers( nn, polarity, fvs );
       }else{
         Assert( n.getKind() == kind::AND || n.getKind() == kind::OR );
-        std::vector< Node > children;
+        vector< Node > children;
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
         }
@@ -1576,7 +1574,7 @@ void SmtEnginePrivate::staticLearning() {
 static void dumpAssertions(const char* key,
                            const std::vector<Node>& assertionList) {
   if( Dump.isOn("assertions") &&
-      Dump.isOn(std::string("assertions:") + key) ) {
+      Dump.isOn(string("assertions:") + key) ) {
     // Push the simplified assertions to the dump output stream
     for(unsigned i = 0; i < assertionList.size(); ++ i) {
       TNode n = assertionList[i];
@@ -2350,7 +2348,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
     }
 
-    Trace("smt") << "POST nonClasualSimplify" << std::endl;
+    Trace("smt") << "POST nonClausalSimplify" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -2367,7 +2365,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       }
     }
 
-    Trace("smt") << "POST theoryPP" << std::endl;
+    Trace("smt") << "POST theoryPP" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -2377,7 +2375,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       simpITE();
     }
 
-    Trace("smt") << "POST iteSimp" << std::endl;
+    Trace("smt") << "POST iteSimp" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -2387,14 +2385,14 @@ bool SmtEnginePrivate::simplifyAssertions()
       unconstrainedSimp();
     }
 
-    Trace("smt") << "POST unconstrainedSimp" << std::endl;
+    Trace("smt") << "POST unconstrainedSimp" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
     if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
       Chat() << "...doing another round of nonclausal simplification..." << endl;
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
-                        << " doing repeated simplification" << std::endl;
+                        << " doing repeated simplification" << endl;
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
       Assert(d_assertionsToCheck.empty());
       bool noConflict = nonClausalSimplify();
@@ -2403,7 +2401,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       }
     }
 
-    Trace("smt") << "POST repeatSimp" << std::endl;
+    Trace("smt") << "POST repeatSimp" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -2630,11 +2628,11 @@ void SmtEnginePrivate::processAssertions() {
     //apply pre-skolemization to existential quantifiers
     for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
       Node prev = d_assertionsToPreprocess[i];
-      std::vector< Node > fvs;
+      vector< Node > fvs;
       d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) );
       if( prev!=d_assertionsToPreprocess[i] ){
-        Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << std::endl;
-        Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << std::endl;
+        Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
+        Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << endl;
       }
     }
   }

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index cf3aeafee0e112c9b08faf1e5e61f54c7899a41f..4655ea34ef971bd118876880104ea3aba7bdc65b 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -371,8 +371,8 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) {
   d_database->pushAssertionOrderWatch(this, witness);
 }
 
-// bool ConstraintValue::isPsuedoConstraint() const {
-//   return d_proof == d_database->d_psuedoConstraintProof;
+// bool ConstraintValue::isPseudoConstraint() const {
+//   return d_proof == d_database->d_pseudoConstraintProof;
 // }
 
 bool ConstraintValue::isSelfExplaining() const {
@@ -486,7 +486,7 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co
   d_equalityEngineProof = d_proofs.size();
   d_proofs.push_back(NullConstraint);
 
-  // d_psuedoConstraintProof = d_proofs.size();
+  // d_pseudoConstraintProof = d_proofs.size();
   // d_proofs.push_back(NullConstraint);
 }
 
@@ -833,11 +833,11 @@ void ConstraintValue::impliedBy(const std::vector<Constraint>& b){
   }
 }
 
-// void ConstraintValue::setPsuedoConstraint(){
+// void ConstraintValue::setPseudoConstraint(){
 //   Assert(truthIsUnknown());
 //   Assert(!hasLiteral());
 
-//   d_database->pushProofWatch(this, d_database->d_psuedoConstraintProof);
+//   d_database->pushProofWatch(this, d_database->d_pseudoConstraintProof);
 // }
 
 void ConstraintValue::setEqualityEngineProof(){
@@ -856,7 +856,7 @@ void ConstraintValue::markAsTrue(){
 void ConstraintValue::markAsTrue(Constraint imp){
   Assert(truthIsUnknown());
   Assert(imp->hasProof());
-  //Assert(!imp->isPsuedoConstraint());
+  //Assert(!imp->isPseudoConstraint());
 
   d_database->d_proofs.push_back(NullConstraint);
   d_database->d_proofs.push_back(imp);
@@ -868,8 +868,8 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){
   Assert(truthIsUnknown());
   Assert(impA->hasProof());
   Assert(impB->hasProof());
-  //Assert(!impA->isPsuedoConstraint());
-  //Assert(!impB->isPsuedoConstraint());
+  //Assert(!impA->isPseudoConstraint());
+  //Assert(!impB->isPseudoConstraint());
 
   d_database->d_proofs.push_back(NullConstraint);
   d_database->d_proofs.push_back(impA);
@@ -886,7 +886,7 @@ void ConstraintValue::markAsTrue(const vector<Constraint>& a){
   for(vector<Constraint>::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
     Constraint c_i = *i;
     Assert(c_i->hasProof());
-    //Assert(!c_i->isPsuedoConstraint());
+    //Assert(!c_i->isPseudoConstraint());
     d_database->d_proofs.push_back(c_i);
   }
 
@@ -903,7 +903,7 @@ SortedConstraintMap& ConstraintValue::constraintSet() const{
 bool ConstraintValue::proofIsEmpty() const{
   Assert(hasProof());
   bool result = d_database->d_proofs[d_proof] == NullConstraint;
-  //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPsuedoConstraint());
+  //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPseudoConstraint());
   Assert((!result) || isSelfExplaining() || hasEqualityEngineProof());
   return result;
 }

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 52aa5a5cedd2c4eaae383ed240d60f447895aaef..82023a48b9e3e79e1c2b0b2b2fdf053a28a9bc62 100644 (file)
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -273,7 +273,7 @@ private:
    */
   AssertionOrder _d_assertionOrder;
   /**
-   * This is guarenteed to be on the fact queue.
+   * This is guaranteed to be on the fact queue.
    * For example if x + y = x + 1 is on the fact queue, then use this 
    */
   TNode d_witness;
@@ -491,8 +491,8 @@ public:
    * The explanation is the constant true.
    * explainInto() does nothing.
    */
-  //void setPsuedoConstraint();
-  //bool isPsuedoConstraint() const;
+  //void setPseudoConstraint();
+  //bool isPseudoConstraint() const;
 
   /**
    * Returns a explanation of the constraint that is appropriate for conflicts.
@@ -709,7 +709,7 @@ private:
    *
    * This is a special proof that is always a member of the list.
    */
-  //ProofId d_psuedoConstraintProof;
+  //ProofId d_pseudoConstraintProof;
 
   typedef context::CDList<Constraint, ConstraintValue::ProofCleanup> ProofCleanupList;
   typedef context::CDList<Constraint, ConstraintValue::CanBePropagatedCleanup> CBPList;

diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 19a16d558032b4b72c069142a41ff374df036329..51c1e5138256dc6b29630d84f2d2f72333511bf2 100644 (file)
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -249,7 +249,7 @@ public:
   }
 
   /**
-   * Computes a sufficient upperbound to seperate two DeltaRationals.
+   * Computes a sufficient upperbound to separate two DeltaRationals.
    * This value is stored in res.
    * For any rational d such that
    *   0 < d < res

diff --git a/src/theory/arith/options b/src/theory/arith/options
index 9e758a0ef634ddf032614b7b3be6b4a38f229b90..efe5947666d1ef254c92a00a3d85ebaac7d9a1fb 100644 (file)
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -60,7 +60,6 @@ option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned
 
 option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write
  turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
-/ turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
-
+/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
 
 endmodule

diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
index 52e7cbf2aba72c9d1fbeee7becdcd207f36a5fb8..f8f851964bfde3ba55f98b154093e0d228a9833a 100644 (file)
--- a/src/theory/arith/options_handlers.h
+++ b/src/theory/arith/options_handlers.h
@@ -52,7 +52,7 @@ This decides on kind of propagation arithmetic attempts to do during the search.
 ";
 
 static const std::string heuristicPivotRulesHelp = "\
-This decides on the rule used by simplex during hueristic rounds\n\
+This decides on the rule used by simplex during heuristic rounds\n\
 for deciding the next basic variable to select.\n\
 Heuristic pivot rules available:\n\
 +min\n\

diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
index 86bdad53f4f1ec3b122e869ebd0469c9cbf6dfaa..4f7584ac10f85769fe309d0f520eb849140b6aa0 100644 (file)
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ b/src/theory/arrays/theory_arrays_model.cpp
@@ -41,7 +41,7 @@ Node ArrayModel::getValue( TheoryModel* m, Node i ){
     return it->second;
   }else{
     return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i );
-    //return d_default_value;   //TODO: guarentee I can return this here
+    //return d_default_value;   //TODO: guarantee I can return this here
   }
 }
 

diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 88ac5b9fbe41fe1c2df0afdb22f4b405129b32cc..2d8012bfbe8f895d0280cb71302d8d7143a3f85b 100755 (executable)
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -2,7 +2,7 @@
 #
 # mkrewriter
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create rewriter_tables.h from a template
 # and a list of theory kinds.
@@ -14,13 +14,14 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 cat <<EOF
 /*********************                                                        */
 /** rewriter_tables.h
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **

diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index a44d8e9c3bd04263be42b6d17bd4140e93addbf2..3edc7c140565da560f2d037da61e79d72e9ae92d 100755 (executable)
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -2,7 +2,7 @@
 #
 # mktheorytraits
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create theory_traits.h from a template
 # and a list of theory kinds.
@@ -14,7 +14,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -22,7 +22,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **

diff --git a/src/theory/model.h b/src/theory/model.h
index e283ee183c24ae8584318e67e255d803b2a8ef0f..98eeda97a9ff216b476e223d3b37b961cbf2c937 100644 (file)
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -87,7 +87,7 @@ public:
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
   /** add term function
     *   addTerm( n ) will do any model-specific processing necessary for n,
-    *   such as contraining the interpretation of uninterpretted functions,
+    *   such as constraining the interpretation of uninterpreted functions,
     *   and adding n to the equality engine of this model
     */
   virtual void addTerm(TNode n);

diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h
index 94922df184808172a3a13020d6f3d8e9078bc7aa..9301339549c7daf9dbbd2feb47934cb4b655c6e4 100644 (file)
--- a/src/theory/quantifiers/inst_gen.h
+++ b/src/theory/quantifiers/inst_gen.h
@@ -50,10 +50,10 @@ public:
   int getNumMatches() { return d_matches.size(); }
   bool getMatch( EqualityQuery* q, int i, InstMatch& m );
   Node getMatchValue( int i ) { return d_match_values[i]; }
-};
+};/* class InstGenProcess */
 
-}
-}
-}
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif
+#endif /* __CVC4__THEORY__QUANTIFIERS__INST_GEN_H */

diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 9f08764a98dff25a79f5e557854bd471e5efe326..bf67bdd25bee08942434b89c4dabcbb55e9d97bd 100644 (file)
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -358,7 +358,7 @@ Node QuantifierMacros::simplify( Node n ){
   if( n.getKind()==APPLY_UF ){
     Node op = n.getOperator();
     if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){
-      //do subsitutition
+      //do substitution
       Node ret = d_macro_defs[op];
       ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() );
       return ret;

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9ac431107cf01223d941caa0bfacf413f576c976..6bfea5c44931232561501c0d197ab7fd5c38146f 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -167,7 +167,7 @@ public:
   /** get counterexample literal (for cbqi) */
   Node getCounterexampleLiteral( Node f );
   /** returns node n with bound vars of f replaced by instantiation constants of f
-      node n : is the futur pattern
+      node n : is the future pattern
       node f : is the quantifier containing which bind the variable
       return a pattern where the variable are replaced by variable for
       instantiation.

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index dc31f2d5fe77ad2c5f795f165f3ebda45ecb3865..019f69ec222f189504c8b32a66a4fbfac12d76ed 100644 (file)
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__REP_SET_H
-#define __CVC4__REP_SET_H
+#ifndef __CVC4__THEORY__REP_SET_H
+#define __CVC4__THEORY__REP_SET_H
 
 #include "expr/node.h"
 #include <map>
@@ -45,7 +45,7 @@ public:
   void complete( TypeNode t );
   /** debug print */
   void toStream(std::ostream& out);
-};
+};/* class RepSet */
 
 //representative domain
 typedef std::vector< int > RepDomain;
@@ -104,9 +104,9 @@ public:
   /** debug print */
   void debugPrint( const char* c );
   void debugPrintSmall( const char* c );
-};
+};/* class RepSetIterator */
 
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif
\ No newline at end of file
+#endif /* __CVC4__THEORY__REP_SET_H */

diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h
index 97c71021932038b94a42a1a85c6ab6c6ae636385..d12c67f6a9b48c08cfab2ccc794fdd69c4d63b5b 100644 (file)
--- a/src/theory/rewriterules/rr_candidate_generator.h
+++ b/src/theory/rewriterules/rr_candidate_generator.h
@@ -32,7 +32,7 @@ typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
 
 //New CandidateGenerator. They have a simpler semantic than the old one
 
-// Just iterate amoung the equivalence classes
+// Just iterate among the equivalence classes
 // node::Null() must be given to reset
 class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{
 private:
@@ -54,7 +54,7 @@ public:
   };
 };
 
-// Just iterate amoung the equivalence class of the given node
+// Just iterate among the equivalence class of the given node
 // node::Null() *can't* be given to reset
 class CandidateGeneratorTheoryEeClass : public CandidateGenerator{
 private:

diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h
index 63728a95b1b618117a582728ad9d39176fa63088..636a4dbc1e67f687a71358e419a1a018843421c5 100644 (file)
--- a/src/theory/rewriterules/rr_inst_match.h
+++ b/src/theory/rewriterules/rr_inst_match.h
@@ -180,7 +180,7 @@ public:
   /** If reset, or getNextMatch return false they remove from the
       InstMatch the binding that they have previously created */
 
-  /** virtual Matcher in order to have definned behavior */
+  /** virtual Matcher in order to have defined behavior */
   virtual ~Matcher(){};
 };
 
@@ -195,7 +195,7 @@ private:
   std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens;
   /** the variable that have been set by this matcher (during its own reset) */
   std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */
-  /** the representant of the argument of the term given by the last reset */
+  /** the representative of the argument of the term given by the last reset */
   std::vector< Node > d_reps;
 public:
   /** The pattern we are producing matches for */
@@ -250,7 +250,7 @@ public:
 PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe );
 PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe );
 
-/** return true if whatever Node is subsituted for the variables the
+/** return true if whatever Node is substituted for the variables the
     given Node can't match the pattern */
 bool nonunifiable( TNode t, TNode pat, const std::vector<Node> & vars);
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f85a5f3cd9d558ddd82e3e2eb165a43f597beafa..f7f68985041ced855f143433993340c31bd19e77 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -809,7 +809,7 @@ Node TheoryEngine::preprocess(TNode assertion) {
       stringstream ss;
       ss << "The logic was specified as " << d_logicInfo.getLogicString()
          << ", which doesn't include " << Theory::theoryOf(current)
-         << ", but got a preprocesing-time fact for that theory." << endl
+         << ", but got a preprocessing-time fact for that theory." << endl
          << "The fact:" << endl
          << current;
       throw LogicException(ss.str());

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 388c0edf0ada01db91658e4c7cdf30679f881cb4..a3779f0e888ac5e2f1c3c443cebac027ea545d26 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -269,7 +269,7 @@ class TheoryEngine {
     void safePoint() throw(theory::Interrupted, AssertionException) {
       if (d_engine->d_interrupted)
         throw theory::Interrupted();
-   }
+    }
 
     void conflict(TNode conflictNode) throw(AssertionException) {
       Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
@@ -741,20 +741,23 @@ private:
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 public:
 
-  /** Set user attribute
-    * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
-    *  via the syntax (! n :attr)
-    */
+  /**
+   * Set user attribute.
+   * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
+   * via the syntax (! n :attr)
+   */
   void setUserAttribute(const std::string& attr, Node n);
 
-  /** Handle user attribute
-    *   Associates theory t with the attribute attr.  Theory t will be
-    *   notifed whenever an attribute of name attr is set.
-    */
+  /**
+   * Handle user attribute.
+   * Associates theory t with the attribute attr.  Theory t will be
+   * notified whenever an attribute of name attr is set.
+   */
   void handleUserAttribute(const char* attr, theory::Theory* t);
 
-  /** Check that the theory assertions are satisfied in the model
-   *  This function is called from the smt engine's checkModel routine
+  /**
+   * Check that the theory assertions are satisfied in the model.
+   * This function is called from the smt engine's checkModel routine.
    */
   void checkTheoryAssertionsWithModel();
 

diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index e0c7507494decb682293d596d38fdc3f25b50f80..4378badc8a4ef936e93f41577002a30ea6bd27ce 100644 (file)
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -124,7 +124,7 @@ This is CVC4 version " CVC4_RELEASE_STRING ) + \
     )) + "\n\
 compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
 on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
-Copyright (C) 2009, 2010, 2011, 2012\n\
+Copyright (C) 2009, 2010, 2011, 2012, 2013\n\
   New York University and The University of Iowa\n\n" + \
     ( IS_CLN_BUILD ? "\
 This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\

diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index 1f01740835a9bbe2201a0e0b6debc17c1751d495..27b589b5a0ad28212ee9b5fdbb32302e3519f6cd 100644 (file)
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file integer.h
+/*! \file integer.h.in
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none

diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index c8e42a2537f5f1d6c1c057677b7a2afe6602e947..7f5b1feb4b8a9ae961508faa4c8b49b13f358f0c 100644 (file)
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file rational.h
+/*! \file rational.h.in
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none

diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 0304a8e350263913318c0144fcb7b9086bc62197..d700b70d917c6b4be01ad3beaf6239055ec9d3ac 100644 (file)
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -425,4 +425,4 @@ void SortInference::setSkolemVar( Node f, Node v, Node sk ){
   d_op_return_types[sk] = getSortId( f, v );
 }
 
-}
\ No newline at end of file
+}/* CVC4 namespace */

diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index 17f1f1d6e01d1a4f7ae8d6ace6b432b816a2fef6..935586f7707ff57cd86fb13352a090bbbcb41beb 100644 (file)
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file tls.h
+/*! \file tls.h.in
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none

diff --git a/test/regress/regress1/arith/Makefile b/test/regress/regress1/arith/Makefile
new file mode 100644 (file)
index 0000000..481d240
--- /dev/null
+++ b/test/regress/regress1/arith/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress1/arith
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check