Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/eager_bitblaster.cpp	Lines:	118	131	90.1 %
Date:	2021-05-22	Branches:	198	569	34.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Mathias Preiner, Andres Noetzli
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Bitblaster for the eager bv solver.
 */

#include "theory/bv/bitblast/eager_bitblaster.h"

#include "cvc5_private.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver_factory.h"
#include "smt/smt_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv.h"
#include "theory/theory_model.h"

namespace cvc5 {
namespace theory {
namespace bv {

EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
    : TBitblaster<Node>(),
      d_context(c),
      d_satSolver(),
      d_bitblastingRegistrar(new BitblastingRegistrar(this)),
      d_bv(theory_bv),
      d_bbAtoms(),
      d_variables(),
      d_notify()
{
  prop::SatSolver *solver = nullptr;
  switch (options::bvSatSolver())
  {
    case options::SatSolverMode::MINISAT:
    {
      prop::BVSatSolverInterface* minisat =
          prop::SatSolverFactory::createMinisat(
              d_nullContext.get(),
              smtStatisticsRegistry(),
              "theory::bv::EagerBitblaster::");
      d_notify.reset(new MinisatEmptyNotify());
      minisat->setNotify(d_notify.get());
      solver = minisat;
      break;
    }
    case options::SatSolverMode::CADICAL:
      solver = prop::SatSolverFactory::createCadical(
          smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
      break;
    case options::SatSolverMode::CRYPTOMINISAT:
      solver = prop::SatSolverFactory::createCryptoMinisat(
          smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
      break;
    case options::SatSolverMode::KISSAT:
      solver = prop::SatSolverFactory::createKissat(
          smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
      break;
    default: Unreachable() << "Unknown SAT solver type";
  }
  d_satSolver.reset(solver);
  ResourceManager* rm = smt::currentResourceManager();
  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
                                        d_bitblastingRegistrar.get(),
                                        d_nullContext.get(),
                                        nullptr,
                                        rm,
                                        prop::FormulaLitPolicy::INTERNAL,
                                        "EagerBitblaster"));
}

EagerBitblaster::~EagerBitblaster() {}

void EagerBitblaster::bbFormula(TNode node)
{
  /* For incremental eager solving we assume formulas at context levels > 1. */
  if (options::incrementalSolving() && d_context->getLevel() > 1)
  {
    d_cnfStream->ensureLiteral(node);
  }
  else
  {
    d_cnfStream->convertAndAssert(node, false, false);
  }
}

/**
 * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
 * NOTE: duplicate clauses are not detected because of marker literal
 * @param node the atom to be bitblasted
 *
 */
void EagerBitblaster::bbAtom(TNode node)
{
  node = node.getKind() == kind::NOT ? node[0] : node;
  if (node.getKind() == kind::BITVECTOR_BITOF
      || node.getKind() == kind::CONST_BOOLEAN || hasBBAtom(node))
  {
    return;
  }

  Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";

  // the bitblasted definition of the atom
  Node normalized = Rewriter::rewrite(node);
  Node atom_bb =
      normalized.getKind() != kind::CONST_BOOLEAN
          ? d_atomBBStrategies[normalized.getKind()](normalized, this)
          : normalized;

  atom_bb = Rewriter::rewrite(atom_bb);

  // asserting that the atom is true iff the definition holds
  Node atom_definition =
      NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb);

  AlwaysAssert(options::bitblastMode() == options::BitblastMode::EAGER);
  storeBBAtom(node, atom_bb);
  d_cnfStream->convertAndAssert(atom_definition, false, false);
}

void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
  d_bbAtoms.insert(atom);
}

void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
  d_termCache.insert(std::make_pair(node, bits));
}

bool EagerBitblaster::hasBBAtom(TNode atom) const {
  return d_bbAtoms.find(atom) != d_bbAtoms.end();
}

void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
  Assert(node.getType().isBitVector());

  if (hasBBTerm(node)) {
    getBBTerm(node, bits);
    return;
  }

  d_bv->spendResource(Resource::BitblastStep);
  Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";

  d_termBBStrategies[node.getKind()](node, bits, this);

  Assert(bits.size() == utils::getSize(node));

  storeBBTerm(node, bits);
}

void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
  Assert(bits.size() == 0);
  for (unsigned i = 0; i < utils::getSize(var); ++i) {
    bits.push_back(utils::mkBitOf(var, i));
  }
  d_variables.insert(var);
}

Node EagerBitblaster::getBBAtom(TNode node) const { return node; }

/**
 * Calls the solve method for the Sat Solver.
 *
 * @return true for sat, and false for unsat
 */

bool EagerBitblaster::solve() {
  if (Trace.isOn("bitvector")) {
    Trace("bitvector") << "EagerBitblaster::solve(). \n";
  }
  Debug("bitvector") << "EagerBitblaster::solve(). \n";
  // TODO: clear some memory
  // if (something) {
  //   NodeManager* nm= NodeManager::currentNM();
  //   Rewriter::garbageCollect();
  //   nm->reclaimZombiesUntil(options::zombieHuntThreshold());
  // }
  return prop::SAT_VALUE_TRUE == d_satSolver->solve();
}

bool EagerBitblaster::solve(const std::vector<Node>& assumptions)
{
  std::vector<prop::SatLiteral> assumpts;
  for (const Node& assumption : assumptions)
  {
    Assert(d_cnfStream->hasLiteral(assumption));
    assumpts.push_back(d_cnfStream->getLiteral(assumption));
  }
  return prop::SAT_VALUE_TRUE == d_satSolver->solve(assumpts);
}

/**
 * Returns the value a is currently assigned to in the SAT solver
 * or null if the value is completely unassigned.
 *
 * @param a
 * @param fullModel whether to create a "full model," i.e., add
 * constants to equivalence classes that don't already have them
 *
 * @return
 */
Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
  if (!hasBBTerm(a)) {
    return fullModel ? utils::mkConst(utils::getSize(a), 0u) : Node();
  }

  Bits bits;
  getBBTerm(a, bits);
  Integer value(0);
  for (int i = bits.size() - 1; i >= 0; --i) {
    prop::SatValue bit_value;
    if (d_cnfStream->hasLiteral(bits[i])) {
      prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
      bit_value = d_satSolver->value(bit);
      Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
    } else {
      if (!fullModel) return Node();
      // unconstrained bits default to false
      bit_value = prop::SAT_VALUE_FALSE;
    }
    Integer bit_int =
        bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
    value = value * 2 + bit_int;
  }
  return utils::mkConst(bits.size(), value);
}

bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
{
  NodeManager* nm = NodeManager::currentNM();

  // Collect the values for the bit-vector variables
  TNodeSet::iterator it = d_variables.begin();
  for (; it != d_variables.end(); ++it) {
    TNode var = *it;
    if (d_bv->isLeaf(var) || isSharedTerm(var) ||
        (var.isVar() && var.getType().isBoolean())) {
      // only shared terms could not have been bit-blasted
      Assert(hasBBTerm(var) || isSharedTerm(var));

      Node const_value = getModelFromSatSolver(var, true);

      if (const_value != Node()) {
        Debug("bitvector-model")
            << "EagerBitblaster::collectModelInfo (assert (= " << var << " "
            << const_value << "))\n";
        if (!m->assertEquality(var, const_value, true))
        {
          return false;
        }
      }
    }
  }

  // Collect the values for the Boolean variables
  std::vector<TNode> vars;
  d_cnfStream->getBooleanVariables(vars);
  for (TNode var : vars)
  {
    Assert(d_cnfStream->hasLiteral(var));
    prop::SatLiteral bit = d_cnfStream->getLiteral(var);
    prop::SatValue value = d_satSolver->value(bit);
    Assert(value != prop::SAT_VALUE_UNKNOWN);
    if (!m->assertEquality(
            var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
    {
      return false;
    }
  }
  return true;
}

bool EagerBitblaster::isSharedTerm(TNode node) {
  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
}


}  // namespace bv
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Liana Hadarean, Mathias Preiner, Andres Noetzli
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		* Bitblaster for the eager bv solver.
14		*/
15
16		#include "theory/bv/bitblast/eager_bitblaster.h"
17
18		#include "cvc5_private.h"
19		#include "options/bv_options.h"
20		#include "options/smt_options.h"
21		#include "prop/cnf_stream.h"
22		#include "prop/sat_solver_factory.h"
23		#include "smt/smt_engine.h"
24		#include "smt/smt_statistics_registry.h"
25		#include "theory/bv/bv_solver_lazy.h"
26		#include "theory/bv/theory_bv.h"
27		#include "theory/theory_model.h"
28
29		namespace cvc5 {
30		namespace theory {
31		namespace bv {
32
33	31	EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
34		: TBitblaster<Node>(),
35		d_context(c),
36		d_satSolver(),
37	31	d_bitblastingRegistrar(new BitblastingRegistrar(this)),
38		d_bv(theory_bv),
39		d_bbAtoms(),
40		d_variables(),
41	62	d_notify()
42		{
43	31	prop::SatSolver *solver = nullptr;
44	80	switch (options::bvSatSolver())
45		{
46	17	case options::SatSolverMode::MINISAT:
47		{
48		prop::BVSatSolverInterface* minisat =
49	34	prop::SatSolverFactory::createMinisat(
50		d_nullContext.get(),
51		smtStatisticsRegistry(),
52	17	"theory::bv::EagerBitblaster::");
53	17	d_notify.reset(new MinisatEmptyNotify());
54	17	minisat->setNotify(d_notify.get());
55	17	solver = minisat;
56	17	break;
57		}
58	5	case options::SatSolverMode::CADICAL:
59	5	solver = prop::SatSolverFactory::createCadical(
60		smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
61	5	break;
62	9	case options::SatSolverMode::CRYPTOMINISAT:
63	9	solver = prop::SatSolverFactory::createCryptoMinisat(
64		smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
65	9	break;
66		case options::SatSolverMode::KISSAT:
67		solver = prop::SatSolverFactory::createKissat(
68		smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
69		break;
70		default: Unreachable() << "Unknown SAT solver type";
71		}
72	31	d_satSolver.reset(solver);
73	31	ResourceManager* rm = smt::currentResourceManager();
74	93	d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
75	31	d_bitblastingRegistrar.get(),
76	31	d_nullContext.get(),
77		nullptr,
78		rm,
79		prop::FormulaLitPolicy::INTERNAL,
80	31	"EagerBitblaster"));
81	31	}
82
83	62	EagerBitblaster::~EagerBitblaster() {}
84
85	624	void EagerBitblaster::bbFormula(TNode node)
86		{
87		/* For incremental eager solving we assume formulas at context levels > 1. */
88	624	if (options::incrementalSolving() && d_context->getLevel() > 1)
89		{
90	48	d_cnfStream->ensureLiteral(node);
91		}
92		else
93		{
94	576	d_cnfStream->convertAndAssert(node, false, false);
95		}
96	624	}
97
98		/**
99		* Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
100		* NOTE: duplicate clauses are not detected because of marker literal
101		* @param node the atom to be bitblasted
102		*
103		*/
104	2975	void EagerBitblaster::bbAtom(TNode node)
105		{
106	2975	node = node.getKind() == kind::NOT ? node[0] : node;
107	5950	if (node.getKind() == kind::BITVECTOR_BITOF
108	5950	\|\| node.getKind() == kind::CONST_BOOLEAN \|\| hasBBAtom(node))
109		{
110	2274	return;
111		}
112
113	701	Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
114
115		// the bitblasted definition of the atom
116	1402	Node normalized = Rewriter::rewrite(node);
117		Node atom_bb =
118	701	normalized.getKind() != kind::CONST_BOOLEAN
119	701	? d_atomBBStrategies[normalized.getKind()](normalized, this)
120	2103	: normalized;
121
122	701	atom_bb = Rewriter::rewrite(atom_bb);
123
124		// asserting that the atom is true iff the definition holds
125		Node atom_definition =
126	1402	NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb);
127
128	701	AlwaysAssert(options::bitblastMode() == options::BitblastMode::EAGER);
129	701	storeBBAtom(node, atom_bb);
130	701	d_cnfStream->convertAndAssert(atom_definition, false, false);
131		}
132
133	701	void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
134	701	d_bbAtoms.insert(atom);
135	701	}
136
137	749	void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
138	749	d_termCache.insert(std::make_pair(node, bits));
139	749	}
140
141	701	bool EagerBitblaster::hasBBAtom(TNode atom) const {
142	701	return d_bbAtoms.find(atom) != d_bbAtoms.end();
143		}
144
145	2105	void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
146	2105	Assert(node.getType().isBitVector());
147
148	2105	if (hasBBTerm(node)) {
149	1356	getBBTerm(node, bits);
150	1356	return;
151		}
152
153	749	d_bv->spendResource(Resource::BitblastStep);
154	749	Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
155
156	749	d_termBBStrategies[node.getKind()](node, bits, this);
157
158	749	Assert(bits.size() == utils::getSize(node));
159
160	749	storeBBTerm(node, bits);
161		}
162
163	323	void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
164	323	Assert(bits.size() == 0);
165	2603	for (unsigned i = 0; i < utils::getSize(var); ++i) {
166	2280	bits.push_back(utils::mkBitOf(var, i));
167		}
168	323	d_variables.insert(var);
169	323	}
170
171		Node EagerBitblaster::getBBAtom(TNode node) const { return node; }
172
173		/**
174		* Calls the solve method for the Sat Solver.
175		*
176		* @return true for sat, and false for unsat
177		*/
178
179	19	bool EagerBitblaster::solve() {
180	19	if (Trace.isOn("bitvector")) {
181		Trace("bitvector") << "EagerBitblaster::solve(). \n";
182		}
183	19	Debug("bitvector") << "EagerBitblaster::solve(). \n";
184		// TODO: clear some memory
185		// if (something) {
186		// NodeManager* nm= NodeManager::currentNM();
187		// Rewriter::garbageCollect();
188		// nm->reclaimZombiesUntil(options::zombieHuntThreshold());
189		// }
190	19	return prop::SAT_VALUE_TRUE == d_satSolver->solve();
191		}
192
193	34	bool EagerBitblaster::solve(const std::vector<Node>& assumptions)
194		{
195	68	std::vector<prop::SatLiteral> assumpts;
196	72	for (const Node& assumption : assumptions)
197		{
198	38	Assert(d_cnfStream->hasLiteral(assumption));
199	38	assumpts.push_back(d_cnfStream->getLiteral(assumption));
200		}
201	68	return prop::SAT_VALUE_TRUE == d_satSolver->solve(assumpts);
202		}
203
204		/**
205		* Returns the value a is currently assigned to in the SAT solver
206		* or null if the value is completely unassigned.
207		*
208		* @param a
209		* @param fullModel whether to create a "full model," i.e., add
210		* constants to equivalence classes that don't already have them
211		*
212		* @return
213		*/
214	21	Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
215	21	if (!hasBBTerm(a)) {
216		return fullModel ? utils::mkConst(utils::getSize(a), 0u) : Node();
217		}
218
219	42	Bits bits;
220	21	getBBTerm(a, bits);
221	42	Integer value(0);
222	357	for (int i = bits.size() - 1; i >= 0; --i) {
223		prop::SatValue bit_value;
224	336	if (d_cnfStream->hasLiteral(bits[i])) {
225	336	prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
226	336	bit_value = d_satSolver->value(bit);
227	336	Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
228		} else {
229		if (!fullModel) return Node();
230		// unconstrained bits default to false
231		bit_value = prop::SAT_VALUE_FALSE;
232		}
233		Integer bit_int =
234	672	bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
235	336	value = value * 2 + bit_int;
236		}
237	21	return utils::mkConst(bits.size(), value);
238		}
239
240	9	bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
241		{
242	9	NodeManager* nm = NodeManager::currentNM();
243
244		// Collect the values for the bit-vector variables
245	9	TNodeSet::iterator it = d_variables.begin();
246	51	for (; it != d_variables.end(); ++it) {
247	42	TNode var = *it;
248	63	if (d_bv->isLeaf(var) \|\| isSharedTerm(var) \|\|
249	21	(var.isVar() && var.getType().isBoolean())) {
250		// only shared terms could not have been bit-blasted
251	21	Assert(hasBBTerm(var) \|\| isSharedTerm(var));
252
253	42	Node const_value = getModelFromSatSolver(var, true);
254
255	21	if (const_value != Node()) {
256	42	Debug("bitvector-model")
257	21	<< "EagerBitblaster::collectModelInfo (assert (= " << var << " "
258	21	<< const_value << "))\n";
259	21	if (!m->assertEquality(var, const_value, true))
260		{
261		return false;
262		}
263		}
264		}
265		}
266
267		// Collect the values for the Boolean variables
268	18	std::vector<TNode> vars;
269	9	d_cnfStream->getBooleanVariables(vars);
270	15	for (TNode var : vars)
271		{
272	6	Assert(d_cnfStream->hasLiteral(var));
273	6	prop::SatLiteral bit = d_cnfStream->getLiteral(var);
274	6	prop::SatValue value = d_satSolver->value(bit);
275	6	Assert(value != prop::SAT_VALUE_UNKNOWN);
276	12	if (!m->assertEquality(
277	12	var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
278		{
279		return false;
280		}
281		}
282	9	return true;
283		}
284
285		bool EagerBitblaster::isSharedTerm(TNode node) {
286		return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
287		}
288
289
290		} // namespace bv
291		} // namespace theory
292	28240	} // namespace cvc5