using namespace CVC4::theory::bv;
using namespace CVC4::theory::bv::utils;
+const TermId CVC4::theory::bv::UndefinedTermId = -1;
+const ReasonId CVC4::theory::bv::UndefinedReasonId = -1;
+
+
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);
- return addInequalityInternal(id_a, id_b, id_reason);
-}
-
-bool InequalityGraph::addInequalityInternal(TermId a, TermId b, TermId reason) {
- if (getValue(a) < getValue(b)) {
- // the inequality is true in the current partial model
- return true;
- }
- if (getValue(b) < getValue(a)) {
- // the inequality is false in the current partial model
- std::vector<ReasonId> conflict;
- computeExplanation(b, a, conflict);
- return false;
+ 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;
+ }
}
// the inequality edge does not exist
- addEdge(a, b, reason);
+ addEdge(id_a, id_b, id_reason);
BFSQueue queue;
- queue.push(a);
- return computeValuesBFS(queue);
+ queue.push(PQueueElement(id_a, getValue(id_a)));
+ TermIdSet seen;
+ return computeValuesBFS(queue, seen);
}
-void InequalityGraph::computeConflict(TermId from, TermId to, std::vector<ReasonId>& explanation) {
- if (to == from)
+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);
- BitVector max(getBitwidth(a), 0);
+ 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;
return;
}
if (getValue(next) >= max) {
- max = it->value;
+ max = getValue(next);
to_visit = it->next;
reason = it->reason;
}
}
Assert(reason != UndefinedReasonId && to_visit != UndefinedTermId);
explanation.push_back(reason);
- computeConflict(from, to_visit, explanation);
+ computeExplanation(from, to_visit, explanation);
}
void InequalityGraph::addEdge(TermId a, TermId b, TermId reason) {
- Edges& out_edges = getEdges(a);
- edges.push_back(InequalityEdge(b, reason));
- Edges& in_edges = getParentEdges(b);
- edges.push_back(InequalityEdge(a, 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));
+}
+
+TermId InequalityGraph::getMaxParent(TermId id) {
+ const Edges& in_edges = getInEdges(id);
+ Assert (in_edges.size() != 0);
+
+ 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;
}
-bool InequalityGraph::computeValuesBFS(BitVector& min_val, BFSQueue& queue, TermIdSet& seen) {
+bool InequalityGraph::hasParents(TermId id) {
+ return getInEdges(id).size() != 0;
+}
+
+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;
+ }
+ }
+ Unreachable();
+}
+
+bool InequalityGraph::computeValuesBFS(BFSQueue& queue, TermIdSet& seen) {
if (queue.empty())
return true;
-
+
TermId current = queue.top().id;
seen.insert(current);
queue.pop();
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";
+
if (ineqNode.isConstant()) {
if (ineqNode.getValue() < min_val) {
- // we have a conflict
+ 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);
+ 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);
}
}
- BitVector next_min = ineqNode.getValue() + 1;
+ unsigned bitwidth = min_val.getSize();
+ BitVector next_min = ineqNode.getValue() + BitVector(bitwidth, 1u);
bool overflow = next_min < min_val;
- const Edges& edges = getEdges(current);
+ const Edges& edges = getOutEdges(current);
if (edges.size() > 0 && overflow) {
// we have reached the maximum value
- computeConflict();
+ Debug("bv-inequality") << "Conflict: overflow: " << getTerm(current) << "\n";
+ std::vector<ReasonId> conflict;
+ computeExplanation(UndefinedTermId, current, conflict);
+ setConflict(conflict);
return false;
}
- // TODO: update key, maybe
+
for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
TermId next = it->next;
- if (!seen.contains(next)) {
- BitVector& value = getInequalityNode(next).getValue();
+ if (!seen.count(next)) {
+ const BitVector& value = getInequalityNode(next).getValue();
queue.push(PQueueElement(next, value));
}
}
- return computeValuesBFS(next_min, queue, seen);
+ return computeValuesBFS(queue, seen);
}
return getValue(a) < getValue(b);
}
-TermId InequalitySolver::registerTerm(TNode term) {
+TermId InequalityGraph::registerTerm(TNode term) {
if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) {
return d_termNodeToIdMap[term];
}
// create InequalityNode
bool isConst = term.getKind() == kind::CONST_BITVECTOR;
- BitVector value = isConst? term.getConst<BitVector>() : BitVector(utils::getSize(term),0);
+ BitVector value(0,0u); // leaves the value unintialized at this time
InequalityNode ineq = InequalityNode(id, utils::getSize(term), isConst, value);
Assert (d_ineqNodes.size() == id);
d_ineqNodes.push_back(ineq);
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";
return id;
}
-ReasonId InequalitySolver::registerReason(TNode reason) {
+ReasonId InequalityGraph::registerReason(TNode reason) {
if (d_reasonToIdMap.find(reason) != d_reasonToIdMap.end()) {
return d_reasonToIdMap[reason];
}
return id;
}
-TNode InequalitySolver::getReason(ReasonId id) const {
+TNode InequalityGraph::getReason(ReasonId id) const {
Assert (d_reasonNodes.size() > id);
return d_reasonNodes[id];
}
-TNode InequalitySolver::getTerm(TermId id) const {
+TNode InequalityGraph::getTerm(TermId id) const {
Assert (d_termNodes.size() > id);
return d_termNodes[id];
}
-void InequalitySolver::setConflict(const std::vector<ReasonId>& conflict) {
+void InequalityGraph::setConflict(const std::vector<ReasonId>& conflict) {
Assert (!d_inConflict);
d_inConflict = true;
d_conflict.clear();
for (unsigned i = 0; i < conflict.size(); ++i) {
d_conflict.push_back(getReason(conflict[i]));
}
+ if (Debug.isOn("bv-inequality")) {
+ Debug("bv-inequality") << "InequalityGraph::setConflict \n";
+ for (unsigned i = 0; i < d_conflict.size(); ++i) {
+ Debug("bv-inequality") << " " << d_conflict[i] <<"\n";
+ }
+ }
}
-void InequalitySolver::getConflict(std::vector<TNode>& conflict) {
- for (unsigned i = 0; i < d_conflict.size(); ++it) {
+void InequalityGraph::getConflict(std::vector<TNode>& conflict) {
+ for (unsigned i = 0; i < d_conflict.size(); ++i) {
conflict.push_back(d_conflict[i]);
}
}
-// bool InequalityGraph::canReach(TermId from, TermId to) {
-// TermIdSet visited;
-// bfs(start, seen);
-// if (seen.constains(to)) {
-// return true;
-// }
-// }
+bool InequalityGraph::canReach(TermId from, TermId to) {
+ if (from == to )
+ return true;
+
+ TermIdSet seen;
+ TermIdQueue queue;
+ queue.push(from);
+ bfs(seen, queue);
+ if (seen.count(to)) {
+ return true;
+ }
+ return false;
+}
-// bool InequalityGraph::bfs(TermId to, TermIdSet& seen, TermIdQueue& queue) {
-// if (queue.empty())
-// return;
+void InequalityGraph::bfs(TermIdSet& seen, TermIdQueue& queue) {
+ if (queue.empty())
+ return;
-// TermId current = queue.front();
-// queue.pop();
-// if (current = to) {
-// return true;
-// }
-// const Edges& edges = getEdges(current);
-// for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
-// TermId next = it->next;
-// if(!seen.contains(next)) {
-// seen.insert(next);
-// queue.push(next);
-// }
-// }
-// return bfs(seen, queue);
-// }
+ 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::initializeValues(TNode a, TNode b) {
-// TermId id_a = registerTerm(a);
-// TermId id_b = registerTerm(b);
-// if (!hasValue(id_a) && !hasValue(id_b)) {
-// InequalityNode& ineq_a = getInequalityNode(id_a);
-// ineq_a.setValue(BiVector(utils::getSize(a), 0));
-// InequalityNode& ineq_b = getInequalityNode(id_b);
-// ineq_a.setValue(BiVector(utils::getSize(a), 1));
-// }
-// if (!hasValue(id_a) && hasValue(id_b)) {
-// BitVector& b_value = getValue(id_b);
-// if (b_value == 0) {
-// return false;
-// }
-// InequalityNode& ineq_a = getInequalityNode(id_a);
-// ineq_a.setValue(b_value - 1);
-// }
-// if (hasValue(id_a) && !hasValue(id_b)) {
-// BitVector& a_value = getValue(id_a);
-// if (a_value + 1 < a_value) {
-// return false;
-// }
-// InequalityNode& ineq_b = getInequalityNode(id_b);
-// ineq_b.setValue(a_value + 1);
-// }
-// return true;
-// }
+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);
+
+ 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;
+}
#include "context/cdqueue.h"
#include "theory/uf/equality_engine.h"
#include "theory/theory.h"
+#include <queue>
namespace CVC4 {
namespace theory {
typedef unsigned TermId;
typedef unsigned ReasonId;
-
+extern const TermId UndefinedTermId;
+extern const ReasonId UndefinedReasonId;
class InequalityGraph {
bool d_isConstant;
BitVector d_value;
public:
- InequalityNode(TermId id, unsigned bitwidth, bool isConst = false)
+ InequalityNode(TermId id, unsigned bitwidth, bool isConst, BitVector val)
: d_id(id),
d_bitwidth(bitwidth),
d_isConstant(isConst),
- d_value(BitVector(bitwidth, 0u))
+ d_value(val)
{}
TermId getId() const { return d_id; }
unsigned getBitwidth() const { return d_bitwidth; }
bool isConstant() const { return d_isConstant; }
const BitVector& getValue() const { return d_value; }
+ void setValue(const BitVector& val) { Assert (val.getSize() == d_bitwidth); d_value = val; }
};
struct PQueueElement {
typedef std::vector<InequalityEdge> Edges;
typedef __gnu_cxx::hash_set<TermId> TermIdSet;
- typedef std::queue<PQueueElement> BFSQueue;
+ typedef std::queue<TermId> TermIdQueue;
+ typedef std::priority_queue<PQueueElement> BFSQueue;
std::vector<InequalityNode> d_ineqNodes;
TermId registerTerm(TNode term);
ReasonId registerReason(TNode reason);
TNode getReason(ReasonId id) const;
+ TermId getReasonId(TermId a, TermId b);
TNode getTerm(TermId id) 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]; }
InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
- const BitVector& getValue(TermId id) const { return getInequalityNode().getValue(); }
+ 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 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);
+
+ 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 computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation);
+
context::CDO<bool> d_inConflict;
- context::CDList<TNode> d_conflict;
- void setConflict(const std::vector<ReasonId>& conflict);
+ std::vector<TNode> d_conflict;
+ void setConflict(const std::vector<ReasonId>& conflict);
+
public:
InequalityGraph(context::Context* c)
d_ineqEdges(),
d_parentEdges(),
d_inConflict(c, false),
- d_conflict(c)
+ d_conflict()
{}
bool addInequality(TNode a, TNode b, TNode reason);
bool areLessThan(TNode a, TNode b);
projects / cvc5.git / commitdiff