const TermId CVC4::theory::bv::UndefinedTermId = -1;
const ReasonId CVC4::theory::bv::UndefinedReasonId = -1;
+const ReasonId CVC4::theory::bv::AxiomReasonId = -2;
-
-bool InequalityGraph::addInequality(TNode a, TNode b, TNode reason) {
- Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << "\n";
- TermId id_a = registerTerm(a);
- TermId id_b = registerTerm(b);
- ReasonId id_reason = registerReason(reason);
-
- if (hasValue(id_a) && hasValue(id_b)) {
- if (getValue(id_a) < getValue(id_b)) {
- // the inequality is true in the current partial model
- // we still add the edge because it may not be true later (cardinality)
- addEdge(id_a, id_b, id_reason);
- return true;
- }
- if (canReach(id_b, id_a)) {
- // we are introducing a cycle; make sure the model reflects this
- Assert (getValue(id_a) >= getValue(id_b));
-
- std::vector<ReasonId> conflict;
- conflict.push_back(id_reason);
- computeExplanation(id_b, id_a, conflict);
- setConflict(conflict);
- return false;
- }
- } else {
- bool ok = initializeValues(a, b, id_reason);
- if (!ok) {
- return false;
- }
+BitVector InequalityGraph::maxValue(unsigned bitwidth) {
+ if (d_signed) {
+ return BitVector(1, 0u).concat(~BitVector(bitwidth - 1, 0u));
}
- // the inequality edge does not exist
- addEdge(id_a, id_b, id_reason);
- BFSQueue queue;
- queue.push(PQueueElement(id_a, getValue(id_a)));
- TermIdSet seen;
- return computeValuesBFS(queue, seen);
+ return ~BitVector(bitwidth, 0u);
}
-void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation) {
- if (to == from || (from == UndefinedTermId && getInequalityNode(to).isConstant())) {
- // we have explained the whole path or reached a constant that forced the value of to
- return;
- }
-
- const Edges& edges = getInEdges(to);
- if (edges.size() == 0) {
- // this can happen when from is Undefined
- Assert (from == UndefinedTermId);
- return;
- }
- BitVector max(getBitwidth(to), 0u);
- TermId to_visit = UndefinedTermId;
- ReasonId reason = UndefinedReasonId;
-
- for (Edges::const_iterator it = edges.begin(); it != edges.end(); ++it) {
- TermId next = it->next;
- if (next == from) {
- explanation.push_back(it->reason);
- return;
- }
- if (getValue(next) >= max) {
- max = getValue(next);
- to_visit = it->next;
- reason = it->reason;
- }
- }
- Assert(reason != UndefinedReasonId && to_visit != UndefinedTermId);
- explanation.push_back(reason);
- computeExplanation(from, to_visit, explanation);
-}
-
-void InequalityGraph::addEdge(TermId a, TermId b, TermId reason) {
- Edges& out_edges = getOutEdges(a);
- out_edges.push_back(InequalityEdge(b, reason));
- Edges& in_edges = getInEdges(b);
- in_edges.push_back(InequalityEdge(a, reason));
+BitVector InequalityGraph::minValue(unsigned bitwidth) {
+ if (d_signed) {
+ return ~BitVector(bitwidth, 0u);
+ }
+ return BitVector(bitwidth, 0u);
}
-TermId InequalityGraph::getMaxParent(TermId id) {
- const Edges& in_edges = getInEdges(id);
- Assert (in_edges.size() != 0);
+TermId InequalityGraph::getMaxValueId(unsigned bitwidth) {
+ BitVector bv = maxValue(bitwidth);
+ Node max = utils::mkConst(bv);
- BitVector max(getBitwidth(0), 0u);
- TermId max_id = UndefinedTermId;
- for (Edges::const_iterator it = in_edges.begin(); it!= in_edges.end(); ++it) {
- // Assert (seen.count(it->next));
- const BitVector& value = getInequalityNode(it->next).getValue();
- if (value >= max) {
- max = value;
- max_id = it->next;
- }
+ if (d_termNodeToIdMap.find(max) == d_termNodeToIdMap.end()) {
+ TermId id = d_termNodes.size();
+ d_termNodes.push_back(max);
+ d_termNodeToIdMap[max] = id;
+ InequalityNode node(id, bitwidth, true, bv);
+ d_ineqNodes.push_back(node);
+
+ // although it will never have out edges we need this to keep the size of
+ // d_termNodes and d_ineqEdges in sync
+ d_ineqEdges.push_back(Edges());
+ return id;
}
- Assert (max_id != UndefinedTermId);
- return max_id;
+ return d_termNodeToIdMap[max];
}
-bool InequalityGraph::hasParents(TermId id) {
- return getInEdges(id).size() != 0;
-}
+TermId InequalityGraph::getMinValueId(unsigned bitwidth) {
+ BitVector bv = minValue(bitwidth);
+ Node min = utils::mkConst(bv);
-TermId InequalityGraph::getReasonId(TermId a, TermId b) {
- const Edges& edges = getOutEdges(a);
- for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
- if (it->next == b) {
- return it->reason;
- }
+ if (d_termNodeToIdMap.find(min) == d_termNodeToIdMap.end()) {
+ TermId id = d_termNodes.size();
+ d_termNodes.push_back(min);
+ d_termNodeToIdMap[min] = id;
+ d_ineqEdges.push_back(Edges());
+ InequalityNode node = InequalityNode(id, bitwidth, true, bv);
+ d_ineqNodes.push_back(node);
+ return id;
}
- Unreachable();
+ return d_termNodeToIdMap[min];
}
-bool InequalityGraph::computeValuesBFS(BFSQueue& queue, TermIdSet& seen) {
- if (queue.empty())
+bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
+ Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << "\n";
+
+ TermId id_a = registerTerm(a);
+ TermId id_b = registerTerm(b);
+ ReasonId id_reason = registerReason(reason);
+
+ Assert (!(isConst(id_a) && isConst(id_b)));
+ BitVector a_val = getValue(id_a);
+ BitVector b_val = getValue(id_b);
+
+ unsigned bitwidth = utils::getSize(a);
+ BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u);
+ if (a_val + diff <= b_val) {
+ // the inequality is true in the current partial model
+ // we still add the edge because it may not be true later (cardinality)
+ addEdge(id_a, id_b, strict, id_reason);
return true;
+ }
- TermId current = queue.top().id;
- seen.insert(current);
- queue.pop();
+ if (isConst(id_b) && a_val + diff > b_val) {
+ // we must be in a conflict since a has the minimum value that
+ // satisifes the constraints
+ std::vector<ReasonId> conflict;
+ conflict.push_back(id_reason);
+ computeExplanation(UndefinedTermId, id_a, conflict);
+ Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant UB \n";
+ setConflict(conflict);
+ return false;
+ }
- InequalityNode& ineqNode = getInequalityNode(current);
- Debug("bv-inequality-internal") << "InequalityGraph::computeValueBFS \n";
- Debug("bv-inequality-internal") << " processing " << getTerm(current) << "\n"
- << " old value " << ineqNode.getValue() << "\n";
- BitVector zero(getBitwidth(current), 0u);
- BitVector one(getBitwidth(current), 1u);
- const BitVector min_val = hasParents(current) ? getInequalityNode(getMaxParent(current)).getValue() + one : zero;
- Debug("bv-inequality-internal") << " min value " << min_val << "\n";
-
+ // add the inequality edge
+ addEdge(id_a, id_b, strict, id_reason);
+ BFSQueue queue;
+ queue.push(PQueueElement(id_a, getValue(id_a), getValue(id_a),
+ (hasExplanation(id_a) ? getExplanation(id_a) : Explanation())));
+ TermIdSet seen;
+ return computeValuesBFS(queue, id_a, seen);
+}
+
+bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen) {
+ TermId id = el.id;
+ const BitVector& lower_bound = el.lower_bound;
+ InequalityNode& ineqNode = getInequalityNode(id);
+
if (ineqNode.isConstant()) {
- if (ineqNode.getValue() < min_val) {
+ if (ineqNode.getValue() < lower_bound) {
Debug("bv-inequality") << "Conflict: constant " << ineqNode.getValue() << "\n";
std::vector<ReasonId> conflict;
- TermId max_parent = getMaxParent(current);
- ReasonId reason_id = getReasonId(max_parent, current);
- conflict.push_back(reason_id);
- computeExplanation(UndefinedTermId, max_parent, conflict);
+ TermId parent = el.explanation.parent;
+ ReasonId reason = el.explanation.reason;
+ conflict.push_back(reason);
+ computeExplanation(UndefinedTermId, parent, conflict);
+ Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant\n";
setConflict(conflict);
return false;
}
} else {
// if not constant we can update the value
- if (ineqNode.getValue() < min_val) {
- Debug("bv-inequality-internal") << "Updating " << getTerm(current) <<
- " from " << ineqNode.getValue() << "\n" <<
- " to " << min_val << "\n";
- ineqNode.setValue(min_val);
+ if (ineqNode.getValue() < lower_bound) {
+ // if we are updating the term we started with we must be in a cycle
+ if (seen.count(id)) {
+ TermId parent = el.explanation.parent;
+ ReasonId reason = el.explanation.reason;
+ std::vector<TermId> conflict;
+ conflict.push_back(reason);
+ computeExplanation(id, parent, conflict);
+ Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n";
+ setConflict(conflict);
+ return false;
+ }
+ Debug("bv-inequality-internal") << "Updating " << getTermNode(id)
+ << " from " << ineqNode.getValue() << "\n"
+ << " to " << lower_bound << "\n";
+ ineqNode.setValue(lower_bound);
+ setExplanation(id, el.explanation);
}
}
- unsigned bitwidth = min_val.getSize();
- BitVector next_min = ineqNode.getValue() + BitVector(bitwidth, 1u);
- bool overflow = next_min < min_val;
- const Edges& edges = getOutEdges(current);
-
- if (edges.size() > 0 && overflow) {
- // we have reached the maximum value
- Debug("bv-inequality") << "Conflict: overflow: " << getTerm(current) << "\n";
- std::vector<ReasonId> conflict;
- computeExplanation(UndefinedTermId, current, conflict);
- setConflict(conflict);
- return false;
- }
+ return true;
+}
+bool InequalityGraph::computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet& seen) {
+ if (queue.empty())
+ return true;
+
+ const PQueueElement current = queue.top();
+ queue.pop();
+
+ if (!updateValue(current, start, seen)) {
+ return false;
+ }
+ if (seen.count(current.id) && current.id != getMaxValueId(getBitwidth(current.id))) {
+ Debug("bv-inequality-internal") << "InequalityGraph::computeValuesBFS equal cycle.";
+ // this means we are in a cycle where all the values are forced to be equal
+ return computeValuesBFS(queue, start, seen);
+ }
+
+ seen.insert(current.id);
+ const BitVector& current_value = getValue(current.id);
+
+ unsigned size = getBitwidth(current.id);
+ const BitVector zero(size, 0u);
+ const BitVector one(size, 1u);
+
+ const Edges& edges = getEdges(current.id);
for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
TermId next = it->next;
- if (!seen.count(next)) {
- const BitVector& value = getInequalityNode(next).getValue();
- queue.push(PQueueElement(next, value));
- }
+ const BitVector increment = it->strict ? one : zero;
+ const BitVector& next_lower_bound = current_value + increment;
+ const BitVector& value = getValue(next);
+ queue.push(PQueueElement(next, value, next_lower_bound, Explanation(current.id, it->reason)));
}
- return computeValuesBFS(queue, seen);
+ return computeValuesBFS(queue, start, seen);
}
+void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation) {
+ while(hasExplanation(to) && from != to) {
+ const Explanation& exp = getExplanation(to);
+ Assert (exp.reason != UndefinedReasonId);
+ explanation.push_back(exp.reason);
+
+ Assert (exp.parent != UndefinedTermId);
+ to = exp.parent;
+ }
+}
-bool InequalityGraph::areLessThanInternal(TermId a, TermId b) {
- return getValue(a) < getValue(b);
+void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) {
+ Edges& edges = getEdges(a);
+ edges.push_back(InequalityEdge(b, strict, reason));
}
TermId InequalityGraph::registerTerm(TNode term) {
+ Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << "\n";
+
+
if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) {
return d_termNodeToIdMap[term];
}
// store in node mapping
TermId id = d_termNodes.size();
+ Debug("bv-inequality-internal") << " with id " << id << "\n";
+
d_termNodes.push_back(term);
d_termNodeToIdMap[term] = id;
// create InequalityNode
+ unsigned size = utils::getSize(term);
bool isConst = term.getKind() == kind::CONST_BITVECTOR;
- BitVector value(0,0u); // leaves the value unintialized at this time
- InequalityNode ineq = InequalityNode(id, utils::getSize(term), isConst, value);
+ BitVector value = isConst? term.getConst<BitVector>() : minValue(size);
+
+ InequalityNode ineq = InequalityNode(id, size, isConst, value);
Assert (d_ineqNodes.size() == id);
d_ineqNodes.push_back(ineq);
+
Assert (d_ineqEdges.size() == id);
d_ineqEdges.push_back(Edges());
- Assert(d_parentEdges.size() == id);
- d_parentEdges.push_back(Edges());
- Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << "\n"
- << "with id " << id << "\n";
+
+ // add the default edges min <= term <= max
+ addEdge(getMinValueId(size), id, false, AxiomReasonId);
+ addEdge(id, getMaxValueId(size), false, AxiomReasonId);
+
return id;
}
return id;
}
-TNode InequalityGraph::getReason(ReasonId id) const {
+TNode InequalityGraph::getReasonNode(ReasonId id) const {
Assert (d_reasonNodes.size() > id);
return d_reasonNodes[id];
}
-TNode InequalityGraph::getTerm(TermId id) const {
+TNode InequalityGraph::getTermNode(TermId id) const {
Assert (d_termNodes.size() > id);
return d_termNodes[id];
}
d_inConflict = true;
d_conflict.clear();
for (unsigned i = 0; i < conflict.size(); ++i) {
- d_conflict.push_back(getReason(conflict[i]));
+ if (conflict[i] != AxiomReasonId) {
+ d_conflict.push_back(getReasonNode(conflict[i]));
+ }
}
if (Debug.isOn("bv-inequality")) {
Debug("bv-inequality") << "InequalityGraph::setConflict \n";
}
}
-bool InequalityGraph::canReach(TermId from, TermId to) {
- if (from == to )
- return true;
+// bool InequalityGraph::initializeValues(TNode a, TNode b, bool strict, TermId reason_id) {
+// TermId id_a = registerTerm(a);
+// TermId id_b = registerTerm(b);
- TermIdSet seen;
- TermIdQueue queue;
- queue.push(from);
- bfs(seen, queue);
- if (seen.count(to)) {
- return true;
- }
- return false;
-}
+// InequalityNode& ineq_a = getInequalityNode(id_a);
+// InequalityNode& ineq_b = getInequalityNode(id_b);
+
+// unsigned size = utils::getSize(a);
+// BitVector one = mkOne(size);
+// BitVector zero = mkZero(size);
+// BitVector diff = strict? one : zero;
+
+// // FIXME: dumb case splitting
+// if (ineq_a.isConstant() && ineq_b.isConstant()) {
+// Assert (a.getConst<BitVector>() + diff <= b.getConst<BitVector>());
+// ineq_a.setValue(a.getConst<BitVector>());
+// ineq_b.setValue(b.getConst<BitVector>());
+// return true;
+// }
+
+// if (ineq_a.isConstant()) {
+// ineq_a.setValue(a.getConst<BitVector>());
+// }
+
+// if (ineq_b.isConstant()) {
+// const BitVector& const_val = b.getConst<BitVector>();
+// ineq_b.setValue(const_val);
-void InequalityGraph::bfs(TermIdSet& seen, TermIdQueue& queue) {
- if (queue.empty())
- return;
+// if (hasValue(id_a) && !(ineq_a.getValue() + diff <= const_val)) {
+// // must be a conflict because we have as an invariant that a will have the min
+// // possible value for a.
+// std::vector<ReasonId> conflict;
+// conflict.push_back(reason_id);
+// // FIXME: this will not compute the most precise conflict
+// // could be fixed by giving computeExplanation a bound (i.e. the size of const_val)
+// computeExplanation(UndefinedTermId, id_a, conflict);
+// setConflict(conflict);
+// return false;
+// }
+// }
+
+// if (!hasValue(id_a) && !hasValue(id_b)) {
+// // initialize to the minimum possible values
+// if (strict) {
+// ineq_a.setValue(MinValue(size));
+// ineq_b.setValue(MinValue(size) + one);
+// } else {
+// ineq_a.setValue(MinValue(size));
+// ineq_b.setValue(MinValue(size));
+// }
+// }
+// else if (!hasValue(id_a) && hasValue(id_b)) {
+// const BitVector& b_value = ineq_b.getValue();
+// if (strict && b_value == MinValue(size) && ineq_b.isConstant()) {
+// Debug("bv-inequality") << "Conflict: underflow " << getTerm(id_a) <<"\n";
+// std::vector<ReasonId> conflict;
+// conflict.push_back(reason_id);
+// setConflict(conflict);
+// return false;
+// }
+// // otherwise we attempt to increment b
+// ineq_b.setValue(one);
+// }
+// // if a has no value then we can assign it to whatever we want
+// // to maintain the invariant that each value has the lowest value
+// // we assign it to zero
+// ineq_a.setValue(zero);
+// } else if (hasValue(id_a) && !hasValue(id_b)) {
+// const BitVector& a_value = ineq_a.getValue();
+// if (a_value + one < a_value) {
+// return false;
+// }
+// ineq_b.setValue(a_value + one);
+// }
+// return true;
+// }
+
+// bool InequalityGraph::canReach(TermId from, TermId to) {
+// if (from == to )
+// return true;
- TermId current = queue.front();
- queue.pop();
+// TermIdSet seen;
+// TermIdQueue queue;
+// queue.push(from);
+// bfs(seen, queue);
+// if (seen.count(to)) {
+// return true;
+// }
+// return false;
+// }
- const Edges& edges = getOutEdges(current);
- for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
- TermId next = it->next;
- if(seen.count(next) == 0) {
- seen.insert(next);
- queue.push(next);
- }
- }
- bfs(seen, queue);
-}
+// void InequalityGraph::bfs(TermIdSet& seen, TermIdQueue& queue) {
+// if (queue.empty())
+// return;
+
+// TermId current = queue.front();
+// queue.pop();
+
+// const Edges& edges = getOutEdges(current);
+// for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
+// TermId next = it->next;
+// if(seen.count(next) == 0) {
+// seen.insert(next);
+// queue.push(next);
+// }
+// }
+// bfs(seen, queue);
+// }
// void InequalityGraph::getPath(TermId to, TermId from, const TermIdSet& seen, std::vector<ReasonId> explanation) {
// // traverse parent edges
// }
// }
-bool InequalityGraph::hasValue(TermId id) const {
- return getInequalityNode(id).getValue() != BitVector(0, 0u);
-}
-
-bool InequalityGraph::initializeValues(TNode a, TNode b, TermId reason_id) {
- TermId id_a = registerTerm(a);
- TermId id_b = registerTerm(b);
-
- InequalityNode& ineq_a = getInequalityNode(id_a);
- InequalityNode& ineq_b = getInequalityNode(id_b);
- // FIXME: dumb case splitting
- if (ineq_a.isConstant() && ineq_b.isConstant()) {
- Assert (a.getConst<BitVector>() < b.getConst<BitVector>());
- ineq_a.setValue(a.getConst<BitVector>());
- ineq_b.setValue(b.getConst<BitVector>());
- return true;
- }
-
- if (ineq_a.isConstant()) {
- ineq_a.setValue(a.getConst<BitVector>());
- }
- if (ineq_b.isConstant()) {
- const BitVector& const_val = b.getConst<BitVector>();
- ineq_b.setValue(const_val);
- // check for potential underflow
- if (hasValue(id_a) && ineq_a.getValue() > const_val) {
- // must be a conflict because we have as an invariant that a will have the min
- // possible value for a.
- std::vector<ReasonId> conflict;
- conflict.push_back(reason_id);
- // FIXME: this will not compute the most precise conflict
- // could be fixed by giving computeExplanation a bound (i.e. the size of const_val)
- computeExplanation(UndefinedTermId, id_a, conflict);
- setConflict(conflict);
- return false;
- }
- }
-
- BitVector one(getBitwidth(id_a), 1u);
- BitVector zero(getBitwidth(id_a), 0u);
+// TermId InequalityGraph::getMaxParent(TermId id) {
+// const Edges& in_edges = getInEdges(id);
+// Assert (in_edges.size() != 0);
- if (!hasValue(id_a) && !hasValue(id_b)) {
- // initialize to the minimum possible values
- ineq_a.setValue(zero);
- ineq_b.setValue(one);
- }
- else if (!hasValue(id_a) && hasValue(id_b)) {
- const BitVector& b_value = ineq_b.getValue();
- if (b_value == zero) {
- if (ineq_b.isConstant()) {
- Debug("bv-inequality") << "Conflict: underflow " << getTerm(id_a) <<"\n";
- std::vector<ReasonId> conflict;
- conflict.push_back(reason_id);
- setConflict(conflict);
- return false;
- }
- // otherwise we attempt to increment b
- ineq_b.setValue(one);
- }
- // if a has no value then we can assign it to whatever we want
- // to maintain the invariant that each value has the lowest value
- // we assign it to zero
- ineq_a.setValue(zero);
- } else if (hasValue(id_a) && !hasValue(id_b)) {
- const BitVector& a_value = ineq_a.getValue();
- if (a_value + one < a_value) {
- return false;
- }
- ineq_b.setValue(a_value + one);
- }
- return true;
-}
+// BitVector max(getBitwidth(0), 0u);
+// TermId max_id = UndefinedTermId;
+// for (Edges::const_iterator it = in_edges.begin(); it!= in_edges.end(); ++it) {
+// // Assert (seen.count(it->next));
+// const BitVector& value = getInequalityNode(it->next).getValue();
+// if (value >= max) {
+// max = value;
+// max_id = it->next;
+// }
+// }
+// Assert (max_id != UndefinedTermId);
+// return max_id;
+// }
typedef unsigned TermId;
typedef unsigned ReasonId;
extern const TermId UndefinedTermId;
-extern const ReasonId UndefinedReasonId;
+extern const ReasonId UndefinedReasonId;
+extern const ReasonId AxiomReasonId;
class InequalityGraph {
struct InequalityEdge {
TermId next;
ReasonId reason;
- InequalityEdge(TermId n, ReasonId r)
- : next(n),
- reason(r)
+ bool strict;
+ InequalityEdge(TermId n, bool s, ReasonId r)
+ : next(n),
+ reason(r),
+ strict(s)
{}
};
-
+
class InequalityNode {
TermId d_id;
unsigned d_bitwidth;
bool d_isConstant;
BitVector d_value;
public:
- InequalityNode(TermId id, unsigned bitwidth, bool isConst, BitVector val)
+ InequalityNode(TermId id, unsigned bitwidth, bool isConst, const BitVector val)
: d_id(id),
d_bitwidth(bitwidth),
d_isConstant(isConst),
- d_value(val)
- {}
+ d_value(val) {}
TermId getId() const { return d_id; }
unsigned getBitwidth() const { return d_bitwidth; }
bool isConstant() const { return d_isConstant; }
void setValue(const BitVector& val) { Assert (val.getSize() == d_bitwidth); d_value = val; }
};
+ struct Explanation {
+ TermId parent;
+ ReasonId reason;
+
+ Explanation()
+ : parent(UndefinedTermId),
+ reason(UndefinedReasonId)
+ {}
+
+ Explanation(TermId p, ReasonId r)
+ : parent(p),
+ reason(r)
+ {}
+ };
+
struct PQueueElement {
TermId id;
- BitVector min_value;
- PQueueElement(TermId id, BitVector min)
- : id(id),
- min_value(min)
+ BitVector value;
+ BitVector lower_bound;
+ Explanation explanation;
+ PQueueElement(TermId id, const BitVector v, const BitVector& lb, Explanation exp)
+ : id(id),
+ value(v),
+ lower_bound(lb),
+ explanation(exp)
{}
+
bool operator< (const PQueueElement& other) const {
- return min_value < other.min_value;
+ return value > other.value;
}
- };
+ };
typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
typedef std::vector<InequalityEdge> Edges;
typedef __gnu_cxx::hash_set<TermId> TermIdSet;
- typedef std::queue<TermId> TermIdQueue;
- typedef std::priority_queue<PQueueElement> BFSQueue;
-
+ typedef std::priority_queue<PQueueElement> BFSQueue;
+ typedef __gnu_cxx::hash_map<TermId, Explanation> TermIdToExplanationMap;
std::vector<InequalityNode> d_ineqNodes;
-
std::vector< Edges > d_ineqEdges;
- std::vector< Edges > d_parentEdges;
std::vector<TNode> d_reasonNodes;
- std::vector<TNode> d_termNodes;
- ReasonToIdMap d_reasonToIdMap;
+ ReasonToIdMap d_reasonToIdMap;
+
+ std::vector<Node> d_termNodes;
TermNodeToIdMap d_termNodeToIdMap;
+ TermIdToExplanationMap d_termToExplanation;
+
+ context::CDO<bool> d_inConflict;
+ std::vector<TNode> d_conflict;
+ bool d_signed;
+
+
+ /**
+ * Registers the term by creating its corresponding InequalityNode
+ * and adding the min <= term <= max default edges.
+ *
+ * @param term
+ *
+ * @return
+ */
TermId registerTerm(TNode term);
- ReasonId registerReason(TNode reason);
- TNode getReason(ReasonId id) const;
- TermId getReasonId(TermId a, TermId b);
- TNode getTerm(TermId id) const;
+ TNode getTermNode(TermId id) const;
+ TermId getTermId(TNode node) const;
- Edges& getOutEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; }
- Edges& getInEdges(TermId id) { Assert (id < d_parentEdges.size()); return d_parentEdges[id]; }
+ ReasonId registerReason(TNode reason);
+ TNode getReasonNode(ReasonId id) const;
+
+ bool hasExplanation(TermId id) const { return d_termToExplanation.find(id) != d_termToExplanation.end(); }
+ Explanation getExplanation(TermId id) const { Assert (hasExplanation(id)); return d_termToExplanation.find(id)->second; }
+ void setExplanation(TermId id, Explanation exp) { d_termToExplanation[id] = exp; }
+
+ Edges& getEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; }
InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
const InequalityNode& getInequalityNode(TermId id) const { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
-
- const BitVector& getValue(TermId id) const { return getInequalityNode(id).getValue(); }
unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); }
+ bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); }
+ BitVector maxValue(unsigned bitwidth);
+ BitVector minValue(unsigned bitwidth);
+ TermId getMaxValueId(unsigned bitwidth);
+ TermId getMinValueId(unsigned bitwidth);
- bool hasValue(TermId id) const;
- bool initializeValues(TNode a, TNode b, TermId reason_id);
- TermId getMaxParent(TermId id);
- bool hasParents(TermId id);
-
- bool canReach(TermId from, TermId to);
- void bfs(TermIdSet& seen, TermIdQueue& queue);
+ const BitVector& getValue(TermId id) const { return getInequalityNode(id).getValue(); }
+
+ void addEdge(TermId a, TermId b, bool strict, TermId reason);
- void addEdge(TermId a, TermId b, TermId reason);
- bool addInequalityInternal(TermId a, TermId b, ReasonId reason);
- bool areLessThanInternal(TermId a, TermId b);
- void getConflictInternal(std::vector<ReasonId>& conflict);
- bool computeValuesBFS(BFSQueue& queue, TermIdSet& seen);
+ void setConflict(const std::vector<ReasonId>& conflict);
+ /**
+ * If necessary update the value in the model of the current queue element.
+ *
+ * @param el current queue element we are updating
+ * @param start node we started with, to detect cycles
+ * @param seen
+ *
+ * @return
+ */
+ bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen);
+ /**
+ * Update the current model starting with the start term.
+ *
+ * @param queue
+ * @param start
+ * @param seen
+ *
+ * @return
+ */
+ bool computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet& seen);
+ /**
+ * Return the reasons why from <= to. If from is undefined we just
+ * explain the current value of to.
+ *
+ * @param from
+ * @param to
+ * @param explanation
+ */
void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation);
- context::CDO<bool> d_inConflict;
- std::vector<TNode> d_conflict;
- void setConflict(const std::vector<ReasonId>& conflict);
-
public:
- InequalityGraph(context::Context* c)
+ InequalityGraph(context::Context* c, bool s = false)
: d_context(c),
d_ineqNodes(),
d_ineqEdges(),
- d_parentEdges(),
d_inConflict(c, false),
- d_conflict()
+ d_conflict(),
+ d_signed(s)
{}
- bool addInequality(TNode a, TNode b, TNode reason);
+ /**
+ *
+ *
+ * @param a
+ * @param b
+ * @param diff
+ * @param reason
+ *
+ * @return
+ */
+ bool addInequality(TNode a, TNode b, bool strict, TNode reason);
bool areLessThan(TNode a, TNode b);
void getConflict(std::vector<TNode>& conflict);
};
projects / cvc5.git / commitdiff