#include "theory/valuation.h"
using namespace std;
+using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
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),
{
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<TNode>& assumptions) {
if( literal.getKind()==kind::SEP_LABEL ||
// 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) {
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
-bool TheorySep::collectModelInfo(TheoryModel* m)
-{
- set<Node> 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;
// 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<Node> children;
+ std::vector<Node> 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<Node> 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; i<labels.size(); i++ ){
- ulem = NodeManager::currentNM()->mkNode( 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; i<labels.size(); i++ ){
- for( unsigned j=(i+1); j<labels.size(); j++ ){
- Node s = NodeManager::currentNM()->mkNode( 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; j<c_lems.size(); j++ ){
- Trace("sep-lemma") << "Sep::Lemma : definition : " << c_lems[j] << std::endl;
- d_out->lemma( 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; k<itt->second.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<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 (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<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{
- 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<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() != 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<Node, std::map<int, Node> >& 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<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;
+ 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<int, Node>& 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<Node, std::map<int, Node> >& 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; j<d_label_model[it->second].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<Assertion>::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<int, Node> mvals;
+ for (const std::pair<int, Node>& 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<Node> conc;
+ bool inst_success = true;
+ // new refinement
+ // instantiate the label
+ std::map<Node, Node> 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<Node> 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<Node>& 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<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())
+ {
+ continue;
+ }
+ computeLabelModel(it->second);
+ Trace("sep-process-debug") << "Check heap data for " << it->first << " -> "
+ << data_type << std::endl;
+ std::vector<Node>& 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<Node, Node>::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<Assertion>::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();
std::vector<TNode> assumptions;
explain(eq, assumptions);
Node conflictNode = mkAnd(assumptions);
- d_conflict = true;
+ d_state.notifyInConflict();
d_out->conflict( conflictNode );
}
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<s_atom.getNumChildren(); j++ ){
- Node lblc = getLabel( s_atom, j, s_lbl );
+ TNode satom = atom[0];
+ TNode slbl = atom[1];
+ if (satom.getKind() == SEP_WAND || satom.getKind() == SEP_STAR)
+ {
+ for (size_t j = 0, nchild = satom.getNumChildren(); j < nchild; j++)
+ {
+ Node lblc = getLabel(satom, j, slbl);
for( unsigned k=0; k<lbl_to_assertions[lblc].size(); k++ ){
setInactiveAssertionRec( lbl_to_assertions[lblc][k], lbl_to_assertions, assert_active );
}
}
}
-void TheorySep::getLabelChildren( Node s_atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels ) {
- for( unsigned i=0; i<s_atom.getNumChildren(); i++ ){
- Node lblc = getLabel( s_atom, i, lbl );
+void TheorySep::getLabelChildren(Node satom,
+ Node lbl,
+ std::vector<Node>& children,
+ std::vector<Node>& 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 );
{
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 );
}
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 );
void TheorySep::doPendingFacts() {
if( d_pending_lem.empty() ){
for( unsigned i=0; i<d_pending.size(); i++ ){
- if( d_conflict ){
+ if (d_state.isInConflict())
+ {
break;
}
Node atom = d_pending[i].getKind()==kind::NOT ? d_pending[i][0] : d_pending[i];
}
}else{
for( unsigned i=0; i<d_pending_lem.size(); i++ ){
- if( d_conflict ){
+ if (d_state.isInConflict())
+ {
break;
}
int index = d_pending_lem[i];
projects / cvc5.git / commitdiff