Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_inequality_graph.cpp	Lines:	284	300	94.7 %
Date:	2021-05-22	Branches:	510	1247	40.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Aina Niemetz, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * 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 cvc5;
using namespace cvc5::context;
using namespace cvc5::theory;
using namespace cvc5::theory::bv;
using namespace cvc5::theory::bv::utils;

const TermId cvc5::theory::bv::UndefinedTermId = -1;
const ReasonId cvc5::theory::bv::UndefinedReasonId = -1;
const ReasonId cvc5::theory::bv::AxiomReasonId = -2;

bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
  Debug("bv-inequality") << "InequalityGraph::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 processing " << 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);
        Assert(hasModelValue(start));
        ReasonId start_reason = getModelValue(start).reason;
        if (start_reason != UndefinedReasonId) {
          conflict.push_back(start_reason);
        }
        computeExplanation(UndefinedTermId, 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];
  }
  d_reasonSet.insert(reason);
  ReasonId id = d_reasonNodes.size();
  d_reasonNodes.push_back(reason);
  d_reasonToIdMap[reason] = id;
  Debug("bv-inequality-internal") << "InequalityGraph::registerReason " << reason << " => id"<< id << "\n";
  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::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();
  }
}

Node InequalityGraph::makeDiseqSplitLemma(TNode diseq)
{
  Assert(diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
  NodeManager* nm = NodeManager::currentNM();
  TNode a = diseq[0][0];
  TNode b = diseq[0][1];
  Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b);
  Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a);
  Node eq = diseq[0];
  Node lemma = nm->mkNode(kind::OR, a_lt_b, b_lt_a, eq);
  return lemma;
}

void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) {
  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)) {
        lemmas.push_back(makeDiseqSplitLemma(diseq));
        d_disequalitiesAlreadySplit.insert(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)
{
  NodeManager* nm = NodeManager::currentNM();
  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 = nm->mkNode(kind::EQUAL, var, constant);
    assignments.push_back(assignment);
    Debug("bitvector-model") << "   " << var << " => " << constant << "\n";
  }
}


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Liana Hadarean, Aina Niemetz, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* A graph representation of the currently asserted bv inequalities.
14		*/
15
16		#include "theory/bv/bv_inequality_graph.h"
17		#include "theory/bv/theory_bv_utils.h"
18
19		using namespace std;
20		using namespace cvc5;
21		using namespace cvc5::context;
22		using namespace cvc5::theory;
23		using namespace cvc5::theory::bv;
24		using namespace cvc5::theory::bv::utils;
25
26		const TermId cvc5::theory::bv::UndefinedTermId = -1;
27		const ReasonId cvc5::theory::bv::UndefinedReasonId = -1;
28		const ReasonId cvc5::theory::bv::AxiomReasonId = -2;
29
30	1158735	bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
31	1158735	Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n";
32
33	1158735	TermId id_a = registerTerm(a);
34	1158735	TermId id_b = registerTerm(b);
35	1158735	ReasonId id_reason = registerReason(reason);
36
37	1158735	Assert(!(isConst(id_a) && isConst(id_b)));
38	2317470	BitVector a_val = getValue(id_a);
39	2317470	BitVector b_val = getValue(id_b);
40
41	1158735	unsigned bitwidth = utils::getSize(a);
42	2317470	BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u);
43
44	1158735	if (a_val + diff < a_val) {
45		// we have an overflow
46	86	std::vector<ReasonId> conflict;
47	43	conflict.push_back(id_reason);
48	43	computeExplanation(UndefinedTermId, id_a, conflict);
49	43	setConflict(conflict);
50	43	return false;
51		}
52
53	1158692	if (a_val + diff <= b_val) {
54		// the inequality is true in the current partial model
55		// we still add the edge because it may not be true later (cardinality)
56	943029	addEdge(id_a, id_b, strict, id_reason);
57	943029	return true;
58		}
59
60	215663	if (isConst(id_b) && a_val + diff > b_val) {
61		// we must be in a conflict since a has the minimum value that
62		// satisifes the constraints
63	366	std::vector<ReasonId> conflict;
64	183	conflict.push_back(id_reason);
65	183	computeExplanation(UndefinedTermId, id_a, conflict);
66	183	Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant UB \n";
67	183	setConflict(conflict);
68	183	return false;
69		}
70
71		// add the inequality edge
72	215480	addEdge(id_a, id_b, strict, id_reason);
73	430960	BFSQueue queue(&d_modelValues);
74	215480	Assert(hasModelValue(id_a));
75	215480	queue.push(id_a);
76	215480	return processQueue(queue, id_a);
77		}
78
79	4310493	bool InequalityGraph::updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed) {
80	8620986	BitVector lower_bound = new_mv.value;
81
82	4310493	if (isConst(id)) {
83	112798	if (getValue(id) < lower_bound) {
84	209	Debug("bv-inequality") << "Conflict: constant " << getValue(id) << "\n";
85	418	std::vector<ReasonId> conflict;
86	209	TermId parent = new_mv.parent;
87	209	ReasonId reason = new_mv.reason;
88	209	conflict.push_back(reason);
89	209	computeExplanation(UndefinedTermId, parent, conflict);
90	209	Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant\n";
91	209	setConflict(conflict);
92	209	return false;
93		}
94		} else {
95		// if not constant we can try to update the value
96	4197695	if (getValue(id) < lower_bound) {
97		// if we are updating the term we started with we must be in a cycle
98	229996	if (id == start) {
99	153	TermId parent = new_mv.parent;
100	153	ReasonId reason = new_mv.reason;
101	306	std::vector<TermId> conflict;
102	153	conflict.push_back(reason);
103	153	computeExplanation(id, parent, conflict);
104	153	Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n";
105	153	setConflict(conflict);
106	153	return false;
107		}
108	459686	Debug("bv-inequality-internal") << "Updating " << getTermNode(id)
109	459686	<< " from " << getValue(id) << "\n"
110	229843	<< " to " << lower_bound << "\n";
111	229843	changed = true;
112	229843	setModelValue(id, new_mv);
113		}
114		}
115	4310131	return true;
116		}
117
118	660315	bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
119	1105150	while (!queue.empty()) {
120	445227	TermId current = queue.top();
121	445227	queue.pop();
122	445227	Debug("bv-inequality-internal") << "InequalityGraph::processQueue processing " << getTermNode(current) << "\n";
123
124	890062	BitVector current_value = getValue(current);
125
126	445227	unsigned size = getBitwidth(current);
127	890062	const BitVector zero(size, 0u);
128	890062	const BitVector one(size, 1u);
129
130	445227	const Edges& edges = getEdges(current);
131	4755358	for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
132	4310523	TermId next = it->next;
133	4310523	ReasonId reason = it->reason;
134
135	4540366	const BitVector increment = it->strict ? one : zero;
136	4540366	const BitVector next_lower_bound = current_value + increment;
137
138	4310523	if (next_lower_bound < current_value) {
139		// it means we have an overflow and hence a conflict
140	60	std::vector<TermId> conflict;
141	30	conflict.push_back(it->reason);
142	30	Assert(hasModelValue(start));
143	30	ReasonId start_reason = getModelValue(start).reason;
144	30	if (start_reason != UndefinedReasonId) {
145	4	conflict.push_back(start_reason);
146		}
147	30	computeExplanation(UndefinedTermId, current, conflict);
148	30	Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n";
149	30	setConflict(conflict);
150	30	return false;
151		}
152
153	4540336	ModelValue new_mv(next_lower_bound, current, reason);
154	4310493	bool updated = false;
155	4310493	if (!updateValue(next, new_mv, start, updated)) {
156	362	return false;
157		}
158
159	4421039	if (next == start) {
160		// we know what we didn't update start or we would have had a conflict
161		// this means we are in a cycle where all the values are forced to be equal
162	110908	Debug("bv-inequality-internal") << "InequalityGraph::processQueue equal cycle.";
163	110908	continue;
164		}
165
166	8168603	if (!updated) {
167		// if we didn't update current we don't need to add to the queue it's children
168	3969380	Debug("bv-inequality-internal") << " unchanged " << getTermNode(next) << "\n";
169	3969380	continue;
170		}
171
172	229843	queue.push(next);
173	229843	Debug("bv-inequality-internal") << " enqueue " << getTermNode(next) << "\n";
174		}
175		}
176	215088	return true;
177		}
178
179	15701	void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation) {
180	15701	if(Debug.isOn("bv-inequality")) {
181		if (from == UndefinedTermId) {
182		Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(to) << "\n";
183		} else {
184		Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(from) <<" => "
185		<< getTermNode(to) << "\n";
186		}
187		}
188
189	31402	TermIdSet seen;
190
191	17339	while(hasReason(to) && from != to && !seen.count(to)) {
192	819	seen.insert(to);
193	1638	const ModelValue& exp = getModelValue(to);
194	819	Assert(exp.reason != UndefinedReasonId);
195	819	explanation.push_back(exp.reason);
196	819	Assert(exp.parent != UndefinedTermId);
197	819	to = exp.parent;
198	1638	Debug("bv-inequality-internal") << " parent: " << getTermNode(to) << "\n"
199	819	<< " reason: " << getReasonNode(exp.reason) << "\n";
200		}
201	15701	}
202
203	1158509	void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) {
204	2317018	Debug("bv-inequality-internal") << "InequalityGraph::addEdge " << getTermNode(a) << " => " << getTermNode(b) << "\n"
205	1158509	<< " strict ? " << strict << "\n";
206	1158509	Edges& edges = getEdges(a);
207	1158509	InequalityEdge new_edge(b, strict, reason);
208	1158509	edges.push_back(new_edge);
209	1158509	d_undoStack.push_back(std::make_pair(a, new_edge));
210	1158509	d_undoStackIndex = d_undoStackIndex + 1;
211	1158509	}
212
213	927954	void InequalityGraph::initializeModelValue(TNode node) {
214	927954	TermId id = getTermId(node);
215	927954	Assert(!hasModelValue(id));
216	927954	bool isConst = node.getKind() == kind::CONST_BITVECTOR;
217	927954	unsigned size = utils::getSize(node);
218	1855908	BitVector value = isConst? node.getConst<BitVector>() : BitVector(size, 0u);
219	927954	setModelValue(id, ModelValue(value, UndefinedTermId, UndefinedReasonId));
220	927954	}
221
222	678577	bool InequalityGraph::isRegistered(TNode term) const {
223	678577	return d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end();
224		}
225
226	2317504	TermId InequalityGraph::registerTerm(TNode term) {
227	2317504	if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) {
228	2287872	TermId id = d_termNodeToIdMap[term];
229	2287872	if (!hasModelValue(id)) {
230		// we could have backtracked and
231	732862	initializeModelValue(term);
232		}
233	2287872	return id;
234		}
235
236		// store in node mapping
237	29632	TermId id = d_termNodes.size();
238	29632	Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << " => id"<< id << "\n";
239
240	29632	d_termNodes.push_back(term);
241	29632	d_termNodeToIdMap[term] = id;
242
243		// create InequalityNode
244	29632	unsigned size = utils::getSize(term);
245
246	29632	bool isConst = term.getKind() == kind::CONST_BITVECTOR;
247	29632	InequalityNode ineq = InequalityNode(id, size, isConst);
248
249	29632	Assert(d_ineqNodes.size() == id);
250	29632	d_ineqNodes.push_back(ineq);
251
252	29632	Assert(d_ineqEdges.size() == id);
253	29632	d_ineqEdges.push_back(Edges());
254
255	29632	initializeModelValue(term);
256
257	29632	return id;
258		}
259
260	1158735	ReasonId InequalityGraph::registerReason(TNode reason) {
261	1158735	if (d_reasonToIdMap.find(reason) != d_reasonToIdMap.end()) {
262	1115230	return d_reasonToIdMap[reason];
263		}
264	43505	d_reasonSet.insert(reason);
265	43505	ReasonId id = d_reasonNodes.size();
266	43505	d_reasonNodes.push_back(reason);
267	43505	d_reasonToIdMap[reason] = id;
268	43505	Debug("bv-inequality-internal") << "InequalityGraph::registerReason " << reason << " => id"<< id << "\n";
269	43505	return id;
270		}
271
272	2260	TNode InequalityGraph::getReasonNode(ReasonId id) const {
273	2260	Assert(d_reasonNodes.size() > id);
274	2260	return d_reasonNodes[id];
275		}
276
277	19597581	TNode InequalityGraph::getTermNode(TermId id) const {
278	19597581	Assert(d_termNodes.size() > id);
279	19597581	return d_termNodes[id];
280		}
281
282	1545660	TermId InequalityGraph::getTermId(TNode node) const {
283	1545660	Assert(d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end());
284	1545660	return d_termNodeToIdMap.find(node)->second;
285		}
286
287	618	void InequalityGraph::setConflict(const std::vector<ReasonId>& conflict) {
288	618	Assert(!d_inConflict);
289	618	d_inConflict = true;
290	618	d_conflict.clear();
291	1862	for (unsigned i = 0; i < conflict.size(); ++i) {
292	1244	if (conflict[i] != AxiomReasonId) {
293	1244	d_conflict.push_back(getReasonNode(conflict[i]));
294		}
295		}
296	618	if (Debug.isOn("bv-inequality")) {
297		Debug("bv-inequality") << "InequalityGraph::setConflict \n";
298		for (unsigned i = 0; i < d_conflict.size(); ++i) {
299		Debug("bv-inequality") << " " << d_conflict[i] <<"\n";
300		}
301		}
302	618	}
303
304	618	void InequalityGraph::getConflict(std::vector<TNode>& conflict) {
305	1862	for (unsigned i = 0; i < d_conflict.size(); ++i) {
306	1244	conflict.push_back(d_conflict[i]);
307		}
308	618	}
309
310	1157797	void InequalityGraph::setModelValue(TermId term, const ModelValue& mv) {
311	1157797	d_modelValues[term] = mv;
312	1157797	}
313
314	17369	InequalityGraph::ModelValue InequalityGraph::getModelValue(TermId term) const {
315	17369	Assert(d_modelValues.find(term) != d_modelValues.end());
316	17369	return (*(d_modelValues.find(term))).second;
317		}
318
319	11970024	bool InequalityGraph::hasModelValue(TermId id) const {
320	11970024	return d_modelValues.find(id) != d_modelValues.end();
321		}
322
323	7920982	BitVector InequalityGraph::getValue(TermId id) const {
324	7920982	Assert(hasModelValue(id));
325	7920982	return (*(d_modelValues.find(id))).second.value;
326		}
327
328	16520	bool InequalityGraph::hasReason(TermId id) const {
329	33040	const ModelValue& mv = getModelValue(id);
330	33040	return mv.reason != UndefinedReasonId;
331		}
332
333	361684	bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
334	361684	Debug("bv-inequality") << "InequalityGraph::addDisequality " << reason << "\n";
335	361684	d_disequalities.push_back(reason);
336
337	361684	if (!isRegistered(a) \|\| !isRegistered(b)) {
338		//splitDisequality(reason);
339	52831	return true;
340		}
341	308853	TermId id_a = getTermId(a);
342	308853	TermId id_b = getTermId(b);
343	308853	if (!hasModelValue(id_a)) {
344	94985	initializeModelValue(a);
345		}
346	308853	if (!hasModelValue(id_b)) {
347	70475	initializeModelValue(b);
348		}
349	617706	const BitVector val_a = getValue(id_a);
350	617706	const BitVector val_b = getValue(id_b);
351	308853	if (val_a == val_b) {
352	106066	if (a.getKind() == kind::CONST_BITVECTOR) {
353		// then we know b cannot be smaller than the assigned value so we try to make it larger
354	1042	std::vector<ReasonId> explanation_ids;
355	521	computeExplanation(UndefinedTermId, id_b, explanation_ids);
356	1042	std::vector<TNode> explanation_nodes;
357	521	explanation_nodes.push_back(reason);
358	575	for (unsigned i = 0; i < explanation_ids.size(); ++i) {
359	54	explanation_nodes.push_back(getReasonNode(explanation_ids[i]));
360		}
361	1042	Node explanation = utils::mkAnd(explanation_nodes);
362	521	d_reasonSet.insert(explanation);
363	521	return addInequality(a, b, true, explanation);
364		}
365	105545	if (b.getKind() == kind::CONST_BITVECTOR) {
366		// then we know b cannot be smaller than the assigned value so we try to make it larger
367	29124	std::vector<ReasonId> explanation_ids;
368	14562	computeExplanation(UndefinedTermId, id_a, explanation_ids);
369	29124	std::vector<TNode> explanation_nodes;
370	14562	explanation_nodes.push_back(reason);
371	14705	for (unsigned i = 0; i < explanation_ids.size(); ++i) {
372	143	explanation_nodes.push_back(getReasonNode(explanation_ids[i]));
373		}
374	29124	Node explanation = utils::mkAnd(explanation_nodes);
375	14562	d_reasonSet.insert(explanation);
376	14562	return addInequality(b, a, true, explanation);
377		}
378		// if none of the terms are constants just add the lemma
379		//splitDisequality(reason);
380		} else {
381	405574	Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n"
382	202787	<< " " << b << " => " << val_b.toString(10) << "\n";
383		}
384	293770	return true;
385		}
386
387		// void InequalityGraph::splitDisequality(TNode diseq) {
388		// Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " <<
389		// diseq <<"\n"; Assert (diseq.getKind() == kind::NOT &&
390		// diseq[0].getKind() == kind::EQUAL); if
391		// (d_disequalitiesAlreadySplit.find(diseq) ==
392		// d_disequalitiesAlreadySplit.end()) {
393		// d_disequalitiesToSplit.push_back(diseq);
394		// }
395		// }
396
397	2239992	void InequalityGraph::backtrack() {
398	2239992	Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n";
399	2239992	int size = d_undoStack.size();
400	3398501	for (int i = size - 1; i >= (int)d_undoStackIndex.get(); --i) {
401	1158509	Assert(!d_undoStack.empty());
402	1158509	TermId id = d_undoStack.back().first;
403	1158509	InequalityEdge edge = d_undoStack.back().second;
404	1158509	d_undoStack.pop_back();
405
406	2317018	Debug("bv-inequality-internal") << " remove edge " << getTermNode(id) << " => "
407	1158509	<< getTermNode(edge.next) <<"\n";
408	1158509	Edges& edges = getEdges(id);
409	11246787	for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
410	10088278	Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n";
411		}
412	1158509	Assert(!edges.empty());
413	1158509	Assert(edges.back() == edge);
414	1158509	edges.pop_back();
415		}
416	2239992	}
417
418	7	Node InequalityGraph::makeDiseqSplitLemma(TNode diseq)
419		{
420	7	Assert(diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
421	7	NodeManager* nm = NodeManager::currentNM();
422	14	TNode a = diseq[0][0];
423	14	TNode b = diseq[0][1];
424	14	Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b);
425	14	Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a);
426	14	Node eq = diseq[0];
427	7	Node lemma = nm->mkNode(kind::OR, a_lt_b, b_lt_a, eq);
428	14	return lemma;
429		}
430
431	44	void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) {
432	66	for (CDQueue<TNode>::const_iterator it = d_disequalities.begin(); it != d_disequalities.end(); ++it) {
433	22	if (d_disequalitiesAlreadySplit.find(*it) == d_disequalitiesAlreadySplit.end()) {
434		// if we haven't already split on this disequality
435	34	TNode diseq = *it;
436	17	TermId a_id = registerTerm(diseq[0][0]);
437	17	TermId b_id = registerTerm(diseq[0][1]);
438	17	if (getValue(a_id) == getValue(b_id)) {
439	7	lemmas.push_back(makeDiseqSplitLemma(diseq));
440	7	d_disequalitiesAlreadySplit.insert(diseq);
441		}
442		}
443		}
444	44	}
445
446		bool InequalityGraph::isLessThan(TNode a, TNode b) {
447		Assert(isRegistered(a) && isRegistered(b));
448		Unimplemented();
449		}
450
451	74	bool InequalityGraph::hasValueInModel(TNode node) const {
452	74	if (isRegistered(node)) {
453		TermId id = getTermId(node);
454		return hasModelValue(id);
455		}
456	74	return false;
457		}
458
459		BitVector InequalityGraph::getValueInModel(TNode node) const {
460		TermId id = getTermId(node);
461		Assert(hasModelValue(id));
462		return getValue(id);
463		}
464
465	31	void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments)
466		{
467	31	NodeManager* nm = NodeManager::currentNM();
468	186	for (ModelValues::const_iterator it = d_modelValues.begin();
469	186	it != d_modelValues.end();
470		++it)
471		{
472	155	TermId id = (*it).first;
473	310	BitVector value = (*it).second.value;
474	310	TNode var = getTermNode(id);
475	310	Node constant = utils::mkConst(value);
476	310	Node assignment = nm->mkNode(kind::EQUAL, var, constant);
477	155	assignments.push_back(assignment);
478	155	Debug("bitvector-model") << " " << var << " => " << constant << "\n";
479		}
480	28222	}