src/theory/bv/bv_subtheory_core.cpp

   1 /*********************                                                        */
   2 /*! \file bv_subtheory_eq.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): lianah
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Algebraic solver.
  13  **
  14  ** Algebraic solver.
  15  **/
  16
  17 #include "theory/bv/bv_subtheory_eq.h"
  18
  19 #include "theory/bv/theory_bv.h"
  20 #include "theory/bv/theory_bv_utils.h"
  21 #include "theory/bv/slicer.h"
  22 #include "theory/model.h"
  23
  24 using namespace std;
  25 using namespace CVC4;
  26 using namespace CVC4::context;
  27 using namespace CVC4::theory;
  28 using namespace CVC4::theory::bv;
  29 using namespace CVC4::theory::bv::utils;
  30
  31 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer)
  32   : SubtheorySolver(c, bv),
  33     d_notify(*this),
  34     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
  35     d_assertions(c),
  36     d_normalFormCache(),
  37     d_slicer(slicer),
  38     d_isCoreTheory(c, true)
  39 {
  40   if (d_useEqualityEngine) {
  41
  42     // The kinds we are treating as function application in congruence
  43     d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
  44     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
  45     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
  46     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
  47     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
  48     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
  49     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
  50     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
  51     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
  52     d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
  53     d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
  54     d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT);
  55     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
  56     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
  57     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
  58     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
  59     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
  60     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
  61     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
  62     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
  63     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
  64     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
  65     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
  66     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
  67     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
  68     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
  69     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
  70     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
  71     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
  72     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
  73   }
  74 }
  75
  76 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  77   d_equalityEngine.setMasterEqualityEngine(eq);
  78 }
  79
  80 void CoreSolver::preRegister(TNode node) {
  81   if (!d_useEqualityEngine)
  82     return;
  83
  84   if (node.getKind() == kind::EQUAL) {
  85       d_equalityEngine.addTriggerEquality(node);
  86   } else {
  87     d_equalityEngine.addTerm(node);
  88   }
  89 }
  90
  91
  92 void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
  93   bool polarity = literal.getKind() != kind::NOT;
  94   TNode atom = polarity ? literal : literal[0];
  95   if (atom.getKind() == kind::EQUAL) {
  96     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
  97   } else {
  98     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
  99   }
 100 }
 101
 102 Node CoreSolver::getBaseDecomposition(TNode a) {
 103   // if (d_normalFormCache.find(a) != d_normalFormCache.end()) {
 104   //   return d_normalFormCache[a];
 105   // }
 106
 107   // otherwise we must compute the normal form
 108   std::vector<Node> a_decomp;
 109   d_slicer->getBaseDecomposition(a, a_decomp);
 110   Node new_a = utils::mkConcat(a_decomp);
 111   //  d_normalFormCache[a] = new_a;
 112   return new_a;
 113 }
 114
 115 bool CoreSolver::decomposeFact(TNode fact) {
 116   Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
 117   // FIXME: are this the right things to assert?
 118   // assert decompositions since the equality engine does not know the semantics of
 119   // concat:
 120   //   a == a_1 concat ... concat a_k
 121   //   b == b_1 concat ... concat b_k
 122   TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;
 123
 124   TNode a = eq[0];
 125   TNode b = eq[1];
 126   Node new_a = getBaseDecomposition(a);
 127   Node new_b = getBaseDecomposition(b);
 128
 129   Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
 130           utils::getSize(new_a) == utils::getSize(a));
 131
 132   NodeManager* nm = NodeManager::currentNM();
 133   Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
 134   Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
 135
 136   bool ok = true;
 137   ok = assertFact(a_eq_new_a, utils::mkTrue());
 138   if (!ok) return false;
 139   ok = assertFact(b_eq_new_b, utils::mkTrue());
 140   if (!ok) return false;
 141   ok = assertFact(fact, fact);
 142   if (!ok) return false;
 143
 144   if (fact.getKind() == kind::EQUAL) {
 145     // assert the individual equalities as well
 146     //    a_i == b_i
 147     if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
 148         new_b.getKind() == kind::BITVECTOR_CONCAT) {
 149
 150       Assert (new_a.getNumChildren() == new_b.getNumChildren());
 151       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
 152         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
 153         ok = assertFact(eq_i, fact);
 154         if (!ok) return false;
 155       }
 156     }
 157   }
 158   return true;
 159 }
 160
 161 bool CoreSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
 162   Trace("bitvector::core") << "CoreSolver::addAssertions \n";
 163   Assert (!d_bv->inConflict());
 164
 165   bool ok = true;
 166   std::vector<Node> core_eqs;
 167   for (unsigned i = 0; i < assertions.size(); ++i) {
 168     TNode fact = assertions[i];
 169
 170     // update whether we are in the core fragment
 171     // FIXME: move isCoreTerm into CoreSolver
 172     if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
 173       d_isCoreTheory = false;
 174     }
 175
 176     // only reason about equalities
 177     // FIXME: should we slice when we have the terms in inequalities?
 178     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
 179       ok = decomposeFact(fact);
 180     } else {
 181       ok = assertFact(fact, fact);
 182     }
 183     if (!ok)
 184       return false;
 185   }
 186
 187   return true;
 188 }
 189
 190 bool CoreSolver::assertFact(TNode fact, TNode reason) {
 191   Debug("bv-slicer") << "CoreSolver::assertFact fact=" << fact << endl;
 192   Debug("bv-slicer") << "                     reason=" << reason << endl;
 193   // Notify the equality engine
 194   if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) {
 195     Trace("bitvector::core") << "     (assert " << fact << ")\n";
 196     //d_assertions.push_back(fact);
 197     bool negated = fact.getKind() == kind::NOT;
 198     TNode predicate = negated ? fact[0] : fact;
 199     if (predicate.getKind() == kind::EQUAL) {
 200       if (negated) {
 201         // dis-equality
 202         d_equalityEngine.assertEquality(predicate, false, reason);
 203       } else {
 204         // equality
 205         d_equalityEngine.assertEquality(predicate, true, reason);
 206       }
 207     } else {
 208       // Adding predicate if the congruence over it is turned on
 209       if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
 210         d_equalityEngine.assertPredicate(predicate, !negated, reason);
 211       }
 212     }
 213   }
 214
 215   // checking for a conflict
 216   if (d_bv->inConflict()) {
 217     return false;
 218   }
 219   return true;
 220 }
 221
 222 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
 223   BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
 224   if (value) {
 225     return d_solver.storePropagation(equality);
 226   } else {
 227     return d_solver.storePropagation(equality.notNode());
 228   }
 229 }
 230
 231 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
 232   BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
 233   if (value) {
 234     return d_solver.storePropagation(predicate);
 235   } else {
 236     return d_solver.storePropagation(predicate.notNode());
 237   }
 238 }
 239
 240 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 241   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 242   if (value) {
 243     return d_solver.storePropagation(t1.eqNode(t2));
 244   } else {
 245     return d_solver.storePropagation(t1.eqNode(t2).notNode());
 246   }
 247 }
 248
 249 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 250   d_solver.conflict(t1, t2);
 251 }
 252
 253 bool CoreSolver::storePropagation(TNode literal) {
 254   return d_bv->storePropagation(literal, SUB_CORE);
 255 }
 256
 257 void CoreSolver::conflict(TNode a, TNode b) {
 258   std::vector<TNode> assumptions;
 259   d_equalityEngine.explainEquality(a, b, true, assumptions);
 260   d_bv->setConflict(mkAnd(assumptions));
 261 }
 262
 263 void CoreSolver::collectModelInfo(TheoryModel* m) {
 264   if (Debug.isOn("bitvector-model")) {
 265     context::CDList<TNode>::const_iterator it = d_assertions.begin();
 266     for (; it!= d_assertions.end(); ++it) {
 267       Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
 268                                << *it << ")\n";
 269     }
 270   }
 271   set<Node> termSet;
 272   d_bv->computeRelevantTerms(termSet);
 273   m->assertEqualityEngine(&d_equalityEngine, &termSet);
 274 }