diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-05 16:21:50 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-05 16:21:50 +0000 |
commit | 7342d1ca87397f3d5beb2c04b819243303e69a7c (patch) | |
tree | 9e166f1884275be7d4b33b13b8bcfe9418e61033 /src/theory/booleans | |
parent | af25c3f8498198dd6dd114c3b4ef39af54611e1e (diff) |
updated preprocessing and rewriting input equalities into inequalities for LRA
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 619 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 207 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 137 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 2 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 53 |
5 files changed, 496 insertions, 522 deletions
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index e5055c164..fd44ec13b 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -19,6 +19,7 @@ #include "theory/booleans/circuit_propagator.h" #include "util/utility.h" +#include <stack> #include <vector> #include <algorithm> @@ -28,353 +29,363 @@ namespace CVC4 { namespace theory { namespace booleans { -void CircuitPropagator::propagateBackward(TNode in, bool polarity, vector<TNode>& changed) { - if(!isPropagatedBackward(in)) { - Debug("circuit-prop") << push << "propagateBackward(" << polarity << "): " << in << endl; - setPropagatedBackward(in); - // backward rules - switch(Kind k = in.getKind()) { +void CircuitPropagator::assert(TNode assertion) +{ + if (assertion.getKind() == kind::AND) { + for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) { + assert(assertion[i]); + } + } else { + // Analyze the assertion for back-edges and all that + computeBackEdges(assertion); + // Assign the given assertion to true + assignAndEnqueue(assertion, true); + } +} + +void CircuitPropagator::computeBackEdges(TNode node) { + + Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" << endl; + + // Vector of nodes to visit + vector<TNode> toVisit; + + // Start with the top node + if (d_seen.find(node) == d_seen.end()) { + toVisit.push_back(node); + d_seen.insert(node); + } + + // Initialize the back-edges for the root, so we don't have a special case + d_backEdges[node]; + + // Go through the visit list + for (unsigned i = 0; i < toVisit.size(); ++ i) { + // Node we need to visit + TNode current = toVisit[i]; + Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(): processing " << current << endl; + Assert(d_seen.find(current) != d_seen.end()); + + // If this not an atom visit all the children and compute the back edges + if (Theory::theoryOf(current) == THEORY_BOOL) { + for (unsigned child = 0, child_end = current.getNumChildren(); child < child_end; ++ child) { + TNode childNode = current[child]; + // Add the back edge + d_backEdges[childNode].push_back(current); + // Add to the queue if not seen yet + if (d_seen.find(childNode) == d_seen.end()) { + toVisit.push_back(childNode); + d_seen.insert(childNode); + } + } + } + } +} + +void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) { + + Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl; + + // backward rules + switch(parent.getKind()) { + case kind::AND: + if (parentAssignment) { + // AND = TRUE: forall children c, assign(c = TRUE) + for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) { + assignAndEnqueue(*i, true); + } + } else { + // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) + TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + if (holdout != parent.end()) { + assignAndEnqueue(*holdout, false); + } + } + break; + case kind::OR: + if (parentAssignment) { + // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) + TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + if (holdout != parent.end()) { + assignAndEnqueue(*holdout, true); + } + } else { + // OR = FALSE: forall children c, assign(c = FALSE) + for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) { + assignAndEnqueue(*i, false); + } + } + break; + case kind::NOT: + // NOT = b: assign(c = !b) + assignAndEnqueue(parent[0], !parentAssignment); + break; + case kind::ITE: + if (isAssignedTo(parent[0], true)) { + // ITE c x y = v: if c is assigned and TRUE, assign(x = v) + assignAndEnqueue(parent[1], parentAssignment); + } else if (isAssignedTo(parent[0], false)) { + // ITE c x y = v: if c is assigned and FALSE, assign(y = v) + assignAndEnqueue(parent[2], parentAssignment); + } else if (isAssigned(parent[1]) && isAssigned(parent[2])) { + if (getAssignment(parent[1]) == parentAssignment && getAssignment(parent[2]) != parentAssignment) { + // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE) + assignAndEnqueue(parent[0], true); + } else if (getAssignment(parent[1]) != parentAssignment && getAssignment(parent[2]) == parentAssignment) { + // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE) + assignAndEnqueue(parent[0], false); + } + } + break; + case kind::IFF: + if (parentAssignment) { + // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment]) + if (isAssigned(parent[0])) { + assignAndEnqueue(parent[1], getAssignment(parent[0])); + } else if (isAssigned(parent[1])) { + assignAndEnqueue(parent[0], getAssignment(parent[1])); + } + } else { + // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment]) + if (isAssigned(parent[0])) { + assignAndEnqueue(parent[1], !getAssignment(parent[0])); + } else if (isAssigned(parent[1])) { + assignAndEnqueue(parent[0], !getAssignment(parent[1])); + } + } + break; + case kind::IMPLIES: + if (parentAssignment) { + if (isAssignedTo(parent[0], true)) { + // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE) + assignAndEnqueue(parent[1], true); + } + if (isAssignedTo(parent[1], false)) { + // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) + assignAndEnqueue(parent[0], false); + } + } else { + // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE) + assignAndEnqueue(parent[0], true); + assignAndEnqueue(parent[1], false); + } + break; + case kind::XOR: + if (parentAssignment) { + if (isAssigned(parent[0])) { + // XOR x y = TRUE, and x assigned, assign(y = !assignment(x)) + assignAndEnqueue(parent[1], !getAssignment(parent[0])); + } else if (isAssigned(parent[1])) { + // XOR x y = TRUE, and y assigned, assign(x = !assignment(y)) + assignAndEnqueue(parent[0], !getAssignment(parent[1])); + } + } else { + if (isAssigned(parent[0])) { + // XOR x y = FALSE, and x assigned, assign(y = assignment(x)) + assignAndEnqueue(parent[1], getAssignment(parent[0])); + } else if (isAssigned(parent[1])) { + // XOR x y = FALSE, and y assigned, assign(x = assignment(y)) + assignAndEnqueue(parent[0], getAssignment(parent[1])); + } + } + break; + default: + Unhandled(); + } +} + + +void CircuitPropagator::propagateForward(TNode child, bool childAssignment) { + + // The assignment we have + Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child << ", " << childAssignment << ")" << endl; + + // Get the back any nodes where this is child + const vector<TNode>& parents = d_backEdges.find(child)->second; + + // Go through the parents and see if there is anything to propagate + vector<TNode>::const_iterator parent_it = parents.begin(); + vector<TNode>::const_iterator parent_it_end = parents.end(); + for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) { + // The current parent of the child + TNode parent = *parent_it; + Assert(parent.hasSubterm(child)); + + // Forward rules + switch(parent.getKind()) { case kind::AND: - if(polarity) { - // AND = TRUE: forall children c, assign(c = TRUE) - for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) { - Debug("circuit-prop") << "bAND1" << endl; - assign(*i, true, changed); + if (childAssignment) { + TNode::iterator holdout; + holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + if (holdout == parent.end()) { // all children are assigned TRUE + // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE) + assignAndEnqueue(parent, true); + } else if (isAssignedTo(parent, false)) {// the AND is FALSE + // is the holdout unique ? + TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, true))); + if (other == parent.end()) { // the holdout is unique + // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE) + assignAndEnqueue(*holdout, false); + } } } else { - // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) - TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, true))); - if(holdout != in.end()) { - Debug("circuit-prop") << "bAND2" << endl; - assign(*holdout, false, changed); - } + // AND ...(x=FALSE)...: assign(AND = FALSE) + assignAndEnqueue(parent, false); } break; case kind::OR: - if(polarity) { - // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) - TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, false))); - if(holdout != in.end()) { - Debug("circuit-prop") << "bOR1" << endl; - assign(*holdout, true, changed); - } + if (childAssignment) { + // OR ...(x=TRUE)...: assign(OR = TRUE) + assignAndEnqueue(parent, true); } else { - // OR = FALSE: forall children c, assign(c = FALSE) - for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) { - Debug("circuit-prop") << "bOR2" << endl; - assign(*i, false, changed); + TNode::iterator holdout; + holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + if (holdout == parent.end()) { // all children are assigned FALSE + // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE) + assignAndEnqueue(parent, false); + } else if (isAssignedTo(parent, true)) {// the OR is TRUE + // is the holdout unique ? + TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, false))); + if (other == parent.end()) { // the holdout is unique + // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE) + assignAndEnqueue(*holdout, true); + } } } break; + case kind::NOT: - // NOT = b: assign(c = !b) - Debug("circuit-prop") << "bNOT" << endl; - assign(in[0], !polarity, changed); + // NOT (x=b): assign(NOT = !b) + assignAndEnqueue(parent, !childAssignment); break; + case kind::ITE: - if(isAssignedTo(in[0], true)) { - // ITE c x y = v: if c is assigned and TRUE, assign(x = v) - Debug("circuit-prop") << "bITE1" << endl; - assign(in[1], polarity, changed); - } else if(isAssignedTo(in[0], false)) { - // ITE c x y = v: if c is assigned and FALSE, assign(y = v) - Debug("circuit-prop") << "bITE2" << endl; - assign(in[2], polarity, changed); - } else if(isAssigned(in[1]) && isAssigned(in[2])) { - if(assignment(in[1]) == polarity && assignment(in[2]) != polarity) { - // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE) - Debug("circuit-prop") << "bITE3" << endl; - assign(in[0], true, changed); - } else if(assignment(in[1]) == !polarity && assignment(in[2]) == polarity) { - // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE) - Debug("circuit-prop") << "bITE4" << endl; - assign(in[0], true, changed); + if (child == parent[0]) { + if (childAssignment) { + if (isAssigned(parent[1])) { + // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment) + assignAndEnqueue(parent, getAssignment(parent[1])); + } + } else { + if (isAssigned(parent[2])) { + // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment) + assignAndEnqueue(parent, getAssignment(parent[2])); + } + } + } + if (child == parent[1]) { + if (isAssignedTo(parent[0], true)) { + // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v) + assignAndEnqueue(parent, childAssignment); + } + } + if (child == parent[2]) { + Assert(child == parent[2]); + if (isAssignedTo(parent[0], false)) { + // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v) + assignAndEnqueue(parent, childAssignment); } } break; case kind::IFF: - if(polarity) { - // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment]) - if(isAssigned(in[0])) { - assign(in[1], assignment(in[0]), changed); - Debug("circuit-prop") << "bIFF1" << endl; - } else if(isAssigned(in[1])) { - Debug("circuit-prop") << "bIFF2" << endl; - assign(in[0], assignment(in[1]), changed); - } + if (isAssigned(parent[0]) && isAssigned(parent[1])) { + // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment)) + assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1])); } else { - // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment]) - if(isAssigned(in[0])) { - Debug("circuit-prop") << "bIFF3" << endl; - assign(in[1], !assignment(in[0]), changed); - } else if(isAssigned(in[1])) { - Debug("circuit-prop") << "bIFF4" << endl; - assign(in[0], !assignment(in[1]), changed); + if (isAssigned(parent)) { + if (child == parent[0]) { + if (getAssignment(parent)) { + // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b) + assignAndEnqueue(parent[1], childAssignment); + } else { + // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b) + assignAndEnqueue(parent[1], !childAssignment); + } + } else { + Assert(child == parent[1]); + if (getAssignment(parent)) { + // IFF x y = b: if IFF is assigned to TRUE, assign(x = b) + assignAndEnqueue(parent[0], childAssignment); + } else { + // IFF x y = b y: if IFF is assigned to TRUE, assign(x = !b) + assignAndEnqueue(parent[0], !childAssignment); + } + } } } break; case kind::IMPLIES: - if(polarity) { - if(isAssignedTo(in[0], true)) { - // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE) - Debug("circuit-prop") << "bIMPLIES1" << endl; - assign(in[1], true, changed); + if (isAssigned(parent[0]) && isAssigned(parent[1])) { + // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2)) + assignAndEnqueue(parent, !getAssignment(parent[0]) || getAssignment(parent[1])); + } else { + if (child == parent[0] && childAssignment && isAssignedTo(parent, true)) { + // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE) + assignAndEnqueue(parent[1], true); } - if(isAssignedTo(in[1], false)) { - // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) - Debug("circuit-prop") << "bIMPLIES2" << endl; - assign(in[0], false, changed); + if (child == parent[1] && !childAssignment && isAssignedTo(parent, true)) { + // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE) + assignAndEnqueue(parent[0], false); } - } else { - // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE) - Debug("circuit-prop") << "bIMPLIES3" << endl; - assign(in[0], true, changed); - assign(in[1], false, changed); + // Note that IMPLIES == FALSE doesn't need any cases here + // because if that assignment has been done, we've already + // propagated all the children (in back-propagation). } break; case kind::XOR: - if(polarity) { - if(isAssigned(in[0])) { - // XOR x y = TRUE, and x assigned, assign(y = !assignment(x)) - Debug("circuit-prop") << "bXOR1" << endl; - assign(in[1], !assignment(in[0]), changed); - } else if(isAssigned(in[1])) { - // XOR x y = TRUE, and y assigned, assign(x = !assignment(y)) - Debug("circuit-prop") << "bXOR2" << endl; - assign(in[0], !assignment(in[1]), changed); - } - } else { - if(isAssigned(in[0])) { - // XOR x y = FALSE, and x assigned, assign(y = assignment(x)) - Debug("circuit-prop") << "bXOR3" << endl; - assign(in[1], assignment(in[0]), changed); - } else if(isAssigned(in[1])) { - // XOR x y = FALSE, and y assigned, assign(x = assignment(y)) - Debug("circuit-prop") << "bXOR4" << endl; - assign(in[0], assignment(in[1]), changed); + if (isAssigned(parent)) { + if (child == parent[0]) { + // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR) + assignAndEnqueue(parent[1], childAssignment != getAssignment(parent)); + } else { + Assert(child == parent[1]); + // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR)) + assignAndEnqueue(parent[0], childAssignment != getAssignment(parent)); } } - break; - case kind::CONST_BOOLEAN: - // nothing to do + if (isAssigned(parent[0]) && isAssigned(parent[1])) { + assignAndEnqueue(parent, getAssignment(parent[0]) != getAssignment(parent[1])); + } break; default: - Unhandled(k); + Unhandled(); } - Debug("circuit-prop") << pop; } } +bool CircuitPropagator::propagate() { -void CircuitPropagator::propagateForward(TNode child, bool polarity, vector<TNode>& changed) { - if(!isPropagatedForward(child)) { - IndentedScope(Debug("circuit-prop")); - Debug("circuit-prop") << "propagateForward (" << polarity << "): " << child << endl; - std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>::const_iterator iter = d_backEdges.find(child); - if(d_backEdges.find(child) == d_backEdges.end()) { - Debug("circuit-prop") << "no backedges, must be ROOT?: " << child << endl; - return; - } - const vector<TNode>& uses = (*iter).second; - setPropagatedForward(child); - for(vector<TNode>::const_iterator useIter = uses.begin(), useIter_end = uses.end(); useIter != useIter_end; ++useIter) { - TNode in = *useIter; // this is the outer node - Debug("circuit-prop") << "considering use: " << in << endl; - IndentedScope(Debug("circuit-prop")); - // forward rules - switch(Kind k = in.getKind()) { - case kind::AND: - if(polarity) { - TNode::iterator holdout; - holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, true))); - if(holdout == in.end()) { // all children are assigned TRUE - // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE) - Debug("circuit-prop") << "fAND1" << endl; - assign(in, true, changed); - } else if(isAssignedTo(in, false)) {// the AND is FALSE - // is the holdout unique ? - TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, true))); - if(other == in.end()) { // the holdout is unique - // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE) - Debug("circuit-prop") << "fAND2" << endl; - assign(*holdout, false, changed); - } - } - } else { - // AND ...(x=FALSE)...: assign(AND = FALSE) - Debug("circuit-prop") << "fAND3" << endl; - assign(in, false, changed); - } - break; - case kind::OR: - if(polarity) { - // OR ...(x=TRUE)...: assign(OR = TRUE) - Debug("circuit-prop") << "fOR1" << endl; - assign(in, true, changed); - } else { - TNode::iterator holdout; - holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, false))); - if(holdout == in.end()) { // all children are assigned FALSE - // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE) - Debug("circuit-prop") << "fOR2" << endl; - assign(in, false, changed); - } else if(isAssignedTo(in, true)) {// the OR is TRUE - // is the holdout unique ? - TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, false))); - if(other == in.end()) { // the holdout is unique - // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE) - Debug("circuit-prop") << "fOR3" << endl; - assign(*holdout, true, changed); - } - } - } - break; - - case kind::NOT: - // NOT (x=b): assign(NOT = !b) - Debug("circuit-prop") << "fNOT" << endl; - assign(in, !polarity, changed); - break; - case kind::ITE: - if(child == in[0]) { - if(polarity) { - if(isAssigned(in[1])) { - // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment) - Debug("circuit-prop") << "fITE1" << endl; - assign(in, assignment(in[1]), changed); - } - } else { - if(isAssigned(in[2])) { - // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment) - Debug("circuit-prop") << "fITE2" << endl; - assign(in, assignment(in[2]), changed); - } - } - } else if(child == in[1]) { - if(isAssignedTo(in[0], true)) { - // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v) - Debug("circuit-prop") << "fITE3" << endl; - assign(in, assignment(in[1]), changed); - } - } else { - Assert(child == in[2]); - if(isAssignedTo(in[0], false)) { - // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v) - Debug("circuit-prop") << "fITE4" << endl; - assign(in, assignment(in[2]), changed); - } - } - break; - case kind::IFF: - if(child == in[0]) { - if(isAssigned(in[1])) { - // IFF (x=b) y: if y is assigned, assign(IFF = (x.assignment <=> y.assignment)) - Debug("circuit-prop") << "fIFF1" << endl; - assign(in, assignment(in[0]) == assignment(in[1]), changed); - } else if(isAssigned(in)) { - // IFF (x=b) y: if IFF is assigned, assign(y = (b <=> IFF.assignment)) - Debug("circuit-prop") << "fIFF2" << endl; - assign(in[1], polarity == assignment(in), changed); - } - } else { - Assert(child == in[1]); - if(isAssigned(in[0])) { - // IFF x (y=b): if x is assigned, assign(IFF = (x.assignment <=> y.assignment)) - Debug("circuit-prop") << "fIFF3" << endl; - assign(in, assignment(in[0]) == assignment(in[1]), changed); - } else if(isAssigned(in)) { - // IFF x (y=b): if IFF is assigned, assign(x = (b <=> IFF.assignment)) - Debug("circuit-prop") << "fIFF4" << endl; - assign(in[0], polarity == assignment(in), changed); - } - } - break; - case kind::IMPLIES: - if(isAssigned(in[0]) && isAssigned(in[1])) { - // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2)) - assign(in, !assignment(in[0]) || assignment(in[1]), changed); - Debug("circuit-prop") << "fIMPLIES1" << endl; - } else { - if(child == in[0] && assignment(in[0]) && isAssignedTo(in, true)) { - // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE) - Debug("circuit-prop") << "fIMPLIES2" << endl; - assign(in[1], true, changed); - } - if(child == in[1] && !assignment(in[1]) && isAssignedTo(in, true)) { - // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE) - Debug("circuit-prop") << "fIMPLIES3" << endl; - assign(in[0], false, changed); - } - // Note that IMPLIES == FALSE doesn't need any cases here - // because if that assignment has been done, we've already - // propagated all the children (in back-propagation). - } - break; - case kind::XOR: - if(isAssigned(in)) { - if(child == in[0]) { - // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR) - Debug("circuit-prop") << "fXOR1" << endl; - assign(in[1], polarity ^ assignment(in), changed); - } else { - Assert(child == in[1]); - // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR)) - Debug("circuit-prop") << "fXOR2" << endl; - assign(in[0], polarity ^ assignment(in), changed); - } - } - if( (child == in[0] && isAssigned(in[1])) || - (child == in[1] && isAssigned(in[0])) ) { - // XOR (x=v) y [with y assigned], assign(XOR = (v ^ assignment(y)) - // XOR x (y=v) [with x assigned], assign(XOR = (assignment(x) ^ v) - Debug("circuit-prop") << "fXOR3" << endl; - assign(in, assignment(in[0]) ^ assignment(in[1]), changed); - } - break; - case kind::CONST_BOOLEAN: - InternalError("Forward-propagating a constant Boolean value makes no sense"); - default: - Unhandled(k); - } - } - } -} + Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl; + for(unsigned i = 0; i < d_propagationQueue.size() && !d_conflict; ++ i) { -bool CircuitPropagator::propagate(TNode in, bool polarity, vector<Node>& newFacts) { - try { - vector<TNode> changed; + // The current node we are propagating + TNode current = d_propagationQueue[i]; + Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " << current << std::endl; + bool assignment = getAssignment(current); + Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl; - Assert(kindToTheoryId(in.getKind()) == THEORY_BOOL); + // Is this an atom + bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.getMetaKind() == kind::metakind::VARIABLE; - Debug("circuit-prop") << "B: " << (polarity ? "" : "~") << in << endl; - propagateBackward(in, polarity, changed); - Debug("circuit-prop") << "F: " << (polarity ? "" : "~") << in << endl; - propagateForward(in, polarity, changed); - - while(!changed.empty()) { - vector<TNode> worklist; - worklist.swap(changed); + // If an atom, add to the list for simplification + if (atom) { + Debug("circuit-prop") << "CircuitPropagator::propagate(): adding to learned: " << (assignment ? (Node)current : current.notNode()) << std::endl; + d_learnedLiterals.push_back(assignment ? (Node)current : current.notNode()); + } - for(vector<TNode>::iterator i = worklist.begin(), i_end = worklist.end(); i != i_end; ++i) { - if(kindToTheoryId((*i).getKind()) != THEORY_BOOL) { - if(assignment(*i)) { - newFacts.push_back(*i); - } else { - newFacts.push_back((*i).notNode()); - } - } else { - Debug("circuit-prop") << "B: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl; - propagateBackward(*i, assignment(*i), changed); - Debug("circuit-prop") << "F: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl; - propagateForward(*i, assignment(*i), changed); - } - } + // Propagate this value to the children (if not an atom or a constant) + if (d_backwardPropagation && !atom && !current.isConst()) { + propagateBackward(current, assignment); + } + // Propagate this value to the parents + if (d_forwardPropagation) { + propagateForward(current, assignment); } - } catch(ConflictException& ce) { - return true; } - return false; + + // No conflict + return d_conflict; } }/* CVC4::theory::booleans namespace */ diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index f9efc20af..73a5be0f8 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -33,6 +33,7 @@ namespace CVC4 { namespace theory { namespace booleans { + /** * The main purpose of the CircuitPropagator class is to maintain the * state of the circuit for subsequent calls to propagate(), so that @@ -40,104 +41,103 @@ namespace booleans { * circuit isn't propagated twice, etc. */ class CircuitPropagator { - const std::vector<TNode>& d_atoms; - const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& d_backEdges; - class ConflictException : Exception { - public: - ConflictException() : Exception("A conflict was found in the CircuitPropagator") { - } - };/* class ConflictException */ +public: + + /** + * Value of a particular node + */ + enum AssignmentStatus { + /** Node is currently unassigned */ + UNASSIGNED = 0, + /** Node is assigned to true */ + ASSIGNED_TO_TRUE, + /** Node is assigned to false */ + ASSIGNED_TO_FALSE, + }; + + /** Invert a set value */ + static inline AssignmentStatus neg(AssignmentStatus value) { + Assert(value != UNASSIGNED); + if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE; + else return ASSIGNED_TO_TRUE; + } + +private: + + /** Back edges from nodes to where they are used */ + typedef std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction> BackEdgesMap; + BackEdgesMap d_backEdges; - enum { - ASSIGNMENT_MASK = 1, - IS_ASSIGNED_MASK = 2, - IS_PROPAGATED_FORWARD_MASK = 4, - IS_PROPAGATED_BACKWARD_MASK = 8 - };/* enum */ + /** The propagation queue */ + std::vector<TNode> d_propagationQueue; + + /** Are we in conflict */ + bool d_conflict; + + /** Map of substitutions */ + std::vector<Node>& d_learnedLiterals; + + /** Nodes that have been attached already (computed forward edges for) */ + // All the nodes we've visited so far + std::hash_set<TNode, TNodeHashFunction> d_seen; /** - * For each Node we care about, we have a 4-bit state: - * Bit 0 (ASSIGNMENT_MASK) is set to indicate the current assignment - * Bit 1 (IS_ASSIGNED_MASK) is set if a value is assigned - * Bit 2 (IS_PROPAGATED_FORWARD) is set to indicate it's been propagated forward - * Bit 2 (IS_PROPAGATED_BACKWARD) is set to indicate it's been propagated backward + * Assignment status of each node. */ - std::hash_map<TNode, unsigned, TNodeHashFunction> d_state; - - /** Assign Node in circuit with the value and add it to the changed vector; note conflicts. */ - void assign(TNode n, bool b, std::vector<TNode>& changed) { - if(n.getMetaKind() == kind::metakind::CONSTANT) { - bool c = n.getConst<bool>(); - if(c != b) { - Debug("circuit-prop") << "while assigning(" << b << "): " << n - << ", constant conflict" << std::endl; - throw ConflictException(); - } else { - Debug("circuit-prop") << "assigning(" << b << "): " << n - << ", nothing to do" << std::endl; + typedef std::hash_map<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap; + AssignmentMap d_state; + + /** + * Assign Node in circuit with the value and add it to the queue; note conflicts. + */ + void assignAndEnqueue(TNode n, bool value) { + + Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl; + + if (n.getKind() == kind::CONST_BOOLEAN) { + // Assigning a constant to the opposite value is dumb + if (value != n.getConst<bool>()) { + d_conflict = true; + return; } - return; } - unsigned& state = d_state[n]; - if((state & IS_ASSIGNED_MASK) != 0) {// if assigned already - if(((state & ASSIGNMENT_MASK) != 0) != b) {// conflict - Debug("circuit-prop") << "while assigning(" << b << "): " << n - << ", got conflicting assignment(" << assignment(n) << "): " - << n << std::endl; - throw ConflictException(); - } else { - Debug("circuit-prop") << "already assigned(" << b << "): " << n << std::endl; + + // Get the current assignement + AssignmentStatus state = d_state[n]; + + if(state != UNASSIGNED) { + // If the node is already assigned we might have a conflict + if(value != (state == ASSIGNED_TO_TRUE)) { + d_conflict = true; } - } else {// if unassigned - Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl; - state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0); - changed.push_back(n); + } else { + // If unassigned, mark it as assigned + d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE; + // Add for further propagation + d_propagationQueue.push_back(n); } } - /** True iff Node is assigned in circuit (either true or false). */ - bool isAssigned(TNode n) { - return (d_state[n] & IS_ASSIGNED_MASK) != 0; - } + /** True iff Node is assigned in circuit (either true or false). */ bool isAssigned(TNode n) const { - std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n); - return i != d_state.end() && ((*i).second & IS_ASSIGNED_MASK) != 0; - } - /** True iff Node is assigned in circuit with the value given. */ - bool isAssignedTo(TNode n, bool b) { - unsigned state = d_state[n]; - return (state & IS_ASSIGNED_MASK) && - (state & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0); + AssignmentMap::const_iterator i = d_state.find(n); + return i != d_state.end() && ((*i).second != UNASSIGNED); } - /** True iff Node is assigned in circuit (either true or false). */ - bool isAssignedTo(TNode n, bool b) const { - std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n); - return i != d_state.end() && - ((*i).second & IS_ASSIGNED_MASK) && - ((*i).second & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0); + + /** True iff Node is assigned to the value. */ + bool isAssignedTo(TNode n, bool value) const { + AssignmentMap::const_iterator i = d_state.find(n); + if (i == d_state.end()) return false; + if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true; + if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true; + return false; } + /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */ - bool assignment(TNode n) { - unsigned state = d_state[n]; - Assert((state & IS_ASSIGNED_MASK) != 0); - return (state & ASSIGNMENT_MASK) != 0; - } - /** Has this node already been propagated forward? */ - bool isPropagatedForward(TNode n) { - return (d_state[n] & IS_PROPAGATED_FORWARD_MASK) != 0; - } - /** Has this node already been propagated backward? */ - bool isPropagatedBackward(TNode n) { - return (d_state[n] & IS_PROPAGATED_BACKWARD_MASK) != 0; - } - /** Mark this node as already having been propagated forward. */ - void setPropagatedForward(TNode n) { - d_state[n] |= IS_PROPAGATED_FORWARD_MASK; - } - /** Mark this node as already having been propagated backward. */ - void setPropagatedBackward(TNode n) { - d_state[n] |= IS_PROPAGATED_BACKWARD_MASK; + bool getAssignment(TNode n) const { + Assert(d_state.find(n) != d_state.end() && d_state.find(n)->second != UNASSIGNED); + return d_state.find(n)->second == ASSIGNED_TO_TRUE; } /** Predicate for use in STL functions. */ @@ -169,33 +169,52 @@ class CircuitPropagator { };/* class IsAssignedTo */ /** - * Propagate new information (in = polarity) forward in circuit to + * Compute the map from nodes to the nodes that use it. + */ + void computeBackEdges(TNode node); + + /** + * Propagate new information forward in circuit to * the parents of "in". */ - void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts); + void propagateForward(TNode child, bool assignment); + /** - * Propagate new information (in = polarity) backward in circuit to + * Propagate new information backward in circuit to * the children of "in". */ - void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts); + void propagateBackward(TNode parent, bool assignment); + + /** Whether to perform forward propagation */ + bool d_forwardPropagation; + /** Whether to perform backward propagation */ + bool d_backwardPropagation; + /** Whether to perform expensive propagations */ + bool d_expensivePropagation; public: /** * Construct a new CircuitPropagator with the given atoms and backEdges. */ - CircuitPropagator(const std::vector<TNode>& atoms, const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& backEdges) - : d_atoms(atoms), - d_backEdges(backEdges) { + CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true, bool enableExpensive = true) : + d_conflict(false), + d_learnedLiterals(outLearnedLiterals), + d_forwardPropagation(enableForward), + d_backwardPropagation(enableBackward), + d_expensivePropagation(enableExpensive) + { } + /** Assert for propagation */ + void assert(TNode assertion); + /** - * Propagate new information (in == polarity) through the circuit - * propagator. New information discovered by the propagator are put - * in the (output-only) newFacts vector. + * Propagate through the asserted circuit propagator. New information discovered by the propagator + * are put in the subsitutions vector used in construction. * * @return true iff conflict found */ - bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT; + bool propagate() CVC4_WARN_UNUSED_RESULT; };/* class CircuitPropagator */ diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 836022bc2..01185281a 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -97,134 +97,29 @@ Node TheoryBool::getValue(TNode n) { } } -static void -findAtoms(TNode in, vector<TNode>& atoms, - hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) { - Kind k CVC4_UNUSED = in.getKind(); - Assert(kindToTheoryId(k) == THEORY_BOOL); - - stack< pair<TNode, TNode::iterator> > trail; - hash_set<TNode, TNodeHashFunction> seen; - trail.push(make_pair(in, in.begin())); - - while(!trail.empty()) { - pair<TNode, TNode::iterator>& pr = trail.top(); - Debug("simplify") << "looking at: " << pr.first << endl; - if(pr.second == pr.first.end()) { - trail.pop(); - } else { - if(pr.second == pr.first.begin()) { - Debug("simplify") << "first visit: " << pr.first << endl; - // first time we've visited this node? - if(seen.find(pr.first) == seen.end()) { - Debug("simplify") << "+ haven't seen it yet." << endl; - seen.insert(pr.first); - } else { - Debug("simplify") << "+ saw it before." << endl; - trail.pop(); - continue; - } - } - TNode n = *pr.second++; - if(seen.find(n) == seen.end()) { - Debug("simplify") << "back edge " << n << " to " << pr.first << endl; - backEdges[n].push_back(pr.first); - Kind nk = n.getKind(); - if(kindToTheoryId(nk) == THEORY_BOOL) { - trail.push(make_pair(n, n.begin())); - } else { - Debug("simplify") << "atom: " << n << endl; - atoms.push_back(n); - } - } - } - } -} +Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitutions) { -Node TheoryBool::simplify(TNode in, Substitutions& outSubstitutions) { - const unsigned prev = outSubstitutions.size(); - - if(kindToTheoryId(in.getKind()) != THEORY_BOOL) { - Assert(in.getMetaKind() == kind::metakind::VARIABLE && - in.getType().isBoolean()); - return in; + if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) { + // If we get a false literal, we're in conflict + return SOLVE_STATUS_CONFLICT; } - // form back edges and atoms - vector<TNode> atoms; - hash_map<TNode, vector<TNode>, TNodeHashFunction> backEdges; - Debug("simplify") << "finding atoms..." << endl << push; - findAtoms(in, atoms, backEdges); - Debug("simplify") << pop << "done finding atoms..." << endl; - - hash_map<TNode, Node, TNodeHashFunction> simplified; - - vector<Node> newFacts; - CircuitPropagator circuit(atoms, backEdges); - Debug("simplify") << "propagate..." << endl; - if(circuit.propagate(in, true, newFacts)) { - Notice() << "Found a conflict in nonclausal Boolean reasoning" << endl; - return NodeManager::currentNM()->mkConst(false); - } - Debug("simplify") << "done w/ propagate..." << endl; - - for(vector<Node>::iterator i = newFacts.begin(), i_end = newFacts.end(); i != i_end; ++i) { - TNode a = *i; - if(a.getKind() == kind::NOT) { - if(a[0].getMetaKind() == kind::metakind::VARIABLE ) { - Debug("simplify") << "found bool unit ~" << a[0] << "..." << endl; - outSubstitutions.push_back(make_pair(a[0], NodeManager::currentNM()->mkConst(false))); - } else if(kindToTheoryId(a[0].getKind()) != THEORY_BOOL) { - Debug("simplify") << "simplifying: " << a << endl; - simplified[a] = d_valuation.simplify(a, outSubstitutions); - Debug("simplify") << "done simplifying, got: " << simplified[a] << endl; - } + // Add the substitution from the variable to it's value + if (in.getKind() == kind::NOT) { + if (in[0].getKind() == kind::VARIABLE) { + outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false)); } else { - if(a.getMetaKind() == kind::metakind::VARIABLE) { - Debug("simplify") << "found bool unit " << a << "..." << endl; - outSubstitutions.push_back(make_pair(a, NodeManager::currentNM()->mkConst(true))); - } else if(kindToTheoryId(a.getKind()) != THEORY_BOOL) { - Debug("simplify") << "simplifying: " << a << endl; - simplified[a] = d_valuation.simplify(a, outSubstitutions); - Debug("simplify") << "done simplifying, got: " << simplified[a] << endl; - } + return SOLVE_STATUS_UNSOLVED; } - } - - Debug("simplify") << "substituting in root..." << endl; - Node n = in.substitute(outSubstitutions.begin(), outSubstitutions.end()); - Debug("simplify") << "got: " << n << endl; - if(Debug.isOn("simplify")) { - Debug("simplify") << "new substitutions:" << endl; - copy(outSubstitutions.begin() + prev, outSubstitutions.end(), - ostream_iterator< pair<TNode, TNode> >(Debug("simplify"), "\n")); - Debug("simplify") << "done." << endl; - } - if(outSubstitutions.size() > prev) { - NodeBuilder<> b(kind::AND); - b << n; - for(Substitutions::iterator i = outSubstitutions.begin() + prev, - i_end = outSubstitutions.end(); - i != i_end; - ++i) { - if((*i).first.getType().isBoolean()) { - if((*i).second.getMetaKind() == kind::metakind::CONSTANT) { - if((*i).second.getConst<bool>()) { - b << (*i).first; - } else { - b << BooleanSimplification::negate((*i).first); - } - } else { - b << (*i).first.iffNode((*i).second); - } - } else { - b << (*i).first.eqNode((*i).second); - } + } else { + if (in.getKind() == kind::VARIABLE) { + outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true)); + } else { + return SOLVE_STATUS_UNSOLVED; } - n = b; } - Debug("simplify") << "final boolean simplification returned: " << n << endl; - return n; + + return SOLVE_STATUS_SOLVED; } diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 40bbd3308..ce9938b10 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -36,7 +36,7 @@ public: Node getValue(TNode n); - Node simplify(TNode in, Substitutions& outSubstitutions); + SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions); std::string identify() const { return std::string("TheoryBool"); } };/* class TheoryBool */ diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index c1be3b906..18aa71667 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -36,7 +36,31 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]); break; } - case kind::IFF: { + case kind::OR: { + if (n.getNumChildren() == 2) { + if (n[0] == tt || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); + if (n[0] == ff) return RewriteResponse(REWRITE_AGAIN, n[1]); + if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0]); + } + break; + } + case kind::AND: { + if (n.getNumChildren() == 2) { + if (n[0] == ff || n[1] == ff) return RewriteResponse(REWRITE_DONE, ff); + if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); + if (n[1] == tt) return RewriteResponse(REWRITE_AGAIN, n[0]); + } + break; + } + case kind::IMPLIES: { + if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); + if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff); + if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); + if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + break; + } + case kind::IFF: + case kind::EQUAL: { // rewrite simple cases of IFF if(n[0] == tt) { // IFF true x @@ -62,10 +86,35 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { } break; } + case kind::XOR: { + // rewrite simple cases of XOR + if(n[0] == tt) { + // XOR true x + return RewriteResponse(REWRITE_AGAIN, n[1].notNode()); + } else if(n[1] == tt) { + // XCR x true + return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + } else if(n[0] == ff) { + // XOR false x + return RewriteResponse(REWRITE_AGAIN, n[1]); + } else if(n[1] == ff) { + // XOR x false + return RewriteResponse(REWRITE_AGAIN, n[0]); + } else if(n[0] == n[1]) { + // XOR x x + return RewriteResponse(REWRITE_DONE, ff); + } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) { + // XOR (NOT x) x + return RewriteResponse(REWRITE_DONE, tt); + } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { + // XOR x (NOT x) + return RewriteResponse(REWRITE_DONE, tt); + } + break; + } case kind::ITE: { // non-Boolean-valued ITEs should have been removed in place of // a variable - Assert(n.getType().isBoolean()); // rewrite simple cases of ITE if(n[0] == tt) { // ITE true x y |