--- /dev/null
+/********************* */
+/*! \file theory_sep.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of the theory of sep.
+ **
+ ** Implementation of the theory of sep.
+ **/
+
+
+#include "theory/sep/theory_sep.h"
+#include "theory/valuation.h"
+#include "expr/kind.h"
+#include <map>
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
+#include "options/sep_options.h"
+#include "options/smt_options.h"
+#include "smt/logic_exception.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace sep {
+
+TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true),
+ d_conflict(c, false),
+ d_reduce(u),
+ d_infer(c),
+ d_infer_exp(c),
+ d_spatial_assertions(c)
+{
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine.addFunctionKind(kind::SEP_PTO);
+ //d_equalityEngine.addFunctionKind(kind::SEP_STAR);
+}
+
+TheorySep::~TheorySep() {
+ for( std::map< Node, HeapAssertInfo * >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){
+ delete it->second;
+ }
+}
+
+void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
+Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
+ if( assumptions.empty() ){
+ return d_true;
+ }else if( assumptions.size()==1 ){
+ return assumptions[0];
+ }else{
+ return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
+ }
+}
+
+/////////////////////////////////////////////////////////////////////////////
+// PREPROCESSING
+/////////////////////////////////////////////////////////////////////////////
+
+
+
+Node TheorySep::ppRewrite(TNode term) {
+/*
+ Trace("sep-pp") << "ppRewrite : " << term << std::endl;
+ Node s_atom = term.getKind()==kind::NOT ? term[0] : term;
+ if( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::EMP_STAR ){
+ //get the reference type (will compute d_type_references)
+ int card = 0;
+ TypeNode tn = getReferenceType( s_atom, card );
+ Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl;
+ }
+*/
+ return term;
+}
+
+//must process assertions at preprocess so that quantified assertions are processed properly
+void TheorySep::processAssertions( std::vector< Node >& assertions ) {
+ std::map< Node, bool > visited;
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ processAssertion( assertions[i], visited );
+ }
+}
+
+void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::EMP_STAR ){
+ //get the reference type (will compute d_type_references)
+ int card = 0;
+ TypeNode tn = getReferenceType( n, card );
+ Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl;
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ processAssertion( n[i], visited );
+ }
+ }
+ }
+}
+
+Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+
+ return PP_ASSERT_STATUS_UNSOLVED;
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// T-PROPAGATION / REGISTRATION
+/////////////////////////////////////////////////////////////////////////////
+
+
+bool TheorySep::propagate(TNode literal)
+{
+ Debug("sep") << "TheorySep::propagate(" << literal << ")" << std::endl;
+ // If already in conflict, no more propagation
+ if (d_conflict) {
+ Debug("sep") << "TheorySep::propagate(" << literal << "): already in conflict" << std::endl;
+ return false;
+ }
+ bool ok = d_out->propagate(literal);
+ if (!ok) {
+ d_conflict = true;
+ }
+ return ok;
+}/* TheorySep::propagate(TNode) */
+
+
+void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
+ if( literal.getKind()==kind::SEP_LABEL ||
+ ( literal.getKind()==kind::NOT && literal[0].getKind()==kind::SEP_LABEL ) ){
+ //labelled assertions are never given to equality engine and should only come from the outside
+ assumptions.push_back( literal );
+ }else{
+ // Do the work
+ bool polarity = literal.getKind() != kind::NOT;
+ TNode atom = polarity ? literal : literal[0];
+ if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ d_equalityEngine.explainEquality( atom[0], atom[1], polarity, assumptions, NULL );
+ } else {
+ d_equalityEngine.explainPredicate( atom, polarity, assumptions );
+ }
+ }
+}
+
+void TheorySep::preRegisterTerm(TNode node){
+
+}
+
+
+void TheorySep::propagate(Effort e){
+
+}
+
+
+Node TheorySep::explain(TNode literal)
+{
+ Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl;
+ std::vector<TNode> assumptions;
+ explain(literal, assumptions);
+ return mkAnd(assumptions);
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// SHARING
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheorySep::addSharedTerm(TNode t) {
+ Debug("sep") << "TheorySep::addSharedTerm(" << 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) {
+ TNode a = d_sharedTerms[i];
+ TypeNode aType = a.getType();
+ for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
+ TNode b = d_sharedTerms[j];
+ if (b.getType() != aType) {
+ // We don't care about the terms of different types
+ continue;
+ }
+ switch (d_valuation.getEqualityStatus(a, b)) {
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ case EQUALITY_FALSE_AND_PROPAGATED:
+ // If we know about it, we should have propagated it, so we can skip
+ break;
+ default:
+ // Let's split on it
+ addCarePair(a, b);
+ break;
+ }
+ }
+ }
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// MODEL GENERATION
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel )
+{
+ // Send the equality engine information to the model
+ m->assertEqualityEngine( &d_equalityEngine );
+
+ if( fullModel ){
+ for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){
+ computeLabelModel( it->second, d_tmodel );
+ //, (label = " << it->second << ")
+ Trace("sep-model") << "Model for heap, type = " << it->first << " : " << std::endl;
+ if( d_label_model[it->second].d_heap_locs_model.empty() ){
+ Trace("sep-model") << " [empty]" << std::endl;
+ }else{
+ 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-model") << " " << l << " -> ";
+ if( d_pto_model[l].isNull() ){
+ Trace("sep-model") << "_";
+ }else{
+ Trace("sep-model") << d_pto_model[l];
+ }
+ Trace("sep-model") << std::endl;
+ }
+ }
+ Node nil = getNilRef( it->first );
+ Node vnil = d_valuation.getModel()->getRepresentative( nil );
+ Trace("sep-model") << "sep.nil = " << vnil << std::endl;
+ Trace("sep-model") << std::endl;
+ }
+ }
+}
+
+/////////////////////////////////////////////////////////////////////////////
+// NOTIFICATIONS
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheorySep::presolve() {
+ Trace("sep-pp") << "Presolving" << std::endl;
+ //TODO: cleanup if incremental?
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// MAIN SOLVER
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheorySep::check(Effort e) {
+ if (done() && !fullEffort(e) && e != EFFORT_LAST_CALL) {
+ return;
+ }
+
+ getOutputChannel().spendResource(options::theoryCheckStep());
+
+ TimerStat::CodeTimer checkTimer(d_checkTime);
+ Trace("sep-check") << "Sep::check(): " << e << endl;
+
+ while( !done() && !d_conflict ){
+ // Get all the assertions
+ Assertion assertion = get();
+ TNode fact = assertion.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::EMP_STAR ){
+ 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
+ }
+ }
+ 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::EMP_STAR;
+ 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
+ int card;
+ TypeNode refType = getReferenceType( s_atom, card );
+ Trace("sep-lemma-debug") << "...reference type is : " << refType << ", card is " << card << std::endl;
+ Node b_lbl = getBaseLabel( refType );
+ Node s_atom_new = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, s_atom, b_lbl );
+ Node lem;
+ 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{
+ //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;
+ std::map< Node, Node >::iterator its = d_red_conc[s_lbl].find( s_atom );
+ if( its==d_red_conc[s_lbl].end() ){
+ //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;
+ int card;
+ TypeNode tn = getReferenceType( s_atom, card );
+ Assert( d_reference_bound.find( tn )!=d_reference_bound.end() );
+ c_lems.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, s_lbl, d_reference_bound[tn] ) );
+ if( options::sepPreciseBound() ){
+ //more precise bound
+ Trace("sep-bound") << "Propagate Bound(" << s_lbl << ") = ";
+ Assert( d_lbl_reference_bound.find( s_lbl )!=d_lbl_reference_bound.end() );
+ for( unsigned j=0; j<d_lbl_reference_bound[s_lbl].size(); j++ ){
+ Trace("sep-bound") << d_lbl_reference_bound[s_lbl][j] << " ";
+ }
+ Trace("sep-bound") << std::endl << " to children of " << s_atom << std::endl;
+ //int rb_start = 0;
+ for( unsigned j=0; j<s_atom.getNumChildren(); j++ ){
+ int ccard = 0;
+ getReferenceType( s_atom, ccard, j );
+ Node c_lbl = getLabel( s_atom, j, s_lbl );
+ Trace("sep-bound") << " for " << c_lbl << ", card = " << ccard << " : ";
+ std::vector< Node > bound_loc;
+ bound_loc.insert( bound_loc.end(), d_references[s_atom][j].begin(), d_references[s_atom][j].end() );
+/* //this is unsound
+ for( int k=0; k<ccard; k++ ){
+ Assert( rb_start<(int)d_lbl_reference_bound[s_lbl].size() );
+ d_lbl_reference_bound[c_lbl].push_back( d_lbl_reference_bound[s_lbl][rb_start] );
+ Trace("sep-bound") << d_lbl_reference_bound[s_lbl][rb_start] << " ";
+ bound_loc.push_back( d_lbl_reference_bound[s_lbl][rb_start] );
+ rb_start++;
+ }
+*/
+ //carry all locations for now
+ bound_loc.insert( bound_loc.end(), d_lbl_reference_bound[s_lbl].begin(), d_lbl_reference_bound[s_lbl].end() );
+ Trace("sep-bound") << std::endl;
+ Node bound_v = mkUnion( tn, bound_loc );
+ Trace("sep-bound") << " ...bound value : " << bound_v << std::endl;
+ children.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, c_lbl, bound_v ) );
+ }
+ Trace("sep-bound") << "Done propagate Bound(" << s_lbl << ")" << std::endl;
+ }
+ std::vector< Node > labels;
+ getLabelChildren( s_atom, s_lbl, children, labels );
+ Node empSet = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType()));
+ 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 );
+ }
+ //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 );
+ }
+ 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{
+ //labeled emp should be rewritten
+ Assert( false );
+ }
+ d_red_conc[s_lbl][s_atom] = conc;
+ }else{
+ conc = its->second;
+ }
+ 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 lit = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+ lit = getValuation().ensureLiteral( lit );
+ 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_out->requirePhase( lit, true );
+ d_neg_guards.push_back( lit );
+ d_guard_to_assertion[lit] = s_atom;
+ //Node lem = NodeManager::currentNM()->mkNode( kind::IFF, 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 ant = atom;
+ if( polarity ){
+ ant = atom.negate();
+ }
+ Node lem = NodeManager::currentNM()->mkNode( kind::OR, ant, 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;
+ }
+ }
+ }
+ //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] );
+ 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;
+ }
+ //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 );
+ }
+ }
+ }
+
+ 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;
+ 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;
+ d_tmodel[v] = t;
+ }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-inst") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl;
+ d_pto_model[vv] = s_atom[1];
+ }
+ }
+ }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;
+ }
+ }
+ }
+ }
+ //(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() != 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, d_tmodel );
+ }
+ }
+ //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") << "---" << 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-eqc") << " } " << std::endl;
+ ++eqcs2_i;
+ }
+ Trace("sep-eqc") << std::endl;
+ }
+
+ 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];
+ if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){
+ Trace("sep-process-debug") << "Active lbl : " << s_lbl << std::endl;
+ active_lbl[s_lbl] = true;
+ }
+ }
+ }
+ }
+ }
+
+ //process spatial assertions
+ bool addedLemma = false;
+ bool needAddLemma = false;
+ 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;
+ Trace("sep-process-debug") << " check atom : " << s_atom << " use polarity " << use_polarity << std::endl;
+ 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( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){
+ needAddLemma = true;
+ int card;
+ TypeNode tn = getReferenceType( s_atom, card );
+ 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( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){
+ Node sub_lbl = itl->second;
+ int sub_index = itl->first;
+ computeLabelModel( sub_lbl, d_tmodel );
+ 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;
+ if( options::sepExp() ){
+ //old refinement lemmas
+ for( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){
+ int sub_index = itl->first;
+ std::map< Node, Node > visited;
+ Node c = applyLabel( s_atom[itl->first], mvals[sub_index], visited );
+ Trace("sep-process-debug") << " applied inst : " << c << std::endl;
+ if( s_atom.getKind()==kind::SEP_STAR || sub_index==0 ){
+ conc.push_back( c.negate() );
+ }else{
+ conc.push_back( c );
+ }
+ }
+ }else{
+ //new refinement
+ std::map< Node, Node > visited;
+ Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, d_tmodel, 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{
+ Trace("sep-process") << "*** repeated refinement lemma : " << lem << std::endl;
+ }
+ }
+ }else{
+ Trace("sep-process-debug") << " no children." << std::endl;
+ Assert( s_atom.getKind()==kind::SEP_PTO );
+ }
+ }else{
+ Trace("sep-process-debug") << "--> inactive negated assertion " << s_atom << std::endl;
+ }
+ }
+ }
+ if( !addedLemma ){
+ if( needAddLemma ){
+ Trace("sep-process") << "WARNING : could not find refinement lemma!!!" << std::endl;
+ Assert( false );
+ d_out->setIncomplete();
+ }
+ }
+ }
+ }
+ Trace("sep-check") << "Sep::check(): " << e << " done, conflict=" << d_conflict.get() << endl;
+}
+
+
+Node TheorySep::getNextDecisionRequest() {
+ for( unsigned i=0; i<d_neg_guards.size(); i++ ){
+ Node g = d_neg_guards[i];
+ bool success = true;
+ if( getLogicInfo().isQuantified() ){
+ Assert( d_guard_to_assertion.find( g )!= d_guard_to_assertion.end() );
+ Node a = d_guard_to_assertion[g];
+ Node q = quantifiers::TermDb::getInstConstAttr( a );
+ if( !q.isNull() ){
+ //must wait to decide on counterexample literal from quantified formula
+ Node cel = getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q );
+ bool value;
+ if( d_valuation.hasSatValue( cel, value ) ){
+ success = value;
+ }else{
+ Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g << " until " << cel << " is set " << std::endl;
+ success = false;
+ }
+ }
+ }
+ if( success ){
+ bool value;
+ if( !d_valuation.hasSatValue( g, value ) ) {
+ Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g << " (" << i << "/" << d_neg_guards.size() << ")" << std::endl;
+ return g;
+ }
+ }
+ }
+ Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : null" << std::endl;
+ return Node::null();
+}
+
+void TheorySep::conflict(TNode a, TNode b) {
+ Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
+ Node conflictNode;
+ if (a.getKind() == kind::CONST_BOOLEAN) {
+ conflictNode = explain(a.iffNode(b));
+ } else {
+ conflictNode = explain(a.eqNode(b));
+ }
+ d_conflict = true;
+ d_out->conflict( conflictNode );
+}
+
+
+TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context* c ) : d_pto(c), d_has_neg_pto(c,false) {
+
+}
+
+TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) {
+ std::map< Node, HeapAssertInfo* >::iterator e_i = d_eqc_info.find( n );
+ if( e_i==d_eqc_info.end() ){
+ if( doMake ){
+ HeapAssertInfo* ei = new HeapAssertInfo( getSatContext() );
+ d_eqc_info[n] = ei;
+ return ei;
+ }else{
+ return NULL;
+ }
+ }else{
+ return (*e_i).second;
+ }
+}
+
+TypeNode TheorySep::getReferenceType( Node atom, int& card, int index ) {
+ Trace("sep-type") << "getReference type " << atom << " " << index << std::endl;
+ Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::EMP_STAR || index!=-1 );
+ std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index );
+ if( it==d_reference_type[atom].end() ){
+ card = 0;
+ TypeNode tn;
+ if( index==-1 && ( atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND ) ){
+ for( unsigned i=0; i<atom.getNumChildren(); i++ ){
+ int cardc = 0;
+ TypeNode ctn = getReferenceType( atom, cardc, i );
+ if( !ctn.isNull() ){
+ tn = ctn;
+ }
+ for( unsigned j=0; j<d_references[atom][i].size(); j++ ){
+ if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), d_references[atom][i][j] )==d_references[atom][index].end() ){
+ d_references[atom][index].push_back( d_references[atom][i][j] );
+ }
+ }
+ card = card + cardc;
+ }
+ }else{
+ Node n = index==-1 ? atom : atom[index];
+ //will compute d_references as well
+ std::map< Node, int > visited;
+ tn = getReferenceType2( atom, card, index, n, visited );
+ }
+ if( tn.isNull() && index==-1 ){
+ tn = NodeManager::currentNM()->booleanType();
+ }
+ d_reference_type[atom][index] = tn;
+ d_reference_type_card[atom][index] = card;
+ Trace("sep-type") << "...ref type return " << card << " for " << atom << " " << index << std::endl;
+ //add to d_type_references
+ if( index==-1 ){
+ //only contributes if top-level (index=-1)
+ for( unsigned i=0; i<d_references[atom][index].size(); i++ ){
+ Assert( !d_references[atom][index][i].isNull() );
+ if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), d_references[atom][index][i] )==d_type_references[tn].end() ){
+ d_type_references[tn].push_back( d_references[atom][index][i] );
+ }
+ }
+ // update maximum cardinality value
+ if( card>(int)d_card_max[tn] ){
+ d_card_max[tn] = card;
+ }
+ }
+ return tn;
+ }else{
+ Assert( d_reference_type_card[atom].find( index )!=d_reference_type_card[atom].end() );
+ card = d_reference_type_card[atom][index];
+ return it->second;
+ }
+}
+
+TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited ) {
+ if( visited.find( n )==visited.end() ){
+ Trace("sep-type-debug") << "visit : " << n << " : " << atom << " " << index << std::endl;
+ visited[n] = -1;
+ if( n.getKind()==kind::SEP_PTO ){
+ TypeNode tn1 = n[0].getType();
+ TypeNode tn2 = n[1].getType();
+ if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){
+ d_reference_bound_invalid[tn1] = true;
+ }else{
+ if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), n[0] )==d_references[atom][index].end() ){
+ d_references[atom][index].push_back( n[0] );
+ }
+ }
+ std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 );
+ if( itt==d_loc_to_data_type.end() ){
+ Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
+ d_loc_to_data_type[tn1] = tn2;
+ }else{
+ if( itt->second!=tn2 ){
+ std::stringstream ss;
+ ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl;
+ throw LogicException(ss.str());
+ Assert( false );
+ }
+ }
+ card = 1;
+ visited[n] = card;
+ return tn1;
+ //return n[1].getType();
+ }else if( n.getKind()==kind::EMP_STAR ){
+ card = 1;
+ visited[n] = card;
+ return n[0].getType();
+ }else if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){
+ Assert( n!=atom );
+ //get the references
+ card = 0;
+ TypeNode tn = getReferenceType( n, card );
+ for( unsigned j=0; j<d_references[n][-1].size(); j++ ){
+ if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), d_references[n][-1][j] )==d_references[atom][index].end() ){
+ d_references[atom][index].push_back( d_references[n][-1][j] );
+ }
+ }
+ visited[n] = card;
+ return tn;
+ }else{
+ card = 0;
+ TypeNode otn;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ int cardc = 0;
+ TypeNode tn = getReferenceType2( atom, cardc, index, n[i], visited );
+ if( !tn.isNull() ){
+ otn = tn;
+ }
+ card = cardc>card ? cardc : card;
+ }
+ visited[n] = card;
+ return otn;
+ }
+ }else{
+ Trace("sep-type-debug") << "already visit : " << n << " : " << atom << " " << index << std::endl;
+ card = 0;
+ return TypeNode::null();
+ }
+}
+/*
+
+int TheorySep::getCardinality( Node n, std::vector< Node >& refs ) {
+ std::map< Node, int > visited;
+ return getCardinality2( n, refs, visited );
+}
+
+int TheorySep::getCardinality2( Node n, std::vector< Node >& refs, std::map< Node, int >& visited ) {
+ std::map< Node, int >::iterator it = visited.find( n );
+ if( it!=visited.end() ){
+ return it->second;
+ }else{
+
+
+ }
+}
+*/
+
+Node TheorySep::getBaseLabel( TypeNode tn ) {
+ std::map< TypeNode, Node >::iterator it = d_base_label.find( tn );
+ if( it==d_base_label.end() ){
+ Trace("sep") << "Make base label for " << tn << std::endl;
+ std::stringstream ss;
+ ss << "__Lb";
+ TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
+ //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
+ Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" );
+ d_base_label[tn] = n_lbl;
+ //make reference bound
+ Trace("sep") << "Make reference bound label for " << tn << std::endl;
+ std::stringstream ss2;
+ ss2 << "__Lu";
+ d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" );
+ d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() );
+ //add a reference type for maximum occurrences of empty in a constraint
+ unsigned n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()];
+ for( unsigned r=0; r<n_emp; r++ ){
+ Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
+ //d_type_references_all[tn].push_back( NodeManager::currentNM()->mkSkolem( "e", NodeManager::currentNM()->mkRefType(tn) ) );
+ if( options::sepDisequalC() ){
+ //ensure that it is distinct from all other references so far
+ for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
+ Node eq = NodeManager::currentNM()->mkNode( e.getType().isBoolean() ? kind::IFF : kind::EQUAL, e, d_type_references_all[tn][j] );
+ d_out->lemma( eq.negate() );
+ }
+ }
+ d_type_references_all[tn].push_back( e );
+ d_lbl_reference_bound[d_base_label[tn]].push_back( e );
+ }
+ //construct bound
+ d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
+ Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
+
+ if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
+ Node slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_reference_bound[tn], d_reference_bound_max[tn] );
+ Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl;
+ d_out->lemma( slem );
+ }else{
+ Trace("sep-bound") << "reference cannot be bound (possibly due to quantified pto)." << std::endl;
+ }
+ //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
+ //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
+ //d_out->lemma( slem );
+ return n_lbl;
+ }else{
+ return it->second;
+ }
+}
+
+Node TheorySep::getNilRef( TypeNode tn ) {
+ std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn );
+ if( it==d_nil_ref.end() ){
+ TypeEnumerator te(tn);
+ Node nil = NodeManager::currentNM()->mkNode( kind::SEP_NIL, *te );
+ d_nil_ref[tn] = nil;
+ return nil;
+ }else{
+ return it->second;
+ }
+}
+
+Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) {
+ Node u;
+ if( locs.empty() ){
+ TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
+ return NodeManager::currentNM()->mkConst(EmptySet(ltn.toType()));
+ }else{
+ for( unsigned i=0; i<locs.size(); i++ ){
+ Node s = locs[i];
+ Assert( !s.isNull() );
+ s = NodeManager::currentNM()->mkNode( kind::SINGLETON, s );
+ if( u.isNull() ){
+ u = s;
+ }else{
+ u = NodeManager::currentNM()->mkNode( kind::UNION, s, u );
+ }
+ }
+ return u;
+ }
+}
+
+Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
+ std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child );
+ if( it==d_label_map[atom][lbl].end() ){
+ int card;
+ TypeNode refType = getReferenceType( atom, card );
+ std::stringstream ss;
+ ss << "__Lc" << child;
+ TypeNode ltn = NodeManager::currentNM()->mkSetType(refType);
+ //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType));
+ Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" );
+ d_label_map[atom][lbl][child] = n_lbl;
+ d_label_map_parent[n_lbl] = lbl;
+ return n_lbl;
+ }else{
+ return (*it).second;
+ }
+}
+
+Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) {
+ Assert( n.getKind()!=kind::SEP_LABEL );
+ if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){
+ return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl );
+ }else if( !n.getType().isBoolean() || n.getNumChildren()==0 ){
+ return n;
+ }else{
+ std::map< Node, Node >::iterator it = visited.find( n );
+ if( it==visited.end() ){
+ std::vector< Node > children;
+ if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ children.push_back( n.getOperator() );
+ }
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node aln = applyLabel( n[i], lbl, visited );
+ children.push_back( aln );
+ childChanged = childChanged || aln!=n[i];
+ }
+ Node ret = n;
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ visited[n] = ret;
+ return ret;
+ }else{
+ return it->second;
+ }
+ }
+}
+
+Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, std::map< Node, Node >& tmodel,
+ TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) {
+ Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl;
+ if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){
+ Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl;
+ return Node::null();
+ }else{
+ if( Trace.isOn("sep-inst") ){
+ if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){
+ for( unsigned j=0; j<ind; j++ ){ Trace("sep-inst") << " "; }
+ Trace("sep-inst") << n << "[" << lbl << "] :: " << lbl_v << std::endl;
+ }
+ }
+ Assert( n.getKind()!=kind::SEP_LABEL );
+ if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){
+ if( lbl==o_lbl ){
+ std::vector< Node > children;
+ children.resize( n.getNumChildren() );
+ Assert( d_label_map[n].find( lbl )!=d_label_map[n].end() );
+ for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
+ Node sub_lbl = itl->second;
+ int sub_index = itl->first;
+ Assert( sub_index>=0 && sub_index<(int)children.size() );
+ Trace("sep-inst-debug") << "Sublabel " << sub_index << " is " << sub_lbl << std::endl;
+ Node lbl_mval;
+ if( n.getKind()==kind::SEP_WAND && sub_index==1 ){
+ Assert( d_label_map[n][lbl].find( 0 )!=d_label_map[n][lbl].end() );
+ Node sub_lbl_0 = d_label_map[n][lbl][0];
+ computeLabelModel( sub_lbl_0, tmodel );
+ Assert( d_label_model.find( sub_lbl_0 )!=d_label_model.end() );
+ lbl_mval = NodeManager::currentNM()->mkNode( kind::UNION, lbl, d_label_model[sub_lbl_0].getValue( rtn ) );
+ }else{
+ computeLabelModel( sub_lbl, tmodel );
+ Assert( d_label_model.find( sub_lbl )!=d_label_model.end() );
+ lbl_mval = d_label_model[sub_lbl].getValue( rtn );
+ }
+ Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval << std::endl;
+ children[sub_index] = instantiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, tmodel, rtn, active_lbl, ind+1 );
+ if( children[sub_index].isNull() ){
+ return Node::null();
+ }
+ }
+ if( n.getKind()==kind::SEP_STAR ){
+ Assert( children.size()>1 );
+ return NodeManager::currentNM()->mkNode( kind::AND, children );
+ }else{
+ return NodeManager::currentNM()->mkNode( kind::OR, children[0].negate(), children[1] );
+ }
+ }else{
+ //nested star/wand, label it and return
+ return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl_v );
+ }
+ }else if( n.getKind()==kind::SEP_PTO ){
+ //check if this pto reference is in the base label, if not, then it does not need to be added as an assumption
+ Assert( d_label_model.find( o_lbl )!=d_label_model.end() );
+ Node vr = d_valuation.getModel()->getRepresentative( n[0] );
+ Node svr = NodeManager::currentNM()->mkNode( kind::SINGLETON, vr );
+ bool inBaseHeap = std::find( d_label_model[o_lbl].d_heap_locs_model.begin(), d_label_model[o_lbl].d_heap_locs_model.end(), svr )!=d_label_model[o_lbl].d_heap_locs_model.end();
+ Trace("sep-inst-debug") << "Is in base (non-instantiating) heap : " << inBaseHeap << " for value ref " << vr << " in " << o_lbl << std::endl;
+ std::vector< Node > children;
+ if( inBaseHeap ){
+ Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] );
+ children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, n[0], n[1] ), s ) );
+ }else{
+ //look up value of data
+ std::map< Node, Node >::iterator it = pto_model.find( vr );
+ if( it!=pto_model.end() ){
+ if( n[1]!=it->second ){
+ children.push_back( NodeManager::currentNM()->mkNode( n[1].getType().isBoolean() ? kind::IFF : kind::EQUAL, n[1], it->second ) );
+ }
+ }else{
+ Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl;
+ }
+ }
+ children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] ), lbl_v ) );
+ Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) );
+ Trace("sep-inst-debug") << "Return " << ret << std::endl;
+ return ret;
+ }else if( n.getKind()==kind::EMP_STAR ){
+ //return NodeManager::currentNM()->mkConst( lbl_v.getKind()==kind::EMPTYSET );
+ return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType().toType())) );
+ }else{
+ std::map< Node, Node >::iterator it = visited.find( n );
+ if( it==visited.end() ){
+ std::vector< Node > children;
+ if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ children.push_back( n.getOperator() );
+ }
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node aln = instantiateLabel( n[i], o_lbl, lbl, lbl_v, visited, pto_model, tmodel, rtn, active_lbl, ind );
+ if( aln.isNull() ){
+ return Node::null();
+ }else{
+ children.push_back( aln );
+ childChanged = childChanged || aln!=n[i];
+ }
+ }
+ Node ret = n;
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ //careful about caching
+ //visited[n] = ret;
+ return ret;
+ }else{
+ return it->second;
+ }
+ }
+ }
+}
+
+void TheorySep::setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ) {
+ Trace("sep-process-debug") << "setInactiveAssertionRec::inactive : " << fact << std::endl;
+ 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 );
+ 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 );
+ Assert( !lblc.isNull() );
+ std::map< Node, Node > visited;
+ Node lc = applyLabel( s_atom[i], lblc, visited );
+ Assert( !lc.isNull() );
+ if( i==1 && s_atom.getKind()==kind::SEP_WAND ){
+ lc = lc.negate();
+ }
+ children.push_back( lc );
+ labels.push_back( lblc );
+ }
+ Assert( children.size()>1 );
+}
+
+void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) {
+ if( !d_label_model[lbl].d_computed ){
+ d_label_model[lbl].d_computed = true;
+
+ //Node v_val = d_valuation.getModelValue( s_lbl );
+ //hack FIXME
+ Node v_val = d_valuation.getModel()->getRepresentative( lbl );
+ Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl;
+ if( v_val.getKind()!=kind::EMPTYSET ){
+ while( v_val.getKind()==kind::UNION ){
+ Assert( v_val[1].getKind()==kind::SINGLETON );
+ d_label_model[lbl].d_heap_locs_model.push_back( v_val[1] );
+ v_val = v_val[0];
+ }
+ Assert( v_val.getKind()==kind::SINGLETON );
+ d_label_model[lbl].d_heap_locs_model.push_back( v_val );
+ }
+ //end hack
+ for( unsigned j=0; j<d_label_model[lbl].d_heap_locs_model.size(); j++ ){
+ Node u = d_label_model[lbl].d_heap_locs_model[j];
+ Assert( u.getKind()==kind::SINGLETON );
+ u = u[0];
+ Node tt;
+ std::map< Node, Node >::iterator itm = tmodel.find( u );
+ if( itm==tmodel.end() ) {
+ //Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << std::endl;
+ //Assert( false );
+ //tt = u;
+ //TypeNode tn = u.getType().getRefConstituentType();
+ TypeNode tn = u.getType();
+ Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << ", cref type " << tn << std::endl;
+ Assert( d_type_references_all.find( tn )!=d_type_references_all.end() && !d_type_references_all[tn].empty() );
+ tt = d_type_references_all[tn][0];
+ }else{
+ tt = itm->second;
+ }
+ Node stt = NodeManager::currentNM()->mkNode( kind::SINGLETON, tt );
+ Trace("sep-process-debug") << "...model : add " << tt << " for " << u << " in lbl " << lbl << std::endl;
+ d_label_model[lbl].d_heap_locs.push_back( stt );
+ }
+ }
+}
+
+Node TheorySep::getRepresentative( Node t ) {
+ if( d_equalityEngine.hasTerm( t ) ){
+ return d_equalityEngine.getRepresentative( t );
+ }else{
+ return t;
+ }
+}
+
+bool TheorySep::hasTerm( Node a ){
+ return d_equalityEngine.hasTerm( a );
+}
+
+bool TheorySep::areEqual( Node a, Node b ){
+ if( a==b ){
+ return true;
+ }else if( hasTerm( a ) && hasTerm( b ) ){
+ return d_equalityEngine.areEqual( a, b );
+ }else{
+ return false;
+ }
+}
+
+bool TheorySep::areDisequal( Node a, Node b ){
+ if( a==b ){
+ return false;
+ }else if( hasTerm( a ) && hasTerm( b ) ){
+ if( d_equalityEngine.areDisequal( a, b, false ) ){
+ return true;
+ }
+ }
+ return false;
+}
+
+void TheorySep::eqNotifyPreMerge(TNode t1, TNode t2) {
+
+}
+
+void TheorySep::eqNotifyPostMerge(TNode t1, TNode t2) {
+ HeapAssertInfo * e2 = getOrMakeEqcInfo( t2, false );
+ if( e2 && ( !e2->d_pto.get().isNull() || e2->d_has_neg_pto.get() ) ){
+ HeapAssertInfo * e1 = getOrMakeEqcInfo( t1, true );
+ if( !e2->d_pto.get().isNull() ){
+ if( !e1->d_pto.get().isNull() ){
+ Trace("sep-pto-debug") << "While merging " << t1 << " " << t2 << ", merge pto." << std::endl;
+ mergePto( e1->d_pto.get(), e2->d_pto.get() );
+ }else{
+ e1->d_pto.set( e2->d_pto.get() );
+ }
+ }
+ e1->d_has_neg_pto.set( e1->d_has_neg_pto.get() || e2->d_has_neg_pto.get() );
+ //validate
+ validatePto( e1, t1 );
+ }
+}
+
+void TheorySep::validatePto( HeapAssertInfo * ei, Node ei_n ) {
+ if( !ei->d_pto.get().isNull() && ei->d_has_neg_pto.get() ){
+ for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
+ Node fact = (*i);
+ bool polarity = fact.getKind() != kind::NOT;
+ if( !polarity ){
+ TNode atom = polarity ? fact : fact[0];
+ Assert( atom.getKind()==kind::SEP_LABEL );
+ TNode s_atom = atom[0];
+ if( s_atom.getKind()==kind::SEP_PTO ){
+ if( areEqual( atom[1], ei_n ) ){
+ addPto( ei, ei_n, atom, false );
+ }
+ }
+ }
+ }
+ //we have now processed all pending negated pto
+ ei->d_has_neg_pto.set( false );
+ }
+}
+
+void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ) {
+ Trace("sep-pto") << "Add pto " << p << ", pol = " << polarity << " to eqc " << ei_n << std::endl;
+ if( !ei->d_pto.get().isNull() ){
+ if( polarity ){
+ Trace("sep-pto-debug") << "...eqc " << ei_n << " already has pto " << ei->d_pto.get() << ", merge." << std::endl;
+ mergePto( ei->d_pto.get(), p );
+ }else{
+ Node pb = ei->d_pto.get();
+ Trace("sep-pto") << "Process positive/negated pto " << " " << pb << " " << p << std::endl;
+ Assert( pb.getKind()==kind::SEP_LABEL && pb[0].getKind()==kind::SEP_PTO );
+ Assert( p.getKind()==kind::SEP_LABEL && p[0].getKind()==kind::SEP_PTO );
+ Assert( areEqual( pb[1], p[1] ) );
+ std::vector< Node > exp;
+ if( pb[1]!=p[1] ){
+ exp.push_back( pb[1].eqNode( p[1] ) );
+ }
+ exp.push_back( pb );
+ exp.push_back( p.negate() );
+ std::vector< Node > conc;
+ if( pb[0][1]!=p[0][1] ){
+ conc.push_back( pb[0][1].eqNode( p[0][1] ).negate() );
+ }
+ if( pb[1]!=p[1] ){
+ 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 ) );
+ sendLemma( exp, n_conc, "PTO_NEG_PROP" );
+ }
+ }else{
+ if( polarity ){
+ ei->d_pto.set( p );
+ validatePto( ei, ei_n );
+ }else{
+ ei->d_has_neg_pto.set( true );
+ }
+ }
+}
+
+void TheorySep::mergePto( Node p1, Node p2 ) {
+ Trace("sep-lemma-debug") << "Merge pto " << p1 << " " << p2 << std::endl;
+ Assert( p1.getKind()==kind::SEP_LABEL && p1[0].getKind()==kind::SEP_PTO );
+ Assert( p2.getKind()==kind::SEP_LABEL && p2[0].getKind()==kind::SEP_PTO );
+ if( !areEqual( p1[0][1], p2[0][1] ) ){
+ std::vector< Node > exp;
+ if( p1[1]!=p2[1] ){
+ Assert( areEqual( p1[1], p2[1] ) );
+ exp.push_back( p1[1].eqNode( p2[1] ) );
+ }
+ exp.push_back( p1 );
+ exp.push_back( p2 );
+ sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" );
+ }
+}
+
+void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer ) {
+ Trace("sep-lemma-debug") << "Do rewrite on inference : " << conc << std::endl;
+ conc = Rewriter::rewrite( conc );
+ Trace("sep-lemma-debug") << "Got : " << conc << std::endl;
+ if( conc!=d_true ){
+ if( infer && conc!=d_false ){
+ Node ant_n;
+ if( ant.empty() ){
+ ant_n = d_true;
+ }else if( ant.size()==1 ){
+ ant_n = ant[0];
+ }else{
+ ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant );
+ }
+ Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << c << std::endl;
+ d_pending_exp.push_back( ant_n );
+ d_pending.push_back( conc );
+ d_infer.push_back( ant_n );
+ d_infer_exp.push_back( conc );
+ }else{
+ std::vector< TNode > ant_e;
+ for( unsigned i=0; i<ant.size(); i++ ){
+ Trace("sep-lemma-debug") << "Explain : " << ant[i] << std::endl;
+ explain( ant[i], ant_e );
+ }
+ Node ant_n;
+ if( ant_e.empty() ){
+ ant_n = d_true;
+ }else if( ant_e.size()==1 ){
+ ant_n = ant_e[0];
+ }else{
+ ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant_e );
+ }
+ if( conc==d_false ){
+ Trace("sep-lemma") << "Sep::Conflict: " << ant_n << " by " << c << std::endl;
+ d_out->conflict( ant_n );
+ d_conflict = true;
+ }else{
+ Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant_n << " by " << c << std::endl;
+ d_pending_exp.push_back( ant_n );
+ d_pending.push_back( conc );
+ d_pending_lem.push_back( d_pending.size()-1 );
+ }
+ }
+ }
+}
+
+void TheorySep::doPendingFacts() {
+ if( d_pending_lem.empty() ){
+ for( unsigned i=0; i<d_pending.size(); i++ ){
+ if( d_conflict ){
+ break;
+ }
+ Node atom = d_pending[i].getKind()==kind::NOT ? d_pending[i][0] : d_pending[i];
+ bool pol = d_pending[i].getKind()!=kind::NOT;
+ Trace("sep-pending") << "Sep : Assert to EE : " << atom << ", pol = " << pol << std::endl;
+ if( atom.getKind()==kind::EQUAL ){
+ d_equalityEngine.assertEquality(atom, pol, d_pending_exp[i]);
+ }else{
+ d_equalityEngine.assertPredicate(atom, pol, d_pending_exp[i]);
+ }
+ }
+ }else{
+ for( unsigned i=0; i<d_pending_lem.size(); i++ ){
+ if( d_conflict ){
+ break;
+ }
+ int index = d_pending_lem[i];
+ Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, d_pending_exp[index], d_pending[index] );
+ d_out->lemma( lem );
+ Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl;
+ }
+ }
+ d_pending_exp.clear();
+ d_pending.clear();
+ d_pending_lem.clear();
+}
+
+void TheorySep::debugPrintHeap( HeapInfo& heap, const char * c ) {
+ Trace(c) << "[" << std::endl;
+ Trace(c) << " ";
+ for( unsigned j=0; j<heap.d_heap_locs.size(); j++ ){
+ Trace(c) << heap.d_heap_locs[j] << " ";
+ }
+ Trace(c) << std::endl;
+ Trace(c) << "]" << std::endl;
+}
+
+Node TheorySep::HeapInfo::getValue( TypeNode tn ) {
+ Assert( d_heap_locs.size()==d_heap_locs_model.size() );
+ if( d_heap_locs.empty() ){
+ return NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
+ }else if( d_heap_locs.size()==1 ){
+ return d_heap_locs[0];
+ }else{
+ Node curr = NodeManager::currentNM()->mkNode( kind::UNION, d_heap_locs[0], d_heap_locs[1] );
+ for( unsigned j=2; j<d_heap_locs.size(); j++ ){
+ curr = NodeManager::currentNM()->mkNode( kind::UNION, curr, d_heap_locs[j] );
+ }
+ return curr;
+ }
+}
+
+}/* CVC4::theory::sep namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file theory_sep.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Dejan Jovanovic, Clark Barrett
+ ** Minor contributors (to current version): Tim King, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Theory of sep
+ **
+ ** Theory of sep.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SEP__THEORY_SEP_H
+#define __CVC4__THEORY__SEP__THEORY_SEP_H
+
+#include "theory/theory.h"
+#include "util/statistics_registry.h"
+#include "theory/uf/equality_engine.h"
+#include "context/cdchunk_list.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
+
+namespace CVC4 {
+namespace theory {
+
+class TheoryModel;
+
+namespace sep {
+
+class TheorySep : public Theory {
+ typedef context::CDChunkList<Node> NodeList;
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+
+ /////////////////////////////////////////////////////////////////////////////
+ // MISC
+ /////////////////////////////////////////////////////////////////////////////
+
+ private:
+
+ /** True node for predicates = true */
+ Node d_true;
+
+ /** True node for predicates = false */
+ Node d_false;
+
+ Node mkAnd( std::vector< TNode >& assumptions );
+
+ void processAssertion( Node n, std::map< Node, bool >& visited );
+
+ public:
+
+ TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ ~TheorySep();
+
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
+ std::string identify() const { return std::string("TheorySep"); }
+
+ /////////////////////////////////////////////////////////////////////////////
+ // PREPROCESSING
+ /////////////////////////////////////////////////////////////////////////////
+
+ public:
+
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ Node ppRewrite(TNode atom);
+
+ void processAssertions( std::vector< Node >& assertions );
+ /////////////////////////////////////////////////////////////////////////////
+ // T-PROPAGATION / REGISTRATION
+ /////////////////////////////////////////////////////////////////////////////
+
+ private:
+
+ /** Should be called to propagate the literal. */
+ bool propagate(TNode literal);
+
+ /** Explain why this literal is true by adding assumptions */
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+
+ public:
+
+ void preRegisterTerm(TNode n);
+ void propagate(Effort e);
+ Node explain(TNode n);
+
+ public:
+
+ void addSharedTerm(TNode t);
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+ void computeCareGraph();
+
+ /////////////////////////////////////////////////////////////////////////////
+ // MODEL GENERATION
+ /////////////////////////////////////////////////////////////////////////////
+
+ public:
+
+ void collectModelInfo(TheoryModel* m, bool fullModel);
+
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
+
+ private:
+ public:
+
+ Node getNextDecisionRequest();
+
+ void presolve();
+ void shutdown() { }
+
+ /////////////////////////////////////////////////////////////////////////////
+ // MAIN SOLVER
+ /////////////////////////////////////////////////////////////////////////////
+ public:
+
+ void check(Effort e);
+
+ private:
+
+ // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
+ class NotifyClass : public eq::EqualityEngineNotify {
+ TheorySep& d_sep;
+ public:
+ NotifyClass(TheorySep& sep): d_sep(sep) {}
+
+ bool eqNotifyTriggerEquality(TNode equality, bool value) {
+ Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
+ // Just forward to sep
+ if (value) {
+ return d_sep.propagate(equality);
+ } else {
+ return d_sep.propagate(equality.notNode());
+ }
+ }
+
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+ Unreachable();
+ }
+
+ bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+ Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
+ if (value) {
+ // Propagate equality between shared terms
+ return d_sep.propagate(t1.eqNode(t2));
+ } else {
+ return d_sep.propagate(t1.eqNode(t2).notNode());
+ }
+ return true;
+ }
+
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+ Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+ d_sep.conflict(t1, t2);
+ }
+
+ void eqNotifyNewClass(TNode t) { }
+ void eqNotifyPreMerge(TNode t1, TNode t2) { d_sep.eqNotifyPreMerge( t1, t2 ); }
+ void eqNotifyPostMerge(TNode t1, TNode t2) { d_sep.eqNotifyPostMerge( t1, t2 ); }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+ };
+
+ /** The notify class for d_equalityEngine */
+ NotifyClass d_notify;
+
+ /** Equaltity engine */
+ eq::EqualityEngine d_equalityEngine;
+
+ /** Are we in conflict? */
+ context::CDO<bool> d_conflict;
+ std::vector< Node > d_pending_exp;
+ std::vector< Node > d_pending;
+ std::vector< int > d_pending_lem;
+
+ /** list of all refinement lemms */
+ std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem;
+
+ /** Conflict when merging constants */
+ void conflict(TNode a, TNode b);
+
+ //cache for positive polarity start reduction
+ NodeSet d_reduce;
+ std::map< Node, std::map< Node, Node > > d_red_conc;
+ std::map< Node, std::map< Node, Node > > d_neg_guard;
+ std::vector< Node > d_neg_guards;
+ std::map< Node, Node > d_guard_to_assertion;
+ //cache for references
+ std::map< Node, std::map< int, TypeNode > > d_reference_type;
+ std::map< Node, std::map< int, int > > d_reference_type_card;
+ std::map< Node, std::map< int, std::vector< Node > > > d_references;
+ /** inferences: maintained to ensure ref count for internally introduced nodes */
+ NodeList d_infer;
+ NodeList d_infer_exp;
+ NodeList d_spatial_assertions;
+
+ //currently fix one data type for each location type, throw error if using more than one
+ std::map< TypeNode, TypeNode > d_loc_to_data_type;
+ //information about types
+ std::map< TypeNode, Node > d_base_label;
+ std::map< TypeNode, Node > d_nil_ref;
+ //reference bound
+ std::map< TypeNode, Node > d_reference_bound;
+ std::map< TypeNode, Node > d_reference_bound_max;
+ std::map< TypeNode, bool > d_reference_bound_invalid;
+ std::map< TypeNode, std::vector< Node > > d_type_references;
+ std::map< TypeNode, std::vector< Node > > d_type_references_all;
+ std::map< TypeNode, unsigned > d_card_max;
+ //bounds for labels
+ std::map< Node, std::vector< Node > > d_lbl_reference_bound;
+ //for empty argument
+ std::map< TypeNode, Node > d_emp_arg;
+ //map from ( atom, label, child index ) -> label
+ std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map;
+ std::map< Node, Node > d_label_map_parent;
+
+ //term model
+ std::map< Node, Node > d_tmodel;
+ std::map< Node, Node > d_pto_model;
+
+ class HeapAssertInfo {
+ public:
+ HeapAssertInfo( context::Context* c );
+ ~HeapAssertInfo(){}
+ context::CDO< Node > d_pto;
+ context::CDO< bool > d_has_neg_pto;
+ };
+ std::map< Node, HeapAssertInfo * > d_eqc_info;
+ HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
+
+ //calculate the element type of the heap for spatial assertions
+ TypeNode getReferenceType( Node atom, int& card, int index = -1 );
+ TypeNode getReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited);
+ //get the base label for the spatial assertion
+ Node getBaseLabel( TypeNode tn );
+ Node getNilRef( TypeNode tn );
+ Node getLabel( Node atom, int child, Node lbl );
+ Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited );
+ void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels );
+
+ class HeapInfo {
+ public:
+ HeapInfo() : d_computed(false) {}
+ //information about the model
+ bool d_computed;
+ std::vector< Node > d_heap_locs;
+ std::vector< Node > d_heap_locs_model;
+ //get value
+ Node getValue( TypeNode tn );
+ };
+ //heap info ( label -> HeapInfo )
+ std::map< Node, HeapInfo > d_label_model;
+
+ void debugPrintHeap( HeapInfo& heap, const char * c );
+ void validatePto( HeapAssertInfo * ei, Node ei_n );
+ void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
+ void mergePto( Node p1, Node p2 );
+ void computeLabelModel( Node lbl, std::map< Node, Node >& tmodel );
+ Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, std::map< Node, Node >& tmodel,
+ TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
+ void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
+
+ Node mkUnion( TypeNode tn, std::vector< Node >& locs );
+private:
+ Node getRepresentative( Node t );
+ bool hasTerm( Node a );
+ bool areEqual( Node a, Node b );
+ bool areDisequal( Node a, Node b );
+ /** called when two equivalence classes will merge */
+ void eqNotifyPreMerge(TNode t1, TNode t2);
+ void eqNotifyPostMerge(TNode t1, TNode t2);
+
+ void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
+ void doPendingFacts();
+public:
+ eq::EqualityEngine* getEqualityEngine() {
+ return &d_equalityEngine;
+ }
+
+};/* class TheorySep */
+
+}/* CVC4::theory::sep namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SEP__THEORY_SEP_H */
projects / cvc5.git / commitdiff