From 31f2135ad14b12e2ee9a24f5ca0da06cf5ed7b92 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 27 Aug 2020 20:30:18 -0500 Subject: (new theory) Update TheorySep to new interface (#4947) This updates the theory of separation logic to the new interface, which involves splitting up its check method based on the 4 check callbacks and using the theory state in the standard way. No behavior changes, unfortunately a lot of code had to change indentation and was updated to new coding guidelines. --- src/theory/sep/theory_sep.cpp | 1171 ++++++++++++++++++++++------------------- 1 file changed, 640 insertions(+), 531 deletions(-) (limited to 'src/theory/sep/theory_sep.cpp') diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 0059d9f3a..dc8ec9203 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -34,6 +34,7 @@ #include "theory/valuation.h" using namespace std; +using namespace CVC4::kind; namespace CVC4 { namespace theory { @@ -50,7 +51,6 @@ TheorySep::TheorySep(context::Context* c, d_bounds_init(false), d_state(c, u, valuation), d_notify(*this), - d_conflict(c, false), d_reduce(u), d_infer(c), d_infer_exp(c), @@ -115,18 +115,18 @@ bool TheorySep::propagateLit(TNode literal) { Debug("sep") << "TheorySep::propagateLit(" << literal << ")" << std::endl; // If already in conflict, no more propagation - if (d_conflict) { + if (d_state.isInConflict()) + { Debug("sep") << "TheorySep::propagateLit(" << literal << "): already in conflict" << std::endl; return false; } bool ok = d_out->propagate(literal); if (!ok) { - d_conflict = true; + d_state.notifyInConflict(); } return ok; -}/* TheorySep::propagate(TNode) */ - +} void TheorySep::explain(TNode literal, std::vector& assumptions) { if( literal.getKind()==kind::SEP_LABEL || @@ -160,29 +160,6 @@ TrustNode TheorySep::explain(TNode literal) // SHARING ///////////////////////////////////////////////////////////////////////////// -void TheorySep::notifySharedTerm(TNode t) -{ - Debug("sep") << "TheorySep::notifySharedTerm(" << t << ")" << std::endl; - d_equalityEngine->addTriggerTerm(t, THEORY_SEP); -} - - -EqualityStatus TheorySep::getEqualityStatus(TNode a, TNode b) { - Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); - if (d_equalityEngine->areEqual(a, b)) - { - // The terms are implied to be equal - return EQUALITY_TRUE; - } - else if (d_equalityEngine->areDisequal(a, b, false)) - { - // The terms are implied to be dis-equal - return EQUALITY_FALSE; - } - return EQUALITY_UNKNOWN;//FALSE_IN_MODEL; -} - - void TheorySep::computeCareGraph() { Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl; for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { @@ -213,17 +190,6 @@ void TheorySep::computeCareGraph() { // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// -bool TheorySep::collectModelInfo(TheoryModel* m) -{ - set termSet; - - // Compute terms appearing in assertions and shared terms - computeRelevantTerms(termSet); - - // Send the equality engine information to the model - return m->assertEqualityEngine(d_equalityEngine, &termSet); -} - void TheorySep::postProcessModel( TheoryModel* m ){ Trace("sep-model") << "Printing model for TheorySep..." << std::endl; @@ -312,532 +278,664 @@ void TheorySep::presolve() { // MAIN SOLVER ///////////////////////////////////////////////////////////////////////////// - -void TheorySep::check(Effort e) { - if (done() && !fullEffort(e) && e != EFFORT_LAST_CALL) { - return; +bool TheorySep::preNotifyFact( + TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal) +{ + TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom; + TNode slbl = atom.getKind() == SEP_LABEL ? atom[1] : TNode::null(); + bool isSpatial = isSpatialKind(satom.getKind()); + if (isSpatial) + { + reduceFact(atom, polarity, fact); + if (!slbl.isNull()) + { + d_spatial_assertions.push_back(fact); + } } + // assert to equality if non-spatial or a labelled pto + if (!isSpatial || (!slbl.isNull() && satom.getKind() == SEP_PTO)) + { + return false; + } + // otherwise, maybe propagate + doPendingFacts(); + return true; +} - getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep); +void TheorySep::notifyFact(TNode atom, + bool polarity, + TNode fact, + bool isInternal) +{ + TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom; + if (atom.getKind() == SEP_LABEL && atom[0].getKind() == SEP_PTO) + { + // associate the equivalence class of the lhs with this pto + Node r = getRepresentative(atom[1]); + HeapAssertInfo* ei = getOrMakeEqcInfo(r, true); + addPto(ei, r, atom, polarity); + } + // maybe propagate + doPendingFacts(); +} - TimerStat::CodeTimer checkTimer(d_checkTime); - Trace("sep-check") << "Sep::check(): " << e << endl; +void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) +{ + if (d_reduce.find(fact) != d_reduce.end()) + { + // already reduced + return; + } + d_reduce.insert(fact); + TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom; + TNode slbl = atom.getKind() == SEP_LABEL ? atom[1] : TNode::null(); NodeManager* nm = NodeManager::currentNM(); - - while( !done() && !d_conflict ){ - // Get all the assertions - Assertion assertion = get(); - TNode fact = assertion.d_assertion; - - Trace("sep-assert") << "TheorySep::check(): processing " << fact << std::endl; - - bool polarity = fact.getKind() != kind::NOT; - TNode atom = polarity ? fact : fact[0]; - /* - if( atom.getKind()==kind::SEP_EMP ){ - TypeNode tn = atom[0].getType(); - if( d_emp_arg.find( tn )==d_emp_arg.end() ){ - d_emp_arg[tn] = atom[0]; - }else{ - //normalize argument TODO - } + if (slbl.isNull()) + { + Trace("sep-lemma-debug") + << "Reducing unlabelled assertion " << atom << std::endl; + // introduce top-level label, add iff + TypeNode refType = getReferenceType(satom); + Trace("sep-lemma-debug") + << "...reference type is : " << refType << std::endl; + Node b_lbl = getBaseLabel(refType); + Node satom_new = nm->mkNode(SEP_LABEL, satom, b_lbl); + Node lem; + Trace("sep-lemma-debug") << "...polarity is " << polarity << std::endl; + if (polarity) + { + lem = nm->mkNode(OR, satom.negate(), satom_new); } - */ - TNode s_atom = atom.getKind()==kind::SEP_LABEL ? atom[0] : atom; - TNode s_lbl = atom.getKind()==kind::SEP_LABEL ? atom[1] : TNode::null(); - bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_EMP; - if( is_spatial && s_lbl.isNull() ){ - if( d_reduce.find( fact )==d_reduce.end() ){ - Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl; - d_reduce.insert( fact ); - //introduce top-level label, add iff - TypeNode refType = getReferenceType( s_atom ); - Trace("sep-lemma-debug") << "...reference type is : " << refType << std::endl; - Node b_lbl = getBaseLabel( refType ); - Node s_atom_new = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, s_atom, b_lbl ); - Node lem; - Trace("sep-lemma-debug") << "...polarity is " << polarity << std::endl; - if( polarity ){ - lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom.negate(), s_atom_new ); - }else{ - lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom, s_atom_new.negate() ); - } - Trace("sep-lemma-debug") << "Sep::Lemma : base reduction : " << lem << std::endl; - d_out->lemma( lem ); + else + { + lem = nm->mkNode(OR, satom, satom_new.negate()); + } + Trace("sep-lemma-debug") + << "Sep::Lemma : base reduction : " << lem << std::endl; + d_out->lemma(lem); + return; + } + Trace("sep-lemma-debug") << "Reducing assertion " << fact << std::endl; + Node conc; + if (Node* in_map = FindOrNull(d_red_conc[slbl], satom)) + { + conc = *in_map; + } + else + { + // make conclusion based on type of assertion + if (satom.getKind() == SEP_STAR || satom.getKind() == SEP_WAND) + { + std::vector children; + std::vector c_lems; + TypeNode tn = getReferenceType(satom); + if (d_reference_bound_max.find(tn) != d_reference_bound_max.end()) + { + c_lems.push_back(nm->mkNode(SUBSET, slbl, d_reference_bound_max[tn])); } - }else{ - //do reductions - if( is_spatial ){ - if( d_reduce.find( fact )==d_reduce.end() ){ - Trace("sep-lemma-debug") << "Reducing assertion " << fact << std::endl; - d_reduce.insert( fact ); - Node conc; - if (Node* in_map = FindOrNull(d_red_conc[s_lbl], s_atom)) - { - conc = *in_map; - } - else + std::vector labels; + getLabelChildren(satom, slbl, children, labels); + Node empSet = nm->mkConst(EmptySet(slbl.getType())); + Assert(children.size() > 1); + if (satom.getKind() == SEP_STAR) + { + // reduction for heap : union, pairwise disjoint + Node ulem = nm->mkNode(UNION, labels[0], labels[1]); + size_t lsize = labels.size(); + for (size_t i = 2; i < lsize; i++) + { + ulem = nm->mkNode(UNION, ulem, labels[i]); + } + ulem = slbl.eqNode(ulem); + Trace("sep-lemma-debug") + << "Sep::Lemma : star reduction, union : " << ulem << std::endl; + c_lems.push_back(ulem); + for (size_t i = 0; i < lsize; i++) + { + for (size_t j = (i + 1); j < lsize; j++) { - //make conclusion based on type of assertion - if( s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND ){ - std::vector< Node > children; - std::vector< Node > c_lems; - TypeNode tn = getReferenceType( s_atom ); - if( d_reference_bound_max.find( tn )!=d_reference_bound_max.end() ){ - c_lems.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, s_lbl, d_reference_bound_max[tn] ) ); - } - std::vector< Node > labels; - getLabelChildren( s_atom, s_lbl, children, labels ); - Node empSet = - NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType())); - Assert(children.size() > 1); - if( s_atom.getKind()==kind::SEP_STAR ){ - //reduction for heap : union, pairwise disjoint - Node ulem = NodeManager::currentNM()->mkNode( kind::UNION, labels[0], labels[1] ); - for( unsigned i=2; imkNode( kind::UNION, ulem, labels[i] ); - } - ulem = s_lbl.eqNode( ulem ); - Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, union : " << ulem << std::endl; - c_lems.push_back( ulem ); - for( unsigned i=0; imkNode( kind::INTERSECTION, labels[i], labels[j] ); - Node ilem = s.eqNode( empSet ); - Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, disjoint : " << ilem << std::endl; - c_lems.push_back( ilem ); - } - } - }else{ - Node ulem = NodeManager::currentNM()->mkNode( kind::UNION, s_lbl, labels[0] ); - ulem = ulem.eqNode( labels[1] ); - Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, union : " << ulem << std::endl; - c_lems.push_back( ulem ); - Node s = NodeManager::currentNM()->mkNode( kind::INTERSECTION, s_lbl, labels[0] ); - Node ilem = s.eqNode( empSet ); - Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl; - c_lems.push_back( ilem ); - //nil does not occur in labels[0] - Node nr = getNilRef( tn ); - Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, labels[0] ).negate(); - Trace("sep-lemma") << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem << std::endl; - d_out->lemma( nrlem ); - } - //send out definitional lemmas for introduced sets - for( unsigned j=0; jlemma( c_lems[j] ); - } - //children.insert( children.end(), c_lems.begin(), c_lems.end() ); - conc = NodeManager::currentNM()->mkNode( kind::AND, children ); - }else if( s_atom.getKind()==kind::SEP_PTO ){ - Node ss = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] ); - if( s_lbl!=ss ){ - conc = s_lbl.eqNode( ss ); - } - //not needed anymore: semantics of sep.nil is enforced globally - //Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate(); - //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn ); - - }else if( s_atom.getKind()==kind::SEP_EMP ){ - // conc = s_lbl.eqNode( - // NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType())) ); - Node lem; - Node emp_s = - NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType())); - if( polarity ){ - lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), s_lbl.eqNode( emp_s ) ); - }else{ - Node kl = NodeManager::currentNM()->mkSkolem( "loc", getReferenceType( s_atom ) ); - Node kd = NodeManager::currentNM()->mkSkolem( "data", getDataType( s_atom ) ); - Node econc = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, - NodeManager::currentNM()->mkNode( kind::SEP_STAR, NodeManager::currentNM()->mkNode( kind::SEP_PTO, kl, kd ), d_true ), s_lbl ); - //Node econc = NodeManager::currentNM()->mkNode( kind::AND, s_lbl.eqNode( emp_s ).negate(), - lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), econc ); - } - Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl; - d_out->lemma( lem ); - - }else{ - //labeled emp should be rewritten - Assert(false); - } - d_red_conc[s_lbl][s_atom] = conc; - } - if( !conc.isNull() ){ - bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity; - if( !use_polarity ){ - // introduce guard, assert positive version - Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact << std::endl; - Node g = nm->mkSkolem("G", nm->booleanType()); - d_neg_guard_strategy[g].reset(new DecisionStrategySingleton( - "sep_neg_guard", g, getSatContext(), getValuation())); - DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get(); - getDecisionManager()->registerStrategy( - DecisionManager::STRAT_SEP_NEG_GUARD, ds); - Node lit = ds->getLiteral(0); - d_neg_guard[s_lbl][s_atom] = lit; - Trace("sep-lemma-debug") << "Neg guard : " << s_lbl << " " << s_atom << " " << lit << std::endl; - AlwaysAssert(!lit.isNull()); - d_neg_guards.push_back( lit ); - d_guard_to_assertion[lit] = s_atom; - //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc ); - Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit.negate(), conc ); - Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl; - d_out->lemma( lem ); - }else{ - //reduce based on implication - Node lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), conc ); - Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem << std::endl; - d_out->lemma( lem ); - } - }else{ - Trace("sep-lemma-debug") << "Trivial conclusion, do not add lemma." << std::endl; + Node s = nm->mkNode(INTERSECTION, labels[i], labels[j]); + Node ilem = s.eqNode(empSet); + Trace("sep-lemma-debug") + << "Sep::Lemma : star reduction, disjoint : " << ilem + << std::endl; + c_lems.push_back(ilem); } } } - //assert to equality engine - if( !is_spatial ){ - Trace("sep-assert") << "Asserting " << atom << ", pol = " << polarity << " to EE..." << std::endl; - if( s_atom.getKind()==kind::EQUAL ){ - d_equalityEngine->assertEquality(atom, polarity, fact); - }else{ - d_equalityEngine->assertPredicate(atom, polarity, fact); - } - Trace("sep-assert") << "Done asserting " << atom << " to EE." << std::endl; - }else if( s_atom.getKind()==kind::SEP_PTO ){ - Node pto_lbl = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] ); - Assert(s_lbl == pto_lbl); - Trace("sep-assert") << "Asserting " << s_atom << std::endl; - d_equalityEngine->assertPredicate(s_atom, polarity, fact); - //associate the equivalence class of the lhs with this pto - Node r = getRepresentative( s_lbl ); - HeapAssertInfo * ei = getOrMakeEqcInfo( r, true ); - addPto( ei, r, atom, polarity ); - } - //maybe propagate - doPendingFacts(); - //add to spatial assertions - if( !d_conflict && is_spatial ){ - d_spatial_assertions.push_back( fact ); + else + { + Node ulem = nm->mkNode(UNION, slbl, labels[0]); + ulem = ulem.eqNode(labels[1]); + Trace("sep-lemma-debug") + << "Sep::Lemma : wand reduction, union : " << ulem << std::endl; + c_lems.push_back(ulem); + Node s = nm->mkNode(INTERSECTION, slbl, labels[0]); + Node ilem = s.eqNode(empSet); + Trace("sep-lemma-debug") + << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl; + c_lems.push_back(ilem); + // nil does not occur in labels[0] + Node nr = getNilRef(tn); + Node nrlem = nm->mkNode(MEMBER, nr, labels[0]).negate(); + Trace("sep-lemma") + << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem + << std::endl; + d_out->lemma(nrlem); } + // send out definitional lemmas for introduced sets + for (const Node& clem : c_lems) + { + Trace("sep-lemma") << "Sep::Lemma : definition : " << clem << std::endl; + d_out->lemma(clem); + } + conc = nm->mkNode(AND, children); + } + else if (satom.getKind() == SEP_PTO) + { + Node ss = nm->mkNode(SINGLETON, satom[0]); + if (slbl != ss) + { + conc = slbl.eqNode(ss); + } + // note semantics of sep.nil is enforced globally + } + else if (satom.getKind() == SEP_EMP) + { + Node lem; + Node emp_s = nm->mkConst(EmptySet(slbl.getType())); + if (polarity) + { + lem = nm->mkNode(OR, fact.negate(), slbl.eqNode(emp_s)); + } + else + { + Node kl = nm->mkSkolem("loc", getReferenceType(satom)); + Node kd = nm->mkSkolem("data", getDataType(satom)); + Node econc = nm->mkNode( + SEP_LABEL, + nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true), + slbl); + // Node econc = nm->mkNode( AND, slbl.eqNode( emp_s ).negate(), + lem = nm->mkNode(OR, fact.negate(), econc); + } + Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl; + d_out->lemma(lem); } + else + { + // labeled emp should be rewritten + Unreachable(); + } + d_red_conc[slbl][satom] = conc; } + if (conc.isNull()) + { + Trace("sep-lemma-debug") + << "Trivial conclusion, do not add lemma." << std::endl; + return; + } + bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity; + if (!use_polarity) + { + // introduce guard, assert positive version + Trace("sep-lemma-debug") + << "Negated spatial constraint asserted to sep theory: " << fact + << std::endl; + Node g = nm->mkSkolem("G", nm->booleanType()); + d_neg_guard_strategy[g].reset(new DecisionStrategySingleton( + "sep_neg_guard", g, getSatContext(), getValuation())); + DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get(); + getDecisionManager()->registerStrategy(DecisionManager::STRAT_SEP_NEG_GUARD, + ds); + Node lit = ds->getLiteral(0); + d_neg_guard[slbl][satom] = lit; + Trace("sep-lemma-debug") + << "Neg guard : " << slbl << " " << satom << " " << lit << std::endl; + AlwaysAssert(!lit.isNull()); + d_neg_guards.push_back(lit); + d_guard_to_assertion[lit] = satom; + // Node lem = nm->mkNode( EQUAL, lit, conc ); + Node lem = nm->mkNode(OR, lit.negate(), conc); + Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl; + d_out->lemma(lem); + } + else + { + // reduce based on implication + Node lem = nm->mkNode(OR, fact.negate(), conc); + Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem << std::endl; + d_out->lemma(lem); + } +} - if( e == EFFORT_LAST_CALL && !d_conflict && !d_valuation.needCheck() ){ - Trace("sep-process") << "Checking heap at full effort..." << std::endl; - d_label_model.clear(); - d_tmodel.clear(); - d_pto_model.clear(); - Trace("sep-process") << "---Locations---" << std::endl; - std::map< Node, int > min_id; - for( std::map< TypeNode, std::vector< Node > >::iterator itt = d_type_references_all.begin(); itt != d_type_references_all.end(); ++itt ){ - for( unsigned k=0; ksecond.size(); k++ ){ - Node t = itt->second[k]; - Trace("sep-process") << " " << t << " = "; - if( d_valuation.getModel()->hasTerm( t ) ){ - Node v = d_valuation.getModel()->getRepresentative( t ); - Trace("sep-process") << v << std::endl; - //take minimal id - std::map< Node, unsigned >::iterator itrc = d_type_ref_card_id.find( t ); - int tid = itrc==d_type_ref_card_id.end() ? -1 : (int)itrc->second; - bool set_term_model; - if( d_tmodel.find( v )==d_tmodel.end() ){ - set_term_model = true; - }else{ - set_term_model = min_id[v]>tid; - } - if( set_term_model ){ - d_tmodel[v] = t; - min_id[v] = tid; - } +bool TheorySep::isSpatialKind(Kind k) const +{ + return k == SEP_STAR || k == SEP_WAND || k == SEP_PTO || k == SEP_EMP; +} + +void TheorySep::postCheck(Effort level) +{ + if (level != EFFORT_LAST_CALL || d_state.isInConflict() + || d_valuation.needCheck()) + { + return; + } + NodeManager* nm = NodeManager::currentNM(); + Trace("sep-process") << "Checking heap at full effort..." << std::endl; + d_label_model.clear(); + d_tmodel.clear(); + d_pto_model.clear(); + Trace("sep-process") << "---Locations---" << std::endl; + std::map min_id; + for (std::map >::iterator itt = + d_type_references_all.begin(); + itt != d_type_references_all.end(); + ++itt) + { + for (const Node& t : itt->second) + { + Trace("sep-process") << " " << t << " = "; + if (d_valuation.getModel()->hasTerm(t)) + { + Node v = d_valuation.getModel()->getRepresentative(t); + Trace("sep-process") << v << std::endl; + // take minimal id + std::map::iterator itrc = d_type_ref_card_id.find(t); + int tid = itrc == d_type_ref_card_id.end() ? -1 : (int)itrc->second; + bool set_term_model; + if (d_tmodel.find(v) == d_tmodel.end()) + { + set_term_model = true; }else{ - Trace("sep-process") << "?" << std::endl; + set_term_model = min_id[v] > tid; } + if (set_term_model) + { + d_tmodel[v] = t; + min_id[v] = tid; + } + } + else + { + Trace("sep-process") << "?" << std::endl; } } - Trace("sep-process") << "---" << std::endl; - //build positive/negative assertion lists for labels - std::map< Node, bool > assert_active; - //get the inactive assertions - std::map< Node, std::vector< Node > > lbl_to_assertions; - for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { - Node fact = (*i); - bool polarity = fact.getKind() != kind::NOT; - TNode atom = polarity ? fact : fact[0]; - Assert(atom.getKind() == kind::SEP_LABEL); - TNode s_atom = atom[0]; - TNode s_lbl = atom[1]; - lbl_to_assertions[s_lbl].push_back( fact ); - //check whether assertion is active : either polarity=true, or guard is not asserted false - assert_active[fact] = true; - bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity; - if( use_polarity ){ - if( s_atom.getKind()==kind::SEP_PTO ){ - Node vv = d_valuation.getModel()->getRepresentative( s_atom[0] ); - if( d_pto_model.find( vv )==d_pto_model.end() ){ - Trace("sep-process") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl; - d_pto_model[vv] = s_atom[1]; - - //replace this on pto-model since this term is more relevant - TypeNode vtn = vv.getType(); - if( std::find( d_type_references_all[vtn].begin(), d_type_references_all[vtn].end(), s_atom[0] )!=d_type_references_all[vtn].end() ){ - d_tmodel[vv] = s_atom[0]; - } - } - } - }else{ - if( d_neg_guard[s_lbl].find( s_atom )!=d_neg_guard[s_lbl].end() ){ - //check if the guard is asserted positively - Node guard = d_neg_guard[s_lbl][s_atom]; - bool value; - if( getValuation().hasSatValue( guard, value ) ) { - assert_active[fact] = value; + } + Trace("sep-process") << "---" << std::endl; + // build positive/negative assertion lists for labels + std::map assert_active; + // get the inactive assertions + std::map > lbl_to_assertions; + for (NodeList::const_iterator i = d_spatial_assertions.begin(); + i != d_spatial_assertions.end(); + ++i) + { + Node fact = (*i); + bool polarity = fact.getKind() != NOT; + TNode atom = polarity ? fact : fact[0]; + Assert(atom.getKind() == SEP_LABEL); + TNode satom = atom[0]; + TNode slbl = atom[1]; + lbl_to_assertions[slbl].push_back(fact); + // check whether assertion is active : either polarity=true, or guard is not + // asserted false + assert_active[fact] = true; + bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity; + if (use_polarity) + { + if (satom.getKind() == SEP_PTO) + { + Node vv = d_valuation.getModel()->getRepresentative(satom[0]); + if (d_pto_model.find(vv) == d_pto_model.end()) + { + Trace("sep-process") << "Pto : " << satom[0] << " (" << vv << ") -> " + << satom[1] << std::endl; + d_pto_model[vv] = satom[1]; + + // replace this on pto-model since this term is more relevant + TypeNode vtn = vv.getType(); + if (std::find(d_type_references_all[vtn].begin(), + d_type_references_all[vtn].end(), + satom[0]) + != d_type_references_all[vtn].end()) + { + d_tmodel[vv] = satom[0]; } } } } - //(recursively) set inactive sub-assertions - for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { - Node fact = (*i); - if( !assert_active[fact] ){ - setInactiveAssertionRec( fact, lbl_to_assertions, assert_active ); + else + { + if (d_neg_guard[slbl].find(satom) != d_neg_guard[slbl].end()) + { + // check if the guard is asserted positively + Node guard = d_neg_guard[slbl][satom]; + bool value; + if (getValuation().hasSatValue(guard, value)) + { + assert_active[fact] = value; + } } } - //set up model information based on active assertions + } + //(recursively) set inactive sub-assertions + for (NodeList::const_iterator i = d_spatial_assertions.begin(); + i != d_spatial_assertions.end(); + ++i) + { + Node fact = (*i); + if (!assert_active[fact]) + { + setInactiveAssertionRec(fact, lbl_to_assertions, assert_active); + } + } + // set up model information based on active assertions + for (NodeList::const_iterator i = d_spatial_assertions.begin(); + i != d_spatial_assertions.end(); + ++i) + { + Node fact = (*i); + bool polarity = fact.getKind() != NOT; + TNode atom = polarity ? fact : fact[0]; + TNode satom = atom[0]; + TNode slbl = atom[1]; + if (assert_active[fact]) + { + computeLabelModel(slbl); + } + } + // debug print + if (Trace.isOn("sep-process")) + { + Trace("sep-process") << "--- Current spatial assertions : " << std::endl; for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { Node fact = (*i); - bool polarity = fact.getKind() != kind::NOT; - TNode atom = polarity ? fact : fact[0]; - TNode s_atom = atom[0]; - TNode s_lbl = atom[1]; - if( assert_active[fact] ){ - computeLabelModel( s_lbl ); - } - } - //debug print - if( Trace.isOn("sep-process") ){ - Trace("sep-process") << "--- Current spatial assertions : " << std::endl; - for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { - Node fact = (*i); - Trace("sep-process") << " " << fact; - if( !assert_active[fact] ){ - Trace("sep-process") << " [inactive]"; - } - Trace("sep-process") << std::endl; + Trace("sep-process") << " " << fact; + if (!assert_active[fact]) + { + Trace("sep-process") << " [inactive]"; } - Trace("sep-process") << "---" << std::endl; + Trace("sep-process") << std::endl; } - if(Trace.isOn("sep-eqc")) { - eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine); - Trace("sep-eqc") << "EQC:" << std::endl; - while( !eqcs2_i.isFinished() ){ - Node eqc = (*eqcs2_i); - eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine); - Trace("sep-eqc") << "Eqc( " << eqc << " ) : { "; - while( !eqc2_i.isFinished() ) { - if( (*eqc2_i)!=eqc ){ - Trace("sep-eqc") << (*eqc2_i) << " "; - } - ++eqc2_i; + Trace("sep-process") << "---" << std::endl; + } + if (Trace.isOn("sep-eqc")) + { + eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine); + Trace("sep-eqc") << "EQC:" << std::endl; + while (!eqcs2_i.isFinished()) + { + Node eqc = (*eqcs2_i); + eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine); + Trace("sep-eqc") << "Eqc( " << eqc << " ) : { "; + while (!eqc2_i.isFinished()) + { + if ((*eqc2_i) != eqc) + { + Trace("sep-eqc") << (*eqc2_i) << " "; } - Trace("sep-eqc") << " } " << std::endl; - ++eqcs2_i; + ++eqc2_i; } - Trace("sep-eqc") << std::endl; + Trace("sep-eqc") << " } " << std::endl; + ++eqcs2_i; } - - bool addedLemma = false; - bool needAddLemma = false; - //check negated star / positive wand - if( options::sepCheckNeg() ){ - //get active labels - std::map< Node, bool > active_lbl; - if( options::sepMinimalRefine() ){ - for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { - Node fact = (*i); - bool polarity = fact.getKind() != kind::NOT; - TNode atom = polarity ? fact : fact[0]; - TNode s_atom = atom[0]; - bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity; - if( !use_polarity ){ - Assert(assert_active.find(fact) != assert_active.end()); - if( assert_active[fact] ){ - Assert(atom.getKind() == kind::SEP_LABEL); - TNode s_lbl = atom[1]; - std::map >& lms = d_label_map[s_atom]; - if (lms.find(s_lbl) != lms.end()) - { - Trace("sep-process-debug") << "Active lbl : " << s_lbl << std::endl; - active_lbl[s_lbl] = true; - } - } - } - } - } + Trace("sep-eqc") << std::endl; + } - //process spatial assertions + bool addedLemma = false; + bool needAddLemma = false; + // check negated star / positive wand + if (options::sepCheckNeg()) + { + // get active labels + std::map active_lbl; + if (options::sepMinimalRefine()) + { for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { Node fact = (*i); - bool polarity = fact.getKind() != kind::NOT; + bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; - TNode s_atom = atom[0]; - - bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity; - Trace("sep-process-debug") << " check atom : " << s_atom << " use polarity " << use_polarity << std::endl; + TNode satom = atom[0]; + bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity; if( !use_polarity ){ Assert(assert_active.find(fact) != assert_active.end()); if( assert_active[fact] ){ - Assert(atom.getKind() == kind::SEP_LABEL); - TNode s_lbl = atom[1]; - Trace("sep-process") << "--> Active negated atom : " << s_atom << ", lbl = " << s_lbl << std::endl; - //add refinement lemma - if (ContainsKey(d_label_map[s_atom], s_lbl)) - { - needAddLemma = true; - TypeNode tn = getReferenceType( s_atom ); - tn = NodeManager::currentNM()->mkSetType(tn); - //tn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn)); - Node o_b_lbl_mval = d_label_model[s_lbl].getValue( tn ); - Trace("sep-process") << " Model for " << s_lbl << " : " << o_b_lbl_mval << std::endl; - - //get model values - std::map< int, Node > mvals; - for (const std::pair& sub_element : - d_label_map[s_atom][s_lbl]) - { - int sub_index = sub_element.first; - Node sub_lbl = sub_element.second; - computeLabelModel( sub_lbl ); - Node lbl_mval = d_label_model[sub_lbl].getValue( tn ); - Trace("sep-process-debug") << " child " << sub_index << " : " << sub_lbl << ", mval = " << lbl_mval << std::endl; - mvals[sub_index] = lbl_mval; - } - - // Now, assert model-instantiated implication based on the negation - Assert(d_label_model.find(s_lbl) != d_label_model.end()); - std::vector< Node > conc; - bool inst_success = true; - //new refinement - //instantiate the label - std::map< Node, Node > visited; - Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, tn, active_lbl ); - Trace("sep-inst-debug") << " applied inst : " << inst << std::endl; - if( inst.isNull() ){ - inst_success = false; - }else{ - inst = Rewriter::rewrite( inst ); - if( inst==( polarity ? d_true : d_false ) ){ - inst_success = false; - } - conc.push_back( polarity ? inst : inst.negate() ); - } - if( inst_success ){ - std::vector< Node > lemc; - Node pol_atom = atom; - if( polarity ){ - pol_atom = atom.negate(); - } - lemc.push_back( pol_atom ); - - //lemc.push_back( s_lbl.eqNode( o_b_lbl_mval ).negate() ); - //lemc.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, o_b_lbl_mval, s_lbl ).negate() ); - lemc.insert( lemc.end(), conc.begin(), conc.end() ); - Node lem = NodeManager::currentNM()->mkNode( kind::OR, lemc ); - if( std::find( d_refinement_lem[s_atom][s_lbl].begin(), d_refinement_lem[s_atom][s_lbl].end(), lem )==d_refinement_lem[s_atom][s_lbl].end() ){ - d_refinement_lem[s_atom][s_lbl].push_back( lem ); - Trace("sep-process") << "-----> refinement lemma (#" << d_refinement_lem[s_atom][s_lbl].size() << ") : " << lem << std::endl; - Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " << lem << std::endl; - d_out->lemma( lem ); - addedLemma = true; - }else{ - //this typically should not happen, should never happen for complete base theories - Trace("sep-process") << "*** repeated refinement lemma : " << lem << std::endl; - Trace("sep-warn") << "TheorySep : WARNING : repeated refinement lemma : " << lem << "!!!" << std::endl; - } - } - } - else + Assert(atom.getKind() == SEP_LABEL); + TNode slbl = atom[1]; + std::map >& lms = d_label_map[satom]; + if (lms.find(slbl) != lms.end()) { - Trace("sep-process-debug") << " no children." << std::endl; - Assert(s_atom.getKind() == kind::SEP_PTO - || s_atom.getKind() == kind::SEP_EMP); + Trace("sep-process-debug") + << "Active lbl : " << slbl << std::endl; + active_lbl[slbl] = true; } - }else{ - Trace("sep-process-debug") << "--> inactive negated assertion " << s_atom << std::endl; } } } - Trace("sep-process") << "...finished check of negated assertions, addedLemma=" << addedLemma << ", needAddLemma=" << needAddLemma << std::endl; } - if( !addedLemma ){ - //must witness finite data points-to - for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){ - TypeNode data_type = d_loc_to_data_type[it->first]; - //if the data type is finite - if( data_type.isInterpretedFinite() ){ - computeLabelModel( it->second ); - Trace("sep-process-debug") << "Check heap data for " << it->first << " -> " << data_type << std::endl; - for( unsigned j=0; jsecond].d_heap_locs_model.size(); j++ ){ - Assert(d_label_model[it->second].d_heap_locs_model[j].getKind() - == kind::SINGLETON); - Node l = d_label_model[it->second].d_heap_locs_model[j][0]; - Trace("sep-process-debug") << " location : " << l << std::endl; - if( d_pto_model[l].isNull() ){ - needAddLemma = true; - Node ll; - std::map< Node, Node >::iterator itm = d_tmodel.find( l ); - if( itm!=d_tmodel.end() ) { - ll = itm->second; - }else{ - //try to assign arbitrary skolem? - } - if( !ll.isNull() ){ - Trace("sep-process") << "Must witness label : " << ll << ", data type is " << data_type << std::endl; - Node dsk = NodeManager::currentNM()->mkSkolem( "dsk", data_type, "pto-data for implicit location" ); - // if location is in the heap, then something must point to it - Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::MEMBER, ll, it->second ), - NodeManager::currentNM()->mkNode( kind::SEP_STAR, - NodeManager::currentNM()->mkNode( kind::SEP_PTO, ll, dsk ), - d_true ) ); - Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem << std::endl; - d_out->lemma( lem ); - addedLemma = true; - }else{ - //This should only happen if we are in an unbounded fragment - Trace("sep-warn") << "TheorySep : WARNING : no term corresponding to location " << l << " in heap!!!" << std::endl; - } - }else{ - Trace("sep-process-debug") << " points-to data witness : " << d_pto_model[l] << std::endl; - } - } - } + + // process spatial assertions + for (NodeList::const_iterator i = d_spatial_assertions.begin(); + i != d_spatial_assertions.end(); + ++i) + { + Node fact = (*i); + bool polarity = fact.getKind() != NOT; + TNode atom = polarity ? fact : fact[0]; + TNode satom = atom[0]; + + bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity; + Trace("sep-process-debug") + << " check atom : " << satom << " use polarity " << use_polarity + << std::endl; + if (use_polarity) + { + continue; } - if( !addedLemma ){ - //set up model - Trace("sep-process-debug") << "...preparing sep model..." << std::endl; - d_heap_locs_nptos.clear(); - //collect data points that are not pointed to - for( context::CDList::const_iterator it = facts_begin(); it != facts_end(); ++ it) { - Node lit = (*it).d_assertion; - if( lit.getKind()==kind::NOT && lit[0].getKind()==kind::SEP_PTO ){ - Node s_atom = lit[0]; - Node v1 = d_valuation.getModel()->getRepresentative( s_atom[0] ); - Node v2 = d_valuation.getModel()->getRepresentative( s_atom[1] ); - Trace("sep-process-debug") << v1 << " does not point-to " << v2 << std::endl; - d_heap_locs_nptos[v1].push_back( v2 ); - } - } - - if( needAddLemma ){ - d_out->setIncomplete(); + Assert(assert_active.find(fact) != assert_active.end()); + if (!assert_active[fact]) + { + Trace("sep-process-debug") + << "--> inactive negated assertion " << satom << std::endl; + continue; + } + Assert(atom.getKind() == SEP_LABEL); + TNode slbl = atom[1]; + Trace("sep-process") << "--> Active negated atom : " << satom + << ", lbl = " << slbl << std::endl; + // add refinement lemma + if (!ContainsKey(d_label_map[satom], slbl)) + { + Trace("sep-process-debug") << " no children." << std::endl; + Assert(satom.getKind() == SEP_PTO || satom.getKind() == SEP_EMP); + continue; + } + needAddLemma = true; + TypeNode tn = getReferenceType(satom); + tn = nm->mkSetType(tn); + // tn = nm->mkSetType(nm->mkRefType(tn)); + Node o_b_lbl_mval = d_label_model[slbl].getValue(tn); + Trace("sep-process") << " Model for " << slbl << " : " << o_b_lbl_mval + << std::endl; + + // get model values + std::map mvals; + for (const std::pair& sub_element : d_label_map[satom][slbl]) + { + int sub_index = sub_element.first; + Node sub_lbl = sub_element.second; + computeLabelModel(sub_lbl); + Node lbl_mval = d_label_model[sub_lbl].getValue(tn); + Trace("sep-process-debug") + << " child " << sub_index << " : " << sub_lbl + << ", mval = " << lbl_mval << std::endl; + mvals[sub_index] = lbl_mval; + } + + // Now, assert model-instantiated implication based on the negation + Assert(d_label_model.find(slbl) != d_label_model.end()); + std::vector conc; + bool inst_success = true; + // new refinement + // instantiate the label + std::map visited; + Node inst = instantiateLabel(satom, + slbl, + slbl, + o_b_lbl_mval, + visited, + d_pto_model, + tn, + active_lbl); + Trace("sep-inst-debug") << " applied inst : " << inst << std::endl; + if (inst.isNull()) + { + inst_success = false; + } + else + { + inst = Rewriter::rewrite(inst); + if (inst == (polarity ? d_true : d_false)) + { + inst_success = false; } + conc.push_back(polarity ? inst : inst.negate()); + } + if (!inst_success) + { + continue; + } + std::vector lemc; + Node pol_atom = atom; + if (polarity) + { + pol_atom = atom.negate(); + } + lemc.push_back(pol_atom); + lemc.insert(lemc.end(), conc.begin(), conc.end()); + Node lem = nm->mkNode(OR, lemc); + std::vector& rlems = d_refinement_lem[satom][slbl]; + if (std::find(rlems.begin(), rlems.end(), lem) == rlems.end()) + { + rlems.push_back(lem); + Trace("sep-process") << "-----> refinement lemma (#" << rlems.size() + << ") : " << lem << std::endl; + Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " + << lem << std::endl; + d_out->lemma(lem); + addedLemma = true; + } + else + { + // this typically should not happen, should never happen for complete + // base theories + Trace("sep-process") + << "*** repeated refinement lemma : " << lem << std::endl; + Trace("sep-warn") + << "TheorySep : WARNING : repeated refinement lemma : " << lem + << "!!!" << std::endl; } } + Trace("sep-process") + << "...finished check of negated assertions, addedLemma=" << addedLemma + << ", needAddLemma=" << needAddLemma << std::endl; + } + if (addedLemma) + { + return; + } + // must witness finite data points-to + for (std::map::iterator it = d_base_label.begin(); + it != d_base_label.end(); + ++it) + { + TypeNode data_type = d_loc_to_data_type[it->first]; + // if the data type is finite + if (!data_type.isInterpretedFinite()) + { + continue; + } + computeLabelModel(it->second); + Trace("sep-process-debug") << "Check heap data for " << it->first << " -> " + << data_type << std::endl; + std::vector& hlmodel = d_label_model[it->second].d_heap_locs_model; + for (size_t j = 0, hsize = hlmodel.size(); j < hsize; j++) + { + Assert(hlmodel[j].getKind() == SINGLETON); + Node l = hlmodel[j][0]; + Trace("sep-process-debug") << " location : " << l << std::endl; + if (!d_pto_model[l].isNull()) + { + Trace("sep-process-debug") + << " points-to data witness : " << d_pto_model[l] << std::endl; + continue; + } + needAddLemma = true; + Node ll; + std::map::iterator itm = d_tmodel.find(l); + if (itm != d_tmodel.end()) + { + ll = itm->second; + } + // otherwise, could try to assign arbitrary skolem? + if (!ll.isNull()) + { + Trace("sep-process") << "Must witness label : " << ll + << ", data type is " << data_type << std::endl; + Node dsk = + nm->mkSkolem("dsk", data_type, "pto-data for implicit location"); + // if location is in the heap, then something must point to it + Node lem = nm->mkNode( + IMPLIES, + nm->mkNode(MEMBER, ll, it->second), + nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, ll, dsk), d_true)); + Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem + << std::endl; + d_out->lemma(lem); + addedLemma = true; + } + else + { + // This should only happen if we are in an unbounded fragment + Trace("sep-warn") + << "TheorySep : WARNING : no term corresponding to location " << l + << " in heap!!!" << std::endl; + } + } + } + if (addedLemma) + { + return; + } + // set up model + Trace("sep-process-debug") << "...preparing sep model..." << std::endl; + d_heap_locs_nptos.clear(); + // collect data points that are not pointed to + for (context::CDList::const_iterator it = facts_begin(); + it != facts_end(); + ++it) + { + Node lit = (*it).d_assertion; + if (lit.getKind() == NOT && lit[0].getKind() == SEP_PTO) + { + Node satom = lit[0]; + Node v1 = d_valuation.getModel()->getRepresentative(satom[0]); + Node v2 = d_valuation.getModel()->getRepresentative(satom[1]); + Trace("sep-process-debug") + << v1 << " does not point-to " << v2 << std::endl; + d_heap_locs_nptos[v1].push_back(v2); + } } - Trace("sep-check") << "Sep::check(): " << e << " done, conflict=" << d_conflict.get() << endl; -} + if (needAddLemma) + { + d_out->setIncomplete(); + } + Trace("sep-check") << "Sep::check(): " << level + << " done, conflict=" << d_state.isInConflict() + << std::endl; +} bool TheorySep::needsCheckLastEffort() { return hasFacts(); @@ -849,7 +947,7 @@ void TheorySep::conflict(TNode a, TNode b) { std::vector assumptions; explain(eq, assumptions); Node conflictNode = mkAnd(assumptions); - d_conflict = true; + d_state.notifyInConflict(); d_out->conflict( conflictNode ); } @@ -1486,11 +1584,13 @@ void TheorySep::setInactiveAssertionRec( Node fact, std::map< Node, std::vector< assert_active[fact] = false; bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; - TNode s_atom = atom[0]; - TNode s_lbl = atom[1]; - if( s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_STAR ){ - for( unsigned j=0; j& children, std::vector< Node >& labels ) { - for( unsigned i=0; i& children, + std::vector& labels) +{ + for (size_t i = 0, nchild = satom.getNumChildren(); i < nchild; i++) + { + Node lblc = getLabel(satom, i, lbl); Assert(!lblc.isNull()); std::map< Node, Node > visited; - Node lc = applyLabel( s_atom[i], lblc, visited ); + Node lc = applyLabel(satom[i], lblc, visited); Assert(!lc.isNull()); - if( i==1 && s_atom.getKind()==kind::SEP_WAND ){ + if (i == 1 && satom.getKind() == SEP_WAND) + { lc = lc.negate(); } children.push_back( lc ); @@ -1621,8 +1727,9 @@ void TheorySep::validatePto( HeapAssertInfo * ei, Node ei_n ) { { TNode atom = fact[0]; Assert(atom.getKind() == kind::SEP_LABEL); - TNode s_atom = atom[0]; - if( s_atom.getKind()==kind::SEP_PTO ){ + TNode satom = atom[0]; + if (satom.getKind() == SEP_PTO) + { if( areEqual( atom[1], ei_n ) ){ addPto( ei, ei_n, atom, false ); } @@ -1732,7 +1839,7 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, if( conc==d_false ){ Trace("sep-lemma") << "Sep::Conflict: " << ant_n << " by " << c << std::endl; d_out->conflict( ant_n ); - d_conflict = true; + d_state.notifyInConflict(); }else{ Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant_n << " by " << c << std::endl; d_pending_exp.push_back( ant_n ); @@ -1746,7 +1853,8 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, void TheorySep::doPendingFacts() { if( d_pending_lem.empty() ){ for( unsigned i=0; i