Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_quick_check.cpp	Lines:	1	189	0.5 %
Date:	2021-05-22	Branches:	2	348	0.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Tim King, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Wrapper around the SAT solver used for bitblasting.
 */

#include "theory/bv/bv_quick_check.h"

#include "smt/smt_statistics_registry.h"
#include "theory/bv/bitblast/lazy_bitblaster.h"
#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv_utils.h"

using namespace cvc5::prop;

namespace cvc5 {
namespace theory {
namespace bv {

BVQuickCheck::BVQuickCheck(const std::string& name,
                           theory::bv::BVSolverLazy* bv)
    : d_ctx(),
      d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)),
      d_conflict(),
      d_inConflict(&d_ctx, false)
{}


bool BVQuickCheck::inConflict() { return d_inConflict.get(); }

uint64_t BVQuickCheck::computeAtomWeight(TNode node, NodeSet& seen) {
  return d_bitblaster->computeAtomWeight(node, seen);
}

void BVQuickCheck::setConflict()
{
  Assert(!inConflict());
  std::vector<TNode> conflict;
  d_bitblaster->getConflict(conflict);
  Node confl = utils::mkAnd(conflict);
  d_inConflict = true;
  d_conflict = confl;
}

prop::SatValue BVQuickCheck::checkSat(std::vector<Node>& assumptions, unsigned long budget) {
  Node conflict;

  for (unsigned i = 0; i < assumptions.size(); ++i) {
    TNode a = assumptions[i];
    Assert(a.getType().isBoolean());
    d_bitblaster->bbAtom(a);
    bool ok = d_bitblaster->assertToSat(a, false);
    if (!ok) {
      setConflict();
      return SAT_VALUE_FALSE;
    }
  }

  if (budget == 0) {
    bool ok = d_bitblaster->propagate();
    if (!ok) {
      setConflict();
      return SAT_VALUE_FALSE;
    }
    return SAT_VALUE_UNKNOWN; // could check if assignment is full and return SAT_VALUE_TRUE
  }

  prop::SatValue res = d_bitblaster->solveWithBudget(budget);
  if (res == SAT_VALUE_FALSE) {
    setConflict();
    return res;
  }
  // could be unknown or could be sat
   return res;
}

prop::SatValue BVQuickCheck::checkSat(unsigned long budget) {
  prop::SatValue res = d_bitblaster->solveWithBudget(budget);
  if (res == SAT_VALUE_FALSE) {
    setConflict();
  }
  return res;
}

bool BVQuickCheck::addAssertion(TNode assertion) {
  Assert(assertion.getType().isBoolean());
  d_bitblaster->bbAtom(assertion);
  // assert to sat solver and run bcp to detect easy conflicts
  bool ok = d_bitblaster->assertToSat(assertion, true);
  if (!ok) {
    setConflict();
  }
  return ok;
}


void BVQuickCheck::push() {
  d_ctx.push();
}

void BVQuickCheck::pop() {
  d_ctx.pop();
}

BVQuickCheck::vars_iterator BVQuickCheck::beginVars() {
  return d_bitblaster->beginVars();
}
BVQuickCheck::vars_iterator BVQuickCheck::endVars() {
  return d_bitblaster->endVars();
}

Node BVQuickCheck::getVarValue(TNode var, bool fullModel) {
  return d_bitblaster->getTermModel(var, fullModel);
}


/**
 * Constructs a new sat solver which requires throwing out the atomBBCache
 * but keeps all the termBBCache
 *
 */
void BVQuickCheck::clearSolver() {
  popToZero();
  d_bitblaster->clearSolver();
}

void BVQuickCheck::popToZero() {
  while (d_ctx.getLevel() > 0) {
    d_ctx.pop();
  }
}

bool BVQuickCheck::collectModelValues(theory::TheoryModel* model,
                                      const std::set<Node>& termSet)
{
  return d_bitblaster->collectModelValues(model, termSet);
}

BVQuickCheck::~BVQuickCheck() {
  clearSolver();
}

QuickXPlain::QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budget)
  : d_solver(solver)
  , d_budget(budget)
  , d_numCalled(0)
  , d_minRatioSum(0)
  , d_numConflicts(0)
  // , d_period(20)
  // , d_thresh(0.7)
  // , d_hardThresh(0.9)
  , d_statistics(name)
{}
QuickXPlain::~QuickXPlain() {}

unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high,
                                      std::vector<TNode>& conflict) {
  Assert(!d_solver->getConflict().isNull() && d_solver->inConflict());
  Node query_confl = d_solver->getConflict();

  // conflict wasn't actually minimized
  if (query_confl.getNumChildren() == high - low + 1) {
    return high;
  }

  TNodeSet nodes;
  for (unsigned i = low; i <= high; i++) {
    nodes.insert(conflict[i]);
  }

  unsigned write = low;
  for (unsigned i = 0; i < query_confl.getNumChildren(); ++i) {
    TNode current = query_confl[i];
    // the conflict can have nodes in lower decision levels
    if (nodes.find(current) != nodes.end()) {
      conflict[write++] = current;
      nodes.erase(nodes.find(current));
    }
  }
  // if all of the nodes in the conflict were on a lower level
  if (write == low) {
    return low;
  }
  Assert(write != 0);
  unsigned new_high = write - 1;

  for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) {
    conflict[write++] = *it;
  }
  Assert(write - 1 == high);
  Assert(new_high <= high);

  return new_high;
}

void QuickXPlain::minimizeConflictInternal(unsigned low, unsigned high,
                                           std::vector<TNode>& conflict,
                                           std::vector<TNode>& new_conflict) {
  Assert(low <= high && high < conflict.size());

  if (low == high) {
    new_conflict.push_back(conflict[low]);
    return;
  }

  // check if top half is unsat
  unsigned new_low = (high - low + 1)/ 2 + low;
  d_solver->push();

  for (unsigned i = new_low; i <=high; ++i) {
    bool ok = d_solver->addAssertion(conflict[i]);
    if (!ok) {
      unsigned top = selectUnsatCore(new_low, i, conflict);
      d_solver->pop();
      minimizeConflictInternal(new_low, top, conflict, new_conflict);
      return;
    }
  }

  SatValue res = d_solver->checkSat(d_budget);

  if (res == SAT_VALUE_UNKNOWN) {
    ++(d_statistics.d_numUnknown);
  } else {
    ++(d_statistics.d_numSolved);
  }

  if (res == SAT_VALUE_FALSE) {
    unsigned top = selectUnsatCore(new_low, high, conflict);
    d_solver->pop();
    minimizeConflictInternal(new_low, top, conflict, new_conflict);
    return;
  }

  d_solver->pop();
  unsigned new_high = new_low - 1;
  d_solver->push();

  // check bottom half
  for (unsigned i = low; i <= new_high; ++i) {
    bool ok = d_solver->addAssertion(conflict[i]);
    if (!ok) {
      unsigned top = selectUnsatCore(low, i, conflict);
      d_solver->pop();
      minimizeConflictInternal(low, top, conflict, new_conflict);
      return;
    }
  }

  res = d_solver->checkSat(d_budget);

  if (res == SAT_VALUE_UNKNOWN) {
    ++(d_statistics.d_numUnknown);
  } else {
    ++(d_statistics.d_numSolved);
  }

  if (res == SAT_VALUE_FALSE) {
    unsigned top = selectUnsatCore(low, new_high, conflict);
    d_solver->pop();
    minimizeConflictInternal(low, top, conflict, new_conflict);
    return;
  }

  // conflict (probably) contains literals in both halves
  // keep bottom half in context (no pop)
  minimizeConflictInternal(new_low, high, conflict, new_conflict);
  d_solver->pop();
  d_solver->push();
  for (unsigned i = 0; i < new_conflict.size(); ++i) {
    bool ok = d_solver->addAssertion(new_conflict[i]);
    if (!ok) {
      ++(d_statistics.d_numUnknownWasUnsat);
      d_solver->pop();
      return;
    }
  }
  minimizeConflictInternal(low, new_high, conflict, new_conflict);
  d_solver->pop();
}


bool QuickXPlain::useHeuristic() {
  return true;
  // d_statistics.d_finalPeriod.setData(d_period);
  // // try to minimize conflict periodically
  // if (d_numConflicts % d_period == 0)
  //   return true;

  // if (d_numCalled == 0) {
  //   return true;
  // }

  // if (d_minRatioSum / d_numCalled >= d_thresh &&
  //     d_numCalled <= 20 ) {
  //   return false;
  // }

  // if (d_minRatioSum / d_numCalled >= d_hardThresh) {
  //   return false;
  // }

  // return true;
}

Node QuickXPlain::minimizeConflict(TNode confl) {
  ++d_numConflicts;

  if (!useHeuristic()) {
    return confl;
  }

  ++d_numCalled;
  ++(d_statistics.d_numConflictsMinimized);
  TimerStat::CodeTimer xplainTimer(d_statistics.d_xplainTime);
  Assert(confl.getNumChildren() > 2);
  std::vector<TNode> conflict;
  for (unsigned i = 0; i < confl.getNumChildren(); ++i) {
    conflict.push_back(confl[i]);
  }
  d_solver->popToZero();
  std::vector<TNode> minimized;
  minimizeConflictInternal(0, conflict.size() - 1, conflict, minimized);

  double minimization_ratio = ((double) minimized.size())/confl.getNumChildren();
  d_minRatioSum+= minimization_ratio;


  // if (minimization_ratio >= d_hardThresh) {
  //   d_period = d_period * 5;
  // }

  // if (minimization_ratio <= d_thresh && d_period >= 40) {
  //   d_period = d_period *0.5;
  // }

  // if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) {
  //   d_period = d_period * 2;
  // }
  d_statistics.d_avgMinimizationRatio << minimization_ratio;
  return utils::mkAnd(minimized);
}

QuickXPlain::Statistics::Statistics(const std::string& name)
    : d_xplainTime(
        smtStatisticsRegistry().registerTimer(name + "QuickXplain::Time")),
      d_numSolved(
          smtStatisticsRegistry().registerInt(name + "QuickXplain::NumSolved")),
      d_numUnknown(smtStatisticsRegistry().registerInt(
          name + "QuickXplain::NumUnknown")),
      d_numUnknownWasUnsat(smtStatisticsRegistry().registerInt(
          name + "QuickXplain::NumUnknownWasUnsat")),
      d_numConflictsMinimized(smtStatisticsRegistry().registerInt(
          name + "QuickXplain::NumConflictsMinimized")),
      d_finalPeriod(smtStatisticsRegistry().registerInt(
          name + "QuickXplain::FinalPeriod")),
      d_avgMinimizationRatio(smtStatisticsRegistry().registerAverage(
          name + "QuickXplain::AvgMinRatio"))
{
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Liana Hadarean, Tim King, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Wrapper around the SAT solver used for bitblasting.
14		*/
15
16		#include "theory/bv/bv_quick_check.h"
17
18		#include "smt/smt_statistics_registry.h"
19		#include "theory/bv/bitblast/lazy_bitblaster.h"
20		#include "theory/bv/bv_solver_lazy.h"
21		#include "theory/bv/theory_bv_utils.h"
22
23		using namespace cvc5::prop;
24
25		namespace cvc5 {
26		namespace theory {
27		namespace bv {
28
29		BVQuickCheck::BVQuickCheck(const std::string& name,
30		theory::bv::BVSolverLazy* bv)
31		: d_ctx(),
32		d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)),
33		d_conflict(),
34		d_inConflict(&d_ctx, false)
35		{}
36
37
38		bool BVQuickCheck::inConflict() { return d_inConflict.get(); }
39
40		uint64_t BVQuickCheck::computeAtomWeight(TNode node, NodeSet& seen) {
41		return d_bitblaster->computeAtomWeight(node, seen);
42		}
43
44		void BVQuickCheck::setConflict()
45		{
46		Assert(!inConflict());
47		std::vector<TNode> conflict;
48		d_bitblaster->getConflict(conflict);
49		Node confl = utils::mkAnd(conflict);
50		d_inConflict = true;
51		d_conflict = confl;
52		}
53
54		prop::SatValue BVQuickCheck::checkSat(std::vector<Node>& assumptions, unsigned long budget) {
55		Node conflict;
56
57		for (unsigned i = 0; i < assumptions.size(); ++i) {
58		TNode a = assumptions[i];
59		Assert(a.getType().isBoolean());
60		d_bitblaster->bbAtom(a);
61		bool ok = d_bitblaster->assertToSat(a, false);
62		if (!ok) {
63		setConflict();
64		return SAT_VALUE_FALSE;
65		}
66		}
67
68		if (budget == 0) {
69		bool ok = d_bitblaster->propagate();
70		if (!ok) {
71		setConflict();
72		return SAT_VALUE_FALSE;
73		}
74		return SAT_VALUE_UNKNOWN; // could check if assignment is full and return SAT_VALUE_TRUE
75		}
76
77		prop::SatValue res = d_bitblaster->solveWithBudget(budget);
78		if (res == SAT_VALUE_FALSE) {
79		setConflict();
80		return res;
81		}
82		// could be unknown or could be sat
83		return res;
84		}
85
86		prop::SatValue BVQuickCheck::checkSat(unsigned long budget) {
87		prop::SatValue res = d_bitblaster->solveWithBudget(budget);
88		if (res == SAT_VALUE_FALSE) {
89		setConflict();
90		}
91		return res;
92		}
93
94		bool BVQuickCheck::addAssertion(TNode assertion) {
95		Assert(assertion.getType().isBoolean());
96		d_bitblaster->bbAtom(assertion);
97		// assert to sat solver and run bcp to detect easy conflicts
98		bool ok = d_bitblaster->assertToSat(assertion, true);
99		if (!ok) {
100		setConflict();
101		}
102		return ok;
103		}
104
105
106		void BVQuickCheck::push() {
107		d_ctx.push();
108		}
109
110		void BVQuickCheck::pop() {
111		d_ctx.pop();
112		}
113
114		BVQuickCheck::vars_iterator BVQuickCheck::beginVars() {
115		return d_bitblaster->beginVars();
116		}
117		BVQuickCheck::vars_iterator BVQuickCheck::endVars() {
118		return d_bitblaster->endVars();
119		}
120
121		Node BVQuickCheck::getVarValue(TNode var, bool fullModel) {
122		return d_bitblaster->getTermModel(var, fullModel);
123		}
124
125
126		/**
127		* Constructs a new sat solver which requires throwing out the atomBBCache
128		* but keeps all the termBBCache
129		*
130		*/
131		void BVQuickCheck::clearSolver() {
132		popToZero();
133		d_bitblaster->clearSolver();
134		}
135
136		void BVQuickCheck::popToZero() {
137		while (d_ctx.getLevel() > 0) {
138		d_ctx.pop();
139		}
140		}
141
142		bool BVQuickCheck::collectModelValues(theory::TheoryModel* model,
143		const std::set<Node>& termSet)
144		{
145		return d_bitblaster->collectModelValues(model, termSet);
146		}
147
148		BVQuickCheck::~BVQuickCheck() {
149		clearSolver();
150		}
151
152		QuickXPlain::QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budget)
153		: d_solver(solver)
154		, d_budget(budget)
155		, d_numCalled(0)
156		, d_minRatioSum(0)
157		, d_numConflicts(0)
158		// , d_period(20)
159		// , d_thresh(0.7)
160		// , d_hardThresh(0.9)
161		, d_statistics(name)
162		{}
163		QuickXPlain::~QuickXPlain() {}
164
165		unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high,
166		std::vector<TNode>& conflict) {
167		Assert(!d_solver->getConflict().isNull() && d_solver->inConflict());
168		Node query_confl = d_solver->getConflict();
169
170		// conflict wasn't actually minimized
171		if (query_confl.getNumChildren() == high - low + 1) {
172		return high;
173		}
174
175		TNodeSet nodes;
176		for (unsigned i = low; i <= high; i++) {
177		nodes.insert(conflict[i]);
178		}
179
180		unsigned write = low;
181		for (unsigned i = 0; i < query_confl.getNumChildren(); ++i) {
182		TNode current = query_confl[i];
183		// the conflict can have nodes in lower decision levels
184		if (nodes.find(current) != nodes.end()) {
185		conflict[write++] = current;
186		nodes.erase(nodes.find(current));
187		}
188		}
189		// if all of the nodes in the conflict were on a lower level
190		if (write == low) {
191		return low;
192		}
193		Assert(write != 0);
194		unsigned new_high = write - 1;
195
196		for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) {
197		conflict[write++] = *it;
198		}
199		Assert(write - 1 == high);
200		Assert(new_high <= high);
201
202		return new_high;
203		}
204
205		void QuickXPlain::minimizeConflictInternal(unsigned low, unsigned high,
206		std::vector<TNode>& conflict,
207		std::vector<TNode>& new_conflict) {
208		Assert(low <= high && high < conflict.size());
209
210		if (low == high) {
211		new_conflict.push_back(conflict[low]);
212		return;
213		}
214
215		// check if top half is unsat
216		unsigned new_low = (high - low + 1)/ 2 + low;
217		d_solver->push();
218
219		for (unsigned i = new_low; i <=high; ++i) {
220		bool ok = d_solver->addAssertion(conflict[i]);
221		if (!ok) {
222		unsigned top = selectUnsatCore(new_low, i, conflict);
223		d_solver->pop();
224		minimizeConflictInternal(new_low, top, conflict, new_conflict);
225		return;
226		}
227		}
228
229		SatValue res = d_solver->checkSat(d_budget);
230
231		if (res == SAT_VALUE_UNKNOWN) {
232		++(d_statistics.d_numUnknown);
233		} else {
234		++(d_statistics.d_numSolved);
235		}
236
237		if (res == SAT_VALUE_FALSE) {
238		unsigned top = selectUnsatCore(new_low, high, conflict);
239		d_solver->pop();
240		minimizeConflictInternal(new_low, top, conflict, new_conflict);
241		return;
242		}
243
244		d_solver->pop();
245		unsigned new_high = new_low - 1;
246		d_solver->push();
247
248		// check bottom half
249		for (unsigned i = low; i <= new_high; ++i) {
250		bool ok = d_solver->addAssertion(conflict[i]);
251		if (!ok) {
252		unsigned top = selectUnsatCore(low, i, conflict);
253		d_solver->pop();
254		minimizeConflictInternal(low, top, conflict, new_conflict);
255		return;
256		}
257		}
258
259		res = d_solver->checkSat(d_budget);
260
261		if (res == SAT_VALUE_UNKNOWN) {
262		++(d_statistics.d_numUnknown);
263		} else {
264		++(d_statistics.d_numSolved);
265		}
266
267		if (res == SAT_VALUE_FALSE) {
268		unsigned top = selectUnsatCore(low, new_high, conflict);
269		d_solver->pop();
270		minimizeConflictInternal(low, top, conflict, new_conflict);
271		return;
272		}
273
274		// conflict (probably) contains literals in both halves
275		// keep bottom half in context (no pop)
276		minimizeConflictInternal(new_low, high, conflict, new_conflict);
277		d_solver->pop();
278		d_solver->push();
279		for (unsigned i = 0; i < new_conflict.size(); ++i) {
280		bool ok = d_solver->addAssertion(new_conflict[i]);
281		if (!ok) {
282		++(d_statistics.d_numUnknownWasUnsat);
283		d_solver->pop();
284		return;
285		}
286		}
287		minimizeConflictInternal(low, new_high, conflict, new_conflict);
288		d_solver->pop();
289		}
290
291
292		bool QuickXPlain::useHeuristic() {
293		return true;
294		// d_statistics.d_finalPeriod.setData(d_period);
295		// // try to minimize conflict periodically
296		// if (d_numConflicts % d_period == 0)
297		// return true;
298
299		// if (d_numCalled == 0) {
300		// return true;
301		// }
302
303		// if (d_minRatioSum / d_numCalled >= d_thresh &&
304		// d_numCalled <= 20 ) {
305		// return false;
306		// }
307
308		// if (d_minRatioSum / d_numCalled >= d_hardThresh) {
309		// return false;
310		// }
311
312		// return true;
313		}
314
315		Node QuickXPlain::minimizeConflict(TNode confl) {
316		++d_numConflicts;
317
318		if (!useHeuristic()) {
319		return confl;
320		}
321
322		++d_numCalled;
323		++(d_statistics.d_numConflictsMinimized);
324		TimerStat::CodeTimer xplainTimer(d_statistics.d_xplainTime);
325		Assert(confl.getNumChildren() > 2);
326		std::vector<TNode> conflict;
327		for (unsigned i = 0; i < confl.getNumChildren(); ++i) {
328		conflict.push_back(confl[i]);
329		}
330		d_solver->popToZero();
331		std::vector<TNode> minimized;
332		minimizeConflictInternal(0, conflict.size() - 1, conflict, minimized);
333
334		double minimization_ratio = ((double) minimized.size())/confl.getNumChildren();
335		d_minRatioSum+= minimization_ratio;
336
337
338		// if (minimization_ratio >= d_hardThresh) {
339		// d_period = d_period * 5;
340		// }
341
342		// if (minimization_ratio <= d_thresh && d_period >= 40) {
343		// d_period = d_period *0.5;
344		// }
345
346		// if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) {
347		// d_period = d_period * 2;
348		// }
349		d_statistics.d_avgMinimizationRatio << minimization_ratio;
350		return utils::mkAnd(minimized);
351		}
352
353		QuickXPlain::Statistics::Statistics(const std::string& name)
354		: d_xplainTime(
355		smtStatisticsRegistry().registerTimer(name + "QuickXplain::Time")),
356		d_numSolved(
357		smtStatisticsRegistry().registerInt(name + "QuickXplain::NumSolved")),
358		d_numUnknown(smtStatisticsRegistry().registerInt(
359		name + "QuickXplain::NumUnknown")),
360		d_numUnknownWasUnsat(smtStatisticsRegistry().registerInt(
361		name + "QuickXplain::NumUnknownWasUnsat")),
362		d_numConflictsMinimized(smtStatisticsRegistry().registerInt(
363		name + "QuickXplain::NumConflictsMinimized")),
364		d_finalPeriod(smtStatisticsRegistry().registerInt(
365		name + "QuickXplain::FinalPeriod")),
366		d_avgMinimizationRatio(smtStatisticsRegistry().registerAverage(
367		name + "QuickXplain::AvgMinRatio"))
368		{
369		}
370
371		} // namespace bv
372		} // namespace theory
373	28191	} // namespace cvc5