diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/theory/uf | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 14 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 2 | ||||
-rw-r--r-- | src/theory/uf/kinds | 2 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 9 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 31 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 7 |
8 files changed, 37 insertions, 42 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 5d929a708..f7084bec3 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -230,8 +230,8 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { d_isConstant.push_back(false); // No terms to evaluate by defaul d_subtermsToEvaluate.push_back(0); - // Mark Boolean nodes - d_isBoolean.push_back(false); + // Mark equality nodes + d_isEquality.push_back(false); // Mark the node as internal by default d_isInternal.push_back(true); // Add the equality node to the nodes @@ -329,10 +329,10 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { d_isConstant[result] = !isOperator && t.isConst(); } - if (t.getType().isBoolean()) { + if (t.getKind() == kind::EQUAL) { // We set this here as this only applies to actual terms, not the // intermediate application terms - d_isBoolean[result] = true; + d_isEquality[result] = true; } else if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); @@ -613,7 +613,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Update class2 table lookup and information if not a boolean // since booleans can't be in an application - if (!d_isBoolean[class2Id]) { + if (!d_isEquality[class2Id]) { Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl; do { // Get the current node @@ -869,7 +869,7 @@ void EqualityEngine::backtrack() { d_nodeIndividualTrigger.resize(d_nodesCount); d_isConstant.resize(d_nodesCount); d_subtermsToEvaluate.resize(d_nodesCount); - d_isBoolean.resize(d_nodesCount); + d_isEquality.resize(d_nodesCount); d_isInternal.resize(d_nodesCount); d_equalityGraph.resize(d_nodesCount); d_equalityNodes.resize(d_nodesCount); @@ -1268,7 +1268,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } else { eqp->d_id = MERGED_THROUGH_TRANS; eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); - eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); + eqp->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); } eqp->debug_print("pf::ee", 1); diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 18e83bd1a..46ec7403b 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -464,7 +464,7 @@ private: /** * Map from ids to whether they are Boolean. */ - std::vector<bool> d_isBoolean; + std::vector<bool> d_isEquality; /** * Map from ids to whether the nods is internal. An internal node is a node diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 888fa140f..e2d740e20 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -15,6 +15,8 @@ parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; fi typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule +variable BOOLEAN_TERM_VARIABLE "Boolean term variable" + operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S" typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index ed5d99bdf..ca7284689 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -246,8 +246,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) { } else { if( (*i).getKind() == kind::OR ) { kids.push_back(normInternal(*i, level)); - } else if((*i).getKind() == kind::IFF || - (*i).getKind() == kind::EQUAL) { + } else if((*i).getKind() == kind::EQUAL) { kids.push_back(normInternal(*i, level)); if((*i)[0].isVar() || (*i)[1].isVar()) { @@ -291,8 +290,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) { first = false; matchingTerm = TNode::null(); kids.push_back(normInternal(*i, level + 1)); - } else if((*i).getKind() == kind::IFF || - (*i).getKind() == kind::EQUAL) { + } else if((*i).getKind() == kind::EQUAL) { kids.push_back(normInternal(*i, level + 1)); if((*i)[0].isVar() || (*i)[1].isVar()) { @@ -361,8 +359,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) { sort(kids.begin(), kids.end()); return result = NodeManager::currentNM()->mkNode(k, kids); } - - case kind::IFF: + case kind::EQUAL: if(n[0].isVar() || n[1].isVar()) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4cdc5e240..e4a3ac78c 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -139,14 +139,14 @@ void TheoryUF::check(Effort level) { } } - - if (d_thss != NULL && ! d_conflict) { - d_thss->check(level); - if( d_thss->isConflict() ){ - d_conflict = true; + if(! d_conflict ){ + if (d_thss != NULL) { + d_thss->check(level); + if( d_thss->isConflict() ){ + d_conflict = true; + } } } - }/* TheoryUF::check() */ void TheoryUF::preRegisterTerm(TNode node) { @@ -217,7 +217,7 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if (atom.getKind() == kind::EQUAL) { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf); } else { d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf); @@ -336,10 +336,10 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { if(n.getKind() == kind::OR && n.getNumChildren() == 2 && n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && - (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && - (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && - (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && - (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) { + (n[0][0].getKind() == kind::EQUAL) && + (n[0][1].getKind() == kind::EQUAL) && + (n[1][0].getKind() == kind::EQUAL) && + (n[1][1].getKind() == kind::EQUAL)) { // now we have (a = b && c = d) || (e = f && g = h) Debug("diamonds") << "has form of a diamond!" << endl; @@ -396,7 +396,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { (a == h && d == e) ) { // learn: n implies a == d Debug("diamonds") << "+ C holds" << endl; - Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d); + Node newEquality = a.eqNode(d); Debug("diamonds") << " ==> " << newEquality << endl; learned << n.impNode(newEquality); } else { @@ -533,12 +533,7 @@ void TheoryUF::computeCareGraph() { void TheoryUF::conflict(TNode a, TNode b) { eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; - - if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b),pf); - } else { - d_conflictNode = explain(a.eqNode(b),pf); - } + d_conflictNode = explain(a.eqNode(b),pf); ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; d_out->conflict(d_conflictNode, puf); d_conflict = true; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 0900b4c90..ce9c70ca2 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -82,27 +82,27 @@ public: } void eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.conflict(t1, t2); } void eqNotifyNewClass(TNode t) { - Debug("uf") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; d_uf.eqNotifyNewClass(t); } void eqNotifyPreMerge(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.eqNotifyPreMerge(t1, t2); } void eqNotifyPostMerge(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.eqNotifyPostMerge(t1, t2); } void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { - Debug("uf") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl; d_uf.eqNotifyDisequal(t1, t2, reason); } diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 166d11451..bce6003eb 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -32,7 +32,7 @@ class TheoryUfRewriter { public: static RewriteResponse postRewrite(TNode node) { - if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { + if(node.getKind() == kind::EQUAL) { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } else if(node[0].isConst() && node[1].isConst()) { @@ -76,7 +76,7 @@ public: } static RewriteResponse preRewrite(TNode node) { - if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { + if(node.getKind() == kind::EQUAL) { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } else if(node[0].isConst() && node[1].isConst()) { diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 6b89c3524..51648fb26 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -639,7 +639,7 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ int bi = d_regions_map[b]; if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){ Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl; - //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) || + //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL || // a!=reason[0][0] || b!=reason[0][1] ){ // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl; //} @@ -1861,8 +1861,9 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ //otherwise, make equal via lemma if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){ Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] ); - Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << lit.iffNode( eqv_lit ) << std::endl; - getOutputChannel().lemma( lit.iffNode( eqv_lit ) ); + eqv_lit = lit.eqNode( eqv_lit ); + Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl; + getOutputChannel().lemma( eqv_lit ); d_card_assertions_eqv_lemma[lit] = true; } } |