Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_subtheory_core.cpp	Lines:	27	198	13.6 %
Date:	2021-09-15	Branches:	11	727	1.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Liana Hadarean, Aina Niemetz
 *
 * 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_core.h"

#include "expr/skolem_manager.h"
#include "options/bv_options.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/ext_theory.h"
#include "theory/theory_model.h"
#include "util/rational.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;

CoreSolver::CoreSolver(context::Context* c, BVSolverLayered* bv)
    : SubtheorySolver(c, bv),
      d_notify(*this),
      d_isComplete(c, true),
      d_lemmaThreshold(16),
      d_preregisterCalled(false),
      d_checkCalled(false),
      d_bv(bv),
      d_reasons(c)
{
}

CoreSolver::~CoreSolver() {}

bool CoreSolver::needsEqualityEngine(EeSetupInfo& esi)
{
  esi.d_notify = &d_notify;
  esi.d_name = "theory::bv::ee";
  return true;
}

void CoreSolver::finishInit()
{
  // use the parent's equality engine, which may be the one we allocated above
  d_equalityEngine = d_bv->d_bv.getEqualityEngine();

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

void CoreSolver::preRegister(TNode node) {
  d_preregisterCalled = true;
  if (node.getKind() == kind::EQUAL) {
    d_equalityEngine->addTriggerPredicate(node);
  } else {
    d_equalityEngine->addTerm(node);
  }
}


void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
  bool polarity = literal.getKind() != kind::NOT;
  TNode atom = polarity ? literal : literal[0];
  if (atom.getKind() == kind::EQUAL) {
    d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
  } else {
    d_equalityEngine->explainPredicate(atom, polarity, assumptions);
  }
}

bool CoreSolver::check(Theory::Effort e) {
  Trace("bitvector::core") << "CoreSolver::check \n";

  d_bv->d_im.spendResource(Resource::TheoryCheckStep);

  d_checkCalled = true;
  Assert(!d_bv->inConflict());
  ++(d_statistics.d_numCallstoCheck);
  bool ok = true;
  std::vector<Node> core_eqs;
  TNodeBoolMap seen;
  while (! done()) {
    TNode fact = get();
    if (d_isComplete && !isCompleteForTerm(fact, seen)) {
      d_isComplete = false;
    }

    // only reason about equalities
    if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
      ok = assertFactToEqualityEngine(fact, fact);
    } else {
      ok = assertFactToEqualityEngine(fact, fact);
    }
    if (!ok)
      return false;
  }

  if (Theory::fullEffort(e) && isComplete()) {
    buildModel();
  }

  return true;
}

void CoreSolver::buildModel()
{
  Debug("bv-core") << "CoreSolver::buildModel() \n";
  NodeManager* nm = NodeManager::currentNM();
  d_modelValues.clear();
  TNodeSet constants;
  TNodeSet constants_in_eq_engine;
  // collect constants in equality engine
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
  while (!eqcs_i.isFinished())
  {
    TNode repr = *eqcs_i;
    if (repr.getKind() == kind::CONST_BITVECTOR)
    {
      // must check if it's just the constant
      eq::EqClassIterator it(repr, d_equalityEngine);
      if (!(++it).isFinished() || true)
      {
        constants.insert(repr);
        constants_in_eq_engine.insert(repr);
      }
    }
    ++eqcs_i;
  }

  // build repr to value map

  eqcs_i = eq::EqClassesIterator(d_equalityEngine);
  while (!eqcs_i.isFinished())
  {
    TNode repr = *eqcs_i;
    ++eqcs_i;

    if (!repr.isVar() && repr.getKind() != kind::CONST_BITVECTOR
        && !d_bv->isSharedTerm(repr))
    {
      continue;
    }

    TypeNode type = repr.getType();
    if (type.isBitVector() && repr.getKind() != kind::CONST_BITVECTOR)
    {
      Debug("bv-core-model") << "   processing " << repr << "\n";
      // we need to assign a value for it
      TypeEnumerator te(type);
      Node val;
      do
      {
        val = *te;
        ++te;
        // Debug("bv-core-model") << "  trying value " << val << "\n";
        // Debug("bv-core-model") << "  is in set? " << constants.count(val) <<
        // "\n"; Debug("bv-core-model") << "  enumerator done? " <<
        // te.isFinished() << "\n";
      } while (constants.count(val) != 0 && !(te.isFinished()));

      if (te.isFinished() && constants.count(val) != 0)
      {
        // if we cannot enumerate anymore values we just return the lemma
        // stating that at least two of the representatives are equal.
        std::vector<TNode> representatives;
        representatives.push_back(repr);

        for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
             it != constants_in_eq_engine.end();
             ++it)
        {
          TNode constant = *it;
          if (utils::getSize(constant) == utils::getSize(repr))
          {
            representatives.push_back(constant);
          }
        }
        for (ModelValue::const_iterator it = d_modelValues.begin();
             it != d_modelValues.end();
             ++it)
        {
          representatives.push_back(it->first);
        }
        std::vector<Node> equalities;
        for (unsigned i = 0; i < representatives.size(); ++i)
        {
          for (unsigned j = i + 1; j < representatives.size(); ++j)
          {
            TNode a = representatives[i];
            TNode b = representatives[j];
            if (a.getKind() == kind::CONST_BITVECTOR
                && b.getKind() == kind::CONST_BITVECTOR)
            {
              Assert(a != b);
              continue;
            }
            if (utils::getSize(a) == utils::getSize(b))
            {
              equalities.push_back(nm->mkNode(kind::EQUAL, a, b));
            }
          }
        }
        // better off letting the SAT solver split on values
        if (equalities.size() > d_lemmaThreshold)
        {
          d_isComplete = false;
          return;
        }

        if (equalities.size() == 0)
        {
          Debug("bv-core") << "  lemma: true (no equalities)" << std::endl;
        }
        else
        {
          Node lemma = utils::mkOr(equalities);
          d_bv->lemma(lemma);
          Debug("bv-core") << "  lemma: " << lemma << std::endl;
        }
        return;
      }

      Debug("bv-core-model") << "   " << repr << " => " << val << "\n";
      constants.insert(val);
      d_modelValues[repr] = val;
    }
  }
}

bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
  // Notify the equality engine
  if (!d_bv->inConflict()
      && (!d_bv->wasPropagatedBySubtheory(fact)
          || d_bv->getPropagatingSubtheory(fact) != SUB_CORE))
  {
    Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
    // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
    bool negated = fact.getKind() == kind::NOT;
    TNode predicate = negated ? fact[0] : fact;
    if (predicate.getKind() == kind::EQUAL) {
      if (negated) {
        // dis-equality
        d_equalityEngine->assertEquality(predicate, false, reason);
      } else {
        // equality
        d_equalityEngine->assertEquality(predicate, true, reason);
      }
    } else {
      // Adding predicate if the congruence over it is turned on
      if (d_equalityEngine->isFunctionKind(predicate.getKind()))
      {
        d_equalityEngine->assertPredicate(predicate, !negated, reason);
      }
    }
  }

  // checking for a conflict
  if (d_bv->inConflict())
  {
    return false;
  }
  return true;
}

bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
  Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
  if (value) {
    return d_solver.storePropagation(predicate);
  }
  return d_solver.storePropagation(predicate.notNode());
}

bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
  if (value) {
    return d_solver.storePropagation(t1.eqNode(t2));
  } else {
    return d_solver.storePropagation(t1.eqNode(t2).notNode());
  }
}

void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  d_solver.conflict(t1, t2);
}

bool CoreSolver::storePropagation(TNode literal) {
  return d_bv->storePropagation(literal, SUB_CORE);
}

void CoreSolver::conflict(TNode a, TNode b) {
  std::vector<TNode> assumptions;
  d_equalityEngine->explainEquality(a, b, true, assumptions);
  Node conflict = flattenAnd(assumptions);
  d_bv->setConflict(conflict);
}

bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
  return utils::isEqualityTerm(term, seen);
}

bool CoreSolver::collectModelValues(TheoryModel* m,
                                    const std::set<Node>& termSet)
{
  if (Debug.isOn("bitvector-model")) {
    context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
    for (; it!= d_assertionQueue.end(); ++it) {
      Debug("bitvector-model")
          << "CoreSolver::collectModelValues (assert " << *it << ")\n";
    }
  }
  if (isComplete()) {
    Debug("bitvector-model") << "CoreSolver::collectModelValues complete.";
    for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
      Node a = it->first;
      Node b = it->second;
      Debug("bitvector-model") << "CoreSolver::collectModelValues modelValues "
                               << a << " => " << b << ")\n";
      if (!m->assertEquality(a, b, true))
      {
        return false;
      }
    }
  }
  return true;
}

Node CoreSolver::getModelValue(TNode var) {
  Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
  Assert(isComplete());
  TNode repr = d_equalityEngine->getRepresentative(var);
  Node result = Node();
  if (repr.getKind() == kind::CONST_BITVECTOR) {
    result = repr;
  } else if (d_modelValues.find(repr) == d_modelValues.end()) {
    // it may be a shared term that never gets asserted
    // result is just Null
    Assert(d_bv->isSharedTerm(var));
  } else {
    result = d_modelValues[repr];
  }
  Debug("bitvector-model") << " => " << result <<"\n";
  return result;
}

EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b)
{
  if (d_equalityEngine->areEqual(a, b))
  {
    // The terms are implied to be equal
    return EQUALITY_TRUE;
  }
  if (d_equalityEngine->areDisequal(a, b, false))
  {
    // The terms are implied to be dis-equal
    return EQUALITY_FALSE;
  }
  return EQUALITY_UNKNOWN;
}

bool CoreSolver::hasTerm(TNode node) const
{
  return d_equalityEngine->hasTerm(node);
}
void CoreSolver::addTermToEqualityEngine(TNode node)
{
  d_equalityEngine->addTerm(node);
}

CoreSolver::Statistics::Statistics()
    : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
        "theory::bv::CoreSolver::NumCallsToCheck"))
{
}


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Liana Hadarean, Aina Niemetz
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_core.h"
17
18		#include "expr/skolem_manager.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_layered.h"
23		#include "theory/bv/theory_bv_utils.h"
24		#include "theory/ext_theory.h"
25		#include "theory/theory_model.h"
26		#include "util/rational.h"
27
28		using namespace std;
29		using namespace cvc5;
30		using namespace cvc5::context;
31		using namespace cvc5::theory;
32		using namespace cvc5::theory::bv;
33		using namespace cvc5::theory::bv::utils;
34
35	2	CoreSolver::CoreSolver(context::Context* c, BVSolverLayered* bv)
36		: SubtheorySolver(c, bv),
37		d_notify(*this),
38		d_isComplete(c, true),
39		d_lemmaThreshold(16),
40		d_preregisterCalled(false),
41		d_checkCalled(false),
42		d_bv(bv),
43	2	d_reasons(c)
44		{
45	2	}
46
47	4	CoreSolver::~CoreSolver() {}
48
49	2	bool CoreSolver::needsEqualityEngine(EeSetupInfo& esi)
50		{
51	2	esi.d_notify = &d_notify;
52	2	esi.d_name = "theory::bv::ee";
53	2	return true;
54		}
55
56	2	void CoreSolver::finishInit()
57		{
58		// use the parent's equality engine, which may be the one we allocated above
59	2	d_equalityEngine = d_bv->d_bv.getEqualityEngine();
60
61		// The kinds we are treating as function application in congruence
62	2	d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true);
63		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_AND);
64		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_OR);
65		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_XOR);
66		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOT);
67		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_NAND);
68		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOR);
69		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR);
70		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP);
71	2	d_equalityEngine->addFunctionKind(kind::BITVECTOR_MULT, true);
72	2	d_equalityEngine->addFunctionKind(kind::BITVECTOR_ADD, true);
73	2	d_equalityEngine->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
74		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB);
75		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG);
76		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_UDIV);
77		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_UREM);
78		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SDIV);
79		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SREM);
80		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SMOD);
81		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SHL);
82		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_LSHR);
83		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_ASHR);
84		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULT);
85		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULE);
86		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGT);
87		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGE);
88		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLT);
89		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLE);
90		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGT);
91		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGE);
92	2	d_equalityEngine->addFunctionKind(kind::BITVECTOR_TO_NAT);
93	2	d_equalityEngine->addFunctionKind(kind::INT_TO_BITVECTOR);
94	2	}
95
96	28	void CoreSolver::preRegister(TNode node) {
97	28	d_preregisterCalled = true;
98	28	if (node.getKind() == kind::EQUAL) {
99	10	d_equalityEngine->addTriggerPredicate(node);
100		} else {
101	18	d_equalityEngine->addTerm(node);
102		}
103	28	}
104
105
106		void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
107		bool polarity = literal.getKind() != kind::NOT;
108		TNode atom = polarity ? literal : literal[0];
109		if (atom.getKind() == kind::EQUAL) {
110		d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
111		} else {
112		d_equalityEngine->explainPredicate(atom, polarity, assumptions);
113		}
114		}
115
116		bool CoreSolver::check(Theory::Effort e) {
117		Trace("bitvector::core") << "CoreSolver::check \n";
118
119		d_bv->d_im.spendResource(Resource::TheoryCheckStep);
120
121		d_checkCalled = true;
122		Assert(!d_bv->inConflict());
123		++(d_statistics.d_numCallstoCheck);
124		bool ok = true;
125		std::vector<Node> core_eqs;
126		TNodeBoolMap seen;
127		while (! done()) {
128		TNode fact = get();
129		if (d_isComplete && !isCompleteForTerm(fact, seen)) {
130		d_isComplete = false;
131		}
132
133		// only reason about equalities
134		if (fact.getKind() == kind::EQUAL \|\| (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
135		ok = assertFactToEqualityEngine(fact, fact);
136		} else {
137		ok = assertFactToEqualityEngine(fact, fact);
138		}
139		if (!ok)
140		return false;
141		}
142
143		if (Theory::fullEffort(e) && isComplete()) {
144		buildModel();
145		}
146
147		return true;
148		}
149
150		void CoreSolver::buildModel()
151		{
152		Debug("bv-core") << "CoreSolver::buildModel() \n";
153		NodeManager* nm = NodeManager::currentNM();
154		d_modelValues.clear();
155		TNodeSet constants;
156		TNodeSet constants_in_eq_engine;
157		// collect constants in equality engine
158		eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
159		while (!eqcs_i.isFinished())
160		{
161		TNode repr = *eqcs_i;
162		if (repr.getKind() == kind::CONST_BITVECTOR)
163		{
164		// must check if it's just the constant
165		eq::EqClassIterator it(repr, d_equalityEngine);
166		if (!(++it).isFinished() \|\| true)
167		{
168		constants.insert(repr);
169		constants_in_eq_engine.insert(repr);
170		}
171		}
172		++eqcs_i;
173		}
174
175		// build repr to value map
176
177		eqcs_i = eq::EqClassesIterator(d_equalityEngine);
178		while (!eqcs_i.isFinished())
179		{
180		TNode repr = *eqcs_i;
181		++eqcs_i;
182
183		if (!repr.isVar() && repr.getKind() != kind::CONST_BITVECTOR
184		&& !d_bv->isSharedTerm(repr))
185		{
186		continue;
187		}
188
189		TypeNode type = repr.getType();
190		if (type.isBitVector() && repr.getKind() != kind::CONST_BITVECTOR)
191		{
192		Debug("bv-core-model") << " processing " << repr << "\n";
193		// we need to assign a value for it
194		TypeEnumerator te(type);
195		Node val;
196		do
197		{
198		val = *te;
199		++te;
200		// Debug("bv-core-model") << " trying value " << val << "\n";
201		// Debug("bv-core-model") << " is in set? " << constants.count(val) <<
202		// "\n"; Debug("bv-core-model") << " enumerator done? " <<
203		// te.isFinished() << "\n";
204		} while (constants.count(val) != 0 && !(te.isFinished()));
205
206		if (te.isFinished() && constants.count(val) != 0)
207		{
208		// if we cannot enumerate anymore values we just return the lemma
209		// stating that at least two of the representatives are equal.
210		std::vector<TNode> representatives;
211		representatives.push_back(repr);
212
213		for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
214		it != constants_in_eq_engine.end();
215		++it)
216		{
217		TNode constant = *it;
218		if (utils::getSize(constant) == utils::getSize(repr))
219		{
220		representatives.push_back(constant);
221		}
222		}
223		for (ModelValue::const_iterator it = d_modelValues.begin();
224		it != d_modelValues.end();
225		++it)
226		{
227		representatives.push_back(it->first);
228		}
229		std::vector<Node> equalities;
230		for (unsigned i = 0; i < representatives.size(); ++i)
231		{
232		for (unsigned j = i + 1; j < representatives.size(); ++j)
233		{
234		TNode a = representatives[i];
235		TNode b = representatives[j];
236		if (a.getKind() == kind::CONST_BITVECTOR
237		&& b.getKind() == kind::CONST_BITVECTOR)
238		{
239		Assert(a != b);
240		continue;
241		}
242		if (utils::getSize(a) == utils::getSize(b))
243		{
244		equalities.push_back(nm->mkNode(kind::EQUAL, a, b));
245		}
246		}
247		}
248		// better off letting the SAT solver split on values
249		if (equalities.size() > d_lemmaThreshold)
250		{
251		d_isComplete = false;
252		return;
253		}
254
255		if (equalities.size() == 0)
256		{
257		Debug("bv-core") << " lemma: true (no equalities)" << std::endl;
258		}
259		else
260		{
261		Node lemma = utils::mkOr(equalities);
262		d_bv->lemma(lemma);
263		Debug("bv-core") << " lemma: " << lemma << std::endl;
264		}
265		return;
266		}
267
268		Debug("bv-core-model") << " " << repr << " => " << val << "\n";
269		constants.insert(val);
270		d_modelValues[repr] = val;
271		}
272		}
273		}
274
275		bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
276		// Notify the equality engine
277		if (!d_bv->inConflict()
278		&& (!d_bv->wasPropagatedBySubtheory(fact)
279		\|\| d_bv->getPropagatingSubtheory(fact) != SUB_CORE))
280		{
281		Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
282		// Debug("bv-slicer-eq") << " reason=" << reason << endl;
283		bool negated = fact.getKind() == kind::NOT;
284		TNode predicate = negated ? fact[0] : fact;
285		if (predicate.getKind() == kind::EQUAL) {
286		if (negated) {
287		// dis-equality
288		d_equalityEngine->assertEquality(predicate, false, reason);
289		} else {
290		// equality
291		d_equalityEngine->assertEquality(predicate, true, reason);
292		}
293		} else {
294		// Adding predicate if the congruence over it is turned on
295		if (d_equalityEngine->isFunctionKind(predicate.getKind()))
296		{
297		d_equalityEngine->assertPredicate(predicate, !negated, reason);
298		}
299		}
300		}
301
302		// checking for a conflict
303		if (d_bv->inConflict())
304		{
305		return false;
306		}
307		return true;
308		}
309
310		bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
311		Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
312		if (value) {
313		return d_solver.storePropagation(predicate);
314		}
315		return d_solver.storePropagation(predicate.notNode());
316		}
317
318		bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
319		Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
320		if (value) {
321		return d_solver.storePropagation(t1.eqNode(t2));
322		} else {
323		return d_solver.storePropagation(t1.eqNode(t2).notNode());
324		}
325		}
326
327		void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
328		d_solver.conflict(t1, t2);
329		}
330
331		bool CoreSolver::storePropagation(TNode literal) {
332		return d_bv->storePropagation(literal, SUB_CORE);
333		}
334
335		void CoreSolver::conflict(TNode a, TNode b) {
336		std::vector<TNode> assumptions;
337		d_equalityEngine->explainEquality(a, b, true, assumptions);
338		Node conflict = flattenAnd(assumptions);
339		d_bv->setConflict(conflict);
340		}
341
342		bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
343		return utils::isEqualityTerm(term, seen);
344		}
345
346		bool CoreSolver::collectModelValues(TheoryModel* m,
347		const std::set<Node>& termSet)
348		{
349		if (Debug.isOn("bitvector-model")) {
350		context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
351		for (; it!= d_assertionQueue.end(); ++it) {
352		Debug("bitvector-model")
353		<< "CoreSolver::collectModelValues (assert " << *it << ")\n";
354		}
355		}
356		if (isComplete()) {
357		Debug("bitvector-model") << "CoreSolver::collectModelValues complete.";
358		for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
359		Node a = it->first;
360		Node b = it->second;
361		Debug("bitvector-model") << "CoreSolver::collectModelValues modelValues "
362		<< a << " => " << b << ")\n";
363		if (!m->assertEquality(a, b, true))
364		{
365		return false;
366		}
367		}
368		}
369		return true;
370		}
371
372		Node CoreSolver::getModelValue(TNode var) {
373		Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
374		Assert(isComplete());
375		TNode repr = d_equalityEngine->getRepresentative(var);
376		Node result = Node();
377		if (repr.getKind() == kind::CONST_BITVECTOR) {
378		result = repr;
379		} else if (d_modelValues.find(repr) == d_modelValues.end()) {
380		// it may be a shared term that never gets asserted
381		// result is just Null
382		Assert(d_bv->isSharedTerm(var));
383		} else {
384		result = d_modelValues[repr];
385		}
386		Debug("bitvector-model") << " => " << result <<"\n";
387		return result;
388		}
389
390		EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b)
391		{
392		if (d_equalityEngine->areEqual(a, b))
393		{
394		// The terms are implied to be equal
395		return EQUALITY_TRUE;
396		}
397		if (d_equalityEngine->areDisequal(a, b, false))
398		{
399		// The terms are implied to be dis-equal
400		return EQUALITY_FALSE;
401		}
402		return EQUALITY_UNKNOWN;
403		}
404
405		bool CoreSolver::hasTerm(TNode node) const
406		{
407		return d_equalityEngine->hasTerm(node);
408		}
409		void CoreSolver::addTermToEqualityEngine(TNode node)
410		{
411		d_equalityEngine->addTerm(node);
412		}
413
414	2	CoreSolver::Statistics::Statistics()
415	2	: d_numCallstoCheck(smtStatisticsRegistry().registerInt(
416	2	"theory::bv::CoreSolver::NumCallsToCheck"))
417		{
418	29579	}