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_slicer(slicer),
  37     d_isCoreTheory(c, true)
  38 {
  39   if (d_useEqualityEngine) {
  40
  41     // The kinds we are treating as function application in congruence
  42     d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
  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);
  52     d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
  53     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
  54     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
  55     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
  56     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
  57     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
  58     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
  59     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
  60     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
  61     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
  62     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
  63     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
  64     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
  65     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
  66     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
  67     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
  68     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
  69     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
  70     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
  71   }
  72 }
  73
  74 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  75   d_equalityEngine.setMasterEqualityEngine(eq);
  76 }
  77
  78 void CoreSolver::preRegister(TNode node) {
  79   if (!d_useEqualityEngine)
  80     return;
  81
  82   if (node.getKind() == kind::EQUAL) {
  83       d_equalityEngine.addTriggerEquality(node);
  84   } else {
  85     d_equalityEngine.addTerm(node);
  86   }
  87 }
  88
  89
  90 void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
  91   bool polarity = literal.getKind() != kind::NOT;
  92   TNode atom = polarity ? literal : literal[0];
  93   if (atom.getKind() == kind::EQUAL) {
  94     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
  95   } else {
  96     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
  97   }
  98 }
  99
 100 bool CoreSolver::decomposeFact(TNode fact) {
 101   Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
 102   // FIXME: are this the right things to assert?
 103   // assert decompositions since the equality engine does not know the semantics of
 104   // concat:
 105   //   a == a_1 concat ... concat a_k
 106   //   b == b_1 concat ... concat b_k
 107   TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;
 108
 109   TNode a = eq[0];
 110   TNode b = eq[1];
 111   std::vector<Node> a_decomp;
 112   std::vector<Node> b_decomp;
 113
 114   d_slicer->getBaseDecomposition(a, a_decomp);
 115   d_slicer->getBaseDecomposition(b, b_decomp);
 116
 117   Assert (a_decomp.size() == b_decomp.size());
 118
 119   Node new_a = utils::mkConcat(a_decomp);
 120   Node new_b = utils::mkConcat(b_decomp);
 121
 122   NodeManager* nm = NodeManager::currentNM();
 123   Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
 124   Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
 125
 126   bool ok = true;
 127   ok = assertFact(a_eq_new_a, utils::mkTrue());
 128   if (!ok) return false;
 129   ok = assertFact(b_eq_new_b, utils::mkTrue());
 130   if (!ok) return false;
 131   ok = assertFact(fact, fact);
 132   if (!ok) return false;
 133
 134   if (fact.getKind() == kind::EQUAL) {
 135     // assert the individual equalities as well
 136     //    a_i == b_i
 137     for (unsigned i = 0; i < a_decomp.size(); ++i) {
 138       Node eq_i = nm->mkNode(kind::EQUAL, a_decomp[i], b_decomp[i]);
 139       ok = assertFact(eq_i, fact);
 140       if (!ok) return false;
 141     }
 142   }
 143   return true;
 144 }
 145
 146 bool CoreSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
 147   Trace("bitvector::core") << "CoreSolver::addAssertions \n";
 148   Assert (!d_bv->inConflict());
 149
 150   bool ok = true;
 151   std::vector<Node> core_eqs;
 152   for (unsigned i = 0; i < assertions.size(); ++i) {
 153     TNode fact = assertions[i];
 154
 155     // update whether we are in the core fragment
 156     // FIXME: move isCoreTerm into CoreSolver
 157     if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
 158       d_isCoreTheory = false;
 159     }
 160     ok = decomposeFact(fact);
 161     if (!ok)
 162       return false;
 163   }
 164
 165   return true;
 166 }
 167
 168 bool CoreSolver::assertFact(TNode fact, TNode reason) {
 169   Debug("bv-slicer") << "CoreSolver::assertFact fact=" << fact << endl;
 170   Debug("bv-slicer") << "                     reason=" << reason << endl;
 171   // Notify the equality engine
 172   if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) {
 173     Trace("bitvector::core") << "     (assert " << fact << ")\n";
 174     //d_assertions.push_back(fact);
 175     bool negated = fact.getKind() == kind::NOT;
 176     TNode predicate = negated ? fact[0] : fact;
 177     if (predicate.getKind() == kind::EQUAL) {
 178       if (negated) {
 179         // dis-equality
 180         d_equalityEngine.assertEquality(predicate, false, reason);
 181       } else {
 182         // equality
 183         d_equalityEngine.assertEquality(predicate, true, reason);
 184       }
 185     } else {
 186       // Adding predicate if the congruence over it is turned on
 187       if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
 188         d_equalityEngine.assertPredicate(predicate, !negated, reason);
 189       }
 190     }
 191   }
 192
 193   // checking for a conflict
 194   if (d_bv->inConflict()) {
 195     return false;
 196   }
 197   return true;
 198 }
 199
 200 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
 201   BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
 202   if (value) {
 203     return d_solver.storePropagation(equality);
 204   } else {
 205     return d_solver.storePropagation(equality.notNode());
 206   }
 207 }
 208
 209 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
 210   BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
 211   if (value) {
 212     return d_solver.storePropagation(predicate);
 213   } else {
 214     return d_solver.storePropagation(predicate.notNode());
 215   }
 216 }
 217
 218 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 219   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 220   if (value) {
 221     return d_solver.storePropagation(t1.eqNode(t2));
 222   } else {
 223     return d_solver.storePropagation(t1.eqNode(t2).notNode());
 224   }
 225 }
 226
 227 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 228   d_solver.conflict(t1, t2);
 229 }
 230
 231 bool CoreSolver::storePropagation(TNode literal) {
 232   return d_bv->storePropagation(literal, SUB_CORE);
 233 }
 234
 235 void CoreSolver::conflict(TNode a, TNode b) {
 236   std::vector<TNode> assumptions;
 237   d_equalityEngine.explainEquality(a, b, true, assumptions);
 238   d_bv->setConflict(mkAnd(assumptions));
 239 }
 240
 241 void CoreSolver::collectModelInfo(TheoryModel* m) {
 242   if (Debug.isOn("bitvector-model")) {
 243     context::CDList<TNode>::const_iterator it = d_assertions.begin();
 244     for (; it!= d_assertions.end(); ++it) {
 245       Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
 246                                << *it << ")\n";
 247     }
 248   }
 249   set<Node> termSet;
 250   d_bv->computeRelevantTerms(termSet);
 251   m->assertEqualityEngine(&d_equalityEngine, &termSet);
 252 }