From: Morgan Deters Date: Wed, 20 Mar 2013 22:16:26 +0000 (-0400) Subject: Merging some cleanup work: X-Git-Tag: cvc5-1.0.0~7352 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b6ad34343d0a09de37dc4e5ff57cd8625dca3fc4;p=cvc5.git Merging some cleanup work: * Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed --- diff --git a/NEWS b/NEWS index 9d4b5452d..e792564ba 100644 --- a/NEWS +++ b/NEWS @@ -6,15 +6,16 @@ Changes since 1.0 * tuple and record support in the compatibility library * user patterns are now supported in the SMT-LIBv1.2 parser * SMT-LIB get-model output now is easier to machine-parse: contains (model...) -* Win32 support via mingw +* Win32-building support via mingw * for printing commands as they're invoked from the driver, you now need verbosity of 3 or higher (e.g. -vvv) instead of verbosity 1 or higher (-v). This allows tracing the solver's activities without having too much output. -* multiline support in interactive mode +* multiline input support in interactive mode * To make CVC4 quieter in abnormal (e.g., "warning" conditions), you can use -q. Previously, this would silence all output (including "sat" or "unsat") as well. Now, single -q silences messages and warnings, and double -qq silences all output (except on exception or signal). * Boolean term support in datatypes +* numerous bug fixes, usability improvements, and build system improvements --- Morgan Deters Wed, 20 Mar 2013 20:03:50 -0400 +-- Morgan Deters Tue, 26 Mar 2013 15:17:52 -0400 diff --git a/configure.ac b/configure.ac index b8127592f..33bdb5128 100644 --- a/configure.ac +++ b/configure.ac @@ -1179,7 +1179,7 @@ AC_SUBST(MAN_DATE) AC_CONFIG_FILES([ Makefile.builds Makefile] - m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^src/prop/cryptominisat/' | sort | sed 's,\.am$,,']) + m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | sort | sed 's,\.am$,,']) ) if test $cvc4_has_threads = yes; then @@ -1206,8 +1206,6 @@ CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3]) -# AC_CONFIG_SUBDIRS([src/prop/cryptominisat]) - AC_OUTPUT # Final information to the user diff --git a/contrib/spellcheck b/contrib/spellcheck index 4aa210a50..20cbd82d9 100755 --- a/contrib/spellcheck +++ b/contrib/spellcheck @@ -2,7 +2,7 @@ dir="$(dirname "$0")" -find src \( -name '*.cpp' -o -name '*.h' \) \! -path 'src/prop/minisat/*' \! -path 'src/prop/bvminisat/*' \! -path 'src/prop/cryptominisat/*' \! -path 'src/parser/*/generated/*' | +find src \( -name '*.cpp' -o -name '*.h' \) \! -path 'src/prop/minisat/*' \! -path 'src/prop/bvminisat/*' \! -path 'src/parser/*/generated/*' | while read f; do misspelled_words=` $dir/extract-strings-and-comments $f | diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 4811a4bbe..f7ce15f6c 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -34,7 +34,7 @@ # the license.) # -my $excluded_directories = '^(minisat|bvminisat|cryptominisat|CVS|generated)$'; +my $excluded_directories = '^(minisat|bvminisat|CVS|generated)$'; my $excluded_paths = '^(src/parser/antlr_input_imports.cpp|src/bindings/compat/.*)$'; # Years of copyright for the template. E.g., the string diff --git a/library_versions b/library_versions index 657c13cd8..f5f3daef7 100644 --- a/library_versions +++ b/library_versions @@ -47,3 +47,4 @@ 1\.0 libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0 1\.0\.1-prerelease libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0 1\.1-prerelease libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0 +1\.1 libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 4d9cbc60d..b436bad7c 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -45,7 +45,7 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) ${typerules} -#line 46 "${template}" +#line 49 "${template}" default: Debug("getType") << "FAILURE" << std::endl; @@ -68,7 +68,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) switch(n.getKind()) { ${construles} -#line 69 "${template}" +#line 72 "${template}" default:; } diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index 0527b7f1a..bb26feef3 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -34,7 +34,7 @@ namespace main { class CommandExecutorPortfolio : public CommandExecutor { - // These shall be created/deleted during initalization + // These shall be created/deleted during initialization std::vector d_exprMgrs; const unsigned d_numThreads; // Currently const, but designed so it is // not too hard to support this changing diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2b909a9a9..d4448787f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -254,7 +254,7 @@ class SmtEnginePrivate : public NodeManagerListener { * A map of AbsractValues to their actual constants. Only used if * options::abstractValues() is on. */ - theory::SubstitutionMap d_abstractValueMap; + SubstitutionMap d_abstractValueMap; /** * A mapping of all abstract values (actual value |-> abstract) that @@ -489,7 +489,7 @@ public: /** * Return the uinterpreted function symbol corresponding to division-by-zero - * for this particular bit-wdith + * for this particular bit-width * @param k should be UREM or UDIV * @param width * @@ -695,7 +695,7 @@ void SmtEngine::finalOptionsAreSet() { setLogicInternal(); } - // finish initalization, creat the prop engine, etc. + // finish initialization, create the prop engine, etc. finishInit(); AlwaysAssert( d_propEngine->getAssertionLevel() == 0, @@ -815,11 +815,11 @@ void SmtEngine::setLogicInternal() throw() { d_logic.lock(); // may need to force uninterpreted functions to be on for non-linear - if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) || - d_logic.isTheoryEnabled(theory::THEORY_BV)) && - !d_logic.isTheoryEnabled(theory::THEORY_UF)){ + if(((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) || + d_logic.isTheoryEnabled(THEORY_BV)) && + !d_logic.isTheoryEnabled(THEORY_UF)){ d_logic = d_logic.getUnlockedCopy(); - d_logic.enableTheory(theory::THEORY_UF); + d_logic.enableTheory(THEORY_UF); d_logic.lock(); } @@ -1030,7 +1030,7 @@ void SmtEngine::setLogicInternal() throw() { } // Non-linear arithmetic does not support models - if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) && + if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) { if (options::produceModels()) { Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl; @@ -1042,8 +1042,8 @@ void SmtEngine::setLogicInternal() throw() { } } - //datatypes theory should assign values to all datatypes terms if logic is quantified - if (d_logic.isQuantified() && d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { + // datatypes theory should assign values to all datatypes terms if logic is quantified + if (d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_DATATYPES)) { if( !options::dtForceAssignment.wasSetByUser() ){ options::dtForceAssignment.set(true); } @@ -1800,7 +1800,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { for( SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin(); pos != d_topLevelSubstitutions.end(); ++pos) { Node n = (*pos).first; Node v = (*pos).second; - Trace("model") << "Add substitution : " << n << " " << v << std::endl; + Trace("model") << "Add substitution : " << n << " " << v << endl; m->addSubstitution( n, v ); } } @@ -2395,7 +2395,7 @@ bool SmtEnginePrivate::simplifyAssertions() // miplib rewrites aren't safe in incremental mode ! options::incrementalSolving() && // only useful in arith - d_smt.d_logic.isTheoryEnabled(theory::THEORY_ARITH) && + d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) && // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) @@ -2654,16 +2654,16 @@ void SmtEnginePrivate::processAssertions() { switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: case booleans::BOOLEAN_TERM_CONVERT_NATIVE: - if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) { + if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) { d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(theory::THEORY_BV); + d_smt.d_logic.enableTheory(THEORY_BV); d_smt.d_logic.lock(); } break; case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: - if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { + if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) { d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(theory::THEORY_DATATYPES); + d_smt.d_logic.enableTheory(THEORY_DATATYPES); d_smt.d_logic.lock(); } break; diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index 499d362a9..ec4b223cf 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -30,7 +30,7 @@ const ReasonId CVC4::theory::bv::AxiomReasonId = -2; bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) { - Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; + Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; TermId id_a = registerTerm(a); TermId id_b = registerTerm(b); @@ -121,7 +121,7 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) { while (!queue.empty()) { TermId current = queue.top(); queue.pop(); - Debug("bv-inequality-internal") << "InequalityGraph::processQueue proceessing " << getTermNode(current) << "\n"; + Debug("bv-inequality-internal") << "InequalityGraph::processQueue processing " << getTermNode(current) << "\n"; BitVector current_value = getValue(current); diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 2ea92635e..ca22f29b6 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -208,12 +208,13 @@ public: */ virtual void spendResource() throw() {} - /** Handle user attribute - * Associates theory t with the attribute attr. Theory t will be - * notifed whenever an attribute of name attr is set on a node. - * This can happen through, for example, the SMT LIB v2 language. - */ - virtual void handleUserAttribute( const char* attr, Theory* t ){} + /** + * Handle user attribute. + * Associates theory t with the attribute attr. Theory t will be + * notified whenever an attribute of name attr is set on a node. + * This can happen through, for example, the SMT-LIBv2 language. + */ + virtual void handleUserAttribute(const char* attr, Theory* t) {} };/* class OutputChannel */ diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 0b4f2654b..187587227 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -31,7 +31,7 @@ namespace theory { class QuantRelevance { private: - /** for computing relavance */ + /** for computing relevance */ bool d_computeRel; /** map from quantifiers to symbols they contain */ std::map< Node, std::vector< Node > > d_syms; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 6bfea5c44..e232a382e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -212,7 +212,7 @@ private: std::map< TNode, std::vector< TNode > > d_var_contains; /** triggers for each operator */ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; - /** helper for is intance of */ + /** helper for is instance of */ bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); public: /** compute var contains */ diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 45f161143..016abb2ac 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -291,7 +291,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { d_subtermsToEvaluate[result] = t.getNumChildren(); for (unsigned i = 0; i < t.getNumChildren(); ++ i) { if (isConstant(getNodeId(t[i]))) { - Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluatates " << t[i] << std::endl; + Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl; subtermEvaluates(result); } } @@ -390,7 +390,7 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) { } void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { - Debug("equality") << d_name << "::eq::mergePredicats(" << p << "," << q << ")" << std::endl; + Debug("equality") << d_name << "::eq::mergePredicates(" << p << "," << q << ")" << std::endl; assertEqualityInternal(p, q, reason); propagate(); } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 2373c7f9a..34cb2443f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -727,7 +727,7 @@ public: } /** - * Returns true if this kind is used for congruencce closure + evaluation of constants. + * Returns true if this kind is used for congruence closure + evaluation of constants. */ bool isInterpretedFunctionKind(Kind fun) const { return d_congruenceKindsInterpreted.tst(fun); diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index f993b941b..9caa8b1f1 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -282,7 +282,7 @@ enum FunctionApplicationType { struct FunctionApplication { /** Type of application */ FunctionApplicationType type; - /** The actuall application elements */ + /** The actual application elements */ EqualityNodeId a, b; /** Construct an application */ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 85d49f921..9a7878066 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -174,10 +174,6 @@ public: /** * Returns the Integer obtained by setting the ith bit of the * current Integer to 1. - * - * @param bit - * - * @return */ Integer setBit(uint32_t i) const { mpz_class res = d_value; diff --git a/test/regress/regress0/simple.smt2 b/test/regress/regress0/simple.smt2 deleted file mode 100644 index c1f65e565..000000000 --- a/test/regress/regress0/simple.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -(set-info :source "contrived") -(set-info :smt-lib-version 2.0) -(set-info :category "check") -(set-info :status unsat) -(set-logic QF_UF) -(set-info :notes |This benchmark simply checks that SMT-LIB v2 can be parsed.|) -(set-info :difficulty 0.000) -(exit)