From 14776d0aeb833a7e728a27af6ef545f20b495f7f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 16 Aug 2013 15:15:03 -0400 Subject: [PATCH] Documentation fixes, some code typo fixes, file perms, other minor things. --- contrib/get-bug-attachments | 4 ++-- contrib/theoryskel/README.WHATS-NEXT | 5 +++++ doc/SmtEngine.3cvc_template.in | 4 ++-- doc/cvc4.1_template.in | 4 ++-- doc/cvc4.5.in | 2 +- doc/libcvc4compat.3.in | 2 +- doc/libcvc4parser.3.in | 2 +- doc/options.3cvc_template.in | 4 ++-- src/expr/metakind_template.h | 2 +- src/expr/type_node.h | 2 +- src/parser/smt2/Smt2.g | 4 ++-- src/parser/tptp/Tptp.g | 2 +- src/parser/tptp/tptp.cpp | 4 ++-- src/parser/tptp/tptp.h | 2 +- src/parser/tptp/tptp_input.h | 2 +- src/prop/minisat/core/Solver.cc | 18 +++++++++--------- src/prop/minisat/core/Solver.h | 4 ++-- src/prop/minisat/minisat.h | 5 ++--- src/prop/minisat/mtl/Vec.h | 2 +- src/prop/minisat/simp/SimpSolver.cc | 8 ++++---- src/prop/options | 4 ++-- src/smt/options | 2 +- src/smt/smt_engine.cpp | 13 ++++++------- src/smt/smt_engine.h | 8 +++++--- src/theory/arith/approx_simplex.h | 4 ++-- src/theory/arith/bound_counts.h | 17 +++++++++++++++++ src/theory/arith/normal_form.cpp | 2 +- src/theory/arith/options | 18 +++++++++--------- src/theory/arith/simplex_update.h | 2 +- src/theory/bv/theory_bv_utils.h | 2 +- src/theory/idl/idl_assertion.cpp | 17 +++++++++++++++++ src/theory/idl/idl_assertion.h | 17 +++++++++++++++++ src/theory/idl/idl_assertion_db.cpp | 17 +++++++++++++++++ src/theory/idl/idl_assertion_db.h | 17 +++++++++++++++++ src/theory/idl/idl_model.cpp | 17 +++++++++++++++++ src/theory/idl/idl_model.h | 17 +++++++++++++++++ src/theory/idl/theory_idl.cpp | 17 +++++++++++++++++ src/theory/idl/theory_idl.h | 17 +++++++++++++++++ src/theory/ite_simplifier.cpp | 4 ++-- src/theory/ite_simplifier.h | 4 +++- src/theory/output_channel.h | 2 +- src/theory/quantifiers/bounded_integers.cpp | 0 src/theory/quantifiers/bounded_integers.h | 0 .../quantifiers/first_order_reasoning.cpp | 0 src/theory/quantifiers/first_order_reasoning.h | 0 src/theory/quantifiers/full_model_check.cpp | 0 src/theory/quantifiers/full_model_check.h | 0 src/theory/quantifiers/model_engine.h | 2 +- src/theory/theory.cpp | 2 +- src/theory/theory.h | 2 +- src/theory/theory_engine.cpp | 6 +++--- src/theory/theory_engine.h | 2 +- src/theory/uf/equality_engine.h | 4 ++-- src/util/result.i | 3 ++- src/util/statistics_registry.h | 2 +- test/regress/regress0/fmf/Makefile.am | 0 test/regress/regress0/fmf/german169.smt2 | 0 test/regress/regress0/fmf/german73.smt2 | 0 test/regress/regress0/fmf/refcount24.cvc.smt2 | 0 59 files changed, 242 insertions(+), 81 deletions(-) mode change 100755 => 100644 src/theory/quantifiers/bounded_integers.cpp mode change 100755 => 100644 src/theory/quantifiers/bounded_integers.h mode change 100755 => 100644 src/theory/quantifiers/first_order_reasoning.cpp mode change 100755 => 100644 src/theory/quantifiers/first_order_reasoning.h mode change 100755 => 100644 src/theory/quantifiers/full_model_check.cpp mode change 100755 => 100644 src/theory/quantifiers/full_model_check.h mode change 100755 => 100644 test/regress/regress0/fmf/Makefile.am mode change 100755 => 100644 test/regress/regress0/fmf/german169.smt2 mode change 100755 => 100644 test/regress/regress0/fmf/german73.smt2 mode change 100755 => 100644 test/regress/regress0/fmf/refcount24.cvc.smt2 diff --git a/contrib/get-bug-attachments b/contrib/get-bug-attachments index 3bb433c51..869eee895 100755 --- a/contrib/get-bug-attachments +++ b/contrib/get-bug-attachments @@ -70,14 +70,14 @@ function webget { count=0 for attachment in $(\ - webcat "http://church.cims.nyu.edu/bugs/show_bug.cgi?id=$bugid" 2>/dev/null \ + webcat "http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=$bugid" 2>/dev/null \ | grep ' href="attachment.cgi?id=[0-9][0-9]*' \ | sed 's,.* href="attachment.cgi?id=\([0-9][0-9]*\).*,\1,' \ | sort -nu); do let count++ printf "%-30s " "Downloading attachment $attachment..." - webget "http://church.cims.nyu.edu/bugs/attachment.cgi?id=$attachment" "test/regress/regress0/bug$bugid" + webget "http://cvc4.cs.nyu.edu/bugs/attachment.cgi?id=$attachment" "test/regress/regress0/bug$bugid" done diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT index b25b6004b..31ff2d47a 100644 --- a/contrib/theoryskel/README.WHATS-NEXT +++ b/contrib/theoryskel/README.WHATS-NEXT @@ -7,6 +7,11 @@ Your next steps will likely be: and constants * to write code in theory_$dir_rewriter.h to implement a normal form for your theory's terms +* for any new types that you have introduced, add "mk*Type()" functions to + the NodeManager and ExprManager in src/expr/node_manager.{h,cpp} and + src/expr/expr_manager_template.{h,cpp}. You may also want "is*()" testers + in src/expr/type_node.h and a corresponding Type derived class in + src/expr/type.h. * to write parser rules in src/parser/cvc/Cvc.g to support the CVC input language, src/parser/smt/Smt.g to support the (deprecated) SMT-LIBv1 language, and src/parser/smt2/Smt2.g to support SMT-LIBv2 diff --git a/doc/SmtEngine.3cvc_template.in b/doc/SmtEngine.3cvc_template.in index 835bef585..3a876fefc 100644 --- a/doc/SmtEngine.3cvc_template.in +++ b/doc/SmtEngine.3cvc_template.in @@ -34,7 +34,7 @@ This manual page refers to version @VERSION@. .SH BUGS A Bugzilla for the CVC4 project is maintained at -.BR http://church.cims.nyu.edu/bugzilla3/ . +.BR http://cvc4.cs.nyu.edu/bugzilla3/ . .SH AUTHORS .B CVC4 is developed by a team of researchers at New York University @@ -48,4 +48,4 @@ contributors. Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://church.cims.nyu.edu/wiki/ . +.BR http://cvc4.cs.nyu.edu/wiki/ . diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in index 5a5f90214..baae1dc4b 100644 --- a/doc/cvc4.1_template.in +++ b/doc/cvc4.1_template.in @@ -115,7 +115,7 @@ This manual page refers to version @VERSION@. .SH BUGS A Bugzilla for the CVC4 project is maintained at -.BR http://church.cims.nyu.edu/bugzilla3/ . +.BR http://cvc4.cs.nyu.edu/bugzilla3/ . .SH AUTHORS .B CVC4 is developed by a team of researchers at New York University @@ -129,4 +129,4 @@ contributors. Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://church.cims.nyu.edu/wiki/ . +.BR http://cvc4.cs.nyu.edu/wiki/ . diff --git a/doc/cvc4.5.in b/doc/cvc4.5.in index ab4e8806c..b54f23560 100644 --- a/doc/cvc4.5.in +++ b/doc/cvc4.5.in @@ -18,4 +18,4 @@ to background theories of interest. Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://church.cims.nyu.edu/wiki/ . +.BR http://cvc4.cs.nyu.edu/wiki/ . diff --git a/doc/libcvc4compat.3.in b/doc/libcvc4compat.3.in index 3722557b0..3aa58b712 100644 --- a/doc/libcvc4compat.3.in +++ b/doc/libcvc4compat.3.in @@ -12,4 +12,4 @@ libcvc4compat \- a CVC3 compatibility library interface for the CVC4 theorem pro Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://church.cims.nyu.edu/wiki/ . +.BR http://cvc4.cs.nyu.edu/wiki/ . diff --git a/doc/libcvc4parser.3.in b/doc/libcvc4parser.3.in index 67ec74326..09fea23f1 100644 --- a/doc/libcvc4parser.3.in +++ b/doc/libcvc4parser.3.in @@ -12,4 +12,4 @@ libcvc4parser \- a parser library interface for the CVC4 theorem prover Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://church.cims.nyu.edu/wiki/ . +.BR http://cvc4.cs.nyu.edu/wiki/ . diff --git a/doc/options.3cvc_template.in b/doc/options.3cvc_template.in index 86f2ff976..a0d6c1640 100644 --- a/doc/options.3cvc_template.in +++ b/doc/options.3cvc_template.in @@ -22,7 +22,7 @@ This manual page refers to version @VERSION@. .SH BUGS A Bugzilla for the CVC4 project is maintained at -.BR http://church.cims.nyu.edu/bugzilla3/ . +.BR http://cvc4.cs.nyu.edu/bugzilla3/ . .SH AUTHORS .B CVC4 is developed by a team of researchers at New York University @@ -36,4 +36,4 @@ contributors. Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at -.BR http://church.cims.nyu.edu/wiki/ . +.BR http://cvc4.cs.nyu.edu/wiki/ . diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index e3f1b5c45..93cebe00a 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -345,7 +345,7 @@ ${metakind_operatorKinds} }/* CVC4::kind namespace */ -#line 348 "${template}" +#line 349 "${template}" namespace theory { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 322f7ad92..145ca2aba 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -622,7 +622,7 @@ public: * If this is \top, i.e. there is no inhabited type that contains both, * a TypeNode such that isNull() is true is returned. * - * For more information see: http://church.cims.nyu.edu/wiki/Cvc4_Type_Lattice + * For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice */ static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 74434f499..5aa1e53e4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -342,7 +342,7 @@ command returns [CVC4::Command* cmd = NULL] ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[expr, expr2] { cmd = new AssertCommand(expr); } - | /* checksat */ + | /* check-sat */ CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( term[expr, expr2] { if(PARSER_STATE->strictModeEnabled()) { @@ -781,7 +781,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. - It just so happens expr should already by the only argument. */ + * It just so happens expr should already be the only argument. */ assert( expr == args[0] ); } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 2ae31e810..61e0999e9 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -189,7 +189,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] } */ PARSER_STATE->includeFile(name /* , inclArgs */ ); - // The command of the included file will be produced at the new parseCommand call + // The command of the included file will be produced at the next parseCommand() call cmd = new EmptyCommand("include::" + name); } | EOF diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 3e6aa82b7..edffaa01f 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -107,7 +107,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer) { Debug("parser") << "Can't open " << fileName << std::endl; return false; } - // Samething than the predefined PUSHSTREAM(in); + // Same thing as the predefined PUSHSTREAM(in); lexer->pushCharStream(lexer,in); // restart it //lexer->rec->state->tokenStartCharIndex = -10; @@ -163,7 +163,7 @@ void Tptp::includeFile(std::string fileName) { // Test in the directory of the actual parsed file std::string currentDirFileName; if(inputName != "") { - // TODO: Use dirname ot Boost::filesystem? + // TODO: Use dirname or Boost::filesystem? size_t pos = inputName.rfind('/'); if(pos != std::string::npos) { currentDirFileName = std::string(inputName, 0, pos + 1); diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index eb49d7dcc..e180d1524 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -203,7 +203,7 @@ inline void Tptp::makeApplication(Expr& expr, std::string& name, inline Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) { // For SZS ontology compliance. - // If we're in cnf() though, conjectures don't result in "Theorem" or + // if we're in cnf() though, conjectures don't result in "Theorem" or // "CounterSatisfiable". if(!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) { d_hasConjecture = true; diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index 19e928e7e..cb2bcd3a3 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -64,7 +64,7 @@ public: /** Get the language that this Input is reading. */ InputLanguage getLanguage() const throw() { - return language::input::LANG_SMTLIB_V2; + return language::input::LANG_TPTP; } protected: diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index cacde258d..36e196821 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -231,7 +231,7 @@ CRef Solver::reason(Var x) { int i, j; Lit prev = lit_Undef; for (i = 0, j = 0; i < explanation.size(); ++ i) { - // This clause is valid theory propagation, so it's level is the level of the top literal + // This clause is valid theory propagation, so its level is the level of the top literal explLevel = std::max(explLevel, intro_level(var(explanation[i]))); Assert(value(explanation[i]) != l_Undef); @@ -348,7 +348,7 @@ bool Solver::addClause_(vec& ps, bool removable) assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } ) - return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); + return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef); } else return ok; } } @@ -806,7 +806,7 @@ CRef Solver::propagate(TheoryCheckType type) // Propagate on the clauses confl = propagateBool(); // If no conflict, do the theory check - if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) { + if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) { // Do the theory check if (type == CHECK_FINAL_FAKE) { theoryCheck(CVC4::theory::Theory::EFFORT_FULL); @@ -1019,8 +1019,8 @@ void Solver::removeClausesAboveLevel(vec& cs, int level) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (c.level() > level) { - assert(!locked(c)); - removeClause(cs[i]); + assert(!locked(c)); + removeClause(cs[i]); } else { cs[j++] = cs[i]; } @@ -1050,7 +1050,7 @@ bool Solver::simplify() { assert(decisionLevel() == 0); - if (!ok || propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef) + if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef) return ok = false; if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) @@ -1212,7 +1212,7 @@ lbool Solver::search(int nof_conflicts) if (next == lit_Undef) { // We need to do a full theory check to confirm - Debug("minisat::search") << "Doing a full theoy check..." + Debug("minisat::search") << "Doing a full theory check..." << std::endl; check_type = CHECK_FINAL; continue; @@ -1492,7 +1492,7 @@ void Solver::pop() Debug("minisat") << "== unassigning " << trail.last() << std::endl; Var x = var(trail.last()); if (user_level(x) > assertionLevel) { - assigns [x] = l_Undef; + assigns[x] = l_Undef; vardata[x] = VarData(CRef_Undef, -1, -1, intro_level(x), -1); if(phase_saving >= 1 && (polarity[x] & 0x2) == 0) polarity[x] = sign(trail.last()); @@ -1505,7 +1505,7 @@ void Solver::pop() // The head should be at the trail top qhead = trail.size(); - // Remove the clause + // Remove the clauses removeClausesAboveLevel(clauses_persistent, assertionLevel); removeClausesAboveLevel(clauses_removable, assertionLevel); diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 55780479a..30d72ac75 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -266,7 +266,7 @@ protected: int level; // User level when the literal was added to the trail int user_level; - // Use level at which this literal was introduced + // User level at which this literal was introduced int intro_level; // The index in the trail int trail_index; @@ -335,7 +335,7 @@ protected: enum TheoryCheckType { // Quick check, but don't perform theory reasoning - CHECK_WITHOUTH_THEORY, + CHECK_WITHOUT_THEORY, // Check and perform theory reasoning CHECK_WITH_THEORY, // The SAT abstraction of the problem is satisfiable, perform a full theory check diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 37e471846..ec49b5f71 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -30,16 +30,15 @@ class MinisatSatSolver : public DPLLSatSolverInterface { /** The SatSolver used */ Minisat::SimpSolver* d_minisat; - /** The SatSolver uses this to communicate with the theories */ TheoryProxy* d_theoryProxy; - /** Context we will be using to synchronzie the sat solver */ + /** Context we will be using to synchronize the sat solver */ context::Context* d_context; public: - MinisatSatSolver (); + MinisatSatSolver(); ~MinisatSatSolver(); static SatVariable toSatVariable(Minisat::Var var); diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index 5d8c2850e..5f85f6fcd 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -86,7 +86,7 @@ public: const T& operator [] (int index) const { return data[index]; } T& operator [] (int index) { return data[index]; } - // Duplicatation (preferred instead): + // Duplication (preferred instead): void copyTo(vec& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; } void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } }; diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 0e0e5d3ae..6dcdb76c7 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -67,7 +67,7 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c if(options::minisatUseElim() && options::minisatUseElim.wasSetByUser() && enableIncremental) { - WarningOnce() << "Incremental mode incompatible with --minisat-elimination" << std::endl; + WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl; } vec dummy(1,lit_Undef); @@ -239,7 +239,7 @@ bool SimpSolver::strengthenClause(CRef cr, Lit l) updateElimHeap(var(l)); } - return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef : true; + return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUT_THEORY) == CRef_Undef : true; } @@ -346,7 +346,7 @@ bool SimpSolver::implied(const vec& c) uncheckedEnqueue(~c[i]); } - bool result = propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef; + bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef; cancelUntil(0); return result; } @@ -435,7 +435,7 @@ bool SimpSolver::asymm(Var v, CRef cr) else l = c[i]; - if (propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef){ + if (propagate(CHECK_WITHOUT_THEORY) != CRef_Undef){ cancelUntil(0); asymm_lits++; if (!strengthenClause(cr, l)) diff --git a/src/prop/options b/src/prop/options index e3a0f814a..b300c3fb6 100644 --- a/src/prop/options +++ b/src/prop/options @@ -22,8 +22,8 @@ option satRestartFirst --restart-int-base=N unsigned :default 25 option satRestartInc --restart-int-inc=F double :default 3.0 :predicate greater_equal(0.0) sets the restart interval increase factor for the sat solver (F=3.0 by default) -option sat_refine_conflicts --refine-conflicts bool - refine theory conflict clauses +option sat_refine_conflicts --refine-conflicts bool :default false + refine theory conflict clauses (default false) option minisatUseElim --minisat-elimination bool :default true :read-write use Minisat elimination diff --git a/src/smt/options b/src/smt/options index e5f9c2eaf..f39662c10 100644 --- a/src/smt/options +++ b/src/smt/options @@ -69,7 +69,7 @@ common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" enable time limiting per query (give milliseconds) common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" - enable resource limiting + enable resource limiting (currently, roughly the number of SAT conflicts) common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long" enable resource limiting per query diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 987220cc7..6e09408d9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -684,7 +684,7 @@ void SmtEngine::finalOptionsAreSet() { return; } - if (options::bitvectorEagerBitblast()) { + if(options::bitvectorEagerBitblast()) { // Eager solver should use the internal decision strategy options::decisionMode.set(DECISION_STRATEGY_INTERNAL); } @@ -1380,20 +1380,19 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map& queue) { } -// neeed a better name, this is not technically a ground term +// need a better name, this is not technically a ground term inline bool isBVGroundTerm(TNode node) { if (node.getNumChildren() == 0) { return node.isConst(); diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp index 861dd0a46..1e725932b 100644 --- a/src/theory/idl/idl_assertion.cpp +++ b/src/theory/idl/idl_assertion.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file idl_assertion.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/idl/idl_assertion.h" using namespace CVC4; diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h index 2ed5a6bef..8ce0e93b2 100644 --- a/src/theory/idl/idl_assertion.h +++ b/src/theory/idl/idl_assertion.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file idl_assertion.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #pragma once #include "theory/idl/idl_model.h" diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp index 7c27e9d0d..697c70c02 100644 --- a/src/theory/idl/idl_assertion_db.cpp +++ b/src/theory/idl/idl_assertion_db.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file idl_assertion_db.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/idl/idl_assertion_db.h" using namespace CVC4; diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h index 3972819da..0501bc6bf 100644 --- a/src/theory/idl/idl_assertion_db.h +++ b/src/theory/idl/idl_assertion_db.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file idl_assertion_db.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #pragma once #include "theory/idl/idl_assertion.h" diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp index 2feabd700..75f4834ea 100644 --- a/src/theory/idl/idl_model.cpp +++ b/src/theory/idl/idl_model.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file idl_model.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/idl/idl_model.h" using namespace CVC4; diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h index a1840a35a..64407684b 100644 --- a/src/theory/idl/idl_model.h +++ b/src/theory/idl/idl_model.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file idl_model.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #pragma once #include "expr/node.h" diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index bf2297d3d..e5100fc71 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file theory_idl.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/idl/theory_idl.h" #include "theory/idl/options.h" #include "theory/rewriter.h" diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h index 25b992981..c629ad2b0 100644 --- a/src/theory/idl/theory_idl.h +++ b/src/theory/idl/theory_idl.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file theory_idl.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #pragma once #include "cvc4_private.h" diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp index ec9eb27d4..463a9c41a 100644 --- a/src/theory/ite_simplifier.cpp +++ b/src/theory/ite_simplifier.cpp @@ -33,7 +33,7 @@ bool ITESimplifier::containsTermITE(TNode e) } hash_map::iterator it; - it = d_containsTermITECache.find(e); + it = d_containsTermITECache.find(e); if (it != d_containsTermITECache.end()) { return (*it).second; } @@ -60,7 +60,7 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) } hash_map::iterator it; - it = d_leavesConstCache.find(e); + it = d_leavesConstCache.find(e); if (it != d_leavesConstCache.end()) { return (*it).second; } diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h index 0f648f91d..2329cd970 100644 --- a/src/theory/ite_simplifier.h +++ b/src/theory/ite_simplifier.h @@ -43,6 +43,7 @@ #include "util/ite_removal.h" namespace CVC4 { +namespace theory { class ITESimplifier { Node d_true; @@ -160,6 +161,7 @@ public: }; -} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 524c9606d..44b89e8cb 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -222,7 +222,7 @@ public: /** Demands that the search restart from sat search level 0. * Using this leads to non-termination issues. - * It is appropraite for prototyping for theories. + * It is appropriate for prototyping for theories. */ virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {} diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp old mode 100755 new mode 100644 diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h old mode 100755 new mode 100644 diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp old mode 100755 new mode 100644 diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h old mode 100755 new mode 100644 diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp old mode 100755 new mode 100644 diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h old mode 100755 new mode 100644 diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 686a2cc13..1c2c38c51 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -56,7 +56,7 @@ public: //get relevant domain RelevantDomain * getRelevantDomain() { return d_rel_dom; } //get the builder - QModelBuilder * getModelBuilder() { return d_builder; } + QModelBuilder* getModelBuilder() { return d_builder; } public: void check( Theory::Effort e ); void registerQuantifier( Node f ); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9ed20cc99..3e30645e8 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -72,7 +72,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { // Variables if (node.isVar()) { if (theoryOf(node.getType()) != theory::THEORY_BOOL) { - // We treat the varibables as uninterpreted + // We treat the variables as uninterpreted return s_uninterpretedSortOwner; } else { // Except for the Boolean ones, which we just ignore anyhow diff --git a/src/theory/theory.h b/src/theory/theory.h index 23fd67b23..6b1974bb8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -516,7 +516,7 @@ public: virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } /** - * Return the model value of the give shared term (or null if not avalilable. + * Return the model value of the give shared term (or null if not available). */ virtual Node getModelValue(TNode var) { return Node::null(); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f6616920a..448e3a8fa 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -212,7 +212,7 @@ void TheoryEngine::preRegister(TNode preprocessed) { } } if (multipleTheories) { - // Collect the shared terms if there are multipe theories + // Collect the shared terms if there are multiple theories NodeVisitor::run(d_sharedTermsVisitor, preprocessed); } } @@ -1317,7 +1317,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable d_iteRemover.run(additionalLemmas, iteSkolemMap); additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); - if(Trace.isOn("lemma-ites")) { + if(Debug.isOn("lemma-ites")) { Debug("lemma-ites") << "removed ITEs from lemma: " << node << endl; Debug("lemma-ites") << " + now have the following " << additionalLemmas.size() << " lemma(s):" << endl; @@ -1417,7 +1417,7 @@ void TheoryEngine::getExplanation(std::vector& explanationVector Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; - // If a treu constant or a negation of a false constant we can ignore it + // If a true constant or a negation of a false constant we can ignore it if (toExplain.node.isConst() && toExplain.node.getConst()) { ++ i; continue; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 97b018214..fcbec2a41 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -773,7 +773,7 @@ private: void dumpAssertions(const char* tag); /** For preprocessing pass simplifying ITEs */ - ITESimplifier d_iteSimplifier; + theory::ITESimplifier d_iteSimplifier; /** For preprocessing pass simplifying unconstrained expressions */ UnconstrainedSimplifier d_unconstrainedSimp; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 6962f0c69..8d1b6f1d9 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -741,7 +741,7 @@ public: /** * Adds a predicate p with given polarity. The predicate asserted * should be in the congruence closure kinds (otherwise it's - * useless. + * useless). * * @param p the (non-negated) predicate * @param polarity true if asserting the predicate, false if @@ -777,7 +777,7 @@ public: void getUseListTerms(TNode t, std::set& output); /** - * Get an explanation of the equality t1 = t2 begin true of false. + * Get an explanation of the equality t1 = t2 being true or false. * Returns the reasons (added when asserting) that imply it * in the assertions vector. */ diff --git a/src/util/result.i b/src/util/result.i index 029a3618a..b77bfd881 100644 --- a/src/util/result.i +++ b/src/util/result.i @@ -12,8 +12,9 @@ %ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); %ignore CVC4::operator==(enum Result::Sat, const Result&); -%ignore CVC4::operator==(enum Result::Validity, const Result&); %ignore CVC4::operator!=(enum Result::Sat, const Result&); + +%ignore CVC4::operator==(enum Result::Validity, const Result&); %ignore CVC4::operator!=(enum Result::Validity, const Result&); %include "util/result.h" diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 3bec559d5..8ffc60d17 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -847,7 +847,7 @@ public: * like in this example, which takes the place of the declaration of a * statistics field "d_checkTimer": * - * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::morgan::checkTime"); + * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime"); * * If any args need to be passed to the constructor, you can specify * them after the string. diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am old mode 100755 new mode 100644 diff --git a/test/regress/regress0/fmf/german169.smt2 b/test/regress/regress0/fmf/german169.smt2 old mode 100755 new mode 100644 diff --git a/test/regress/regress0/fmf/german73.smt2 b/test/regress/regress0/fmf/german73.smt2 old mode 100755 new mode 100644 diff --git a/test/regress/regress0/fmf/refcount24.cvc.smt2 b/test/regress/regress0/fmf/refcount24.cvc.smt2 old mode 100755 new mode 100644 -- 2.30.2