diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-21 08:12:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-21 13:12:11 +0000 |
commit | 09097cd3b9cd3233b938ace34f3513a16ac17f80 (patch) | |
tree | b889e15b487582e810db61b64dade7e6a14d225b /src/theory/sep | |
parent | 02dd48563db0c5effd608eda70d4c262309322a6 (diff) |
Clean up remaining raw uses of output channel (#6161)
After this PR, with only a few exceptions, all calls to output channel for lemmas, conflicts are made through inference manager.
This is work towards standardizing the statistics for theories.
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 47 |
1 files changed, 16 insertions, 31 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 47eac5359..52e89159b 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -128,19 +128,7 @@ Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) { bool TheorySep::propagateLit(TNode literal) { - Debug("sep") << "TheorySep::propagateLit(" << literal << ")" << std::endl; - // If already in conflict, no more propagation - 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_state.notifyInConflict(); - } - return ok; + return d_im.propagateLit(literal); } TrustNode TheorySep::explain(TNode literal) @@ -345,7 +333,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) } Trace("sep-lemma-debug") << "Sep::Lemma : base reduction : " << lem << std::endl; - d_out->lemma(lem); + d_im.lemma(lem, InferenceId::SEP_LABEL_INTRO); return; } Trace("sep-lemma-debug") << "Reducing assertion " << fact << std::endl; @@ -414,13 +402,13 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) Trace("sep-lemma") << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem << std::endl; - d_out->lemma(nrlem); + d_im.lemma(nrlem, InferenceId::SEP_NIL_NOT_IN_HEAP); } // 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); + d_im.lemma(clem, InferenceId::SEP_LABEL_DEF); } conc = nm->mkNode(AND, children); } @@ -454,7 +442,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) lem = nm->mkNode(OR, fact.negate(), econc); } Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl; - d_out->lemma(lem); + d_im.lemma(lem, InferenceId::SEP_EMP); } else { @@ -492,14 +480,14 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) // 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); + d_im.lemma(lem, InferenceId::SEP_NEG_REDUCTION); } 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); + d_im.lemma(lem, InferenceId::SEP_POS_REDUCTION); } } @@ -799,7 +787,7 @@ void TheorySep::postCheck(Effort level) << ") : " << lem << std::endl; Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " << lem << std::endl; - d_out->lemma(lem); + d_im.lemma(lem, InferenceId::SEP_REFINEMENT); addedLemma = true; } else @@ -868,7 +856,7 @@ void TheorySep::postCheck(Effort level) 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); + d_im.lemma(lem, InferenceId::SEP_WITNESS_FINITE_DATA); addedLemma = true; } else @@ -906,7 +894,7 @@ void TheorySep::postCheck(Effort level) if (needAddLemma) { - d_out->setIncomplete(); + d_im.setIncomplete(); } Trace("sep-check") << "Sep::check(): " << level << " done, conflict=" << d_state.isInConflict() @@ -1219,7 +1207,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { //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( kind::EQUAL, e, d_type_references_all[tn][j] ); - d_out->lemma( eq.negate() ); + d_im.lemma(eq.negate(), InferenceId::SEP_DISTINCT_REF); } d_type_references_all[tn].push_back( e ); } @@ -1237,11 +1225,8 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { Node slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] ); Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl; - d_out->lemma( slem ); - //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 ); - + d_im.lemma(slem, InferenceId::SEP_REF_BOUND); + //symmetry breaking if( d_type_references_card[tn].size()>1 ){ std::map< unsigned, Node > lit_mem_map; @@ -1257,7 +1242,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { Node sym_lem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ); sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, lit_mem_map[i].negate(), sym_lem ); Trace("sep-lemma") << "Sep::Lemma: symmetry breaking lemma : " << sym_lem << std::endl; - d_out->lemma( sym_lem ); + d_im.lemma(sym_lem, InferenceId::SEP_SYM_BREAK); } } } @@ -1267,8 +1252,8 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { Node nr = getNilRef( tn ); Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate(); Trace("sep-lemma") << "Sep::Lemma: sep.nil not in base label " << tn << " : " << nrlem << std::endl; - d_out->lemma( nrlem ); - + d_im.lemma(nrlem, InferenceId::SEP_NIL_NOT_IN_HEAP); + return n_lbl; }else{ return it->second; |