diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/theory/arrays | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_info.cpp | 4 | ||||
-rw-r--r-- | src/theory/arrays/array_info.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/static_fact_manager.cpp | 14 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 39 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 3 | ||||
-rw-r--r-- | src/theory/arrays/union_find.cpp | 1 |
6 files changed, 36 insertions, 27 deletions
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 0d1095a23..3103f4ecc 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -134,7 +134,7 @@ void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{ void ArrayInfo::addIndex(const Node a, const TNode i) { Assert(a.getType().isArray()); - Assert(!i.getType().isArray()); // temporary for flat arrays + Assert(!i.getType().isArray()); // temporary for flat arrays Trace("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n"; CTNodeList* temp_indices; @@ -160,7 +160,7 @@ void ArrayInfo::addIndex(const Node a, const TNode i) { void ArrayInfo::addStore(const Node a, const TNode st){ Assert(a.getType().isArray()); - Assert(st.getKind()== kind::STORE); // temporary for flat arrays + Assert(st.getKind() == kind::STORE); // temporary for flat arrays CTNodeList* temp_store; Info* temp_info; diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 7e18f9ed2..982317350 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -78,7 +78,7 @@ public: * prints the information */ void print() const { - Assert(indices != NULL && stores!= NULL && in_stores != NULL); + Assert(indices != NULL && stores != NULL && in_stores != NULL); Trace("arrays-info")<<" indices "; printList(indices); Trace("arrays-info")<<" stores "; diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp index 63dfae173..546db649c 100644 --- a/src/theory/arrays/static_fact_manager.cpp +++ b/src/theory/arrays/static_fact_manager.cpp @@ -18,7 +18,7 @@ #include <iostream> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/node.h" #include "theory/arrays/static_fact_manager.h" @@ -97,7 +97,8 @@ void StaticFactManager::addEq(TNode eq) { // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b); // if(deq_ib != d_disequalities.end()) { // CTNodeListAlloc* deq = (*deq_ib).second; - // for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) { + // for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); + // j++) { // TNode deqn = *j; // TNode s = deqn[0]; // TNode t = deqn[1]; @@ -120,12 +121,11 @@ void StaticFactManager::addEq(TNode eq) { // */ // CTNodeListAlloc* deqa = (*deq_ia).second; - // for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) { + // for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); + // i++) { // TNode deqn = (*i); - // Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF); - // TNode s = deqn[0]; - // TNode t = deqn[1]; - // TNode sp = find(s); + // Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == + // kind::IFF); TNode s = deqn[0]; TNode t = deqn[1]; TNode sp = find(s); // TNode tp = find(t); // if(find(s) == find(t)) { diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 003bb0d68..f2beec0b8 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -189,7 +189,8 @@ void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) { bool TheoryArrays::ppDisequal(TNode a, TNode b) { bool termsExist = d_ppEqualityEngine.hasTerm(a) && d_ppEqualityEngine.hasTerm(b); - Assert(!termsExist || !a.isConst() || !b.isConst() || a == b || d_ppEqualityEngine.areDisequal(a, b, false)); + Assert(!termsExist || !a.isConst() || !b.isConst() || a == b + || d_ppEqualityEngine.areDisequal(a, b, false)); return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false)) || Rewriter::rewrite(a.eqNode(b)) == d_false); } @@ -621,14 +622,17 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) { Assert(pointer.isNull() == (weakEquivGetRep(n) == n)); Assert(!pointer.isNull() || secondary.isNull()); Assert(!index.isNull() || secondary.isNull()); - Assert(d_infoMap.getWeakEquivSecondaryReason(n).isNull() || !secondary.isNull()); + Assert(d_infoMap.getWeakEquivSecondaryReason(n).isNull() + || !secondary.isNull()); if (!pointer.isNull()) { if (index.isNull()) { Assert(d_equalityEngine.areEqual(n, pointer)); } else { - Assert((n.getKind() == kind::STORE && n[0] == pointer && n[1] == index) || - (pointer.getKind() == kind::STORE && pointer[0] == n && pointer[1] == index)); + Assert( + (n.getKind() == kind::STORE && n[0] == pointer && n[1] == index) + || (pointer.getKind() == kind::STORE && pointer[0] == n + && pointer[1] == index)); } } } @@ -694,7 +698,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) TNode s = *it; if (!d_infoMap.rIntro1Applied(s)) { d_infoMap.setRIntro1Applied(s); - Assert(s.getKind()==kind::STORE); + Assert(s.getKind() == kind::STORE); Node ni = nm->mkNode(kind::SELECT, s, s[1]); if (ni != node) { preRegisterTermInternal(ni); @@ -823,7 +827,8 @@ void TheoryArrays::preRegisterTermInternal(TNode node) } // Invariant: preregistered terms are exactly the terms in the equality engine // Disabled, see comment above for kind::EQUAL - // Assert(d_equalityEngine.hasTerm(node) || !d_equalityEngine.consistent()); + // Assert(d_equalityEngine.hasTerm(node) || + // !d_equalityEngine.consistent()); } @@ -915,7 +920,8 @@ void TheoryArrays::checkPair(TNode r1, TNode r2) if (r1[0] != r2[0]) { // If arrays are known to be disequal, or cannot become equal, we can continue - Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) && d_mayEqualEqualityEngine.hasTerm(r2[0])); + Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) + && d_mayEqualEqualityEngine.hasTerm(r2[0])); if (r1[0].getType() != r2[0].getType() || d_equalityEngine.areDisequal(r1[0], r2[0], false)) { Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl; @@ -976,7 +982,8 @@ void TheoryArrays::computeCareGraph() if (eqStatusArr != EQUALITY_UNKNOWN) { continue; } - Assert(d_valuation.getEqualityStatus((*it1), (*it2)) == EQUALITY_UNKNOWN); + Assert(d_valuation.getEqualityStatus((*it1), (*it2)) + == EQUALITY_UNKNOWN); addCarePair((*it1), (*it2)); ++d_numSharedArrayVarSplits; return; @@ -1133,7 +1140,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m) size_t it = 0; for(; it < instores->size(); ++it) { TNode instore = (*instores)[it]; - Assert(instore.getKind()==kind::STORE); + Assert(instore.getKind() == kind::STORE); if (termSet.find(instore) != termSet.end() && !d_equalityEngine.areEqual(instore[1],n[1])) { Node r = nm->mkNode(kind::SELECT, instore, n[1]); @@ -1203,7 +1210,8 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m) TypeNode valueType = nrep.getType().getArrayConstituentType(); rep = defaultValuesSet.nextTypeEnum(valueType); if (rep.isNull()) { - Assert(defaultValuesSet.getSet(valueType)->begin() != defaultValuesSet.getSet(valueType)->end()); + Assert(defaultValuesSet.getSet(valueType)->begin() + != defaultValuesSet.getSet(valueType)->end()); rep = *(defaultValuesSet.getSet(valueType)->begin()); } Trace("arrays-models") << "New default value = " << rep << endl; @@ -1558,7 +1566,8 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned explained.insert(t); } else { // EXT lemma - Assert(t[1].getKind() == kind::NOT && t[1][0].getKind() == kind::EQUAL); + Assert(t[1].getKind() == kind::NOT + && t[1][0].getKind() == kind::EQUAL); Assert(t[0].getKind() == kind::EQUAL); all.insert(t[0].notNode()); explained.insert(t); @@ -1618,7 +1627,7 @@ void TheoryArrays::setNonLinear(TNode a) // Propagate non-linearity down chain of stores for( ; it < st_a->size(); ++it) { TNode store = (*st_a)[it]; - Assert(store.getKind()==kind::STORE); + Assert(store.getKind() == kind::STORE); setNonLinear(store[0]); } @@ -1847,7 +1856,7 @@ void TheoryArrays::checkStore(TNode a) { d_infoMap.getInfo(a)->print(); } Assert(a.getType().isArray()); - Assert(a.getKind()==kind::STORE); + Assert(a.getKind() == kind::STORE); TNode b = a[0]; TNode i = a[1]; @@ -1898,7 +1907,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) for(; it < stores->size(); ++it) { TNode store = (*stores)[it]; - Assert(store.getKind()==kind::STORE); + Assert(store.getKind() == kind::STORE); TNode j = store[1]; if (i == j) continue; lem = std::make_tuple(store, store[0], j, i); @@ -1910,7 +1919,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) it = 0; for(; it < instores->size(); ++it) { TNode instore = (*instores)[it]; - Assert(instore.getKind()==kind::STORE); + Assert(instore.getKind() == kind::STORE); TNode j = instore[1]; if (i == j) continue; lem = std::make_tuple(instore, instore[0], j, i); diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 78756176d..223d742eb 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -218,7 +218,8 @@ struct ArraysProperties { struct ArrayPartialSelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::PARTIAL_SELECT_0 || n.getKind() == kind::PARTIAL_SELECT_1); + Assert(n.getKind() == kind::PARTIAL_SELECT_0 + || n.getKind() == kind::PARTIAL_SELECT_1); return nodeManager->integerType(); } };/* struct ArrayPartialSelectTypeRule */ diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp index af2cf3c3f..0afa94a8e 100644 --- a/src/theory/arrays/union_find.cpp +++ b/src/theory/arrays/union_find.cpp @@ -18,7 +18,6 @@ #include <iostream> -#include "base/cvc4_assert.h" #include "expr/node.h" #include "theory/arrays/union_find.h" |