diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-14 09:25:03 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-14 09:25:03 -0500 |
commit | 57a2dca922e27ce7da8733d3d411148f23450bf7 (patch) | |
tree | 16e001492ec264cf08eaedf72d07927324b12147 | |
parent | e24dda4029d2cc98fcd7237c78216b5413346c2a (diff) | |
parent | 21439d98e9afe1541bb0f5371c4ab0011666bd5e (diff) |
Merge branch 'master' into fixWinTypesfixWinTypes
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 102 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 9 | ||||
-rw-r--r-- | src/theory/theory_inference_manager.cpp | 1 | ||||
-rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 2 |
4 files changed, 53 insertions, 61 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 585f13d82..afa640650 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -602,21 +602,7 @@ bool TheoryDatatypes::propagateLit(TNode literal) { Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal << ")" << std::endl; - // If already in conflict, no more propagation - if (d_state.isInConflict()) - { - Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal - << "): already in conflict" << std::endl; - return false; - } - Trace("dt-prop") << "dtPropagate " << literal << std::endl; - // Propagate out - bool ok = d_out->propagate(literal); - if (!ok) { - Trace("dt-conflict") << "CONFLICT: Eq engine propagate conflict " << std::endl; - d_state.notifyInConflict(); - } - return ok; + return d_im.propagateLit(literal); } void TheoryDatatypes::addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ) { @@ -671,8 +657,7 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){ TrustNode TheoryDatatypes::explain(TNode literal) { - Node exp = explainLit(literal); - return TrustNode::mkTrustPropExp(literal, exp, nullptr); + return d_im.explainLit(literal); } Node TheoryDatatypes::explainLit(TNode literal) @@ -692,11 +677,9 @@ Node TheoryDatatypes::explain( std::vector< Node >& lits ) { /** Conflict when merging two constants */ void TheoryDatatypes::conflict(TNode a, TNode b){ - Node eq = a.eqNode(b); - d_conflictNode = explainLit(eq); - Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_state.notifyInConflict(); + Trace("dt-conflict") << "CONFLICT: Eq engine conflict merge : " << a + << " == " << b << std::endl; + d_im.conflictEqConstantMerge(a, b); } /** called when a new equivalance class is created */ @@ -744,10 +727,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ std::vector< Node > rew; if (utils::checkClash(cons1, cons2, rew)) { - d_conflictNode = explainLit(unifEq); - Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_state.notifyInConflict(); + std::vector<Node> conf; + conf.push_back(unifEq); + Trace("dt-conflict") + << "CONFLICT: Clash conflict : " << conf << std::endl; + d_im.conflictExp(conf, nullptr); return; } else @@ -946,13 +930,12 @@ void TheoryDatatypes::addTester( { if( !eqc->d_constructor.get().isNull() ){ //conflict because equivalence class contains a constructor - std::vector< TNode > assumptions; - explain( t, assumptions ); - explainEquality( eqc->d_constructor.get(), t_arg, true, assumptions ); - d_conflictNode = mkAnd( assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_state.notifyInConflict(); + std::vector<Node> conf; + conf.push_back(t); + conf.push_back(eqc->d_constructor.get().eqNode(t_arg)); + Trace("dt-conflict") + << "CONFLICT: Tester eq conflict " << conf << std::endl; + d_im.conflictExp(conf, nullptr); return; }else{ makeConflict = true; @@ -1051,15 +1034,13 @@ void TheoryDatatypes::addTester( } } if( makeConflict ){ - d_state.notifyInConflict(); Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl; - std::vector< TNode > assumptions; - explain( j, assumptions ); - explain( t, assumptions ); - explainEquality( jt[0], t_arg, true, assumptions ); - d_conflictNode = mkAnd( assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); + std::vector<Node> conf; + conf.push_back(j); + conf.push_back(t); + conf.push_back(jt[0].eqNode(t_arg)); + Trace("dt-conflict") << "CONFLICT: Tester conflict : " << conf << std::endl; + d_im.conflictExp(conf, nullptr); } } @@ -1112,13 +1093,12 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ unsigned tindex = d_labels_tindex[n][i]; if (tindex == constructorIndex) { - std::vector< TNode > assumptions; - explain( t, assumptions ); - explainEquality( c, t[0][0], true, assumptions ); - d_conflictNode = mkAnd( assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_state.notifyInConflict(); + std::vector<Node> conf; + conf.push_back(t); + conf.push_back(c.eqNode(t[0][0])); + Trace("dt-conflict") + << "CONFLICT: Tester merge eq conflict : " << conf << std::endl; + d_im.conflictExp(conf, nullptr); return; } } @@ -1671,7 +1651,7 @@ void TheoryDatatypes::checkCycles() { //do cycle checks std::map< TNode, bool > visited; std::map< TNode, bool > proc; - std::vector< TNode > expl; + std::vector<Node> expl; Trace("datatypes-cycle-check") << "...search for cycle starting at " << eqc << std::endl; Node cn = searchForCycle( eqc, eqc, visited, proc, expl ); Trace("datatypes-cycle-check") << "...finish." << std::endl; @@ -1687,10 +1667,9 @@ void TheoryDatatypes::checkCycles() { if( !cn.isNull() ) { Assert(expl.size() > 0); - d_conflictNode = mkAnd( expl ); - Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_state.notifyInConflict(); + Trace("dt-conflict") + << "CONFLICT: Cycle conflict : " << expl << std::endl; + d_im.conflictExp(expl, nullptr); return; } } @@ -1860,16 +1839,23 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< } //postcondition: if cycle detected, explanation is why n is a subterm of on -Node TheoryDatatypes::searchForCycle( TNode n, TNode on, - std::map< TNode, bool >& visited, std::map< TNode, bool >& proc, - std::vector< TNode >& explanation, bool firstTime ) { +Node TheoryDatatypes::searchForCycle(TNode n, + TNode on, + std::map<TNode, bool>& visited, + std::map<TNode, bool>& proc, + std::vector<Node>& explanation, + bool firstTime) +{ Trace("datatypes-cycle-check2") << "Search for cycle " << n << " " << on << endl; TNode ncons; TNode nn; if( !firstTime ){ nn = getRepresentative( n ); if( nn==on ){ - explainEquality( n, nn, true, explanation ); + if (n != nn) + { + explanation.push_back(n.eqNode(nn)); + } return on; } }else{ @@ -1893,7 +1879,7 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, //add explanation for why the constructor is connected if (n != nncons) { - explainEquality(n, nncons, true, explanation); + explanation.push_back(n.eqNode(nncons)); } return on; }else if( !cn.isNull() ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index bf5d33177..d34390a5f 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -293,9 +293,12 @@ private: Node removeUninterpretedConstants( Node n, std::map< Node, Node >& visited ); /** for checking if cycles exist */ void checkCycles(); - Node searchForCycle( TNode n, TNode on, - std::map< TNode, bool >& visited, std::map< TNode, bool >& proc, - std::vector< TNode >& explanation, bool firstTime = true ); + Node searchForCycle(TNode n, + TNode on, + std::map<TNode, bool>& visited, + std::map<TNode, bool>& proc, + std::vector<Node>& explanation, + bool firstTime = true); /** for checking whether two codatatype terms must be equal */ void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out, std::vector< TNode >& exp, diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 81f5c45e6..980763040 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -141,6 +141,7 @@ TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp, { if (d_pfee != nullptr) { + Assert(pg != nullptr); // use proof equality engine to construct the trust node return d_pfee->assertConflict(exp, pg); } diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 00e4662f9..fa9482094 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -221,6 +221,7 @@ TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp, TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp, ProofGenerator* pg) { + Assert(pg != nullptr); Trace("pfee") << "pfee::assertConflict " << exp << " via generator" << std::endl; return assertLemma(d_false, exp, {}, pg); @@ -306,6 +307,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, const std::vector<Node>& noExplain, ProofGenerator* pg) { + Assert(pg != nullptr); Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp << ", noExplain = " << noExplain << " via buffer with generator" << std::endl; |