Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv.cpp	Lines:	113	122	92.6 %
Date:	2021-05-24	Branches:	186	393	47.3 %


/******************************************************************************
 * 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 "expr/proof_checker.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/bv_solver_bitblast.h"
#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/bv_solver_simple.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_stats("theory::bv::")
{
  switch (options::bvSolver())
  {
    case options::BVSolver::BITBLAST:
      d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
      break;

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

    default:
      AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE);
      d_internal.reset(new BVSolverSimple(&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::SIMPLE)
  {
    return static_cast<BVSolverSimple*>(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_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();
}

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)
{
  return d_internal->getEqualityStatus(a, b);
}

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);
}

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 "expr/proof_checker.h"
19		#include "options/bv_options.h"
20		#include "options/smt_options.h"
21		#include "smt/smt_statistics_registry.h"
22		#include "theory/bv/bv_solver_bitblast.h"
23		#include "theory/bv/bv_solver_lazy.h"
24		#include "theory/bv/bv_solver_simple.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	9459	TheoryBV::TheoryBV(context::Context* c,
34		context::UserContext* u,
35		OutputChannel& out,
36		Valuation valuation,
37		const LogicInfo& logicInfo,
38		ProofNodeManager* pnm,
39	9459	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	9459	d_stats("theory::bv::")
47		{
48	9459	switch (options::bvSolver())
49		{
50		case options::BVSolver::BITBLAST:
51		d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
52		break;
53
54	9444	case options::BVSolver::LAZY:
55	9444	d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
56	9444	break;
57
58	15	default:
59	15	AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE);
60	15	d_internal.reset(new BVSolverSimple(&d_state, d_im, pnm));
61		}
62	9459	d_theoryState = &d_state;
63	9459	d_inferManager = &d_im;
64	9459	}
65
66	18918	TheoryBV::~TheoryBV() {}
67
68	9459	TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
69
70	3600	ProofRuleChecker* TheoryBV::getProofChecker()
71		{
72	3600	if (options::bvSolver() == options::BVSolver::SIMPLE)
73		{
74	3	return static_cast<BVSolverSimple*>(d_internal.get())->getProofChecker();
75		}
76	3597	return nullptr;
77		}
78
79	9459	bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
80		{
81	9459	bool need_ee = d_internal->needsEqualityEngine(esi);
82
83		/* Set up default notify class for equality engine. */
84	9459	if (need_ee && esi.d_notify == nullptr)
85		{
86		esi.d_notify = &d_notify;
87		esi.d_name = "theory::bv::ee";
88		}
89
90	9459	return need_ee;
91		}
92
93	9459	void TheoryBV::finishInit()
94		{
95		// these kinds are semi-evaluated in getModelValue (applications of this
96		// kind are treated as variables)
97	9459	getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
98	9459	getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
99	9459	d_internal->finishInit();
100
101	9459	eq::EqualityEngine* ee = getEqualityEngine();
102	9459	if (ee)
103		{
104		// The kinds we are treating as function application in congruence
105	9403	ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
106		// ee->addFunctionKind(kind::BITVECTOR_AND);
107		// ee->addFunctionKind(kind::BITVECTOR_OR);
108		// ee->addFunctionKind(kind::BITVECTOR_XOR);
109		// ee->addFunctionKind(kind::BITVECTOR_NOT);
110		// ee->addFunctionKind(kind::BITVECTOR_NAND);
111		// ee->addFunctionKind(kind::BITVECTOR_NOR);
112		// ee->addFunctionKind(kind::BITVECTOR_XNOR);
113		// ee->addFunctionKind(kind::BITVECTOR_COMP);
114	9403	ee->addFunctionKind(kind::BITVECTOR_MULT, true);
115	9403	ee->addFunctionKind(kind::BITVECTOR_ADD, true);
116	9403	ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
117		// ee->addFunctionKind(kind::BITVECTOR_SUB);
118		// ee->addFunctionKind(kind::BITVECTOR_NEG);
119		// ee->addFunctionKind(kind::BITVECTOR_UDIV);
120		// ee->addFunctionKind(kind::BITVECTOR_UREM);
121		// ee->addFunctionKind(kind::BITVECTOR_SDIV);
122		// ee->addFunctionKind(kind::BITVECTOR_SREM);
123		// ee->addFunctionKind(kind::BITVECTOR_SMOD);
124		// ee->addFunctionKind(kind::BITVECTOR_SHL);
125		// ee->addFunctionKind(kind::BITVECTOR_LSHR);
126		// ee->addFunctionKind(kind::BITVECTOR_ASHR);
127		// ee->addFunctionKind(kind::BITVECTOR_ULT);
128		// ee->addFunctionKind(kind::BITVECTOR_ULE);
129		// ee->addFunctionKind(kind::BITVECTOR_UGT);
130		// ee->addFunctionKind(kind::BITVECTOR_UGE);
131		// ee->addFunctionKind(kind::BITVECTOR_SLT);
132		// ee->addFunctionKind(kind::BITVECTOR_SLE);
133		// ee->addFunctionKind(kind::BITVECTOR_SGT);
134		// ee->addFunctionKind(kind::BITVECTOR_SGE);
135	9403	ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
136	9403	ee->addFunctionKind(kind::INT_TO_BITVECTOR);
137		}
138	9459	}
139
140	223881	void TheoryBV::preRegisterTerm(TNode node)
141		{
142	223881	d_internal->preRegisterTerm(node);
143
144	223881	eq::EqualityEngine* ee = getEqualityEngine();
145	223881	if (ee)
146		{
147	221279	if (node.getKind() == kind::EQUAL)
148		{
149	54604	ee->addTriggerPredicate(node);
150		}
151		else
152		{
153	166675	ee->addTerm(node);
154		}
155		}
156	223881	}
157
158	238668	bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
159
160	211	void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); }
161
162	862	bool TheoryBV::preNotifyFact(
163		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
164		{
165	862	return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
166		}
167
168		void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
169		{
170		d_internal->notifyFact(atom, pol, fact, isInternal);
171		}
172
173	8488	bool TheoryBV::needsCheckLastEffort()
174		{
175	8488	return d_internal->needsCheckLastEffort();
176		}
177
178	7165	bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
179		{
180	7165	return d_internal->collectModelValues(m, termSet);
181		}
182
183	829782	void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
184
185	3822	Theory::PPAssertStatus TheoryBV::ppAssert(
186		TrustNode tin, TrustSubstitutionMap& outSubstitutions)
187		{
188	7644	TNode in = tin.getNode();
189	3822	Kind k = in.getKind();
190	3822	if (k == kind::EQUAL)
191		{
192		// Substitute variables
193	1217	if (in[0].isVar() && isLegalElimination(in[0], in[1]))
194		{
195	233	++d_stats.d_solveSubstitutions;
196	233	outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
197	1024	return Theory::PP_ASSERT_STATUS_SOLVED;
198		}
199	984	if (in[1].isVar() && isLegalElimination(in[1], in[0]))
200		{
201	532	++d_stats.d_solveSubstitutions;
202	532	outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
203	532	return Theory::PP_ASSERT_STATUS_SOLVED;
204		}
205		/**
206		* Eliminate extract over bit-vector variables.
207		*
208		* Given x[h:l] = c, where c is a constant and x is a variable.
209		*
210		* We rewrite to:
211		*
212		* x = sk1::c if l == 0, where bw(sk1) = bw(x)-1-h
213		* x = c::sk2 if h == bw(x)-1, where bw(sk2) = l
214		* x = sk1::c::sk2 otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
215		*/
216	878	Node node = Rewriter::rewrite(in);
217	1410	if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
218	2282	\|\| (node[1].getKind() == kind::BITVECTOR_EXTRACT
219	518	&& node[0].isConst()))
220		{
221	62	Node extract = node[0].isConst() ? node[1] : node[0];
222	44	if (extract[0].isVar())
223		{
224	26	Node c = node[0].isConst() ? node[0] : node[1];
225
226	26	uint32_t high = utils::getExtractHigh(extract);
227	26	uint32_t low = utils::getExtractLow(extract);
228	26	uint32_t var_bw = utils::getSize(extract[0]);
229	26	std::vector<Node> children;
230
231		// create sk1 with size bw(x)-1-h
232	26	if (low == 0 \|\| high != var_bw - 1)
233		{
234	22	Assert(high != var_bw - 1);
235	22	uint32_t skolem_size = var_bw - high - 1;
236	44	Node skolem = utils::mkVar(skolem_size);
237	22	children.push_back(skolem);
238		}
239
240	26	children.push_back(c);
241
242		// create sk2 with size l
243	26	if (high == var_bw - 1 \|\| low != 0)
244		{
245	4	Assert(low != 0);
246	4	uint32_t skolem_size = low;
247	8	Node skolem = utils::mkVar(skolem_size);
248	4	children.push_back(skolem);
249		}
250
251	26	Node concat = utils::mkConcat(children);
252	26	Assert(utils::getSize(concat) == utils::getSize(extract[0]));
253	26	if (isLegalElimination(extract[0], concat))
254		{
255	26	outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
256	26	return Theory::PP_ASSERT_STATUS_SOLVED;
257		}
258		}
259		}
260		}
261	3031	return Theory::PP_ASSERT_STATUS_UNSOLVED;
262		}
263
264	316312	TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
265		{
266		// first, see if we need to expand definitions
267	632624	TrustNode texp = d_rewriter.expandDefinition(t);
268	316312	if (!texp.isNull())
269		{
270		return texp;
271		}
272	316312	return d_internal->ppRewrite(t);
273		}
274
275	14306	void TheoryBV::presolve() { d_internal->presolve(); }
276
277	55078	EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
278		{
279	55078	return d_internal->getEqualityStatus(a, b);
280		}
281
282	23652	TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
283
284	52482	void TheoryBV::notifySharedTerm(TNode t)
285		{
286	52482	d_internal->notifySharedTerm(t);
287	52482	}
288
289	104072	void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
290		{
291	104072	d_internal->ppStaticLearn(in, learned);
292	104072	}
293
294	4	bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
295		std::vector<Node>& new_assertions)
296		{
297	4	return d_internal->applyAbstraction(assertions, new_assertions);
298		}
299
300	9459	TheoryBV::Statistics::Statistics(const std::string& name)
301		: d_solveSubstitutions(
302	9459	smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions"))
303		{
304	9459	}
305
306		} // namespace bv
307		} // namespace theory
308	28191	} // namespace cvc5