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_core.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)
  32   : SubtheorySolver(c, bv),
  33     d_notify(*this),
  34     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
  35     d_slicer(new Slicer(c, this)),
  36     d_isCoreTheory(c, true),
  37     d_reasons(c)
  38 {
  39   if (d_useEqualityEngine) {
  40
  41     // The kinds we are treating as function application in congruence
  42     d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
  43     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
  44     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
  45     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
  46     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
  47     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
  48     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
  49     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
  50     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
  51     d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
  52     d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
  53     d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
  54     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
  55     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
  56     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
  57     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
  58     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
  59     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
  60     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
  61     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
  62     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
  63     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
  64     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
  65     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
  66     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
  67     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
  68     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
  69     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
  70     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
  71     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
  72   }
  73 }
  74
  75 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  76   d_equalityEngine.setMasterEqualityEngine(eq);
  77 }
  78
  79 void CoreSolver::preRegister(TNode node) {
  80   if (!d_useEqualityEngine)
  81     return;
  82
  83   if (node.getKind() == kind::EQUAL) {
  84       d_equalityEngine.addTriggerEquality(node);
  85       // d_slicer->processEquality(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, std::vector<TNode>& explanation) {
 103   std::vector<Node> a_decomp;
 104   d_slicer->getBaseDecomposition(a, a_decomp, explanation);
 105   Node new_a = utils::mkConcat(a_decomp);
 106   return new_a;
 107 }
 108
 109 bool CoreSolver::decomposeFact(TNode fact) {
 110   Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
 111   // assert decompositions since the equality engine does not know the semantics of
 112   // concat:
 113   //   a == a_1 concat ... concat a_k
 114   //   b == b_1 concat ... concat b_k
 115
 116   if (fact.getKind() == kind::EQUAL) {
 117     TNode a = fact[0];
 118     TNode b = fact[1];
 119
 120     d_slicer->processEquality(fact);
 121     std::vector<TNode> explanation;
 122     Node new_a = getBaseDecomposition(a, explanation);
 123     Node new_b = getBaseDecomposition(b, explanation);
 124
 125     explanation.push_back(fact);
 126     Node reason = utils::mkAnd(explanation);
 127     d_reasons.insert(reason);
 128
 129     Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
 130             utils::getSize(new_a) == utils::getSize(a));
 131     // FIXME: do we still need to assert these?
 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     d_reasons.insert(a_eq_new_a);
 137     d_reasons.insert(b_eq_new_b);
 138
 139     bool ok = true;
 140     ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
 141     if (!ok) return false;
 142     ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
 143     if (!ok) return false;
 144     // assert the individual equalities as well
 145     //    a_i == b_i
 146     if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
 147         new_b.getKind() == kind::BITVECTOR_CONCAT) {
 148       Assert (new_a.getNumChildren() == new_b.getNumChildren());
 149       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
 150         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
 151         ok = assertFactToEqualityEngine(eq_i, reason);
 152         d_reasons.insert(eq_i);
 153         if (!ok) return false;
 154       }
 155     }
 156     // merge the two terms in the slicer as well
 157     d_slicer->assertEquality(fact);
 158   } else {
 159     // still need to register the terms
 160     TNode a = fact[0][0];
 161     TNode b = fact[0][1];
 162     d_slicer->registerTerm(a);
 163     d_slicer->registerTerm(b);
 164   }
 165   // finally assert the actual fact to the equality engine
 166   return assertFactToEqualityEngine(fact, fact);
 167 }
 168
 169 bool CoreSolver::check(Theory::Effort e) {
 170   Trace("bitvector::core") << "CoreSolver::check \n";
 171   Assert (!d_bv->inConflict());
 172
 173   bool ok = true;
 174   std::vector<Node> core_eqs;
 175   while (! done()) {
 176     TNode fact = get();
 177
 178     // update whether we are in the core fragment
 179     if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
 180       d_isCoreTheory = false;
 181     }
 182
 183     // only reason about equalities
 184     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
 185       ok = decomposeFact(fact);
 186     } else {
 187       ok = assertFactToEqualityEngine(fact, fact);
 188     }
 189     if (!ok)
 190       return false;
 191   }
 192
 193   // make sure to assert the new splits
 194   std::vector<Node> new_splits;
 195   d_slicer->getNewSplits(new_splits);
 196   for (unsigned i = 0; i < new_splits.size(); ++i) {
 197     ok = assertFactToEqualityEngine(new_splits[i], utils::mkTrue());
 198     if (!ok)
 199       return false;
 200   }
 201   return true;
 202 }
 203
 204 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
 205   // Notify the equality engine
 206   if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) {
 207     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
 208     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
 209     bool negated = fact.getKind() == kind::NOT;
 210     TNode predicate = negated ? fact[0] : fact;
 211     if (predicate.getKind() == kind::EQUAL) {
 212       if (negated) {
 213         // dis-equality
 214         d_equalityEngine.assertEquality(predicate, false, reason);
 215       } else {
 216         // equality
 217         d_equalityEngine.assertEquality(predicate, true, reason);
 218       }
 219     } else {
 220       // Adding predicate if the congruence over it is turned on
 221       if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
 222         d_equalityEngine.assertPredicate(predicate, !negated, reason);
 223       }
 224     }
 225   }
 226
 227   // checking for a conflict
 228   if (d_bv->inConflict()) {
 229     return false;
 230   }
 231   return true;
 232 }
 233
 234 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
 235   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
 236   if (value) {
 237     return d_solver.storePropagation(equality);
 238   } else {
 239     return d_solver.storePropagation(equality.notNode());
 240   }
 241 }
 242
 243 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
 244   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
 245   if (value) {
 246     return d_solver.storePropagation(predicate);
 247   } else {
 248     return d_solver.storePropagation(predicate.notNode());
 249   }
 250 }
 251
 252 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 253   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 254   if (value) {
 255     return d_solver.storePropagation(t1.eqNode(t2));
 256   } else {
 257     return d_solver.storePropagation(t1.eqNode(t2).notNode());
 258   }
 259 }
 260
 261 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 262   d_solver.conflict(t1, t2);
 263 }
 264
 265 bool CoreSolver::storePropagation(TNode literal) {
 266   return d_bv->storePropagation(literal, SUB_CORE);
 267 }
 268
 269 void CoreSolver::conflict(TNode a, TNode b) {
 270   std::vector<TNode> assumptions;
 271   d_equalityEngine.explainEquality(a, b, true, assumptions);
 272   d_bv->setConflict(mkAnd(assumptions));
 273 }
 274
 275 void CoreSolver::collectModelInfo(TheoryModel* m) {
 276   if (Debug.isOn("bitvector-model")) {
 277     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
 278     for (; it!= d_assertionQueue.end(); ++it) {
 279       Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
 280                                << *it << ")\n";
 281     }
 282   }
 283   set<Node> termSet;
 284   d_bv->computeRelevantTerms(termSet);
 285   m->assertEqualityEngine(&d_equalityEngine, &termSet);
 286 }