diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 81 |
1 files changed, 42 insertions, 39 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b0681b1ff..750710769 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -73,7 +73,7 @@ Node TheoryStrings::TermIndex::add(TNode n, } return d_data; }else{ - Assert( index<n.getNumChildren() ); + Assert(index < n.getNumChildren()); TNode nir = s.getRepresentative(n[index]); //if it is empty, and doing CONCAT, ignore if( nir==er && n.getKind()==kind::STRING_CONCAT ){ @@ -164,8 +164,8 @@ TheoryStrings::~TheoryStrings() { } bool TheoryStrings::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_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS); TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS); @@ -585,8 +585,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) } else { - Assert(len_value.getConst<Rational>() <= Rational(String::maxSize()), - "Exceeded UINT32_MAX in string model"); + Assert(len_value.getConst<Rational>() <= Rational(String::maxSize())) + << "Exceeded UINT32_MAX in string model"; unsigned lvalue = len_value.getConst<Rational>().getNumerator().toUnsignedInt(); std::map<unsigned, Node>::iterator itvu = values_used.find(lvalue); @@ -668,8 +668,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Trace("strings-model") << std::endl; //use type enumerator - Assert(lts_values[i].getConst<Rational>() <= Rational(String::maxSize()), - "Exceeded UINT32_MAX in string model"); + Assert(lts_values[i].getConst<Rational>() <= Rational(String::maxSize())) + << "Exceeded UINT32_MAX in string model"; StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); for (const Node& eqc : pure_eq) { @@ -677,7 +677,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) std::map<Node, Node>::iterator itp = pure_eq_assign.find(eqc); if (itp == pure_eq_assign.end()) { - Assert( !sel.isFinished() ); + Assert(!sel.isFinished()); c = *sel; while (m->hasTerm(c)) { @@ -765,11 +765,11 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) for (const Node& n : nf.d_nf) { Node r = d_state.getRepresentative(n); - Assert( r.isConst() || processed.find( r )!=processed.end() ); + Assert(r.isConst() || processed.find(r) != processed.end()); nc.push_back(r.isConst() ? r : processed[r]); } Node cc = utils::mkNConcat(nc); - Assert( cc.getKind()==kind::CONST_STRING ); + Assert(cc.getKind() == kind::CONST_STRING); Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl; processed[nodes[i]] = cc; if (!m->assertEquality(nodes[i], cc, true)) @@ -1164,10 +1164,10 @@ void TheoryStrings::addCarePairs(TNodeTrie* t1, for (unsigned k = 0; 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_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS); @@ -1259,7 +1259,7 @@ void TheoryStrings::computeCareGraph(){ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl; - Assert(atom.getKind() != kind::OR, "Infer error: a split."); + Assert(atom.getKind() != kind::OR) << "Infer error: a split."; if( atom.getKind()==kind::EQUAL ){ Trace("strings-pending-debug") << " Register term" << std::endl; for( unsigned j=0; j<2; j++ ) { @@ -1369,7 +1369,7 @@ void TheoryStrings::checkInit() { } //explain equal components if( count[0]<nc.getNumChildren() ){ - Assert( count[1]<n.getNumChildren() ); + Assert(count[1] < n.getNumChildren()); if( nc[count[0]]!=n[count[1]] ){ exp.push_back( nc[count[0]].eqNode( n[count[1]] ) ); } @@ -1409,12 +1409,12 @@ void TheoryStrings::checkInit() { } else { - Assert( !foundNEmpty ); + Assert(!foundNEmpty); ns = n[i]; foundNEmpty = true; } } - AlwaysAssert( foundNEmpty ); + AlwaysAssert(foundNEmpty); //infer the equality d_im.sendInference(exp, n.eqNode(ns), "I_Norm_S"); } @@ -1492,7 +1492,7 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< if (!d_state.areEqual(n[count], vecc[countc])) { Node nrr = d_state.getRepresentative(n[count]); - Assert( !d_eqc_to_const_exp[nrr].isNull() ); + Assert(!d_eqc_to_const_exp[nrr].isNull()); d_im.addToExplanation(n[count], d_eqc_to_const_base[nrr], exp); exp.push_back( d_eqc_to_const_exp[nrr] ); } @@ -1505,7 +1505,7 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< } } //exp contains an explanation of n==c - Assert( countc==vecc.size() ); + Assert(countc == vecc.size()); if (d_state.hasTerm(c)) { d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE"); @@ -1722,7 +1722,7 @@ void TheoryStrings::checkExtfEval( int effort ) { } //if not reduced if( !to_reduce.isNull() ){ - Assert( effort<3 ); + Assert(effort < 3); if( effort==1 ){ Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl; } @@ -2445,7 +2445,7 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto } Trace("strings-error") << "Looping term should be congruent : " << n << " " << eqc << " " << ncy << std::endl; //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S) - Assert( false ); + Assert(false); }else{ return ncy; } @@ -2661,7 +2661,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc ) { } //construct the normal form - Assert( !normal_forms.empty() ); + Assert(!normal_forms.empty()); unsigned nf_index = 0; std::map<Node, unsigned>::iterator it = term_to_nf_index.find(eqc); // we prefer taking the normal form whose base is the equivalence @@ -2901,9 +2901,9 @@ void TheoryStrings::getNormalForms(Node eqc, Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl; //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] ) std::vector< Node > exp; - Assert( d_eqc_to_const_base.find( eqc )!=d_eqc_to_const_base.end() ); + Assert(d_eqc_to_const_base.find(eqc) != d_eqc_to_const_base.end()); d_im.addToExplanation(n, d_eqc_to_const_base[eqc], exp); - Assert( d_eqc_to_const_exp.find( eqc )!=d_eqc_to_const_exp.end() ); + Assert(d_eqc_to_const_exp.find(eqc) != d_eqc_to_const_exp.end()); if( !d_eqc_to_const_exp[eqc].isNull() ){ exp.push_back( d_eqc_to_const_exp[eqc] ); } @@ -3219,8 +3219,10 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, NormalForm& nfnc = nfiv[index].isConst() ? nfj : nfi; std::vector<Node>& nfncv = nfnc.d_nf; Node other_str = nfncv[index]; - Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." ); - Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." ); + Assert(other_str.getKind() != kind::CONST_STRING) + << "Other string is not constant."; + Assert(other_str.getKind() != kind::STRING_CONCAT) + << "Other string is not CONCAT."; if( !d_equalityEngine.areDisequal( other_str, d_emptyString, true ) ){ Node eq = other_str.eqNode( d_emptyString ); eq = Rewriter::rewrite(eq); @@ -3263,7 +3265,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, Node const_str = TheoryStringsRewriter::collectConstantStringAt( nfcv, index_c_k, false); - Assert( !const_str.isNull() ); + Assert(!const_str.isNull()); CVC4::String stra = const_str.getConst<String>(); CVC4::String strb = next_const_str.getConst<String>(); //since non-empty, we start with charecter #1 @@ -3428,7 +3430,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, } if( info_valid ){ pinfer.push_back( info ); - Assert( !success ); + Assert(!success); } } } @@ -3703,13 +3705,14 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { if( ret!=0 ) { return; }else{ - Assert( index<nfi.size() && index<nfj.size() ); + Assert(index < nfi.size() && index < nfj.size()); Node i = nfi[index]; Node j = nfj[index]; Trace("strings-solve-debug") << "...Processing(DEQ) " << i << " " << j << std::endl; if (!d_state.areEqual(i, j)) { - Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING ); + Assert(i.getKind() != kind::CONST_STRING + || j.getKind() != kind::CONST_STRING); std::vector< Node > lexp; Node li = d_state.getLength(i, lexp); Node lj = d_state.getLength(j, lexp); @@ -3835,7 +3838,7 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { index++; } } - Assert( false ); + Assert(false); } } @@ -3965,8 +3968,8 @@ void TheoryStrings::addNormalFormPair( Node n1, Node n2 ){ d_nf_pairs_data[n1][index] = n2; }else{ d_nf_pairs_data[n1].push_back( n2 ); - } - Assert( isNormalFormPair( n1, n2 ) ); + } + Assert(isNormalFormPair(n1, n2)); } else { Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl; } @@ -3981,9 +3984,9 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); if( it!=d_nf_pairs.end() ){ - Assert( d_nf_pairs_data.find( n1 )!=d_nf_pairs_data.end() ); + Assert(d_nf_pairs_data.find(n1) != d_nf_pairs_data.end()); for( int i=0; i<(*it).second; i++ ){ - Assert( i<(int)d_nf_pairs_data[n1].size() ); + Assert(i < (int)d_nf_pairs_data[n1].size()); if( d_nf_pairs_data[n1][i]==n2 ){ return true; } @@ -4489,7 +4492,7 @@ void TheoryStrings::separateByLength(std::vector< Node >& n, std::map< unsigned, std::vector< Node > > eqc_to_strings; for( unsigned i=0; i<n.size(); i++ ) { Node eqc = n[i]; - Assert( d_equalityEngine.getRepresentative(eqc)==eqc ); + Assert(d_equalityEngine.getRepresentative(eqc) == eqc); EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); Node lt = ei ? ei->d_lengthTerm : Node::null(); if( !lt.isNull() ){ @@ -4593,7 +4596,7 @@ Node TheoryStrings::ppRewrite(TNode atom) { } return ret; }else{ - Assert( new_nodes.empty() ); + Assert(new_nodes.empty()); } } return atom; @@ -4658,7 +4661,7 @@ bool TheoryStrings::hasStrategyEffort(Effort e) const void TheoryStrings::addStrategyStep(InferStep s, int effort, bool addBreak) { // must run check init first - Assert((s == CHECK_INIT)==d_infer_steps.empty()); + Assert((s == CHECK_INIT) == d_infer_steps.empty()); // must use check cycles when using flat forms Assert(s != CHECK_FLAT_FORMS || std::find(d_infer_steps.begin(), d_infer_steps.end(), CHECK_CYCLES) |