diff options
Diffstat (limited to 'src')
41 files changed, 157 insertions, 153 deletions
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index 0c84eda80..74e2fcf28 100644 --- 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 5f090341d..2d2020a16 100644 --- 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 9e8add752..08a3e49d0 100644 --- 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 a3c0d1684..a2fda44fe 100644 --- 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 342aec5ff..9877044fb 100644 --- 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 5134d561e..ca89dfc91 100755 --- 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 786d6187b..f8432466d 100755 --- 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 47ffc77f9..160a74eac 100755 --- 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 0632cb3f9..fa6c4c260 100755 --- 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 904f9a7fa..6a6ae8609 100644 --- 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 1af4799be..b8ec160e8 100644 --- 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 e3c36cf91..f8331c899 100644 --- 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 648666091..1ee288aa4 100644 --- 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 62ed33632..62959c766 100644 --- 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 2180255ca..ec6868c5b 100644 --- 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 1e40ea63f..59b1d205b 100644 --- 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 324988585..ccbde6e80 100644 --- 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 index 000000000..71888016d --- /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 ca65ab1df..6b0d953dd 100644 --- 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 cf3aeafee..4655ea34e 100644 --- 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 52aa5a5ce..82023a48b 100644 --- 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 19a16d558..51c1e5138 100644 --- 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 9e758a0ef..efe594766 100644 --- 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 52e7cbf2a..f8f851964 100644 --- 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 86bdad53f..4f7584ac1 100644 --- 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 88ac5b9fb..2d8012bfb 100755 --- 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 a44d8e9c3..3edc7c140 100755 --- 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 e283ee183..98eeda97a 100644 --- 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 94922df18..930133954 100644 --- 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 9f08764a9..bf67bdd25 100644 --- 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 9ac431107..6bfea5c44 100644 --- 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 dc31f2d5f..019f69ec2 100644 --- 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 97c710219..d12c67f6a 100644 --- 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 63728a95b..636a4dbc1 100644 --- 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 f85a5f3cd..f7f689850 100644 --- 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 388c0edf0..a3779f0e8 100644 --- 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 e0c750749..4378badc8 100644 --- 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 1f0174083..27b589b5a 100644 --- 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 c8e42a253..7f5b1feb4 100644 --- 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 0304a8e35..d700b70d9 100644 --- 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 17f1f1d6e..935586f77 100644 --- 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 |