Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/lazy_bitblaster.cpp	Lines:	209	304	68.8 %
Date:	2021-05-24	Branches:	346	1105	31.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Aina Niemetz, Mathias Preiner
 *
 * 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 lazy bv solver.
 */

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

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

namespace cvc5 {
namespace theory {
namespace bv {

namespace {

/* Determine the number of uncached nodes that a given node consists of.  */
uint64_t numNodes(TNode node, utils::NodeSet& seen)
{
  std::vector<TNode> stack;
  uint64_t res = 0;

  stack.push_back(node);
  while (!stack.empty())
  {
    Node n = stack.back();
    stack.pop_back();

    if (seen.find(n) != seen.end()) continue;

    res += 1;
    seen.insert(n);
    stack.insert(stack.end(), n.begin(), n.end());
  }
  return res;
}
}

TLazyBitblaster::TLazyBitblaster(context::Context* c,
                                 bv::BVSolverLazy* bv,
                                 const std::string name,
                                 bool emptyNotify)
    : TBitblaster<Node>(),
      d_bv(bv),
      d_ctx(c),
      d_nullRegistrar(new prop::NullRegistrar()),
      d_assertedAtoms(new (true) context::CDList<prop::SatLiteral>(c)),
      d_explanations(new (true) ExplanationMap(c)),
      d_variables(),
      d_bbAtoms(),
      d_abstraction(NULL),
      d_emptyNotify(emptyNotify),
      d_fullModelAssertionLevel(c, 0),
      d_name(name),
      d_statistics(name + "::")
{
  d_satSolver.reset(prop::SatSolverFactory::createMinisat(
      c, smtStatisticsRegistry(), name + "::"));

  ResourceManager* rm = smt::currentResourceManager();
  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
                                        d_nullRegistrar.get(),
                                        d_nullContext.get(),
                                        nullptr,
                                        rm,
                                        prop::FormulaLitPolicy::INTERNAL,
                                        "LazyBitblaster"));

  d_satSolverNotify.reset(
      d_emptyNotify
          ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
          : (prop::BVSatSolverNotify*)new MinisatNotify(
                d_cnfStream.get(), bv, this));

  d_satSolver->setNotify(d_satSolverNotify.get());
}

void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
  d_abstraction = abs;
}

TLazyBitblaster::~TLazyBitblaster()
{
  d_assertedAtoms->deleteSelf();
  d_explanations->deleteSelf();
}


/**
 * 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 TLazyBitblaster::bbAtom(TNode node)
{
  NodeManager* nm = NodeManager::currentNM();
  node = node.getKind() == kind::NOT ? node[0] : node;

  if (hasBBAtom(node))
  {
    return;
  }

  // make sure it is marked as an atom
  addAtom(node);

  Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
  ++d_statistics.d_numAtoms;

  /// if we are using bit-vector abstraction bit-blast the original
  /// interpretation
  if (options::bvAbstraction() && d_abstraction != NULL
      && d_abstraction->isAbstraction(node))
  {
    // node must be of the form P(args) = bv1
    Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node));

    Node atom_bb;
    if (expansion.getKind() == kind::CONST_BOOLEAN)
    {
      atom_bb = expansion;
    }
    else
    {
      Assert(expansion.getKind() == kind::AND);
      std::vector<Node> atoms;
      for (unsigned i = 0; i < expansion.getNumChildren(); ++i)
      {
        Node normalized_i = Rewriter::rewrite(expansion[i]);
        Node atom_i =
            normalized_i.getKind() != kind::CONST_BOOLEAN
                ? Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()](
                      normalized_i, this))
                : normalized_i;
        atoms.push_back(atom_i);
      }
      atom_bb = utils::mkAnd(atoms);
    }
    Assert(!atom_bb.isNull());
    Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb);
    storeBBAtom(node, atom_bb);
    d_cnfStream->convertAndAssert(atom_definition, false, false);
    return;
  }

  // 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 = nm->mkNode(kind::EQUAL, node, atom_bb);
  storeBBAtom(node, atom_bb);
  d_cnfStream->convertAndAssert(atom_definition, false, false);
}

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

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


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


void TLazyBitblaster::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);
}

uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen)
{
  node = node.getKind() == kind::NOT ? node[0] : node;
  if (!utils::isBitblastAtom(node)) { return 0; }
  Node atom_bb =
      Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
  uint64_t size = numNodes(atom_bb, seen);
  return size;
}

// cnf conversion ensures the atom represents itself
Node TLazyBitblaster::getBBAtom(TNode node) const {
  return node;
}

void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {

  if (hasBBTerm(node)) {
    getBBTerm(node, bits);
    return;
  }
  Assert(node.getType().isBitVector());

  d_bv->spendResource(Resource::BitblastStep);
  Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
  ++d_statistics.d_numTerms;

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

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

  storeBBTerm(node, bits);
}
/// Public methods

void TLazyBitblaster::addAtom(TNode atom) {
  d_cnfStream->ensureLiteral(atom);
  prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
  d_satSolver->addMarkerLiteral(lit);
}

void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
  prop::SatLiteral lit = d_cnfStream->getLiteral(atom);

  ++(d_statistics.d_numExplainedPropagations);
  if (options::bvEagerExplanations()) {
    Assert(d_explanations->find(lit) != d_explanations->end());
    const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get();
    for (unsigned i = 0; i < literal_explanation.size(); ++i) {
      explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
    }
    return;
  }

  std::vector<prop::SatLiteral> literal_explanation;
  d_satSolver->explain(lit, literal_explanation);
  for (unsigned i = 0; i < literal_explanation.size(); ++i) {
    explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
  }
}


/*
 * Asserts the clauses corresponding to the atom to the Sat Solver
 * by turning on the marker literal (i.e. setting it to false)
 * @param node the atom to be asserted
 *
 */

bool TLazyBitblaster::propagate() {
  return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
}

bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
  // strip the not
  TNode atom;
  if (lit.getKind() == kind::NOT) {
    atom = lit[0];
  } else {
    atom = lit;
  }
  Assert(utils::isBitblastAtom(atom));

  Assert(hasBBAtom(atom));

  prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom);

  if(lit.getKind() == kind::NOT) {
    markerLit = ~markerLit;
  }

  Debug("bitvector-bb")
      << "BVSolverLazy::TLazyBitblaster::assertToSat asserting node: " << atom
      << "\n";
  Debug("bitvector-bb")
      << "BVSolverLazy::TLazyBitblaster::assertToSat with literal:   "
      << markerLit << "\n";

  prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);

  d_assertedAtoms->push_back(markerLit);

  return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN;
}

/**
 * Calls the solve method for the Sat Solver.
 * passing it the marker literals to be asserted
 *
 * @return true for sat, and false for unsat
 */

bool TLazyBitblaster::solve() {
  if (Trace.isOn("bitvector")) {
    Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms ";
    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
    for (; it != d_assertedAtoms->end(); ++it) {
      Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
    }
  }
  Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
  d_fullModelAssertionLevel.set(d_bv->numAssertions());
  return prop::SAT_VALUE_TRUE == d_satSolver->solve();
}

prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) {
  if (Trace.isOn("bitvector")) {
    Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms ";
    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
    for (; it != d_assertedAtoms->end(); ++it) {
      Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
    }
  }
  Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n";
  return d_satSolver->solve(budget);
}

void TLazyBitblaster::getConflict(std::vector<TNode>& conflict)
{
  NodeManager* nm = NodeManager::currentNM();
  prop::SatClause conflictClause;
  d_satSolver->getUnsatCore(conflictClause);

  for (unsigned i = 0; i < conflictClause.size(); i++)
  {
    prop::SatLiteral lit = conflictClause[i];
    TNode atom = d_cnfStream->getNode(lit);
    Node not_atom;
    if (atom.getKind() == kind::NOT)
    {
      not_atom = atom[0];
    }
    else
    {
      not_atom = nm->mkNode(kind::NOT, atom);
    }
    conflict.push_back(not_atom);
  }
}

TLazyBitblaster::Statistics::Statistics(const std::string& prefix)
    : d_numTermClauses(
        smtStatisticsRegistry().registerInt(prefix + "NumTermSatClauses")),
      d_numAtomClauses(
          smtStatisticsRegistry().registerInt(prefix + "NumAtomSatClauses")),
      d_numTerms(
          smtStatisticsRegistry().registerInt(prefix + "NumBitblastedTerms")),
      d_numAtoms(
          smtStatisticsRegistry().registerInt(prefix + "NumBitblastedAtoms")),
      d_numExplainedPropagations(smtStatisticsRegistry().registerInt(
          prefix + "NumExplainedPropagations")),
      d_numBitblastingPropagations(smtStatisticsRegistry().registerInt(
          prefix + "NumBitblastingPropagations")),
      d_bitblastTimer(
          smtStatisticsRegistry().registerTimer(prefix + "BitblastTimer"))
{
}

bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
  if(options::bvEagerExplanations()) {
    // compute explanation
    if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) {
      std::vector<prop::SatLiteral> literal_explanation;
      d_lazyBB->d_satSolver->explain(lit, literal_explanation);
      d_lazyBB->d_explanations->insert(lit, literal_explanation);
    } else {
      // we propagated it at a lower level
      return true;
    }
  }
  ++(d_lazyBB->d_statistics.d_numBitblastingPropagations);
  TNode atom = d_cnf->getNode(lit);
  return d_bv->storePropagation(atom, SUB_BITBLAST);
}

void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
  if (clause.size() > 1) {
    NodeBuilder lemmab(kind::OR);
    for (unsigned i = 0; i < clause.size(); ++ i) {
      lemmab << d_cnf->getNode(clause[i]);
    }
    Node lemma = lemmab;
    d_bv->d_im.lemma(lemma, InferenceId::BV_LAZY_LEMMA);
  } else {
    d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::BV_LAZY_LEMMA);
  }
}

void TLazyBitblaster::MinisatNotify::spendResource(Resource r)
{
  d_bv->spendResource(r);
}

void TLazyBitblaster::MinisatNotify::safePoint(Resource r)
{
  d_bv->d_im.safePoint(r);
}

EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b)
{
  int numAssertions = d_bv->numAssertions();
  bool has_full_model =
      numAssertions != 0 && d_fullModelAssertionLevel.get() == numAssertions;

  Debug("bv-equality-status")
      << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n";
  Debug("bv-equality-status")
      << "BVSatSolver has full model? " << has_full_model << "\n";

  // First check if it trivially rewrites to false/true
  Node a_eq_b =
      Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b));

  if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE;
  if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;

  if (!has_full_model)
  {
    return theory::EQUALITY_UNKNOWN;
  }

  // Check if cache is valid (invalidated in check and pops)
  if (d_bv->d_invalidateModelCache.get())
  {
    invalidateModelCache();
  }
  d_bv->d_invalidateModelCache.set(false);

  Node a_value = getTermModel(a, true);
  Node b_value = getTermModel(b, true);

  Assert(a_value.isConst() && b_value.isConst());

  if (a_value == b_value)
  {
    Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n";
    return theory::EQUALITY_TRUE_IN_MODEL;
  }
  Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n";
  return theory::EQUALITY_FALSE_IN_MODEL;
}

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

bool TLazyBitblaster::hasValue(TNode a) {
  Assert(hasBBTerm(a));
  Bits bits;
  getBBTerm(a, bits);
  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);
      if (bit_value ==  prop::SAT_VALUE_UNKNOWN)
        return false;
    } else {
      return false;
    }
  }
  return true;
}
/**
 * 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 TLazyBitblaster::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 TLazyBitblaster::collectModelValues(TheoryModel* m,
                                         const std::set<Node>& termSet)
{
  for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
    TNode var = *it;
    // not actually a leaf of the bit-vector theory
    if (d_variables.find(var) == d_variables.end())
      continue;

    Assert(Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
    // only shared terms could not have been bit-blasted
    Assert(hasBBTerm(var) || isSharedTerm(var));

    Node const_value = getModelFromSatSolver(var, true);
    Assert(const_value.isNull() || const_value.isConst());
    if(const_value != Node()) {
      Debug("bitvector-model")
          << "TLazyBitblaster::collectModelValues (assert (= " << var << " "
          << const_value << "))\n";
      if (!m->assertEquality(var, const_value, true))
      {
        return false;
      }
    }
  }
  return true;
}

void TLazyBitblaster::clearSolver() {
  Assert(d_ctx->getLevel() == 0);
  d_assertedAtoms->deleteSelf();
  d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
  d_explanations->deleteSelf();
  d_explanations = new(true) ExplanationMap(d_ctx);
  d_bbAtoms.clear();
  d_variables.clear();
  d_termCache.clear();

  invalidateModelCache();
  // recreate sat solver
  d_satSolver.reset(
      prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
  ResourceManager* rm = smt::currentResourceManager();
  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
                                        d_nullRegistrar.get(),
                                        d_nullContext.get(),
                                        nullptr,
                                        rm));
  d_satSolverNotify.reset(
      d_emptyNotify
          ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
          : (prop::BVSatSolverNotify*)new MinisatNotify(
                d_cnfStream.get(), d_bv, this));
  d_satSolver->setNotify(d_satSolverNotify.get());
}

}  // 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, Aina Niemetz, Mathias Preiner
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 lazy bv solver.
14		*/
15
16		#include "theory/bv/bitblast/lazy_bitblaster.h"
17
18		#include "cvc5_private.h"
19		#include "options/bv_options.h"
20		#include "prop/cnf_stream.h"
21		#include "prop/sat_solver.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/abstraction.h"
26		#include "theory/bv/bv_solver_lazy.h"
27		#include "theory/bv/theory_bv.h"
28		#include "theory/bv/theory_bv_utils.h"
29		#include "theory/rewriter.h"
30		#include "theory/theory_model.h"
31
32		namespace cvc5 {
33		namespace theory {
34		namespace bv {
35
36		namespace {
37
38		/* Determine the number of uncached nodes that a given node consists of. */
39		uint64_t numNodes(TNode node, utils::NodeSet& seen)
40		{
41		std::vector<TNode> stack;
42		uint64_t res = 0;
43
44		stack.push_back(node);
45		while (!stack.empty())
46		{
47		Node n = stack.back();
48		stack.pop_back();
49
50		if (seen.find(n) != seen.end()) continue;
51
52		res += 1;
53		seen.insert(n);
54		stack.insert(stack.end(), n.begin(), n.end());
55		}
56		return res;
57		}
58		}
59
60	9405	TLazyBitblaster::TLazyBitblaster(context::Context* c,
61		bv::BVSolverLazy* bv,
62		const std::string name,
63	9405	bool emptyNotify)
64		: TBitblaster<Node>(),
65		d_bv(bv),
66		d_ctx(c),
67	9405	d_nullRegistrar(new prop::NullRegistrar()),
68	9405	d_assertedAtoms(new (true) context::CDList<prop::SatLiteral>(c)),
69	9405	d_explanations(new (true) ExplanationMap(c)),
70		d_variables(),
71		d_bbAtoms(),
72		d_abstraction(NULL),
73		d_emptyNotify(emptyNotify),
74		d_fullModelAssertionLevel(c, 0),
75		d_name(name),
76	37620	d_statistics(name + "::")
77		{
78	18810	d_satSolver.reset(prop::SatSolverFactory::createMinisat(
79	18810	c, smtStatisticsRegistry(), name + "::"));
80
81	9405	ResourceManager* rm = smt::currentResourceManager();
82	28215	d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
83	9405	d_nullRegistrar.get(),
84	9405	d_nullContext.get(),
85		nullptr,
86		rm,
87		prop::FormulaLitPolicy::INTERNAL,
88	9405	"LazyBitblaster"));
89
90	28215	d_satSolverNotify.reset(
91	9405	d_emptyNotify
92		? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
93		: (prop::BVSatSolverNotify*)new MinisatNotify(
94	9405	d_cnfStream.get(), bv, this));
95
96	9405	d_satSolver->setNotify(d_satSolverNotify.get());
97	9405	}
98
99	2	void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
100	2	d_abstraction = abs;
101	2	}
102
103	28215	TLazyBitblaster::~TLazyBitblaster()
104		{
105	9405	d_assertedAtoms->deleteSelf();
106	9405	d_explanations->deleteSelf();
107	18810	}
108
109
110		/**
111		* Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
112		* NOTE: duplicate clauses are not detected because of marker literal
113		* @param node the atom to be bitblasted
114		*
115		*/
116	861800	void TLazyBitblaster::bbAtom(TNode node)
117		{
118	861800	NodeManager* nm = NodeManager::currentNM();
119	861800	node = node.getKind() == kind::NOT ? node[0] : node;
120
121	861800	if (hasBBAtom(node))
122		{
123	1575228	return;
124		}
125
126		// make sure it is marked as an atom
127	74186	addAtom(node);
128
129	74186	Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
130	74186	++d_statistics.d_numAtoms;
131
132		/// if we are using bit-vector abstraction bit-blast the original
133		/// interpretation
134	148384	if (options::bvAbstraction() && d_abstraction != NULL
135	148384	&& d_abstraction->isAbstraction(node))
136		{
137		// node must be of the form P(args) = bv1
138		Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node));
139
140		Node atom_bb;
141		if (expansion.getKind() == kind::CONST_BOOLEAN)
142		{
143		atom_bb = expansion;
144		}
145		else
146		{
147		Assert(expansion.getKind() == kind::AND);
148		std::vector<Node> atoms;
149		for (unsigned i = 0; i < expansion.getNumChildren(); ++i)
150		{
151		Node normalized_i = Rewriter::rewrite(expansion[i]);
152		Node atom_i =
153		normalized_i.getKind() != kind::CONST_BOOLEAN
154		? Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()](
155		normalized_i, this))
156		: normalized_i;
157		atoms.push_back(atom_i);
158		}
159		atom_bb = utils::mkAnd(atoms);
160		}
161		Assert(!atom_bb.isNull());
162		Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb);
163		storeBBAtom(node, atom_bb);
164		d_cnfStream->convertAndAssert(atom_definition, false, false);
165		return;
166		}
167
168		// the bitblasted definition of the atom
169	148372	Node normalized = Rewriter::rewrite(node);
170		Node atom_bb =
171	74186	normalized.getKind() != kind::CONST_BOOLEAN
172	74143	? d_atomBBStrategies[normalized.getKind()](normalized, this)
173	222515	: normalized;
174
175	74186	atom_bb = Rewriter::rewrite(atom_bb);
176
177		// asserting that the atom is true iff the definition holds
178	148372	Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb);
179	74186	storeBBAtom(node, atom_bb);
180	74186	d_cnfStream->convertAndAssert(atom_definition, false, false);
181		}
182
183	74186	void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
184	74186	d_bbAtoms.insert(atom);
185	74186	}
186
187	95820	void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) {
188	95820	d_termCache.insert(std::make_pair(node, bits));
189	95820	}
190
191
192	1708813	bool TLazyBitblaster::hasBBAtom(TNode atom) const {
193	1708813	return d_bbAtoms.find(atom) != d_bbAtoms.end();
194		}
195
196
197	18440	void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
198	18440	Assert(bits.size() == 0);
199	226240	for (unsigned i = 0; i < utils::getSize(var); ++i) {
200	207800	bits.push_back(utils::mkBitOf(var, i));
201		}
202	18440	d_variables.insert(var);
203	18440	}
204
205		uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen)
206		{
207		node = node.getKind() == kind::NOT ? node[0] : node;
208		if (!utils::isBitblastAtom(node)) { return 0; }
209		Node atom_bb =
210		Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
211		uint64_t size = numNodes(atom_bb, seen);
212		return size;
213		}
214
215		// cnf conversion ensures the atom represents itself
216		Node TLazyBitblaster::getBBAtom(TNode node) const {
217		return node;
218		}
219
220	307908	void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
221
222	307908	if (hasBBTerm(node)) {
223	212784	getBBTerm(node, bits);
224	212784	return;
225		}
226	95124	Assert(node.getType().isBitVector());
227
228	95124	d_bv->spendResource(Resource::BitblastStep);
229	95124	Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
230	95124	++d_statistics.d_numTerms;
231
232	95124	d_termBBStrategies[node.getKind()] (node, bits,this);
233
234	95124	Assert(bits.size() == utils::getSize(node));
235
236	95124	storeBBTerm(node, bits);
237		}
238		/// Public methods
239
240	74186	void TLazyBitblaster::addAtom(TNode atom) {
241	74186	d_cnfStream->ensureLiteral(atom);
242	74186	prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
243	74186	d_satSolver->addMarkerLiteral(lit);
244	74186	}
245
246	20101	void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
247	20101	prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
248
249	20101	++(d_statistics.d_numExplainedPropagations);
250	20101	if (options::bvEagerExplanations()) {
251	11236	Assert(d_explanations->find(lit) != d_explanations->end());
252	11236	const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get();
253	44650	for (unsigned i = 0; i < literal_explanation.size(); ++i) {
254	33414	explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
255		}
256	22472	return;
257		}
258
259	17730	std::vector<prop::SatLiteral> literal_explanation;
260	8865	d_satSolver->explain(lit, literal_explanation);
261	44522	for (unsigned i = 0; i < literal_explanation.size(); ++i) {
262	35657	explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
263		}
264		}
265
266
267		/*
268		* Asserts the clauses corresponding to the atom to the Sat Solver
269		* by turning on the marker literal (i.e. setting it to false)
270		* @param node the atom to be asserted
271		*
272		*/
273
274	190624	bool TLazyBitblaster::propagate() {
275	190624	return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
276		}
277
278	762762	bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
279		// strip the not
280	1525524	TNode atom;
281	762762	if (lit.getKind() == kind::NOT) {
282	313303	atom = lit[0];
283		} else {
284	449459	atom = lit;
285		}
286	762762	Assert(utils::isBitblastAtom(atom));
287
288	762762	Assert(hasBBAtom(atom));
289
290	762762	prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom);
291
292	762762	if(lit.getKind() == kind::NOT) {
293	313303	markerLit = ~markerLit;
294		}
295
296	1525524	Debug("bitvector-bb")
297	762762	<< "BVSolverLazy::TLazyBitblaster::assertToSat asserting node: " << atom
298	762762	<< "\n";
299	1525524	Debug("bitvector-bb")
300	762762	<< "BVSolverLazy::TLazyBitblaster::assertToSat with literal: "
301	762762	<< markerLit << "\n";
302
303	762762	prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
304
305	762762	d_assertedAtoms->push_back(markerLit);
306
307	1525524	return ret == prop::SAT_VALUE_TRUE \|\| ret == prop::SAT_VALUE_UNKNOWN;
308		}
309
310		/**
311		* Calls the solve method for the Sat Solver.
312		* passing it the marker literals to be asserted
313		*
314		* @return true for sat, and false for unsat
315		*/
316
317	10064	bool TLazyBitblaster::solve() {
318	10064	if (Trace.isOn("bitvector")) {
319		Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms ";
320		context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
321		for (; it != d_assertedAtoms->end(); ++it) {
322		Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n";
323		}
324		}
325	10064	Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
326	10064	d_fullModelAssertionLevel.set(d_bv->numAssertions());
327	10064	return prop::SAT_VALUE_TRUE == d_satSolver->solve();
328		}
329
330		prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) {
331		if (Trace.isOn("bitvector")) {
332		Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms ";
333		context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
334		for (; it != d_assertedAtoms->end(); ++it) {
335		Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n";
336		}
337		}
338		Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n";
339		return d_satSolver->solve(budget);
340		}
341
342	14409	void TLazyBitblaster::getConflict(std::vector<TNode>& conflict)
343		{
344	14409	NodeManager* nm = NodeManager::currentNM();
345	28818	prop::SatClause conflictClause;
346	14409	d_satSolver->getUnsatCore(conflictClause);
347
348	172519	for (unsigned i = 0; i < conflictClause.size(); i++)
349		{
350	158110	prop::SatLiteral lit = conflictClause[i];
351	316220	TNode atom = d_cnfStream->getNode(lit);
352	316220	Node not_atom;
353	158110	if (atom.getKind() == kind::NOT)
354		{
355	128864	not_atom = atom[0];
356		}
357		else
358		{
359	29246	not_atom = nm->mkNode(kind::NOT, atom);
360		}
361	158110	conflict.push_back(not_atom);
362		}
363	14409	}
364
365	9405	TLazyBitblaster::Statistics::Statistics(const std::string& prefix)
366		: d_numTermClauses(
367	18810	smtStatisticsRegistry().registerInt(prefix + "NumTermSatClauses")),
368		d_numAtomClauses(
369	18810	smtStatisticsRegistry().registerInt(prefix + "NumAtomSatClauses")),
370		d_numTerms(
371	18810	smtStatisticsRegistry().registerInt(prefix + "NumBitblastedTerms")),
372		d_numAtoms(
373	18810	smtStatisticsRegistry().registerInt(prefix + "NumBitblastedAtoms")),
374	9405	d_numExplainedPropagations(smtStatisticsRegistry().registerInt(
375	18810	prefix + "NumExplainedPropagations")),
376	9405	d_numBitblastingPropagations(smtStatisticsRegistry().registerInt(
377	18810	prefix + "NumBitblastingPropagations")),
378		d_bitblastTimer(
379	65835	smtStatisticsRegistry().registerTimer(prefix + "BitblastTimer"))
380		{
381	9405	}
382
383	2125902	bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
384	2125902	if(options::bvEagerExplanations()) {
385		// compute explanation
386	1133979	if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) {
387	206956	std::vector<prop::SatLiteral> literal_explanation;
388	103478	d_lazyBB->d_satSolver->explain(lit, literal_explanation);
389	103478	d_lazyBB->d_explanations->insert(lit, literal_explanation);
390		} else {
391		// we propagated it at a lower level
392	1030501	return true;
393		}
394		}
395	1095401	++(d_lazyBB->d_statistics.d_numBitblastingPropagations);
396	2190802	TNode atom = d_cnf->getNode(lit);
397	1095401	return d_bv->storePropagation(atom, SUB_BITBLAST);
398		}
399
400		void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
401		if (clause.size() > 1) {
402		NodeBuilder lemmab(kind::OR);
403		for (unsigned i = 0; i < clause.size(); ++ i) {
404		lemmab << d_cnf->getNode(clause[i]);
405		}
406		Node lemma = lemmab;
407		d_bv->d_im.lemma(lemma, InferenceId::BV_LAZY_LEMMA);
408		} else {
409		d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::BV_LAZY_LEMMA);
410		}
411		}
412
413	1608	void TLazyBitblaster::MinisatNotify::spendResource(Resource r)
414		{
415	1608	d_bv->spendResource(r);
416	1608	}
417
418	22061132	void TLazyBitblaster::MinisatNotify::safePoint(Resource r)
419		{
420	22061132	d_bv->d_im.safePoint(r);
421	22061132	}
422
423	29399	EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b)
424		{
425	29399	int numAssertions = d_bv->numAssertions();
426		bool has_full_model =
427	29399	numAssertions != 0 && d_fullModelAssertionLevel.get() == numAssertions;
428
429	58798	Debug("bv-equality-status")
430	29399	<< "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n";
431	58798	Debug("bv-equality-status")
432	29399	<< "BVSatSolver has full model? " << has_full_model << "\n";
433
434		// First check if it trivially rewrites to false/true
435		Node a_eq_b =
436	58798	Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b));
437
438	29399	if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE;
439	26681	if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;
440
441	26681	if (!has_full_model)
442		{
443	102	return theory::EQUALITY_UNKNOWN;
444		}
445
446		// Check if cache is valid (invalidated in check and pops)
447	26579	if (d_bv->d_invalidateModelCache.get())
448		{
449	86	invalidateModelCache();
450		}
451	26579	d_bv->d_invalidateModelCache.set(false);
452
453	53158	Node a_value = getTermModel(a, true);
454	53158	Node b_value = getTermModel(b, true);
455
456	26579	Assert(a_value.isConst() && b_value.isConst());
457
458	26579	if (a_value == b_value)
459		{
460	1696	Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n";
461	1696	return theory::EQUALITY_TRUE_IN_MODEL;
462		}
463	24883	Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n";
464	24883	return theory::EQUALITY_FALSE_IN_MODEL;
465		}
466
467	5928	bool TLazyBitblaster::isSharedTerm(TNode node) {
468	5928	return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
469		}
470
471		bool TLazyBitblaster::hasValue(TNode a) {
472		Assert(hasBBTerm(a));
473		Bits bits;
474		getBBTerm(a, bits);
475		for (int i = bits.size() -1; i >= 0; --i) {
476		prop::SatValue bit_value;
477		if (d_cnfStream->hasLiteral(bits[i])) {
478		prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
479		bit_value = d_satSolver->value(bit);
480		if (bit_value == prop::SAT_VALUE_UNKNOWN)
481		return false;
482		} else {
483		return false;
484		}
485		}
486		return true;
487		}
488		/**
489		* Returns the value a is currently assigned to in the SAT solver
490		* or null if the value is completely unassigned.
491		*
492		* @param a
493		* @param fullModel whether to create a "full model," i.e., add
494		* constants to equivalence classes that don't already have them
495		*
496		* @return
497		*/
498	21000	Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
499	21000	if (!hasBBTerm(a)) {
500	262	return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
501		}
502
503	41476	Bits bits;
504	20738	getBBTerm(a, bits);
505	41476	Integer value(0);
506	279436	for (int i = bits.size() -1; i >= 0; --i) {
507		prop::SatValue bit_value;
508	258752	if (d_cnfStream->hasLiteral(bits[i])) {
509	255819	prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
510	255819	bit_value = d_satSolver->value(bit);
511	255819	Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
512		} else {
513	2987	if (!fullModel) return Node();
514		// unconstrained bits default to false
515	2879	bit_value = prop::SAT_VALUE_FALSE;
516		}
517	517396	Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
518	258698	value = value * 2 + bit_int;
519		}
520	20684	return utils::mkConst(bits.size(), value);
521		}
522
523	3186	bool TLazyBitblaster::collectModelValues(TheoryModel* m,
524		const std::set<Node>& termSet)
525		{
526	399160	for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
527	416482	TNode var = *it;
528		// not actually a leaf of the bit-vector theory
529	395974	if (d_variables.find(var) == d_variables.end())
530	375466	continue;
531
532	20508	Assert(Theory::theoryOf(var) == theory::THEORY_BV \|\| isSharedTerm(var));
533		// only shared terms could not have been bit-blasted
534	20508	Assert(hasBBTerm(var) \|\| isSharedTerm(var));
535
536	41016	Node const_value = getModelFromSatSolver(var, true);
537	20508	Assert(const_value.isNull() \|\| const_value.isConst());
538	20508	if(const_value != Node()) {
539	41016	Debug("bitvector-model")
540	20508	<< "TLazyBitblaster::collectModelValues (assert (= " << var << " "
541	20508	<< const_value << "))\n";
542	20508	if (!m->assertEquality(var, const_value, true))
543		{
544		return false;
545		}
546		}
547		}
548	3186	return true;
549		}
550
551		void TLazyBitblaster::clearSolver() {
552		Assert(d_ctx->getLevel() == 0);
553		d_assertedAtoms->deleteSelf();
554		d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
555		d_explanations->deleteSelf();
556		d_explanations = new(true) ExplanationMap(d_ctx);
557		d_bbAtoms.clear();
558		d_variables.clear();
559		d_termCache.clear();
560
561		invalidateModelCache();
562		// recreate sat solver
563		d_satSolver.reset(
564		prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
565		ResourceManager* rm = smt::currentResourceManager();
566		d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
567		d_nullRegistrar.get(),
568		d_nullContext.get(),
569		nullptr,
570		rm));
571		d_satSolverNotify.reset(
572		d_emptyNotify
573		? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
574		: (prop::BVSatSolverNotify*)new MinisatNotify(
575		d_cnfStream.get(), d_bv, this));
576		d_satSolver->setNotify(d_satSolverNotify.get());
577		}
578
579		} // namespace bv
580		} // namespace theory
581	28191	} // namespace cvc5