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/uf | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 58 | ||||
-rw-r--r-- | src/theory/uf/cardinality_extension.h | 2 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 64 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_types.h | 2 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 18 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 4 |
9 files changed, 91 insertions, 71 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 87696ef5f..bb1e434f2 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -65,8 +65,8 @@ void Region::addRep( Node n ) { } void Region::takeNode( Region* r, Node n ){ - Assert( !hasRep( n ) ); - Assert( r->hasRep( n ) ); + Assert(!hasRep(n)); + Assert(r->hasRep(n)); //add representative setRep( n, true ); //take disequalities from r @@ -130,7 +130,7 @@ void Region::combine( Region* r ){ /** setEqual */ void Region::setEqual( Node a, Node b ){ - Assert( hasRep( a ) && hasRep( b ) ); + Assert(hasRep(a) && hasRep(b)); //move disequalities of b over to a for( int t=0; t<2; t++ ){ DiseqList* del = d_nodes[b]->get(t); @@ -181,7 +181,7 @@ void Region::setDisequal( Node n1, Node n2, int type, bool valid ){ } void Region::setRep( Node n, bool valid ) { - Assert( hasRep( n )!=valid ); + Assert(hasRep(n) != valid); if( valid && d_nodes.find( n )==d_nodes.end() ){ d_nodes[n] = new RegionNodeInfo( d_cf->d_thss->getSatContext() ); } @@ -189,7 +189,7 @@ void Region::setRep( Node n, bool valid ) { d_reps_size = d_reps_size + ( valid ? 1 : -1 ); //removing a member of the test clique from this region if( d_testClique.find( n ) != d_testClique.end() && d_testClique[n] ){ - Assert( !valid ); + Assert(!valid); d_testClique[n] = false; d_testCliqueSize = d_testCliqueSize - 1; //remove all splits involving n @@ -326,7 +326,7 @@ bool Region::check( Theory::Effort level, int cardinality, } } } - Assert( maxNode!=Node::null() ); + Assert(maxNode != Node::null()); newClique.push_back( maxNode ); } //check splits internal to new members @@ -540,7 +540,7 @@ void SortModel::newEqClass( Node n ){ if( d_regions_index<d_regions.size() ){ d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true); d_regions[ d_regions_index ]->setValid(true); - Assert(d_regions[d_regions_index]->getNumReps()==0); + Assert(d_regions[d_regions_index]->getNumReps() == 0); }else{ d_regions.push_back( new Region( this, d_thss->getSatContext() ) ); } @@ -564,8 +564,8 @@ void SortModel::merge( Node a, Node b ){ Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b << "..." << std::endl; if( a!=b ){ - Assert( d_regions_map.find( a )!=d_regions_map.end() ); - Assert( d_regions_map.find( b )!=d_regions_map.end() ); + Assert(d_regions_map.find(a) != d_regions_map.end()); + Assert(d_regions_map.find(b) != d_regions_map.end()); int ai = d_regions_map[a]; int bi = d_regions_map[b]; Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; @@ -636,8 +636,8 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ } d_disequalities_index = d_disequalities_index + 1; //now, add disequalities to regions - Assert( d_regions_map.find( a )!=d_regions_map.end() ); - Assert( d_regions_map.find( b )!=d_regions_map.end() ); + Assert(d_regions_map.find(a) != d_regions_map.end()); + Assert(d_regions_map.find(b) != d_regions_map.end()); Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; if( ai==bi ){ //internal disequality @@ -671,7 +671,7 @@ bool SortModel::areDisequal( Node a, Node b ) { /** check */ void SortModel::check( Theory::Effort level, OutputChannel* out ){ - Assert( options::ufssMode()==UF_SS_FULL ); + Assert(options::ufssMode() == UF_SS_FULL); if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){ Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type << std::endl; @@ -809,7 +809,7 @@ void SortModel::getDisequalitiesToRegions(int ri, DiseqList* del = it->second->get(0); for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){ if( (*it2).second ){ - Assert( isValid( d_regions_map[ (*it2).first ] ) ); + Assert(isValid(d_regions_map[(*it2).first])); //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl; regions_diseq[ d_regions_map[ (*it2).first ] ]++; } @@ -836,7 +836,7 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ << "Assert cardinality " << d_type << " " << c << " " << val << " level = " << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl; - Assert( c>0 ); + Assert(c > 0); Node cl = getCardinalityLiteral( c ); if( val ){ bool doCheckRegions = !d_hasCard; @@ -883,7 +883,7 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ void SortModel::checkRegion( int ri, bool checkCombine ){ if( isValid(ri) && d_hasCard ){ - Assert( d_cardinality>0 ); + Assert(d_cardinality > 0); if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){ ////alternatively, check if we can reduce the number of external disequalities by moving single nodes //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){ @@ -931,9 +931,9 @@ int SortModel::forceCombineRegion( int ri, bool useDensity ){ Debug("uf-ss-check-region") << it->first << " : " << it->second << std::endl; } for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){ - Assert( it->first!=ri ); - Assert( isValid( it->first ) ); - Assert( d_regions[ it->first ]->getNumReps()>0 ); + Assert(it->first != ri); + Assert(isValid(it->first)); + Assert(d_regions[it->first]->getNumReps() > 0); double tempScore = double(it->second)/double(d_regions[it->first]->getNumReps() ); if( tempScore>maxScore ){ maxRegion = it->first; @@ -959,7 +959,7 @@ int SortModel::combineRegions( int ai, int bi ){ } #endif Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl; - Assert( isValid( ai ) && isValid( bi ) ); + Assert(isValid(ai) && isValid(bi)); Region* region_bi = d_regions[bi]; for(Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it){ Region::RegionNodeInfo* rni = it->second; @@ -975,8 +975,8 @@ int SortModel::combineRegions( int ai, int bi ){ void SortModel::moveNode( Node n, int ri ){ Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl; - Assert( isValid( d_regions_map[ n ] ) ); - Assert( isValid( ri ) ); + Assert(isValid(d_regions_map[n])); + Assert(isValid(ri)); //move node to region ri d_regions[ri]->takeNode( d_regions[ d_regions_map[n] ], n ); d_regions_map[n] = ri; @@ -993,11 +993,11 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){ break; } } - Assert( s!=Node::null() ); + Assert(s != Node::null()); } if (!s.isNull() ){ //add lemma to output channel - Assert( s.getKind()==EQUAL ); + Assert(s.getKind() == EQUAL); Node ss = Rewriter::rewrite( s ); if( ss.getKind()!=EQUAL ){ Node b_t = NodeManager::currentNM()->mkConst( true ); @@ -1042,8 +1042,8 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){ - Assert( d_hasCard ); - Assert( d_cardinality>0 ); + Assert(d_hasCard); + Assert(d_cardinality > 0); while( clique.size()>size_t(d_cardinality+1) ){ clique.pop_back(); } @@ -1454,8 +1454,8 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) if( options::ufssMode()==UF_SS_FULL ){ if( lit.getKind()==CARDINALITY_CONSTRAINT ){ TypeNode tn = lit[0].getType(); - Assert( tn.isSort() ); - Assert( d_rep_model[tn] ); + Assert(tn.isSort()); + Assert(d_rep_model[tn]); int nCard = lit[1].getConst<Rational>().getNumerator().getSignedInt(); Node ct = d_rep_model[tn]->getCardinalityTerm(); Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl; @@ -1627,7 +1627,7 @@ void CardinalityExtension::check(Theory::Effort level) } }else{ // unhandled uf ss mode - Assert( false ); + Assert(false); } Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level << std::endl; @@ -1776,7 +1776,7 @@ void CardinalityExtension::initializeCombinedCardinality() /** check */ void CardinalityExtension::checkCombinedCardinality() { - Assert( options::ufssMode()==UF_SS_FULL ); + Assert(options::ufssMode() == UF_SS_FULL); if( options::ufssFairness() ){ Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl; int totalCombinedCard = 0; diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index 3e3d90be5..37d442968 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -76,7 +76,7 @@ class CardinalityExtension ~DiseqList(){} void setDisequal( Node n, bool valid ){ - Assert( (!isSet(n)) || getDisequalityValue(n) != valid ); + Assert((!isSet(n)) || getDisequalityValue(n) != valid); d_disequalities[ n ] = valid; d_size = d_size + ( valid ? 1 : -1 ); } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 32d32b479..8e0c96ae3 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -375,7 +375,7 @@ bool EqualityEngine::hasTerm(TNode t) const { } EqualityNodeId EqualityEngine::getNodeId(TNode node) const { - Assert(hasTerm(node), node.toString().c_str()); + Assert(hasTerm(node)) << node; return (*d_nodeIds.find(node)).second; } @@ -417,7 +417,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, un void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; - Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead"); + Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead"; assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid); propagate(); } @@ -556,8 +556,9 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Check for constant merges bool class1isConstant = d_isConstant[class1Id]; bool class2isConstant = d_isConstant[class2Id]; - Assert(class1isConstant || !class2isConstant, "Should always merge into constants"); - Assert(!class1isConstant || !class2isConstant, "Don't merge constants"); + Assert(class1isConstant || !class2isConstant) + << "Should always merge into constants"; + Assert(!class1isConstant || !class2isConstant) << "Don't merge constants"; // Trigger set of class 1 TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; @@ -884,7 +885,8 @@ void EqualityEngine::backtrack() { if (d_deducedDisequalities.size() > d_deducedDisequalitiesSize) { for(int i = d_deducedDisequalities.size() - 1, i_end = (int)d_deducedDisequalitiesSize; i >= i_end; -- i) { EqualityPair pair = d_deducedDisequalities[i]; - Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()); + Assert(d_disequalityReasonsMap.find(pair) + != d_disequalityReasonsMap.end()); // Remove from the map d_disequalityReasonsMap.erase(pair); std::swap(pair.first, pair.second); @@ -934,7 +936,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; // The terms must be there already - Assert(hasTerm(t1) && hasTerm(t2));; + Assert(hasTerm(t1) && hasTerm(t2)); + ; // Get the ids EqualityNodeId t1Id = getNodeId(t1); @@ -952,7 +955,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, // Get the reason for this disequality EqualityPair pair(t1Id, t2Id); - Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end(), "Don't ask for stuff I didn't notify you about"); + Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()) + << "Don't ask for stuff I didn't notify you about"; DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second; for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { @@ -1219,7 +1223,8 @@ void EqualityEngine::getExplanation( eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]); // The first child is a PARTIAL_SELECT_0. // Give it a child so that we know what kind of (read) it is, when we dump to LFSC. - Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0); + Assert(eqpc->d_children[0]->d_node.getKind() + == kind::PARTIAL_SELECT_0); Assert(eqpc->d_children[0]->d_children.size() == 0); eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, @@ -1241,7 +1246,7 @@ void EqualityEngine::getExplanation( Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode; const FunctionApplication& eq = d_applications[eqId].original; - Assert(eq.isEquality(), "Must be an equality"); + Assert(eq.isEquality()) << "Must be an equality"; // Explain why a = b constant Debug("equality") << push; @@ -1416,8 +1421,10 @@ void EqualityEngine::addTriggerEquality(TNode eq) { } void EqualityEngine::addTriggerPredicate(TNode predicate) { - Assert(predicate.getKind() != kind::NOT && predicate.getKind() != kind::EQUAL); - Assert(d_congruenceKinds.tst(predicate.getKind()), "No point in adding non-congruence predicates"); + Assert(predicate.getKind() != kind::NOT + && predicate.getKind() != kind::EQUAL); + Assert(d_congruenceKinds.tst(predicate.getKind())) + << "No point in adding non-congruence predicates"; if (d_done) { return; @@ -1811,7 +1818,8 @@ size_t EqualityEngine::getSize(TNode t) { void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) { // Currently we can only inform one callback per trigger - Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end()); + Assert(d_pathReconstructionTriggers.find(trigger) + == d_pathReconstructionTriggers.end()); d_pathReconstructionTriggers[trigger] = notify; } @@ -1993,7 +2001,7 @@ bool EqualityEngine::hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNode bool propagated = d_propagatedDisequalities.find(eq) != d_propagatedDisequalities.end(); #ifdef CVC4_ASSERTIONS bool stored = d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end(); - Assert(propagated == stored, "These two should be in sync"); + Assert(propagated == stored) << "These two should be in sync"; #endif Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (propagated ? "true" : "false") << std::endl; return propagated; @@ -2005,11 +2013,13 @@ bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId PropagatedDisequalitiesMap::const_iterator it = d_propagatedDisequalities.find(eq); if (it == d_propagatedDisequalities.end()) { - Assert(d_disequalityReasonsMap.find(eq) == d_disequalityReasonsMap.end(), "Why do we have a proof if not propagated"); + Assert(d_disequalityReasonsMap.find(eq) == d_disequalityReasonsMap.end()) + << "Why do we have a proof if not propagated"; Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => false" << std::endl; return false; } - Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end(), "We propagated but there is no proof"); + Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end()) + << "We propagated but there is no proof"; bool result = Theory::setContains(tag, (*it).second); Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (result ? "true" : "false") << std::endl; return result; @@ -2017,9 +2027,9 @@ bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) { - - Assert(!hasPropagatedDisequality(tag, lhsId, rhsId), "Check before you store it"); - Assert(lhsId != rhsId, "Wow, wtf!"); + Assert(!hasPropagatedDisequality(tag, lhsId, rhsId)) + << "Check before you store it"; + Assert(lhsId != rhsId) << "Wow, wtf!"; Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ")" << std::endl; @@ -2040,12 +2050,15 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs // Store the proof if provided if (d_deducedDisequalityReasons.size() > d_deducedDisequalityReasonsSize) { Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << "): storing proof" << std::endl; - Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end(), "There can't be a proof if you're adding a new one"); + Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end()) + << "There can't be a proof if you're adding a new one"; DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size()); #ifdef CVC4_ASSERTIONS // Check that the reasons are valid for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) { - Assert(getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind()); + Assert( + getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() + == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind()); } #endif if (Debug.isOn("equality::disequality")) { @@ -2065,7 +2078,8 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs d_disequalityReasonsMap[pair1] = ref; d_disequalityReasonsMap[pair2] = ref; } else { - Assert(d_disequalityReasonsMap.find(pair1) != d_disequalityReasonsMap.end(), "You must provide a proof initially"); + Assert(d_disequalityReasonsMap.find(pair1) != d_disequalityReasonsMap.end()) + << "You must provide a proof initially"; } } @@ -2073,7 +2087,11 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI // Must be empty on input Assert(out.size() == 0); // The class we are looking for, shouldn't have any of the tags we are looking for already set - Assert(d_nodeIndividualTrigger[classId] == null_set_id || Theory::setIntersection(getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags, inputTags) == 0); + Assert(d_nodeIndividualTrigger[classId] == null_set_id + || Theory::setIntersection( + getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags, + inputTags) + == 0); if (inputTags == 0) { return; @@ -2259,7 +2277,7 @@ EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee) Assert(d_ee->consistent()); d_current = d_start = d_ee->getNodeId(eqc); Assert(d_start == d_ee->getEqualityNode(d_start).getFind()); - Assert (!d_ee->d_isInternal[d_start]); + Assert(!d_ee->d_isInternal[d_start]); } Node EqClassIterator::operator*() const { diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 3813bb697..402b21a02 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -261,7 +261,7 @@ public: */ template<typename memory_class> void removeTopFromUseList(memory_class& memory) { - Assert ((int) d_useList == (int)memory.size() - 1); + Assert((int)d_useList == (int)memory.size() - 1); d_useList = memory.back().getNext(); memory.pop_back(); } diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 9c1d4c2f1..56d0c59cc 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -86,8 +86,7 @@ bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) { Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl; return false; } - Assert(t.isVar() && - n.isVar()); + Assert(t.isVar() && n.isVar()); t = find(t); n = find(n); Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl; @@ -720,7 +719,8 @@ void SymmetryBreaker::selectTerms(const Permutation& p) { Debug("ufsymm:eq") << "UFSYMM -- yep" << endl; } } - Assert(j != teq.end(), "failed to find a difference between p and teq ?!"); + Assert(j != teq.end()) + << "failed to find a difference between p and teq ?!"; } } } else { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 76e6e08bc..95e3f702b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -188,7 +188,7 @@ void TheoryUF::check(Effort level) { }/* TheoryUF::check() */ Node TheoryUF::getOperatorForApplyTerm( TNode node ) { - Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY ); + Assert(node.getKind() == kind::APPLY_UF || node.getKind() == kind::HO_APPLY); if( node.getKind()==kind::APPLY_UF ){ return node.getOperator(); }else{ @@ -197,7 +197,7 @@ Node TheoryUF::getOperatorForApplyTerm( TNode node ) { } unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) { - Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY ); + Assert(node.getKind() == kind::APPLY_UF || node.getKind() == kind::HO_APPLY); return node.getKind()==kind::APPLY_UF ? 0 : 1; } @@ -230,7 +230,7 @@ void TheoryUF::preRegisterTerm(TNode node) { // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() ); - Assert( node.getKind()!=kind::HO_APPLY || options::ufHo() ); + Assert(node.getKind() != kind::HO_APPLY || options::ufHo()); switch (node.getKind()) { case kind::EQUAL: @@ -507,8 +507,8 @@ void TheoryUF::addSharedTerm(TNode t) { } bool TheoryUF::areCareDisequal(TNode x, TNode y){ - Assert( d_equalityEngine.hasTerm(x) ); - Assert( d_equalityEngine.hasTerm(y) ); + Assert(d_equalityEngine.hasTerm(x)); + Assert(d_equalityEngine.hasTerm(y)); if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF); TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF); @@ -536,10 +536,10 @@ void TheoryUF::addCarePairs(TNodeTrie* t1, for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) { TNode x = f1[k]; TNode y = f2[k]; - Assert( d_equalityEngine.hasTerm(x) ); - Assert( d_equalityEngine.hasTerm(y) ); - Assert( !d_equalityEngine.areDisequal( x, y, false ) ); - Assert( !areCareDisequal( x, y ) ); + Assert(d_equalityEngine.hasTerm(x)); + Assert(d_equalityEngine.hasTerm(y)); + Assert(!d_equalityEngine.areDisequal(x, y, false)); + Assert(!areCareDisequal(x, y)); if( !d_equalityEngine.areEqual( x, y ) ){ if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF); diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index f279aebaf..ffe3730c4 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -91,7 +91,9 @@ Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node stk.push(val); val = val[2]; } while(val.getKind() == ITE); - AlwaysAssert(val == defaultValue, "default values don't match when constructing function definition!"); + AlwaysAssert(val == defaultValue) + << "default values don't match when constructing function " + "definition!"; while(!stk.empty()) { val = stk.top(); stk.pop(); diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index bad4189d6..7f4c1c164 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -160,7 +160,7 @@ public: public: //conversion between HO_APPLY AND APPLY_UF // converts an APPLY_UF to a curried HO_APPLY e.g. (f a b) becomes (@ (@ f a) b) static Node getHoApplyForApplyUf(TNode n) { - Assert( n.getKind()==kind::APPLY_UF ); + Assert(n.getKind() == kind::APPLY_UF); Node curr = n.getOperator(); for( unsigned i=0; i<n.getNumChildren(); i++ ){ curr = NodeManager::currentNM()->mkNode( kind::HO_APPLY, curr, n[i] ); @@ -169,7 +169,7 @@ public: //conversion between HO_APPLY AND APPLY_UF } // converts a curried HO_APPLY into an APPLY_UF e.g. (@ (@ f a) b) becomes (f a b) static Node getApplyUfForHoApply(TNode n) { - Assert( n.getType().getNumChildren()==2 ); + Assert(n.getType().getNumChildren() == 2); std::vector< TNode > children; TNode curr = decomposeHoApply( n, children, true ); // if operator is standard diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index cb373b535..f782cd618 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -145,13 +145,13 @@ class HoApplyTypeRule { // the typing rule for HO_APPLY terms inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert( n.getKind()==kind::HO_APPLY ); + Assert(n.getKind() == kind::HO_APPLY); TypeNode fType = n[0].getType(check); if (!fType.isFunction()) { throw TypeCheckingExceptionPrivate( n, "first argument does not have function type"); } - Assert( fType.getNumChildren()>=2 ); + Assert(fType.getNumChildren() >= 2); if (check) { TypeNode aType = n[1].getType(check); if( !aType.isSubtypeOf( fType[0] ) ){ |