summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/equality_engine.cpp14
-rw-r--r--src/theory/uf/equality_engine.h2
-rw-r--r--src/theory/uf/kinds2
-rw-r--r--src/theory/uf/symmetry_breaker.cpp9
-rw-r--r--src/theory/uf/theory_uf.cpp31
-rw-r--r--src/theory/uf/theory_uf.h10
-rw-r--r--src/theory/uf/theory_uf_rewriter.h4
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp7
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;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback