From: Andrew Reynolds Date: Thu, 27 Feb 2020 01:11:31 +0000 (-0600) Subject: Initial work towards -Wshadow (#3817) X-Git-Tag: cvc5-1.0.0~3589 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d41d2a817f884e0f6c8d5cb3b87b4298bc1b56f5;p=cvc5.git Initial work towards -Wshadow (#3817) --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4e5f4604e..02fbbc42c 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1832,9 +1832,9 @@ DatatypeDecl::DatatypeDecl(const Solver* s, bool isCoDatatype) { std::vector tparams; - for (const Sort& s : params) + for (const Sort& p : params) { - tparams.push_back(*s.d_type); + tparams.push_back(*p.d_type); } d_dtype = std::shared_ptr( new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype)); diff --git a/src/expr/node.h b/src/expr/node.h index d02cbcefd..616e256ab 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1363,14 +1363,15 @@ NodeTemplate::substitute(TNode node, TNode replacement, nb << getOperator().substitute(node, replacement, cache); } } - for(const_iterator i = begin(), - iend = end(); - i != iend; - ++i) { - if(*i == node) { + for (const_iterator it = begin(), iend = end(); it != iend; ++it) + { + if (*it == node) + { nb << replacement; - } else { - nb << (*i).substitute(node, replacement, cache); + } + else + { + nb << (*it).substitute(node, replacement, cache); } } @@ -1429,13 +1430,10 @@ NodeTemplate::substitute(Iterator1 nodesBegin, replacementsBegin, replacementsEnd, cache); } - for(const_iterator i = begin(), - iend = end(); - i != iend; - ++i) { - nb << (*i).substitute(nodesBegin, nodesEnd, - replacementsBegin, replacementsEnd, - cache); + for (const_iterator it = begin(), iend = end(); it != iend; ++it) + { + nb << (*it).substitute( + nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache); } Node n = nb; cache[*this] = n; @@ -1480,11 +1478,9 @@ NodeTemplate::substitute(Iterator substitutionsBegin, // push the operator nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache); } - for(const_iterator i = begin(), - iend = end(); - i != iend; - ++i) { - nb << (*i).substitute(substitutionsBegin, substitutionsEnd, cache); + for (const_iterator it = begin(), iend = end(); it != iend; ++it) + { + nb << (*it).substitute(substitutionsBegin, substitutionsEnd, cache); } Node n = nb; cache[*this] = n; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 017ffe3dd..14eb9064c 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -798,12 +798,10 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin, // push the operator nb << TypeNode(d_nv->d_children[0]); } - for(TypeNode::const_iterator i = begin(), - iend = end(); - i != iend; - ++i) { - nb << (*i).substitute(typesBegin, typesEnd, - replacementsBegin, replacementsEnd, cache); + for (TypeNode::const_iterator it = begin(), iend = end(); it != iend; ++it) + { + nb << (*it).substitute( + typesBegin, typesEnd, replacementsBegin, replacementsEnd, cache); } TypeNode tn = nb.constructTypeNode(); cache[*this] = tn; diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 150e41b8f..372df90ce 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -39,9 +39,9 @@ namespace { // TODO: clean this up struct intToBV_stack_element { - TNode node; - bool children_added; - intToBV_stack_element(TNode node) : node(node), children_added(false) {} + TNode d_node; + bool d_children_added; + intToBV_stack_element(TNode node) : d_node(node), d_children_added(false) {} }; /* struct intToBV_stack_element */ Node intToBVMakeBinary(TNode n, NodeMap& cache) @@ -54,7 +54,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) { // The current node we are processing intToBV_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; + TNode current = stackHead.d_node; NodeMap::iterator find = cache.find(current); if (find != cache.end()) @@ -62,7 +62,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) toVisit.pop_back(); continue; } - if (stackHead.children_added) + if (stackHead.d_children_added) { // Children have been processed, so rebuild this node Node result; @@ -99,7 +99,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) // Mark that we have added the children if any if (current.getNumChildren() > 0) { - stackHead.children_added = true; + stackHead.d_children_added = true; // We need to add the children for (TNode::iterator child_it = current.begin(); child_it != current.end(); @@ -138,7 +138,7 @@ Node intToBV(TNode n, NodeMap& cache) { // The current node we are processing intToBV_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; + TNode current = stackHead.d_node; // If node is already in the cache we're done, pop from the stack NodeMap::iterator find = cache.find(current); @@ -150,7 +150,7 @@ Node intToBV(TNode n, NodeMap& cache) // Not yet substituted, so process NodeManager* nm = NodeManager::currentNM(); - if (stackHead.children_added) + if (stackHead.d_children_added) { // Children have been processed, so rebuild this node vector children; @@ -245,7 +245,7 @@ Node intToBV(TNode n, NodeMap& cache) // Mark that we have added the children if any if (current.getNumChildren() > 0) { - stackHead.children_added = true; + stackHead.d_children_added = true; // We need to add the children for (TNode::iterator child_it = current.begin(); child_it != current.end(); diff --git a/src/smt_util/node_visitor.h b/src/smt_util/node_visitor.h index 58070c0b2..47ed6eff8 100644 --- a/src/smt_util/node_visitor.h +++ b/src/smt_util/node_visitor.h @@ -59,13 +59,15 @@ public: */ struct stack_element { /** The node to be visited */ - TNode node; + TNode d_node; /** The parent of the node */ - TNode parent; + TNode d_parent; /** Have the children been queued up for visitation */ - bool children_added; + bool d_childrenAdded; stack_element(TNode node, TNode parent) - : node(node), parent(parent), children_added(false) {} + : d_node(node), d_parent(parent), d_childrenAdded(false) + { + } };/* struct preprocess_stack_element */ /** @@ -84,20 +86,24 @@ public: while (!toVisit.empty()) { stack_element& stackHead = toVisit.back(); // The current node we are processing - TNode current = stackHead.node; - TNode parent = stackHead.parent; + TNode current = stackHead.d_node; + TNode parent = stackHead.d_parent; if (visitor.alreadyVisited(current, parent)) { // If already visited, we're done toVisit.pop_back(); - } else if (stackHead.children_added) { + } + else if (stackHead.d_childrenAdded) + { // Call the visitor visitor.visit(current, parent); // Done with this node, remove from the stack toVisit.pop_back(); - } else { + } + else + { // Mark that we have added the children - stackHead.children_added = true; + stackHead.d_childrenAdded = true; // We need to add the children for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { TNode childNode = *child_it; diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index d8dd2cf58..4f93ba745 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -639,14 +639,16 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ RewriteResponse ArithRewriter::postRewrite(TNode t){ if(isTerm(t)){ RewriteResponse response = postRewriteTerm(t); - if(Debug.isOn("arith::rewriter") && response.status == REWRITE_DONE) { - Polynomial::parsePolynomial(response.node); + if (Debug.isOn("arith::rewriter") && response.d_status == REWRITE_DONE) + { + Polynomial::parsePolynomial(response.d_node); } return response; }else if(isAtom(t)){ RewriteResponse response = postRewriteAtom(t); - if(Debug.isOn("arith::rewriter") && response.status == REWRITE_DONE) { - Comparison::parseNormalForm(response.node); + if (Debug.isOn("arith::rewriter") && response.d_status == REWRITE_DONE) + { + Comparison::parseNormalForm(response.d_node); } return response; }else{ diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 94c925131..2d530d602 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -645,7 +645,7 @@ void NonlinearExtension::getAssertions(std::vector& assertions) { nassertions++; const Assertion& assertion = *it; - Node lit = assertion.assertion; + Node lit = assertion.d_assertion; init_assertions.insert(lit); // check for concrete bounds bool pol = lit.getKind() != NOT; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 534a019c3..d721b7e7a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1327,14 +1327,15 @@ void TheoryArrays::check(Effort e) { { // Get all the assertions Assertion assertion = get(); - TNode fact = assertion.assertion; + TNode fact = assertion.d_assertion; Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl; bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; - if (!assertion.isPreregistered) { + if (!assertion.d_isPreregistered) + { if (atom.getKind() == kind::EQUAL) { if (!d_equalityEngine.hasTerm(atom[0])) { Assert(atom[0].isConst()); diff --git a/src/theory/assertion.cpp b/src/theory/assertion.cpp index 4f428e85c..97b3dcbbb 100644 --- a/src/theory/assertion.cpp +++ b/src/theory/assertion.cpp @@ -20,7 +20,7 @@ namespace CVC4 { namespace theory { std::ostream& operator<<(std::ostream& out, const Assertion& a) { - return out << a.assertion; + return out << a.d_assertion; } }/* CVC4::theory namespace */ diff --git a/src/theory/assertion.h b/src/theory/assertion.h index 863a7e893..797ff3372 100644 --- a/src/theory/assertion.h +++ b/src/theory/assertion.h @@ -28,19 +28,21 @@ namespace theory { /** Information about an assertion for the theories. */ struct Assertion { /** The assertion expression. */ - const Node assertion; + const Node d_assertion; /** Has this assertion been preregistered with this theory. */ - const bool isPreregistered; + const bool d_isPreregistered; Assertion(TNode assertion, bool isPreregistered) - : assertion(assertion), isPreregistered(isPreregistered) {} + : d_assertion(assertion), d_isPreregistered(isPreregistered) + { + } /** Convert the assertion to a TNode. */ - operator TNode() const { return assertion; } + operator TNode() const { return d_assertion; } /** Convert the assertion to a Node. */ - operator Node() const { return assertion; } + operator Node() const { return d_assertion; } }; /* struct Assertion */ diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp index 6054ac603..821c2384c 100644 --- a/src/theory/atom_requests.cpp +++ b/src/theory/atom_requests.cpp @@ -65,15 +65,13 @@ void AtomRequests::add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toT d_triggerToRequestMap[triggerAtom] = index; } -bool AtomRequests::atom_iterator::done() const { - return index == null_index; -} +bool AtomRequests::atom_iterator::done() const { return d_index == null_index; } void AtomRequests::atom_iterator::next() { - index = requests.d_requests[index].previous; + d_index = d_requests.d_requests[d_index].d_previous; } const AtomRequests::Request& AtomRequests::atom_iterator::get() const { - return requests.d_requests[index].request; + return d_requests.d_requests[d_index].d_request; } diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h index 6a3ffe5e9..b96b042af 100644 --- a/src/theory/atom_requests.h +++ b/src/theory/atom_requests.h @@ -34,24 +34,18 @@ public: /** Which atom and where to send it */ struct Request { /** Atom */ - Node atom; + Node d_atom; /** Where to send it */ - theory::TheoryId toTheory; + theory::TheoryId d_toTheory; - Request(TNode atom, theory::TheoryId toTheory) - : atom(atom), toTheory(toTheory) {} - Request() - : toTheory(theory::THEORY_LAST) - {} + Request(TNode a, theory::TheoryId tt) : d_atom(a), d_toTheory(tt) {} + Request() : d_toTheory(theory::THEORY_LAST) {} bool operator == (const Request& other) const { - return atom == other.atom && toTheory == other.toTheory; - } - - size_t hash() const { - return atom.getId(); + return d_atom == other.d_atom && d_toTheory == other.d_toTheory; } + size_t hash() const { return d_atom.getId(); } }; AtomRequests(context::Context* context); @@ -66,11 +60,14 @@ public: typedef size_t element_index; class atom_iterator { - const AtomRequests& requests; - element_index index; + const AtomRequests& d_requests; + element_index d_index; friend class AtomRequests; atom_iterator(const AtomRequests& requests, element_index start) - : requests(requests), index(start) {} + : d_requests(requests), d_index(start) + { + } + public: /** Is this iterator done */ bool done() const; @@ -97,13 +94,11 @@ private: struct Element { /** Current request */ - Request request; + Request d_request; /** Previous request */ - element_index previous; + element_index d_previous; - Element(const Request& request, element_index previous) - : request(request), previous(previous) - {} + Element(const Request& r, element_index p) : d_request(r), d_previous(p) {} }; /** We index the requests in this vector, it's a list */ diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 1c5eab364..ca22467d4 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -169,7 +169,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { } if (!done) { RewriteResponse ret = flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt); - Debug("bool-flatten") << n << ": " << ret.node << std::endl; + Debug("bool-flatten") << n << ": " << ret.d_node << std::endl; return ret; } break; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 033a50916..94fc1e34c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -338,7 +338,7 @@ void TheoryBV::check(Effort e) std::vector assertions; while (!done()) { - TNode fact = get().assertion; + TNode fact = get().d_assertion; Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM); assertions.push_back(fact); d_eagerSolver->assertFormula(fact[0]); @@ -369,7 +369,7 @@ void TheoryBV::check(Effort e) } while (!done()) { - TNode fact = get().assertion; + TNode fact = get().d_assertion; checkForLemma(fact); diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 153f785ca..a7638325c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -1382,12 +1382,11 @@ bool RewriteRule::applies(TNode node) { if (node[i].getKind() == kind::CONST_BITVECTOR) { BitVector constant = node[i].getConst(); // we do not apply the rule if the constant is all 0s or all 1s - if (constant == BitVector(utils::getSize(node), 0u)) - return false; - - for (unsigned i = 0; i < constant.getSize(); ++i) { - if (!constant.isBitSet(i)) - return true; + if (constant == BitVector(utils::getSize(node), 0u)) return false; + + for (unsigned j = 0, csize = constant.getSize(); j < csize; ++j) + { + if (!constant.isBitSet(j)) return true; } return false; } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 282ae2e27..6a04d6e4e 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -33,18 +33,22 @@ TheoryBVRewriter::TheoryBVRewriter() { initializeRewrites(); } RewriteResponse TheoryBVRewriter::preRewrite(TNode node) { RewriteResponse res = d_rewriteTable[node.getKind()](node, true); - if(res.node != node) { + if (res.d_node != node) + { Debug("bitvector-rewrite") << "TheoryBV::preRewrite " << node << std::endl; - Debug("bitvector-rewrite") << "TheoryBV::preRewrite to " << res.node << std::endl; + Debug("bitvector-rewrite") + << "TheoryBV::preRewrite to " << res.d_node << std::endl; } return res; } RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { RewriteResponse res = d_rewriteTable[node.getKind()](node, false); - if(res.node!= node) { + if (res.d_node != node) + { Debug("bitvector-rewrite") << "TheoryBV::postRewrite " << node << std::endl; - Debug("bitvector-rewrite") << "TheoryBV::postRewrite to " << res.node << std::endl; + Debug("bitvector-rewrite") + << "TheoryBV::postRewrite to " << res.d_node << std::endl; } return res; } diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h index 55851c1a4..f17f67ee0 100644 --- a/src/theory/care_graph.h +++ b/src/theory/care_graph.h @@ -31,22 +31,25 @@ namespace theory { * A (ordered) pair of terms a theory cares about. */ struct CarePair { - const TNode a, b; - const TheoryId theory; + const TNode d_a, d_b; + const TheoryId d_theory; CarePair(TNode a, TNode b, TheoryId theory) - : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {} + : d_a(a < b ? a : b), d_b(a < b ? b : a), d_theory(theory) + { + } bool operator==(const CarePair& other) const { - return (theory == other.theory) && (a == other.a) && (b == other.b); + return (d_theory == other.d_theory) && (d_a == other.d_a) + && (d_b == other.d_b); } bool operator<(const CarePair& other) const { - if (theory < other.theory) return true; - if (theory > other.theory) return false; - if (a < other.a) return true; - if (a > other.a) return false; - return b < other.b; + if (d_theory < other.d_theory) return true; + if (d_theory > other.d_theory) return false; + if (d_a < other.d_a) return true; + if (d_a > other.d_a) return false; + return d_b < other.d_b; } }; /* struct CarePair */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index cf07bc0c1..141c9476f 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -154,7 +154,7 @@ void TheoryDatatypes::check(Effort e) { while(!done() && !d_conflict) { // Get all the assertions Assertion assertion = get(); - TNode fact = assertion.assertion; + TNode fact = assertion.d_assertion; Trace("datatypes-assert") << "Assert " << fact << std::endl; TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 788545b3c..2632a6f38 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -962,7 +962,7 @@ void TheoryFp::check(Effort level) { while (!done() && !d_conflict) { // Get all the assertions Assertion assertion = get(); - TNode fact = assertion.assertion; + TNode fact = assertion.d_assertion; Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl; diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 8854b400d..338c1c871 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -46,9 +46,12 @@ namespace rewrite { RewriteResponse then (TNode node, bool isPreRewrite) { RewriteResponse result(first(node, isPreRewrite)); - if (result.status == REWRITE_DONE) { - return second(result.node, isPreRewrite); - } else { + if (result.d_status == REWRITE_DONE) + { + return second(result.d_node, isPreRewrite); + } + else + { return result; } } @@ -1268,9 +1271,11 @@ TheoryFpRewriter::TheoryFpRewriter() RewriteResponse TheoryFpRewriter::preRewrite(TNode node) { Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl; RewriteResponse res = d_preRewriteTable[node.getKind()](node, true); - if (res.node != node) { + if (res.d_node != node) + { Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl; - Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after " << res.node << std::endl; + Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after " + << res.d_node << std::endl; } return res; } @@ -1301,46 +1306,52 @@ TheoryFpRewriter::TheoryFpRewriter() RewriteResponse TheoryFpRewriter::postRewrite(TNode node) { Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl; RewriteResponse res = d_postRewriteTable[node.getKind()](node, false); - if (res.node != node) { + if (res.d_node != node) + { Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl; - Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after " << res.node << std::endl; + Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after " + << res.d_node << std::endl; } - if (res.status == REWRITE_DONE) { + if (res.d_status == REWRITE_DONE) + { bool allChildrenConst = true; bool apartFromRoundingMode = false; bool apartFromPartiallyDefinedArgument = false; - for (Node::const_iterator i = res.node.begin(); - i != res.node.end(); - ++i) { - - if ((*i).getMetaKind() != kind::metakind::CONSTANT) { + for (Node::const_iterator i = res.d_node.begin(); i != res.d_node.end(); + ++i) + { + if ((*i).getMetaKind() != kind::metakind::CONSTANT) { if ((*i).getType().isRoundingMode() && !apartFromRoundingMode) { apartFromRoundingMode = true; - } else if ((res.node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL || - res.node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL || - res.node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL || - res.node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL || - res.node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL) && - ((*i).getType().isBitVector() || - (*i).getType().isReal()) && - !apartFromPartiallyDefinedArgument) { - apartFromPartiallyDefinedArgument = true; - } else { - allChildrenConst = false; + } + else if ((res.d_node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL + || res.d_node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL + || res.d_node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL + || res.d_node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL + || res.d_node.getKind() + == kind::FLOATINGPOINT_TO_REAL_TOTAL) + && ((*i).getType().isBitVector() || (*i).getType().isReal()) + && !apartFromPartiallyDefinedArgument) + { + apartFromPartiallyDefinedArgument = true; + } + else + { + allChildrenConst = false; break; - } - } + } + } } if (allChildrenConst) { RewriteStatus rs = REWRITE_DONE; // This is a bit messy because - Node rn = res.node; // RewriteResponse is too functional.. + Node rn = res.d_node; // RewriteResponse is too functional.. - if (apartFromRoundingMode) { - if (!(res.node.getKind() == kind::EQUAL) + if (apartFromRoundingMode) { + if (!(res.d_node.getKind() == kind::EQUAL) && // Avoid infinite recursion... - !(res.node.getKind() == kind::ROUNDINGMODE_BITBLAST)) + !(res.d_node.getKind() == kind::ROUNDINGMODE_BITBLAST)) { // Don't eliminate the bit-blast // We are close to being able to constant fold this // and in many cases the rounding mode really doesn't matter. @@ -1354,16 +1365,15 @@ TheoryFpRewriter::TheoryFpRewriter() Node RTN(nm->mkConst(roundTowardNegative)); Node RTP(nm->mkConst(roundTowardZero)); - TNode RM(res.node[0]); - - Node wRNE(res.node.substitute(RM, TNode(RNE))); - Node wRNA(res.node.substitute(RM, TNode(RNA))); - Node wRTZ(res.node.substitute(RM, TNode(RTZ))); - Node wRTN(res.node.substitute(RM, TNode(RTN))); - Node wRTP(res.node.substitute(RM, TNode(RTP))); + TNode RM(res.d_node[0]); + Node wRNE(res.d_node.substitute(RM, TNode(RNE))); + Node wRNA(res.d_node.substitute(RM, TNode(RNA))); + Node wRTZ(res.d_node.substitute(RM, TNode(RTZ))); + Node wRTN(res.d_node.substitute(RM, TNode(RTN))); + Node wRTP(res.d_node.substitute(RM, TNode(RTP))); - rs = REWRITE_AGAIN_FULL; + rs = REWRITE_AGAIN_FULL; rn = nm->mkNode(kind::ITE, nm->mkNode(kind::EQUAL, RM, RNE), wRNE, @@ -1380,19 +1390,24 @@ TheoryFpRewriter::TheoryFpRewriter() } } else { RewriteResponse tmp = - d_constantFoldTable[res.node.getKind()](res.node, false); - rs = tmp.status; - rn = tmp.node; - } + d_constantFoldTable[res.d_node.getKind()](res.d_node, false); + rs = tmp.d_status; + rn = tmp.d_node; + } RewriteResponse constRes(rs,rn); - if (constRes.node != res.node) { - Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before constant fold " << res.node << std::endl; - Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after constant fold " << constRes.node << std::endl; - } - - return constRes; + if (constRes.d_node != res.d_node) + { + Debug("fp-rewrite") + << "TheoryFpRewriter::postRewrite(): before constant fold " + << res.d_node << std::endl; + Debug("fp-rewrite") + << "TheoryFpRewriter::postRewrite(): after constant fold " + << constRes.d_node << std::endl; + } + + return constRes; } } diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h index 790e9d83d..732eeab0a 100644 --- a/src/theory/fp/theory_fp_rewriter.h +++ b/src/theory/fp/theory_fp_rewriter.h @@ -42,7 +42,7 @@ class TheoryFpRewriter : public TheoryRewriter Node rewriteEquality(TNode equality) { // often this will suffice - return postRewrite(equality).node; + return postRewrite(equality).d_node; } protected: diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index 12ac1e802..f92738bcb 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -62,10 +62,11 @@ void TheoryIdl::check(Effort level) { // Get the next assertion Assertion assertion = get(); - Debug("theory::idl") << "TheoryIdl::check(): processing " << assertion.assertion << std::endl; + Debug("theory::idl") << "TheoryIdl::check(): processing " + << assertion.d_assertion << std::endl; // Convert the assertion into the internal representation - IDLAssertion idlAssertion(assertion.assertion); + IDLAssertion idlAssertion(assertion.d_assertion); Debug("theory::idl") << "TheoryIdl::check(): got " << idlAssertion << std::endl; if (idlAssertion.ok()) { diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 4f3ce4327..34e66da9e 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1448,7 +1448,7 @@ void CegInstantiator::processAssertions() { d_curr_asserts[tid].clear(); //collect all assertions from theory for( context::CDList::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) { - Node lit = (*it).assertion; + Node lit = (*it).d_assertion; Node atom = lit.getKind()==NOT ? lit[0] : lit; if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){ d_curr_asserts[tid].push_back( lit ); diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index aa3efca19..fecefb8e1 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -211,8 +211,8 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod } }else{ //simplify term - std::map visited; - getConstraints(n, constraints, visited); + std::map visitedT; + getConstraints(n, constraints, visitedT); } if( !constraints.empty() && isBool && hasPol ){ //conjoin with current diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 1d1eb9751..11b9bd14b 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -339,7 +339,6 @@ bool Instantiate::addInstantiation( } if (options::trackInstLemmas()) { - bool recorded; if (options::incrementalSolving()) { recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index d1bd5db63..ad281b009 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -823,9 +823,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // "Let W be a subset of D such that S ^ W is unsat." // and uasserts is set to W. uasserts.clear(); - std::unordered_set queryAsserts; - queryAsserts.insert(d_sc); - getUnsatCore(checkSc, queryAsserts, uasserts); + std::unordered_set queryAsserts2; + queryAsserts2.insert(d_sc); + getUnsatCore(checkSc, queryAsserts2, uasserts); falseCore = true; } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index dc290d4ba..7c1451771 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -229,9 +229,9 @@ bool SygusPbe::constructCandidates(const std::vector& enums, // the lemmas must be guarded by the active guard of the enumerator Node g = d_tds->getActiveGuardForEnumerator(e); Assert(!g.isNull()); - for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + for (unsigned k = 0, size = enum_lems.size(); k < size; k++) { - enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + enum_lems[k] = nm->mkNode(OR, g.negate(), enum_lems[k]); } lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index b78263f0e..444d6f329 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1100,8 +1100,9 @@ bool TermDb::reset( Theory::Effort effort ){ if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) { context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); for (unsigned i = 0; it != it_end; ++ it, ++i) { - if( (*it).assertion.getKind()!=INST_CLOSURE ){ - setHasTerm( (*it).assertion ); + if ((*it).d_assertion.getKind() != INST_CLOSURE) + { + setHasTerm((*it).d_assertion); } } } diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 1682b4d0c..227f4d5b5 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -95,13 +95,17 @@ void TheoryQuantifiers::ppNotifyAssertions( bool TheoryQuantifiers::collectModelInfo(TheoryModel* m) { for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { - if((*i).assertion.getKind() == kind::NOT) { - Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl; - if (!m->assertPredicate((*i).assertion[0], false)) + if ((*i).d_assertion.getKind() == kind::NOT) + { + Debug("quantifiers::collectModelInfo") + << "got quant FALSE: " << (*i).d_assertion[0] << endl; + if (!m->assertPredicate((*i).d_assertion[0], false)) { return false; } - } else { + } + else + { Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; if (!m->assertPredicate(*i, true)) { diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 2a7c3ff0d..e5d6748aa 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -156,11 +156,11 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { d_theoryRewriters[rewriteStackTop.getTheoryId()]->preRewrite( rewriteStackTop.node); // Put the rewritten node to the top of the stack - rewriteStackTop.node = response.node; + rewriteStackTop.node = response.d_node; TheoryId newTheory = theoryOf(rewriteStackTop.node); // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite if (newTheory == rewriteStackTop.getTheoryId() - && response.status == REWRITE_DONE) + && response.d_status == REWRITE_DONE) { break; } @@ -225,41 +225,42 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { d_theoryRewriters[rewriteStackTop.getTheoryId()]->postRewrite( rewriteStackTop.node); // We continue with the response we got - TheoryId newTheoryId = theoryOf(response.node); + TheoryId newTheoryId = theoryOf(response.d_node); if (newTheoryId != rewriteStackTop.getTheoryId() - || response.status == REWRITE_AGAIN_FULL) + || response.d_status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite - Assert(response.node != rewriteStackTop.node); + Assert(response.d_node != rewriteStackTop.node); //TODO: this is not thread-safe - should make this assertion dependent on sequential build #ifdef CVC4_ASSERTIONS - Assert(d_rewriteStack->find(response.node) == d_rewriteStack->end()); - d_rewriteStack->insert(response.node); + Assert(d_rewriteStack->find(response.d_node) + == d_rewriteStack->end()); + d_rewriteStack->insert(response.d_node); #endif - Node rewritten = rewriteTo(newTheoryId, response.node); + Node rewritten = rewriteTo(newTheoryId, response.d_node); rewriteStackTop.node = rewritten; #ifdef CVC4_ASSERTIONS - d_rewriteStack->erase(response.node); + d_rewriteStack->erase(response.d_node); #endif break; } - else if (response.status == REWRITE_DONE) + else if (response.d_status == REWRITE_DONE) { #ifdef CVC4_ASSERTIONS RewriteResponse r2 = - d_theoryRewriters[newTheoryId]->postRewrite(response.node); - Assert(r2.node == response.node); + d_theoryRewriters[newTheoryId]->postRewrite(response.d_node); + Assert(r2.d_node == response.d_node); #endif - rewriteStackTop.node = response.node; + rewriteStackTop.node = response.d_node; break; } // Check for trivial rewrite loops of size 1 or 2 - Assert(response.node != rewriteStackTop.node); + Assert(response.d_node != rewriteStackTop.node); Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()] - ->postRewrite(response.node) - .node + ->postRewrite(response.d_node) + .d_node != rewriteStackTop.node); - rewriteStackTop.node = response.node; + rewriteStackTop.node = response.d_node; } // We're done with the post rewrite, so we add to the cache setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(), diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index b5fc1cbc9..0b6e7a5fb 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -317,7 +317,7 @@ void TheorySep::check(Effort e) { while( !done() && !d_conflict ){ // Get all the assertions Assertion assertion = get(); - TNode fact = assertion.assertion; + TNode fact = assertion.d_assertion; Trace("sep-assert") << "TheorySep::check(): processing " << fact << std::endl; @@ -806,7 +806,7 @@ void TheorySep::check(Effort e) { d_heap_locs_nptos.clear(); //collect data points that are not pointed to for( context::CDList::const_iterator it = facts_begin(); it != facts_end(); ++ it) { - Node lit = (*it).assertion; + Node lit = (*it).d_assertion; if( lit.getKind()==kind::NOT && lit[0].getKind()==kind::SEP_PTO ){ Node s_atom = lit[0]; Node v1 = d_valuation.getModel()->getRepresentative( s_atom[0] ); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f1a11baf8..df6f76cbf 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -955,7 +955,7 @@ void TheorySetsPrivate::check(Theory::Effort level) { // Get all the assertions Assertion assertion = d_external.get(); - TNode fact = assertion.assertion; + TNode fact = assertion.d_assertion; Trace("sets-assert") << "Assert from input " << fact << std::endl; // assert the fact assertFact(fact, fact); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index d8f5f8c4f..114dfa9a6 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -62,7 +62,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { case kind::MEMBER: { if(node[0].isConst() && node[1].isConst()) { // both are constants - TNode S = preRewrite(node[1]).node; + TNode S = preRewrite(node[1]).d_node; bool isMember = checkConstantMembership(node[0], S); return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember)); }else if( node[1].getKind()==kind::EMPTYSET ){ diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index b6c14e30a..3d96e4ece 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -68,7 +68,7 @@ class TheorySetsRewriter : public TheoryRewriter Node rewriteEquality(TNode equality) { // often this will suffice - return postRewrite(equality).node; + return postRewrite(equality).d_node; } }; /* class TheorySetsRewriter */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 92af3cc0a..c2790fe42 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -620,7 +620,7 @@ void TheoryStrings::check(Effort e) { { // Get all the assertions Assertion assertion = get(); - TNode fact = assertion.assertion; + TNode fact = assertion.d_assertion; Trace("strings-assertion") << "get assertion: " << fact << endl; polarity = fact.getKind() != kind::NOT; diff --git a/src/theory/theory.h b/src/theory/theory.h index 36db0fda8..d6b02e070 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -867,7 +867,7 @@ inline theory::Assertion Theory::get() { Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; if(Dump.isOn("state")) { - Dump("state") << AssertCommand(fact.assertion.toExpr()); + Dump("state") << AssertCommand(fact.d_assertion.toExpr()); } return fact; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index dec648688..d176b015d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -472,12 +472,15 @@ void TheoryEngine::printAssertions(const char* tag) { Trace(tag) << "Assertions of " << theory->getId() << ": " << endl; context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); for (unsigned i = 0; it != it_end; ++ it, ++i) { - if ((*it).isPreregistered) { - Trace(tag) << "[" << i << "]: "; - } else { - Trace(tag) << "(" << i << "): "; - } - Trace(tag) << (*it).assertion << endl; + if ((*it).d_isPreregistered) + { + Trace(tag) << "[" << i << "]: "; + } + else + { + Trace(tag) << "(" << i << "): "; + } + Trace(tag) << (*it).d_assertion << endl; } if (d_logicInfo.isSharingEnabled()) { @@ -517,12 +520,15 @@ void TheoryEngine::dumpAssertions(const char* tag) { context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); for (; it != it_end; ++ it) { // Get the assertion - Node assertionNode = (*it).assertion; + Node assertionNode = (*it).d_assertion; // Purify all the terms - if ((*it).isPreregistered) { + if ((*it).d_isPreregistered) + { Dump(tag) << CommentCommand("Preregistered"); - } else { + } + else + { Dump(tag) << CommentCommand("Shared assertion"); } Dump(tag) << AssertCommand(assertionNode.toExpr()); @@ -725,14 +731,16 @@ void TheoryEngine::combineTheories() { for (; care_it != care_it_end; ++ care_it) { const CarePair& carePair = *care_it; - Debug("combineTheories") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << endl; + Debug("combineTheories") + << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = " + << carePair.d_b << " from " << carePair.d_theory << endl; - Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst()); - Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst()); + Assert(d_sharedTerms.isShared(carePair.d_a) || carePair.d_a.isConst()); + Assert(d_sharedTerms.isShared(carePair.d_b) || carePair.d_b.isConst()); // The equality in question (order for no repetition) - Node equality = carePair.a.eqNode(carePair.b); - // EqualityStatus es = getEqualityStatus(carePair.a, carePair.b); + Node equality = carePair.d_a.eqNode(carePair.d_b); + // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b); // Debug("combineTheories") << "TheoryEngine::combineTheories(): " << // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" : // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" : @@ -746,7 +754,12 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory); + lemma(equality.orNode(equality.notNode()), + RULE_INVALID, + false, + false, + false, + carePair.d_theory); // This code is supposed to force preference to follow what the theory models already have // but it doesn't seem to make a big difference - need to explore more -Clark @@ -1440,9 +1453,11 @@ void TheoryEngine::assertFact(TNode literal) AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom); while (!it.done()) { const AtomRequests::Request& request = it.get(); - Node toAssert = polarity ? (Node) request.atom : request.atom.notNode(); + Node toAssert = + polarity ? (Node)request.d_atom : request.d_atom.notNode(); Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl; - assertToTheory(toAssert, literal, request.toTheory, THEORY_SAT_SOLVER); + assertToTheory( + toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER); it.next(); } @@ -1621,8 +1636,8 @@ static Node mkExplanation(const std::vector& explanation) { std::set all; for (unsigned i = 0; i < explanation.size(); ++ i) { - Assert(explanation[i].theory == THEORY_SAT_SOLVER); - all.insert(explanation[i].node); + Assert(explanation[i].d_theory == THEORY_SAT_SOLVER); + all.insert(explanation[i].d_node); } if (all.size() == 0) { @@ -1632,7 +1647,7 @@ static Node mkExplanation(const std::vector& explanation) { if (all.size() == 1) { // All the same, or just one - return explanation[0].node; + return explanation[0].d_node; } NodeBuilder<> conjunction(kind::AND); @@ -1710,10 +1725,11 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe Assert(d_propagationMap.find(toExplain) != d_propagationMap.end()); NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain]; - Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node " - << nodeExplainerPair.node - << " is theory: " << nodeExplainerPair.theory << std::endl; - TheoryId explainer = nodeExplainerPair.theory; + Debug("theory::explain") + << "TheoryEngine::getExplanation: explainer for node " + << nodeExplainerPair.d_node + << " is theory: " << nodeExplainerPair.d_theory << std::endl; + TheoryId explainer = nodeExplainerPair.d_theory; // Create the workplace for explanations std::vector explanationVector; @@ -2061,31 +2077,42 @@ void TheoryEngine::getExplanation(std::vector& explanationVector // Get the current literal to explain NodeTheoryPair toExplain = explanationVector[i]; - Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; - + Debug("theory::explain") + << "[i=" << i << "] TheoryEngine::explain(): processing [" + << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from " + << toExplain.d_theory << endl; // If a true constant or a negation of a false constant we can ignore it - if (toExplain.node.isConst() && toExplain.node.getConst()) { + if (toExplain.d_node.isConst() && toExplain.d_node.getConst()) + { ++ i; continue; } - if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst()) { + if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst() + && !toExplain.d_node[0].getConst()) + { ++ i; continue; } // If from the SAT solver, keep it - if (toExplain.theory == THEORY_SAT_SOLVER) { + if (toExplain.d_theory == THEORY_SAT_SOLVER) + { Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; continue; } // If an and, expand it - if (toExplain.node.getKind() == kind::AND) { - Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << endl; - for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) { - NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp); + if (toExplain.d_node.getKind() == kind::AND) + { + Debug("theory::explain") + << "TheoryEngine::explain(): expanding " << toExplain.d_node + << " got from " << toExplain.d_theory << endl; + for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k) + { + NodeTheoryPair newExplain( + toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); } ++ i; @@ -2097,24 +2124,31 @@ void TheoryEngine::getExplanation(std::vector& explanationVector if (find != d_propagationMap.end()) { Debug("theory::explain") << "\tTerm was propagated by another theory (theory = " - << getTheoryString((*find).second.theory) << ")" << std::endl; + << getTheoryString((*find).second.d_theory) << ")" << std::endl; // There is some propagation, check if its a timely one - if ((*find).second.timestamp < toExplain.timestamp) { - Debug("theory::explain") << "\tRelevant timetsamp, pushing " - << (*find).second.node << "to index = " << explanationVector.size() << std::endl; + if ((*find).second.d_timestamp < toExplain.d_timestamp) + { + Debug("theory::explain") + << "\tRelevant timetsamp, pushing " << (*find).second.d_node + << "to index = " << explanationVector.size() << std::endl; explanationVector.push_back((*find).second); ++i; PROOF({ - if (toExplain.node != (*find).second.node) { - Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node - << ", toExplain = " << (*find).second.node << std::endl; + if (toExplain.d_node != (*find).second.d_node) + { + Debug("pf::explain") + << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " + << toExplain.d_node << ", toExplain = " << (*find).second.d_node + << std::endl; - if (proofRecipe) { - proofRecipe->addRewriteRule(toExplain.node, (*find).second.node); - } + if (proofRecipe) + { + proofRecipe->addRewriteRule(toExplain.d_node, + (*find).second.d_node); } - }) + } + }) continue; } @@ -2122,21 +2156,27 @@ void TheoryEngine::getExplanation(std::vector& explanationVector // It was produced by the theory, so ask for an explanation Node explanation; - if (toExplain.theory == THEORY_BUILTIN) { - explanation = d_sharedTerms.explain(toExplain.node); + if (toExplain.d_theory == THEORY_BUILTIN) + { + explanation = d_sharedTerms.explain(toExplain.d_node); Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl; - } else { - explanation = theoryOf(toExplain.theory)->explain(toExplain.node); + } + else + { + explanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); Debug("theory::explain") << "\tTerm was propagated by owner theory: " - << theoryOf(toExplain.theory)->getId() + << theoryOf(toExplain.d_theory)->getId() << ". Explanation: " << explanation << std::endl; } - Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl; - Assert(explanation != toExplain.node) + Debug("theory::explain") + << "TheoryEngine::explain(): got explanation " << explanation + << " got from " << toExplain.d_theory << endl; + Assert(explanation != toExplain.d_node) << "wasn't sent to you, so why are you explaining it trivially"; // Mark the explanation - NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); + NodeTheoryPair newExplain( + explanation, toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); ++ i; @@ -2147,10 +2187,10 @@ void TheoryEngine::getExplanation(std::vector& explanationVector // If we're expanding the target node of the explanation (this is the // first expansion...), we don't want to add it as a separate proof // step. It is already part of the assertions. - if (!ContainsKey(*inputAssertions, toExplain.node)) + if (!ContainsKey(*inputAssertions, toExplain.d_node)) { - LemmaProofRecipe::ProofStep proofStep(toExplain.theory, - toExplain.node); + LemmaProofRecipe::ProofStep proofStep(toExplain.d_theory, + toExplain.d_node); if (explanation.getKind() == kind::AND) { Node flat = flattenAnd(explanation); @@ -2189,7 +2229,7 @@ void TheoryEngine::getExplanation(std::vector& explanationVector if (proofRecipe) { // The remaining literals are the base of the proof for (unsigned k = 0; k < explanationVector.size(); ++k) { - proofRecipe->addBaseAssertion(explanationVector[k].node.negate()); + proofRecipe->addBaseAssertion(explanationVector[k].d_node.negate()); } } }); @@ -2224,7 +2264,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { it_end = theory->facts_end(); it != it_end; ++it) { - Node assertion = (*it).assertion; + Node assertion = (*it).d_assertion; Node val = getModel()->getValue(assertion); if (val != d_true) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index a5631059f..1757d7a6d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -60,15 +60,17 @@ class LemmaProofRecipe; * propagations between theories. */ struct NodeTheoryPair { - Node node; - theory::TheoryId theory; - size_t timestamp; - NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp = 0) - : node(node), theory(theory), timestamp(timestamp) {} - NodeTheoryPair() : theory(theory::THEORY_LAST), timestamp() {} + Node d_node; + theory::TheoryId d_theory; + size_t d_timestamp; + NodeTheoryPair(TNode n, theory::TheoryId t, size_t ts = 0) + : d_node(n), d_theory(t), d_timestamp(ts) + { + } + NodeTheoryPair() : d_theory(theory::THEORY_LAST), d_timestamp() {} // Comparison doesn't take into account the timestamp bool operator == (const NodeTheoryPair& pair) const { - return node == pair.node && theory == pair.theory; + return d_node == pair.d_node && d_theory == pair.d_theory; } };/* struct NodeTheoryPair */ @@ -76,8 +78,8 @@ struct NodeTheoryPairHashFunction { NodeHashFunction hashFunction; // Hash doesn't take into account the timestamp size_t operator()(const NodeTheoryPair& pair) const { - uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.node)); - return static_cast(fnv1a::fnv1a_64(pair.theory, hash)); + uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node)); + return static_cast(fnv1a::fnv1a_64(pair.d_theory, hash)); } };/* struct NodeTheoryPairHashFunction */ diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index 61f0fc27a..e7dc782bb 100644 --- a/src/theory/theory_rewriter.h +++ b/src/theory/theory_rewriter.h @@ -46,11 +46,9 @@ enum RewriteStatus */ struct RewriteResponse { - const RewriteStatus status; - const Node node; - RewriteResponse(RewriteStatus status, Node node) : status(status), node(node) - { - } + const RewriteStatus d_status; + const Node d_node; + RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {} }; /* struct RewriteResponse */ /** diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 8e0c96ae3..63aa81097 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -24,22 +24,22 @@ namespace theory { namespace eq { EqualityEngine::Statistics::Statistics(std::string name) - : mergesCount(name + "::mergesCount", 0), - termsCount(name + "::termsCount", 0), - functionTermsCount(name + "::functionTermsCount", 0), - constantTermsCount(name + "::constantTermsCount", 0) + : d_mergesCount(name + "::mergesCount", 0), + d_termsCount(name + "::termsCount", 0), + d_functionTermsCount(name + "::functionTermsCount", 0), + d_constantTermsCount(name + "::constantTermsCount", 0) { - smtStatisticsRegistry()->registerStat(&mergesCount); - smtStatisticsRegistry()->registerStat(&termsCount); - smtStatisticsRegistry()->registerStat(&functionTermsCount); - smtStatisticsRegistry()->registerStat(&constantTermsCount); + smtStatisticsRegistry()->registerStat(&d_mergesCount); + smtStatisticsRegistry()->registerStat(&d_termsCount); + smtStatisticsRegistry()->registerStat(&d_functionTermsCount); + smtStatisticsRegistry()->registerStat(&d_constantTermsCount); } EqualityEngine::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&mergesCount); - smtStatisticsRegistry()->unregisterStat(&termsCount); - smtStatisticsRegistry()->unregisterStat(&functionTermsCount); - smtStatisticsRegistry()->unregisterStat(&constantTermsCount); + smtStatisticsRegistry()->unregisterStat(&d_mergesCount); + smtStatisticsRegistry()->unregisterStat(&d_termsCount); + smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount); + smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount); } /** @@ -47,28 +47,31 @@ EqualityEngine::Statistics::~Statistics() { */ struct BfsData { // The current node - EqualityNodeId nodeId; + EqualityNodeId d_nodeId; // The index of the edge we traversed - EqualityEdgeId edgeId; + EqualityEdgeId d_edgeId; // Index in the queue of the previous node. Shouldn't be too much of them, at most the size // of the biggest equivalence class - size_t previousIndex; + size_t d_previousIndex; - BfsData(EqualityNodeId nodeId = null_id, EqualityEdgeId edgeId = null_edge, size_t prev = 0) - : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {} + BfsData(EqualityNodeId nodeId = null_id, + EqualityEdgeId edgeId = null_edge, + size_t prev = 0) + : d_nodeId(nodeId), d_edgeId(edgeId), d_previousIndex(prev) + { + } }; class ScopedBool { - bool& watch; - bool oldValue; -public: - ScopedBool(bool& watch, bool newValue) - : watch(watch), oldValue(watch) { - watch = newValue; - } - ~ScopedBool() { - watch = oldValue; + bool& d_watch; + bool d_oldValue; + + public: + ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch) + { + d_watch = newValue; } + ~ScopedBool() { d_watch = d_oldValue; } }; EqualityEngineNotifyNone EqualityEngine::s_notifyNone; @@ -158,7 +161,10 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) { } void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) { - Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << "). reason: " << candidate.reason << std::endl; + Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.d_t1Id] + << ", " << d_nodes[candidate.d_t2Id] << ", " + << candidate.d_type << "). reason: " << candidate.d_reason + << std::endl; if (back) { d_propagationQueue.push_back(candidate); } else { @@ -169,7 +175,7 @@ void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) { EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type) { Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl; - ++ d_stats.functionTermsCount; + ++d_stats.d_functionTermsCount; // Get another id for this EqualityNodeId funId = newNode(original); @@ -211,7 +217,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { Debug("equality") << d_name << "::eq::newNode(" << node << ")" << std::endl; - ++ d_stats.termsCount; + ++d_stats.d_termsCount; // Register the new id of the term EqualityNodeId newId = d_nodes.size(); @@ -477,8 +483,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef); TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef); // Go through and notify the shared dis-equalities - Theory::Set aTags = aTriggerTerms.tags; - Theory::Set bTags = bTriggerTerms.tags; + Theory::Set aTags = aTriggerTerms.d_tags; + Theory::Set bTags = bTriggerTerms.d_tags; TheoryId aTag = Theory::setPop(aTags); TheoryId bTag = Theory::setPop(bTags); int a_i = 0, b_i = 0; @@ -491,8 +497,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig ++ b_i; } else { // Same tags, notify - EqualityNodeId aSharedId = aTriggerTerms.triggers[a_i++]; - EqualityNodeId bSharedId = bTriggerTerms.triggers[b_i++]; + EqualityNodeId aSharedId = aTriggerTerms.d_triggers[a_i++]; + EqualityNodeId bSharedId = bTriggerTerms.d_triggers[b_i++]; // Propagate if (!hasPropagatedDisequality(aTag, aSharedId, bSharedId)) { // Store a proof if not there already @@ -533,7 +539,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Assert(triggersFired.empty()); - ++ d_stats.mergesCount; + ++d_stats.d_mergesCount; EqualityNodeId class1Id = class1.getFind(); EqualityNodeId class2Id = class2.getFind(); @@ -562,10 +568,14 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Trigger set of class 1 TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; - Theory::Set class1Tags = class1triggerRef == null_set_id ? 0 : getTriggerTermSet(class1triggerRef).tags; + Theory::Set class1Tags = class1triggerRef == null_set_id + ? 0 + : getTriggerTermSet(class1triggerRef).d_tags; // Trigger set of class 2 TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; - Theory::Set class2Tags = class2triggerRef == null_set_id ? 0 : getTriggerTermSet(class2triggerRef).tags; + Theory::Set class2Tags = class2triggerRef == null_set_id + ? 0 + : getTriggerTermSet(class2triggerRef).d_tags; // Disequalities coming from class2 TaggedEqualitiesSet class2disequalitiesToNotify; @@ -600,17 +610,19 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1]; // If the two are not already in the same class - if (otherTrigger.classId != trigger.classId) { - trigger.classId = class1Id; + if (otherTrigger.d_classId != trigger.d_classId) + { + trigger.d_classId = class1Id; // If they became the same, call the trigger - if (otherTrigger.classId == class1Id) { + if (otherTrigger.d_classId == class1Id) + { // Id of the real trigger is half the internal one triggersFired.push_back(currentTrigger); } } // Go to the next trigger - currentTrigger = trigger.nextTrigger; + currentTrigger = trigger.d_nextTrigger; } // Move to the next node @@ -635,17 +647,19 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Get the function application EqualityNodeId funId = useNode.getApplicationId(); Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; - const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; + const FunctionApplication& fun = + d_applications[useNode.getApplicationId()].d_normalized; // If it's interpreted and we can interpret - if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { - // Get the actual term id - TNode term = d_nodes[funId]; - subtermEvaluates(getNodeId(term)); - } - // Check if there is an application with find arguments - EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); - EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); - FunctionApplication funNormalized(fun.type, aNormalized, bNormalized); + if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) + { + // Get the actual term id + TNode term = d_nodes[funId]; + subtermEvaluates(getNodeId(term)); + } + // Check if there is an application with find arguments + EqualityNodeId aNormalized = getEqualityNode(fun.d_a).getFind(); + EqualityNodeId bNormalized = getEqualityNode(fun.d_b).getFind(); + FunctionApplication funNormalized(fun.d_type, aNormalized, bNormalized); ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); if (find != d_applicationLookup.end()) { // Applications fun and the funNormalized can be merged due to congruence @@ -696,14 +710,15 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef); // Initialize the merged set - Theory::Set newSetTags = Theory::setUnion(class1triggers.tags, class2triggers.tags); + Theory::Set newSetTags = + Theory::setUnion(class1triggers.d_tags, class2triggers.d_tags); EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = 0; int i1 = 0; int i2 = 0; - Theory::Set tags1 = class1triggers.tags; - Theory::Set tags2 = class2triggers.tags; + Theory::Set tags1 = class1triggers.d_tags; + Theory::Set tags2 = class2triggers.d_tags; TheoryId tag1 = Theory::setPop(tags1); TheoryId tag2 = Theory::setPop(tags2); @@ -713,18 +728,21 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect { if (tag1 < tag2) { // copy tag1 - newSetTriggers[newSetTriggersSize++] = class1triggers.triggers[i1++]; + newSetTriggers[newSetTriggersSize++] = + class1triggers.d_triggers[i1++]; tag1 = Theory::setPop(tags1); } else if (tag1 > tag2) { // copy tag2 - newSetTriggers[newSetTriggersSize++] = class2triggers.triggers[i2++]; + newSetTriggers[newSetTriggersSize++] = + class2triggers.d_triggers[i2++]; tag2 = Theory::setPop(tags2); } else { // copy tag1 - EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = class1triggers.triggers[i1++]; + EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = + class1triggers.d_triggers[i1++]; // since they are both tagged notify of merge if (d_performNotify) { - EqualityNodeId tag2id = class2triggers.triggers[i2++]; + EqualityNodeId tag2id = class2triggers.d_triggers[i2++]; if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { return false; } @@ -736,7 +754,8 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } // Add the new trigger set, if different from previous one - if (class1triggers.tags != class2triggers.tags) { + if (class1triggers.d_tags != class2triggers.d_tags) + { // Add it to the list for backtracking d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, class1triggerRef)); d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; @@ -771,8 +790,8 @@ void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, Equal TriggerId currentTrigger = d_nodeTriggers[currentId]; while (currentTrigger != null_trigger) { Trigger& trigger = d_equalityTriggers[currentTrigger]; - trigger.classId = class2Id; - currentTrigger = trigger.nextTrigger; + trigger.d_classId = class2Id; + currentTrigger = trigger.d_nextTrigger; } // Move to the next node @@ -800,8 +819,10 @@ void EqualityEngine::backtrack() { // Get the ids of the merged classes Equality& eq = d_assertedEqualities[i]; // Undo the merge - if (eq.lhs != null_id) { - undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs); + if (eq.d_lhs != null_id) + { + undoMerge( + d_equalityNodes[eq.d_lhs], d_equalityNodes[eq.d_rhs], eq.d_rhs); } } @@ -823,7 +844,7 @@ void EqualityEngine::backtrack() { // Unset the individual triggers for (int i = d_triggerTermSetUpdates.size() - 1, i_end = d_triggerTermSetUpdatesSize; i >= i_end; -- i) { const TriggerSetUpdate& update = d_triggerTermSetUpdates[i]; - d_nodeIndividualTrigger[update.classId] = update.oldValue; + d_nodeIndividualTrigger[update.d_classId] = update.d_oldValue; } d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize); } @@ -832,7 +853,7 @@ void EqualityEngine::backtrack() { // Unlink the triggers from the lists for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) { const Trigger& trigger = d_equalityTriggers[i]; - d_nodeTriggers[trigger.classId] = trigger.nextTrigger; + d_nodeTriggers[trigger.d_classId] = trigger.d_nextTrigger; } // Get rid of the triggers d_equalityTriggers.resize(d_equalityTriggersCount); @@ -860,12 +881,12 @@ void EqualityEngine::backtrack() { Debug("equality") << d_name << "::eq::backtrack(): removing node " << d_nodes[i] << std::endl; d_nodeIds.erase(d_nodes[i]); - const FunctionApplication& app = d_applications[i].original; + const FunctionApplication& app = d_applications[i].d_original; if (!app.isNull()) { // Remove b from use-list - getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); + getEqualityNode(app.d_b).removeTopFromUseList(d_useListNodes); // Remove a from use-list - getEqualityNode(app.a).removeTopFromUseList(d_useListNodes); + getEqualityNode(app.d_a).removeTopFromUseList(d_useListNodes); } } @@ -959,8 +980,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, << "Don't ask for stuff I didn't notify you about"; DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second; - for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { - + for (unsigned i = reasonRef.d_mergesStart; i < reasonRef.d_mergesEnd; ++i) + { EqualityPair toExplain = d_deducedDisequalityReasons[i]; std::shared_ptr eqpc; @@ -1143,7 +1164,7 @@ void EqualityEngine::getExplanation( // The next node to visit BfsData current = bfsQueue[currentIndex]; - EqualityNodeId currentNode = current.nodeId; + EqualityNodeId currentNode = current.d_nodeId; Debug("equality") << d_name << "::eq::getExplanation(): currentNode = " << d_nodes[currentNode] << std::endl; @@ -1159,8 +1180,8 @@ void EqualityEngine::getExplanation( const EqualityEdge& edge = d_equalityEdges[currentEdge]; // If not just the backwards edge - if ((currentEdge | 1u) != (current.edgeId | 1u)) { - + if ((currentEdge | 1u) != (current.d_edgeId | 1u)) + { Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; // Did we find the path @@ -1173,7 +1194,7 @@ void EqualityEngine::getExplanation( // Reconstruct the path do { // The current node - currentNode = bfsQueue[currentIndex].nodeId; + currentNode = bfsQueue[currentIndex].d_nodeId; EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId(); unsigned reasonType = d_equalityEdges[currentEdge].getReasonType(); Node reason = d_equalityEdges[currentEdge].getReason(); @@ -1195,18 +1216,20 @@ void EqualityEngine::getExplanation( case MERGED_THROUGH_CONGRUENCE: { // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2 Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl; - const FunctionApplication& f1 = d_applications[currentNode].original; - const FunctionApplication& f2 = d_applications[edgeNode].original; + const FunctionApplication& f1 = + d_applications[currentNode].d_original; + const FunctionApplication& f2 = + d_applications[edgeNode].d_original; Debug("equality") << push; Debug("equality") << "Explaining left hand side equalities" << std::endl; std::shared_ptr eqpc1 = eqpc ? std::make_shared() : nullptr; - getExplanation(f1.a, f2.a, equalities, cache, eqpc1.get()); + getExplanation(f1.d_a, f2.d_a, equalities, cache, eqpc1.get()); Debug("equality") << "Explaining right hand side equalities" << std::endl; std::shared_ptr eqpc2 = eqpc ? std::make_shared() : nullptr; - getExplanation(f1.b, f2.b, equalities, cache, eqpc2.get()); + getExplanation(f1.d_b, f2.d_b, equalities, cache, eqpc2.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); @@ -1214,25 +1237,35 @@ void EqualityEngine::getExplanation( //leave node null for now eqpc->d_node = Node::null(); } else { - if(d_nodes[f1.a].getKind() == kind::APPLY_UF || - d_nodes[f1.a].getKind() == kind::SELECT || - d_nodes[f1.a].getKind() == kind::STORE) { - eqpc->d_node = d_nodes[f1.a]; - } else { - if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst() == kind::SELECT) { - eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]); + if (d_nodes[f1.d_a].getKind() == kind::APPLY_UF + || d_nodes[f1.d_a].getKind() == kind::SELECT + || d_nodes[f1.d_a].getKind() == kind::STORE) + { + eqpc->d_node = d_nodes[f1.d_a]; + } + else + { + if (d_nodes[f1.d_a].getKind() == kind::BUILTIN + && d_nodes[f1.d_a].getConst() == kind::SELECT) + { + eqpc->d_node = NodeManager::currentNM()->mkNode( + kind::PARTIAL_SELECT_1, d_nodes[f1.d_b]); // The first child is a PARTIAL_SELECT_0. // Give it a child so that we know what kind of (read) it is, when we dump to LFSC. Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0); Assert(eqpc->d_children[0]->d_children.size() == 0); - eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, - d_nodes[f1.b]); - } else { - eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, - ProofManager::currentPM()->mkOp(d_nodes[f1.a]), - d_nodes[f1.b]); + eqpc->d_children[0]->d_node = + NodeManager::currentNM()->mkNode( + kind::PARTIAL_SELECT_0, d_nodes[f1.d_b]); + } + else + { + eqpc->d_node = NodeManager::currentNM()->mkNode( + kind::PARTIAL_APPLY_UF, + ProofManager::currentPM()->mkOp(d_nodes[f1.d_a]), + d_nodes[f1.d_b]); } } } @@ -1245,14 +1278,14 @@ void EqualityEngine::getExplanation( // x1 == x1 Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode; - const FunctionApplication& eq = d_applications[eqId].original; + const FunctionApplication& eq = d_applications[eqId].d_original; Assert(eq.isEquality()) << "Must be an equality"; // Explain why a = b constant Debug("equality") << push; std::shared_ptr eqpc1 = eqpc ? std::make_shared() : nullptr; - getExplanation(eq.a, eq.b, equalities, cache, eqpc1.get()); + getExplanation(eq.d_a, eq.d_b, equalities, cache, eqpc1.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); } @@ -1335,8 +1368,8 @@ void EqualityEngine::getExplanation( } // Go to the previous - currentEdge = bfsQueue[currentIndex].edgeId; - currentIndex = bfsQueue[currentIndex].previousIndex; + currentEdge = bfsQueue[currentIndex].d_edgeId; + currentIndex = bfsQueue[currentIndex].d_previousIndex; //---from Morgan--- if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { @@ -1577,8 +1610,8 @@ void EqualityEngine::propagate() { d_propagationQueue.pop_front(); // Get the representatives - EqualityNodeId t1classId = getEqualityNode(current.t1Id).getFind(); - EqualityNodeId t2classId = getEqualityNode(current.t2Id).getFind(); + EqualityNodeId t1classId = getEqualityNode(current.d_t1Id).getFind(); + EqualityNodeId t2classId = getEqualityNode(current.d_t2Id).getFind(); // If already the same, we're done if (t1classId == t2classId) { @@ -1596,7 +1629,8 @@ void EqualityEngine::propagate() { Assert(node2.getFind() == t2classId); // Add the actual equality to the equality graph - addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason); + addGraphEdge( + current.d_t1Id, current.d_t2Id, current.d_type, current.d_reason); // If constants are being merged we're done if (d_isConstant[t1classId] && d_isConstant[t2classId]) { @@ -1642,14 +1676,18 @@ void EqualityEngine::propagate() { } if (mergeInto == t2classId) { - Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; + Debug("equality") << d_name << "::eq::propagate(): merging " + << d_nodes[current.d_t1Id] << " into " + << d_nodes[current.d_t2Id] << std::endl; d_assertedEqualities.push_back(Equality(t2classId, t1classId)); d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; if (!merge(node2, node1, triggers)) { d_done = true; } } else { - Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl; + Debug("equality") << d_name << "::eq::propagate(): merging " + << d_nodes[current.d_t2Id] << " into " + << d_nodes[current.d_t1Id] << std::endl; d_assertedEqualities.push_back(Equality(t1classId, t2classId)); d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; if (!merge(node1, node2, triggers)) { @@ -1667,11 +1705,13 @@ void EqualityEngine::propagate() { if (d_performNotify && !d_done) { for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) { const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]]; - if (triggerInfo.trigger.getKind() == kind::EQUAL) { + if (triggerInfo.d_trigger.getKind() == kind::EQUAL) + { // Special treatment for disequalities - if (!triggerInfo.polarity) { + if (!triggerInfo.d_polarity) + { // Store that we are propagating a diseauality - TNode equality = triggerInfo.trigger; + TNode equality = triggerInfo.d_trigger; EqualityNodeId original = getNodeId(equality); TNode lhs = equality[0]; TNode rhs = equality[1]; @@ -1685,18 +1725,28 @@ void EqualityEngine::propagate() { d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId)); } storePropagatedDisequality(THEORY_LAST, lhsId, rhsId); - if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { + if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger, + triggerInfo.d_polarity)) + { d_done = true; } } - } else { + } + else + { // Equalities are simple - if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { + if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger, + triggerInfo.d_polarity)) + { d_done = true; } } - } else { - if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity)) { + } + else + { + if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger, + triggerInfo.d_polarity)) + { d_done = true; } } @@ -1776,10 +1826,13 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const if (find != d_applicationLookup.end()) { if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) { if (ensureProof) { - const FunctionApplication original = d_applications[find->second].original; - nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.a)); + const FunctionApplication original = + d_applications[find->second].d_original; + nonConst->d_deducedDisequalityReasons.push_back( + EqualityPair(t1Id, original.d_a)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId)); - nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b)); + nonConst->d_deducedDisequalityReasons.push_back( + EqualityPair(t2Id, original.d_b)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } Debug("equality") << "\t(YES)" << std::endl; @@ -1788,15 +1841,18 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const } // Check the symmetric disequality - std::swap(eqNormalized.a, eqNormalized.b); + std::swap(eqNormalized.d_a, eqNormalized.d_b); find = d_applicationLookup.find(eqNormalized); if (find != d_applicationLookup.end()) { if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) { if (ensureProof) { - const FunctionApplication original = d_applications[find->second].original; - nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.a)); + const FunctionApplication original = + d_applications[find->second].d_original; + nonConst->d_deducedDisequalityReasons.push_back( + EqualityPair(t2Id, original.d_a)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId)); - nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b)); + nonConst->d_deducedDisequalityReasons.push_back( + EqualityPair(t1Id, original.d_b)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } Debug("equality") << "\t(YES)" << std::endl; @@ -1875,7 +1931,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Get the existing set TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); // Initialize the new set for copy/insert - newSetTags = Theory::setInsert(tag, triggerSet.tags); + newSetTags = Theory::setInsert(tag, triggerSet.d_tags); newSetTriggersSize = 0; // Copy into to new one, and insert the new tag/id unsigned i = 0; @@ -1886,7 +1942,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) tags = Theory::setRemove(current, tags); // Insert the id into the triggers newSetTriggers[newSetTriggersSize++] = - current == tag ? eqNodeId : triggerSet.triggers[i++]; + current == tag ? eqNodeId : triggerSet.d_triggers[i++]; } } else { // Setup a singleton @@ -1920,11 +1976,11 @@ TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const EqualityNodeId classId = getEqualityNode(t).getFind(); const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]); unsigned i = 0; - Theory::Set tags = triggerSet.tags; + Theory::Set tags = triggerSet.d_tags; while (Theory::setPop(tags) != tag) { ++ i; } - return d_nodes[triggerSet.triggers[i]]; + return d_nodes[triggerSet.d_triggers[i]]; } void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId) { @@ -1938,9 +1994,12 @@ void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, // If an equality over constants we merge to false if (funNormalized.isEquality()) { - if (funNormalized.a == funNormalized.b) { + if (funNormalized.d_a == funNormalized.d_b) + { enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null())); - } else if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) { + } + else if (d_isConstant[funNormalized.d_a] && d_isConstant[funNormalized.d_b]) + { enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); } } @@ -1988,9 +2047,9 @@ EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(Theory::Set d_triggerDatabaseSize = d_triggerDatabaseSize + size; // Copy the information TriggerTermSet& newSet = getTriggerTermSet(newTriggerSetRef); - newSet.tags = newSetTags; + newSet.d_tags = newSetTags; for (unsigned i = 0; i < newSetTriggersSize; ++i) { - newSet.triggers[i] = newSetTriggers[i]; + newSet.d_triggers[i] = newSetTriggers[i]; } // Return the new reference return newTriggerSetRef; @@ -2055,19 +2114,20 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size()); #ifdef CVC4_ASSERTIONS // Check that the reasons are valid - for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) { + for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i) + { Assert( getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind()); } #endif if (Debug.isOn("equality::disequality")) { - for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) { + for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i) + { TNode lhs = d_nodes[d_deducedDisequalityReasons[i].first]; TNode rhs = d_nodes[d_deducedDisequalityReasons[i].second]; Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(): because " << lhs << " == " << rhs << std::endl; } - } // Store for backtracking @@ -2089,7 +2149,7 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI // The class we are looking for, shouldn't have any of the tags we are looking for already set Assert(d_nodeIndividualTrigger[classId] == null_set_id || Theory::setIntersection( - getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags, + getTriggerTermSet(d_nodeIndividualTrigger[classId]).d_tags, inputTags) == 0); @@ -2117,14 +2177,15 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI Debug("equality::trigger") << d_name << "::getDisequalities() : checking " << d_nodes[funId] << std::endl; - const FunctionApplication& fun = d_applications[useListNode.getApplicationId()].original; + const FunctionApplication& fun = + d_applications[useListNode.getApplicationId()].d_original; // If it's an equality asserted to false, we do the work if (fun.isEquality() && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { // Get the other equality member bool lhs = false; - EqualityNodeId toCompare = fun.b; + EqualityNodeId toCompare = fun.d_b; if (toCompare == currentId) { - toCompare = fun.a; + toCompare = fun.d_a; lhs = true; } // Representative of the other member @@ -2145,7 +2206,8 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI // Tags of the other gey TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); // We only care if there are things in inputTags that is also in toCompareTags - Theory::Set commonTags = Theory::setIntersection(inputTags, toCompareTriggerSet.tags); + Theory::Set commonTags = + Theory::setIntersection(inputTags, toCompareTriggerSet.d_tags); if (commonTags) { out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs)); } @@ -2178,14 +2240,17 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger for (; !d_done && it != it_end; ++ it) { // The information about the equality that is asserted to false const TaggedEquality& disequalityInfo = *it; - const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef); - Theory::Set commonTags = Theory::setIntersection(disequalityTriggerSet.tags, tags); + const TriggerTermSet& disequalityTriggerSet = + getTriggerTermSet(disequalityInfo.d_triggerSetRef); + Theory::Set commonTags = + Theory::setIntersection(disequalityTriggerSet.d_tags, tags); Assert(commonTags); // This is the actual function - const FunctionApplication& fun = d_applications[disequalityInfo.equalityId].original; + const FunctionApplication& fun = + d_applications[disequalityInfo.d_equalityId].d_original; // Figure out who we are comparing to in the original equality - EqualityNodeId toCompare = disequalityInfo.lhs ? fun.a : fun.b; - EqualityNodeId myCompare = disequalityInfo.lhs ? fun.b : fun.a; + EqualityNodeId toCompare = disequalityInfo.d_lhs ? fun.d_a : fun.d_b; + EqualityNodeId myCompare = disequalityInfo.d_lhs ? fun.d_b : fun.d_a; if (getEqualityNode(toCompare).getFind() == getEqualityNode(myCompare).getFind()) { // We're propagating a != a, which means we're inconsistent, just bail and let it go into // a regular conflict @@ -2203,7 +2268,8 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger if (!hasPropagatedDisequality(myRep, tagRep)) { d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep)); d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); - d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId)); + d_deducedDisequalityReasons.push_back( + EqualityPair(disequalityInfo.d_equalityId, d_falseId)); } // Store the propagation storePropagatedDisequality(currentTag, myRep, tagRep); diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 73d8bd4e9..041625568 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -211,13 +211,13 @@ public: /** Statistics about the equality engine instance */ struct Statistics { /** Total number of merges */ - IntStat mergesCount; + IntStat d_mergesCount; /** Number of terms managed by the system */ - IntStat termsCount; + IntStat d_termsCount; /** Number of function terms managed by the system */ - IntStat functionTermsCount; + IntStat d_functionTermsCount; /** Number of constant terms managed by the system */ - IntStat constantTermsCount; + IntStat d_constantTermsCount; Statistics(std::string name); @@ -300,12 +300,14 @@ private: */ struct Equality { /** Left hand side of the equality */ - EqualityNodeId lhs; + EqualityNodeId d_lhs; /** Right hand side of the equality */ - EqualityNodeId rhs; + EqualityNodeId d_rhs; /** Equality constructor */ - Equality(EqualityNodeId lhs = null_id, EqualityNodeId rhs = null_id) - : lhs(lhs), rhs(rhs) {} + Equality(EqualityNodeId l = null_id, EqualityNodeId r = null_id) + : d_lhs(l), d_rhs(r) + { + } };/* struct EqualityEngine::Equality */ /** The ids of the classes we have merged */ @@ -402,12 +404,15 @@ private: */ struct Trigger { /** The current class id of the LHS of the trigger */ - EqualityNodeId classId; + EqualityNodeId d_classId; /** Next trigger for class */ - TriggerId nextTrigger; + TriggerId d_nextTrigger; - Trigger(EqualityNodeId classId = null_id, TriggerId nextTrigger = null_trigger) - : classId(classId), nextTrigger(nextTrigger) {} + Trigger(EqualityNodeId classId = null_id, + TriggerId nextTrigger = null_trigger) + : d_classId(classId), d_nextTrigger(nextTrigger) + { + } };/* struct EqualityEngine::Trigger */ /** @@ -573,14 +578,17 @@ private: /** Set of trigger terms */ struct TriggerTermSet { /** Set of theories in this set */ - Theory::Set tags; + Theory::Set d_tags; /** The trigger terms */ - EqualityNodeId triggers[0]; + EqualityNodeId d_triggers[0]; /** Returns the theory tags */ - Theory::Set hasTrigger(TheoryId tag) const { return Theory::setContains(tag, tags); } + Theory::Set hasTrigger(TheoryId tag) const + { + return Theory::setContains(tag, d_tags); + } /** Returns a trigger by tag */ EqualityNodeId getTrigger(TheoryId tag) const { - return triggers[Theory::setIndex(tag, tags)]; + return d_triggers[Theory::setIndex(tag, d_tags)]; } };/* struct EqualityEngine::TriggerTermSet */ @@ -618,10 +626,13 @@ private: context::CDO d_triggerDatabaseSize; struct TriggerSetUpdate { - EqualityNodeId classId; - TriggerTermSetRef oldValue; - TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id) - : classId(classId), oldValue(oldValue) {} + EqualityNodeId d_classId; + TriggerTermSetRef d_oldValue; + TriggerSetUpdate(EqualityNodeId classId = null_id, + TriggerTermSetRef oldValue = null_set_id) + : d_classId(classId), d_oldValue(oldValue) + { + } };/* struct EqualityEngine::TriggerSetUpdate */ /** @@ -693,14 +704,18 @@ private: */ struct TaggedEquality { /** Id of the equality */ - EqualityNodeId equalityId; + EqualityNodeId d_equalityId; /** TriggerSet reference for the class of one of the sides */ - TriggerTermSetRef triggerSetRef; + TriggerTermSetRef d_triggerSetRef; /** Is trigger equivalent to the lhs (rhs otherwise) */ - bool lhs; + bool d_lhs; - TaggedEquality(EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = true) - : equalityId(equalityId), triggerSetRef(triggerSetRef), lhs(lhs) {} + TaggedEquality(EqualityNodeId equalityId = null_id, + TriggerTermSetRef triggerSetRef = null_set_id, + bool lhs = true) + : d_equalityId(equalityId), d_triggerSetRef(triggerSetRef), d_lhs(lhs) + { + } }; /** A map from equivalence class id's to tagged equalities */ diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 402b21a02..0e6d283fe 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -109,11 +109,14 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { * additional information. */ struct MergeCandidate { - EqualityNodeId t1Id, t2Id; - unsigned type; - TNode reason; - MergeCandidate(EqualityNodeId x, EqualityNodeId y, unsigned type, TNode reason) - : t1Id(x), t2Id(y), type(type), reason(reason) + EqualityNodeId d_t1Id, d_t2Id; + unsigned d_type; + TNode d_reason; + MergeCandidate(EqualityNodeId x, + EqualityNodeId y, + unsigned type, + TNode reason) + : d_t1Id(x), d_t2Id(y), d_type(type), d_reason(reason) {} }; @@ -121,10 +124,13 @@ struct MergeCandidate { * Just an index into the reasons array, and the number of merges to consume. */ struct DisequalityReasonRef { - DefaultSizeType mergesStart; - DefaultSizeType mergesEnd; - DisequalityReasonRef(DefaultSizeType mergesStart = 0, DefaultSizeType mergesEnd = 0) - : mergesStart(mergesStart), mergesEnd(mergesEnd) {} + DefaultSizeType d_mergesStart; + DefaultSizeType d_mergesEnd; + DisequalityReasonRef(DefaultSizeType mergesStart = 0, + DefaultSizeType mergesEnd = 0) + : d_mergesStart(mergesStart), d_mergesEnd(mergesEnd) + { + } }; /** @@ -289,41 +295,38 @@ enum FunctionApplicationType { */ struct FunctionApplication { /** Type of application */ - FunctionApplicationType type; + FunctionApplicationType d_type; /** The actual application elements */ - EqualityNodeId a, b; + EqualityNodeId d_a, d_b; /** Construct an application */ - FunctionApplication(FunctionApplicationType type = APP_EQUALITY, EqualityNodeId a = null_id, EqualityNodeId b = null_id) - : type(type), a(a), b(b) {} + FunctionApplication(FunctionApplicationType type = APP_EQUALITY, + EqualityNodeId a = null_id, + EqualityNodeId b = null_id) + : d_type(type), d_a(a), d_b(b) + { + } /** Equality of two applications */ bool operator == (const FunctionApplication& other) const { - return type == other.type && a == other.a && b == other.b; + return d_type == other.d_type && d_a == other.d_a && d_b == other.d_b; } /** Is this a null application */ - bool isNull() const { - return a == null_id || b == null_id; - } + bool isNull() const { return d_a == null_id || d_b == null_id; } /** Is this an equality */ - bool isEquality() const { - return type == APP_EQUALITY; - } + bool isEquality() const { return d_type == APP_EQUALITY; } /** Is this an interpreted application (equality is special, i.e. not interpreted) */ - bool isInterpreted() const { - return type == APP_INTERPRETED; - } - + bool isInterpreted() const { return d_type == APP_INTERPRETED; } }; struct FunctionApplicationHashFunction { size_t operator () (const FunctionApplication& app) const { size_t hash = 0; - hash = 0x9e3779b9 + app.a; - hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2); + hash = 0x9e3779b9 + app.d_a; + hash ^= 0x9e3779b9 + app.d_b + (hash << 6) + (hash >> 2); return hash; } }; @@ -333,14 +336,15 @@ struct FunctionApplicationHashFunction { * we keep both the original, and the normalized version. */ struct FunctionApplicationPair { - FunctionApplication original; - FunctionApplication normalized; + FunctionApplication d_original; + FunctionApplication d_normalized; FunctionApplicationPair() {} - FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized) - : original(original), normalized(normalized) {} - bool isNull() const { - return original.isNull(); + FunctionApplicationPair(const FunctionApplication& original, + const FunctionApplication& normalized) + : d_original(original), d_normalized(normalized) + { } + bool isNull() const { return d_original.isNull(); } }; /** @@ -348,12 +352,14 @@ struct FunctionApplicationPair { */ struct TriggerInfo { /** The trigger itself */ - Node trigger; + Node d_trigger; /** Polarity of the trigger */ - bool polarity; - TriggerInfo() : polarity(false) {} + bool d_polarity; + TriggerInfo() : d_polarity(false) {} TriggerInfo(Node trigger, bool polarity) - : trigger(trigger), polarity(polarity) {} + : d_trigger(trigger), d_polarity(polarity) + { + } }; } // namespace eq diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e336d1630..3b42fa6a1 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -124,7 +124,7 @@ void TheoryUF::check(Effort level) { { // Get all the assertions Assertion assertion = get(); - TNode fact = assertion.assertion; + TNode fact = assertion.d_assertion; Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl; Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl;