path: root/src/theory/bv/bv_inequality_graph.cpp

/*********************                                                        */
/*! \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;

bool InequalityGraph::addInequality(TNode a, TNode b, TNode reason) {
  TermId id_a = registerTerm(a);
  TermId id_b = registerTerm(b);
  ReasonId id_reason = registerReason(reason);
  return addInequalityInternal(id_a, id_b, id_reason);
}


bool InequalityGraph::addInequalityInternal(TermId a, TermId b, TermId reason) {
  if (getValue(a) < getValue(b)) {
    // the inequality is true in the current partial model
    return true;
  }
  if (getValue(b) < getValue(a)) {
    // the inequality is false in the current partial model
    std::vector<ReasonId> conflict; 
    computeExplanation(b, a, conflict); 
    return false; 
  }
  // the inequality edge does not exist
  addEdge(a, b, reason);
  BFSQueue queue;
  queue.push(a); 
  return computeValuesBFS(queue); 
}

void InequalityGraph::computeConflict(TermId from, TermId to, std::vector<ReasonId>& explanation) {
  if (to == from)
    return;
  const Edges& edges = getInEdges(to);
  BitVector max(getBitwidth(a), 0);
  TermId to_visit = UndefinedTermId;
  ReasonId reason = UndefinedReasonId;
  
  for (Edges::const_iterator it = edges.begin(); it != edges.end(); ++it) {
    TermId next = it->next; 
    if (next == from) {
      explanation.push_back(it->reason); 
      return; 
    }
    if (getValue(next) >= max) {
      max = it->value;
      to_visit = it->next;
      reason = it->reason; 
    } 
  }
  Assert(reason != UndefinedReasonId && to_visit != UndefinedTermId);
  explanation.push_back(reason);
  computeConflict(from, to_visit, explanation); 
}

void InequalityGraph::addEdge(TermId a, TermId b, TermId reason) {
  Edges& out_edges = getEdges(a);
  edges.push_back(InequalityEdge(b, reason));
  Edges& in_edges = getParentEdges(b);
  edges.push_back(InequalityEdge(a, reason)); 
}

bool InequalityGraph::computeValuesBFS(BitVector& min_val, BFSQueue& queue, TermIdSet& seen) {
  if (queue.empty())
    return true;
  
  TermId current = queue.top().id;
  seen.insert(current); 
  queue.pop();
  
  InequalityNode& ineqNode = getInequalityNode(current);
  if (ineqNode.isConstant()) {
    if (ineqNode.getValue() < min_val) {
      // we have a conflict 
      return false; 
    }
  } else {
    // if not constant we can update the value
    if (ineqNode.getValue() < min_val) {
      ineqNode.setValue(min_val); 
    }
  }
  BitVector next_min = ineqNode.getValue() + 1; 
  bool overflow = next_min < min_val; 
  const Edges& edges = getEdges(current);

  if (edges.size() > 0 && overflow) {
    // we have reached the maximum value
    computeConflict(); 
    return false;
  }
  // TODO: update key, maybe
  for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
    TermId next = it->next;
    if (!seen.contains(next)) {
      BitVector& value = getInequalityNode(next).getValue(); 
      queue.push(PQueueElement(next, value));
    }
  }
  return computeValuesBFS(next_min, queue, seen); 
}


bool InequalityGraph::areLessThanInternal(TermId a, TermId b) {
  return getValue(a) < getValue(b); 
}

TermId InequalitySolver::registerTerm(TNode term) {
  if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) {
    return d_termNodeToIdMap[term]; 
  }

  // store in node mapping
  TermId id = d_termNodes.size();
  d_termNodes.push_back(term);
  d_termNodeToIdMap[term] = id;
  
  // create InequalityNode
  bool isConst = term.getKind() == kind::CONST_BITVECTOR;
  BitVector value = isConst? term.getConst<BitVector>() : BitVector(utils::getSize(term),0); 
  InequalityNode ineq = InequalityNode(id, utils::getSize(term), isConst, value);
  Assert (d_ineqNodes.size() == id); 
  d_ineqNodes.push_back(ineq);
  Assert (d_ineqEdges.size() == id); 
  d_ineqEdges.push_back(Edges());
  Assert(d_parentEdges.size() == id);
  d_parentEdges.push_back(Edges()); 
  return id; 
}

ReasonId InequalitySolver::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 InequalitySolver::getReason(ReasonId id) const {
  Assert (d_reasonNodes.size() > id);
  return d_reasonNodes[id]; 
}

TNode InequalitySolver::getTerm(TermId id) const {
  Assert (d_termNodes.size() > id);
  return d_termNodes[id]; 
}

void InequalitySolver::setConflict(const std::vector<ReasonId>& conflict) {
  Assert (!d_inConflict); 
  d_inConflict = true;
  d_conflict.clear(); 
  for (unsigned i = 0; i < conflict.size(); ++i) {
    d_conflict.push_back(getReason(conflict[i])); 
  }
}

void InequalitySolver::getConflict(std::vector<TNode>& conflict) {
  for (unsigned i = 0; i < d_conflict.size(); ++it) {
    conflict.push_back(d_conflict[i]); 
  }
}

// bool InequalityGraph::canReach(TermId from, TermId to) {
//   TermIdSet visited;
//   bfs(start, seen);
//   if (seen.constains(to)) {
//     return true; 
//   }
// }

// bool InequalityGraph::bfs(TermId to, TermIdSet& seen, TermIdQueue& queue) {
//   if (queue.empty())
//     return;
  
//   TermId current = queue.front();
//   queue.pop();
//   if (current = to) {
//     return true; 
//   }
//   const Edges& edges = getEdges(current);
//   for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
//     TermId next = it->next;
//     if(!seen.contains(next)) {
//       seen.insert(next);
//       queue.push(next); 
//     }
//   }
//   return bfs(seen, queue);
// }

// void InequalityGraph::getPath(TermId to, TermId from, const TermIdSet& seen, std::vector<ReasonId> explanation) {
//   // traverse parent edges
//   const Edges& out = getOutEdges(to);
//   for (Edges::const_iterator it = out.begin(); it != out.end(); ++it) {
//     if (seen.find(it->next)) {
//       path.push_back(it->reason); 
//       getPath(it->next, from, seen, path);
//       return; 
//     }
//   }
// }

// bool InequalityGraph::initializeValues(TNode a, TNode b) {
//   TermId id_a = registerTerm(a);
//   TermId id_b = registerTerm(b);
//   if (!hasValue(id_a) && !hasValue(id_b)) {
//     InequalityNode& ineq_a = getInequalityNode(id_a);
//     ineq_a.setValue(BiVector(utils::getSize(a), 0));
//     InequalityNode& ineq_b = getInequalityNode(id_b);
//     ineq_a.setValue(BiVector(utils::getSize(a), 1));
//   }
//   if (!hasValue(id_a) && hasValue(id_b)) {
//     BitVector& b_value = getValue(id_b);
//     if (b_value == 0) {
//       return false; 
//     }
//     InequalityNode& ineq_a = getInequalityNode(id_a);
//     ineq_a.setValue(b_value - 1); 
//   }
//   if (hasValue(id_a) && !hasValue(id_b)) {
//     BitVector& a_value = getValue(id_a);
//     if (a_value + 1 < a_value) {
//       return false; 
//     }
//     InequalityNode& ineq_b = getInequalityNode(id_b);
//     ineq_b.setValue(a_value + 1); 
//   }
//   return true; 
// }