From 62ec0666dd4d409ee85603ae94d7ab1a2b4c9dcc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Sep 2020 16:22:54 -0500 Subject: [PATCH] (new theory) Update TheoryDatatypes to the new standard (#4986) Updates it to use the new inference manager as well as updating its check to the standard callbacks. --- src/theory/datatypes/inference_manager.cpp | 13 + src/theory/datatypes/inference_manager.h | 5 + src/theory/datatypes/theory_datatypes.cpp | 364 ++++++--------------- src/theory/datatypes/theory_datatypes.h | 55 +--- 4 files changed, 133 insertions(+), 304 deletions(-) diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 3dc16355b..762cdfd8b 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -108,6 +108,19 @@ void InferenceManager::process() doPendingFacts(); } +bool InferenceManager::sendLemmas(const std::vector& lemmas) +{ + bool ret = false; + for (const Node& lem : lemmas) + { + if (lemma(lem)) + { + ret = true; + } + } + return ret; +} + } // namespace datatypes } // namespace theory } // namespace CVC4 diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 0dda3259e..0dfdfb281 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -81,6 +81,11 @@ class InferenceManager : public InferenceManagerBuffered * or processed internally. */ void process(); + /** + * Send lemmas with property NONE on the output channel immediately. + * Returns true if any lemma was sent. + */ + bool sendLemmas(const std::vector& lemmas); }; } // namespace datatypes diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 4c8fa87ba..78b6d81c2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -47,22 +47,18 @@ TheoryDatatypes::TheoryDatatypes(Context* c, 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 ); @@ -71,6 +67,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, // indicate we are using the default theory state object d_theoryState = &d_state; + d_inferManager = &d_im; } TheoryDatatypes::~TheoryDatatypes() { @@ -156,64 +153,43 @@ TNode TheoryDatatypes::getEqcConstructor( TNode r ) { } } -void TheoryDatatypes::check(Effort e) { - if (done() && e lemmas; + std::vector 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() ){ @@ -265,7 +241,7 @@ void TheoryDatatypes::check(Effort e) { 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{ @@ -279,8 +255,6 @@ void TheoryDatatypes::check(Effort e) { //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. @@ -322,10 +296,8 @@ void TheoryDatatypes::check(Effort e) { //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 ){ @@ -335,14 +307,13 @@ void TheoryDatatypes::check(Effort e) { 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; @@ -358,29 +329,32 @@ void TheoryDatatypes::check(Effort e) { } ++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; } @@ -390,100 +364,17 @@ bool TheoryDatatypes::needsCheckLastEffort() { 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; @@ -493,28 +384,37 @@ void TheoryDatatypes::assertFact( Node fact, Node exp) 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: @@ -530,12 +430,11 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { { 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) @@ -699,21 +598,13 @@ TrustNode TheoryDatatypes::ppRewrite(TNode in) 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; @@ -723,7 +614,7 @@ bool TheoryDatatypes::propagateLit(TNode literal) 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; } @@ -805,7 +696,7 @@ void TheoryDatatypes::conflict(TNode a, TNode b){ 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 */ @@ -826,7 +717,8 @@ void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2) } 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; @@ -855,7 +747,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ 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 @@ -864,22 +756,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ 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; id_inst << " " << eqc2->d_inst << std::endl; @@ -889,7 +769,8 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ 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; } } @@ -916,7 +797,8 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ 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; } @@ -940,7 +822,8 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( checkInst ){ Trace("datatypes-debug") << " checking instantiate" << std::endl; instantiate( eqc1, t1 ); - if( d_conflict ){ + if (d_state.isInConflict()) + { return; } } @@ -979,6 +862,8 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){ 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; } @@ -1033,9 +918,7 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) { 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; @@ -1051,6 +934,7 @@ void TheoryDatatypes::addTester( 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); @@ -1068,7 +952,7 @@ void TheoryDatatypes::addTester( 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; @@ -1122,16 +1006,8 @@ void TheoryDatatypes::addTester( 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 @@ -1167,18 +1043,15 @@ void TheoryDatatypes::addTester( ? 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 ); @@ -1245,7 +1118,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ 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; } } @@ -1332,10 +1205,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { 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); } } } @@ -1486,7 +1356,7 @@ void TheoryDatatypes::computeCareGraph(){ bool TheoryDatatypes::collectModelValues(TheoryModel* m, const std::set& 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" ); @@ -1639,7 +1509,7 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) { 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; @@ -1697,7 +1567,7 @@ void TheoryDatatypes::collectTerms( Node n ) { 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().isZero()) { @@ -1722,7 +1592,7 @@ void TheoryDatatypes::collectTerms( Node n ) { : nm->mkNode(OR, children)); } Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; - d_pending_lem.push_back(lem); + d_im.addPendingLemma(lem); } } @@ -1751,6 +1621,7 @@ Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index) } 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) @@ -1781,13 +1652,10 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ 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() { @@ -1822,7 +1690,7 @@ 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; } } @@ -1872,11 +1740,8 @@ void TheoryDatatypes::checkCycles() { 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 ); } } } @@ -2051,39 +1916,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, } } -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 ){ @@ -2250,8 +2082,6 @@ void TheoryDatatypes::computeRelevantTerms(std::set& termSet) } ++eqcs_i; } - Trace("dt-cmi") << "After adding non-singletons, has " << termSet.size() - << " relevant terms..." << std::endl; } std::pair TheoryDatatypes::entailmentCheck(TNode lit) diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 211653125..37a4f81f7 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -26,6 +26,7 @@ #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" @@ -43,9 +44,6 @@ class TheoryDatatypes : public Theory { typedef context::CDHashMap BoolMap; typedef context::CDHashMap NodeMap; - /** inferences */ - NodeList d_infer; - NodeList d_infer_exp; Node d_true; Node d_zero; /** mkAnd */ @@ -70,6 +68,7 @@ class TheoryDatatypes : public Theory { 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)); @@ -169,20 +168,6 @@ private: /** 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 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; /** @@ -195,10 +180,6 @@ private: * 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 d_functionTerms; /** counter for forcing assignments (ensures fairness) */ @@ -218,12 +199,6 @@ private: /** 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 ); @@ -263,9 +238,10 @@ private: /** 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& assumptions, std::vector& tassumptions ); void explainEquality( TNode a, TNode b, bool polarity, std::vector& assumptions ); @@ -274,23 +250,25 @@ private: 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& termSet) override; - void shutdown() override {} std::string identify() const override { return std::string("TheoryDatatypes"); @@ -337,8 +315,6 @@ private: 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 ); @@ -347,6 +323,9 @@ private: 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& termSet) override; /** * Compute relevant terms. This includes datatypes in non-singleton * equivalence classes. @@ -360,6 +339,8 @@ private: DatatypesRewriter d_rewriter; /** A (default) theory state object */ TheoryState d_state; + /** The inference manager */ + InferenceManager d_im; };/* class TheoryDatatypes */ }/* CVC4::theory::datatypes namespace */ -- 2.30.2