diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-03 15:09:12 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-03 15:09:26 -0500 |
commit | b6d5d0b11cf7624cd7a3e0a2f6f77d83d2f7001a (patch) | |
tree | b0e5acbce9023c28bf1bb85eee5da97b79c94561 /src/theory/sep | |
parent | 8a8455d955c084c9a9f7add1f4e4da6b1dbc35eb (diff) |
Add priorities to getNextDecision. Properly handle case for finite types + unbounded heaps in sep logic. Fix another simple memory leak in sygus.
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 42 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 2 |
2 files changed, 29 insertions, 15 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 426daf622..ea025e3a2 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -683,6 +683,7 @@ void TheorySep::check(Effort e) { }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{ @@ -700,6 +701,7 @@ void TheorySep::check(Effort e) { //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; @@ -708,18 +710,29 @@ void TheorySep::check(Effort e) { 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() ){ - Node ll = d_tmodel[l]; - Assert( !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; + 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; } @@ -727,7 +740,6 @@ void TheorySep::check(Effort e) { } } if( !addedLemma && needAddLemma ){ - Trace("sep-process") << "WARNING : could not find sep refinement lemma!!!" << std::endl; Assert( false ); d_out->setIncomplete(); } @@ -741,7 +753,7 @@ bool TheorySep::needsCheckLastEffort() { return hasFacts(); } -Node TheorySep::getNextDecisionRequest() { +Node TheorySep::getNextDecisionRequest( unsigned& priority ) { for( unsigned i=0; i<d_neg_guards.size(); i++ ){ Node g = d_neg_guards[i]; bool success = true; @@ -754,6 +766,7 @@ Node TheorySep::getNextDecisionRequest() { Node cel = getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q ); bool value; if( d_valuation.hasSatValue( cel, value ) ){ + Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : dependent guard " << g << " depends on value for guard for quantified formula : " << value << std::endl; success = value; }else{ Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g << " until " << cel << " is set " << std::endl; @@ -765,6 +778,7 @@ Node TheorySep::getNextDecisionRequest() { bool value; if( !d_valuation.hasSatValue( g, value ) ) { Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g << " (" << i << "/" << d_neg_guards.size() << ")" << std::endl; + priority = 0; return g; } } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index a3bb1bd7b..35b7fe5e9 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -118,7 +118,7 @@ class TheorySep : public Theory { private: public: - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); void presolve(); void shutdown() { } |