src/theory/bv/bv_subtheory_core.cpp

   1 /*********************                                                        */
   2 /*! \file bv_subtheory_core.cpp
   3  ** \verbatim
   4  ** Original author: Liana Hadarean
   5  ** Major contributors: lianah
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  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 #include "theory/bv/options.h"
  24
  25 using namespace std;
  26 using namespace CVC4;
  27 using namespace CVC4::context;
  28 using namespace CVC4::theory;
  29 using namespace CVC4::theory::bv;
  30 using namespace CVC4::theory::bv::utils;
  31
  32 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
  33   : SubtheorySolver(c, bv),
  34     d_notify(*this),
  35     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
  36     d_slicer(new Slicer()),
  37     d_isCoreTheory(c, true),
  38     d_reasons(c)
  39 {
  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 CoreSolver::~CoreSolver() {
  75   delete d_slicer;
  76 }
  77 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  78   d_equalityEngine.setMasterEqualityEngine(eq);
  79 }
  80
  81 void CoreSolver::preRegister(TNode node) {
  82   if (node.getKind() == kind::EQUAL) {
  83       d_equalityEngine.addTriggerEquality(node);
  84       if (options::bitvectorCoreSolver()) {
  85         d_slicer->processEquality(node);
  86       }
  87   } else {
  88     d_equalityEngine.addTerm(node);
  89   }
  90 }
  91
  92
  93 void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
  94   bool polarity = literal.getKind() != kind::NOT;
  95   TNode atom = polarity ? literal : literal[0];
  96   if (atom.getKind() == kind::EQUAL) {
  97     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
  98   } else {
  99     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
 100   }
 101 }
 102
 103 Node CoreSolver::getBaseDecomposition(TNode a) {
 104   std::vector<Node> a_decomp;
 105   d_slicer->getBaseDecomposition(a, a_decomp);
 106   Node new_a = utils::mkConcat(a_decomp);
 107   Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n";
 108   return new_a;
 109 }
 110
 111 bool CoreSolver::decomposeFact(TNode fact) {
 112   Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
 113   // assert decompositions since the equality engine does not know the semantics of
 114   // concat:
 115   //   a == a_1 concat ... concat a_k
 116   //   b == b_1 concat ... concat b_k
 117   Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
 118   // FIXME: are this the right things to assert?
 119   // assert decompositions since the equality engine does not know the semantics of
 120   // concat:
 121   //   a == a_1 concat ... concat a_k
 122   //   b == b_1 concat ... concat b_k
 123   TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;
 124
 125   TNode a = eq[0];
 126   TNode b = eq[1];
 127   Node new_a = getBaseDecomposition(a);
 128   Node new_b = getBaseDecomposition(b);
 129
 130   Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
 131           utils::getSize(new_a) == utils::getSize(a));
 132
 133   NodeManager* nm = NodeManager::currentNM();
 134   Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
 135   Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
 136
 137   bool ok = true;
 138   ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
 139   if (!ok) return false;
 140   ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
 141   if (!ok) return false;
 142   ok = assertFactToEqualityEngine(fact, fact);
 143   if (!ok) return false;
 144
 145   if (fact.getKind() == kind::EQUAL) {
 146     // assert the individual equalities as well
 147     //    a_i == b_i
 148     if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
 149         new_b.getKind() == kind::BITVECTOR_CONCAT) {
 150
 151       Assert (new_a.getNumChildren() == new_b.getNumChildren());
 152       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
 153         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
 154         ok = assertFactToEqualityEngine(eq_i, fact);
 155         if (!ok) return false;
 156       }
 157     }
 158   }
 159   return true;
 160 }
 161
 162 bool CoreSolver::check(Theory::Effort e) {
 163   Trace("bitvector::core") << "CoreSolver::check \n";
 164   Assert (!d_bv->inConflict());
 165   ++(d_statistics.d_numCallstoCheck);
 166   bool ok = true;
 167   std::vector<Node> core_eqs;
 168   while (! done()) {
 169     TNode fact = get();
 170
 171     // update whether we are in the core fragment
 172     if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
 173       d_isCoreTheory = false;
 174     }
 175
 176     // only reason about equalities
 177     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
 178       if (options::bitvectorCoreSolver()) {
 179         ok = decomposeFact(fact);
 180       } else {
 181         ok = assertFactToEqualityEngine(fact, fact);
 182       }
 183     } else {
 184       ok = assertFactToEqualityEngine(fact, fact);
 185     }
 186     if (!ok)
 187       return false;
 188   }
 189
 190   if (Theory::fullEffort(e) && isComplete()) {
 191     buildModel();
 192   }
 193
 194   return true;
 195 }
 196
 197 void CoreSolver::buildModel() {
 198   if (options::bitvectorCoreSolver()) {
 199     // FIXME
 200     Unreachable();
 201     return;
 202   }
 203   Debug("bv-core") << "CoreSolver::buildModel() \n";
 204   d_modelValues.clear();
 205   TNodeSet constants;
 206   TNodeSet constants_in_eq_engine;
 207   // collect constants in equality engine
 208   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
 209   while (!eqcs_i.isFinished()) {
 210     TNode repr = *eqcs_i;
 211     if  (repr.getKind() == kind::CONST_BITVECTOR) {
 212       // must check if it's just the constant
 213       eq::EqClassIterator it(repr, &d_equalityEngine);
 214       if (!(++it).isFinished() || true) {
 215         constants.insert(repr);
 216         constants_in_eq_engine.insert(repr);
 217       }
 218     }
 219     ++eqcs_i;
 220   }
 221   // build repr to value map
 222
 223   eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
 224   while (!eqcs_i.isFinished()) {
 225     TNode repr = *eqcs_i;
 226     ++eqcs_i;
 227
 228     if (repr.getKind() != kind::VARIABLE &&
 229         repr.getKind() != kind::SKOLEM &&
 230         repr.getKind() != kind::CONST_BITVECTOR &&
 231         !d_bv->isSharedTerm(repr)) {
 232       continue;
 233     }
 234
 235     TypeNode type = repr.getType();
 236     if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
 237       Debug("bv-core-model") << "   processing " << repr <<"\n";
 238       // we need to assign a value for it
 239       TypeEnumerator te(type);
 240       Node val;
 241       do {
 242         val = *te;
 243         ++te;
 244         // Debug("bv-core-model") << "  trying value " << val << "\n";
 245         // Debug("bv-core-model") << "  is in set? " << constants.count(val) << "\n";
 246         // Debug("bv-core-model") << "  enumerator done? " << te.isFinished() << "\n";
 247       } while (constants.count(val) != 0 && !(te.isFinished()));
 248
 249       if (te.isFinished() && constants.count(val) != 0) {
 250         // if we cannot enumerate anymore values we just return the lemma stating that
 251         // at least two of the representatives are equal.
 252         std::vector<TNode> representatives;
 253         representatives.push_back(repr);
 254
 255         for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
 256              it != constants_in_eq_engine.end(); ++it) {
 257           TNode constant = *it;
 258           if (utils::getSize(constant) == utils::getSize(repr)) {
 259             representatives.push_back(constant);
 260           }
 261         }
 262         for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
 263           representatives.push_back(it->first);
 264         }
 265         std::vector<Node> equalities;
 266         for (unsigned i = 0; i < representatives.size(); ++i) {
 267           for (unsigned j = i + 1; j < representatives.size(); ++j) {
 268             TNode a = representatives[i];
 269             TNode b = representatives[j];
 270             if (utils::getSize(a) == utils::getSize(b)) {
 271               equalities.push_back(utils::mkNode(kind::EQUAL, a, b));
 272             }
 273           }
 274         }
 275         Node lemma = utils::mkOr(equalities);
 276         d_bv->lemma(lemma);
 277         Debug("bv-core") << "  lemma: " << lemma << "\n";
 278         return;
 279       }
 280       Debug("bv-core-model") << "   " << repr << " => " << val <<"\n" ;
 281       constants.insert(val);
 282       d_modelValues[repr] = val;
 283     }
 284   }
 285 }
 286
 287 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
 288   // Notify the equality engine
 289   if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
 290     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
 291     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
 292     bool negated = fact.getKind() == kind::NOT;
 293     TNode predicate = negated ? fact[0] : fact;
 294     if (predicate.getKind() == kind::EQUAL) {
 295       if (negated) {
 296         // dis-equality
 297         d_equalityEngine.assertEquality(predicate, false, reason);
 298       } else {
 299         // equality
 300         d_equalityEngine.assertEquality(predicate, true, reason);
 301       }
 302     } else {
 303       // Adding predicate if the congruence over it is turned on
 304       if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
 305         d_equalityEngine.assertPredicate(predicate, !negated, reason);
 306       }
 307     }
 308   }
 309
 310   // checking for a conflict
 311   if (d_bv->inConflict()) {
 312     return false;
 313   }
 314   return true;
 315 }
 316
 317 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
 318   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
 319   if (value) {
 320     return d_solver.storePropagation(equality);
 321   } else {
 322     return d_solver.storePropagation(equality.notNode());
 323   }
 324 }
 325
 326 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
 327   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
 328   if (value) {
 329     return d_solver.storePropagation(predicate);
 330   } else {
 331     return d_solver.storePropagation(predicate.notNode());
 332   }
 333 }
 334
 335 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 336   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 337   if (value) {
 338     return d_solver.storePropagation(t1.eqNode(t2));
 339   } else {
 340     return d_solver.storePropagation(t1.eqNode(t2).notNode());
 341   }
 342 }
 343
 344 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 345   d_solver.conflict(t1, t2);
 346 }
 347
 348 bool CoreSolver::storePropagation(TNode literal) {
 349   return d_bv->storePropagation(literal, SUB_CORE);
 350 }
 351
 352 void CoreSolver::conflict(TNode a, TNode b) {
 353   std::vector<TNode> assumptions;
 354   d_equalityEngine.explainEquality(a, b, true, assumptions);
 355   Node conflict = flattenAnd(assumptions);
 356   d_bv->setConflict(conflict);
 357 }
 358
 359 void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
 360   if (options::bitvectorCoreSolver()) {
 361     Unreachable();
 362     return;
 363   }
 364   if (Debug.isOn("bitvector-model")) {
 365     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
 366     for (; it!= d_assertionQueue.end(); ++it) {
 367       Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
 368                                << *it << ")\n";
 369     }
 370   }
 371   set<Node> termSet;
 372   d_bv->computeRelevantTerms(termSet);
 373   m->assertEqualityEngine(&d_equalityEngine, &termSet);
 374   if (isComplete()) {
 375     Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
 376     for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
 377       Node a = it->first;
 378       Node b = it->second;
 379       m->assertEquality(a, b, true);
 380     }
 381   }
 382 }
 383
 384 Node CoreSolver::getModelValue(TNode var) {
 385   // we don't need to evaluate bv expressions and only look at variable values
 386   // because this only gets called when the core theory is complete (i.e. no other bv
 387   // function symbols are currently asserted)
 388   Assert (d_slicer->isCoreTerm(var));
 389
 390   Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
 391   Assert (isComplete());
 392   TNode repr = d_equalityEngine.getRepresentative(var);
 393   Node result = Node();
 394   if (repr.getKind() == kind::CONST_BITVECTOR) {
 395     result = repr;
 396   } else if (d_modelValues.find(repr) == d_modelValues.end()) {
 397     // it may be a shared term that never gets asserted
 398     // result is just Null
 399     Assert(d_bv->isSharedTerm(var));
 400   } else {
 401     result = d_modelValues[repr];
 402   }
 403   Debug("bitvector-model") << " => " << result <<"\n";
 404   return result;
 405 }
 406
 407 CoreSolver::Statistics::Statistics()
 408   : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
 409 {
 410   StatisticsRegistry::registerStat(&d_numCallstoCheck);
 411 }
 412 CoreSolver::Statistics::~Statistics() {
 413   StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
 414 }