if (d_cnfStream->hasLiteral(bits[i])) {
SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
bit_value = d_satSolver->value(bit);
-- Assert (bit_value != SAT_VALUE_UNKNOWN);
++ Assert (bit_value != SAT_VALUE_UNKNOWN);
} else {
// the bit is unconstrainted so we can give it an arbitrary value
bit_value = SAT_VALUE_FALSE;
__gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
for (; it!= d_variables.end(); ++it) {
TNode var = *it;
- if ((Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) && hasValue(var)) {
- if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
++ if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
Node const_value = getVarValue(var);
Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
<< var << " "
--- /dev/null
+/********************* */
+/*! \file bv_inequality_graph.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A graph representation of the currently asserted bv inequalities.
+ **
+ ** A graph representation of the currently asserted bv inequalities.
+ **/
+
+#include "theory/bv/bv_inequality_graph.h"
+#include "theory/bv/theory_bv_utils.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+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;
+const ReasonId CVC4::theory::bv::AxiomReasonId = -2;
+
+
+bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
+ Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << " strict: " << strict << "\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 < a_val) {
+ // we have an overflow
+ std::vector<ReasonId> conflict;
+ conflict.push_back(id_reason);
+ computeExplanation(UndefinedTermId, id_a, conflict);
+ setConflict(conflict);
+ return false;
+ }
+
+ 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;
+ }
+
+ 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;
+ }
+
+ // add the inequality edge
+ addEdge(id_a, id_b, strict, id_reason);
+ BFSQueue queue(&d_modelValues);
+ Assert (hasModelValue(id_a));
+ queue.push(id_a);
+ return processQueue(queue, id_a);
+}
+
+bool InequalityGraph::updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed) {
+ BitVector lower_bound = new_mv.value;
+
+ if (isConst(id)) {
+ if (getValue(id) < lower_bound) {
+ Debug("bv-inequality") << "Conflict: constant " << getValue(id) << "\n";
+ std::vector<ReasonId> conflict;
+ TermId parent = new_mv.parent;
+ ReasonId reason = new_mv.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 try to update the value
+ if (getValue(id) < lower_bound) {
+ // if we are updating the term we started with we must be in a cycle
+ if (id == start) {
+ TermId parent = new_mv.parent;
+ ReasonId reason = new_mv.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 " << getValue(id) << "\n"
+ << " to " << lower_bound << "\n";
+ changed = true;
+ setModelValue(id, new_mv);
+ }
+ }
+ return true;
+}
+
+bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
+ while (!queue.empty()) {
+ TermId current = queue.top();
+ queue.pop();
+ Debug("bv-inequality-internal") << "InequalityGraph::processQueue proceessing " << getTermNode(current) << "\n";
+
+ BitVector current_value = getValue(current);
+
+ unsigned size = getBitwidth(current);
+ const BitVector zero(size, 0u);
+ const BitVector one(size, 1u);
+
+ const Edges& edges = getEdges(current);
+ for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
+ TermId next = it->next;
+ ReasonId reason = it->reason;
+
+ const BitVector increment = it->strict ? one : zero;
+ const BitVector next_lower_bound = current_value + increment;
+
+ if (next_lower_bound < current_value) {
+ // it means we have an overflow and hence a conflict
+ std::vector<TermId> conflict;
+ conflict.push_back(it->reason);
+ computeExplanation(start, current, conflict);
+ Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n";
+ setConflict(conflict);
+ return false;
+ }
+
+ ModelValue new_mv(next_lower_bound, current, reason);
+ bool updated = false;
+ if (!updateValue(next, new_mv, start, updated)) {
+ return false;
+ }
+
+ if (next == start) {
+ // we know what we didn't update start or we would have had a conflict
+ // this means we are in a cycle where all the values are forced to be equal
+ Debug("bv-inequality-internal") << "InequalityGraph::processQueue equal cycle.";
+ continue;
+ }
+
+ if (!updated) {
+ // if we didn't update current we don't need to add to the queue it's children
+ Debug("bv-inequality-internal") << " unchanged " << getTermNode(next) << "\n";
+ continue;
+ }
+
+ queue.push(next);
+ Debug("bv-inequality-internal") << " enqueue " << getTermNode(next) << "\n";
+ }
+ }
+ return true;
+}
+
+void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation) {
+ if(Debug.isOn("bv-inequality")) {
+ if (from == UndefinedTermId) {
+ Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(to) << "\n";
+ } else {
+ Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(from) <<" => "
+ << getTermNode(to) << "\n";
+ }
+ }
+
+ TermIdSet seen;
+
+ while(hasReason(to) && from != to && !seen.count(to)) {
+ seen.insert(to);
+ const ModelValue& exp = getModelValue(to);
+ Assert (exp.reason != UndefinedReasonId);
+ explanation.push_back(exp.reason);
+ Assert (exp.parent != UndefinedTermId);
+ to = exp.parent;
+ Debug("bv-inequality-internal") << " parent: " << getTermNode(to) << "\n"
+ << " reason: " << getReasonNode(exp.reason) << "\n";
+ }
+}
+
+void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) {
+ Debug("bv-inequality-internal") << "InequalityGraph::addEdge " << getTermNode(a) << " => " << getTermNode(b) << "\n"
+ << " strict ? " << strict << "\n";
+ Edges& edges = getEdges(a);
+ InequalityEdge new_edge(b, strict, reason);
+ edges.push_back(new_edge);
+ d_undoStack.push_back(std::make_pair(a, new_edge));
+ d_undoStackIndex = d_undoStackIndex + 1;
+}
+
+void InequalityGraph::initializeModelValue(TNode node) {
+ TermId id = getTermId(node);
+ Assert (!hasModelValue(id));
+ bool isConst = node.getKind() == kind::CONST_BITVECTOR;
+ unsigned size = utils::getSize(node);
+ BitVector value = isConst? node.getConst<BitVector>() : BitVector(size, 0u);
+ setModelValue(id, ModelValue(value, UndefinedTermId, UndefinedReasonId));
+}
+
+bool InequalityGraph::isRegistered(TNode term) const {
+ return d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end();
+}
+
+TermId InequalityGraph::registerTerm(TNode term) {
+ if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) {
+ TermId id = d_termNodeToIdMap[term];
+ if (!hasModelValue(id)) {
+ // we could have backtracked and
+ initializeModelValue(term);
+ }
+ return id;
+ }
+
+ // store in node mapping
+ TermId id = d_termNodes.size();
+ Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << " => 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;
+ InequalityNode ineq = InequalityNode(id, size, isConst);
+
+ Assert (d_ineqNodes.size() == id);
+ d_ineqNodes.push_back(ineq);
+
+ Assert (d_ineqEdges.size() == id);
+ d_ineqEdges.push_back(Edges());
+
+ initializeModelValue(term);
+
+ return id;
+}
+
+ReasonId InequalityGraph::registerReason(TNode reason) {
+ if (d_reasonToIdMap.find(reason) != d_reasonToIdMap.end()) {
+ return d_reasonToIdMap[reason];
+ }
+ ReasonId id = d_reasonNodes.size();
+ d_reasonNodes.push_back(reason);
+ d_reasonToIdMap[reason] = id;
+ return id;
+}
+
+TNode InequalityGraph::getReasonNode(ReasonId id) const {
+ Assert (d_reasonNodes.size() > id);
+ return d_reasonNodes[id];
+}
+
+TNode InequalityGraph::getTermNode(TermId id) const {
+ Assert (d_termNodes.size() > id);
+ return d_termNodes[id];
+}
+
+TermId InequalityGraph::getTermId(TNode node) const {
+ Assert (d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end());
+ return d_termNodeToIdMap.find(node)->second;
+}
+
+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) {
+ if (conflict[i] != AxiomReasonId) {
+ d_conflict.push_back(getReasonNode(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 InequalityGraph::getConflict(std::vector<TNode>& conflict) {
+ for (unsigned i = 0; i < d_conflict.size(); ++i) {
+ conflict.push_back(d_conflict[i]);
+ }
+}
+
+void InequalityGraph::setModelValue(TermId term, const ModelValue& mv) {
+ d_modelValues[term] = mv;
+}
+
+InequalityGraph::ModelValue InequalityGraph::getModelValue(TermId term) const {
+ Assert (d_modelValues.find(term) != d_modelValues.end());
+ return (*(d_modelValues.find(term))).second;
+}
+
+bool InequalityGraph::hasModelValue(TermId id) const {
+ return d_modelValues.find(id) != d_modelValues.end();
+}
+
+BitVector InequalityGraph::getValue(TermId id) const {
+ Assert (hasModelValue(id));
+ return (*(d_modelValues.find(id))).second.value;
+}
+
+bool InequalityGraph::hasReason(TermId id) const {
+ const ModelValue& mv = getModelValue(id);
+ return mv.reason != UndefinedReasonId;
+}
+
+bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
+ Debug("bv-inequality") << "InequalityGraph::addDisequality " << reason << "\n";
+ d_disequalities.push_back(reason);
+
+ if (!isRegistered(a) || !isRegistered(b)) {
+ splitDisequality(reason);
+ return true;
+ }
+ TermId id_a = getTermId(a);
+ TermId id_b = getTermId(b);
+ if (!hasModelValue(id_a)) {
+ initializeModelValue(a);
+ }
+ if (!hasModelValue(id_b)) {
+ initializeModelValue(b);
+ }
+ const BitVector val_a = getValue(id_a);
+ const BitVector val_b = getValue(id_b);
+ if (val_a == val_b) {
+ if (a.getKind() == kind::CONST_BITVECTOR) {
+ // then we know b cannot be smaller than the assigned value so we try to make it larger
+ std::vector<ReasonId> explanation_ids;
+ computeExplanation(UndefinedTermId, id_b, explanation_ids);
+ std::vector<TNode> explanation_nodes;
+ explanation_nodes.push_back(reason);
+ for (unsigned i = 0; i < explanation_ids.size(); ++i) {
+ explanation_nodes.push_back(getReasonNode(explanation_ids[i]));
+ }
+ Node explanation = utils::mkAnd(explanation_nodes);
+ d_reasonSet.insert(explanation);
+ return addInequality(a, b, true, explanation);
+ }
+ if (b.getKind() == kind::CONST_BITVECTOR) {
+ // then we know b cannot be smaller than the assigned value so we try to make it larger
+ std::vector<ReasonId> explanation_ids;
+ computeExplanation(UndefinedTermId, id_a, explanation_ids);
+ std::vector<TNode> explanation_nodes;
+ explanation_nodes.push_back(reason);
+ for (unsigned i = 0; i < explanation_ids.size(); ++i) {
+ explanation_nodes.push_back(getReasonNode(explanation_ids[i]));
+ }
+ Node explanation = utils::mkAnd(explanation_nodes);
+ d_reasonSet.insert(explanation);
+ return addInequality(b, a, true, explanation);
+ }
+ // if none of the terms are constants just add the lemma
+ splitDisequality(reason);
+ } else {
+ Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n"
+ << " " << b << " => " << val_b.toString(10) << "\n";
+ }
+ return true;
+}
+
+void InequalityGraph::splitDisequality(TNode diseq) {
+ Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << diseq <<"\n";
+ Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
+ if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) {
+ d_disequalitiesToSplit.push_back(diseq);
+ }
+}
+
+void InequalityGraph::getNewLemmas(std::vector<Node>& new_lemmas) {
+ for (unsigned i = d_diseqToSplitIndex; i < d_disequalitiesToSplit.size(); ++i) {
+ TNode diseq = d_disequalitiesToSplit[i];
+ if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) {
+ TNode a = diseq[0][0];
+ TNode b = diseq[0][1];
+ Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
+ Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
+ Node eq = diseq[0];
+ Node lemma = utils::mkNode(kind::OR, a_lt_b, b_lt_a, eq);
+ new_lemmas.push_back(lemma);
+ d_disequalitiesAlreadySplit.insert(diseq);
+ }
+ d_diseqToSplitIndex = d_diseqToSplitIndex + 1;
+ }
+}
+
+void InequalityGraph::backtrack() {
+ Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n";
+ int size = d_undoStack.size();
+ for (int i = size - 1; i >= (int)d_undoStackIndex.get(); --i) {
+ Assert (!d_undoStack.empty());
+ TermId id = d_undoStack.back().first;
+ InequalityEdge edge = d_undoStack.back().second;
+ d_undoStack.pop_back();
+
+ Debug("bv-inequality-internal") << " remove edge " << getTermNode(id) << " => "
+ << getTermNode(edge.next) <<"\n";
+ Edges& edges = getEdges(id);
+ for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
+ Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n";
+ }
+ Assert (!edges.empty());
+ Assert (edges.back() == edge);
+ edges.pop_back();
+ }
+}
+
+void InequalityGraph::checkDisequalities() {
+ for (CDQueue<TNode>::const_iterator it = d_disequalities.begin(); it != d_disequalities.end(); ++it) {
+ if (d_disequalitiesAlreadySplit.find(*it) == d_disequalitiesAlreadySplit.end()) {
+ // if we haven't already split on this disequality
+ TNode diseq = *it;
+ TermId a_id = registerTerm(diseq[0][0]);
+ TermId b_id = registerTerm(diseq[0][1]);
+ if (getValue(a_id) == getValue(b_id)) {
+ // if the disequality is not satisified by the model
+ d_disequalitiesToSplit.push_back(diseq);
+ }
+ }
+ }
+}
+
+bool InequalityGraph::isLessThan(TNode a, TNode b) {
+ Assert (isRegistered(a) && isRegistered(b));
+ Unimplemented();
+}
+
+bool InequalityGraph::hasValueInModel(TNode node) const {
+ if (isRegistered(node)) {
+ TermId id = getTermId(node);
+ return hasModelValue(id);
+ }
+ return false;
+}
+
+BitVector InequalityGraph::getValueInModel(TNode node) const {
+ TermId id = getTermId(node);
+ Assert (hasModelValue(id));
+ return getValue(id);
+}
++
++void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) {
++ for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
++ TermId id = (*it).first;
++ BitVector value = (*it).second.value;
++ TNode var = getTermNode(id);
++ Node constant = utils::mkConst(value);
++ Node assignment = utils::mkNode(kind::EQUAL, var, constant);
++ assignments.push_back(assignment);
++ Debug("bitvector-model") << " " << var <<" => " << constant << "\n";
++ }
++}
--- /dev/null
- typedef context::CDHashMap<TermId, ModelValue> Model;
+/********************* */
+/*! \file bv_inequality_graph.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
+
+#include "context/context.h"
+#include "context/cdqueue.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/theory.h"
+#include <queue>
+#include <list>
+namespace CVC4 {
+namespace theory {
+
+
+namespace bv {
+
+typedef unsigned TermId;
+typedef unsigned ReasonId;
+extern const TermId UndefinedTermId;
+extern const ReasonId UndefinedReasonId;
+extern const ReasonId AxiomReasonId;
+
+class InequalityGraph : public context::ContextNotifyObj{
+
+
+ context::Context* d_context;
+
+ struct InequalityEdge {
+ TermId next;
+ ReasonId reason;
+ bool strict;
+ InequalityEdge(TermId n, bool s, ReasonId r)
+ : next(n),
+ reason(r),
+ strict(s)
+ {}
+ bool operator==(const InequalityEdge& other) const {
+ return next == other.next && reason == other.reason && strict == other.strict;
+ }
+ };
+
+ class InequalityNode {
+ TermId d_id;
+ unsigned d_bitwidth;
+ bool d_isConstant;
+ public:
+ InequalityNode(TermId id, unsigned bitwidth, bool isConst)
+ : d_id(id),
+ d_bitwidth(bitwidth),
+ d_isConstant(isConst)
+ {}
+ TermId getId() const { return d_id; }
+ unsigned getBitwidth() const { return d_bitwidth; }
+ bool isConstant() const { return d_isConstant; }
+ };
+
+ struct ModelValue {
+ TermId parent;
+ ReasonId reason;
+ BitVector value;
+ ModelValue()
+ : parent(UndefinedTermId),
+ reason(UndefinedReasonId),
+ value(0, 0u)
+ {}
+
+ ModelValue(const BitVector& val, TermId p, ReasonId r)
+ : parent(p),
+ reason(r),
+ value(val)
+ {}
+ };
+
- const Model* d_model;
- QueueComparator(const Model* model)
++ typedef context::CDHashMap<TermId, ModelValue> ModelValues;
+
+ struct QueueComparator {
- Model d_modelValues;
++ const ModelValues* d_model;
++ QueueComparator(const ModelValues* model)
+ : d_model(model)
+ {}
+ bool operator() (TermId left, TermId right) const {
+ Assert (d_model->find(left) != d_model->end() &&
+ d_model->find(right) != d_model->end());
+
+ return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.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::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue;
+ typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+
+ std::vector<InequalityNode> d_ineqNodes;
+ std::vector< Edges > d_ineqEdges;
+
+ // to keep the explanation nodes alive
+ NodeSet d_reasonSet;
+ std::vector<TNode> d_reasonNodes;
+ ReasonToIdMap d_reasonToIdMap;
+
+ std::vector<Node> d_termNodes;
+ TermNodeToIdMap d_termNodeToIdMap;
+
+ context::CDO<bool> d_inConflict;
+ std::vector<TNode> d_conflict;
+ bool d_signed;
+
- BitVector getValueInModel(TNode a) const;
++ ModelValues d_modelValues;
+ void initializeModelValue(TNode node);
+ void setModelValue(TermId term, const ModelValue& mv);
+ ModelValue getModelValue(TermId term) const;
+ bool hasModelValue(TermId id) const;
+ bool hasReason(TermId id) const;
+
+ /**
+ * Registers the term by creating its corresponding InequalityNode
+ * and adding the min <= term <= max default edges.
+ *
+ * @param term
+ *
+ * @return
+ */
+ TermId registerTerm(TNode term);
+ TNode getTermNode(TermId id) const;
+ TermId getTermId(TNode node) const;
+ bool isRegistered(TNode term) const;
+
+ ReasonId registerReason(TNode reason);
+ TNode getReasonNode(ReasonId id) const;
+
+
+ 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]; }
+ unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); }
+ bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); }
+
+ BitVector getValue(TermId id) const;
+
+ void addEdge(TermId a, TermId b, bool strict, TermId reason);
+
+ void setConflict(const std::vector<ReasonId>& conflict);
+ /**
+ * If necessary update the value in the model of the current queue element.
+ *
+ * @param id current queue element we are updating
+ * @param start node we started with, to detect cycles
+ *
+ * @return
+ */
+ bool updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed);
+ /**
+ * Update the current model starting with the start term.
+ *
+ * @param queue
+ * @param start
+ *
+ * @return
+ */
+ bool processQueue(BFSQueue& queue, TermId start);
+ /**
+ * 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);
+ void splitDisequality(TNode diseq);
+
+ /**
+ Disequality reasoning
+ */
+
+ /*** The currently asserted disequalities */
+ context::CDQueue<TNode> d_disequalities;
+ context::CDQueue<TNode> d_disequalitiesToSplit;
+ context::CDO<unsigned> d_diseqToSplitIndex;
+ TNodeSet d_lemmasAdded;
+ TNodeSet d_disequalitiesAlreadySplit;
+
+ /** Backtracking mechanisms **/
+ std::vector<std::pair<TermId, InequalityEdge> > d_undoStack;
+ context::CDO<unsigned> d_undoStackIndex;
+
+ void contextNotifyPop() {
+ backtrack();
+ }
+
+ void backtrack();
+
+public:
+
+ InequalityGraph(context::Context* c, bool s = false)
+ : ContextNotifyObj(c),
+ d_context(c),
+ d_ineqNodes(),
+ d_ineqEdges(),
+ d_inConflict(c, false),
+ d_conflict(),
+ d_signed(s),
+ d_modelValues(c),
+ d_disequalities(c),
+ d_disequalitiesToSplit(c),
+ d_diseqToSplitIndex(c, 0),
+ d_disequalitiesAlreadySplit(),
+ d_undoStack(),
+ d_undoStackIndex(c)
+ {}
+ /**
+ * Add a new inequality to the graph
+ *
+ * @param a
+ * @param b
+ * @param strict
+ * @param reason
+ *
+ * @return
+ */
+ bool addInequality(TNode a, TNode b, bool strict, TNode reason);
+ /**
+ * Add a new disequality to the graph. This may lead in a lemma.
+ *
+ * @param a
+ * @param b
+ * @param reason
+ *
+ * @return
+ */
+ bool addDisequality(TNode a, TNode b, TNode reason);
+ void getConflict(std::vector<TNode>& conflict);
+ virtual ~InequalityGraph() throw(AssertionException) {}
+ /**
+ * Get any new lemmas (resulting from disequalities splits) that need
+ * to be added.
+ *
+ * @param new_lemmas
+ */
+ void getNewLemmas(std::vector<Node>& new_lemmas);
+ /**
+ * Check that the currently asserted disequalities that have not been split on
+ * are still true in the current model.
+ */
+ void checkDisequalities();
+ /**
+ * Return true if a < b is entailed by the current set of assertions.
+ *
+ * @param a
+ * @param b
+ *
+ * @return
+ */
+ bool isLessThan(TNode a, TNode b);
+ /**
+ * Returns true if the term has a value in the model (i.e. if we have seen it)
+ *
+ * @param a
+ *
+ * @return
+ */
+ bool hasValueInModel(TNode a) const;
+ /**
+ * Return the value of a in the current model.
+ *
+ * @param a
+ *
+ * @return
+ */
++ BitVector getValueInModel(TNode a) const;
++
++ void getAllValuesInModel(std::vector<Node>& assignments);
+};
+
+}
+}
+}
+
+#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
SubtheorySolver(context::Context* c, TheoryBV* bv) :
d_context(c),
- d_bv(bv)
+ d_bv(bv),
+ d_assertionQueue(c),
+ d_assertionIndex(c, 0)
{}
virtual ~SubtheorySolver() {}
-
- virtual bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) = 0;
- virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
- virtual void preRegister(TNode node) {}
- virtual void collectModelInfo(TheoryModel* m) = 0;
+ virtual bool check(Theory::Effort e) = 0;
+ virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
+ virtual void preRegister(TNode node) {}
+ virtual void propagate(Theory::Effort e) {}
+ virtual void collectModelInfo(TheoryModel* m) = 0;
++ virtual Node getModelValue(TNode var) = 0;
+ virtual bool isComplete() = 0;
+ virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
+ virtual void addSharedTerm(TNode node) {}
+ bool done() { return d_assertionQueue.size() == d_assertionIndex; }
+ TNode get() {
+ Assert (!done());
+ TNode res = d_assertionQueue[d_assertionIndex];
+ d_assertionIndex = d_assertionIndex + 1;
+ return res;
+ }
+ virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
};
}
d_bitblaster->explain(literal, assumptions);
}
-bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
- Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
+bool BitblastSolver::check(Theory::Effort e) {
++ Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
+ ++(d_statistics.d_numCallstoCheck);
//// Eager bit-blasting
if (options::bitvectorEagerBitblast()) {
- for (unsigned i = 0; i < assertions.size(); ++i) {
- TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i];
+ while (!done()) {
+ TNode assertion = get();
+ TNode atom = assertion.getKind() == kind::NOT ? assertion[0] : assertion;
if (atom.getKind() != kind::BITVECTOR_BITOF) {
d_bitblaster->bbAtom(atom);
}
d_bitblastQueue.pop();
}
- // propagation
- for (unsigned i = 0; i < assertions.size(); ++i) {
- TNode fact = assertions[i];
- if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) {
+ // Processing assertions
+ while (!done()) {
- TNode fact = get();
++ TNode fact = get();
++ Debug("bv-bitblast") << " fact " << fact << ")\n";
+ if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
// Some atoms have not been bit-blasted yet
d_bitblaster->bbAtom(fact);
// Assert to sat
~BitblastSolver();
void preRegister(TNode node);
- bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+ bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
EqualityStatus getEqualityStatus(TNode a, TNode b);
- void collectModelInfo(TheoryModel* m);
+ void collectModelInfo(TheoryModel* m);
+ Node getModelValue(TNode node);
+ bool isComplete() { return true; }
};
}
--- /dev/null
-
-
+/********************* */
+/*! \file bv_subtheory_eq.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): lianah
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#include "theory/bv/bv_subtheory_core.h"
+
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/slicer.h"
+#include "theory/model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace CVC4::theory::bv::utils;
+
+CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
+ : SubtheorySolver(c, bv),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
+ d_slicer(new Slicer(c, this)),
+ d_isCoreTheory(c, true),
+ d_reasons(c)
+{
+ if (d_useEqualityEngine) {
+
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
+ d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
+ d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
+ d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
+ }
+}
+
+CoreSolver::~CoreSolver() {
+ delete d_slicer;
+}
+void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
+void CoreSolver::preRegister(TNode node) {
+ if (!d_useEqualityEngine)
+ return;
+
+ if (node.getKind() == kind::EQUAL) {
+ d_equalityEngine.addTriggerEquality(node);
+ // d_slicer->processEquality(node);
+ } else {
+ d_equalityEngine.addTerm(node);
+ }
+}
+
+
+void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
+ bool polarity = literal.getKind() != kind::NOT;
+ TNode atom = polarity ? literal : literal[0];
+ if (atom.getKind() == kind::EQUAL) {
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ } else {
+ d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+ }
+}
+
+Node CoreSolver::getBaseDecomposition(TNode a, std::vector<TNode>& explanation) {
+ std::vector<Node> a_decomp;
+ d_slicer->getBaseDecomposition(a, a_decomp, explanation);
+ Node new_a = utils::mkConcat(a_decomp);
+ Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n";
+ return new_a;
+}
+
+bool CoreSolver::decomposeFact(TNode fact) {
+ Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
+ // assert decompositions since the equality engine does not know the semantics of
+ // concat:
+ // a == a_1 concat ... concat a_k
+ // b == b_1 concat ... concat b_k
+
+ if (fact.getKind() == kind::EQUAL) {
+ TNode a = fact[0];
+ TNode b = fact[1];
+
+ d_slicer->processEquality(fact);
+ std::vector<TNode> explanation_a;
+ Node new_a = getBaseDecomposition(a, explanation_a);
+ Node reason_a = mkAnd(explanation_a);
+ d_reasons.insert(reason_a);
+
+ std::vector<TNode> explanation_b;
+ Node new_b = getBaseDecomposition(b, explanation_b);
+ Node reason_b = mkAnd(explanation_b);
+ d_reasons.insert(reason_b);
+
+ std::vector<Node> explanation;
+ explanation.push_back(fact);
+ explanation.insert(explanation.end(), explanation_a.begin(), explanation_a.end());
+ explanation.insert(explanation.end(), explanation_b.begin(), explanation_b.end());
+
+ Node reason = utils::mkAnd(explanation);
+ d_reasons.insert(reason);
+
+ Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
+ utils::getSize(new_a) == utils::getSize(a));
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
+ Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
+
+ bool ok = true;
+ ok = assertFactToEqualityEngine(a_eq_new_a, reason_a);
+ if (!ok) return false;
+ ok = assertFactToEqualityEngine(b_eq_new_b, reason_a);
+ if (!ok) return false;
+ // assert the individual equalities as well
+ // a_i == b_i
+ if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
+ new_b.getKind() == kind::BITVECTOR_CONCAT) {
+ Assert (new_a.getNumChildren() == new_b.getNumChildren());
+ for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
+ Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
+ // this reason is not very precise!!
+ ok = assertFactToEqualityEngine(eq_i, reason);
+ d_reasons.insert(eq_i);
+ if (!ok) return false;
+ }
+ }
+ // merge the two terms in the slicer as well
+ d_slicer->assertEquality(fact);
+ } else {
+ // still need to register the terms
+ d_slicer->processEquality(fact[0]);
+ TNode a = fact[0][0];
+ TNode b = fact[0][1];
+ std::vector<TNode> explanation_a;
+ Node new_a = getBaseDecomposition(a, explanation_a);
+ Node reason_a = explanation_a.empty()? mkTrue() : mkAnd(explanation_a);
+ assertFactToEqualityEngine(utils::mkNode(kind::EQUAL, a, new_a), reason_a);
+
+ std::vector<TNode> explanation_b;
+ Node new_b = getBaseDecomposition(b, explanation_b);
+ Node reason_b = explanation_b.empty()? mkTrue() : mkAnd(explanation_b);
+ assertFactToEqualityEngine(utils::mkNode(kind::EQUAL, b, new_b), reason_b);
+
+ d_reasons.insert(reason_a);
+ d_reasons.insert(reason_b);
+ }
+ // finally assert the actual fact to the equality engine
+ return assertFactToEqualityEngine(fact, fact);
+}
+
+bool CoreSolver::check(Theory::Effort e) {
+ Trace("bitvector::core") << "CoreSolver::check \n";
+ Assert (!d_bv->inConflict());
+ ++(d_statistics.d_numCallstoCheck);
+ bool ok = true;
+ std::vector<Node> core_eqs;
+ while (! done()) {
+ TNode fact = get();
+
+ // update whether we are in the core fragment
+ if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
+ d_isCoreTheory = false;
+ }
+
+ // only reason about equalities
+ if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
+ // ok = decomposeFact(fact);
+ ok = assertFactToEqualityEngine(fact, fact);
+ } else {
+ ok = assertFactToEqualityEngine(fact, fact);
+ }
+ if (!ok)
+ return false;
+ }
+
+ // make sure to assert the new splits
+ // std::vector<Node> new_splits;
+ // d_slicer->getNewSplits(new_splits);
+ // for (unsigned i = 0; i < new_splits.size(); ++i) {
+ // ok = assertFactToEqualityEngine(new_splits[i], utils::mkTrue());
+ // if (!ok)
+ // return false;
+ // }
++
++ // if we are sat and in full check attempt to construct a model
++ if (Theory::fullEffort(e) && isComplete()) {
++ buildModel();
++ }
++
+ return true;
+}
+
++void CoreSolver::buildModel() {
++ Debug("bv-core") << "CoreSolver::buildModel() \n";
++ d_modelValues.clear();
++ TNodeSet constants;
++ TNodeSet constants_in_eq_engine;
++ // collect constants in equality engine
++ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
++ while (!eqcs_i.isFinished()) {
++ TNode repr = *eqcs_i;
++ if (repr.getKind() == kind::CONST_BITVECTOR) {
++ // must check if it's just the constant
++ eq::EqClassIterator it(repr, &d_equalityEngine);
++ if (!(++it).isFinished()) {
++ constants.insert(repr);
++ constants_in_eq_engine.insert(repr);
++ }
++ }
++ ++eqcs_i;
++ }
++ // build repr to value map
++
++ eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
++ while (!eqcs_i.isFinished()) {
++ TNode repr = *eqcs_i;
++ ++eqcs_i;
++ TypeNode type = repr.getType();
++ if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
++ Debug("bv-core-model") << " processing " << repr <<"\n";
++ // we need to assign a value for it
++ TypeEnumerator te(type);
++ Node val;
++ do {
++ val = *te;
++ ++te;
++ // Debug("bv-core-model") << " trying value " << val << "\n";
++ // Debug("bv-core-model") << " is in set? " << constants.count(val) << "\n";
++ // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n";
++ } while (constants.count(val) != 0 && !(te.isFinished()));
++
++ if (te.isFinished() && constants.count(val) != 0) {
++ // if we cannot enumerate anymore values we just return the lemma stating that
++ // at least two of the representatives are equal.
++ std::vector<TNode> representatives;
++ representatives.push_back(repr);
++
++ for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
++ it != constants_in_eq_engine.end(); ++it) {
++ TNode constant = *it;
++ if (utils::getSize(constant) == utils::getSize(repr)) {
++ representatives.push_back(constant);
++ }
++ }
++ for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
++ representatives.push_back(it->first);
++ }
++ std::vector<Node> equalities;
++ for (unsigned i = 0; i < representatives.size(); ++i) {
++ for (unsigned j = i + 1; j < representatives.size(); ++j) {
++ TNode a = representatives[i];
++ TNode b = representatives[j];
++ if (utils::getSize(a) == utils::getSize(b)) {
++ equalities.push_back(utils::mkNode(kind::EQUAL, a, b));
++ }
++ }
++ }
++ Node lemma = utils::mkOr(equalities);
++ d_bv->lemma(lemma);
++ Debug("bv-core") << " lemma: " << lemma << "\n";
++ return;
++ }
++ Debug("bv-core-model") << " " << repr << " => " << val <<"\n" ;
++ constants.insert(val);
++ d_modelValues[repr] = val;
++ }
++ }
++}
++
+bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
+ // Notify the equality engine
+ if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
+ Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
+ // Debug("bv-slicer-eq") << " reason=" << reason << endl;
+ bool negated = fact.getKind() == kind::NOT;
+ TNode predicate = negated ? fact[0] : fact;
+ if (predicate.getKind() == kind::EQUAL) {
+ if (negated) {
+ // dis-equality
+ d_equalityEngine.assertEquality(predicate, false, reason);
+ } else {
+ // equality
+ d_equalityEngine.assertEquality(predicate, true, reason);
+ }
+ } else {
+ // Adding predicate if the congruence over it is turned on
+ if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
+ d_equalityEngine.assertPredicate(predicate, !negated, reason);
+ }
+ }
+ }
+
+ // checking for a conflict
+ if (d_bv->inConflict()) {
+ return false;
+ }
+ return true;
+}
+
+bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
+ Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+ if (value) {
+ return d_solver.storePropagation(equality);
+ } else {
+ return d_solver.storePropagation(equality.notNode());
+ }
+}
+
+bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
+ Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
+ if (value) {
+ return d_solver.storePropagation(predicate);
+ } else {
+ return d_solver.storePropagation(predicate.notNode());
+ }
+}
+
+bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+ Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+ if (value) {
+ return d_solver.storePropagation(t1.eqNode(t2));
+ } else {
+ return d_solver.storePropagation(t1.eqNode(t2).notNode());
+ }
+}
+
+void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+ d_solver.conflict(t1, t2);
+}
+
+bool CoreSolver::storePropagation(TNode literal) {
+ return d_bv->storePropagation(literal, SUB_CORE);
+}
+
+void CoreSolver::conflict(TNode a, TNode b) {
+ std::vector<TNode> assumptions;
+ d_equalityEngine.explainEquality(a, b, true, assumptions);
+ Node conflict = flattenAnd(assumptions);
+ d_bv->setConflict(conflict);
+}
+
+void CoreSolver::collectModelInfo(TheoryModel* m) {
+ if (Debug.isOn("bitvector-model")) {
+ context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
+ for (; it!= d_assertionQueue.end(); ++it) {
+ Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
+ << *it << ")\n";
+ }
+ }
+ set<Node> termSet;
+ d_bv->computeRelevantTerms(termSet);
+ m->assertEqualityEngine(&d_equalityEngine, &termSet);
++ if (isComplete()) {
++ Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
++ for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
++ Node a = it->first;
++ Node b = it->second;
++ m->assertEquality(a, b, true);
++ }
++ }
++}
++
++Node CoreSolver::getModelValue(TNode var) {
++ Assert (isComplete());
++ Assert (d_modelValues.find(var) != d_modelValues.end());
++ return d_modelValues[d_equalityEngine.getRepresentative(var)];
+}
+
+CoreSolver::Statistics::Statistics()
+ : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
+{
+ StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+CoreSolver::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
--- /dev/null
- context::CDHashSet<Node, NodeHashFunction> d_reasons;
+/********************* */
+/*! \file bv_subtheory_eq.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): lianah, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#pragma once
+
+#include "cvc4_private.h"
+#include "theory/bv/bv_subtheory.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class Slicer;
+class Base;
+/**
+ * Bitvector equality solver
+ */
+class CoreSolver : public SubtheorySolver {
++ typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
++ typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
++
+ struct Statistics {
+ IntStat d_numCallstoCheck;
+ Statistics();
+ ~Statistics();
+ };
+
+ // NotifyClass: handles call-back from congruence closure module
+ class NotifyClass : public eq::EqualityEngineNotify {
+ CoreSolver& d_solver;
+
+ public:
+ NotifyClass(CoreSolver& solver): d_solver(solver) {}
+ bool eqNotifyTriggerEquality(TNode equality, bool value);
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+ bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2);
+ void eqNotifyNewClass(TNode t) { }
+ void eqNotifyPreMerge(TNode t1, TNode t2) { }
+ void eqNotifyPostMerge(TNode t1, TNode t2) { }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+ };
+
+
+ /** The notify class for d_equalityEngine */
+ NotifyClass d_notify;
+
+ /** Equality engine */
+ eq::EqualityEngine d_equalityEngine;
+
+ /** Store a propagation to the bv solver */
+ bool storePropagation(TNode literal);
+
+ /** Store a conflict from merging two constants */
+ void conflict(TNode a, TNode b);
+
+ Slicer* d_slicer;
+ context::CDO<bool> d_isCoreTheory;
+ /** To make sure we keep the explanations */
++ context::CDHashSet<Node, NodeHashFunction> d_reasons;
++ ModelValue d_modelValues;
++ void buildModel();
+ bool assertFactToEqualityEngine(TNode fact, TNode reason);
+ bool decomposeFact(TNode fact);
+ Node getBaseDecomposition(TNode a, std::vector<TNode>& explanation);
+ Statistics d_statistics;
+public:
+ CoreSolver(context::Context* c, TheoryBV* bv);
+ ~CoreSolver();
+ bool isComplete() { return d_isCoreTheory; }
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void preRegister(TNode node);
+ bool check(Theory::Effort e);
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+ void collectModelInfo(TheoryModel* m);
++ Node getModelValue(TNode var);
+ void addSharedTerm(TNode t) {
+ d_equalityEngine.addTriggerTerm(t, THEORY_BV);
+ }
+ EqualityStatus getEqualityStatus(TNode a, TNode b) {
+ if (d_equalityEngine.areEqual(a, b)) {
+ // The terms are implied to be equal
+ return EQUALITY_TRUE;
+ }
+ if (d_equalityEngine.areDisequal(a, b, false)) {
+ // The terms are implied to be dis-equal
+ return EQUALITY_FALSE;
+ }
+ return EQUALITY_UNKNOWN;
+ }
+ bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
+ void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); }
+};
+
+
+}
+}
+}
--- /dev/null
+/********************* */
+/*! \file bv_subtheory_inequality.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#include "theory/bv/bv_subtheory_inequality.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace CVC4::theory::bv::utils;
+
+bool InequalitySolver::check(Theory::Effort e) {
+ Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
+ ++(d_statistics.d_numCallstoCheck);
+
+ bool ok = true;
+ while (!done() && ok) {
+ TNode fact = get();
+ Debug("bv-subtheory-inequality") << " "<< fact <<"\n";
+ if (fact.getKind() == kind::EQUAL) {
+ TNode a = fact[0];
+ TNode b = fact[1];
+ ok = d_inequalityGraph.addInequality(a, b, false, fact);
+ if (ok)
+ ok = d_inequalityGraph.addInequality(b, a, false, fact);
+ } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
+ TNode a = fact[0][0];
+ TNode b = fact[0][1];
+ ok = d_inequalityGraph.addDisequality(a, b, fact);
+ }
+ if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
+ TNode a = fact[0][1];
+ TNode b = fact[0][0];
+ ok = d_inequalityGraph.addInequality(a, b, true, fact);
+ } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
+ TNode a = fact[0][1];
+ TNode b = fact[0][0];
+ ok = d_inequalityGraph.addInequality(a, b, false, fact);
+ } else if (fact.getKind() == kind::BITVECTOR_ULT) {
+ TNode a = fact[0];
+ TNode b = fact[1];
+ ok = d_inequalityGraph.addInequality(a, b, true, fact);
+ } else if (fact.getKind() == kind::BITVECTOR_ULE) {
+ TNode a = fact[0];
+ TNode b = fact[1];
+ ok = d_inequalityGraph.addInequality(a, b, false, fact);
+ }
+ }
+
+ if (!ok) {
+ std::vector<TNode> conflict;
+ d_inequalityGraph.getConflict(conflict);
+ d_bv->setConflict(utils::flattenAnd(conflict));
+ return false;
+ }
+
+ // make sure all the disequalities we didn't split on are still satisifed
+ // and split on the ones that are not
+ d_inequalityGraph.checkDisequalities();
+
+ // send out any lemmas
+ std::vector<Node> lemmas;
+ d_inequalityGraph.getNewLemmas(lemmas);
+ for(unsigned i = 0; i < lemmas.size(); ++i) {
+ d_bv->lemma(lemmas[i]);
+ }
+ return true;
+}
+
+EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) {
+ Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
+ Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
+
+ // if an inequality containing the terms has been asserted then we know
+ // the equality is false
+ if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) {
+ return EQUALITY_FALSE;
+ }
+
+ if (!d_inequalityGraph.hasValueInModel(a) ||
+ !d_inequalityGraph.hasValueInModel(b)) {
+ return EQUALITY_UNKNOWN;
+ }
+
+ // TODO: check if this disequality is entailed by inequalities via transitivity
+
+ BitVector a_val = d_inequalityGraph.getValueInModel(a);
+ BitVector b_val = d_inequalityGraph.getValueInModel(b);
+
+ if (a_val == b_val) {
+ return EQUALITY_TRUE_IN_MODEL;
+ } else {
+ return EQUALITY_FALSE_IN_MODEL;
+ }
+}
+
+void InequalitySolver::assertFact(TNode fact) {
+ d_assertionQueue.push_back(fact);
+ d_assertionSet.insert(fact);
+ if (!isInequalityOnly(fact)) {
+ d_isComplete = false;
+ }
+}
+
+bool InequalitySolver::isInequalityOnly(TNode node) {
+ if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) {
+ return d_ineqTermCache[node];
+ }
+
+ if (node.getKind() == kind::NOT) {
+ node = node[0];
+ }
+
+ if (node.getKind() != kind::EQUAL &&
+ node.getKind() != kind::BITVECTOR_ULT &&
+ node.getKind() != kind::BITVECTOR_ULE &&
+ node.getKind() != kind::CONST_BITVECTOR &&
+ node.getKind() != kind::SELECT &&
+ node.getKind() != kind::STORE &&
+ node.getMetaKind() != kind::metakind::VARIABLE) {
+ return false;
+ }
+ bool res = true;
+ for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+ res = res && isInequalityOnly(node[i]);
+ }
+ d_ineqTermCache[node] = res;
+ return res;
+}
+
+void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
+ Assert (false);
+}
+
+void InequalitySolver::propagate(Theory::Effort e) {
+ Assert (false);
+}
+
++void InequalitySolver::collectModelInfo(TheoryModel* m) {
++ Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
++ std::vector<Node> model;
++ d_inequalityGraph.getAllValuesInModel(model);
++ for (unsigned i = 0; i < model.size(); ++i) {
++ Assert (model[i].getKind() == kind::EQUAL);
++ m->assertEquality(model[i][0], model[i][1], true);
++ }
++}
++
++Node InequalitySolver::getModelValue(TNode var) {
++ Assert (isComplete());
++ Assert (d_inequalityGraph.hasValueInModel(var));
++ BitVector val = d_inequalityGraph.getValueInModel(var);
++ return utils::mkConst(val);
++}
++
+InequalitySolver::Statistics::Statistics()
+ : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
+{
+ StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+InequalitySolver::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
+
--- /dev/null
- void collectModelInfo(TheoryModel* m) {}
+/********************* */
+/*! \file bv_subtheory_inequality.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+
+#include "theory/bv/bv_subtheory.h"
+#include "theory/bv/bv_inequality_graph.h"
+#include "context/cdhashset.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class InequalitySolver: public SubtheorySolver {
+ struct Statistics {
+ IntStat d_numCallstoCheck;
+ Statistics();
+ ~Statistics();
+ };
+
+ context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
+ InequalityGraph d_inequalityGraph;
+ context::CDO<bool> d_isComplete;
+ __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache;
+ bool isInequalityOnly(TNode node);
+ Statistics d_statistics;
+public:
+ InequalitySolver(context::Context* c, TheoryBV* bv)
+ : SubtheorySolver(c, bv),
+ d_assertionSet(c),
+ d_inequalityGraph(c),
+ d_isComplete(c, true),
+ d_ineqTermCache(),
+ d_statistics()
+ {}
+
+ bool check(Theory::Effort e);
+ void propagate(Theory::Effort e);
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+ bool isComplete() { return d_isComplete; }
++ void collectModelInfo(TheoryModel* m);
++ Node getModelValue(TNode var);
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+ void assertFact(TNode fact);
+};
+
+}
+}
+}
+
+#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool
check the bitblasting eagerly
++option bitvectorInequalitySolver --bv-inequality-solver bool
++ turn on the inequality solver for the bit-vector theory
endmodule
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
d_propagatedBy(c)
- {}
-
-TheoryBV::~TheoryBV() {}
+ {
+ SubtheorySolver* core_solver = new CoreSolver(c, this);
+ d_subtheories.push_back(core_solver);
+ d_subtheoryMap[SUB_CORE] = core_solver;
+
- SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
- d_subtheories.push_back(ineq_solver);
- d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
-
++ if (options::bitvectorInequalitySolver()) {
++ SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
++ d_subtheories.push_back(ineq_solver);
++ d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
++ }
++
+ SubtheorySolver* bb_solver = new BitblastSolver(c, this);
+ d_subtheories.push_back(bb_solver);
+ d_subtheoryMap[SUB_BITBLAST] = bb_solver;
+ }
+TheoryBV::~TheoryBV() {
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+ delete d_subtheories[i];
+ }
+}
void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_equalitySolver.setMasterEqualityEngine(eq);
+ dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
}
TheoryBV::Statistics::Statistics():
void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
Assert(!inConflict());
// Assert (fullModel); // can only query full model
- d_equalitySolver.collectModelInfo(m);
- d_bitblastSolver.collectModelInfo(m);
-
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- d_subtheories[i]->collectModelInfo(m);
++ if (d_subtheories[i]->isComplete()) {
++ d_subtheories[i]->collectModelInfo(m);
++ return;
++ }
++ }
+ }
+
+ Node TheoryBV::getModelValue(TNode var) {
+ Assert(!inConflict());
- return d_bitblastSolver.getModelValue(var);
++ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
++ if (d_subtheories[i]->isComplete()) {
++ return d_subtheories[i]->getModelValue(var);
++ }
+ }
++ Unreachable();
}
-
void TheoryBV::propagate(Effort e) {
Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
return bv.isPow2();
}
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
++inline Node mkOr(const std::vector<Node>& nodes) {
++ std::set<TNode> all;
++ all.insert(nodes.begin(), nodes.end());
++
++ if (all.size() == 0) {
++ return mkTrue();
++ }
++
++ if (all.size() == 1) {
++ // All the same, or just one
++ return nodes[0];
++ }
++
++
++ NodeBuilder<> disjunction(kind::OR);
++ std::set<TNode>::const_iterator it = all.begin();
++ std::set<TNode>::const_iterator it_end = all.end();
++ while (it != it_end) {
++ disjunction << *it;
++ ++ it;
++ }
++
++ return disjunction;
++}/* mkOr() */
++
++
+inline Node mkAnd(const std::vector<TNode>& conjunctions) {
+ std::set<TNode> all;
+ all.insert(conjunctions.begin(), conjunctions.end());
+
+ if (all.size() == 0) {
+ return mkTrue();
+ }
+
+ if (all.size() == 1) {
+ // All the same, or just one
+ return conjunctions[0];
+ }
+
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
+}/* mkAnd() */
+
+inline Node mkAnd(const std::vector<Node>& conjunctions) {
+ std::set<TNode> all;
+ all.insert(conjunctions.begin(), conjunctions.end());
+
+ if (all.size() == 0) {
+ return mkTrue();
+ }
+
+ if (all.size() == 1) {
+ // All the same, or just one
+ return conjunctions[0];
+ }
+
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
+}/* mkAnd() */
+
+
+
+inline Node flattenAnd(std::vector<TNode>& queue) {
+ TNodeSet nodes;
+ while(!queue.empty()) {
+ TNode current = queue.back();
+ queue.pop_back();
+ if (current.getKind() == kind::AND) {
+ for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+ if (nodes.count(current[i]) == 0) {
+ queue.push_back(current[i]);
+ }
+ }
+ } else {
+ nodes.insert(current);
+ }
+ }
+ std::vector<TNode> children;
+ for (TNodeSet::const_iterator it = nodes.begin(); it!= nodes.end(); ++it) {
+ children.push_back(*it);
+ }
+ return mkAnd(children);
+}
+
+
// neeed a better name, this is not technically a ground term
inline bool isBVGroundTerm(TNode node) {
if (node.getNumChildren() == 0) {
projects / cvc5.git / commitdiff