src/theory/bv/eager_bitblaster.cpp

   1 /*********************                                                        */
   2 /*! \file eager_bitblaster.cpp
   3  ** \verbatim
   4  ** Original author: Liana Hadarean
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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
  13  **
  14  ** Bitblaster for the eager bv solver.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #include "theory/bv/bitblaster_template.h"
  20 #include "theory/bv/options.h"
  21 #include "theory/theory_model.h"
  22 #include "theory/bv/theory_bv.h"
  23 #include "prop/cnf_stream.h"
  24 #include "prop/sat_solver_factory.h"
  25
  26
  27 using namespace CVC4;
  28 using namespace CVC4::theory;
  29 using namespace CVC4::theory::bv;
  30
  31 void BitblastingRegistrar::preRegister(Node n) {
  32   d_bitblaster->bbAtom(n);
  33 };
  34
  35 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
  36   : TBitblaster<Node>()
  37   , d_bv(theory_bv)
  38   , d_bbAtoms()
  39   , d_variables()
  40 {
  41   d_bitblastingRegistrar = new BitblastingRegistrar(this);
  42   d_nullContext = new context::Context();
  43
  44   d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
  45   d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext);
  46
  47   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
  48   d_satSolver->setNotify(notify);
  49 }
  50
  51 EagerBitblaster::~EagerBitblaster() {
  52   delete d_cnfStream;
  53   delete d_satSolver;
  54   delete d_nullContext;
  55   delete d_bitblastingRegistrar;
  56 }
  57
  58 void EagerBitblaster::bbFormula(TNode node) {
  59   d_cnfStream->convertAndAssert(node, false, false);
  60 }
  61
  62 /**
  63  * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
  64  * NOTE: duplicate clauses are not detected because of marker literal
  65  * @param node the atom to be bitblasted
  66  *
  67  */
  68 void EagerBitblaster::bbAtom(TNode node) {
  69   node = node.getKind() == kind::NOT?  node[0] : node;
  70   if (node.getKind() == kind::BITVECTOR_BITOF)
  71     return;
  72   if (hasBBAtom(node)) {
  73     return;
  74   }
  75
  76   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
  77
  78   // the bitblasted definition of the atom
  79   Node normalized = Rewriter::rewrite(node);
  80   Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
  81       Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
  82       normalized;
  83   // asserting that the atom is true iff the definition holds
  84   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
  85
  86   AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
  87   storeBBAtom(node, atom_definition);
  88   d_cnfStream->convertAndAssert(atom_definition, false, false);
  89 }
  90
  91 void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
  92   // no need to store the definition for the lazy bit-blaster
  93   d_bbAtoms.insert(atom);
  94 }
  95
  96 bool EagerBitblaster::hasBBAtom(TNode atom) const {
  97   return d_bbAtoms.find(atom) != d_bbAtoms.end();
  98 }
  99
 100 void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
 101   if (hasBBTerm(node)) {
 102     getBBTerm(node, bits);
 103     return;
 104   }
 105
 106   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
 107
 108   d_termBBStrategies[node.getKind()] (node, bits, this);
 109
 110   Assert (bits.size() == utils::getSize(node));
 111
 112   storeBBTerm(node, bits);
 113 }
 114
 115 void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
 116   Assert(bits.size() == 0);
 117   for (unsigned i = 0; i < utils::getSize(var); ++i) {
 118     bits.push_back(utils::mkBitOf(var, i));
 119   }
 120   d_variables.insert(var);
 121 }
 122
 123 Node EagerBitblaster::getBBAtom(TNode node) const {
 124   return node;
 125 }
 126
 127
 128 /**
 129  * Calls the solve method for the Sat Solver.
 130  *
 131  * @return true for sat, and false for unsat
 132  */
 133
 134 bool EagerBitblaster::solve() {
 135   if (Trace.isOn("bitvector")) {
 136     Trace("bitvector") << "EagerBitblaster::solve(). \n";
 137   }
 138   Debug("bitvector") << "EagerBitblaster::solve(). \n";
 139   // TODO: clear some memory
 140   // if (something) {
 141   //   NodeManager* nm= NodeManager::currentNM();
 142   //   Rewriter::garbageCollect();
 143   //   nm->reclaimZombiesUntil(options::zombieHuntThreshold());
 144   // }
 145   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 146 }
 147
 148
 149 /**
 150  * Returns the value a is currently assigned to in the SAT solver
 151  * or null if the value is completely unassigned.
 152  *
 153  * @param a
 154  * @param fullModel whether to create a "full model," i.e., add
 155  * constants to equivalence classes that don't already have them
 156  *
 157  * @return
 158  */
 159 Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
 160   if (!hasBBTerm(a)) {
 161     Assert(isSharedTerm(a));
 162     return Node();
 163   }
 164   Bits bits;
 165   getBBTerm(a, bits);
 166   Integer value(0);
 167   for (int i = bits.size() -1; i >= 0; --i) {
 168     prop::SatValue bit_value;
 169     if (d_cnfStream->hasLiteral(bits[i])) {
 170       prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
 171       bit_value = d_satSolver->value(bit);
 172       Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
 173     } else {
 174       // the bit is unconstrainted so we can give it an arbitrary value
 175       bit_value = prop::SAT_VALUE_FALSE;
 176     }
 177     Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
 178     value = value * 2 + bit_int;
 179   }
 180   return utils::mkConst(BitVector(bits.size(), value));
 181 }
 182
 183
 184 void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
 185   TNodeSet::const_iterator it = d_variables.begin();
 186   for (; it!= d_variables.end(); ++it) {
 187     TNode var = *it;
 188     if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
 189       Node const_value = getVarValue(var, fullModel);
 190       if(const_value == Node()) {
 191         if( fullModel ){
 192           // if the value is unassigned just set it to zero
 193           const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
 194         }
 195       }
 196       if(const_value != Node()) {
 197         Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
 198                                  << var << " "
 199                                  << const_value << "))\n";
 200         m->assertEquality(var, const_value, true);
 201       }
 202     }
 203   }
 204 }
 205
 206 bool EagerBitblaster::isSharedTerm(TNode node) {
 207   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 208 }