Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv.cpp	Lines:	207	213	97.2 %
Date:	2021-11-07	Branches:	418	874	47.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Andrew Reynolds, Haniel Barbosa
 *
 * 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.
 * ****************************************************************************
 *
 * Theory of bit-vectors.
 */

#include "theory/bv/theory_bv.h"

#include "options/bv_options.h"
#include "options/smt_options.h"
#include "proof/proof_checker.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/bv_solver_bitblast.h"
#include "theory/bv/bv_solver_bitblast_internal.h"
#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/ee_setup_info.h"
#include "theory/trust_substitutions.h"
#include "theory/uf/equality_engine.h"

namespace cvc5 {
namespace theory {
namespace bv {

TheoryBV::TheoryBV(Env& env,
                   OutputChannel& out,
                   Valuation valuation,
                   std::string name)
    : Theory(THEORY_BV, env, out, valuation, name),
      d_internal(nullptr),
      d_rewriter(),
      d_state(env, valuation),
      d_im(env, *this, d_state, "theory::bv::"),
      d_notify(d_im),
      d_invalidateModelCache(context(), true),
      d_stats(statisticsRegistry(), "theory::bv::")
{
  switch (options().bv.bvSolver)
  {
    case options::BVSolver::BITBLAST:
      d_internal.reset(new BVSolverBitblast(env, &d_state, d_im, d_pnm));
      break;

    default:
      AlwaysAssert(options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL);
      d_internal.reset(
          new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm));
  }
  d_theoryState = &d_state;
  d_inferManager = &d_im;
}

TheoryBV::~TheoryBV() {}

TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }

ProofRuleChecker* TheoryBV::getProofChecker()
{
  if (options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL)
  {
    return static_cast<BVSolverBitblastInternal*>(d_internal.get())
        ->getProofChecker();
  }
  return nullptr;
}

bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
{
  bool need_ee = d_internal->needsEqualityEngine(esi);

  /* Set up default notify class for equality engine. */
  if (need_ee && esi.d_notify == nullptr)
  {
    esi.d_notify = &d_notify;
    esi.d_name = "theory::bv::ee";
  }

  return need_ee;
}

void TheoryBV::finishInit()
{
  // these kinds are semi-evaluated in getModelValue (applications of this
  // kind are treated as variables)
  getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
  getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
  d_internal->finishInit();

  eq::EqualityEngine* ee = getEqualityEngine();
  if (ee)
  {
    // The kinds we are treating as function application in congruence
    ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
    //    ee->addFunctionKind(kind::BITVECTOR_AND);
    //    ee->addFunctionKind(kind::BITVECTOR_OR);
    //    ee->addFunctionKind(kind::BITVECTOR_XOR);
    //    ee->addFunctionKind(kind::BITVECTOR_NOT);
    //    ee->addFunctionKind(kind::BITVECTOR_NAND);
    //    ee->addFunctionKind(kind::BITVECTOR_NOR);
    //    ee->addFunctionKind(kind::BITVECTOR_XNOR);
    //    ee->addFunctionKind(kind::BITVECTOR_COMP);
    ee->addFunctionKind(kind::BITVECTOR_MULT, true);
    ee->addFunctionKind(kind::BITVECTOR_ADD, true);
    ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
    //    ee->addFunctionKind(kind::BITVECTOR_SUB);
    //    ee->addFunctionKind(kind::BITVECTOR_NEG);
    //    ee->addFunctionKind(kind::BITVECTOR_UDIV);
    //    ee->addFunctionKind(kind::BITVECTOR_UREM);
    //    ee->addFunctionKind(kind::BITVECTOR_SDIV);
    //    ee->addFunctionKind(kind::BITVECTOR_SREM);
    //    ee->addFunctionKind(kind::BITVECTOR_SMOD);
    //    ee->addFunctionKind(kind::BITVECTOR_SHL);
    //    ee->addFunctionKind(kind::BITVECTOR_LSHR);
    //    ee->addFunctionKind(kind::BITVECTOR_ASHR);
    //    ee->addFunctionKind(kind::BITVECTOR_ULT);
    //    ee->addFunctionKind(kind::BITVECTOR_ULE);
    //    ee->addFunctionKind(kind::BITVECTOR_UGT);
    //    ee->addFunctionKind(kind::BITVECTOR_UGE);
    //    ee->addFunctionKind(kind::BITVECTOR_SLT);
    //    ee->addFunctionKind(kind::BITVECTOR_SLE);
    //    ee->addFunctionKind(kind::BITVECTOR_SGT);
    //    ee->addFunctionKind(kind::BITVECTOR_SGE);
    ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
    ee->addFunctionKind(kind::INT_TO_BITVECTOR);
  }
}

void TheoryBV::preRegisterTerm(TNode node)
{
  d_internal->preRegisterTerm(node);

  eq::EqualityEngine* ee = getEqualityEngine();
  if (ee)
  {
    if (node.getKind() == kind::EQUAL)
    {
      ee->addTriggerPredicate(node);
    }
    else
    {
      ee->addTerm(node);
    }
  }
}

bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }

void TheoryBV::postCheck(Effort e)
{
  d_invalidateModelCache = true;
  d_internal->postCheck(e);
}

bool TheoryBV::preNotifyFact(
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
{
  return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
}

void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
{
  d_internal->notifyFact(atom, pol, fact, isInternal);
}

bool TheoryBV::needsCheckLastEffort()
{
  return d_internal->needsCheckLastEffort();
}

void TheoryBV::computeRelevantTerms(std::set<Node>& termSet)
{
  return d_internal->computeRelevantTerms(termSet);
}

bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
{
  return d_internal->collectModelValues(m, termSet);
}

void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }

Theory::PPAssertStatus TheoryBV::ppAssert(
    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
{
  TNode in = tin.getNode();
  Kind k = in.getKind();
  if (k == kind::EQUAL)
  {
    // Substitute variables
    if (in[0].isVar() && isLegalElimination(in[0], in[1]))
    {
      ++d_stats.d_solveSubstitutions;
      outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
      return Theory::PP_ASSERT_STATUS_SOLVED;
    }
    if (in[1].isVar() && isLegalElimination(in[1], in[0]))
    {
      ++d_stats.d_solveSubstitutions;
      outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
      return Theory::PP_ASSERT_STATUS_SOLVED;
    }
    /**
     * Eliminate extract over bit-vector variables.
     *
     * Given x[h:l] = c, where c is a constant and x is a variable.
     *
     * We rewrite to:
     *
     * x = sk1::c       if l == 0, where bw(sk1) = bw(x)-1-h
     * x = c::sk2       if h == bw(x)-1, where bw(sk2) = l
     * x = sk1::c::sk2  otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
     */
    Node node = rewrite(in);
    if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
        || (node[1].getKind() == kind::BITVECTOR_EXTRACT
            && node[0].isConst()))
    {
      Node extract = node[0].isConst() ? node[1] : node[0];
      if (extract[0].isVar())
      {
        Node c = node[0].isConst() ? node[0] : node[1];

        uint32_t high = utils::getExtractHigh(extract);
        uint32_t low = utils::getExtractLow(extract);
        uint32_t var_bw = utils::getSize(extract[0]);
        std::vector<Node> children;

        // create sk1 with size bw(x)-1-h
        if (low == 0 || high != var_bw - 1)
        {
          Assert(high != var_bw - 1);
          uint32_t skolem_size = var_bw - high - 1;
          Node skolem = utils::mkVar(skolem_size);
          children.push_back(skolem);
        }

        children.push_back(c);

        // create sk2 with size l
        if (high == var_bw - 1 || low != 0)
        {
          Assert(low != 0);
          uint32_t skolem_size = low;
          Node skolem = utils::mkVar(skolem_size);
          children.push_back(skolem);
        }

        Node concat = utils::mkConcat(children);
        Assert(utils::getSize(concat) == utils::getSize(extract[0]));
        if (isLegalElimination(extract[0], concat))
        {
          outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
          return Theory::PP_ASSERT_STATUS_SOLVED;
        }
      }
    }
  }
  return Theory::PP_ASSERT_STATUS_UNSOLVED;
}

TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
{
  // first, see if we need to expand definitions
  TrustNode texp = d_rewriter.expandDefinition(t);
  if (!texp.isNull())
  {
    return texp;
  }

  Debug("theory-bv-pp-rewrite") << "ppRewrite " << t << "\n";
  Node res = t;
  if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t))
  {
    res = rewrite(RewriteRule<BitwiseEq>::run<false>(t));
  }
  // useful on QF_BV/space/ndist
  else if (RewriteRule<UltAddOne>::applies(t))
  {
    res = rewrite(RewriteRule<UltAddOne>::run<false>(t));
  }
  // Useful for BV/2017-Preiner-scholl-smt08, but not for QF_BV
  else if (options().bv.rwExtendEq)
  {
    if (RewriteRule<SignExtendEqConst>::applies(t))
    {
      res = RewriteRule<SignExtendEqConst>::run<false>(t);
    }
    else if (RewriteRule<ZeroExtendEqConst>::applies(t))
    {
      res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
    }
  }

  Debug("theory-bv-pp-rewrite") << "to   " << res << "\n";
  if (res != t)
  {
    return TrustNode::mkTrustRewrite(t, res, nullptr);
  }

  return d_internal->ppRewrite(t);
}

void TheoryBV::presolve() { d_internal->presolve(); }

EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
{
  EqualityStatus status = d_internal->getEqualityStatus(a, b);

  if (status == EqualityStatus::EQUALITY_UNKNOWN)
  {
    Node value_a = getValue(a);
    Node value_b = getValue(b);

    if (value_a.isNull() || value_b.isNull())
    {
      return status;
    }

    if (value_a == value_b)
    {
      Debug("theory-bv") << EQUALITY_TRUE_IN_MODEL << std::endl;
      return EQUALITY_TRUE_IN_MODEL;
    }
    Debug("theory-bv") << EQUALITY_FALSE_IN_MODEL << std::endl;
    return EQUALITY_FALSE_IN_MODEL;
  }
  return status;
}

TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }

void TheoryBV::notifySharedTerm(TNode t)
{
  d_internal->notifySharedTerm(t);
}

void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
{
  if (in.getKind() == kind::EQUAL)
  {
    // Only useful in combination with --bv-intro-pow2 on
    // QF_BV/pspace/power2sum benchmarks.
    //
    // Matches for equality:
    //
    // (= (bvadd (bvshl 1 x) (bvshl 1 y)) (bvshl 1 z))
    //
    // and does case analysis on the sum of two power of twos.
    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)
      {
        if (utils::isOne(s[0]) && utils::isOne(p[0][0])
            && utils::isOne(p[1][0]))
        {
          Node zero = utils::mkZero(utils::getSize(s));
          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;
        }
      }
    }
  }

  d_internal->ppStaticLearn(in, learned);
}

Node TheoryBV::getValue(TNode node)
{
  if (d_invalidateModelCache.get())
  {
    d_modelCache.clear();
  }
  d_invalidateModelCache.set(false);

  std::vector<TNode> visit;

  TNode cur;
  visit.push_back(node);
  do
  {
    cur = visit.back();
    visit.pop_back();

    auto it = d_modelCache.find(cur);
    if (it != d_modelCache.end() && !it->second.isNull())
    {
      continue;
    }

    if (cur.isConst())
    {
      d_modelCache[cur] = cur;
      continue;
    }

    Node value = d_internal->getValue(cur, false);
    if (value.isConst())
    {
      d_modelCache[cur] = value;
      continue;
    }

    if (Theory::isLeafOf(cur, theory::THEORY_BV))
    {
      value = d_internal->getValue(cur, true);
      d_modelCache[cur] = value;
      continue;
    }

    if (it == d_modelCache.end())
    {
      visit.push_back(cur);
      d_modelCache.emplace(cur, Node());
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
    else if (it->second.isNull())
    {
      NodeBuilder nb(cur.getKind());
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        nb << cur.getOperator();
      }

      std::unordered_map<Node, Node>::iterator iit;
      for (const TNode& child : cur)
      {
        iit = d_modelCache.find(child);
        Assert(iit != d_modelCache.end());
        Assert(iit->second.isConst());
        nb << iit->second;
      }
      it->second = rewrite(nb.constructNode());
    }
  } while (!visit.empty());

  auto it = d_modelCache.find(node);
  Assert(it != d_modelCache.end());
  return it->second;
}

TheoryBV::Statistics::Statistics(StatisticsRegistry& reg,
                                 const std::string& name)
    : d_solveSubstitutions(reg.registerInt(name + "NumSolveSubstitutions"))
{
}

}  // 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, Andrew Reynolds, Haniel Barbosa
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		* Theory of bit-vectors.
14		*/
15
16		#include "theory/bv/theory_bv.h"
17
18		#include "options/bv_options.h"
19		#include "options/smt_options.h"
20		#include "proof/proof_checker.h"
21		#include "smt/smt_statistics_registry.h"
22		#include "theory/bv/bv_solver_bitblast.h"
23		#include "theory/bv/bv_solver_bitblast_internal.h"
24		#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
25		#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
26		#include "theory/bv/theory_bv_utils.h"
27		#include "theory/ee_setup_info.h"
28		#include "theory/trust_substitutions.h"
29		#include "theory/uf/equality_engine.h"
30
31		namespace cvc5 {
32		namespace theory {
33		namespace bv {
34
35	15273	TheoryBV::TheoryBV(Env& env,
36		OutputChannel& out,
37		Valuation valuation,
38	15273	std::string name)
39		: Theory(THEORY_BV, env, out, valuation, name),
40		d_internal(nullptr),
41		d_rewriter(),
42		d_state(env, valuation),
43		d_im(env, *this, d_state, "theory::bv::"),
44		d_notify(d_im),
45		d_invalidateModelCache(context(), true),
46	15273	d_stats(statisticsRegistry(), "theory::bv::")
47		{
48	15273	switch (options().bv.bvSolver)
49		{
50	7289	case options::BVSolver::BITBLAST:
51	7289	d_internal.reset(new BVSolverBitblast(env, &d_state, d_im, d_pnm));
52	7289	break;
53
54	7984	default:
55	7984	AlwaysAssert(options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL);
56	15968	d_internal.reset(
57	7984	new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm));
58		}
59	15273	d_theoryState = &d_state;
60	15273	d_inferManager = &d_im;
61	15273	}
62
63	30536	TheoryBV::~TheoryBV() {}
64
65	15273	TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
66
67	7989	ProofRuleChecker* TheoryBV::getProofChecker()
68		{
69	7989	if (options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL)
70		{
71	7970	return static_cast<BVSolverBitblastInternal*>(d_internal.get())
72	7970	->getProofChecker();
73		}
74	19	return nullptr;
75		}
76
77	15273	bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
78		{
79	15273	bool need_ee = d_internal->needsEqualityEngine(esi);
80
81		/* Set up default notify class for equality engine. */
82	15273	if (need_ee && esi.d_notify == nullptr)
83		{
84	15248	esi.d_notify = &d_notify;
85	15248	esi.d_name = "theory::bv::ee";
86		}
87
88	15273	return need_ee;
89		}
90
91	15273	void TheoryBV::finishInit()
92		{
93		// these kinds are semi-evaluated in getModelValue (applications of this
94		// kind are treated as variables)
95	15273	getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
96	15273	getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
97	15273	d_internal->finishInit();
98
99	15273	eq::EqualityEngine* ee = getEqualityEngine();
100	15273	if (ee)
101		{
102		// The kinds we are treating as function application in congruence
103	15248	ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
104		// ee->addFunctionKind(kind::BITVECTOR_AND);
105		// ee->addFunctionKind(kind::BITVECTOR_OR);
106		// ee->addFunctionKind(kind::BITVECTOR_XOR);
107		// ee->addFunctionKind(kind::BITVECTOR_NOT);
108		// ee->addFunctionKind(kind::BITVECTOR_NAND);
109		// ee->addFunctionKind(kind::BITVECTOR_NOR);
110		// ee->addFunctionKind(kind::BITVECTOR_XNOR);
111		// ee->addFunctionKind(kind::BITVECTOR_COMP);
112	15248	ee->addFunctionKind(kind::BITVECTOR_MULT, true);
113	15248	ee->addFunctionKind(kind::BITVECTOR_ADD, true);
114	15248	ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
115		// ee->addFunctionKind(kind::BITVECTOR_SUB);
116		// ee->addFunctionKind(kind::BITVECTOR_NEG);
117		// ee->addFunctionKind(kind::BITVECTOR_UDIV);
118		// ee->addFunctionKind(kind::BITVECTOR_UREM);
119		// ee->addFunctionKind(kind::BITVECTOR_SDIV);
120		// ee->addFunctionKind(kind::BITVECTOR_SREM);
121		// ee->addFunctionKind(kind::BITVECTOR_SMOD);
122		// ee->addFunctionKind(kind::BITVECTOR_SHL);
123		// ee->addFunctionKind(kind::BITVECTOR_LSHR);
124		// ee->addFunctionKind(kind::BITVECTOR_ASHR);
125		// ee->addFunctionKind(kind::BITVECTOR_ULT);
126		// ee->addFunctionKind(kind::BITVECTOR_ULE);
127		// ee->addFunctionKind(kind::BITVECTOR_UGT);
128		// ee->addFunctionKind(kind::BITVECTOR_UGE);
129		// ee->addFunctionKind(kind::BITVECTOR_SLT);
130		// ee->addFunctionKind(kind::BITVECTOR_SLE);
131		// ee->addFunctionKind(kind::BITVECTOR_SGT);
132		// ee->addFunctionKind(kind::BITVECTOR_SGE);
133	15248	ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
134	15248	ee->addFunctionKind(kind::INT_TO_BITVECTOR);
135		}
136	15273	}
137
138	341869	void TheoryBV::preRegisterTerm(TNode node)
139		{
140	341869	d_internal->preRegisterTerm(node);
141
142	341869	eq::EqualityEngine* ee = getEqualityEngine();
143	341869	if (ee)
144		{
145	336919	if (node.getKind() == kind::EQUAL)
146		{
147	52426	ee->addTriggerPredicate(node);
148		}
149		else
150		{
151	284493	ee->addTerm(node);
152		}
153		}
154	341869	}
155
156	1002516	bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
157
158	1002516	void TheoryBV::postCheck(Effort e)
159		{
160	1002516	d_invalidateModelCache = true;
161	1002516	d_internal->postCheck(e);
162	1002516	}
163
164	2836060	bool TheoryBV::preNotifyFact(
165		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
166		{
167	2836060	return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
168		}
169
170	2833722	void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
171		{
172	2833722	d_internal->notifyFact(atom, pol, fact, isInternal);
173	2833722	}
174
175	11996	bool TheoryBV::needsCheckLastEffort()
176		{
177	11996	return d_internal->needsCheckLastEffort();
178		}
179
180	10631	void TheoryBV::computeRelevantTerms(std::set<Node>& termSet)
181		{
182	10631	return d_internal->computeRelevantTerms(termSet);
183		}
184
185	10631	bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
186		{
187	10631	return d_internal->collectModelValues(m, termSet);
188		}
189
190	1993172	void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
191
192	4622	Theory::PPAssertStatus TheoryBV::ppAssert(
193		TrustNode tin, TrustSubstitutionMap& outSubstitutions)
194		{
195	9244	TNode in = tin.getNode();
196	4622	Kind k = in.getKind();
197	4622	if (k == kind::EQUAL)
198		{
199		// Substitute variables
200	1306	if (in[0].isVar() && isLegalElimination(in[0], in[1]))
201		{
202	282	++d_stats.d_solveSubstitutions;
203	282	outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
204	1123	return Theory::PP_ASSERT_STATUS_SOLVED;
205		}
206	1024	if (in[1].isVar() && isLegalElimination(in[1], in[0]))
207		{
208	531	++d_stats.d_solveSubstitutions;
209	531	outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
210	531	return Theory::PP_ASSERT_STATUS_SOLVED;
211		}
212		/**
213		* Eliminate extract over bit-vector variables.
214		*
215		* Given x[h:l] = c, where c is a constant and x is a variable.
216		*
217		* We rewrite to:
218		*
219		* x = sk1::c if l == 0, where bw(sk1) = bw(x)-1-h
220		* x = c::sk2 if h == bw(x)-1, where bw(sk2) = l
221		* x = sk1::c::sk2 otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
222		*/
223	958	Node node = rewrite(in);
224	1538	if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
225	2487	\|\| (node[1].getKind() == kind::BITVECTOR_EXTRACT
226	560	&& node[0].isConst()))
227		{
228	68	Node extract = node[0].isConst() ? node[1] : node[0];
229	48	if (extract[0].isVar())
230		{
231	28	Node c = node[0].isConst() ? node[0] : node[1];
232
233	28	uint32_t high = utils::getExtractHigh(extract);
234	28	uint32_t low = utils::getExtractLow(extract);
235	28	uint32_t var_bw = utils::getSize(extract[0]);
236	28	std::vector<Node> children;
237
238		// create sk1 with size bw(x)-1-h
239	28	if (low == 0 \|\| high != var_bw - 1)
240		{
241	24	Assert(high != var_bw - 1);
242	24	uint32_t skolem_size = var_bw - high - 1;
243	48	Node skolem = utils::mkVar(skolem_size);
244	24	children.push_back(skolem);
245		}
246
247	28	children.push_back(c);
248
249		// create sk2 with size l
250	28	if (high == var_bw - 1 \|\| low != 0)
251		{
252	6	Assert(low != 0);
253	6	uint32_t skolem_size = low;
254	12	Node skolem = utils::mkVar(skolem_size);
255	6	children.push_back(skolem);
256		}
257
258	28	Node concat = utils::mkConcat(children);
259	28	Assert(utils::getSize(concat) == utils::getSize(extract[0]));
260	28	if (isLegalElimination(extract[0], concat))
261		{
262	28	outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
263	28	return Theory::PP_ASSERT_STATUS_SOLVED;
264		}
265		}
266		}
267		}
268	3781	return Theory::PP_ASSERT_STATUS_UNSOLVED;
269		}
270
271	251988	TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
272		{
273		// first, see if we need to expand definitions
274	503976	TrustNode texp = d_rewriter.expandDefinition(t);
275	251988	if (!texp.isNull())
276		{
277	107	return texp;
278		}
279
280	251881	Debug("theory-bv-pp-rewrite") << "ppRewrite " << t << "\n";
281	503762	Node res = t;
282	251881	if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t))
283		{
284	431	res = rewrite(RewriteRule<BitwiseEq>::run<false>(t));
285		}
286		// useful on QF_BV/space/ndist
287	251450	else if (RewriteRule<UltAddOne>::applies(t))
288		{
289	54	res = rewrite(RewriteRule<UltAddOne>::run<false>(t));
290		}
291		// Useful for BV/2017-Preiner-scholl-smt08, but not for QF_BV
292	251396	else if (options().bv.rwExtendEq)
293		{
294		if (RewriteRule<SignExtendEqConst>::applies(t))
295		{
296		res = RewriteRule<SignExtendEqConst>::run<false>(t);
297		}
298		else if (RewriteRule<ZeroExtendEqConst>::applies(t))
299		{
300		res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
301		}
302		}
303
304	251881	Debug("theory-bv-pp-rewrite") << "to " << res << "\n";
305	251881	if (res != t)
306		{
307	485	return TrustNode::mkTrustRewrite(t, res, nullptr);
308		}
309
310	251396	return d_internal->ppRewrite(t);
311		}
312
313	20560	void TheoryBV::presolve() { d_internal->presolve(); }
314
315	30447	EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
316		{
317	30447	EqualityStatus status = d_internal->getEqualityStatus(a, b);
318
319	30447	if (status == EqualityStatus::EQUALITY_UNKNOWN)
320		{
321	60894	Node value_a = getValue(a);
322	60894	Node value_b = getValue(b);
323
324	30447	if (value_a.isNull() \|\| value_b.isNull())
325		{
326		return status;
327		}
328
329	30447	if (value_a == value_b)
330		{
331	4052	Debug("theory-bv") << EQUALITY_TRUE_IN_MODEL << std::endl;
332	4052	return EQUALITY_TRUE_IN_MODEL;
333		}
334	26395	Debug("theory-bv") << EQUALITY_FALSE_IN_MODEL << std::endl;
335	26395	return EQUALITY_FALSE_IN_MODEL;
336		}
337		return status;
338		}
339
340	4986	TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
341
342	95686	void TheoryBV::notifySharedTerm(TNode t)
343		{
344	95686	d_internal->notifySharedTerm(t);
345	95686	}
346
347	250978	void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
348		{
349	250978	if (in.getKind() == kind::EQUAL)
350		{
351		// Only useful in combination with --bv-intro-pow2 on
352		// QF_BV/pspace/power2sum benchmarks.
353		//
354		// Matches for equality:
355		//
356		// (= (bvadd (bvshl 1 x) (bvshl 1 y)) (bvshl 1 z))
357		//
358		// and does case analysis on the sum of two power of twos.
359	71193	if ((in[0].getKind() == kind::BITVECTOR_ADD
360	23747	&& in[1].getKind() == kind::BITVECTOR_SHL)
361	118655	\|\| (in[1].getKind() == kind::BITVECTOR_ADD
362	23737	&& in[0].getKind() == kind::BITVECTOR_SHL))
363		{
364	4	TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1];
365	4	TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0];
366
367	6	if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
368	6	&& p[1].getKind() == kind::BITVECTOR_SHL)
369		{
370	8	if (utils::isOne(s[0]) && utils::isOne(p[0][0])
371	8	&& utils::isOne(p[1][0]))
372		{
373	4	Node zero = utils::mkZero(utils::getSize(s));
374	4	TNode b = p[0];
375	4	TNode c = p[1];
376		// (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
377	4	Node b_eq_0 = b.eqNode(zero);
378	4	Node c_eq_0 = c.eqNode(zero);
379	4	Node b_eq_c = b.eqNode(c);
380
381		Node dis = NodeManager::currentNM()->mkNode(
382	4	kind::OR, b_eq_0, c_eq_0, b_eq_c);
383	4	Node imp = in.impNode(dis);
384	2	learned << imp;
385		}
386		}
387		}
388		}
389
390	250978	d_internal->ppStaticLearn(in, learned);
391	250978	}
392
393	60894	Node TheoryBV::getValue(TNode node)
394		{
395	60894	if (d_invalidateModelCache.get())
396		{
397	250	d_modelCache.clear();
398		}
399	60894	d_invalidateModelCache.set(false);
400
401	121788	std::vector<TNode> visit;
402
403	121788	TNode cur;
404	60894	visit.push_back(node);
405	569	do
406		{
407	61463	cur = visit.back();
408	61463	visit.pop_back();
409
410	61463	auto it = d_modelCache.find(cur);
411	61463	if (it != d_modelCache.end() && !it->second.isNull())
412		{
413	121041	continue;
414		}
415
416	1715	if (cur.isConst())
417		{
418	272	d_modelCache[cur] = cur;
419	272	continue;
420		}
421
422	1613	Node value = d_internal->getValue(cur, false);
423	1648	if (value.isConst())
424		{
425	477	d_modelCache[cur] = value;
426	477	continue;
427		}
428
429	946	if (Theory::isLeafOf(cur, theory::THEORY_BV))
430		{
431	252	value = d_internal->getValue(cur, true);
432	252	d_modelCache[cur] = value;
433	252	continue;
434		}
435
436	442	if (it == d_modelCache.end())
437		{
438	221	visit.push_back(cur);
439	221	d_modelCache.emplace(cur, Node());
440	221	visit.insert(visit.end(), cur.begin(), cur.end());
441		}
442	221	else if (it->second.isNull())
443		{
444	442	NodeBuilder nb(cur.getKind());
445	221	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
446		{
447	33	nb << cur.getOperator();
448		}
449
450	221	std::unordered_map<Node, Node>::iterator iit;
451	569	for (const TNode& child : cur)
452		{
453	348	iit = d_modelCache.find(child);
454	348	Assert(iit != d_modelCache.end());
455	348	Assert(iit->second.isConst());
456	348	nb << iit->second;
457		}
458	221	it->second = rewrite(nb.constructNode());
459		}
460	61463	} while (!visit.empty());
461
462	60894	auto it = d_modelCache.find(node);
463	60894	Assert(it != d_modelCache.end());
464	121788	return it->second;
465		}
466
467	15273	TheoryBV::Statistics::Statistics(StatisticsRegistry& reg,
468	15273	const std::string& name)
469	15273	: d_solveSubstitutions(reg.registerInt(name + "NumSolveSubstitutions"))
470		{
471	15273	}
472
473		} // namespace bv
474		} // namespace theory
475	31137	} // namespace cvc5