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.
* 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
{
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).
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);
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),
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; }
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<TNode> 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);
}
#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"
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.
Node abstractFloatToReal(Node);
private:
- context::CDO<Node> d_conflictNode;
ComparisonUFMap d_minMap;
ComparisonUFMap d_maxMap;
TheoryFpRewriter d_rewriter;
/** A (default) theory state object */
TheoryState d_state;
+ /** A (default) inference manager */
+ TheoryInferenceManager d_im;
}; /* class TheoryFp */
} // namespace fp
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";
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
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)
}
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;
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);
}
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
{
// 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);
}
}
<< ") : " << 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
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
if (needAddLemma)
{
- d_out->setIncomplete();
+ d_im.setIncomplete();
}
Trace("sep-check") << "Sep::check(): " << level
<< " done, conflict=" << d_state.isInConflict()
//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 );
}
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;
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);
}
}
}
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;
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
projects / cvc5.git / commitdiff