From 09097cd3b9cd3233b938ace34f3513a16ac17f80 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 21 Mar 2021 08:12:11 -0500 Subject: 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. --- src/theory/arith/nl/nonlinear_extension.h | 8 +++--- src/theory/datatypes/theory_datatypes.cpp | 2 +- src/theory/fp/theory_fp.cpp | 35 ++++++++--------------- src/theory/fp/theory_fp.h | 6 ++-- src/theory/inference_id.cpp | 11 ++++++++ src/theory/inference_id.h | 23 +++++++++++++++ src/theory/sep/theory_sep.cpp | 47 +++++++++++-------------------- src/theory/uf/theory_uf.cpp | 2 +- 8 files changed, 71 insertions(+), 63 deletions(-) diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 09e3a8370..820c317c5 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -74,9 +74,9 @@ class NlLemma; * which is called by TheoryArithPrivate either: * (1) at full effort with no conflicts or lemmas emitted, or * (2) at last call effort. - * In this method, this class calls d_out->lemma(...) + * In this method, this class calls d_im.lemma(...) * for valid arithmetic theory lemmas, based on the current set of assertions, - * where d_out is the output channel of TheoryArith. + * where d_im is the inference manager of TheoryArith. */ class NonlinearExtension { @@ -94,8 +94,8 @@ class NonlinearExtension void preRegisterTerm(TNode n); /** Check at effort level e. * - * This call may result in (possibly multiple) calls to d_out->lemma(...) - * where d_out is the output channel of TheoryArith. + * This call may result in (possibly multiple) calls to d_im.lemma(...) + * where d_im is the inference manager of TheoryArith. * * If e is FULL, then we add lemmas based on context-depedent * simplification (see Reynolds et al FroCoS 2017). diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 53680530d..7f57d5942 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -327,7 +327,7 @@ void TheoryDatatypes::postCheck(Effort level) nb << test << test.notNode(); Node lemma = nb; d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT); - d_out->requirePhase( test, true ); + d_im.requirePhase(test, true); }else{ Trace("dt-split") << "*************Split for constructors on " << n << endl; Node lemma = utils::mkSplit(n, dt); diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index d17e2999e..3099d9aab 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -114,7 +114,6 @@ TheoryFp::TheoryFp(context::Context* c, d_registeredTerms(u), d_conv(new FpConverter(u)), d_expansionRequested(false), - d_conflictNode(c, Node::null()), d_minMap(u), d_maxMap(u), d_toUBVMap(u), @@ -123,10 +122,12 @@ TheoryFp::TheoryFp(context::Context* c, d_realToFloatMap(u), d_floatToRealMap(u), d_abstractionMap(u), - d_state(c, u, valuation) + d_state(c, u, valuation), + d_im(*this, d_state, pnm, "theory::fp", false) { - // indicate we are using the default theory state object + // indicate we are using the default theory state and inference manager d_theoryState = &d_state; + d_inferManager = &d_im; } /* TheoryFp::TheoryFp() */ TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; } @@ -917,39 +918,25 @@ void TheoryFp::preRegisterTerm(TNode node) return; } -void TheoryFp::handleLemma(Node node) { +void TheoryFp::handleLemma(Node node, InferenceId id) +{ Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl; // will be preprocessed when sent, which is important because it contains // embedded ITEs - d_out->lemma(node); + d_im.lemma(node, id); } bool TheoryFp::propagateLit(TNode node) { Trace("fp") << "TheoryFp::propagateLit(): propagate " << node << std::endl; - - bool stat = d_out->propagate(node); - - if (!stat) - { - d_state.notifyInConflict(); - } - return stat; + return d_im.propagateLit(node); } void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2) { - std::vector assumptions; - d_equalityEngine->explainEquality(t1, t2, true, assumptions); - - Node conflict = helper::buildConjunct(assumptions); - Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected " - << conflict << std::endl; - - d_conflictNode = conflict; - d_state.notifyInConflict(); - d_out->conflict(conflict); - return; + Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected" + << std::endl; + d_im.conflictEqConstantMerge(t1, t2); } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 1660d5799..b15b5c2dd 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -27,6 +27,7 @@ #include "context/cdo.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/theory.h" +#include "theory/theory_inference_manager.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" @@ -142,7 +143,7 @@ class TheoryFp : public Theory void convertAndEquateTerm(TNode node); /** Interaction with the rest of the solver **/ - void handleLemma(Node node); + void handleLemma(Node node, InferenceId id = InferenceId::UNKNOWN); /** * Called when literal node is inferred by the equality engine. This * propagates node on the output channel. @@ -168,7 +169,6 @@ class TheoryFp : public Theory Node abstractFloatToReal(Node); private: - context::CDO d_conflictNode; ComparisonUFMap d_minMap; ComparisonUFMap d_maxMap; @@ -183,6 +183,8 @@ class TheoryFp : public Theory TheoryFpRewriter d_rewriter; /** A (default) theory state object */ TheoryState d_state; + /** A (default) inference manager */ + TheoryInferenceManager d_im; }; /* class TheoryFp */ } // namespace fp diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index e53ba35f8..c786117f3 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -174,6 +174,17 @@ const char* toString(InferenceId i) case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP"; case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP"; + case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO"; + case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF"; + case InferenceId::SEP_EMP: return "SEP_EMP"; + case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION"; + case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION"; + case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT"; + case InferenceId::SEP_NIL_NOT_IN_HEAP: return "SEP_NIL_NOT_IN_HEAP"; + case InferenceId::SEP_SYM_BREAK: return "SEP_SYM_BREAK"; + case InferenceId::SEP_WITNESS_FINITE_DATA: return "SEP_WITNESS_FINITE_DATA"; + case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF"; + case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND"; case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION"; case InferenceId::SETS_DEQ: return "SETS_DEQ"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 4af7761a0..380b5eca6 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -294,6 +294,29 @@ enum class InferenceId SEP_PTO_NEG_PROP, // enforces injectiveness of pto: (pto x y) ^ (pto y w) ^ x = y => y = w SEP_PTO_PROP, + // introduces a label for a heap, of the form U => L, where U is an + // unlabelled separation logic predicate and L is its labelled form + SEP_LABEL_INTRO, + // introduces the set constraints for a label + SEP_LABEL_DEF, + // lemma for sep.emp + SEP_EMP, + // positive reduction for sep constraint + SEP_POS_REDUCTION, + // negative reduction for sep constraint + SEP_NEG_REDUCTION, + // model-based refinement for negated star/wand + SEP_REFINEMENT, + // sep.nil is not in the heap + SEP_NIL_NOT_IN_HEAP, + // a symmetry breaking lemma + SEP_SYM_BREAK, + // finite witness data lemma + SEP_WITNESS_FINITE_DATA, + // element distinctness lemma + SEP_DISTINCT_REF, + // reference bound lemma + SEP_REF_BOUND, // ---------------------------------- end sep theory // ---------------------------------- sets theory 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; jmkNode( 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; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 32524b562..ac25ede14 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -181,7 +181,7 @@ bool TheoryUF::preNotifyFact( else { // support for cardinality constraints is not enabled, set incomplete - d_out->setIncomplete(); + d_im.setIncomplete(); } } // don't need to assert cardinality constraints if not producing models -- cgit v1.2.3