Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_solver_layered.cpp	Lines:	101	320	31.6 %
Date:	2021-09-17	Branches:	214	1306	16.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Liana Hadarean, Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Layered bit-vector solver.
 */

#include "theory/bv/bv_solver_layered.h"

#include "expr/node_algorithm.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
#include "theory/bv/bv_eager_solver.h"
#include "theory/bv/bv_subtheory_algebraic.h"
#include "theory/bv/bv_subtheory_bitblast.h"
#include "theory/bv/bv_subtheory_core.h"
#include "theory/bv/bv_subtheory_inequality.h"
#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
#include "theory/bv/theory_bv_rewriter.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"

using namespace cvc5::theory::bv::utils;

namespace cvc5 {
namespace theory {
namespace bv {

BVSolverLayered::BVSolverLayered(Env& env,
                                 TheoryBV& bv,
                                 context::Context* c,
                                 context::UserContext* u,
                                 ProofNodeManager* pnm,
                                 std::string name)
    : BVSolver(env, bv.d_state, bv.d_im),
      d_bv(bv),
      d_context(c),
      d_alreadyPropagatedSet(c),
      d_sharedTermsSet(c),
      d_subtheories(),
      d_subtheoryMap(),
      d_statistics(),
      d_staticLearnCache(),
      d_lemmasAdded(c, false),
      d_conflict(c, false),
      d_invalidateModelCache(c, true),
      d_literalsToPropagate(c),
      d_literalsToPropagateIndex(c, 0),
      d_propagatedBy(c),
      d_eagerSolver(),
      d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
      d_calledPreregister(false)
{
  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
  {
    d_eagerSolver.reset(new EagerBitblastSolver(c, this));
    return;
  }

  if (options().bv.bitvectorEqualitySolver)
  {
    d_subtheories.emplace_back(new CoreSolver(c, this));
    d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
  }

  if (options().bv.bitvectorInequalitySolver)
  {
    d_subtheories.emplace_back(new InequalitySolver(c, u, this));
    d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
  }

  if (options().bv.bitvectorAlgebraicSolver)
  {
    d_subtheories.emplace_back(new AlgebraicSolver(c, this));
    d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
  }

  BitblastSolver* bb_solver = new BitblastSolver(c, this);
  if (options().bv.bvAbstraction)
  {
    bb_solver->setAbstraction(d_abstractionModule.get());
  }
  d_subtheories.emplace_back(bb_solver);
  d_subtheoryMap[SUB_BITBLAST] = bb_solver;
}

BVSolverLayered::~BVSolverLayered() {}

bool BVSolverLayered::needsEqualityEngine(EeSetupInfo& esi)
{
  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
  if (core)
  {
    return core->needsEqualityEngine(esi);
  }
  // otherwise we don't use an equality engine
  return false;
}

void BVSolverLayered::finishInit()
{
  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
  if (core)
  {
    // must finish initialization in the core solver
    core->finishInit();
  }
}

void BVSolverLayered::spendResource(Resource r) { d_im.spendResource(r); }

BVSolverLayered::Statistics::Statistics()
    : d_avgConflictSize(smtStatisticsRegistry().registerAverage(
        "theory::bv::lazy::AvgBVConflictSize")),
      d_solveTimer(smtStatisticsRegistry().registerTimer(
          "theory::bv::lazy::solveTimer")),
      d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt(
          "theory::bv::lazy::NumFullCheckCalls")),
      d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt(
          "theory::bv::lazy::NumStandardCheckCalls")),
      d_weightComputationTimer(smtStatisticsRegistry().registerTimer(
          "theory::bv::lazy::weightComputationTimer")),
      d_numMultSlice(smtStatisticsRegistry().registerInt(
          "theory::bv::lazy::NumMultSliceApplied"))
{
}

void BVSolverLayered::preRegisterTerm(TNode node)
{
  d_calledPreregister = true;
  Debug("bitvector-preregister")
      << "BVSolverLayered::preRegister(" << node << ")" << std::endl;

  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
  {
    // the aig bit-blaster option is set heuristically
    // if bv abstraction is used
    if (!d_eagerSolver->isInitialized())
    {
      d_eagerSolver->initialize();
    }

    if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
    {
      Node formula = node[0];
      d_eagerSolver->assertFormula(formula);
    }
    return;
  }

  for (unsigned i = 0; i < d_subtheories.size(); ++i)
  {
    d_subtheories[i]->preRegister(node);
  }

  // AJR : equality solver currently registers all terms to ExtTheory, if we
  // want a lazy reduction without the bv equality solver, need to call this
  // d_bv.d_extTheory->registerTermRec( node );
}

void BVSolverLayered::sendConflict()
{
  Assert(d_conflict);
  if (d_conflictNode.isNull())
  {
    return;
  }
  else
  {
    Debug("bitvector") << indent() << "BVSolverLayered::check(): conflict "
                       << d_conflictNode << std::endl;
    d_im.conflict(d_conflictNode, InferenceId::BV_LAYERED_CONFLICT);
    d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren();
    d_conflictNode = Node::null();
  }
}

void BVSolverLayered::checkForLemma(TNode fact)
{
  if (fact.getKind() == kind::EQUAL)
  {
    NodeManager* nm = NodeManager::currentNM();
    if (fact[0].getKind() == kind::BITVECTOR_UREM)
    {
      TNode urem = fact[0];
      TNode result = fact[1];
      TNode divisor = urem[1];
      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
      Node divisor_eq_0 =
          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
      Node split = nm->mkNode(
          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
      lemma(split);
    }
    if (fact[1].getKind() == kind::BITVECTOR_UREM)
    {
      TNode urem = fact[1];
      TNode result = fact[0];
      TNode divisor = urem[1];
      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
      Node divisor_eq_0 =
          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
      Node split = nm->mkNode(
          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
      lemma(split);
    }
  }
}

bool BVSolverLayered::preCheck(Theory::Effort e)
{
  check(e);
  return true;
}

void BVSolverLayered::check(Theory::Effort e)
{
  if (done() && e < Theory::EFFORT_FULL)
  {
    return;
  }

  Debug("bitvector") << "BVSolverLayered::check(" << e << ")" << std::endl;
  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
  // we may be getting new assertions so the model cache may not be sound
  d_invalidateModelCache.set(true);
  // if we are using the eager solver
  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
  {
    // this can only happen on an empty benchmark
    if (!d_eagerSolver->isInitialized())
    {
      d_eagerSolver->initialize();
    }
    if (!Theory::fullEffort(e)) return;

    std::vector<TNode> assertions;
    while (!done())
    {
      TNode fact = get().d_assertion;
      Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
      assertions.push_back(fact);
      d_eagerSolver->assertFormula(fact[0]);
    }

    bool ok = d_eagerSolver->checkSat();
    if (!ok)
    {
      if (assertions.size() == 1)
      {
        d_im.conflict(assertions[0], InferenceId::BV_LAYERED_CONFLICT);
        return;
      }
      Node conflict = utils::mkAnd(assertions);
      d_im.conflict(conflict, InferenceId::BV_LAYERED_CONFLICT);
      return;
    }
    return;
  }

  if (Theory::fullEffort(e))
  {
    ++(d_statistics.d_numCallsToCheckFullEffort);
  }
  else
  {
    ++(d_statistics.d_numCallsToCheckStandardEffort);
  }
  // if we are already in conflict just return the conflict
  if (inConflict())
  {
    sendConflict();
    return;
  }

  while (!done())
  {
    TNode fact = get().d_assertion;

    checkForLemma(fact);

    for (unsigned i = 0; i < d_subtheories.size(); ++i)
    {
      d_subtheories[i]->assertFact(fact);
    }
  }

  bool ok = true;
  bool complete = false;
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
  {
    Assert(!inConflict());
    ok = d_subtheories[i]->check(e);
    complete = d_subtheories[i]->isComplete();

    if (!ok)
    {
      // if we are in a conflict no need to check with other theories
      Assert(inConflict());
      sendConflict();
      return;
    }
    if (complete)
    {
      // if the last subtheory was complete we stop
      break;
    }
  }
}

bool BVSolverLayered::collectModelValues(TheoryModel* m,
                                         const std::set<Node>& termSet)
{
  Assert(!inConflict());
  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
  {
    if (!d_eagerSolver->collectModelInfo(m, true))
    {
      return false;
    }
  }
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
  {
    if (d_subtheories[i]->isComplete())
    {
      return d_subtheories[i]->collectModelValues(m, termSet);
    }
  }
  return true;
}

Node BVSolverLayered::getModelValue(TNode var)
{
  Assert(!inConflict());
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
  {
    if (d_subtheories[i]->isComplete())
    {
      return d_subtheories[i]->getModelValue(var);
    }
  }
  Unreachable();
}

void BVSolverLayered::propagate(Theory::Effort e)
{
  Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl;
  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
  {
    return;
  }

  if (inConflict())
  {
    return;
  }

  // go through stored propagations
  bool ok = true;
  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok;
       d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
  {
    TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
    // temporary fix for incremental bit-blasting
    if (d_state.isSatLiteral(literal))
    {
      Debug("bitvector::propagate")
          << "BVSolverLayered:: propagating " << literal << "\n";
      ok = d_im.propagateLit(literal);
    }
  }

  if (!ok)
  {
    Debug("bitvector::propagate")
        << indent()
        << "BVSolverLayered::propagate(): conflict from theory engine"
        << std::endl;
    setConflict();
  }
}

TrustNode BVSolverLayered::ppRewrite(TNode t)
{
  Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n";
  Node res = t;
  if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t))
  {
    Node result = RewriteRule<BitwiseEq>::run<false>(t);
    res = rewrite(result);
  }
  else if (RewriteRule<UltAddOne>::applies(t))
  {
    Node result = RewriteRule<UltAddOne>::run<false>(t);
    res = rewrite(result);
  }
  else if (res.getKind() == kind::EQUAL
           && ((res[0].getKind() == kind::BITVECTOR_ADD
                && RewriteRule<ConcatToMult>::applies(res[1]))
               || (res[1].getKind() == kind::BITVECTOR_ADD
                   && RewriteRule<ConcatToMult>::applies(res[0]))))
  {
    Node mult = RewriteRule<ConcatToMult>::applies(res[0])
                    ? RewriteRule<ConcatToMult>::run<false>(res[0])
                    : RewriteRule<ConcatToMult>::run<true>(res[1]);
    Node factor = mult[0];
    Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
    Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
    Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
    if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
    {
      res = rewrite(rewr_eq);
    }
    else
    {
      res = t;
    }
  }
  else if (RewriteRule<SignExtendEqConst>::applies(t))
  {
    res = RewriteRule<SignExtendEqConst>::run<false>(t);
  }
  else if (RewriteRule<ZeroExtendEqConst>::applies(t))
  {
    res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
  }
  else if (RewriteRule<NormalizeEqAddNeg>::applies(t))
  {
    res = RewriteRule<NormalizeEqAddNeg>::run<false>(t);
  }

  // if(t.getKind() == kind::EQUAL &&
  //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
  //    kind::BITVECTOR_ADD) ||
  //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
  //     kind::BITVECTOR_ADD))) {
  //   // if we have an equality between a multiplication and addition
  //   // try to express multiplication in terms of addition
  //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
  //   Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1];
  //   if (RewriteRule<MultSlice>::applies(mult)) {
  //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
  //     Node new_eq =
  //     rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
  //     new_mult, add));

  //     // the simplification can cause the formula to blow up
  //     // only apply if formula reduced
  //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
  //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
  //       uint64_t old_size = bv->computeAtomWeight(t);
  //       Assert (old_size);
  //       uint64_t new_size = bv->computeAtomWeight(new_eq);
  //       double ratio = ((double)new_size)/old_size;
  //       if (ratio <= 0.4) {
  //         ++(d_statistics.d_numMultSlice);
  //         return new_eq;
  //       }
  //     }

  //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
  //       ++(d_statistics.d_numMultSlice);
  //       return new_eq;
  //     }
  //   }
  // }

  if (options().bv.bvAbstraction && t.getType().isBoolean())
  {
    d_abstractionModule->addInputAtom(res);
  }
  Debug("bv-pp-rewrite") << "to   " << res << "\n";
  if (res != t)
  {
    return TrustNode::mkTrustRewrite(t, res, nullptr);
  }
  return TrustNode::null();
}

void BVSolverLayered::presolve()
{
  Debug("bitvector") << "BVSolverLayered::presolve" << std::endl;
}

static int prop_count = 0;

bool BVSolverLayered::storePropagation(TNode literal, SubTheory subtheory)
{
  Debug("bitvector::propagate")
      << indent() << d_context->getLevel() << " "
      << "BVSolverLayered::storePropagation(" << literal << ", " << subtheory
      << ")" << std::endl;
  prop_count++;

  // If already in conflict, no more propagation
  if (d_conflict)
  {
    Debug("bitvector::propagate")
        << indent() << "BVSolverLayered::storePropagation(" << literal << ", "
        << subtheory << "): already in conflict" << std::endl;
    return false;
  }

  // If propagated already, just skip
  PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
  if (find != d_propagatedBy.end())
  {
    return true;
  }
  else
  {
    bool polarity = literal.getKind() != kind::NOT;
    Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0];
    find = d_propagatedBy.find(negatedLiteral);
    if (find != d_propagatedBy.end() && (*find).second != subtheory)
    {
      // Safe to ignore this one, subtheory should produce a conflict
      return true;
    }

    d_propagatedBy[literal] = subtheory;
  }

  // Propagate differs depending on the subtheory
  // * bitblaster needs to be left alone until it's done, otherwise it doesn't
  //   know how to explain
  // * equality engine can propagate eagerly
  // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
  constexpr bool ok = true;
  if (subtheory == SUB_CORE)
  {
    d_im.propagateLit(literal);
    if (!ok)
    {
      setConflict();
    }
  }
  else
  {
    d_literalsToPropagate.push_back(literal);
  }
  return ok;

} /* BVSolverLayered::propagate(TNode) */

void BVSolverLayered::explain(TNode literal, std::vector<TNode>& assumptions)
{
  Assert(wasPropagatedBySubtheory(literal));
  SubTheory sub = getPropagatingSubtheory(literal);
  d_subtheoryMap[sub]->explain(literal, assumptions);
}

TrustNode BVSolverLayered::explain(TNode node)
{
  Debug("bitvector::explain")
      << "BVSolverLayered::explain(" << node << ")" << std::endl;
  std::vector<TNode> assumptions;

  // Ask for the explanation
  explain(node, assumptions);
  // this means that it is something true at level 0
  Node explanation;
  if (assumptions.size() == 0)
  {
    explanation = utils::mkTrue();
  }
  else
  {
    // return the explanation
    explanation = utils::mkAnd(assumptions);
  }
  Debug("bitvector::explain") << "BVSolverLayered::explain(" << node << ") => "
                              << explanation << std::endl;
  Debug("bitvector::explain") << "BVSolverLayered::explain done. \n";
  return TrustNode::mkTrustPropExp(node, explanation, nullptr);
}

void BVSolverLayered::notifySharedTerm(TNode t)
{
  Debug("bitvector::sharing")
      << indent() << "BVSolverLayered::notifySharedTerm(" << t << ")"
      << std::endl;
  d_sharedTermsSet.insert(t);
}

EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b)
{
  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
    return EQUALITY_UNKNOWN;
  Assert(options().bv.bitblastMode == options::BitblastMode::LAZY);
  for (unsigned i = 0; i < d_subtheories.size(); ++i)
  {
    EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
    if (status != EQUALITY_UNKNOWN)
    {
      return status;
    }
  }
  return EQUALITY_UNKNOWN;
  ;
}

void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned)
{
  if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
  {
    return;
  }
  d_staticLearnCache.insert(in);

  if (in.getKind() == kind::EQUAL)
  {
    if ((in[0].getKind() == kind::BITVECTOR_ADD
         && in[1].getKind() == kind::BITVECTOR_SHL)
        || (in[1].getKind() == kind::BITVECTOR_ADD
            && in[0].getKind() == kind::BITVECTOR_SHL))
    {
      TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1];
      TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0];

      if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
          && p[1].getKind() == kind::BITVECTOR_SHL)
      {
        unsigned size = utils::getSize(s);
        Node one = utils::mkConst(size, 1u);
        if (s[0] == one && p[0][0] == one && p[1][0] == one)
        {
          Node zero = utils::mkConst(size, 0u);
          TNode b = p[0];
          TNode c = p[1];
          // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
          Node b_eq_0 = b.eqNode(zero);
          Node c_eq_0 = c.eqNode(zero);
          Node b_eq_c = b.eqNode(c);

          Node dis = NodeManager::currentNM()->mkNode(
              kind::OR, b_eq_0, c_eq_0, b_eq_c);
          Node imp = in.impNode(dis);
          learned << imp;
        }
      }
    }
  }
  else if (in.getKind() == kind::AND)
  {
    for (size_t i = 0, N = in.getNumChildren(); i < N; ++i)
    {
      ppStaticLearn(in[i], learned);
    }
  }
}

bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions,
                                       std::vector<Node>& new_assertions)
{
  bool changed =
      d_abstractionModule->applyAbstraction(assertions, new_assertions);
  if (changed && options().bv.bitblastMode == options::BitblastMode::EAGER
      && options().bv.bitvectorAig)
  {
    // disable AIG mode
    AlwaysAssert(!d_eagerSolver->isInitialized());
    d_eagerSolver->turnOffAig();
    d_eagerSolver->initialize();
  }
  return changed;
}

void BVSolverLayered::setConflict(Node conflict)
{
  if (options().bv.bvAbstraction)
  {
    NodeManager* const nm = NodeManager::currentNM();
    Node new_conflict = d_abstractionModule->simplifyConflict(conflict);

    std::vector<Node> lemmas;
    lemmas.push_back(new_conflict);
    d_abstractionModule->generalizeConflict(new_conflict, lemmas);
    for (unsigned i = 0; i < lemmas.size(); ++i)
    {
      lemma(nm->mkNode(kind::NOT, lemmas[i]));
    }
  }
  d_conflict = true;
  d_conflictNode = conflict;
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner, Liana Hadarean, Andrew Reynolds
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		* Layered bit-vector solver.
14		*/
15
16		#include "theory/bv/bv_solver_layered.h"
17
18		#include "expr/node_algorithm.h"
19		#include "options/bv_options.h"
20		#include "options/smt_options.h"
21		#include "smt/smt_statistics_registry.h"
22		#include "theory/bv/abstraction.h"
23		#include "theory/bv/bv_eager_solver.h"
24		#include "theory/bv/bv_subtheory_algebraic.h"
25		#include "theory/bv/bv_subtheory_bitblast.h"
26		#include "theory/bv/bv_subtheory_core.h"
27		#include "theory/bv/bv_subtheory_inequality.h"
28		#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
29		#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
30		#include "theory/bv/theory_bv_rewriter.h"
31		#include "theory/bv/theory_bv_utils.h"
32		#include "theory/theory_model.h"
33
34		using namespace cvc5::theory::bv::utils;
35
36		namespace cvc5 {
37		namespace theory {
38		namespace bv {
39
40	4	BVSolverLayered::BVSolverLayered(Env& env,
41		TheoryBV& bv,
42		context::Context* c,
43		context::UserContext* u,
44		ProofNodeManager* pnm,
45	4	std::string name)
46		: BVSolver(env, bv.d_state, bv.d_im),
47		d_bv(bv),
48		d_context(c),
49		d_alreadyPropagatedSet(c),
50		d_sharedTermsSet(c),
51		d_subtheories(),
52		d_subtheoryMap(),
53		d_statistics(),
54		d_staticLearnCache(),
55		d_lemmasAdded(c, false),
56		d_conflict(c, false),
57		d_invalidateModelCache(c, true),
58		d_literalsToPropagate(c),
59		d_literalsToPropagateIndex(c, 0),
60		d_propagatedBy(c),
61		d_eagerSolver(),
62	12	d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
63	16	d_calledPreregister(false)
64		{
65	4	if (options().bv.bitblastMode == options::BitblastMode::EAGER)
66		{
67	2	d_eagerSolver.reset(new EagerBitblastSolver(c, this));
68	2	return;
69		}
70
71	2	if (options().bv.bitvectorEqualitySolver)
72		{
73	2	d_subtheories.emplace_back(new CoreSolver(c, this));
74	2	d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
75		}
76
77	2	if (options().bv.bitvectorInequalitySolver)
78		{
79	2	d_subtheories.emplace_back(new InequalitySolver(c, u, this));
80	2	d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
81		}
82
83	2	if (options().bv.bitvectorAlgebraicSolver)
84		{
85		d_subtheories.emplace_back(new AlgebraicSolver(c, this));
86		d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
87		}
88
89	2	BitblastSolver* bb_solver = new BitblastSolver(c, this);
90	2	if (options().bv.bvAbstraction)
91		{
92		bb_solver->setAbstraction(d_abstractionModule.get());
93		}
94	2	d_subtheories.emplace_back(bb_solver);
95	2	d_subtheoryMap[SUB_BITBLAST] = bb_solver;
96		}
97
98	8	BVSolverLayered::~BVSolverLayered() {}
99
100	4	bool BVSolverLayered::needsEqualityEngine(EeSetupInfo& esi)
101		{
102	4	CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
103	4	if (core)
104		{
105	2	return core->needsEqualityEngine(esi);
106		}
107		// otherwise we don't use an equality engine
108	2	return false;
109		}
110
111	4	void BVSolverLayered::finishInit()
112		{
113	4	CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
114	4	if (core)
115		{
116		// must finish initialization in the core solver
117	2	core->finishInit();
118		}
119	4	}
120
121	12	void BVSolverLayered::spendResource(Resource r) { d_im.spendResource(r); }
122
123	4	BVSolverLayered::Statistics::Statistics()
124	4	: d_avgConflictSize(smtStatisticsRegistry().registerAverage(
125	8	"theory::bv::lazy::AvgBVConflictSize")),
126	4	d_solveTimer(smtStatisticsRegistry().registerTimer(
127	8	"theory::bv::lazy::solveTimer")),
128	4	d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt(
129	8	"theory::bv::lazy::NumFullCheckCalls")),
130	4	d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt(
131	8	"theory::bv::lazy::NumStandardCheckCalls")),
132	4	d_weightComputationTimer(smtStatisticsRegistry().registerTimer(
133	8	"theory::bv::lazy::weightComputationTimer")),
134	4	d_numMultSlice(smtStatisticsRegistry().registerInt(
135	24	"theory::bv::lazy::NumMultSliceApplied"))
136		{
137	4	}
138
139	28	void BVSolverLayered::preRegisterTerm(TNode node)
140		{
141	28	d_calledPreregister = true;
142	56	Debug("bitvector-preregister")
143	28	<< "BVSolverLayered::preRegister(" << node << ")" << std::endl;
144
145	28	if (options().bv.bitblastMode == options::BitblastMode::EAGER)
146		{
147		// the aig bit-blaster option is set heuristically
148		// if bv abstraction is used
149		if (!d_eagerSolver->isInitialized())
150		{
151		d_eagerSolver->initialize();
152		}
153
154		if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
155		{
156		Node formula = node[0];
157		d_eagerSolver->assertFormula(formula);
158		}
159		return;
160		}
161
162	112	for (unsigned i = 0; i < d_subtheories.size(); ++i)
163		{
164	84	d_subtheories[i]->preRegister(node);
165		}
166
167		// AJR : equality solver currently registers all terms to ExtTheory, if we
168		// want a lazy reduction without the bv equality solver, need to call this
169		// d_bv.d_extTheory->registerTermRec( node );
170		}
171
172		void BVSolverLayered::sendConflict()
173		{
174		Assert(d_conflict);
175		if (d_conflictNode.isNull())
176		{
177		return;
178		}
179		else
180		{
181		Debug("bitvector") << indent() << "BVSolverLayered::check(): conflict "
182		<< d_conflictNode << std::endl;
183		d_im.conflict(d_conflictNode, InferenceId::BV_LAYERED_CONFLICT);
184		d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren();
185		d_conflictNode = Node::null();
186		}
187		}
188
189		void BVSolverLayered::checkForLemma(TNode fact)
190		{
191		if (fact.getKind() == kind::EQUAL)
192		{
193		NodeManager* nm = NodeManager::currentNM();
194		if (fact[0].getKind() == kind::BITVECTOR_UREM)
195		{
196		TNode urem = fact[0];
197		TNode result = fact[1];
198		TNode divisor = urem[1];
199		Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
200		Node divisor_eq_0 =
201		nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
202		Node split = nm->mkNode(
203		kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
204		lemma(split);
205		}
206		if (fact[1].getKind() == kind::BITVECTOR_UREM)
207		{
208		TNode urem = fact[1];
209		TNode result = fact[0];
210		TNode divisor = urem[1];
211		Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
212		Node divisor_eq_0 =
213		nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
214		Node split = nm->mkNode(
215		kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
216		lemma(split);
217		}
218		}
219		}
220
221		bool BVSolverLayered::preCheck(Theory::Effort e)
222		{
223		check(e);
224		return true;
225		}
226
227		void BVSolverLayered::check(Theory::Effort e)
228		{
229		if (done() && e < Theory::EFFORT_FULL)
230		{
231		return;
232		}
233
234		Debug("bitvector") << "BVSolverLayered::check(" << e << ")" << std::endl;
235		TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
236		// we may be getting new assertions so the model cache may not be sound
237		d_invalidateModelCache.set(true);
238		// if we are using the eager solver
239		if (options().bv.bitblastMode == options::BitblastMode::EAGER)
240		{
241		// this can only happen on an empty benchmark
242		if (!d_eagerSolver->isInitialized())
243		{
244		d_eagerSolver->initialize();
245		}
246		if (!Theory::fullEffort(e)) return;
247
248		std::vector<TNode> assertions;
249		while (!done())
250		{
251		TNode fact = get().d_assertion;
252		Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
253		assertions.push_back(fact);
254		d_eagerSolver->assertFormula(fact[0]);
255		}
256
257		bool ok = d_eagerSolver->checkSat();
258		if (!ok)
259		{
260		if (assertions.size() == 1)
261		{
262		d_im.conflict(assertions[0], InferenceId::BV_LAYERED_CONFLICT);
263		return;
264		}
265		Node conflict = utils::mkAnd(assertions);
266		d_im.conflict(conflict, InferenceId::BV_LAYERED_CONFLICT);
267		return;
268		}
269		return;
270		}
271
272		if (Theory::fullEffort(e))
273		{
274		++(d_statistics.d_numCallsToCheckFullEffort);
275		}
276		else
277		{
278		++(d_statistics.d_numCallsToCheckStandardEffort);
279		}
280		// if we are already in conflict just return the conflict
281		if (inConflict())
282		{
283		sendConflict();
284		return;
285		}
286
287		while (!done())
288		{
289		TNode fact = get().d_assertion;
290
291		checkForLemma(fact);
292
293		for (unsigned i = 0; i < d_subtheories.size(); ++i)
294		{
295		d_subtheories[i]->assertFact(fact);
296		}
297		}
298
299		bool ok = true;
300		bool complete = false;
301		for (unsigned i = 0; i < d_subtheories.size(); ++i)
302		{
303		Assert(!inConflict());
304		ok = d_subtheories[i]->check(e);
305		complete = d_subtheories[i]->isComplete();
306
307		if (!ok)
308		{
309		// if we are in a conflict no need to check with other theories
310		Assert(inConflict());
311		sendConflict();
312		return;
313		}
314		if (complete)
315		{
316		// if the last subtheory was complete we stop
317		break;
318		}
319		}
320		}
321
322		bool BVSolverLayered::collectModelValues(TheoryModel* m,
323		const std::set<Node>& termSet)
324		{
325		Assert(!inConflict());
326		if (options().bv.bitblastMode == options::BitblastMode::EAGER)
327		{
328		if (!d_eagerSolver->collectModelInfo(m, true))
329		{
330		return false;
331		}
332		}
333		for (unsigned i = 0; i < d_subtheories.size(); ++i)
334		{
335		if (d_subtheories[i]->isComplete())
336		{
337		return d_subtheories[i]->collectModelValues(m, termSet);
338		}
339		}
340		return true;
341		}
342
343		Node BVSolverLayered::getModelValue(TNode var)
344		{
345		Assert(!inConflict());
346		for (unsigned i = 0; i < d_subtheories.size(); ++i)
347		{
348		if (d_subtheories[i]->isComplete())
349		{
350		return d_subtheories[i]->getModelValue(var);
351		}
352		}
353		Unreachable();
354		}
355
356		void BVSolverLayered::propagate(Theory::Effort e)
357		{
358		Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl;
359		if (options().bv.bitblastMode == options::BitblastMode::EAGER)
360		{
361		return;
362		}
363
364		if (inConflict())
365		{
366		return;
367		}
368
369		// go through stored propagations
370		bool ok = true;
371		for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok;
372		d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
373		{
374		TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
375		// temporary fix for incremental bit-blasting
376		if (d_state.isSatLiteral(literal))
377		{
378		Debug("bitvector::propagate")
379		<< "BVSolverLayered:: propagating " << literal << "\n";
380		ok = d_im.propagateLit(literal);
381		}
382		}
383
384		if (!ok)
385		{
386		Debug("bitvector::propagate")
387		<< indent()
388		<< "BVSolverLayered::propagate(): conflict from theory engine"
389		<< std::endl;
390		setConflict();
391		}
392		}
393
394	46	TrustNode BVSolverLayered::ppRewrite(TNode t)
395		{
396	46	Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n";
397	92	Node res = t;
398	46	if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t))
399		{
400		Node result = RewriteRule<BitwiseEq>::run<false>(t);
401		res = rewrite(result);
402		}
403	46	else if (RewriteRule<UltAddOne>::applies(t))
404		{
405		Node result = RewriteRule<UltAddOne>::run<false>(t);
406		res = rewrite(result);
407		}
408	92	else if (res.getKind() == kind::EQUAL
409	138	&& ((res[0].getKind() == kind::BITVECTOR_ADD
410	54	&& RewriteRule<ConcatToMult>::applies(res[1]))
411	66	\|\| (res[1].getKind() == kind::BITVECTOR_ADD
412	46	&& RewriteRule<ConcatToMult>::applies(res[0]))))
413		{
414		Node mult = RewriteRule<ConcatToMult>::applies(res[0])
415		? RewriteRule<ConcatToMult>::run<false>(res[0])
416		: RewriteRule<ConcatToMult>::run<true>(res[1]);
417		Node factor = mult[0];
418		Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
419		Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
420		Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
421		if (rewr_eq[0].isVar() \|\| rewr_eq[1].isVar())
422		{
423		res = rewrite(rewr_eq);
424		}
425		else
426		{
427		res = t;
428		}
429		}
430	46	else if (RewriteRule<SignExtendEqConst>::applies(t))
431		{
432		res = RewriteRule<SignExtendEqConst>::run<false>(t);
433		}
434	46	else if (RewriteRule<ZeroExtendEqConst>::applies(t))
435		{
436		res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
437		}
438	46	else if (RewriteRule<NormalizeEqAddNeg>::applies(t))
439		{
440	8	res = RewriteRule<NormalizeEqAddNeg>::run<false>(t);
441		}
442
443		// if(t.getKind() == kind::EQUAL &&
444		// ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
445		// kind::BITVECTOR_ADD) \|\|
446		// (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
447		// kind::BITVECTOR_ADD))) {
448		// // if we have an equality between a multiplication and addition
449		// // try to express multiplication in terms of addition
450		// Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
451		// Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1];
452		// if (RewriteRule<MultSlice>::applies(mult)) {
453		// Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
454		// Node new_eq =
455		// rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
456		// new_mult, add));
457
458		// // the simplification can cause the formula to blow up
459		// // only apply if formula reduced
460		// if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
461		// BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
462		// uint64_t old_size = bv->computeAtomWeight(t);
463		// Assert (old_size);
464		// uint64_t new_size = bv->computeAtomWeight(new_eq);
465		// double ratio = ((double)new_size)/old_size;
466		// if (ratio <= 0.4) {
467		// ++(d_statistics.d_numMultSlice);
468		// return new_eq;
469		// }
470		// }
471
472		// if (new_eq.getKind() == kind::CONST_BOOLEAN) {
473		// ++(d_statistics.d_numMultSlice);
474		// return new_eq;
475		// }
476		// }
477		// }
478
479	46	if (options().bv.bvAbstraction && t.getType().isBoolean())
480		{
481		d_abstractionModule->addInputAtom(res);
482		}
483	46	Debug("bv-pp-rewrite") << "to " << res << "\n";
484	46	if (res != t)
485		{
486		return TrustNode::mkTrustRewrite(t, res, nullptr);
487		}
488	46	return TrustNode::null();
489		}
490
491	2	void BVSolverLayered::presolve()
492		{
493	2	Debug("bitvector") << "BVSolverLayered::presolve" << std::endl;
494	2	}
495
496		static int prop_count = 0;
497
498		bool BVSolverLayered::storePropagation(TNode literal, SubTheory subtheory)
499		{
500		Debug("bitvector::propagate")
501		<< indent() << d_context->getLevel() << " "
502		<< "BVSolverLayered::storePropagation(" << literal << ", " << subtheory
503		<< ")" << std::endl;
504		prop_count++;
505
506		// If already in conflict, no more propagation
507		if (d_conflict)
508		{
509		Debug("bitvector::propagate")
510		<< indent() << "BVSolverLayered::storePropagation(" << literal << ", "
511		<< subtheory << "): already in conflict" << std::endl;
512		return false;
513		}
514
515		// If propagated already, just skip
516		PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
517		if (find != d_propagatedBy.end())
518		{
519		return true;
520		}
521		else
522		{
523		bool polarity = literal.getKind() != kind::NOT;
524		Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0];
525		find = d_propagatedBy.find(negatedLiteral);
526		if (find != d_propagatedBy.end() && (*find).second != subtheory)
527		{
528		// Safe to ignore this one, subtheory should produce a conflict
529		return true;
530		}
531
532		d_propagatedBy[literal] = subtheory;
533		}
534
535		// Propagate differs depending on the subtheory
536		// * bitblaster needs to be left alone until it's done, otherwise it doesn't
537		// know how to explain
538		// * equality engine can propagate eagerly
539		// TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
540		constexpr bool ok = true;
541		if (subtheory == SUB_CORE)
542		{
543		d_im.propagateLit(literal);
544		if (!ok)
545		{
546		setConflict();
547		}
548		}
549		else
550		{
551		d_literalsToPropagate.push_back(literal);
552		}
553		return ok;
554
555		} /* BVSolverLayered::propagate(TNode) */
556
557		void BVSolverLayered::explain(TNode literal, std::vector<TNode>& assumptions)
558		{
559		Assert(wasPropagatedBySubtheory(literal));
560		SubTheory sub = getPropagatingSubtheory(literal);
561		d_subtheoryMap[sub]->explain(literal, assumptions);
562		}
563
564		TrustNode BVSolverLayered::explain(TNode node)
565		{
566		Debug("bitvector::explain")
567		<< "BVSolverLayered::explain(" << node << ")" << std::endl;
568		std::vector<TNode> assumptions;
569
570		// Ask for the explanation
571		explain(node, assumptions);
572		// this means that it is something true at level 0
573		Node explanation;
574		if (assumptions.size() == 0)
575		{
576		explanation = utils::mkTrue();
577		}
578		else
579		{
580		// return the explanation
581		explanation = utils::mkAnd(assumptions);
582		}
583		Debug("bitvector::explain") << "BVSolverLayered::explain(" << node << ") => "
584		<< explanation << std::endl;
585		Debug("bitvector::explain") << "BVSolverLayered::explain done. \n";
586		return TrustNode::mkTrustPropExp(node, explanation, nullptr);
587		}
588
589		void BVSolverLayered::notifySharedTerm(TNode t)
590		{
591		Debug("bitvector::sharing")
592		<< indent() << "BVSolverLayered::notifySharedTerm(" << t << ")"
593		<< std::endl;
594		d_sharedTermsSet.insert(t);
595		}
596
597		EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b)
598		{
599		if (options().bv.bitblastMode == options::BitblastMode::EAGER)
600		return EQUALITY_UNKNOWN;
601		Assert(options().bv.bitblastMode == options::BitblastMode::LAZY);
602		for (unsigned i = 0; i < d_subtheories.size(); ++i)
603		{
604		EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
605		if (status != EQUALITY_UNKNOWN)
606		{
607		return status;
608		}
609		}
610		return EQUALITY_UNKNOWN;
611		;
612		}
613
614	20	void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned)
615		{
616	20	if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
617		{
618	4	return;
619		}
620	16	d_staticLearnCache.insert(in);
621
622	16	if (in.getKind() == kind::EQUAL)
623		{
624	6	if ((in[0].getKind() == kind::BITVECTOR_ADD
625	4	&& in[1].getKind() == kind::BITVECTOR_SHL)
626	10	\|\| (in[1].getKind() == kind::BITVECTOR_ADD
627	2	&& in[0].getKind() == kind::BITVECTOR_SHL))
628		{
629	4	TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1];
630	4	TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0];
631
632	6	if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
633	6	&& p[1].getKind() == kind::BITVECTOR_SHL)
634		{
635	2	unsigned size = utils::getSize(s);
636	4	Node one = utils::mkConst(size, 1u);
637	2	if (s[0] == one && p[0][0] == one && p[1][0] == one)
638		{
639	4	Node zero = utils::mkConst(size, 0u);
640	4	TNode b = p[0];
641	4	TNode c = p[1];
642		// (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
643	4	Node b_eq_0 = b.eqNode(zero);
644	4	Node c_eq_0 = c.eqNode(zero);
645	4	Node b_eq_c = b.eqNode(c);
646
647		Node dis = NodeManager::currentNM()->mkNode(
648	4	kind::OR, b_eq_0, c_eq_0, b_eq_c);
649	4	Node imp = in.impNode(dis);
650	2	learned << imp;
651		}
652		}
653		}
654		}
655	14	else if (in.getKind() == kind::AND)
656		{
657	12	for (size_t i = 0, N = in.getNumChildren(); i < N; ++i)
658		{
659	8	ppStaticLearn(in[i], learned);
660		}
661		}
662		}
663
664		bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions,
665		std::vector<Node>& new_assertions)
666		{
667		bool changed =
668		d_abstractionModule->applyAbstraction(assertions, new_assertions);
669		if (changed && options().bv.bitblastMode == options::BitblastMode::EAGER
670		&& options().bv.bitvectorAig)
671		{
672		// disable AIG mode
673		AlwaysAssert(!d_eagerSolver->isInitialized());
674		d_eagerSolver->turnOffAig();
675		d_eagerSolver->initialize();
676		}
677		return changed;
678		}
679
680		void BVSolverLayered::setConflict(Node conflict)
681		{
682		if (options().bv.bvAbstraction)
683		{
684		NodeManager* const nm = NodeManager::currentNM();
685		Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
686
687		std::vector<Node> lemmas;
688		lemmas.push_back(new_conflict);
689		d_abstractionModule->generalizeConflict(new_conflict, lemmas);
690		for (unsigned i = 0; i < lemmas.size(); ++i)
691		{
692		lemma(nm->mkNode(kind::NOT, lemmas[i]));
693		}
694		}
695		d_conflict = true;
696		d_conflictNode = conflict;
697		}
698
699		} // namespace bv
700		} // namespace theory
701	29577	} // namespace cvc5