src/theory/bv/bv_eager_solver.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mathias Preiner, Liana Hadarean, Tim King
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Eager bit-blasting solver.
  14  */
  15
  16 #include "theory/bv/bv_eager_solver.h"
  17
  18 #include "options/base_options.h"
  19 #include "options/bv_options.h"
  20 #include "options/smt_options.h"
  21 #include "theory/bv/bitblast/aig_bitblaster.h"
  22 #include "theory/bv/bitblast/eager_bitblaster.h"
  23
  24 using namespace std;
  25
  26 namespace cvc5 {
  27 namespace theory {
  28 namespace bv {
  29
  30 EagerBitblastSolver::EagerBitblastSolver(context::Context* c, BVSolverLazy* bv)
  31     : d_assertionSet(c),
  32       d_assumptionSet(c),
  33       d_context(c),
  34       d_bitblaster(),
  35       d_aigBitblaster(),
  36       d_useAig(options::bitvectorAig()),
  37       d_bv(bv)
  38 {
  39 }
  40
  41 EagerBitblastSolver::~EagerBitblastSolver() {}
  42
  43 void EagerBitblastSolver::turnOffAig() {
  44   Assert(d_aigBitblaster == nullptr && d_bitblaster == nullptr);
  45   d_useAig = false;
  46 }
  47
  48 void EagerBitblastSolver::initialize() {
  49   Assert(!isInitialized());
  50   if (d_useAig) {
  51 #ifdef CVC5_USE_ABC
  52     d_aigBitblaster.reset(new AigBitblaster());
  53 #else
  54     Unreachable();
  55 #endif
  56   } else {
  57     d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
  58   }
  59 }
  60
  61 bool EagerBitblastSolver::isInitialized() {
  62   const bool init = d_aigBitblaster != nullptr || d_bitblaster != nullptr;
  63   Assert(!init || !d_useAig || d_aigBitblaster);
  64   Assert(!init || d_useAig || d_bitblaster);
  65   return init;
  66 }
  67
  68 void EagerBitblastSolver::assertFormula(TNode formula) {
  69   d_bv->spendResource(Resource::BvEagerAssertStep);
  70   Assert(isInitialized());
  71   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula " << formula
  72                            << "\n";
  73   if (options::incrementalSolving() && d_context->getLevel() > 1)
  74   {
  75     d_assumptionSet.insert(formula);
  76   }
  77   d_assertionSet.insert(formula);
  78   // ensures all atoms are bit-blasted and converted to AIG
  79   if (d_useAig) {
  80 #ifdef CVC5_USE_ABC
  81     d_aigBitblaster->bbFormula(formula);
  82 #else
  83     Unreachable();
  84 #endif
  85   }
  86   else
  87   {
  88     d_bitblaster->bbFormula(formula);
  89   }
  90 }
  91
  92 bool EagerBitblastSolver::checkSat() {
  93   Assert(isInitialized());
  94   if (d_assertionSet.empty()) {
  95     return true;
  96   }
  97
  98   if (d_useAig) {
  99 #ifdef CVC5_USE_ABC
 100     const std::vector<Node> assertions = {d_assertionSet.key_begin(),
 101                                           d_assertionSet.key_end()};
 102     Assert(!assertions.empty());
 103
 104     Node query = utils::mkAnd(assertions);
 105     return d_aigBitblaster->solve(query);
 106 #else
 107     Unreachable();
 108 #endif
 109   }
 110
 111   if (options::incrementalSolving())
 112   {
 113     const std::vector<Node> assumptions = {d_assumptionSet.key_begin(),
 114                                            d_assumptionSet.key_end()};
 115     return d_bitblaster->solve(assumptions);
 116   }
 117   return d_bitblaster->solve();
 118 }
 119
 120 bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
 121 {
 122   AlwaysAssert(!d_useAig && d_bitblaster);
 123   return d_bitblaster->collectModelInfo(m, fullModel);
 124 }
 125
 126 }  // namespace bv
 127 }  // namespace theory
 128 }  // namespace cvc5