From 14776d0aeb833a7e728a27af6ef545f20b495f7f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 16 Aug 2013 15:15:03 -0400 Subject: Documentation fixes, some code typo fixes, file perms, other minor things. --- 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 src/theory/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 ++-- 29 files changed, 182 insertions(+), 27 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 (limited to 'src/theory') 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& 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. */ -- cgit v1.2.3