Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_subtheory_inequality.cpp	Lines:	1	139	0.7 %
Date:	2021-08-13	Branches:	2	638	0.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Aina Niemetz, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Algebraic solver.
 */

#include "theory/bv/bv_subtheory_inequality.h"

#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/bv_solver_layered.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"

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

bool InequalitySolver::check(Theory::Effort e) {
  Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
  TimerStat::CodeTimer inequalityTimer(d_statistics.d_solveTime);
  ++(d_statistics.d_numCallstoCheck);
  d_bv->spendResource(Resource::TheoryCheckStep);

  bool ok = true;
  while (!done() && ok) {
    TNode fact = get();
    Debug("bv-subtheory-inequality") << "  "<< fact <<"\n";
    if (fact.getKind() == kind::EQUAL) {
      TNode a = fact[0];
      if( a.getType().isBitVector() ){
        TNode b = fact[1];
        ok = addInequality(a, b, false, fact);
        if (ok)
          ok = addInequality(b, a, false, fact);
      }
    } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
      TNode a = fact[0][0];
      if( a.getType().isBitVector() ){
        TNode b = fact[0][1];
        ok = d_inequalityGraph.addDisequality(a, b, fact);
      }
    }
    if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
      TNode a = fact[0][1];
      TNode b = fact[0][0];
      ok = addInequality(a, b, true, fact);
      // propagate
      // NodeManager *nm = NodeManager::currentNM();
      // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
      //   Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, a, b));
      //   d_bv->storePropagation(neq, SUB_INEQUALITY);
      //   d_explanations[neq] = fact;
      // }
    } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
      TNode a = fact[0][1];
      TNode b = fact[0][0];
      ok = addInequality(a, b, false, fact);
    } else if (fact.getKind() == kind::BITVECTOR_ULT) {
      TNode a = fact[0];
      TNode b = fact[1];
      ok = addInequality(a, b, true, fact);
      // propagate
      // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
      //   Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, a, b));
      //   d_bv->storePropagation(neq, SUB_INEQUALITY);
      //   d_explanations[neq] = fact;
      // }
    } else if (fact.getKind() == kind::BITVECTOR_ULE) {
      TNode a = fact[0];
      TNode b = fact[1];
      ok = addInequality(a, b, false, fact);
    }
  }

  if (!ok) {
    std::vector<TNode> conflict;
    d_inequalityGraph.getConflict(conflict);
    Node confl = utils::flattenAnd(conflict);
    d_bv->setConflict(confl);
    Debug("bv-subtheory-inequality") << "InequalitySolver::conflict:  "<< confl <<"\n";
    return false;
  }

  if (isComplete() && Theory::fullEffort(e)) {
    // make sure all the disequalities we didn't split on are still satisifed
    // and split on the ones that are not
    std::vector<Node> lemmas;
    d_inequalityGraph.checkDisequalities(lemmas);
    for(unsigned i = 0; i < lemmas.size(); ++i) {
      d_bv->lemma(lemmas[i]);
    }
  }
  Debug("bv-subtheory-inequality") << "InequalitySolver done. ";
  return true;
}

EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b)
{
  if (!isComplete()) return EQUALITY_UNKNOWN;

  NodeManager* nm = NodeManager::currentNM();
  Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b);
  Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a);

  // if an inequality containing the terms has been asserted then we know
  // the equality is false
  if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a))
  {
    return EQUALITY_FALSE;
  }

  if (!d_inequalityGraph.hasValueInModel(a)
      || !d_inequalityGraph.hasValueInModel(b))
  {
    return EQUALITY_UNKNOWN;
  }

  // TODO: check if this disequality is entailed by inequalities via
  // transitivity

  BitVector a_val = d_inequalityGraph.getValueInModel(a);
  BitVector b_val = d_inequalityGraph.getValueInModel(b);

  if (a_val == b_val)
  {
    return EQUALITY_TRUE_IN_MODEL;
  }
  else
  {
    return EQUALITY_FALSE_IN_MODEL;
  }
}

void InequalitySolver::assertFact(TNode fact) {
  d_assertionQueue.push_back(fact);
  d_assertionSet.insert(fact);
  if (!isInequalityOnly(fact)) {
    d_isComplete = false;
  }
}

bool InequalitySolver::isInequalityOnly(TNode node) {
  if (node.getKind() == kind::NOT) {
    node = node[0];
  }

  if (node.getAttribute(IneqOnlyComputedAttribute())) {
    return node.getAttribute(IneqOnlyAttribute());
  }

  if (node.getKind() != kind::EQUAL &&
      node.getKind() != kind::BITVECTOR_ULT &&
      node.getKind() != kind::BITVECTOR_ULE &&
      node.getKind() != kind::CONST_BITVECTOR &&
      node.getKind() != kind::SELECT &&
      node.getKind() != kind::STORE &&
      node.getMetaKind() != kind::metakind::VARIABLE) {
    // not worth caching
    return false;
  }
  bool res = true;
  for (unsigned i = 0; res && i < node.getNumChildren(); ++i) {
    res = res && isInequalityOnly(node[i]);
  }
  node.setAttribute(IneqOnlyComputedAttribute(), true);
  node.setAttribute(IneqOnlyAttribute(), res);
  return res;
}

void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
  Assert(d_explanations.find(literal) != d_explanations.end());
  TNode explanation = d_explanations[literal];
  assumptions.push_back(explanation);
  Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n";
}

void InequalitySolver::propagate(Theory::Effort e) { Assert(false); }
bool InequalitySolver::collectModelValues(TheoryModel* m,
                                          const std::set<Node>& termSet)
{
  Debug("bitvector-model") << "InequalitySolver::collectModelValues \n";
  std::vector<Node> model;
  d_inequalityGraph.getAllValuesInModel(model);
  for (unsigned i = 0; i < model.size(); ++i) {
    Assert(model[i].getKind() == kind::EQUAL);
    if (!m->assertEquality(model[i][0], model[i][1], true))
    {
      return false;
    }
  }
  return true;
}

Node InequalitySolver::getModelValue(TNode var) {
  Assert(isInequalityOnly(var));
  Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";
  Assert(isComplete());
  Node result = Node();
  if (!d_inequalityGraph.hasValueInModel(var)) {
    Assert(d_bv->isSharedTerm(var));
  } else {
    BitVector val = d_inequalityGraph.getValueInModel(var);
    result = utils::mkConst(val);
  }
  Debug("bitvector-model") << " => " << result <<"\n";
  return result;
}

void InequalitySolver::preRegister(TNode node) {
  Kind kind = node.getKind();
  if (kind == kind::EQUAL ||
      kind == kind::BITVECTOR_ULE ||
      kind == kind::BITVECTOR_ULT) {
    d_ineqTerms.insert(node[0]);
    d_ineqTerms.insert(node[1]);
  }
}

bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact)
{
  bool ok = d_inequalityGraph.addInequality(a, b, strict, fact);
  if (!ok || !strict) return ok;

  Node one = utils::mkConst(utils::getSize(a), 1);
  Node a_plus_one = Rewriter::rewrite(
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, a, one));
  if (d_ineqTerms.find(a_plus_one) != d_ineqTerms.end())
  {
    ok = d_inequalityGraph.addInequality(a_plus_one, b, false, fact);
  }
  return ok;
}

InequalitySolver::Statistics::Statistics()
    : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
        "theory::bv::inequality::NumCallsToCheck")),
      d_solveTime(smtStatisticsRegistry().registerTimer(
          "theory::bv::inequality::SolveTime"))
{
}


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Liana Hadarean, Aina Niemetz, Andrew Reynolds
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Algebraic solver.
14		*/
15
16		#include "theory/bv/bv_subtheory_inequality.h"
17
18		#include "options/smt_options.h"
19		#include "smt/smt_statistics_registry.h"
20		#include "theory/bv/bv_solver_layered.h"
21		#include "theory/bv/theory_bv_utils.h"
22		#include "theory/rewriter.h"
23		#include "theory/theory_model.h"
24
25		using namespace std;
26		using namespace cvc5;
27		using namespace cvc5::context;
28		using namespace cvc5::theory;
29		using namespace cvc5::theory::bv;
30		using namespace cvc5::theory::bv::utils;
31
32		bool InequalitySolver::check(Theory::Effort e) {
33		Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
34		TimerStat::CodeTimer inequalityTimer(d_statistics.d_solveTime);
35		++(d_statistics.d_numCallstoCheck);
36		d_bv->spendResource(Resource::TheoryCheckStep);
37
38		bool ok = true;
39		while (!done() && ok) {
40		TNode fact = get();
41		Debug("bv-subtheory-inequality") << " "<< fact <<"\n";
42		if (fact.getKind() == kind::EQUAL) {
43		TNode a = fact[0];
44		if( a.getType().isBitVector() ){
45		TNode b = fact[1];
46		ok = addInequality(a, b, false, fact);
47		if (ok)
48		ok = addInequality(b, a, false, fact);
49		}
50		} else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
51		TNode a = fact[0][0];
52		if( a.getType().isBitVector() ){
53		TNode b = fact[0][1];
54		ok = d_inequalityGraph.addDisequality(a, b, fact);
55		}
56		}
57		if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
58		TNode a = fact[0][1];
59		TNode b = fact[0][0];
60		ok = addInequality(a, b, true, fact);
61		// propagate
62		// NodeManager *nm = NodeManager::currentNM();
63		// if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
64		// Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, a, b));
65		// d_bv->storePropagation(neq, SUB_INEQUALITY);
66		// d_explanations[neq] = fact;
67		// }
68		} else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
69		TNode a = fact[0][1];
70		TNode b = fact[0][0];
71		ok = addInequality(a, b, false, fact);
72		} else if (fact.getKind() == kind::BITVECTOR_ULT) {
73		TNode a = fact[0];
74		TNode b = fact[1];
75		ok = addInequality(a, b, true, fact);
76		// propagate
77		// if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
78		// Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, a, b));
79		// d_bv->storePropagation(neq, SUB_INEQUALITY);
80		// d_explanations[neq] = fact;
81		// }
82		} else if (fact.getKind() == kind::BITVECTOR_ULE) {
83		TNode a = fact[0];
84		TNode b = fact[1];
85		ok = addInequality(a, b, false, fact);
86		}
87		}
88
89		if (!ok) {
90		std::vector<TNode> conflict;
91		d_inequalityGraph.getConflict(conflict);
92		Node confl = utils::flattenAnd(conflict);
93		d_bv->setConflict(confl);
94		Debug("bv-subtheory-inequality") << "InequalitySolver::conflict: "<< confl <<"\n";
95		return false;
96		}
97
98		if (isComplete() && Theory::fullEffort(e)) {
99		// make sure all the disequalities we didn't split on are still satisifed
100		// and split on the ones that are not
101		std::vector<Node> lemmas;
102		d_inequalityGraph.checkDisequalities(lemmas);
103		for(unsigned i = 0; i < lemmas.size(); ++i) {
104		d_bv->lemma(lemmas[i]);
105		}
106		}
107		Debug("bv-subtheory-inequality") << "InequalitySolver done. ";
108		return true;
109		}
110
111		EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b)
112		{
113		if (!isComplete()) return EQUALITY_UNKNOWN;
114
115		NodeManager* nm = NodeManager::currentNM();
116		Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b);
117		Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a);
118
119		// if an inequality containing the terms has been asserted then we know
120		// the equality is false
121		if (d_assertionSet.contains(a_lt_b) \|\| d_assertionSet.contains(b_lt_a))
122		{
123		return EQUALITY_FALSE;
124		}
125
126		if (!d_inequalityGraph.hasValueInModel(a)
127		\|\| !d_inequalityGraph.hasValueInModel(b))
128		{
129		return EQUALITY_UNKNOWN;
130		}
131
132		// TODO: check if this disequality is entailed by inequalities via
133		// transitivity
134
135		BitVector a_val = d_inequalityGraph.getValueInModel(a);
136		BitVector b_val = d_inequalityGraph.getValueInModel(b);
137
138		if (a_val == b_val)
139		{
140		return EQUALITY_TRUE_IN_MODEL;
141		}
142		else
143		{
144		return EQUALITY_FALSE_IN_MODEL;
145		}
146		}
147
148		void InequalitySolver::assertFact(TNode fact) {
149		d_assertionQueue.push_back(fact);
150		d_assertionSet.insert(fact);
151		if (!isInequalityOnly(fact)) {
152		d_isComplete = false;
153		}
154		}
155
156		bool InequalitySolver::isInequalityOnly(TNode node) {
157		if (node.getKind() == kind::NOT) {
158		node = node[0];
159		}
160
161		if (node.getAttribute(IneqOnlyComputedAttribute())) {
162		return node.getAttribute(IneqOnlyAttribute());
163		}
164
165		if (node.getKind() != kind::EQUAL &&
166		node.getKind() != kind::BITVECTOR_ULT &&
167		node.getKind() != kind::BITVECTOR_ULE &&
168		node.getKind() != kind::CONST_BITVECTOR &&
169		node.getKind() != kind::SELECT &&
170		node.getKind() != kind::STORE &&
171		node.getMetaKind() != kind::metakind::VARIABLE) {
172		// not worth caching
173		return false;
174		}
175		bool res = true;
176		for (unsigned i = 0; res && i < node.getNumChildren(); ++i) {
177		res = res && isInequalityOnly(node[i]);
178		}
179		node.setAttribute(IneqOnlyComputedAttribute(), true);
180		node.setAttribute(IneqOnlyAttribute(), res);
181		return res;
182		}
183
184		void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
185		Assert(d_explanations.find(literal) != d_explanations.end());
186		TNode explanation = d_explanations[literal];
187		assumptions.push_back(explanation);
188		Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n";
189		}
190
191		void InequalitySolver::propagate(Theory::Effort e) { Assert(false); }
192		bool InequalitySolver::collectModelValues(TheoryModel* m,
193		const std::set<Node>& termSet)
194		{
195		Debug("bitvector-model") << "InequalitySolver::collectModelValues \n";
196		std::vector<Node> model;
197		d_inequalityGraph.getAllValuesInModel(model);
198		for (unsigned i = 0; i < model.size(); ++i) {
199		Assert(model[i].getKind() == kind::EQUAL);
200		if (!m->assertEquality(model[i][0], model[i][1], true))
201		{
202		return false;
203		}
204		}
205		return true;
206		}
207
208		Node InequalitySolver::getModelValue(TNode var) {
209		Assert(isInequalityOnly(var));
210		Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";
211		Assert(isComplete());
212		Node result = Node();
213		if (!d_inequalityGraph.hasValueInModel(var)) {
214		Assert(d_bv->isSharedTerm(var));
215		} else {
216		BitVector val = d_inequalityGraph.getValueInModel(var);
217		result = utils::mkConst(val);
218		}
219		Debug("bitvector-model") << " => " << result <<"\n";
220		return result;
221		}
222
223		void InequalitySolver::preRegister(TNode node) {
224		Kind kind = node.getKind();
225		if (kind == kind::EQUAL \|\|
226		kind == kind::BITVECTOR_ULE \|\|
227		kind == kind::BITVECTOR_ULT) {
228		d_ineqTerms.insert(node[0]);
229		d_ineqTerms.insert(node[1]);
230		}
231		}
232
233		bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact)
234		{
235		bool ok = d_inequalityGraph.addInequality(a, b, strict, fact);
236		if (!ok \|\| !strict) return ok;
237
238		Node one = utils::mkConst(utils::getSize(a), 1);
239		Node a_plus_one = Rewriter::rewrite(
240		NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, a, one));
241		if (d_ineqTerms.find(a_plus_one) != d_ineqTerms.end())
242		{
243		ok = d_inequalityGraph.addInequality(a_plus_one, b, false, fact);
244		}
245		return ok;
246		}
247
248		InequalitySolver::Statistics::Statistics()
249		: d_numCallstoCheck(smtStatisticsRegistry().registerInt(
250		"theory::bv::inequality::NumCallsToCheck")),
251		d_solveTime(smtStatisticsRegistry().registerTimer(
252		"theory::bv::inequality::SolveTime"))
253		{
254	29340	}