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/quantifiers | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/quantifiers')
38 files changed, 374 insertions, 365 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 9d516de61..9e6e4842f 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -85,7 +85,7 @@ Node AlphaEquivalenceTypeNode::registerNode(Node q, while (index < typs.size()) { TypeNode curr = typs[index]; - Assert( typ_count.find( curr )!=typ_count.end() ); + Assert(typ_count.find(curr) != typ_count.end()); Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] "; aetn = &(aetn->d_children[curr][typ_count[curr]]); index = index + 1; @@ -96,7 +96,7 @@ Node AlphaEquivalenceTypeNode::registerNode(Node q, Node AlphaEquivalenceDb::addTerm(Node q) { - Assert( q.getKind()==FORALL ); + Assert(q.getKind() == FORALL); Trace("aeq") << "Alpha equivalence : register " << q << std::endl; //construct canonical quantified formula Node t = d_tc->getCanonicalTerm(q[1], true); diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index d972f2a1c..cdb15b349 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -37,7 +37,7 @@ struct sortTypeOrder { void QuantAntiSkolem::SkQuantTypeCache::add( std::vector< TypeNode >& typs, Node q, unsigned index ) { if( index==typs.size() ){ - Assert( std::find( d_quants.begin(), d_quants.end(), q )==d_quants.end() ); + Assert(std::find(d_quants.begin(), d_quants.end(), q) == d_quants.end()); d_quants.push_back( q ); }else{ d_children[typs[index]].add( typs, q, index+1 ); @@ -134,12 +134,12 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e) for( unsigned j=0; j<d_ask_types[q].size(); ){ TypeNode curr = d_ask_types[q][j]; for( unsigned k=0; k<indices[curr].size(); k++ ){ - Assert( d_ask_types[q][j]==curr ); + Assert(d_ask_types[q][j] == curr); d_ask_types_index[q].push_back( indices[curr][k] ); j++; } } - Assert( d_ask_types_index[q].size()==d_ask_types[q].size() ); + Assert(d_ask_types_index[q].size() == d_ask_types[q].size()); }else{ d_quant_sip.erase( q ); } @@ -158,7 +158,7 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e) } bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) { - Assert( !quants.empty() ); + Assert(!quants.empty()); std::sort( quants.begin(), quants.end() ); if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){ //partition into connected components @@ -190,7 +190,7 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool eqcs.push_back( func_to_eqc[f] ); } } - Assert( !eqcs.empty() ); + Assert(!eqcs.empty()); //merge equivalence classes int id = eqcs[0]; eqc_to_quant[id].push_back( q ); @@ -214,7 +214,7 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool if( eqc_to_quant.size()>1 ){ bool addedLemma = false; for( std::map< int, std::vector< Node > >::iterator it = eqc_to_quant.begin(); it != eqc_to_quant.end(); ++it ){ - Assert( it->second.size()<quants.size() ); + Assert(it->second.size() < quants.size()); bool ret = sendAntiSkolemizeLemma( it->second, false ); addedLemma = addedLemma || ret; } @@ -245,7 +245,7 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool std::vector< Node > subs_lhs; std::vector< Node > subs_rhs; //get outer variable substitution - Assert( d_ask_types_index[q].size()==d_ask_types[q].size() ); + Assert(d_ask_types_index[q].size() == d_ask_types[q].size()); std::vector<Node> sivars; d_quant_sip[q].getSingleInvocationVariables(sivars); for (unsigned j = 0, size = d_ask_types_index[q].size(); j < size; j++) diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index c52666dad..bed382e28 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -479,7 +479,7 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) if( tn.isReal() ){ vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache()); }else if( tn.isSort() ){ - Assert( options::quantEpr() ); + Assert(options::quantEpr()); vinst = new EprInstantiator(tn); }else if( tn.isDatatype() ){ vinst = new DtInstantiator(tn); @@ -622,7 +622,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) //get the instantiator object Assert(d_instantiator.find(pv) != d_instantiator.end()); Instantiator* vinst = d_instantiator[pv]; - Assert( vinst!=NULL ); + Assert(vinst != NULL); d_active_instantiators[pv] = vinst; vinst->reset(this, sf, pv, d_effort); // if d_effort is full, we must choose at least one model value @@ -656,7 +656,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) && d_qe->getLogicInfo().isLinear()) { Trace("cbqi-warn") << "Had to resort to model value." << std::endl; - Assert( false ); + Assert(false); } #endif Node mv = getModelValue( pv ); @@ -940,7 +940,7 @@ void CegInstantiator::pushStackVariable( Node v ) { } void CegInstantiator::popStackVariable() { - Assert( !d_stack_vars.empty() ); + Assert(!d_stack_vars.empty()); d_stack_vars.pop_back(); } @@ -961,11 +961,11 @@ bool CegInstantiator::constructInstantiationInc(Node pv, << ") "; Node mod_pv = pv_prop.getModifiedTerm( pv ); Trace("cbqi-inst-debug") << mod_pv << " -> " << n << std::endl; - Assert( n.getType().isSubtypeOf( pv.getType() ) ); + Assert(n.getType().isSubtypeOf(pv.getType())); } //must ensure variables have been computed for n computeProgVars( n ); - Assert( d_inelig.find( n )==d_inelig.end() ); + Assert(d_inelig.find(n) == d_inelig.end()); //substitute into previous substitutions, when applicable std::vector< Node > a_var; @@ -986,7 +986,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv, Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl; for( unsigned j=0; j<sf.d_subs.size(); j++ ){ Trace("cbqi-inst-debug2") << " Apply for " << sf.d_subs[j] << std::endl; - Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() ); + Assert(d_prog_var.find(sf.d_subs[j]) != d_prog_var.end()); if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){ prev_subs[j] = sf.d_subs[j]; TNode tv = pv; @@ -1016,14 +1016,17 @@ bool CegInstantiator::constructInstantiationInc(Node pv, // if previously was basic, becomes non-basic if( prev_basic && !sf.d_props[j].isBasic() ){ - Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), sf.d_vars[j] )==sf.d_non_basic.end() ); + Assert(std::find(sf.d_non_basic.begin(), + sf.d_non_basic.end(), + sf.d_vars[j]) + == sf.d_non_basic.end()); new_non_basic.push_back( sf.d_vars[j] ); sf.d_non_basic.push_back( sf.d_vars[j] ); } } if( sf.d_subs[j]!=prev_subs[j] ){ computeProgVars( sf.d_subs[j] ); - Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() ); + Assert(d_inelig.find(sf.d_subs[j]) == d_inelig.end()); } Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl; }else{ @@ -1088,7 +1091,7 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i) { std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]); - Assert( it!=subs_map.end() ); + Assert(it != subs_map.end()); Node n = it->second; Trace("cbqi-inst-debug") << " " << d_input_vars[i] << " -> " << n << std::endl; @@ -1144,7 +1147,7 @@ bool CegInstantiator::isEligibleForInstantiation(Node n) const } bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){ - Assert( d_prog_var.find( n )!=d_prog_var.end() ); + Assert(d_prog_var.find(n) != d_prog_var.end()); if( !non_basic.empty() ){ for (std::unordered_set<Node, NodeHashFunction>::iterator it = d_prog_var[n].begin(); @@ -1163,13 +1166,13 @@ bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& no Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) { computeProgVars( n ); - Assert( n==Rewriter::rewrite( n ) ); + Assert(n == Rewriter::rewrite(n)); bool is_basic = canApplyBasicSubstitution( n, non_basic ); if( Trace.isOn("cegqi-si-apply-subs-debug") ){ Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl; for( unsigned i=0; i<subs.size(); i++ ){ Trace("cegqi-si-apply-subs-debug") << " " << vars[i] << " -> " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl; - Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) ); + Assert(subs[i].getType().isSubtypeOf(vars[i].getType())); } } Node nret; @@ -1182,8 +1185,8 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node std::vector< Node > nsubs; for( unsigned i=0; i<vars.size(); i++ ){ if( !prop[i].d_coeff.isNull() ){ - Assert( vars[i].getType().isInteger() ); - Assert( prop[i].d_coeff.isConst() ); + Assert(vars[i].getType().isInteger()); + Assert(prop[i].d_coeff.isConst()); Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) ); nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn ); nn = Rewriter::rewrite( nn ); @@ -1238,7 +1241,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node if( !it->second.isNull() ){ c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); } - Assert( !c_coeff.isNull() ); + Assert(!c_coeff.isNull()); Node c; if( msum_term[it->first].isNull() ){ c = c_coeff; @@ -1285,7 +1288,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ - Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Assert(atom.getKind() != GEQ || atom[1].isConst()); Node atom_lhs; Node atom_rhs; if( atom.getKind()==GEQ ){ @@ -1512,7 +1515,7 @@ void CegInstantiator::processAssertions() { addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); }else{ Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl; - Assert( false ); + Assert(false); } } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 7f9c21a65..0ec87f239 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -121,7 +121,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) //add totality lemma std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); if( itc!=qepr->d_consts.end() ){ - Assert( !itc->second.empty() ); + Assert(!itc->second.empty()); Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); std::vector< Node > disj; for( unsigned j=0; j<itc->second.size(); j++ ){ @@ -131,10 +131,10 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl; d_quantEngine->getOutputChannel().lemma( tlem ); }else{ - Assert( false ); + Assert(false); } }else{ - Assert( !options::cbqiAll() ); + Assert(!options::cbqiAll()); } } } @@ -152,7 +152,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){ d_parent_quant[q].push_back( qi ); d_children_quant[qi].push_back( q ); - Assert( hasAddedCbqiLemma( qi ) ); + Assert(hasAddedCbqiLemma(qi)); Node qicel = getCounterexampleLiteral(qi); dep.push_back( qi ); dep.push_back( qicel ); @@ -221,7 +221,7 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ - Assert( hasAddedCbqiLemma( q ) ); + Assert(hasAddedCbqiLemma(q)); if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ d_active_quant[q] = true; Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; @@ -242,8 +242,8 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) //process from waitlist while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){ int index = d_nested_qe_waitlist_proc[q]; - Assert( index>=0 ); - Assert( index<(int)d_nested_qe_waitlist[q].size() ); + Assert(index >= 0); + Assert(index < (int)d_nested_qe_waitlist[q].size()); Node nq = d_nested_qe_waitlist[q][index]; Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts ); Node dqelem = nq.eqNode( nqeqn ); @@ -279,10 +279,10 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) } Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; for( unsigned i=0; i<ninner.size(); i++ ){ - Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() ); + Assert(d_active_quant.find(ninner[i]) != d_active_quant.end()); d_active_quant.erase( ninner[i] ); } - Assert( !d_active_quant.empty() ); + Assert(!d_active_quant.empty()); Trace("cbqi-debug") << "...done removing." << std::endl; } } @@ -293,7 +293,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) { if (quant_e == QEFFORT_STANDARD) { - Assert( !d_quantEngine->inConflict() ); + Assert(!d_quantEngine->inConflict()); double clSet = 0; if( Trace.isOn("cbqi-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); @@ -314,7 +314,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) } }else{ Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; - Assert( false ); + Assert(false); } } if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ @@ -490,9 +490,10 @@ Node InstStrategyCegqi::doNestedQENode( Trace("cbqi-nqe") << " " << ceq << std::endl; Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl; //should not contain quantifiers - Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) ); + Assert(!QuantifiersRewriter::containsQuantifiers(d_nested_qe[ceq])); } - Assert( d_quantEngine->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() ); + Assert(d_quantEngine->getTermUtil()->d_inst_constants[q].size() + == inst_terms.size()); //replace inst constants with instantiation Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(), d_quantEngine->getTermUtil()->d_inst_constants[q].end(), @@ -544,7 +545,7 @@ Node InstStrategyCegqi::doNestedQERec(Node q, d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() ); d_nested_qe_info[nr].d_doVts = doVts; //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true. - Assert( !options::cbqiInnermost() ); + Assert(!options::cbqiInnermost()); } } } @@ -665,7 +666,7 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q) } bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { - Assert( !d_curr_quant.isNull() ); + Assert(!d_curr_quant.isNull()); //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){ d_cbqi_set_quant_inactive = true; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 400db4a8e..bdab6810c 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -42,7 +42,7 @@ struct sortConjectureScore { void OpArgIndex::addTerm( std::vector< TNode >& terms, TNode n, unsigned index ){ if( index==n.getNumChildren() ){ - Assert( n.hasOperator() ); + Assert(n.hasOperator()); if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){ d_ops.push_back( n.getOperator() ); d_op_terms.push_back( n ); @@ -188,12 +188,12 @@ void ConjectureGenerator::setUniversalRelevant( TNode n ) { bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) { //prefer the one that is (normal, smaller) lexographically - Assert( d_pattern_is_relevant.find( rt1 )!=d_pattern_is_relevant.end() ); - Assert( d_pattern_is_relevant.find( rt2 )!=d_pattern_is_relevant.end() ); - Assert( d_pattern_is_normal.find( rt1 )!=d_pattern_is_normal.end() ); - Assert( d_pattern_is_normal.find( rt2 )!=d_pattern_is_normal.end() ); - Assert( d_pattern_fun_sum.find( rt1 )!=d_pattern_fun_sum.end() ); - Assert( d_pattern_fun_sum.find( rt2 )!=d_pattern_fun_sum.end() ); + Assert(d_pattern_is_relevant.find(rt1) != d_pattern_is_relevant.end()); + Assert(d_pattern_is_relevant.find(rt2) != d_pattern_is_relevant.end()); + Assert(d_pattern_is_normal.find(rt1) != d_pattern_is_normal.end()); + Assert(d_pattern_is_normal.find(rt2) != d_pattern_is_normal.end()); + Assert(d_pattern_fun_sum.find(rt1) != d_pattern_fun_sum.end()); + Assert(d_pattern_fun_sum.find(rt2) != d_pattern_fun_sum.end()); if( d_pattern_is_relevant[rt1] && !d_pattern_is_relevant[rt2] ){ Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl; @@ -271,7 +271,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){ assertEq = true; }else{ - Assert( eq_terms[i].getType()==tn ); + Assert(eq_terms[i].getType() == tn); registerPattern( eq_terms[i], tn ); if( isUniversalLessThan( eq_terms[i], t ) || ( options::conjectureUeeIntro() && d_pattern_fun_sum[t]>=d_pattern_fun_sum[eq_terms[i]] ) ){ setUniversalRelevant( eq_terms[i] ); @@ -409,8 +409,8 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) } ++eqcs_i; } - Assert( !d_bool_eqc[0].isNull() ); - Assert( !d_bool_eqc[1].isNull() ); + Assert(!d_bool_eqc[0].isNull()); + Assert(!d_bool_eqc[1].isNull()); d_urelevant_terms.clear(); Trace("sg-proc") << "...done get eq classes" << std::endl; @@ -675,7 +675,10 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) //add information about pattern Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl; - Assert( std::find( d_rel_patterns[tnn].begin(), d_rel_patterns[tnn].end(), nn )==d_rel_patterns[tnn].end() ); + Assert(std::find(d_rel_patterns[tnn].begin(), + d_rel_patterns[tnn].end(), + nn) + == d_rel_patterns[tnn].end()); d_rel_patterns[tnn].push_back( nn ); //build information concerning the variables in this pattern unsigned sum = 0; @@ -695,7 +698,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) d_rel_pattern_var_sum[nn] = sum; //register the pattern registerPattern( nn, tnn ); - Assert( d_pattern_is_normal[nn] ); + Assert(d_pattern_is_normal[nn]); Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl; //record information about types @@ -739,7 +742,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) Trace("sg-rel-term-debug") << " "; } Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second; - Assert( tindex+it2->first<gsubs_terms.size() ); + Assert(tindex + it2->first < gsubs_terms.size()); gsubs_terms[tindex+it2->first] = it2->second; } } @@ -787,7 +790,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) if( considerTermCanon( rhs, false ) ){ Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl; //register pattern - Assert( rhs.getType()==rt_types[i] ); + Assert(rhs.getType() == rt_types[i]); registerPattern( rhs, rt_types[i] ); if( rdepth<depth ){ //consider against all LHS at depth @@ -969,7 +972,7 @@ unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< } return sum; }else{ - Assert( pat.getNumChildren()==0 ); + Assert(pat.getNumChildren() == 0); funcs[pat]++; //for variables if( pat.getKind()==BOUND_VARIABLE ){ @@ -1009,8 +1012,8 @@ void ConjectureGenerator::registerPattern( Node pat, TypeNode tpat ) { d_patterns[TypeNode::null()].push_back( pat ); d_patterns[tpat].push_back( pat ); - Assert( d_pattern_fun_id.find( pat )==d_pattern_fun_id.end() ); - Assert( d_pattern_var_id.find( pat )==d_pattern_var_id.end() ); + Assert(d_pattern_fun_id.find(pat) == d_pattern_fun_id.end()); + Assert(d_pattern_var_id.find(pat) == d_pattern_var_id.end()); //collect functions std::map< TypeNode, unsigned > mnvn; @@ -1034,11 +1037,11 @@ bool ConjectureGenerator::isGeneralization( TNode patg, TNode pat, std::map< TNo return true; } }else{ - Assert( patg.hasOperator() ); + Assert(patg.hasOperator()); if( !pat.hasOperator() || patg.getOperator()!=pat.getOperator() ){ return false; }else{ - Assert( patg.getNumChildren()==pat.getNumChildren() ); + Assert(patg.getNumChildren() == pat.getNumChildren()); for( unsigned i=0; i<patg.getNumChildren(); i++ ){ if( !isGeneralization( patg[i], pat[i], subs ) ){ return false; @@ -1151,8 +1154,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< children.push_back( n.getOperator() ); for( unsigned i=0; i<(vec.size()-1); i++ ){ Node nn = te->getEnumerateTerm(types[i], vec[i]); - Assert( !nn.isNull() ); - Assert( nn.getType()==n[i].getType() ); + Assert(!nn.isNull()); + Assert(nn.getType() == n[i].getType()); children.push_back( nn ); } children.push_back( lc ); @@ -1233,7 +1236,7 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi } int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { - Assert( lhs.getType()==rhs.getType() ); + Assert(lhs.getType() == rhs.getType()); Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl; if( lhs==rhs ){ @@ -1288,7 +1291,7 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl; //find witness for counterexample, if possible if( options::conjectureFilterModel() ){ - Assert( d_rel_pattern_var_sum.find( lhs )!=d_rel_pattern_var_sum.end() ); + Assert(d_rel_pattern_var_sum.find(lhs) != d_rel_pattern_var_sum.end()); Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl; std::map< TNode, TNode > subs; d_subs_confirmCount = 0; @@ -1329,7 +1332,7 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode if( Trace.isOn("sg-cconj-debug") ){ Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs << ", based on substituion: " << std::endl; for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){ - Assert( getRepresentative( it->second )==it->second ); + Assert(getRepresentative(it->second) == it->second); Trace("sg-cconj-debug") << " " << it->first << " -> " << it->second << std::endl; } } @@ -1398,7 +1401,7 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode void TermGenerator::reset( TermGenEnv * s, TypeNode tn ) { - Assert( d_children.empty() ); + Assert(d_children.empty()); d_typ = tn; d_status = 0; d_status_num = 0; @@ -1496,14 +1499,14 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) { return s->considerCurrentTermCanon( d_id ) ? true : getNextTerm( s, depth ); //return true; }else{ - Assert( d_status_child_num<(int)s->d_func_args[f].size() ); + Assert(d_status_child_num < (int)s->d_func_args[f].size()); if( d_status_child_num==(int)d_children.size() ){ d_children.push_back( s->d_tg_id ); - Assert( s->d_tg_alloc.find( s->d_tg_id )==s->d_tg_alloc.end() ); + Assert(s->d_tg_alloc.find(s->d_tg_id) == s->d_tg_alloc.end()); s->d_tg_alloc[d_children[d_status_child_num]].reset( s, s->d_func_args[f][d_status_child_num] ); return getNextTerm( s, depth ); }else{ - Assert( d_status_child_num+1==(int)d_children.size() ); + Assert(d_status_child_num + 1 == (int)d_children.size()); if( s->d_tg_alloc[d_children[d_status_child_num]].getNextTerm( s, depth-1 ) ){ d_status_child_num++; return getNextTerm( s, depth ); @@ -1520,7 +1523,7 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) { }else if( d_status==1 || d_status==3 ){ if( d_status==1 ){ s->removeVar( d_typ ); - Assert( d_status_num==(int)s->d_var_id[d_typ] ); + Assert(d_status_num == (int)s->d_var_id[d_typ]); //check if there is only one feasible equivalence class. if so, don't make pattern any more specific. //unsigned i = s->d_ccand_eqc[0].size()-1; //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){ @@ -1533,7 +1536,7 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) { d_status_num = -1; return getNextTerm( s, depth ); }else{ - Assert( d_children.empty() ); + Assert(d_children.empty()); return false; } } @@ -1598,7 +1601,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, return false; } } - Assert( subs[d_typ].find( d_status_num )==subs[d_typ].end() ); + Assert(subs[d_typ].find(d_status_num) == subs[d_typ].end()); subs[d_typ][d_status_num] = eqc; return true; }else{ @@ -1612,9 +1615,9 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, }else if( d_status==2 ){ if( d_match_status==0 ){ d_match_status++; - Assert( d_status_num<(int)s->getNumTgVars( d_typ ) ); + Assert(d_status_num < (int)s->getNumTgVars(d_typ)); std::map< unsigned, TNode >::iterator it = subs[d_typ].find( d_status_num ); - Assert( it!=subs[d_typ].end() ); + Assert(it != subs[d_typ].end()); return it->second==eqc; }else{ return false; @@ -1630,7 +1633,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, if( d_match_status_child_num==0 ){ //initial binding TNode f = s->getTgFunc( d_typ, d_status_num ); - Assert( !eqc.isNull() ); + Assert(!eqc.isNull()); TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f); if( tat ){ d_match_children.push_back( tat->d_data.begin() ); @@ -1646,7 +1649,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, } } d_match_status++; - Assert( d_match_status_child_num+1==(int)d_match_children.size() ); + Assert(d_match_status_child_num + 1 == (int)d_match_children.size()); if( d_match_children[d_match_status_child_num]==d_match_children_end[d_match_status_child_num] ){ //no more arguments to bind d_match_children.pop_back(); @@ -1667,9 +1670,10 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, } } }else{ - Assert( d_match_status==1 ); - Assert( d_match_status_child_num+1==(int)d_match_children.size() ); - Assert( d_match_children[d_match_status_child_num]!=d_match_children_end[d_match_status_child_num] ); + Assert(d_match_status == 1); + Assert(d_match_status_child_num + 1 == (int)d_match_children.size()); + Assert(d_match_children[d_match_status_child_num] + != d_match_children_end[d_match_status_child_num]); d_match_status--; if( s->d_tg_alloc[d_children[d_match_status_child_num]].getNextMatch( s, d_match_children[d_match_status_child_num]->first, subs, rev_subs ) ){ d_match_status_child_num++; @@ -1681,7 +1685,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, } } } - Assert( false ); + Assert(false); return false; } @@ -1708,7 +1712,7 @@ unsigned TermGenerator::calculateGeneralizationDepth( TermGenEnv * s, std::map< } return sum; }else{ - Assert( d_status==2 || d_status==1 ); + Assert(d_status == 2 || d_status == 1); std::map< TypeNode, std::vector< int > >::iterator it = fvs.find( d_typ ); if( it!=fvs.end() ){ if( std::find( it->second.begin(), it->second.end(), d_status_num )!=it->second.end() ){ @@ -1731,7 +1735,7 @@ unsigned TermGenerator::getGeneralizationDepth( TermGenEnv * s ) { Node TermGenerator::getTerm( TermGenEnv * s ) { if( d_status==1 || d_status==2 ){ - Assert( !d_typ.isNull() ); + Assert(!d_typ.isNull()); return s->getFreeVar( d_typ, d_status_num ); }else if( d_status==5 ){ Node f = s->getTgFunc( d_typ, d_status_num ); @@ -1752,7 +1756,7 @@ Node TermGenerator::getTerm( TermGenEnv * s ) { return NodeManager::currentNM()->mkNode( s->d_func_kind[f], children ); } }else{ - Assert( false ); + Assert(false); } return Node::null(); } @@ -1833,7 +1837,7 @@ void TermGenEnv::collectSignatureInformation() { } void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) { - Assert( d_tg_alloc.empty() ); + Assert(d_tg_alloc.empty()); d_tg_alloc.clear(); if( genRelevant ){ @@ -1852,7 +1856,8 @@ void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) { bool TermGenEnv::getNextTerm() { if( d_tg_alloc[0].getNextTerm( this, d_tg_gdepth_limit ) ){ - Assert( (int)d_tg_alloc[0].getGeneralizationDepth( this )<=d_tg_gdepth_limit ); + Assert((int)d_tg_alloc[0].getGeneralizationDepth(this) + <= d_tg_gdepth_limit); if( (int)d_tg_alloc[0].getGeneralizationDepth( this )!=d_tg_gdepth_limit ){ return getNextTerm(); }else{ @@ -1919,7 +1924,7 @@ Node TermGenEnv::getFreeVar( TypeNode tn, unsigned i ) { } bool TermGenEnv::considerCurrentTerm() { - Assert( !d_tg_alloc.empty() ); + Assert(!d_tg_alloc.empty()); //if generalization depth is too large, don't consider it unsigned i = d_tg_alloc.size(); @@ -1954,10 +1959,10 @@ bool TermGenEnv::considerCurrentTerm() { Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC"; Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc[0][i-1].size() << "/" << d_ccand_eqc[1][i-1].size() << std::endl; - Assert( d_ccand_eqc[0].size()>=2 ); - Assert( d_ccand_eqc[0].size()==d_ccand_eqc[1].size() ); - Assert( d_ccand_eqc[0].size()==d_tg_id+1 ); - Assert( d_tg_id==d_tg_alloc.size() ); + Assert(d_ccand_eqc[0].size() >= 2); + Assert(d_ccand_eqc[0].size() == d_ccand_eqc[1].size()); + Assert(d_ccand_eqc[0].size() == d_tg_id + 1); + Assert(d_tg_id == d_tg_alloc.size()); for( unsigned r=0; r<2; r++ ){ d_ccand_eqc[r][i].clear(); } @@ -2018,13 +2023,13 @@ void TermGenEnv::changeContext( bool add ) { d_ccand_eqc[r].pop_back(); } d_tg_id--; - Assert( d_tg_alloc.find( d_tg_id )!=d_tg_alloc.end() ); + Assert(d_tg_alloc.find(d_tg_id) != d_tg_alloc.end()); d_tg_alloc.erase( d_tg_id ); } } bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){ - Assert( tg_id<d_tg_alloc.size() ); + Assert(tg_id < d_tg_alloc.size()); if( options::conjectureFilterCanonical() ){ //check based on a canonicity of the term (if there is one) Trace("sg-gen-tg-debug") << "Consider term canon "; @@ -2081,7 +2086,7 @@ void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars, if( i==vars.size() ){ d_var = eqc; }else{ - Assert( d_var.isNull() || d_var==vars[i] ); + Assert(d_var.isNull() || d_var == vars[i]); d_var = vars[i]; d_children[terms[i]].addSubstitution( eqc, vars, terms, i+1 ); } @@ -2089,10 +2094,10 @@ void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars, bool SubstitutionIndex::notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i ) { if( i==numVars ){ - Assert( d_children.empty() ); + Assert(d_children.empty()); return s->notifySubstitution( d_var, subs, rhs ); }else{ - Assert( i==0 || !d_children.empty() ); + Assert(i == 0 || !d_children.empty()); for( std::map< TNode, SubstitutionIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ Trace("sg-cconj-debug2") << "Try " << d_var << " -> " << it->first << " (" << i << "/" << numVars << ")" << std::endl; subs[d_var] = it->first; @@ -2130,9 +2135,9 @@ void TheoremIndex::addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std: lhs_arg.push_back( 0 ); d_children[curr.getOperator()].addTheorem( lhs_v, lhs_arg, rhs ); }else{ - Assert( curr.getKind()==kind::BOUND_VARIABLE ); + Assert(curr.getKind() == kind::BOUND_VARIABLE); TypeNode tn = curr.getType(); - Assert( d_var[tn].isNull() || d_var[tn]==curr ); + Assert(d_var[tn].isNull() || d_var[tn] == curr); d_var[tn] = curr; d_children[curr].addTheorem( lhs_v, lhs_arg, rhs ); } @@ -2180,7 +2185,7 @@ void TheoremIndex::getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, std::map< TypeNode, TNode >::iterator itt = d_var.find( tn ); if( itt!=d_var.end() ){ Trace("thm-db-debug") << "Check for substitution with " << itt->second << "..." << std::endl; - Assert( curr.getType()==itt->second.getType() ); + Assert(curr.getType() == itt->second.getType()); //add to substitution if possible bool success = false; std::map< TNode, TNode >::iterator it = smap.find( itt->second ); diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 3be1d4a4b..3a075ec8a 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -40,7 +40,7 @@ CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat) d_mode(cand_term_none) { d_op = qe->getTermDatabase()->getMatchOperator( pat ); - Assert( !d_op.isNull() ); + Assert(!d_op.isNull()); } void CandidateGeneratorQE::resetInstantiationRound(){ @@ -130,8 +130,7 @@ Node CandidateGeneratorQE::getNextCandidate(){ CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : CandidateGenerator( qe ), d_match_pattern( mpat ){ - - Assert( d_match_pattern.getKind()==EQUAL ); + Assert(d_match_pattern.getKind() == EQUAL); d_match_pattern_type = d_match_pattern[0].getType(); } @@ -161,7 +160,7 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : CandidateGenerator( qe ), d_match_pattern( mpat ){ d_match_pattern_type = mpat.getType(); - Assert( mpat.getKind()==INST_CONSTANT ); + Assert(mpat.getKind() == INST_CONSTANT); d_f = quantifiers::TermUtil::getInstConstAttr( mpat ); d_index = mpat.getAttribute(InstVarNumAttribute()); d_firstTime = false; diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 9e76a6a31..e639dc446 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -43,7 +43,7 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ d_cg = NULL; d_needsReset = true; d_active_add = true; - Assert( quantifiers::TermUtil::hasInstConstAttr(pat) ); + Assert(quantifiers::TermUtil::hasInstConstAttr(pat)); d_pattern = pat; d_match_pattern = pat; d_match_pattern_type = pat.getType(); @@ -258,7 +258,7 @@ int InstMatchGenerator::getMatch( { Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; - Assert( !d_match_pattern.isNull() ); + Assert(!d_match_pattern.isNull()); if (d_cg == nullptr) { Trace("matching-fail") << "Internal error for match generator." << std::endl; @@ -270,10 +270,12 @@ int InstMatchGenerator::getMatch( //InstMatch prev( &m ); std::vector< int > prev; //if t is null - Assert( !t.isNull() ); - Assert( !quantifiers::TermUtil::hasInstConstAttr(t) ); - Assert( d_match_pattern.getKind()==INST_CONSTANT || t.getKind()==d_match_pattern.getKind() ); - Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() ); + Assert(!t.isNull()); + Assert(!quantifiers::TermUtil::hasInstConstAttr(t)); + Assert(d_match_pattern.getKind() == INST_CONSTANT + || t.getKind() == d_match_pattern.getKind()); + Assert(!Trigger::isAtomicTrigger(d_match_pattern) + || t.getOperator() == d_match_pattern.getOperator()); //first, check if ground arguments are not equal, or a match is in conflict Trace("matching-debug2") << "Setting immediate matches..." << std::endl; for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++) @@ -338,7 +340,7 @@ int InstMatchGenerator::getMatch( if( t.getType().isBoolean() ){ t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermUtil()->d_true, t ) ); }else{ - Assert( t.getType().isReal() ); + Assert(t.getType().isReal()); t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one); } }else if( pat.getKind()==GEQ ){ @@ -467,7 +469,7 @@ int InstMatchGenerator::getNextMatch(Node f, //if t not null, try to fit it into match m if( !t.isNull() ){ if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){ - Assert( t.getType().isComparableTo( d_match_pattern_type ) ); + Assert(t.getType().isComparableTo(d_match_pattern_type)); Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl; success = getMatch(f, t, m, qe, tparent); if( d_independent_gen && success<0 ){ @@ -533,11 +535,11 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, } InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) { - Assert( pats.size()>1 ); + Assert(pats.size() > 1); InstMatchGeneratorMultiLinear * imgm = new InstMatchGeneratorMultiLinear( q, pats, qe ); std::vector< InstMatchGenerator* > gens; imgm->initialize(q, qe, gens); - Assert( gens.size()==pats.size() ); + Assert(gens.size() == pats.size()); std::vector< Node > patsn; std::map< Node, InstMatchGenerator * > pat_map_init; for( unsigned i=0; i<gens.size(); i++ ){ @@ -704,7 +706,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto for( unsigned i=0; i<pats_ordered.size(); i++ ){ Trace("multi-trigger-linear") << "...make for " << pats_ordered[i] << std::endl; InstMatchGenerator* cimg = getInstMatchGenerator(q, pats_ordered[i]); - Assert( cimg!=NULL ); + Assert(cimg != NULL); d_children.push_back( cimg ); if( i==0 ){ //TODO : improve cimg->setIndependent(); @@ -722,7 +724,7 @@ int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){ } bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) { - Assert( eqc.isNull() ); + Assert(eqc.isNull()); if( options::multiTriggerLinear() ){ return true; }else{ @@ -744,7 +746,7 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, } } Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl; - Assert( d_next!=NULL ); + Assert(d_next != NULL); int ret_val = continueNextMatch(q, m, qe, tparent); if( ret_val>0 ){ Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl; @@ -924,7 +926,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, int endChildIndex, bool modEq) { - Assert( !qe->inConflict() ); + Assert(!qe->inConflict()); if( childIndex==endChildIndex ){ // m is an instantiation if (sendInstantiation(tparent, m)) @@ -1036,9 +1038,9 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q, if( d_match_pattern.getKind()==EQUAL ){ d_eqc = d_match_pattern[1]; d_match_pattern = d_match_pattern[0]; - Assert( !quantifiers::TermUtil::hasInstConstAttr( d_eqc ) ); + Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc)); } - Assert( Trigger::isSimpleTrigger( d_match_pattern ) ); + Assert(Trigger::isSimpleTrigger(d_match_pattern)); for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){ if( d_match_pattern[i].getKind()==INST_CONSTANT ){ if( !options::cbqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){ @@ -1105,7 +1107,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; if (argIndex == d_match_pattern.getNumChildren()) { - Assert( !tat->d_data.empty() ); + Assert(!tat->d_data.empty()); TNode t = tat->getData(); Debug("simple-trigger") << "Actual term is " << t << std::endl; //convert to actual used terms @@ -1135,7 +1137,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, Node t = tt.first; Node prev = m.get( v ); //using representatives, just check if equal - Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) ); + Assert( + t.getType().isComparableTo(d_match_pattern_arg_types[argIndex])); if( prev.isNull() || prev==t ){ m.setValue( v, t); addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second)); diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 876e4e369..3420f282d 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -125,7 +125,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ } void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ - Assert( pat.getKind()==INST_PATTERN ); + Assert(pat.getKind() == INST_PATTERN); //add to generators bool usable = true; std::vector< Node > nodes; @@ -308,7 +308,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( Trace.isOn("auto-gen-trigger-debug") ){ Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; for( unsigned i=0; i<patTermsF.size(); i++ ){ - Assert( tinfo.find( patTermsF[i] )!=tinfo.end() ); + Assert(tinfo.find(patTermsF[i]) != tinfo.end()); Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl; Trace("auto-gen-trigger-debug2") << " info = [" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl; } @@ -320,7 +320,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ std::map< Node, bool > rmPatTermsF; int last_weight = -1; for( unsigned i=0; i<patTermsF.size(); i++ ){ - Assert( patTermsF[i].getKind()!=NOT ); + Assert(patTermsF[i].getKind() != NOT); bool newVar = false; for( unsigned j=0; j<tinfo[ patTermsF[i] ].d_fv.size(); j++ ){ if( vcMap.find( tinfo[ patTermsF[i] ].d_fv[j] )==vcMap.end() ){ @@ -362,17 +362,17 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl; Node mpat = pat; //process the pattern: if it has a required polarity, consider it - Assert( tinfo.find( pat )!=tinfo.end() ); + Assert(tinfo.find(pat) != tinfo.end()); int rpol = tinfo[pat].d_reqPol; Node rpoleq = tinfo[pat].d_reqPolEq; unsigned num_fv = tinfo[pat].d_fv.size(); Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl; if( rpol!=0 ){ - Assert( rpol==1 || rpol==-1 ); + Assert(rpol == 1 || rpol == -1); if( Trigger::isRelationalTrigger( pat ) ){ pat = rpol==-1 ? pat.negate() : pat; }else{ - Assert( Trigger::isAtomicTrigger( pat ) ); + Assert(Trigger::isAtomicTrigger(pat)); if( pat.getType().isBoolean() && rpoleq.isNull() ){ if( options::literalMatchMode()==LITERAL_MATCH_USE ){ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); @@ -380,7 +380,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) ); } }else{ - Assert( !rpoleq.isNull() ); + Assert(!rpoleq.isNull()); if( rpol==-1 ){ if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){ //all equivalence classes except rpoleq @@ -436,8 +436,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ sortQuantifiersForSymbol sqfs; sqfs.d_quant_rel = d_quant_rel; for( unsigned i=0; i<patTerms.size(); i++ ){ - Assert( d_pat_to_mpat.find( patTerms[i] )!=d_pat_to_mpat.end() ); - Assert( d_pat_to_mpat[patTerms[i]].hasOperator() ); + Assert(d_pat_to_mpat.find(patTerms[i]) != d_pat_to_mpat.end()); + Assert(d_pat_to_mpat[patTerms[i]].hasOperator()); sqfs.d_op_map[ patTerms[i] ] = d_pat_to_mpat[patTerms[i]].getOperator(); } //sort based on # occurrences (this will cause Trigger to select rarer symbols) @@ -591,7 +591,7 @@ bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) { } void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) { - Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 ); + Assert(pat.getKind() == INST_NO_PATTERN && pat.getNumChildren() == 1); if( std::find( d_user_no_gen[q].begin(), d_user_no_gen[q].end(), pat[0] )==d_user_no_gen[q].end() ){ Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl; d_user_no_gen[q].push_back( pat[0] ); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 2fe28fc61..23b1ff6c9 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -145,7 +145,7 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); doInstantiationRound( e ); if( d_quantEngine->inConflict() ){ - Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting ); + Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting); Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; }else if( d_quantEngine->hasAddedLemma() ){ Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 201aad3a0..f539bccf5 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -144,7 +144,7 @@ bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_var bool foundVar = false; for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){ Node v = varContains[ temp[i] ][j]; - Assert( quantifiers::TermUtil::getInstConstAttr(v)==q ); + Assert(quantifiers::TermUtil::getInstConstAttr(v) == q); if( vars.find( v )==vars.end() ){ varCount++; vars[ v ] = true; @@ -282,7 +282,7 @@ bool Trigger::isUsable( Node n, Node q ){ } Node Trigger::getIsUsableEq( Node q, Node n ) { - Assert( isRelationalTrigger( n ) ); + Assert(isRelationalTrigger(n)); for( unsigned i=0; i<2; i++) { if( isUsableEqTerms( q, n[i], n[1-i] ) ){ if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){ @@ -451,8 +451,8 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod } } if( !nu.isNull() ){ - Assert( nu==n ); - Assert( nu.getKind()!=NOT ); + Assert(nu == n); + Assert(nu.getKind() != NOT); Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl; Node reqEq; if( nu.getKind()==EQUAL ){ @@ -463,8 +463,9 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod nu = nu[0]; } } - Assert( reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr( reqEq ) ); - Assert( isUsableTrigger( nu, q ) ); + Assert(reqEq.isNull() + || !quantifiers::TermUtil::hasInstConstAttr(reqEq)); + Assert(isUsableTrigger(nu, q)); //tinfo.find( nu )==tinfo.end() Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl; tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq ); @@ -484,7 +485,7 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod bool rm_nu = false; for( unsigned i=0; i<added2.size(); i++ ){ Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl; - Assert( added2[i]!=nu ); + Assert(added2[i] != nu); // if child was not already removed if( tinfo.find( added2[i] )!=tinfo.end() ){ if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ @@ -839,7 +840,7 @@ Node Trigger::getInversion( Node n, Node x ) { if( n.getKind()==PLUS ){ x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] ); }else if( n.getKind()==MULT ){ - Assert( n[i].isConst() ); + Assert(n[i].isConst()); if( x.getType().isInteger() ){ Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() ); if( !n[i].getConst<Rational>().abs().isOne() ){ diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index ef80af5f5..66745c94a 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -97,7 +97,7 @@ Node EqualityInference::getMaster( Node t, EqcInfo * eqc, bool& updated, Node ne return t; } }else{ - Assert( d_eqci.find( eqc->d_master.get() )!=d_eqci.end() ); + Assert(d_eqci.find(eqc->d_master.get()) != d_eqci.end()); EqcInfo * eqc_m = d_eqci[eqc->d_master.get()]; Node m = getMaster( eqc->d_master.get(), eqc_m, updated, new_m ); eqc->d_master = m; @@ -141,7 +141,7 @@ void EqualityInference::eqNotifyNewClass(TNode t) { }else{ eqci = itec->second; } - Assert( !eqci->d_valid.get() ); + Assert(!eqci->d_valid.get()); if( !eqci->d_solved.get() ){ //somewhat strange: t may not be in rewritten form Node r = Rewriter::rewrite( t ); @@ -160,16 +160,16 @@ void EqualityInference::eqNotifyNewClass(TNode t) { BoolMap::const_iterator itv = d_elim_vars.find( n ); if( itv!=d_elim_vars.end() ){ changed = true; - Assert( d_eqci.find( n )!=d_eqci.end() ); - Assert( n!=t ); - Assert( d_eqci[n]->d_solved.get() ); + Assert(d_eqci.find(n) != d_eqci.end()); + Assert(n != t); + Assert(d_eqci[n]->d_solved.get()); Trace("eq-infer-debug2") << "......its solved form is " << d_eqci[n]->d_rep.get() << std::endl; if( d_trackExplain ){ //track the explanation: justified by explanation for each substitution addToExplanationEqc( exp, n ); } n = d_eqci[n]->d_rep; - Assert( !n.isNull() ); + Assert(!n.isNull()); } if( it->second.isNull() ){ children.push_back( n ); @@ -177,7 +177,7 @@ void EqualityInference::eqNotifyNewClass(TNode t) { children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) ); } }else{ - Assert( !it->second.isNull() ); + Assert(!it->second.isNull()); children.push_back( it->second ); } } @@ -275,8 +275,8 @@ void EqualityInference::setEqcRep( Node t, Node r, std::vector< Node >& exp_to_a } void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { - Assert( !t1.isNull() ); - Assert( !t2.isNull() ); + Assert(!t1.isNull()); + Assert(!t2.isNull()); std::map< Node, EqcInfo * >::iterator itv1 = d_eqci.find( t1 ); if( itv1!=d_eqci.end() ){ std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 ); @@ -324,7 +324,7 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { { Node v_value = veq[1]; Trace("eq-infer") << "...solved " << v_solve << " == " << v_value << std::endl; - Assert( d_elim_vars.find( v_solve )==d_elim_vars.end() ); + Assert(d_elim_vars.find(v_solve) == d_elim_vars.end()); d_elim_vars[v_solve] = true; //store value in eqc info EqcInfo * eqci_solved; diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index bb0306c06..f7fd13d4d 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -105,7 +105,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, if( r.getType().isSort() ){ Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; //should never happen : UF constants should never escape model - Assert( false ); + Assert(false); } } } @@ -165,7 +165,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, d_rep_score[ r_best ] = d_reset_count; } Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl; - Assert( r_best.getType().isSubtypeOf( v_tn ) ); + Assert(r_best.getType().isSubtypeOf(v_tn)); v_int_rep[r] = r_best; if( r_best!=a ){ Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; @@ -193,7 +193,7 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N eqc.push_back( a ); } //a should be in its equivalence class - Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() ); + Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end()); } TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) { @@ -243,7 +243,7 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n, //score prefers earliest use of this term as a representative return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; }else{ - Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH ); + Assert(options::quantRepMode() == quantifiers::QUANT_REP_MODE_DEPTH); return quantifiers::TermUtil::getTermDepth( n ); } } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 4b8b65697..bfef42b65 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -46,7 +46,7 @@ void FirstOrderModel::assertQuantifier( Node n ){ if( n.getKind()==FORALL ){ d_forall_asserts.push_back( n ); }else if( n.getKind()==NOT ){ - Assert( n[0].getKind()==FORALL ); + Assert(n[0].getKind() == FORALL); } } @@ -58,7 +58,7 @@ Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) { if( !ordered ){ return d_forall_asserts[i]; }else{ - Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() ); + Assert(d_forall_rlv_assert.size() == d_forall_asserts.size()); return d_forall_rlv_assert[i]; } } @@ -186,7 +186,7 @@ void FirstOrderModel::reset_round() { } } Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl; - Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() ); + Assert(d_forall_rlv_assert.size() == d_forall_asserts.size()); }else{ for( unsigned i=0; i<d_forall_asserts.size(); i++ ){ d_forall_rlv_assert.push_back( d_forall_asserts[i] ); @@ -225,7 +225,7 @@ bool FirstOrderModel::isQuantifierActive(TNode q) const bool FirstOrderModel::isQuantifierAsserted(TNode q) const { - Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() ); + Assert(d_forall_rlv_assert.size() == d_forall_asserts.size()); return std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )!=d_forall_rlv_assert.end(); } @@ -395,7 +395,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { Node v = d_models[op]->d_value[i]; Trace("fmc-model-func") << "Value is : " << v << std::endl; - Assert( v.isConst() ); + Assert(v.isConst()); /* if( !hasTerm( v ) ){ //can happen when the model basis term does not exist in ground assignment @@ -431,7 +431,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); } } - Assert( !children.empty() ); + Assert(!children.empty()); Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); Trace("fmc-model-func") << "condition : " << cc << ", value : " << v << std::endl; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 87f0b1ffe..c6800b092 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -167,7 +167,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol, conj = TermUtil::simpleNegate( conj ); } Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl; - Assert( conj.getKind()==AND ); + Assert(conj.getKind() == AND); Node v; std::vector< Node > v_cases; bool success = true; @@ -199,7 +199,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol, bound_lit_type_map[v] = BOUND_FIXED_SET; bound_lit_map[3][v] = n; bound_lit_pol_map[3][v] = pol; - Assert( v_cases.size()==1 ); + Assert(v_cases.size() == 1); bound_fixed_set[v].clear(); bound_fixed_set[v].push_back( v_cases[0] ); } @@ -266,7 +266,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol, } } }else{ - Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT ); + Assert(n.getKind() != LEQ && n.getKind() != LT && n.getKind() != GT); } } @@ -335,7 +335,8 @@ void BoundedIntegers::checkOwnership(Node f) setBoundVar = true; for( unsigned b=0; b<2; b++ ){ //set the bounds - Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() ); + Assert(bound_int_range_term[b].find(v) + != bound_int_range_term[b].end()); d_bounds[b][f][v] = bound_int_range_term[b][v]; } Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]); @@ -396,7 +397,7 @@ void BoundedIntegers::checkOwnership(Node f) } else { - Assert( it->second!=BOUND_INT_RANGE ); + Assert(it->second != BOUND_INT_RANGE); } } } @@ -424,7 +425,7 @@ void BoundedIntegers::checkOwnership(Node f) for( unsigned i=0; i<f[0].getNumChildren(); i++) { Node v = f[0][i]; if( std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end() ){ - Assert( d_bound_type[f].find( v )!=d_bound_type[f].end() ); + Assert(d_bound_type[f].find(v) != d_bound_type[f].end()); if( d_bound_type[f][v]==BOUND_INT_RANGE ){ Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl; }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){ @@ -446,7 +447,7 @@ void BoundedIntegers::checkOwnership(Node f) Trace("bound-int") << " " << v << " has small finite type." << std::endl; }else{ Trace("bound-int") << " " << v << " has unknown bound." << std::endl; - Assert( false ); + Assert(false); } }else{ Trace("bound-int") << " " << "*** " << v << " is unbounded." << std::endl; @@ -470,7 +471,7 @@ void BoundedIntegers::checkOwnership(Node f) std::map< Node, Node >::iterator itr = d_range[f].find( v ); if( itr != d_range[f].end() ){ Node r = itr->second; - Assert( !r.isNull() ); + Assert(!r.isNull()); bool isProxy = false; if (expr::hasBoundVar(r)) { @@ -695,16 +696,16 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) { Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl; - Assert( d_set_nums[q].find( v )!=d_set_nums[q].end() ); + Assert(d_set_nums[q].find(v) != d_set_nums[q].end()); int vindex = d_set_nums[q][v]; - Assert( d_set_nums[q][v]==vindex ); + Assert(d_set_nums[q][v] == vindex); Trace("bound-int-rsi-debug") << " index order is " << vindex << std::endl; //must take substitution for all variables that are iterating at higher level for( int i=0; i<vindex; i++) { - Assert( d_set_nums[q][d_set[q][i]]==i ); + Assert(d_set_nums[q][d_set[q][i]] == i); Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl; int v = rsi->getVariableOrder( i ); - Assert( q[0][v]==d_set[q][i] ); + Assert(q[0][v] == d_set[q][i]); Node t = rsi->getCurrentTerm(v, true); Trace("bound-int-rsi") << "term : " << t << std::endl; vars.push_back( d_set[q][i] ); @@ -772,7 +773,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node tl = l; Node tu = u; getBounds( q, v, rsi, tl, tu ); - Assert( !tl.isNull() && !tu.isNull() ); + Assert(!tl.isNull() && !tu.isNull()); if( ra==d_quantEngine->getTermUtil()->d_true ){ long rr = range.getConst<Rational>().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; @@ -797,11 +798,11 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node if( srv.getKind()!=EMPTYSET ){ //collect the elements while( srv.getKind()==UNION ){ - Assert( srv[1].getKind()==kind::SINGLETON ); + Assert(srv[1].getKind() == kind::SINGLETON); elements.push_back( srv[1][0] ); srv = srv[0]; } - Assert( srv.getKind()==kind::SINGLETON ); + Assert(srv.getKind() == kind::SINGLETON); elements.push_back( srv[0] ); //check if we need to do matching, for literals like ( tuple( v ) in S ) Node t = d_setm_range_lit[q][v][0]; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 2306a0565..f6edd3195 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -443,7 +443,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ } if( !isStar && !ri.isConst() ){ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; - Assert( false ); + Assert(false); } entry_children.push_back(ri); } @@ -453,7 +453,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ << "Representative of " << v << " is " << nv << std::endl; if( !nv.isConst() ){ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl; - Assert( false ); + Assert(false); } Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ @@ -501,13 +501,14 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ inst.push_back( r ); } Node ev = fm->d_models[op]->evaluate( fm, inst ); - Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl; - AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) ); + Trace("fmc-model-debug") << ".....Checking eval( " << + fm->d_uf_terms[op][i] << " ) = " << ev << std::endl; AlwaysAssert( + fm->areEqual( ev, fm->d_uf_terms[op][i] ) ); } */ } - Assert( d_addedLemmas==0 ); - + Assert(d_addedLemmas == 0); + //make function values for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){ Node f_def = getFunctionValue( fm, it->first, "$x" ); @@ -582,7 +583,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; - Assert( !d_qe->inConflict() ); + Assert(!d_qe->inConflict()); if( optUseModel() ){ FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc(); if (effort==0) { @@ -606,7 +607,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i //model check the quantifier doCheck(fmfmc, f, d_quant_models[f], f[1]); Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; - Assert( !d_quant_models[f].d_cond.empty() ); + Assert(!d_quant_models[f].d_cond.empty()); d_quant_models[f].debugPrint("fmc", Node::null(), this); Trace("fmc") << std::endl; @@ -1159,7 +1160,7 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, De int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) { Trace("fmc-debug3") << "isCompat " << c << std::endl; - Assert(cond.size()==c.getNumChildren()+1); + Assert(cond.size() == c.getNumChildren() + 1); for (unsigned i=1; i<cond.size(); i++) { if (cond[i] != c[i - 1] && !fm->isStar(cond[i]) && !fm->isStar(c[i - 1])) { @@ -1171,7 +1172,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) { Trace("fmc-debug3") << "doMeet " << c << std::endl; - Assert(cond.size()==c.getNumChildren()+1); + Assert(cond.size() == c.getNumChildren() + 1); for (unsigned i=1; i<cond.size(); i++) { if( cond[i]!=c[i-1] ) { if (fm->isStar(cond[i])) @@ -1203,7 +1204,7 @@ void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::v cond.push_back(d_quant_cond[f]); for (unsigned i=0; i<f[0].getNumChildren(); i++) { Node ts = fm->getStar(f[0][i].getType()); - Assert( ts.getType()==f[0][i].getType() ); + Assert(ts.getType() == f[0][i].getType()); cond.push_back(ts); } } diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 3ab52a63b..cdaaa239a 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -77,7 +77,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) doCheck = quant_e == QEFFORT_MODEL; } if( doCheck ){ - Assert( !d_quantEngine->inConflict() ); + Assert(!d_quantEngine->inConflict()); int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); @@ -240,7 +240,7 @@ int ModelEngine::checkModel(){ if( d_addedLemmas>0 ){ break; }else{ - Assert( !d_quantEngine->inConflict() ); + Assert(!d_quantEngine->inConflict()); } } diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 185a349c0..aa3efca19 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -36,7 +36,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { for( unsigned i=0; i<assertions.size(); i++ ){ Node n = QuantAttributes::getFunDefHead( assertions[i] ); if( !n.isNull() ){ - Assert( n.getKind()==APPLY_UF ); + Assert(n.getKind() == APPLY_UF); Node f = n.getOperator(); //check if already defined, if so, throw error @@ -127,7 +127,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def, std::map< int, std::map< Node, Node > >& visited, std::map< int, std::map< Node, Node > >& visited_cons ) { - Assert( constraints.empty() ); + Assert(constraints.empty()); int index = ( is_fun_def ? 1 : 0 ) + 2*( hasPol ? ( pol ? 1 : -1 ) : 0 ); std::map< Node, Node >::iterator itv = visited[index].find( n ); if( itv!=visited[index].end() ){ @@ -240,7 +240,7 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod cons = constraints[0]; } visited_cons[index][n] = cons; - Assert( constraints.size()==1 && constraints[0]==cons ); + Assert(constraints.size() == 1 && constraints[0] == cons); } visited[index][n] = ret; return ret; diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 069d5b888..bd947d70b 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -107,7 +107,7 @@ void InstMatch::setValue( int i, TNode n ) { } bool InstMatch::set(EqualityQuery* q, int i, TNode n) { - Assert( i>=0 ); + Assert(i >= 0); if( !d_vals[i].isNull() ){ if (q->areEqual(d_vals[i], n)) { diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index a3c114d90..6566319fa 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -121,8 +121,8 @@ Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& e if( !ar.isNull() ){ if( engine_has_a || getEngine()->hasTerm( ar ) ){ Trace("qip-eq") << "getRepresentativeExp " << a << " returns " << ar << std::endl; - Assert( getEngine()->hasTerm( ar ) ); - Assert( getEngine()->getRepresentative( ar )==ar ); + Assert(getEngine()->hasTerm(ar)); + Assert(getEngine()->getRepresentative(ar) == ar); return ar; } }else{ @@ -187,15 +187,15 @@ TNode EqualityQueryInstProp::getCongruentTermExp( Node f, std::vector< TNode >& } Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) { - Assert( exp.empty() ); + Assert(exp.empty()); std::map< Node, Node >::iterator it = d_uf.find( a ); if( it!=d_uf.end() ){ if( it->second==a ){ - Assert( d_uf_exp[ a ].empty() ); + Assert(d_uf_exp[a].empty()); return it->second; }else{ Node m = getUfRepresentative( it->second, exp ); - Assert( !m.isNull() ); + Assert(!m.isNull()); if( m!=it->second ){ //update union find d_uf[ a ] = m; @@ -224,7 +224,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No std::vector< Node > exp_a; Node ar = getUfRepresentative( a, exp_a ); if( ar.isNull() ){ - Assert( exp_a.empty() ); + Assert(exp_a.empty()); ar = a; } if( ar==b ){ @@ -241,7 +241,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No std::vector< Node > exp_b; Node br = getUfRepresentative( b, exp_b ); if( br.isNull() ){ - Assert( exp_b.empty() ); + Assert(exp_b.empty()); br = b; if( !getEngine()->hasTerm( br ) ){ if( ar!=a || getEngine()->hasTerm( ar ) ){ @@ -278,8 +278,8 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No br = temp_r; } - Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) ); - Assert( ar!=br ); + Assert(!getEngine()->hasTerm(ar) || getEngine()->hasTerm(br)); + Assert(ar != br); std::vector< Node > exp_d; if( areDisequalExp( ar, br, exp_d ) ){ @@ -294,8 +294,8 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No }else{ if( pol ){ //update the union find - Assert( d_uf_exp[ar].empty() ); - Assert( d_uf_exp[br].empty() ); + Assert(d_uf_exp[ar].empty()); + Assert(d_uf_exp[br].empty()); //registerUfTerm( ar ); d_uf[ar] = br; @@ -326,8 +326,8 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No return status; }else{ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : disequal " << ar << " <> " << br << std::endl; - Assert( d_diseq_list[ar].find( br )==d_diseq_list[ar].end() ); - Assert( d_diseq_list[br].find( ar )==d_diseq_list[br].end() ); + Assert(d_diseq_list[ar].find(br) == d_diseq_list[ar].end()); + Assert(d_diseq_list[br].find(ar) == d_diseq_list[br].end()); merge_exp( d_diseq_list[ar][br], reason ); merge_exp( d_diseq_list[br][ar], reason ); @@ -372,7 +372,7 @@ bool EqualityQueryInstProp::isPropagateLiteral( Node n ) { Node atom = n.getKind()==NOT ? n[0] : n; return !atom[0].getType().isBoolean(); }else{ - Assert( ak!=NOT ); + Assert(ak != NOT); return ak!=AND && ak!=OR && ak!=ITE; } } @@ -410,7 +410,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s Node ret; //check if it should be propagated in this context if( hasPol && isPropagateLiteral( n ) ){ - Assert( n.getType().isBoolean() ); + Assert(n.getType().isBoolean()); //must be Boolean ret = evaluateTermExp( n, exp, visited, false, pol, watch_list_out, props ); if( isPropagateLiteral( ret ) ){ @@ -432,7 +432,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s bool childChanged = false; int abort_i = -1; //get the child entailed polarity - Assert( n.getKind()!=IMPLIES ); + Assert(n.getKind() != IMPLIES); bool newHasPol, newPol; QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol ); std::vector< Node > watch; @@ -511,19 +511,19 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s Trace("qip-eval") << "arg " << i << " : " << args[i] << std::endl; t_args.push_back( args[i] ); } - Assert( args.size()==n.getNumChildren() ); + Assert(args.size() == n.getNumChildren()); //args contains terms known by the equality engine TNode nn = getCongruentTerm( f, t_args ); Trace("qip-eval") << " got congruent term " << nn << " for " << n << std::endl; if( !nn.isNull() ){ //successfully constructed representative in EE - Assert( exp_n.empty() ); + Assert(exp_n.empty()); ret = getRepresentativeExp( nn, exp_n ); Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl; merge_exp( exp, exp_n ); ret_set = true; - Assert( !ret.isNull() ); - Assert( ret!=n ); + Assert(!ret.isNull()); + Assert(ret != n); // we have that n == ret, check if the union find should be updated TODO? }else{ watch.push_back( ret ); @@ -542,7 +542,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s ret_set = true; } }else{ - Assert( args.size()==n.getNumChildren() ); + Assert(args.size() == n.getNumChildren()); } if( !ret_set ){ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ @@ -576,7 +576,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) { //TODO : optimize if( v.empty() ){ - Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() ); + Assert(up_to_size == -1 || up_to_size == (int)v_to_merge.size()); v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() ); }else{ //std::vector< Node >::iterator v_end = v.end(); @@ -595,7 +595,7 @@ void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& term //information about the instance d_q = q; d_lem = lem; - Assert( d_terms.empty() ); + Assert(d_terms.empty()); d_terms.insert( d_terms.end(), terms.begin(), terms.end() ); //the current lemma d_curr = body; @@ -641,7 +641,7 @@ bool InstPropagator::notifyInstantiation(QuantifiersModule::QEffort quant_e, unsigned id = allocateInstantiation( q, lem, terms, body ); //initialize the information if( cacheConclusion( id, body ) ){ - Assert( d_update_list.empty() ); + Assert(d_update_list.empty()); d_update_list.push_back( id ); bool firstTime = true; //update infos in the update list until empty @@ -660,7 +660,7 @@ bool InstPropagator::notifyInstantiation(QuantifiersModule::QEffort quant_e, Trace("qip-prop") << "...finished notify instantiation." << std::endl; return !d_conflict; }else{ - Assert( false ); + Assert(false); return false; } } @@ -676,7 +676,7 @@ void InstPropagator::filterInstantiations() { it->second.d_q, it->second.d_lem, it->second.d_terms)) { Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; - Assert( false ); + Assert(false); }else{ Trace("qip-prop-debug") << it->first << " "; } @@ -700,8 +700,8 @@ unsigned InstPropagator::allocateInstantiation( Node q, Node lem, std::vector< N } bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) { - Assert( !d_conflict ); - Assert( ii.d_active ); + Assert(!d_conflict); + Assert(ii.d_active); Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl; //update the evaluation of the current lemma std::map< Node, std::vector< Node > > watch_list_out; @@ -733,14 +733,14 @@ bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) { } //determine the status of eval if( eval==d_qy.d_false ){ - Assert( props.empty() ); + Assert(props.empty()); //we have inferred a conflict conflict( ii.d_curr_exp ); return false; }else{ for( unsigned i=0; i<props.size(); i++ ){ Trace("qip-prop-debug2") << "Process propagation " << props[i] << std::endl; - Assert( d_qy.isPropagateLiteral( props[i] ) ); + Assert(d_qy.isPropagateLiteral(props[i])); //if we haven't propagated this literal yet if( cacheConclusion( id, props[i], 1 ) ){ //watch list for propagated literal: may not yet be purely EE representatives @@ -778,7 +778,7 @@ bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) { }else{ Trace("qip-prop-debug") << "...did not update." << std::endl; } - Assert( !d_conflict ); + Assert(!d_conflict); return true; } @@ -802,8 +802,8 @@ void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& e if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){ Trace("qip-rlv-propagate") << "Relevant propagation : " << a << " == " << b << std::endl; - Assert( d_qy.getEngine()->hasTerm( a ) ); - Assert( d_qy.getEngine()->hasTerm( b ) ); + Assert(d_qy.getEngine()->hasTerm(a)); + Assert(d_qy.getEngine()->hasTerm(b)); Trace("qip-prop-debug") << "...equality between known terms." << std::endl; addRelevantInstances( exp, "qip-propagate" ); //d_has_relevant_inst = true; @@ -837,7 +837,7 @@ void InstPropagator::conflict( std::vector< Node >& exp ) { } bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) { - Assert( prop_index==0 || prop_index==1 ); + Assert(prop_index == 0 || prop_index == 1); //check if the conclusion is non-redundant if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){ d_conc_to_id[prop_index][body] = id; @@ -849,7 +849,7 @@ bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) { void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) { for( unsigned i=0; i<exp.size(); i++ ){ - Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() ); + Assert(d_conc_to_id[0].find(exp[i]) != d_conc_to_id[0].end()); Trace(c) << " relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl; d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true; } @@ -857,7 +857,7 @@ void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) { for( unsigned i=0; i<exp.size(); i++ ){ - Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() ); + Assert(d_conc_to_id[0].find(exp[i]) != d_conc_to_id[0].end()); Trace(c) << d_conc_to_id[0][ exp[i] ] << " "; } } diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index 520088328..a3de5ced9 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -164,11 +164,11 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { reset(); for( unsigned i=0; i<d_lte_asserts.size(); i++ ){ Node q = d_lte_asserts[i]; - Assert( d_do_inst.find( q )!=d_do_inst.end() && d_do_inst[q] ); + Assert(d_do_inst.find(q) != d_do_inst.end() && d_do_inst[q]); if( d_inst.find( q )==d_inst.end() ){ Trace("lte-partial-inst") << "LTE : Get partial instantiations for " << q << "..." << std::endl; d_inst[q] = true; - Assert( !d_vars[q].empty() ); + Assert(!d_vars[q].empty()); //make bound list Node bvl; std::vector< Node > bvs; @@ -189,7 +189,7 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { } getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, NULL, 0, 0, 0 ); - Assert( !conj.empty() ); + Assert(!conj.empty()); lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); d_wasInvoked = true; } @@ -226,16 +226,16 @@ void LtePartialInst::getPartialInstantiations(std::vector<Node>& conj, conj.push_back( nq ); } }else{ - Assert( pindex<q[2][0].getNumChildren() ); + Assert(pindex < q[2][0].getNumChildren()); Node pat = q[2][0][pindex]; - Assert( pat.getNumChildren()==0 || paindex<=pat.getNumChildren() ); + Assert(pat.getNumChildren() == 0 || paindex <= pat.getNumChildren()); if( pat.getKind()==APPLY_UF ){ - Assert( paindex<=pat.getNumChildren() ); + Assert(paindex <= pat.getNumChildren()); if( paindex==pat.getNumChildren() ){ getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex ); }else{ if( !curr ){ - Assert( paindex==0 ); + Assert(paindex == 0); //start traversing term index for the operator curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() ); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 4b055f71c..de46eee74 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -148,7 +148,7 @@ void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& v bool rec = true; bool newPol = pol; if( d_var_num.find( n )!=d_var_num.end() ){ - Assert( std::find( vars.begin(), vars.end(), n )==vars.end() ); + Assert(std::find(vars.begin(), vars.end(), n) == vars.end()); vars.push_back( n ); TNode f = p->getTermDatabase()->getMatchOperator( n ); if( !f.isNull() ){ @@ -157,7 +157,7 @@ void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& v } } }else if( MatchGen::isHandledBoolConnective( n ) ){ - Assert( n.getKind()!=IMPLIES ); + Assert(n.getKind() != IMPLIES); QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol ); } Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl; @@ -298,7 +298,7 @@ TNode QuantInfo::getCurrentValue( TNode n ) { if( d_match[v].isNull() ){ return n; }else{ - Assert( getVarNum( d_match[v] )!=v ); + Assert(getVarNum(d_match[v]) != v); return getCurrentValue( d_match[v] ); } } @@ -312,7 +312,7 @@ TNode QuantInfo::getCurrentExpValue( TNode n ) { if( d_match[v].isNull() ){ return n; }else{ - Assert( getVarNum( d_match[v] )!=v ); + Assert(getVarNum(d_match[v]) != v); if( d_match_term[v].isNull() ){ return getCurrentValue( d_match[v] ); }else{ @@ -356,9 +356,9 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo //for handling equalities between variables, and disequalities involving variables Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")"; Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl; - Assert( doRemove || n==getCurrentValue( n ) ); - Assert( doRemove || v==getCurrentRepVar( v ) ); - Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) ); + Assert(doRemove || n == getCurrentValue(n)); + Assert(doRemove || v == getCurrentRepVar(v)); + Assert(doRemove || vn == getCurrentRepVar(getVarNum(n))); if( polarity ){ if( vn!=v ){ if( doRemove ){ @@ -398,7 +398,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo bool alreadySet = false; if( !d_match[vn].isNull() ){ alreadySet = true; - Assert( !isVar( d_match[vn] ) ); + Assert(!isVar(d_match[vn])); } //copy or check disequalities @@ -461,7 +461,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo return -1; }else{ if( doRemove ){ - Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() ); + Assert(d_curr_var_deq[v].find(n) != d_curr_var_deq[v].end()); d_curr_var_deq[v].erase( n ); return 1; }else{ @@ -831,7 +831,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl; } }else{ - Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 ); + Assert(doFail || d_una_index == (int)d_una_eqc_count.size() - 1); if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){ int currIndex = d_una_eqc_count[d_una_index]; d_una_eqc_count[d_una_index]++; @@ -975,7 +975,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) std::vector< Node > qni_apps; d_qni_size = 0; if( isVar ){ - Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() ); + Assert(qi->d_var_num.find(n) != qi->d_var_num.end()); if( n.getKind()==ITE ){ d_type = typ_invalid; }else{ @@ -1026,10 +1026,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) d_type = typ_invalid; //literals if( isHandledUfTerm( d_n ) ){ - Assert( qi->isVar( d_n ) ); + Assert(qi->isVar(d_n)); d_type = typ_pred; }else if( d_n.getKind()==BOUND_VARIABLE ){ - Assert( d_n.getType().isBoolean() ); + Assert(d_n.getType().isBoolean()); d_type = typ_bool_var; }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){ for (unsigned i = 0; i < d_n.getNumChildren(); i++) @@ -1140,7 +1140,7 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars Trace("qcf-qregister-vo") << vu_count[min_score_index] << " " << vb_count[min_score_index] << " " << has_nested[min_score_index] << std::endl; Trace("qcf-qregister-debug") << "...assign child " << min_score_index << std::endl; Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl; - Assert( min_score_index!=-1 ); + Assert(min_score_index != -1); //add to children order d_children_order.push_back( min_score_index ); assigned[min_score_index] = true; @@ -1291,7 +1291,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { d_qn.push_back( NULL ); } }else if( d_type==typ_var ){ - Assert( isHandledUfTerm( d_n ) ); + Assert(isHandledUfTerm(d_n)); TNode f = getMatchOperator( p, d_n ); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f); @@ -1520,7 +1520,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { //clean up the matches you set for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){ Debug("qcf-match") << " Clean up bound var " << it->second << std::endl; - Assert( it->second<qi->getNumVars() ); + Assert(it->second < qi->getNumVars()); qi->unsetMatch( p, it->second ); qi->d_match_term[ it->second ] = TNode::null(); } @@ -1650,8 +1650,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { d_qn.clear(); return true; }else{ - Assert( d_type==typ_var ); - Assert( d_qni_size>0 ); + Assert(d_type == typ_var); + Assert(d_qni_size > 0); bool invalidMatch; do { invalidMatch = false; @@ -1694,10 +1694,10 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { } }else{ Debug("qcf-match-debug") << " Match " << index << " is ground term" << std::endl; - Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() ); - Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() ); + Assert(d_qni_gterm.find(index) != d_qni_gterm.end()); + Assert(d_qni_gterm_rep.find(index) != d_qni_gterm_rep.end()); val = d_qni_gterm_rep[index]; - Assert( !val.isNull() ); + Assert(!val.isNull()); } if( !val.isNull() ){ //constrained by val @@ -1715,7 +1715,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { } } }else{ - Assert( d_qn.size()==d_qni.size() ); + Assert(d_qn.size() == d_qni.size()); int index = d_qni.size()-1; //increment if binding this variable bool success = false; @@ -1751,7 +1751,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { if( d_qni.size()==d_qni_size ){ //Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() ); //Debug("qcf-match-debug") << " We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl; - Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() ); + Assert(!d_qni[d_qni.size() - 1]->second.d_data.empty()); TNode t = d_qni[d_qni.size()-1]->second.d_data.begin()->first; Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl; qi->d_match_term[d_qni_var_num[0]] = t; @@ -1760,8 +1760,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl; //if( it->second<(int)qi->d_q[0].getNumChildren() ){ //if it is an actual variable, we are interested in knowing the actual term if( it->first>0 ){ - Assert( !qi->d_match[ it->second ].isNull() ); - Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) ); + Assert(!qi->d_match[it->second].isNull()); + Assert(p->areEqual(t[it->first - 1], qi->d_match[it->second])); qi->d_match_term[it->second] = t[it->first-1]; } //} diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index f5ebb33b1..0e6eb1581 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -64,24 +64,24 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve QuantNameAttribute qna; n.setAttribute(qna, true); } else if (attr == "sygus-synth-grammar") { - Assert( node_values.size()==1 ); + Assert(node_values.size() == 1); Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to " << node_values[0] << std::endl; SygusSynthGrammarAttribute ssg; n.setAttribute(ssg, node_values[0]); }else if( attr=="sygus-synth-fun-var-list" ){ - Assert( node_values.size()==1 ); + Assert(node_values.size() == 1); Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to " << node_values[0] << std::endl; SygusSynthFunVarListAttribute ssfvla; n.setAttribute( ssfvla, node_values[0] ); }else if( attr=="quant-inst-max-level" ){ - Assert( node_values.size()==1 ); + Assert(node_values.size() == 1); uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong(); Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl; QuantInstLevelAttribute qila; n.setAttribute( qila, lvl ); }else if( attr=="rr-priority" ){ - Assert( node_values.size()==1 ); + Assert(node_values.size() == 1); uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong(); Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; RrPriorityAttribute rrpa; @@ -296,7 +296,7 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ } if( avar.getKind()==REWRITE_RULE ){ Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; - Assert( i==0 ); + Assert(i == 0); qa.d_rr = avar; } } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 33da46675..0039ec845 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -92,7 +92,7 @@ void QuantifiersRewriter::computeArgVec(const std::vector<Node>& args, std::vector<Node>& activeArgs, Node n) { - Assert( activeArgs.empty() ); + Assert(activeArgs.empty()); std::map< Node, bool > activeMap; std::map< Node, bool > visited; computeArgs( args, activeMap, n, visited ); @@ -110,7 +110,7 @@ void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args, Node n, Node ipl) { - Assert( activeArgs.empty() ); + Assert(activeArgs.empty()); std::map< Node, bool > activeMap; std::map< Node, bool > visited; computeArgs( args, activeMap, n, visited ); @@ -286,7 +286,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { } if( !success ){ // tautology - Assert( k==OR || k==AND ); + Assert(k == OR || k == AND); return NodeManager::currentNM()->mkConst( k==OR ); } childrenChanged = childrenChanged || c!=body[i]; @@ -405,7 +405,7 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ }else if( j==start ){ res1 = res; }else{ - Assert( res!=0 ); + Assert(res != 0); if( n.getKind()==ITE ){ return res1==res ? res : 0; }else if( n.getKind()==EQUAL ){ @@ -456,7 +456,7 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v if( n.getKind()==APPLY_TESTER ){ const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); unsigned index = Datatype::indexOf(n.getOperator().toExpr()); - Assert( dt.getNumConstructors()>1 ); + Assert(dt.getNumConstructors() > 1); if( pol ){ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ if( i!=index ){ @@ -491,7 +491,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n std::map< Node, Node > icache; if( qa.isFunDef() ){ Node h = QuantAttributes::getFunDefHead( q ); - Assert( !h.isNull() ); + Assert(!h.isNull()); // if it is a function definition, rewrite the body independently Node fbody = QuantAttributes::getFunDefBody( q ); Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; @@ -572,8 +572,8 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol nCurrCond = nCurrCond + 1; } setEntailedCond( children[0], i==1, currCond, new_cond, conflict ); - //should not conflict (entailment check failed) - Assert( !conflict ); + // should not conflict (entailment check failed) + Assert(!conflict); } if( body.getKind()==OR || body.getKind()==AND ){ bool use_pol = body.getKind()==AND; @@ -763,7 +763,7 @@ Node QuantifiersRewriter::computeCondSplit(Node body, std::map< Node, std::map< int, Node > > ncons; std::vector< Node > conj; computeDtTesterIteSplit( body, pcons, ncons, conj ); - Assert( !conj.empty() ); + Assert(!conj.empty()); if( conj.size()>1 ){ Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl; for( unsigned i=0; i<conj.size(); i++ ){ @@ -1507,7 +1507,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) ); return computePrenex( nn, args, nargs, pol, prenexAgg ); }else if( body.getType().isBoolean() ){ - Assert( body.getKind()!=EXISTS ); + Assert(body.getKind() != EXISTS); bool childrenChanged = false; std::vector< Node > newChildren; for( unsigned i=0; i<body.getNumChildren(); i++ ){ @@ -1629,8 +1629,8 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< uns } ret = nnn; }else{ - Assert( args.empty() ); - Assert( nargs.empty() ); + Assert(args.empty()); + Assert(nargs.empty()); } } visited[tindex][n] = ret; @@ -1640,7 +1640,7 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< uns } Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { - Assert( body.getKind()==OR ); + Assert(body.getKind() == OR); size_t var_found_count = 0; size_t eqc_count = 0; size_t eqc_active = 0; @@ -1732,7 +1732,7 @@ Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QA Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); lits.push_back(fa); } - Assert( !lits.empty() ); + Assert(!lits.empty()); Node nf = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode(OR,lits); Trace("clause-split-debug") << "Made node : " << nf << std::endl; return nf; @@ -1828,7 +1828,7 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } } }else if( body.getKind()==NOT ){ - Assert( isLiteral( body[0] ) ); + Assert(isLiteral(body[0])); } //remove variables that don't occur std::vector< Node > activeArgs; @@ -1902,8 +1902,8 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg qvl2.push_back( args[i] ); } } - Assert( !qvl1.empty() ); - Assert( !qvl2.empty() || !qvsh.empty() ); + Assert(!qvl1.empty()); + Assert(!qvl2.empty() || !qvsh.empty()); //check for literals that only contain shared variables std::vector<Node> qlitsh; std::vector<Node> qlit2; @@ -2023,7 +2023,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut }else{ std::vector< Node > nargs; n = computePrenex( n, args, nargs, true, false ); - Assert( nargs.empty() ); + Assert(nargs.empty()); } }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ n = computeVarElimination( n, args, qa ); @@ -2091,9 +2091,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { break; } break; - default: - Unreachable("RewriteRules can be of only three kinds"); - break; + default: Unreachable() << "RewriteRules can be of only three kinds"; break; } // Add the other guards TNode g = r[1]; diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 742b3000b..99e7b5a8c 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -177,7 +177,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) ss << " " << d_vars[i] << " -> " << pt[i] << std::endl; } ss << "but CVC4 answered unsat!" << std::endl; - AlwaysAssert(false, ss.str().c_str()); + AlwaysAssert(false) << ss.str(); } if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_UNSOLVED) { diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 071bd7933..fbd1f05a6 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -27,8 +27,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; void RelevantDomain::RDomain::merge( RDomain * r ) { - Assert( !d_parent ); - Assert( !r->d_parent ); + Assert(!d_parent); + Assert(!r->d_parent); d_parent = r; for( unsigned i=0; i<d_terms.size(); i++ ){ r->addTerm( d_terms[i] ); @@ -79,7 +79,7 @@ RelevantDomain::~RelevantDomain() { for( std::map< Node, std::map< int, RDomain * > >::iterator itr = d_rel_doms.begin(); itr != d_rel_doms.end(); ++itr ){ for( std::map< int, RDomain * >::iterator itr2 = itr->second.begin(); itr2 != itr->second.end(); ++itr2 ){ RDomain * current = (*itr2).second; - Assert( current != NULL ); + Assert(current != NULL); delete current; } } @@ -183,7 +183,8 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po //compute the information for what this literal does computeRelevantDomainLit( q, hasPol, pol, n ); if( d_rel_dom_lit[hasPol][pol][n].d_merge ){ - Assert( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL && d_rel_dom_lit[hasPol][pol][n].d_rd[1]!=NULL ); + Assert(d_rel_dom_lit[hasPol][pol][n].d_rd[0] != NULL + && d_rel_dom_lit[hasPol][pol][n].d_rd[1] != NULL); RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent(); RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent(); if( rd1!=rd2 ){ diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 07ff9ee46..9903456c9 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -68,7 +68,7 @@ void RewriteEngine::check(Theory::Effort e, QEffort quant_e) { if (quant_e == QEFFORT_STANDARD) { - Assert( !d_quantEngine->inConflict() ); + Assert(!d_quantEngine->inConflict()); Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; //if( e==Theory::EFFORT_LAST_CALL ){ // if( !d_quantEngine->getModel()->isModelSet() ){ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 47a1f6142..c34b7d4e3 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -53,7 +53,7 @@ CegSingleInv::~CegSingleInv() void CegSingleInv::initialize(Node q) { // can only register one quantified formula with this - Assert( d_quant.isNull() ); + Assert(d_quant.isNull()); d_quant = q; d_simp_quant = q; Trace("cegqi-si") << "CegSingleInv::initialize : " << q << std::endl; @@ -466,7 +466,7 @@ Node CegSingleInv::getSolution(unsigned sol_index, int& reconstructed, bool rconsSygus) { - Assert( d_sol!=NULL ); + Assert(d_sol != NULL); const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); Node varList = Node::fromExpr( dt.getSygusVarList() ); Node prog = d_quant[0][sol_index]; @@ -486,7 +486,7 @@ Node CegSingleInv::getSolution(unsigned sol_index, Trace("csi-sol") << "Get solution for " << prog << ", with skolems : "; sol_index = d_prog_to_sol_index[prog]; d_sol->d_varList.clear(); - Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() ); + Assert(d_single_inv_arg_sk.size() == varList.getNumChildren()); for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){ Trace("csi-sol") << d_single_inv_arg_sk[i] << " "; vars.push_back( d_single_inv_arg_sk[i] ); @@ -501,7 +501,7 @@ Node CegSingleInv::getSolution(unsigned sol_index, { indices.push_back(i); } - Assert( !indices.empty() ); + Assert(!indices.empty()); //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions) // TODO : to minimize solution size, put the largest term last sortSiInstanceIndices ssii; @@ -520,7 +520,7 @@ Node CegSingleInv::getSolution(unsigned sol_index, cond = TermUtil::simpleNegate(cond); s = nm->mkNode(ITE, cond, d_inst[uindex][sol_index], s); } - Assert( vars.size()==d_sol->d_varList.size() ); + Assert(vars.size() == d_sol->d_varList.size()); s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() ); } d_orig_solution = s; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index d349e8ad4..811210628 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -119,7 +119,7 @@ Node CegSingleInvSol::reconstructSolution(Node sol, if( status==0 ){ Node ret = getReconstructedSolution( d_root_id ); Trace("csi-rcons") << "Sygus solution is : " << ret << std::endl; - Assert( !ret.isNull() ); + Assert(!ret.isNull()); reconstructed = 1; return ret; } @@ -224,11 +224,11 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) int id = allocate( t, stn ); d_rcons_to_status[stn][t] = -1; TypeNode tn = t.getType(); - Assert( stn.isDatatype() ); + Assert(stn.isDatatype()); const Datatype& dt = stn.getDatatype(); TermDbSygus* tds = d_qe->getTermDatabaseSygus(); SygusTypeInfo& sti = tds->getTypeInfo(stn); - Assert( dt.isSygus() ); + Assert(dt.isSygus()); Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl; int carg = -1; int karg = -1; @@ -291,7 +291,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) //try identity functions for (unsigned ii : d_id_funcs[stn]) { - Assert( dt[ii].getNumArgs()==1 ); + Assert(dt[ii].getNumArgs() == 1); //try to directly reconstruct from single argument std::vector< Node > tchildren; tchildren.push_back( min_t ); @@ -402,7 +402,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) //if one succeeds if( status==0 ){ Node rsol = getReconstructedSolution( equiv_ids[i] ); - Assert( !rsol.isNull() ); + Assert(!rsol.isNull()); //set all members of the equivalence class that this is the reconstructed solution setReconstructed( id, rsol ); break; @@ -433,7 +433,7 @@ bool CegSingleInvSol::collectReconstructNodes(int pid, std::vector<int>& ids, int& status) { - Assert( dtc.getNumArgs()==ts.size() ); + Assert(dtc.getNumArgs() == ts.size()); for( unsigned i=0; i<ts.size(); i++ ){ TypeNode cstn = d_qe->getTermDatabaseSygus()->getArgType( dtc, i ); int cstatus; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 0dc49fa96..8f935de27 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -177,7 +177,7 @@ Node CegGrammarConstructor::process(Node q, std::map<Node, Node>::const_iterator itta = templates_arg.find(sf); Assert(itta != templates_arg.end()); TNode templ_arg = itta->second; - Assert( !templ_arg.isNull() ); + Assert(!templ_arg.isNull()); // if there is a template for this argument, make a sygus type on top of it if( options::sygusTemplEmbedGrammar() ){ Trace("cegqi-debug") << "Template for " << sf << " is : " << templ @@ -737,7 +737,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( weights[i].push_back(-1); // length TypeNode intType = nm->integerType(); - Assert(std::find(types.begin(),types.end(),intType)!=types.end()); + Assert(std::find(types.begin(), types.end(), intType) != types.end()); unsigned i_intType = std::distance( types.begin(), std::find(types.begin(), @@ -1086,12 +1086,12 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( datatypes, unres); Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; - Assert( !datatypes.empty() ); + Assert(!datatypes.empty()); std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes( datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); Trace("sygus-grammar-def") << "...finished" << std::endl; - Assert( types.size()==datatypes.size() ); + Assert(types.size() == datatypes.size()); return TypeNode::fromType( types[0] ); } @@ -1114,7 +1114,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a // TODO : can short circuit to this case when !TermUtil::containsTerm( templ, templ_arg ) op = templ; }else{ - Assert( templ.hasOperator() ); + Assert(templ.hasOperator()); op = templ.getOperator(); // make constructor taking arguments types from children for( unsigned i=0; i<templ.getNumChildren(); i++ ){ @@ -1132,7 +1132,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes( datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); - Assert( types.size()==1 ); + Assert(types.size() == 1); return TypeNode::fromType( types[0] ); } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 64bf0972c..474fdb5d8 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -440,7 +440,7 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, std::vector<Node>& candidate_values, std::vector<Node>& lems) { - Assert( enums.size()==enum_values.size() ); + Assert(enums.size() == enum_values.size()); if( !enums.empty() ){ unsigned min_term_size = 0; Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index ff58dbe38..72091c0cf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1453,12 +1453,11 @@ Node SygusUnifIo::constructSol( if (!rec_c.isNull()) { Assert(ecache_child.d_enum_val_to_index.find(rec_c) - != ecache_child.d_enum_val_to_index.end()); + != ecache_child.d_enum_val_to_index.end()); split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c]; set_split_cond_res_index = true; split_cond_enum = ce; - Assert(split_cond_res_index - < ecache_child.d_enum_vals_res.size()); + Assert(split_cond_res_index < ecache_child.d_enum_vals_res.size()); } } else diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index ff9fede0b..7fb54f14e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" -#include "base/cvc4_check.h" +#include "base/check.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" @@ -80,7 +80,7 @@ TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) { }else{ ss << "fv_" << tn << "_" << i; } - Assert( !vtn.isNull() ); + Assert(!vtn.isNull()); Node v = NodeManager::currentNM()->mkSkolem( ss.str(), vtn, "for sygus normal form testing" ); d_fv_stype[v] = tn; d_fv_num[v] = i; @@ -155,7 +155,7 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) } TypeNode TermDbSygus::getSygusTypeForVar( Node v ) { - Assert( d_fv_stype.find( v )!=d_fv_stype.end() ); + Assert(d_fv_stype.find(v) != d_fv_stype.end()); return d_fv_stype[v]; } @@ -165,8 +165,8 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, std::map<int, Node>& pre) { Assert(c < dt.getNumConstructors()); - Assert( dt.isSygus() ); - Assert( !dt[c].getSygusOp().isNull() ); + Assert(dt.isSygus()); + Assert(!dt[c].getSygusOp().isNull()); std::vector< Node > children; Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << c << "..." << std::endl; @@ -182,7 +182,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, } Trace("sygus-db-debug") << " child " << i << " : " << a << " : " << a.getType() << std::endl; - Assert( !a.isNull() ); + Assert(!a.isNull()); children.push_back( a ); } return datatypes::utils::mkSygusTerm(dt, c, children); @@ -495,7 +495,7 @@ void TermDbSygus::registerEnumerator(Node e, } else { - Unreachable("Unknown enumerator mode in registerEnumerator"); + Unreachable() << "Unknown enumerator mode in registerEnumerator"; } } Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole @@ -1039,7 +1039,7 @@ Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) { std::vector< Node > vars; std::vector< Node > subs; Node var_list = Node::fromExpr( dt.getSygusVarList() ); - Assert( var_list.getNumChildren()+1==n.getNumChildren() ); + Assert(var_list.getNumChildren() + 1 == n.getNumChildren()); for( unsigned j=0; j<var_list.getNumChildren(); j++ ){ vars.push_back( var_list[j] ); } @@ -1049,7 +1049,7 @@ Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) { Assert(subs[j - 1].getType().isComparableTo( var_list[j - 1].getType())); } - Assert( vars.size()==subs.size() ); + Assert(vars.size() == subs.size()); bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl; Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl; diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 818a53711..8f280c587 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/sygus/type_info.h" -#include "base/cvc4_check.h" +#include "base/check.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -123,7 +123,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) TypeNode ct = TypeNode::fromType(dt[i].getArgType(j)); TypeNode cbt = tds->sygusToBuiltinType(ct); TypeNode lat = TypeNode::fromType(sop[0][j].getType()); - CVC4_CHECK(cbt.isSubtypeOf(lat)) + AlwaysAssert(cbt.isSubtypeOf(lat)) << "In sygus datatype " << dt.getName() << ", argument to a lambda constructor is not " << lat << std::endl; } @@ -152,7 +152,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) // e.g. bitvector-and is a constructor of an integer grammar. Node g = tds->mkGeneric(dt, i); TypeNode gtn = g.getType(); - CVC4_CHECK(gtn.isSubtypeOf(btn)) + AlwaysAssert(gtn.isSubtypeOf(btn)) << "Sygus datatype " << dt.getName() << " encodes terms that are not of type " << btn << std::endl; Trace("sygus-db") << "...done register Operator #" << i << std::endl; diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 10d7ef6ab..834ca1975 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -813,8 +813,8 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr) if (options::sygusRewVerifyAbort()) { - AlwaysAssert(false, - "--sygus-rr-verify detected unsoundness in the rewriter!"); + AlwaysAssert(false) + << "--sygus-rr-verify detected unsoundness in the rewriter!"; } } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 9da9c95b6..79279eb41 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -46,7 +46,8 @@ TermDb::~TermDb(){ } void TermDb::registerQuantifier( Node q ) { - Assert( q[0].getNumChildren()==d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ) ); + Assert(q[0].getNumChildren() + == d_quantEngine->getTermUtil()->getNumInstantiationConstants(q)); for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); setTermInactive( ic ); @@ -257,7 +258,7 @@ void TermDb::computeArgReps( TNode n ) { } void TermDb::computeUfEqcTerms( TNode f ) { - Assert( f==getOperatorRepresentative( f ) ); + Assert(f == getOperatorRepresentative(f)); if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end()) { return; @@ -291,7 +292,7 @@ void TermDb::computeUfTerms( TNode f ) { // already computed return; } - Assert( f==getOperatorRepresentative( f ) ); + Assert(f == getOperatorRepresentative(f)); d_op_nonred_count[f] = 0; // get the matchable operators in the equivalence class of f std::vector<TNode> ops; @@ -501,8 +502,9 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { f = getOperatorRepresentative( f ); } computeUfTerms( f ); - Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) || - d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r ); + Assert(!d_quantEngine->getActiveEqualityEngine()->hasTerm(r) + || d_quantEngine->getActiveEqualityEngine()->getRepresentative(r) + == r); std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); if( it != d_func_map_rel_dom.end() ){ std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i ); @@ -712,7 +714,7 @@ Node TermDb::evaluateTerm2(TNode n, TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) { - Assert( !qy->extendsEngine() ); + Assert(!qy->extendsEngine()); Trace("term-db-entail") << "get entailed term : " << n << std::endl; if( qy->getEngine()->hasTerm( n ) ){ Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; @@ -723,8 +725,8 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su if( it!=subs.end() ){ Trace("term-db-entail") << "...substitution is : " << it->second << std::endl; if( subsRep ){ - Assert( qy->getEngine()->hasTerm( it->second ) ); - Assert( qy->getEngine()->getRepresentative( it->second )==it->second ); + Assert(qy->getEngine()->hasTerm(it->second)); + Assert(qy->getEngine()->getRepresentative(it->second) == it->second); return it->second; }else{ return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy ); @@ -805,9 +807,9 @@ TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) { } bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) { - Assert( !qy->extendsEngine() ); + Assert(!qy->extendsEngine()); Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; - Assert( n.getType().isBoolean() ); + Assert(n.getType().isBoolean()); if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy ); if( !n1.isNull() ){ @@ -816,8 +818,8 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, if( n1==n2 ){ return pol; }else{ - Assert( qy->getEngine()->hasTerm( n1 ) ); - Assert( qy->getEngine()->hasTerm( n2 ) ); + Assert(qy->getEngine()->hasTerm(n1)); + Assert(qy->getEngine()->hasTerm(n2)); if( pol ){ return qy->getEngine()->areEqual( n1, n2 ); }else{ @@ -854,7 +856,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, }else if( n.getKind()==APPLY_UF ){ TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy ); if( !n1.isNull() ){ - Assert( qy->hasTerm( n1 ) ); + Assert(qy->hasTerm(n1)); if( n1==d_true ){ return pol; }else if( n1==d_false ){ @@ -871,7 +873,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) { if( qy==NULL ){ - Assert( d_consistent_ee ); + Assert(d_consistent_ee); qy = d_quantEngine->getEqualityQuery(); } std::map< TNode, TNode > subs; @@ -880,7 +882,7 @@ bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) { bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) { if( qy==NULL ){ - Assert( d_consistent_ee ); + Assert(d_consistent_ee); qy = d_quantEngine->getEqualityQuery(); } return isEntailed2( n, subs, subsRep, true, pol, qy ); @@ -908,7 +910,7 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { }else if( options::termDbMode()==TERM_DB_RELEVANT ){ return d_has_map.find( n )!=d_has_map.end(); }else{ - Assert( false ); + Assert(false); return false; } } diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index c9c738eb3..7f94130f3 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -217,7 +217,7 @@ Node TermUtil::substituteBoundVariables(Node n, std::vector<Node>& terms) { registerQuantifier(q); - Assert( d_vars[q].size()==terms.size() ); + Assert(d_vars[q].size() == terms.size()); return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() ); } @@ -306,7 +306,7 @@ void TermUtil::computeInstConstContainsForQuant(Node q, Node TermUtil::ensureType( Node n, TypeNode tn ) { TypeNode ntn = n.getType(); - Assert( ntn.isComparableTo( tn ) ); + Assert(ntn.isComparableTo(tn)); if( ntn.isSubtypeOf( tn ) ){ return n; }else{ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index f24a4bb2b..1682b4d0c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -16,8 +16,7 @@ #include "theory/quantifiers/theory_quantifiers.h" - -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/kind.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/instantiation_engine.h" @@ -147,15 +146,11 @@ void TheoryQuantifiers::check(Effort e) { //do nothing break; case kind::INST_CLOSURE: - default: - Unhandled(assertion[0].getKind()); - break; + default: Unhandled() << assertion[0].getKind(); break; } } break; - default: - Unhandled(assertion.getKind()); - break; + default: Unhandled() << assertion.getKind(); break; } } // call the quantifiers engine to check diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index ad1c4c69b..62d75cf18 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -29,7 +29,7 @@ struct QuantifierForallTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Debug("typecheck-q") << "type check for fa " << n << std::endl; - Assert(n.getKind() == kind::FORALL && n.getNumChildren()>0 ); + Assert(n.getKind() == kind::FORALL && n.getNumChildren() > 0); if( check ){ if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ throw TypeCheckingExceptionPrivate(n, "first argument of universal quantifier is not bound var list"); @@ -49,7 +49,7 @@ struct QuantifierExistsTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Debug("typecheck-q") << "type check for ex " << n << std::endl; - Assert(n.getKind() == kind::EXISTS && n.getNumChildren()>0 ); + Assert(n.getKind() == kind::EXISTS && n.getNumChildren() > 0); if( check ){ if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ throw TypeCheckingExceptionPrivate(n, "first argument of existential quantifier is not bound var list"); @@ -68,7 +68,7 @@ struct QuantifierExistsTypeRule { struct QuantifierBoundVarListTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::BOUND_VAR_LIST ); + Assert(n.getKind() == kind::BOUND_VAR_LIST); if( check ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ if( n[i].getKind()!=kind::BOUND_VARIABLE ){ @@ -83,7 +83,7 @@ struct QuantifierBoundVarListTypeRule { struct QuantifierInstPatternTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::INST_PATTERN ); + Assert(n.getKind() == kind::INST_PATTERN); if( check ){ TypeNode tn = n[0].getType(check); // this check catches the common mistake writing :pattern (f x) instead of :pattern ((f x)) @@ -98,7 +98,7 @@ struct QuantifierInstPatternTypeRule { struct QuantifierInstNoPatternTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::INST_NO_PATTERN ); + Assert(n.getKind() == kind::INST_NO_PATTERN); return nodeManager->instPatternType(); } };/* struct QuantifierInstNoPatternTypeRule */ @@ -106,7 +106,7 @@ struct QuantifierInstNoPatternTypeRule { struct QuantifierInstAttributeTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::INST_ATTRIBUTE ); + Assert(n.getKind() == kind::INST_ATTRIBUTE); return nodeManager->instPatternType(); } };/* struct QuantifierInstAttributeTypeRule */ @@ -114,7 +114,7 @@ struct QuantifierInstAttributeTypeRule { struct QuantifierInstPatternListTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::INST_PATTERN_LIST ); + Assert(n.getKind() == kind::INST_PATTERN_LIST); if( check ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ if( n[i].getKind()!=kind::INST_PATTERN && n[i].getKind()!=kind::INST_NO_PATTERN && n[i].getKind()!=kind::INST_ATTRIBUTE ){ @@ -129,7 +129,7 @@ struct QuantifierInstPatternListTypeRule { struct QuantifierInstClosureTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::INST_CLOSURE ); + Assert(n.getKind() == kind::INST_CLOSURE); if( check ){ TypeNode tn = n[0].getType(check); if( tn.isBoolean() ){ @@ -157,7 +157,7 @@ public: bool check) { Debug("typecheck-r") << "type check for rr " << n << std::endl; - Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 ); + Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren() == 3); if( check ){ if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ throw TypeCheckingExceptionPrivate(n[0], @@ -182,7 +182,7 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::RR_REWRITE ); + Assert(n.getKind() == kind::RR_REWRITE); if( check ){ if( n[0].getType(check)!=n[1].getType(check) ){ throw TypeCheckingExceptionPrivate(n, @@ -204,8 +204,8 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::RR_REDUCTION || - n.getKind() == kind::RR_DEDUCTION ); + Assert(n.getKind() == kind::RR_REDUCTION + || n.getKind() == kind::RR_DEDUCTION); if( check ){ if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){ throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean"); |