diff options
59 files changed, 242 insertions, 81 deletions
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 != "<stdin>") { - // 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<Lit>& 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<CRef>& 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<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; } void moveTo(vec<T>& 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<Lit> 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<Lit>& 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<Node, Node, NodeHashF // otherwise expand it NodeManager* nm = d_smt.d_nodeManager; - // FIXME: this theory specific code should be factored out of the SmtEngine, somehow + // FIXME: this theory-specific code should be factored out of the + // SmtEngine, somehow switch(k) { case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: - case kind::BITVECTOR_SMOD: { + case kind::BITVECTOR_SMOD: node = bv::TheoryBVRewriter::eliminateBVSDiv(node); break; - } case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UREM: { + case kind::BITVECTOR_UREM: node = expandBVDivByZero(node); break; - } case kind::DIVISION: { // partial function: division @@ -2961,7 +2960,7 @@ void SmtEnginePrivate::processAssertions() { Rewriter::rewrite(Node(builder)); } // For some reason this is needed for some benchmarks, such as - // http://church.cims.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 + // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 // Figure it out later removeITEs(); // Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3531f92e7..9655297b3 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -507,9 +507,11 @@ public: /** * Set a resource limit for SmtEngine operations. This is like a time * limit, but it's deterministic so that reproducible results can be - * obtained. However, please note that it may not be deterministic - * between different versions of CVC4, or even the same version on - * different platforms. + * obtained. Currently, it's based on the number of conflicts. + * However, please note that the definition may change between different + * versions of CVC4 (as may the number of conflicts required, anyway), + * and it might even be different between instances of the same version + * of CVC4 on different platforms. * * A cumulative and non-cumulative (per-call) resource limit can be * set at the same time. A call to setResourceLimit() with diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 175e56f8e..a34c8981d 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -24,7 +24,7 @@ public: /** * If glpk is enabled, return a subclass that can do something. - * If glpk is disabled, return a sublass that does nothing. + * If glpk is disabled, return a subclass that does nothing. */ static ApproximateSimplex* mkApproximateSimplexSolver(const ArithVariables& vars); ApproximateSimplex(); @@ -52,7 +52,7 @@ public: virtual ApproxResult solveMIP() = 0; virtual Solution extractMIP() const = 0; - /** UTILIES FOR DEALING WITH ESTIMATES */ + /** UTILITIES FOR DEALING WITH ESTIMATES */ static const double SMALL_FIXED_DELTA; static const double TOLERENCE; diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 1ee6ada06..49c1a94ce 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file bound_counts.h + ** \verbatim + ** Original author: Tim King + ** 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 "cvc4_private.h" #pragma once diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 1ebbe49e0..7cd202e53 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -22,7 +22,7 @@ using namespace std; namespace CVC4 { -namespace theory{ +namespace theory { namespace arith { bool Variable::isDivMember(Node n){ diff --git a/src/theory/arith/options b/src/theory/arith/options index 57ef3d1b9..43b582bc8 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -56,7 +56,7 @@ option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bo turns on the preprocessing step of attempting to infer bounds on miplib problems /turns off the preprocessing step of attempting to infer bounds on miplib problems -option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned :default 1 +option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1 do substitution for miplib 'tmp' vars if defined in <= N eliminated vars option doCutAllBounded --cut-all-bounded bool :default false :read-write @@ -67,11 +67,11 @@ option maxCutsInContext --maxCutsInContext unsigned :default 65535 maximum cuts in a given context before signalling a restart option revertArithModels --revert-arith-models-on-unsat bool :default false - Revert the arithmetic model to a known safe model on unsat if one is cached + revert the arithmetic model to a known safe model on unsat if one is cached option havePenalties --fc-penalties bool :default false :read-write turns on degenerate pivot penalties -/ turns off degenerate pivot penalties +/turns off degenerate pivot penalties option useFC --use-fcsimplex bool :default false :read-write use focusing and converging simplex (FMCAD 2013 submission) @@ -80,25 +80,25 @@ option useSOI --use-soi bool :default false :read-write use sum of infeasibility simplex (FMCAD 2013 submission) option restrictedPivots --restrict-pivots bool :default true :read-write - have a pivot cap for simplex at effort levels below fullEffort. + have a pivot cap for simplex at effort levels below fullEffort option collectPivots --collect-pivot-stats bool :default false :read-write collect the pivot history option fancyFinal --fancy-final bool :default false :read-write - Tuning how final check works for really hard problems. + tuning how final check works for really hard problems option exportDioDecompositions --dio-decomps bool :default false :read-write - Let skolem variables for integer divisibility constraints leak from the dio solver. + let skolem variables for integer divisibility constraints leak from the dio solver option newProp --new-prop bool :default false :read-write - Use the new row propagation system + use the new row propagation system option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write - Rows shorter than this are propagated as clauses + rows shorter than this are propagated as clauses option soiQuickExplain --soi-qe bool :default false :read-write - Use quick explain to minimize the sum of infeasibility conflicts. + use quick explain to minimize the sum of infeasibility conflicts option rewriteDivk rewrite-divk --rewrite-divk bool :default false rewrite division and mod when by a constant into linear terms diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index 516586568..64aa193dd 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -318,7 +318,7 @@ private: } /** - * Determines the appropraite WitnessImprovement for the update. + * Determines the appropriate WitnessImprovement for the update. * useBlands breaks ties for degenerate pivots. * * This is safe if: diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 5847bac3e..ab6a615a2 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -357,7 +357,7 @@ inline Node flattenAnd(std::vector<TNode>& 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<Node, bool, NodeHashFunction>::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<Node, bool, NodeHashFunction>::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 index 13e075265..13e075265 100755..100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 27d5b7569..27d5b7569 100755..100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp index ebfb55f08..ebfb55f08 100755..100644 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ b/src/theory/quantifiers/first_order_reasoning.cpp diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h index 5f217050c..5f217050c 100755..100644 --- a/src/theory/quantifiers/first_order_reasoning.h +++ b/src/theory/quantifiers/first_order_reasoning.h diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index a0b195a9c..a0b195a9c 100755..100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 6bb375c34..6bb375c34 100755..100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h 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<SharedTermsVisitor>::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<NodeTheoryPair>& 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<bool>()) { ++ 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<TNode>& 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 index 97b48c716..97b48c716 100755..100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am diff --git a/test/regress/regress0/fmf/german169.smt2 b/test/regress/regress0/fmf/german169.smt2 index f0906d6b5..f0906d6b5 100755..100644 --- a/test/regress/regress0/fmf/german169.smt2 +++ b/test/regress/regress0/fmf/german169.smt2 diff --git a/test/regress/regress0/fmf/german73.smt2 b/test/regress/regress0/fmf/german73.smt2 index 388a53624..388a53624 100755..100644 --- a/test/regress/regress0/fmf/german73.smt2 +++ b/test/regress/regress0/fmf/german73.smt2 diff --git a/test/regress/regress0/fmf/refcount24.cvc.smt2 b/test/regress/regress0/fmf/refcount24.cvc.smt2 index bf042c9b2..bf042c9b2 100755..100644 --- a/test/regress/regress0/fmf/refcount24.cvc.smt2 +++ b/test/regress/regress0/fmf/refcount24.cvc.smt2 |