Kind k = n.getKind();
//datatype operators may be parametric, always assume they are
if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
- k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ){
+ k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){
//since it is parametric, use a particular one as op
TypeNode tn = n[0].getType();
Node op = n.getOperator();
bool Trigger::isAtomicTriggerKind( Kind k ) {
return k==APPLY_UF || k==SELECT || k==STORE ||
k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
- k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON;
+ k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
+ k==SEP_PTO;
}
bool Trigger::isRelationalTrigger( Node n ) {
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] );
- if( polarity && s_lbl!=pto_lbl ){
- //also propagate equality
- Node eq = s_lbl.eqNode( pto_lbl );
- Trace("sep-assert") << "Asserting implied equality " << eq << " to EE..." << std::endl;
- d_equalityEngine.assertEquality(eq, true, fact);
- Trace("sep-assert") << "Done asserting implied equality " << eq << " to EE." << std::endl;
- }
+ 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 );
Assert( areEqual( pb[1], p[1] ) );
std::vector< Node > exp;
if( pb[1]!=p[1] ){
+ //if( pb[1].getKind()==kind::SINGLETON && p[1].getKind()==kind::SINGLETON ){
+ // exp.push_back( pb[1][0].eqNode( p[1][0] ) );
+ //}else{
exp.push_back( pb[1].eqNode( p[1] ) );
+ //}
}
exp.push_back( pb );
exp.push_back( p.negate() );
// conc.push_back( pb[1].eqNode( p[1] ).negate() );
//}
Node n_conc = conc.empty() ? d_false : ( conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::OR, conc ) );
+ Trace("sep-pto") << "Conclusion is " << n_conc << std::endl;
+ // propagation for (pto x y) ^ ~(pto z w) ^ x = z => y != w
sendLemma( exp, n_conc, "PTO_NEG_PROP" );
}
}else{
}
exp.push_back( p1 );
exp.push_back( p2 );
+ //enforces injectiveness of pto : (pto x y) ^ (pto y w) ^ x = y => y = w
sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" );
}
}