diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast_strategies.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/instantiator_tables_template.cpp | 2 | ||||
-rw-r--r-- | src/theory/rewriter_tables_template.h | 2 | ||||
-rw-r--r-- | src/theory/theory_traits_template.h | 5 | ||||
-rw-r--r-- | src/theory/type_enumerator_template.cpp | 3 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 22 |
8 files changed, 19 insertions, 23 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index 8cfdab5af..80b689b8c 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -100,7 +100,7 @@ void inline makeZero(Bits& bits, unsigned width) { * * @param a first term to be added * @param b second term to be added - * @param sum the sum + * @param res the result * @param carry the carry-in bit * * @return the carry-out diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h index 826b61d4f..5b53678dd 100644 --- a/src/theory/bv/bitblast_strategies.h +++ b/src/theory/bv/bitblast_strategies.h @@ -41,7 +41,6 @@ typedef std::vector<Node> Bits; * Default Atom Bitblasting strategies: * * @param node the atom to be bitblasted - * @param markerLit the marker literal corresponding to the atom * @param bb the bitblaster */ @@ -68,9 +67,8 @@ Node SleBB(TNode node, Bitblaster* bb); * Default Term Bitblasting strategies * * @param node the term to be bitblasted + * @param bits [output parameter] bits representing the new term * @param bb the bitblaster in which the clauses are added - * - * @return the bits representing the new term */ void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb); diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index c86f14398..eb5f3e155 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -170,7 +170,7 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) { /** * Asserts the clauses corresponding to the atom to the Sat Solver * by turning on the marker literal (i.e. setting it to false) - * @param node the atom to be aserted + * @param node the atom to be asserted * */ diff --git a/src/theory/instantiator_tables_template.cpp b/src/theory/instantiator_tables_template.cpp index 7a78c3aae..7234993fa 100644 --- a/src/theory/instantiator_tables_template.cpp +++ b/src/theory/instantiator_tables_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file instantiator_tables_template.cpp +/*! \file instantiator_tables.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 9ab98168e..6533e9335 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file rewriter_tables_template.h +/*! \file rewriter_tables.h ** \verbatim ** Original author: dejan ** Major contributors: mdeters diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index bbf13b425..4522af568 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_traits_template.h +/*! \file theory_traits.h ** \verbatim ** Original author: dejan ** Major contributors: mdeters @@ -27,7 +27,6 @@ ${theory_includes} namespace CVC4 { - namespace theory { template <TheoryId theoryId> @@ -37,5 +36,5 @@ ${theory_traits} ${theory_for_each_macro} -}/* theory namespace */ +}/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index 426bf52a0..0619a900f 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file type_enumerator_template.cpp +/*! \file type_enumerator.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -58,4 +58,3 @@ ${mk_type_enumerator_cases} }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7f216d634..1e3b276a4 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -58,7 +58,7 @@ public: /** * Notifies about a trigger equality that became true or false. * - * @param eq the equality that became true or false + * @param equality the equality that became true or false * @param value the value of the equality */ virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0; @@ -680,13 +680,13 @@ public: /** * Adds a predicate p with given polarity. The predicate asserted - * should be in the congruence closure kinds (otherwise it's + * should be in the congruence closure kinds (otherwise it's * useless. * * @param p the (non-negated) predicate - * @param polarity true if asserting the predicate, false if + * @param polarity true if asserting the predicate, false if * asserting the negated predicate - * @param the reason to keep for building explanations + * @param reason the reason to keep for building explanations */ void assertPredicate(TNode p, bool polarity, TNode reason); @@ -694,9 +694,9 @@ public: * Adds an equality eq with the given polarity to the database. * * @param eq the (non-negated) equality - * @param polarity true if asserting the equality, false if + * @param polarity true if asserting the equality, false if * asserting the negated equality - * @param the reason to keep for building explanations + * @param reason the reason to keep for building explanations */ void assertEquality(TNode eq, bool polarity, TNode reason); @@ -706,20 +706,20 @@ public: TNode getRepresentative(TNode t) const; /** - * Add all the terms where the given term appears as a first child + * Add all the terms where the given term appears as a first child * (directly or implicitly). */ 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 begin true of false. * Returns the reasons (added when asserting) that imply it * in the assertions vector. */ void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions) const; /** - * Get an explanation of the predicate being true or false. + * Get an explanation of the predicate being true or false. * Returns the reasons (added when asserting) that imply imply it * in the assertions vector. */ @@ -733,12 +733,12 @@ public: * it's own notification. * * @param t the trigger term - * @param tag tag for this trigger (do NOT use THEORY_LAST) + * @param theoryTag tag for this trigger (do NOT use THEORY_LAST) */ void addTriggerTerm(TNode t, TheoryId theoryTag); /** - * Returns true if t is a trigger term or in the same equivalence + * Returns true if t is a trigger term or in the same equivalence * class as some other trigger term. */ bool isTriggerTerm(TNode t, TheoryId theoryTag) const; |