const LogicInfo& logicInfo,
ProofNodeManager* pnm)
: Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm),
- d_infer(c),
- d_infer_exp(c),
d_term_sk(u),
d_notify(*this),
d_labels(c),
d_selector_apps(c),
- d_conflict(c, false),
- d_addedLemma(false),
- d_addedFact(false),
d_collectTermsCache(c),
d_collectTermsCacheU(u),
d_functionTerms(c),
d_singleton_eq(u),
d_lemmas_produced_c(u),
d_sygusExtension(nullptr),
- d_state(c, u, valuation)
+ d_state(c, u, valuation),
+ d_im(*this, d_state, pnm)
{
d_true = NodeManager::currentNM()->mkConst( true );
// indicate we are using the default theory state object
d_theoryState = &d_state;
+ d_inferManager = &d_im;
}
TheoryDatatypes::~TheoryDatatypes() {
}
}
-void TheoryDatatypes::check(Effort e) {
- if (done() && e<EFFORT_FULL) {
- return;
- }
- Assert(d_pending.empty());
- d_addedLemma = false;
-
- if( e == EFFORT_LAST_CALL ){
+bool TheoryDatatypes::preCheck(Effort level)
+{
+ d_im.reset();
+ return false;
+}
+
+void TheoryDatatypes::postCheck(Effort level)
+{
+ if (level == EFFORT_LAST_CALL)
+ {
Assert(d_sygusExtension != nullptr);
- std::vector< Node > lemmas;
+ std::vector<Node> lemmas;
d_sygusExtension->check(lemmas);
- doSendLemmas( lemmas );
+ d_im.sendLemmas(lemmas);
return;
}
-
- TimerStat::CodeTimer checkTimer(d_checkTime);
-
- Trace("datatypes-check") << "Check effort " << e << std::endl;
- while(!done() && !d_conflict) {
- // Get all the assertions
- Assertion assertion = get();
- TNode fact = assertion.d_assertion;
- Trace("datatypes-assert") << "Assert " << fact << std::endl;
-
- TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact;
-
- // extra debug check to make sure that the rewriter did its job correctly
- Assert(atom.getKind() != kind::EQUAL
- || (atom[0].getKind() != kind::TUPLE_UPDATE
- && atom[1].getKind() != kind::TUPLE_UPDATE
- && atom[0].getKind() != kind::RECORD_UPDATE
- && atom[1].getKind() != kind::RECORD_UPDATE))
- << "tuple/record escaped into datatypes decision procedure; should "
- "have been rewritten away";
-
- //assert the fact
- assertFact( fact, fact );
- flushPendingFacts();
- }
-
- if( e == EFFORT_FULL && !d_conflict && !d_addedLemma && !d_valuation.needCheck() ) {
+ else if (level == EFFORT_FULL && !d_state.isInConflict()
+ && !d_im.hasAddedLemma() && !d_valuation.needCheck())
+ {
//check for cycles
- Assert(d_pending.empty());
+ Assert(!d_im.hasPendingFact());
do {
- d_addedFact = false;
+ d_im.reset();
Trace("datatypes-proc") << "Check cycles..." << std::endl;
checkCycles();
Trace("datatypes-proc") << "...finish check cycles" << std::endl;
- flushPendingFacts();
- if( d_conflict || d_addedLemma ){
+ d_im.process();
+ if (d_state.isInConflict() || d_im.hasAddedLemma())
+ {
return;
}
- }while( d_addedFact );
-
+ } while (d_im.hasAddedFact());
+
//check for splits
- Trace("datatypes-debug") << "Check for splits " << e << endl;
+ Trace("datatypes-debug") << "Check for splits " << endl;
do {
- d_addedFact = false;
+ d_im.reset();
std::map< TypeNode, Node > rec_singletons;
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
while( !eqcs_i.isFinished() ){
assumptions.push_back(assumption);
Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
- doSendLemma( lemma );
+ d_im.lemma(lemma);
}
}
}else{
//all other cases
std::vector< bool > pcons;
getPossibleCons( eqc, n, pcons );
- //std::map< int, bool > sel_apps;
- //getSelectorsForCons( n, sel_apps );
//check if we do not need to resolve the constructor type for this equivalence class.
// this is if there are no selectors for this equivalence class, and its possible values are infinite,
// then do not split.
//this may not be necessary?
//if only one constructor, then this term must be this constructor
Node t = utils::mkTester(n, 0, dt);
- d_pending.push_back( t );
- d_pending_exp[ t ] = d_true;
+ d_im.addPendingInference(t, d_true);
Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl;
- d_infer.push_back( t );
}else{
Assert(consIndex != -1 || dt.isSygus());
if( options::dtBinarySplit() && consIndex!=-1 ){
NodeBuilder<> nb(kind::OR);
nb << test << test.notNode();
Node lemma = nb;
- doSendLemma( lemma );
+ d_im.lemma(lemma);
d_out->requirePhase( test, true );
}else{
Trace("dt-split") << "*************Split for constructors on " << n << endl;
Node lemma = utils::mkSplit(n, dt);
Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
- d_out->lemma(lemma, LemmaProperty::SEND_ATOMS);
- d_addedLemma = true;
+ d_im.lemma(lemma, LemmaProperty::SEND_ATOMS, false);
}
if( !options::dtBlastSplits() ){
break;
}
++eqcs_i;
}
- if (d_addedLemma)
+ if (d_im.hasAddedLemma())
{
// clear pending facts: we added a lemma, so internal inferences are
// no longer necessary
- d_pending.clear();
- d_pending_exp.clear();
+ d_im.clearPendingFacts();
}
else
{
// we did not add a lemma, process internal inferences. This loop
// will repeat.
Trace("datatypes-debug") << "Flush pending facts..." << std::endl;
- flushPendingFacts();
+ d_im.process();
}
- }while( !d_conflict && !d_addedLemma && d_addedFact );
- Trace("datatypes-debug") << "Finished, conflict=" << d_conflict << ", lemmas=" << d_addedLemma << std::endl;
- if( !d_conflict ){
+ } while (!d_state.isInConflict() && !d_im.hasAddedLemma()
+ && d_im.hasAddedFact());
+ Trace("datatypes-debug")
+ << "Finished, conflict=" << d_state.isInConflict()
+ << ", lemmas=" << d_im.hasAddedLemma() << std::endl;
+ if (!d_state.isInConflict())
+ {
Trace("dt-model-debug") << std::endl;
printModelDebug("dt-model-debug");
}
}
- Trace("datatypes-check") << "Finished check effort " << e << std::endl;
+ Trace("datatypes-check") << "Finished check effort " << level << std::endl;
if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
Notice() << "TheoryDatatypes::check(): done" << endl;
}
return d_sygusExtension != nullptr;
}
-void TheoryDatatypes::flushPendingFacts(){
- //pending lemmas: used infrequently, only for definitional lemmas
- if( !d_pending_lem.empty() ){
- int i = 0;
- while( i<(int)d_pending_lem.size() ){
- doSendLemma( d_pending_lem[i] );
- i++;
- }
- d_pending_lem.clear();
- }
- int i = 0;
- while( !d_conflict && i<(int)d_pending.size() ){
- Node fact = d_pending[i];
- Node exp = d_pending_exp[ fact ];
- Trace("datatypes-debug") << "Assert fact (#" << (i+1) << "/" << d_pending.size() << ") " << fact << " with explanation " << exp << std::endl;
- //check to see if we have to communicate it to the rest of the system
- if( mustCommunicateFact( fact, exp ) ){
- Node lem = fact;
- if( exp.isNull() || exp==d_true ){
- Trace("dt-lemma-debug") << "Trivial explanation." << std::endl;
- }else{
- Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
- std::vector< TNode > assumptions;
- //if( options::dtRExplainLemmas() ){
- explain( exp, assumptions );
- //}else{
- // ee_exp = exp;
- //}
- //Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
- if( assumptions.empty() ){
- lem = fact;
- }else{
- std::vector< Node > children;
- for (const TNode& assumption : assumptions)
- {
- children.push_back(assumption.negate());
- }
- children.push_back( fact );
- lem = NodeManager::currentNM()->mkNode( OR, children );
- }
- }
- Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
- doSendLemma( lem );
- }else{
- assertFact( fact, exp );
- d_addedFact = true;
- }
- Trace("datatypes-debug") << "Finished fact " << fact << ", now = " << d_conflict << " " << d_pending.size() << std::endl;
- i++;
- }
- d_pending.clear();
- d_pending_exp.clear();
-}
-
-bool TheoryDatatypes::doSendLemma( Node lem ) {
- if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
- Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : " << lem << std::endl;
- d_lemmas_produced_c[lem] = true;
- d_out->lemma( lem );
- d_addedLemma = true;
- return true;
- }else{
- Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : duplicate : "
- << lem << std::endl;
- return false;
- }
-}
-bool TheoryDatatypes::doSendLemmas( std::vector< Node >& lemmas ){
- bool ret = false;
- for (const Node& lem : lemmas)
- {
- bool cret = doSendLemma(lem);
- ret = ret || cret;
- }
- lemmas.clear();
- return ret;
-}
-
-void TheoryDatatypes::assertFact( Node fact, Node exp)
+void TheoryDatatypes::notifyFact(TNode atom,
+ bool polarity,
+ TNode fact,
+ bool isInternal)
{
- Trace("datatypes-debug") << "TheoryDatatypes::assertFact : " << fact << std::endl;
- bool polarity = fact.getKind() != kind::NOT;
- TNode atom = polarity ? fact : fact[0];
- if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine->assertEquality(atom, polarity, exp);
- }else{
- d_equalityEngine->assertPredicate(atom, polarity, exp);
- }
// could be sygus-specific
if (d_sygusExtension)
{
std::vector< Node > lemmas;
d_sygusExtension->assertFact(atom, polarity, lemmas);
- doSendLemmas( lemmas );
+ d_im.sendLemmas(lemmas);
}
//add to tester if applicable
Node t_arg;
Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl;
Node rep = getRepresentative( t_arg );
EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
- addTester( tindex, fact, eqc, rep, t_arg );
+ Node tst =
+ isInternal ? (polarity ? Node(atom) : atom.notNode()) : Node(fact);
+ addTester(tindex, tst, eqc, rep, t_arg);
Trace("dt-tester") << "Done assert tester." << std::endl;
Trace("dt-tester") << "Done pending merges." << std::endl;
- if( !d_conflict && polarity ){
+ if (!d_state.isInConflict() && polarity)
+ {
if (d_sygusExtension)
{
Trace("dt-tester") << "Assert tester to sygus : " << atom << std::endl;
- //Assert( !d_sygus_util->d_conflict );
std::vector< Node > lemmas;
d_sygusExtension->assertTester(tindex, t_arg, atom, lemmas);
Trace("dt-tester") << "Done assert tester to sygus." << std::endl;
- doSendLemmas( lemmas );
+ d_im.sendLemmas(lemmas);
}
}
}else{
Trace("dt-tester-debug") << "Assert (non-tester) : " << atom << std::endl;
}
Trace("datatypes-debug") << "TheoryDatatypes::assertFact : finished " << fact << std::endl;
+ // now, flush pending facts if this wasn't an internal call
+ if (!isInternal)
+ {
+ d_im.process();
+ }
}
-void TheoryDatatypes::preRegisterTerm(TNode n) {
- Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl;
+void TheoryDatatypes::preRegisterTerm(TNode n)
+{
+ Debug("datatypes-prereg")
+ << "TheoryDatatypes::preRegisterTerm() " << n << endl;
collectTerms( n );
switch (n.getKind()) {
case kind::EQUAL:
{
std::vector< Node > lemmas;
d_sygusExtension->preRegisterTerm(n, lemmas);
- doSendLemmas( lemmas );
+ d_im.sendLemmas(lemmas);
}
- // d_equalityEngine->addTriggerTerm(n, THEORY_DATATYPES);
break;
}
- flushPendingFacts();
+ d_im.process();
}
TrustNode TheoryDatatypes::expandDefinition(Node n)
return TrustNode::null();
}
-void TheoryDatatypes::notifySharedTerm(TNode t)
-{
- Debug("datatypes") << "TheoryDatatypes::notifySharedTerm(): " << t << " "
- << t.getType().isBoolean() << endl;
- d_equalityEngine->addTriggerTerm(t, THEORY_DATATYPES);
- Debug("datatypes") << "TheoryDatatypes::notifySharedTerm() finished"
- << std::endl;
-}
-
bool TheoryDatatypes::propagateLit(TNode literal)
{
Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal << ")"
<< std::endl;
// If already in conflict, no more propagation
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal
<< "): already in conflict" << std::endl;
return false;
bool ok = d_out->propagate(literal);
if (!ok) {
Trace("dt-conflict") << "CONFLICT: Eq engine propagate conflict " << std::endl;
- d_conflict = true;
+ d_state.notifyInConflict();
}
return ok;
}
d_conflictNode = explainLit(eq);
Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
- d_conflict = true;
+ d_state.notifyInConflict();
}
/** called when a new equivalance class is created */
}
void TheoryDatatypes::merge( Node t1, Node t2 ){
- if( !d_conflict ){
+ if (!d_state.isInConflict())
+ {
TNode trep1 = t1;
TNode trep2 = t2;
Trace("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl;
d_conflictNode = explainLit(unifEq);
Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
- d_conflict = true;
+ d_state.notifyInConflict();
return;
}
else
for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
if( !areEqual( cons1[i], cons2[i] ) ){
Node eq = cons1[i].eqNode( cons2[i] );
- d_pending.push_back( eq );
- d_pending_exp[ eq ] = unifEq;
+ d_im.addPendingInference(eq, unifEq);
Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
- d_infer.push_back( eq );
- d_infer_exp.push_back( unifEq );
}
}
-/*
- for( unsigned i=0; i<rew.size(); i++ ){
- d_pending.push_back( rew[i] );
- d_pending_exp[ rew[i] ] = unifEq;
- Trace("datatypes-infer") << "DtInfer : cons-inj : " << rew[i] << " by " << unifEq << std::endl;
- d_infer.push_back( rew[i] );
- d_infer_exp.push_back( unifEq );
- }
-*/
}
}
Trace("datatypes-debug") << " instantiated : " << eqc1->d_inst << " " << eqc2->d_inst << std::endl;
Trace("datatypes-debug") << " must check if it is okay to set the constructor." << std::endl;
checkInst = true;
addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
- if( d_conflict ){
+ if (d_state.isInConflict())
+ {
return;
}
}
Node t_arg = d_labels_args[t2][i];
unsigned tindex = d_labels_tindex[t2][i];
addTester( tindex, t, eqc1, t1, t_arg );
- if( d_conflict ){
+ if (d_state.isInConflict())
+ {
Trace("datatypes-debug") << " conflict!" << std::endl;
return;
}
if( checkInst ){
Trace("datatypes-debug") << " checking instantiate" << std::endl;
instantiate( eqc1, t1 );
- if( d_conflict ){
+ if (d_state.isInConflict())
+ {
return;
}
}
return -1;
}else{
int tindex = utils::isTester(lbl);
+ Trace("datatypes-debug") << "Label of " << n << " is " << lbl
+ << " with tindex " << tindex << std::endl;
Assert(tindex != -1);
return tindex;
}
d_term_sk[n] = k;
Node eq = k.eqNode( n );
Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
- d_pending_lem.push_back( eq );
- //doSendLemma( eq );
- //d_pending_exp[ eq ] = d_true;
+ d_im.addPendingLemma(eq);
return k;
}else{
return (*it).second;
Trace("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
bool tpolarity = t.getKind()!=NOT;
+ Assert((tpolarity ? t : t[0]).getKind() == APPLY_TESTER);
Node j, jt;
bool makeConflict = false;
int prevTIndex = getLabelIndex(eqc, n);
d_conflictNode = mkAnd( assumptions );
Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
- d_conflict = true;
+ d_state.notifyInConflict();
return;
}else{
makeConflict = true;
Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl;
if( tpolarity ){
instantiate( eqc, n );
- for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
- {
- if( i!=ttindex && neg_testers.find( i )==neg_testers.end() ){
- Assert(n.getKind() != APPLY_CONSTRUCTOR);
- Node infer = utils::mkTester(n, i, dt).negate();
- Trace("datatypes-infer") << "DtInfer : neg label : " << infer << " by " << t << std::endl;
- d_infer.push_back( infer );
- d_infer_exp.push_back( t );
- }
- }
+ // We could propagate is-C1(x) => not is-C2(x) here for all other
+ // constructors, but empirically this hurts performance.
}else{
//check if we have reached the maximum number of testers
// in this case, add the positive tester
? NodeManager::currentNM()->mkConst(false)
: utils::mkTester(t_arg, testerIndex, dt);
Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
- d_pending.push_back( t_concl );
- d_pending_exp[ t_concl ] = t_concl_exp;
+ d_im.addPendingInference(t_concl, t_concl_exp);
Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl;
- d_infer.push_back( t_concl );
- d_infer_exp.push_back( t_concl_exp );
return;
}
}
}
}
if( makeConflict ){
- d_conflict = true;
+ d_state.notifyInConflict();
Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl;
std::vector< TNode > assumptions;
explain( j, assumptions );
d_conflictNode = mkAnd( assumptions );
Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
- d_conflict = true;
+ d_state.notifyInConflict();
return;
}
}
Trace("datatypes-infer") << "DtInfer : collapse sel";
//Trace("datatypes-infer") << ( wrong ? " wrong" : "");
Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl;
- d_pending.push_back( eq );
- d_pending_exp[eq] = peq;
- d_infer.push_back( eq );
- d_infer_exp.push_back(peq);
+ d_im.addPendingInference(eq, peq);
}
}
}
bool TheoryDatatypes::collectModelValues(TheoryModel* m,
const std::set<Node>& termSet)
{
- Trace("dt-cmi") << "Datatypes : Collect model info "
+ Trace("dt-cmi") << "Datatypes : Collect model values "
<< d_equalityEngine->consistent() << std::endl;
Trace("dt-model") << std::endl;
printModelDebug( "dt-model" );
Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
a = v1.eqNode( v2 ).negate();
//send out immediately as lemma
- doSendLemma( a );
+ d_im.lemma(a);
Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
}
d_singleton_lemma[index][tn] = a;
Node lem = nm->mkNode(LEQ, d_zero, n);
Trace("datatypes-infer")
<< "DtInfer : size geq zero : " << lem << std::endl;
- d_pending_lem.push_back(lem);
+ d_im.addPendingLemma(lem);
}
else if (nk == DT_HEIGHT_BOUND && n[1].getConst<Rational>().isZero())
{
: nm->mkNode(OR, children));
}
Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
- d_pending_lem.push_back(lem);
+ d_im.addPendingLemma(lem);
}
}
}
void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
+ Trace("datatypes-debug") << "Instantiate: " << n << std::endl;
//add constructor to equivalence class if not done so already
int index = getLabelIndex( eqc, n );
if (index == -1 || eqc->d_inst)
eq = tt.eqNode(tt_cons);
Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq
<< std::endl;
- d_pending.push_back(eq);
- d_pending_exp[eq] = exp;
+ d_im.addPendingInference(eq, exp);
Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl;
Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp
<< std::endl;
- d_infer.push_back(eq);
- d_infer_exp.push_back(exp);
}
void TheoryDatatypes::checkCycles() {
d_conflictNode = mkAnd( expl );
Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
- d_conflict = true;
+ d_state.notifyInConflict();
return;
}
}
Trace("dt-cdt") << std::endl;
Node eq = part_out[i][0].eqNode( part_out[i][j] );
Node eqExp = mkAnd( exp );
- d_pending.push_back( eq );
- d_pending_exp[ eq ] = eqExp;
+ d_im.addPendingInference(eq, eqExp);
Trace("datatypes-infer") << "DtInfer : cdt-bisimilar : " << eq << " by " << eqExp << std::endl;
- d_infer.push_back( eq );
- d_infer_exp.push_back( eqExp );
}
}
}
}
}
-bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
- //the datatypes decision procedure makes "internal" inferences apart from the equality engine :
- // (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
- // (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
- // (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
- // (4) collapse selector : S( C( t1...tn ) ) = t'
- // (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... + size( tn )
- // (6) non-negative size : 0 <= size( t )
- //We may need to communicate outwards if the conclusions involve other theories. Also communicate (6) and OR conclusions.
- Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
- bool addLemma = false;
- if( options::dtInferAsLemmas() && exp!=d_true ){
- addLemma = true;
- }else if( n.getKind()==EQUAL ){
- TypeNode tn = n[0].getType();
- if( !tn.isDatatype() ){
- addLemma = true;
- }else{
- const DType& dt = tn.getDType();
- addLemma = dt.involvesExternalType();
- }
- }else if( n.getKind()==LEQ || n.getKind()==OR ){
- addLemma = true;
- }
- if( addLemma ){
- Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
- return true;
- }else{
- Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
- return false;
- }
-}
-
bool TheoryDatatypes::hasTerm(TNode a) { return d_equalityEngine->hasTerm(a); }
bool TheoryDatatypes::areEqual( TNode a, TNode b ){
}
++eqcs_i;
}
- Trace("dt-cmi") << "After adding non-singletons, has " << termSet.size()
- << " relevant terms..." << std::endl;
}
std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit)
#include "expr/attribute.h"
#include "expr/node_trie.h"
#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/inference_manager.h"
#include "theory/datatypes/sygus_extension.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
- /** inferences */
- NodeList d_infer;
- NodeList d_infer_exp;
Node d_true;
Node d_zero;
/** mkAnd */
TNode t2,
bool value) override
{
+ AlwaysAssert(tag == THEORY_DATATYPES);
Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
return d_dt.propagateLit(t1.eqNode(t2));
/** selector apps for eqch equivalence class */
NodeUIntMap d_selector_apps;
std::map< Node, std::vector< Node > > d_selector_apps_data;
- /** Are we in conflict */
- context::CDO<bool> d_conflict;
- /** added lemma
- *
- * This flag is set to true during a full effort check if this theory
- * called d_out->lemma(...).
- */
- bool d_addedLemma;
- /** added fact
- *
- * This flag is set to true during a full effort check if this theory
- * added an internal fact to its equality engine.
- */
- bool d_addedFact;
/** The conflict node */
Node d_conflictNode;
/**
* collectTerms(...) on.
*/
BoolMap d_collectTermsCacheU;
- /** pending assertions/merges */
- std::vector< Node > d_pending_lem;
- std::vector< Node > d_pending;
- std::map< Node, Node > d_pending_exp;
/** All the function terms that the theory has seen */
context::CDList<TNode> d_functionTerms;
/** counter for forcing assignments (ensures fairness) */
/** assert fact */
void assertFact( Node fact, Node exp );
- /** flush pending facts */
- void flushPendingFacts();
-
- /** do send lemma */
- bool doSendLemma( Node lem );
- bool doSendLemmas( std::vector< Node >& lem );
/** get or make eqc info */
EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
/** finish initialization */
void finishInit() override;
//--------------------------------- end initialization
-
/** propagate */
bool propagateLit(TNode literal);
+ /** Conflict when merging two constants */
+ void conflict(TNode a, TNode b);
/** explain */
void addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions );
void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
TrustNode explain(TNode literal) override;
Node explainLit(TNode literal);
Node explain( std::vector< Node >& lits );
- /** Conflict when merging two constants */
- void conflict(TNode a, TNode b);
/** called when a new equivalance class is created */
void eqNotifyNewClass(TNode t);
/** called when two equivalance classes have merged */
void eqNotifyMerge(TNode t1, TNode t2);
- void check(Effort e) override;
+ //--------------------------------- standard check
+ /** Do we need a check call at last call effort? */
bool needsCheckLastEffort() override;
+ /** Pre-check, called before the fact queue of the theory is processed. */
+ bool preCheck(Effort level) override;
+ /** Post-check, called after the fact queue of the theory is processed. */
+ void postCheck(Effort level) override;
+ /** Notify fact */
+ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+ //--------------------------------- end standard check
void preRegisterTerm(TNode n) override;
TrustNode expandDefinition(Node n) override;
TrustNode ppRewrite(TNode n) override;
- void notifySharedTerm(TNode t) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
- bool collectModelValues(TheoryModel* m,
- const std::set<Node>& termSet) override;
- void shutdown() override {}
std::string identify() const override
{
return std::string("TheoryDatatypes");
Node getInstantiateCons(Node n, const DType& dt, int index);
/** check instantiate */
void instantiate( EqcInfo* eqc, Node n );
- /** must communicate fact */
- bool mustCommunicateFact( Node n, Node exp );
private:
//equality queries
bool hasTerm( TNode a );
bool areCareDisequal( TNode x, TNode y );
TNode getRepresentative( TNode a );
+ /** Collect model values in m based on the relevant terms given by termSet */
+ bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet) override;
/**
* Compute relevant terms. This includes datatypes in non-singleton
* equivalence classes.
DatatypesRewriter d_rewriter;
/** A (default) theory state object */
TheoryState d_state;
+ /** The inference manager */
+ InferenceManager d_im;
};/* class TheoryDatatypes */
}/* CVC4::theory::datatypes namespace */
projects / cvc5.git / commitdiff