Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv.cpp	Lines:	180	182	98.9 %
Date:	2021-08-01	Branches:	301	619	48.6 %


/******************************************************************************
 * 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/bv_solver_layered.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/ee_setup_info.h"
#include "theory/trust_substitutions.h"

namespace cvc5 {
namespace theory {
namespace bv {

TheoryBV::TheoryBV(context::Context* c,
                   context::UserContext* u,
                   OutputChannel& out,
                   Valuation valuation,
                   const LogicInfo& logicInfo,
                   ProofNodeManager* pnm,
                   std::string name)
    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
      d_internal(nullptr),
      d_rewriter(),
      d_state(c, u, valuation),
      d_im(*this, d_state, nullptr, "theory::bv::"),
      d_notify(d_im),
      d_invalidateModelCache(c, true),
      d_stats("theory::bv::")
{
  switch (options::bvSolver())
  {
    case options::BVSolver::BITBLAST:
      d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
      break;

    case options::BVSolver::LAYERED:
      d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name));
      break;

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

TheoryBV::~TheoryBV() {}

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

ProofRuleChecker* TheoryBV::getProofChecker()
{
  if (options::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 = Rewriter::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;
  }
  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)
{
  d_internal->ppStaticLearn(in, learned);
}

bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
                                std::vector<Node>& new_assertions)
{
  return d_internal->applyAbstraction(assertions, new_assertions);
}

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 = Rewriter::rewrite(nb.constructNode());
    }
  } while (!visit.empty());

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

TheoryBV::Statistics::Statistics(const std::string& name)
    : d_solveSubstitutions(
        smtStatisticsRegistry().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/bv_solver_layered.h"
25		#include "theory/bv/theory_bv_utils.h"
26		#include "theory/ee_setup_info.h"
27		#include "theory/trust_substitutions.h"
28
29		namespace cvc5 {
30		namespace theory {
31		namespace bv {
32
33	9838	TheoryBV::TheoryBV(context::Context* c,
34		context::UserContext* u,
35		OutputChannel& out,
36		Valuation valuation,
37		const LogicInfo& logicInfo,
38		ProofNodeManager* pnm,
39	9838	std::string name)
40		: Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
41		d_internal(nullptr),
42		d_rewriter(),
43		d_state(c, u, valuation),
44		d_im(*this, d_state, nullptr, "theory::bv::"),
45		d_notify(d_im),
46		d_invalidateModelCache(c, true),
47	9838	d_stats("theory::bv::")
48		{
49	9838	switch (options::bvSolver())
50		{
51	6094	case options::BVSolver::BITBLAST:
52	6094	d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
53	6094	break;
54
55	2	case options::BVSolver::LAYERED:
56	2	d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name));
57	2	break;
58
59	3742	default:
60	3742	AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL);
61	3742	d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm));
62		}
63	9838	d_theoryState = &d_state;
64	9838	d_inferManager = &d_im;
65	9838	}
66
67	19676	TheoryBV::~TheoryBV() {}
68
69	9838	TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
70
71	3756	ProofRuleChecker* TheoryBV::getProofChecker()
72		{
73	3756	if (options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL)
74		{
75	3728	return static_cast<BVSolverBitblastInternal*>(d_internal.get())
76	3728	->getProofChecker();
77		}
78	28	return nullptr;
79		}
80
81	9838	bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
82		{
83	9838	bool need_ee = d_internal->needsEqualityEngine(esi);
84
85		/* Set up default notify class for equality engine. */
86	9838	if (need_ee && esi.d_notify == nullptr)
87		{
88	9836	esi.d_notify = &d_notify;
89	9836	esi.d_name = "theory::bv::ee";
90		}
91
92	9838	return need_ee;
93		}
94
95	9838	void TheoryBV::finishInit()
96		{
97		// these kinds are semi-evaluated in getModelValue (applications of this
98		// kind are treated as variables)
99	9838	getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
100	9838	getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
101	9838	d_internal->finishInit();
102
103	9838	eq::EqualityEngine* ee = getEqualityEngine();
104	9838	if (ee)
105		{
106		// The kinds we are treating as function application in congruence
107	9836	ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
108		// ee->addFunctionKind(kind::BITVECTOR_AND);
109		// ee->addFunctionKind(kind::BITVECTOR_OR);
110		// ee->addFunctionKind(kind::BITVECTOR_XOR);
111		// ee->addFunctionKind(kind::BITVECTOR_NOT);
112		// ee->addFunctionKind(kind::BITVECTOR_NAND);
113		// ee->addFunctionKind(kind::BITVECTOR_NOR);
114		// ee->addFunctionKind(kind::BITVECTOR_XNOR);
115		// ee->addFunctionKind(kind::BITVECTOR_COMP);
116	9836	ee->addFunctionKind(kind::BITVECTOR_MULT, true);
117	9836	ee->addFunctionKind(kind::BITVECTOR_ADD, true);
118	9836	ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
119		// ee->addFunctionKind(kind::BITVECTOR_SUB);
120		// ee->addFunctionKind(kind::BITVECTOR_NEG);
121		// ee->addFunctionKind(kind::BITVECTOR_UDIV);
122		// ee->addFunctionKind(kind::BITVECTOR_UREM);
123		// ee->addFunctionKind(kind::BITVECTOR_SDIV);
124		// ee->addFunctionKind(kind::BITVECTOR_SREM);
125		// ee->addFunctionKind(kind::BITVECTOR_SMOD);
126		// ee->addFunctionKind(kind::BITVECTOR_SHL);
127		// ee->addFunctionKind(kind::BITVECTOR_LSHR);
128		// ee->addFunctionKind(kind::BITVECTOR_ASHR);
129		// ee->addFunctionKind(kind::BITVECTOR_ULT);
130		// ee->addFunctionKind(kind::BITVECTOR_ULE);
131		// ee->addFunctionKind(kind::BITVECTOR_UGT);
132		// ee->addFunctionKind(kind::BITVECTOR_UGE);
133		// ee->addFunctionKind(kind::BITVECTOR_SLT);
134		// ee->addFunctionKind(kind::BITVECTOR_SLE);
135		// ee->addFunctionKind(kind::BITVECTOR_SGT);
136		// ee->addFunctionKind(kind::BITVECTOR_SGE);
137	9836	ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
138	9836	ee->addFunctionKind(kind::INT_TO_BITVECTOR);
139		}
140	9838	}
141
142	347709	void TheoryBV::preRegisterTerm(TNode node)
143		{
144	347709	d_internal->preRegisterTerm(node);
145
146	347709	eq::EqualityEngine* ee = getEqualityEngine();
147	347709	if (ee)
148		{
149	347709	if (node.getKind() == kind::EQUAL)
150		{
151	50050	ee->addTriggerPredicate(node);
152		}
153		else
154		{
155	297659	ee->addTerm(node);
156		}
157		}
158	347709	}
159
160	975947	bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
161
162	975947	void TheoryBV::postCheck(Effort e)
163		{
164	975947	d_invalidateModelCache = true;
165	975947	d_internal->postCheck(e);
166	975947	}
167
168	3222889	bool TheoryBV::preNotifyFact(
169		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
170		{
171	3222889	return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
172		}
173
174	1199047	void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
175		{
176	1199047	d_internal->notifyFact(atom, pol, fact, isInternal);
177	1199047	}
178
179	9154	bool TheoryBV::needsCheckLastEffort()
180		{
181	9154	return d_internal->needsCheckLastEffort();
182		}
183
184	7816	void TheoryBV::computeRelevantTerms(std::set<Node>& termSet)
185		{
186	7816	return d_internal->computeRelevantTerms(termSet);
187		}
188
189	7816	bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
190		{
191	7816	return d_internal->collectModelValues(m, termSet);
192		}
193
194	1556949	void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
195
196	4405	Theory::PPAssertStatus TheoryBV::ppAssert(
197		TrustNode tin, TrustSubstitutionMap& outSubstitutions)
198		{
199	8810	TNode in = tin.getNode();
200	4405	Kind k = in.getKind();
201	4405	if (k == kind::EQUAL)
202		{
203		// Substitute variables
204	1198	if (in[0].isVar() && isLegalElimination(in[0], in[1]))
205		{
206	226	++d_stats.d_solveSubstitutions;
207	226	outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
208	987	return Theory::PP_ASSERT_STATUS_SOLVED;
209		}
210	972	if (in[1].isVar() && isLegalElimination(in[1], in[0]))
211		{
212	507	++d_stats.d_solveSubstitutions;
213	507	outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
214	507	return Theory::PP_ASSERT_STATUS_SOLVED;
215		}
216		/**
217		* Eliminate extract over bit-vector variables.
218		*
219		* Given x[h:l] = c, where c is a constant and x is a variable.
220		*
221		* We rewrite to:
222		*
223		* x = sk1::c if l == 0, where bw(sk1) = bw(x)-1-h
224		* x = c::sk2 if h == bw(x)-1, where bw(sk2) = l
225		* x = sk1::c::sk2 otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
226		*/
227	902	Node node = Rewriter::rewrite(in);
228	1454	if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
229	2347	\|\| (node[1].getKind() == kind::BITVECTOR_EXTRACT
230	532	&& node[0].isConst()))
231		{
232	68	Node extract = node[0].isConst() ? node[1] : node[0];
233	48	if (extract[0].isVar())
234		{
235	28	Node c = node[0].isConst() ? node[0] : node[1];
236
237	28	uint32_t high = utils::getExtractHigh(extract);
238	28	uint32_t low = utils::getExtractLow(extract);
239	28	uint32_t var_bw = utils::getSize(extract[0]);
240	28	std::vector<Node> children;
241
242		// create sk1 with size bw(x)-1-h
243	28	if (low == 0 \|\| high != var_bw - 1)
244		{
245	24	Assert(high != var_bw - 1);
246	24	uint32_t skolem_size = var_bw - high - 1;
247	48	Node skolem = utils::mkVar(skolem_size);
248	24	children.push_back(skolem);
249		}
250
251	28	children.push_back(c);
252
253		// create sk2 with size l
254	28	if (high == var_bw - 1 \|\| low != 0)
255		{
256	6	Assert(low != 0);
257	6	uint32_t skolem_size = low;
258	12	Node skolem = utils::mkVar(skolem_size);
259	6	children.push_back(skolem);
260		}
261
262	28	Node concat = utils::mkConcat(children);
263	28	Assert(utils::getSize(concat) == utils::getSize(extract[0]));
264	28	if (isLegalElimination(extract[0], concat))
265		{
266	28	outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
267	28	return Theory::PP_ASSERT_STATUS_SOLVED;
268		}
269		}
270		}
271		}
272	3644	return Theory::PP_ASSERT_STATUS_UNSOLVED;
273		}
274
275	424711	TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
276		{
277		// first, see if we need to expand definitions
278	849422	TrustNode texp = d_rewriter.expandDefinition(t);
279	424711	if (!texp.isNull())
280		{
281	96	return texp;
282		}
283	424615	return d_internal->ppRewrite(t);
284		}
285
286	15189	void TheoryBV::presolve() { d_internal->presolve(); }
287
288	28965	EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
289		{
290	28965	EqualityStatus status = d_internal->getEqualityStatus(a, b);
291
292	28965	if (status == EqualityStatus::EQUALITY_UNKNOWN)
293		{
294	57930	Node value_a = getValue(a);
295	57930	Node value_b = getValue(b);
296
297	28965	if (value_a.isNull() \|\| value_b.isNull())
298		{
299		return status;
300		}
301
302	28965	if (value_a == value_b)
303		{
304	4172	Debug("theory-bv") << EQUALITY_TRUE_IN_MODEL << std::endl;
305	4172	return EQUALITY_TRUE_IN_MODEL;
306		}
307	24793	Debug("theory-bv") << EQUALITY_FALSE_IN_MODEL << std::endl;
308	24793	return EQUALITY_FALSE_IN_MODEL;
309		}
310		return status;
311		}
312
313	4420	TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
314
315	88260	void TheoryBV::notifySharedTerm(TNode t)
316		{
317	88260	d_internal->notifySharedTerm(t);
318	88260	}
319
320	105752	void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
321		{
322	105752	d_internal->ppStaticLearn(in, learned);
323	105752	}
324
325	4	bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
326		std::vector<Node>& new_assertions)
327		{
328	4	return d_internal->applyAbstraction(assertions, new_assertions);
329		}
330
331	57930	Node TheoryBV::getValue(TNode node)
332		{
333	57930	if (d_invalidateModelCache.get())
334		{
335	248	d_modelCache.clear();
336		}
337	57930	d_invalidateModelCache.set(false);
338
339	115860	std::vector<TNode> visit;
340
341	115860	TNode cur;
342	57930	visit.push_back(node);
343	561	do
344		{
345	58491	cur = visit.back();
346	58491	visit.pop_back();
347
348	58491	auto it = d_modelCache.find(cur);
349	58491	if (it != d_modelCache.end() && !it->second.isNull())
350		{
351	115107	continue;
352		}
353
354	1722	if (cur.isConst())
355		{
356	281	d_modelCache[cur] = cur;
357	281	continue;
358		}
359
360	1594	Node value = d_internal->getValue(cur, false);
361	1639	if (value.isConst())
362		{
363	479	d_modelCache[cur] = value;
364	479	continue;
365		}
366
367	928	if (Theory::isLeafOf(cur, theory::THEORY_BV))
368		{
369	247	value = d_internal->getValue(cur, true);
370	247	d_modelCache[cur] = value;
371	247	continue;
372		}
373
374	434	if (it == d_modelCache.end())
375		{
376	217	visit.push_back(cur);
377	217	d_modelCache.emplace(cur, Node());
378	217	visit.insert(visit.end(), cur.begin(), cur.end());
379		}
380	217	else if (it->second.isNull())
381		{
382	434	NodeBuilder nb(cur.getKind());
383	217	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
384		{
385	29	nb << cur.getOperator();
386		}
387
388	217	std::unordered_map<Node, Node>::iterator iit;
389	561	for (const TNode& child : cur)
390		{
391	344	iit = d_modelCache.find(child);
392	344	Assert(iit != d_modelCache.end());
393	344	Assert(iit->second.isConst());
394	344	nb << iit->second;
395		}
396	217	it->second = Rewriter::rewrite(nb.constructNode());
397		}
398	58491	} while (!visit.empty());
399
400	57930	auto it = d_modelCache.find(node);
401	57930	Assert(it != d_modelCache.end());
402	115860	return it->second;
403		}
404
405	9838	TheoryBV::Statistics::Statistics(const std::string& name)
406		: d_solveSubstitutions(
407	9838	smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions"))
408		{
409	9838	}
410
411		} // namespace bv
412		} // namespace theory
413	29280	} // namespace cvc5