bool isCoDatatype)
{
std::vector<Type> 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<CVC4::Datatype>(
new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype));
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);
}
}
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;
// 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;
// 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;
// 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)
{
// 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())
toVisit.pop_back();
continue;
}
- if (stackHead.children_added)
+ if (stackHead.d_children_added)
{
// Children have been processed, so rebuild this node
Node result;
// 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();
{
// 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);
// 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<Node> children;
// 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();
*/
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 */
/**
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;
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{
{
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;
{
// 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());
namespace theory {
std::ostream& operator<<(std::ostream& out, const Assertion& a) {
- return out << a.assertion;
+ return out << a.d_assertion;
}
}/* CVC4::theory namespace */
/** 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 */
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;
}
/** 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);
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;
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 */
}
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;
std::vector<TNode> 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]);
}
while (!done()) {
- TNode fact = get().assertion;
+ TNode fact = get().d_assertion;
checkForLemma(fact);
if (node[i].getKind() == kind::CONST_BITVECTOR) {
BitVector constant = node[i].getConst<BitVector>();
// 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;
}
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;
}
* 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 */
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;
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;
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;
}
}
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;
}
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.
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,
}
} 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;
}
}
Node rewriteEquality(TNode equality)
{
// often this will suffice
- return postRewrite(equality).node;
+ return postRewrite(equality).d_node;
}
protected:
// 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()) {
d_curr_asserts[tid].clear();
//collect all assertions from theory
for( context::CDList<Assertion>::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 );
}
}else{
//simplify term
- std::map<Node, Node> visited;
- getConstraints(n, constraints, visited);
+ std::map<Node, Node> visitedT;
+ getConstraints(n, constraints, visitedT);
}
if( !constraints.empty() && isBool && hasPol ){
//conjoin with current
}
if (options::trackInstLemmas())
{
- bool recorded;
if (options::incrementalSolving())
{
recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem);
// "Let W be a subset of D such that S ^ W is unsat."
// and uasserts is set to W.
uasserts.clear();
- std::unordered_set<Node, NodeHashFunction> queryAsserts;
- queryAsserts.insert(d_sc);
- getUnsatCore(checkSc, queryAsserts, uasserts);
+ std::unordered_set<Node, NodeHashFunction> queryAsserts2;
+ queryAsserts2.insert(d_sc);
+ getUnsatCore(checkSc, queryAsserts2, uasserts);
falseCore = true;
}
}
// 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());
}
if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
context::CDList<Assertion>::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);
}
}
}
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))
{
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;
}
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(),
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;
d_heap_locs_nptos.clear();
//collect data points that are not pointed to
for( context::CDList<Assertion>::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] );
{
// 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);
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 ){
Node rewriteEquality(TNode equality)
{
// often this will suffice
- return postRewrite(equality).node;
+ return postRewrite(equality).d_node;
}
}; /* class TheorySetsRewriter */
{
// 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;
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;
Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
context::CDList<Assertion>::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()) {
context::CDList<Assertion>::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());
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" :
// 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
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();
}
std::set<TNode> 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) {
if (all.size() == 1) {
// All the same, or just one
- return explanation[0].node;
+ return explanation[0].d_node;
}
NodeBuilder<> conjunction(kind::AND);
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<NodeTheoryPair> 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<bool>()) {
+ if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
+ {
++ i;
continue;
}
- if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) {
+ if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst()
+ && !toExplain.d_node[0].getConst<bool>())
+ {
++ 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;
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;
}
// 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;
// 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);
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());
}
}
});
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)
{
* 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 */
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<size_t>(fnv1a::fnv1a_64(pair.theory, hash));
+ uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node));
+ return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash));
}
};/* struct NodeTheoryPairHashFunction */
*/
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 */
/**
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);
}
/**
*/
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;
}
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 {
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);
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();
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;
++ 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
Assert(triggersFired.empty());
- ++ d_stats.mergesCount;
+ ++d_stats.d_mergesCount;
EqualityNodeId class1Id = class1.getFind();
EqualityNodeId class2Id = class2.getFind();
// 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;
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
// 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
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);
{
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;
}
}
// 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;
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
// 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);
}
}
// 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);
}
// 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);
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);
}
}
<< "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<EqProof> eqpc;
// 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;
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
// 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();
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<EqProof> eqpc1 =
eqpc ? std::make_shared<EqProof>() : 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<EqProof> eqpc2 =
eqpc ? std::make_shared<EqProof>() : 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 );
//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>() == 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>() == 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]);
}
}
}
// 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<EqProof> eqpc1 =
eqpc ? std::make_shared<EqProof>() : 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 );
}
}
// 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) {
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) {
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]) {
}
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)) {
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];
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;
}
}
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;
}
// 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;
// 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;
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
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) {
// 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()));
}
}
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;
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
// 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);
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
// 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));
}
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
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);
/** 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);
*/
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 */
*/
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 */
/**
/** 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 */
context::CDO<DefaultSizeType> 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 */
/**
*/
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 */
* 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)
{}
};
* 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)
+ {
+ }
};
/**
*/
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;
}
};
* 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(); }
};
/**
*/
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
{
// 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;
projects / cvc5.git / commitdiff