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 "options/bv_options.h"
  20 #include "prop/cnf_stream.h"
  21 #include "prop/sat_solver_factory.h"
  22 #include "proof/bitvector_proof.h"
  23 #include "smt/smt_statistics_registry.h"
  24 #include "theory/bv/bitblaster_template.h"
  25 #include "theory/bv/theory_bv.h"
  26 #include "theory/theory_model.h"
  27
  28
  29 namespace CVC4 {
  30 namespace theory {
  31 namespace bv {
  32
  33 void BitblastingRegistrar::preRegister(Node n) {
  34   d_bitblaster->bbAtom(n);
  35 };
  36
  37 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
  38   : TBitblaster<Node>()
  39   , d_bv(theory_bv)
  40   , d_bbAtoms()
  41   , d_variables()
  42 {
  43   d_bitblastingRegistrar = new BitblastingRegistrar(this);
  44   d_nullContext = new context::Context();
  45
  46   d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext,
  47                                                       smtStatisticsRegistry(),
  48                                                       "EagerBitblaster");
  49   d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
  50                                            d_bitblastingRegistrar,
  51                                            d_nullContext,
  52                                            d_bv->globals(),
  53                                            options::proof(),
  54                                            "EagerBitblaster");
  55
  56   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
  57   d_satSolver->setNotify(notify);
  58   d_bvp = NULL;
  59 }
  60
  61 EagerBitblaster::~EagerBitblaster() {
  62   delete d_cnfStream;
  63   delete d_satSolver;
  64   delete d_nullContext;
  65   delete d_bitblastingRegistrar;
  66 }
  67
  68 void EagerBitblaster::bbFormula(TNode node) {
  69   d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, TNode::null());
  70 }
  71
  72 /**
  73  * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
  74  * NOTE: duplicate clauses are not detected because of marker literal
  75  * @param node the atom to be bitblasted
  76  *
  77  */
  78 void EagerBitblaster::bbAtom(TNode node) {
  79   node = node.getKind() == kind::NOT?  node[0] : node;
  80   if (node.getKind() == kind::BITVECTOR_BITOF)
  81     return;
  82   if (hasBBAtom(node)) {
  83     return;
  84   }
  85
  86   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
  87
  88   // the bitblasted definition of the atom
  89   Node normalized = Rewriter::rewrite(node);
  90   Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
  91     d_atomBBStrategies[normalized.getKind()](normalized, this) :
  92     normalized;
  93
  94   if (!options::proof()) {
  95     atom_bb = Rewriter::rewrite(atom_bb);
  96   }
  97
  98   // asserting that the atom is true iff the definition holds
  99   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
 100
 101   AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
 102   storeBBAtom(node, atom_bb);
 103   d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 104 }
 105
 106 void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
 107   if( d_bvp ){
 108     d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
 109   }
 110   d_bbAtoms.insert(atom);
 111 }
 112
 113 void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
 114   if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); }
 115   d_termCache.insert(std::make_pair(node, bits));
 116 }
 117
 118
 119 bool EagerBitblaster::hasBBAtom(TNode atom) const {
 120   return d_bbAtoms.find(atom) != d_bbAtoms.end();
 121 }
 122
 123 void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
 124   if (hasBBTerm(node)) {
 125     getBBTerm(node, bits);
 126     return;
 127   }
 128
 129   d_bv->spendResource(options::bitblastStep());
 130   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
 131
 132   d_termBBStrategies[node.getKind()] (node, bits, this);
 133
 134   Assert (bits.size() == utils::getSize(node));
 135
 136   storeBBTerm(node, bits);
 137 }
 138
 139 void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
 140   Assert(bits.size() == 0);
 141   for (unsigned i = 0; i < utils::getSize(var); ++i) {
 142     bits.push_back(utils::mkBitOf(var, i));
 143   }
 144   d_variables.insert(var);
 145 }
 146
 147 Node EagerBitblaster::getBBAtom(TNode node) const {
 148   return node;
 149 }
 150
 151
 152 /**
 153  * Calls the solve method for the Sat Solver.
 154  *
 155  * @return true for sat, and false for unsat
 156  */
 157
 158 bool EagerBitblaster::solve() {
 159   if (Trace.isOn("bitvector")) {
 160     Trace("bitvector") << "EagerBitblaster::solve(). \n";
 161   }
 162   Debug("bitvector") << "EagerBitblaster::solve(). \n";
 163   // TODO: clear some memory
 164   // if (something) {
 165   //   NodeManager* nm= NodeManager::currentNM();
 166   //   Rewriter::garbageCollect();
 167   //   nm->reclaimZombiesUntil(options::zombieHuntThreshold());
 168   // }
 169   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 170 }
 171
 172
 173 /**
 174  * Returns the value a is currently assigned to in the SAT solver
 175  * or null if the value is completely unassigned.
 176  *
 177  * @param a
 178  * @param fullModel whether to create a "full model," i.e., add
 179  * constants to equivalence classes that don't already have them
 180  *
 181  * @return
 182  */
 183 Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
 184   if (!hasBBTerm(a)) {
 185     return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
 186   }
 187
 188   Bits bits;
 189   getBBTerm(a, bits);
 190   Integer value(0);
 191   for (int i = bits.size() -1; i >= 0; --i) {
 192     prop::SatValue bit_value;
 193     if (d_cnfStream->hasLiteral(bits[i])) {
 194       prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
 195       bit_value = d_satSolver->value(bit);
 196       Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
 197     } else {
 198       if (!fullModel) return Node();
 199       // unconstrained bits default to false
 200       bit_value = prop::SAT_VALUE_FALSE;
 201     }
 202     Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
 203     value = value * 2 + bit_int;
 204   }
 205   return utils::mkConst(BitVector(bits.size(), value));
 206 }
 207
 208
 209 void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
 210   TNodeSet::iterator it = d_variables.begin();
 211   for (; it!= d_variables.end(); ++it) {
 212     TNode var = *it;
 213     if (d_bv->isLeaf(var) || isSharedTerm(var) ||
 214         (var.isVar() && var.getType().isBoolean()))  {
 215       // only shared terms could not have been bit-blasted
 216       Assert (hasBBTerm(var) || isSharedTerm(var));
 217
 218       Node const_value = getModelFromSatSolver(var, fullModel);
 219
 220       if(const_value != Node()) {
 221         Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= "
 222                                  << var << " "
 223                                  << const_value << "))\n";
 224         m->assertEquality(var, const_value, true);
 225       }
 226     }
 227   }
 228 }
 229
 230 void EagerBitblaster::setProofLog( BitVectorProof * bvp ) {
 231   d_bvp = bvp;
 232   d_satSolver->setProofLog(bvp);
 233   bvp->initCnfProof(d_cnfStream, d_nullContext);
 234 }
 235
 236 bool EagerBitblaster::isSharedTerm(TNode node) {
 237   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 238 }
 239
 240 } /* namespace CVC4::theory::bv; */
 241 } /* namespace CVC4::theory; */
 242 } /* namespace CVC4; */