Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_subtheory_core.cpp	Lines:	263	308	85.4 %
Date:	2021-05-22	Branches:	538	1187	45.3 %


/******************************************************************************
 * 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_lazy.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/ext_theory.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 CoreSolverExtTheoryCallback::getCurrentSubstitution(
    int effort,
    const std::vector<Node>& vars,
    std::vector<Node>& subs,
    std::map<Node, std::vector<Node> >& exp)
{
  if (d_equalityEngine == nullptr)
  {
    return false;
  }
  // get the constant equivalence classes
  bool retVal = false;
  for (const Node& n : vars)
  {
    if (d_equalityEngine->hasTerm(n))
    {
      Node nr = d_equalityEngine->getRepresentative(n);
      if (nr.isConst())
      {
        subs.push_back(nr);
        exp[n].push_back(n.eqNode(nr));
        retVal = true;
      }
      else
      {
        subs.push_back(n);
      }
    }
    else
    {
      subs.push_back(n);
    }
  }
  // return true if the substitution is non-trivial
  return retVal;
}

bool CoreSolverExtTheoryCallback::getReduction(int effort,
                                               Node n,
                                               Node& nr,
                                               bool& satDep)
{
  Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
  if (n.getKind() == kind::BITVECTOR_TO_NAT)
  {
    nr = utils::eliminateBv2Nat(n);
    satDep = false;
    return true;
  }
  else if (n.getKind() == kind::INT_TO_BITVECTOR)
  {
    nr = utils::eliminateInt2Bv(n);
    satDep = false;
    return true;
  }
  return false;
}

CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
    : SubtheorySolver(c, bv),
      d_notify(*this),
      d_isComplete(c, true),
      d_lemmaThreshold(16),
      d_preregisterCalled(false),
      d_checkCalled(false),
      d_bv(bv),
      d_extTheoryCb(),
      d_extTheory(new ExtTheory(d_extTheoryCb,
                                bv->d_bv.getSatContext(),
                                bv->d_bv.getUserContext(),
                                bv->d_bv.getOutputChannel())),
      d_reasons(c),
      d_needsLastCallCheck(false),
      d_extf_range_infer(bv->d_bv.getUserContext()),
      d_extf_collapse_infer(bv->d_bv.getUserContext())
{
  d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
  d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
}

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);
    // Register with the extended theory, for context-dependent simplification.
    // Notice we do this for registered terms but not internally generated
    // equivalence classes. The two should roughly cooincide. Since ExtTheory is
    // being used as a heuristic, it is good enough to be registered here.
    d_extTheory->registerTerm(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"))
{
}

void CoreSolver::checkExtf(Theory::Effort e)
{
  if (e == Theory::EFFORT_LAST_CALL)
  {
    std::vector<Node> nred = d_extTheory->getActive();
    doExtfReductions(nred);
  }
  Assert(e == Theory::EFFORT_FULL);
  // do inferences (adds external lemmas)  TODO: this can be improved to add
  // internal inferences
  std::vector<Node> nred;
  if (d_extTheory->doInferences(0, nred))
  {
    return;
  }
  d_needsLastCallCheck = false;
  if (!nred.empty())
  {
    // other inferences involving bv2nat, int2bv
    if (options::bvAlgExtf())
    {
      if (doExtfInferences(nred))
      {
        return;
      }
    }
    if (!options::bvLazyReduceExtf())
    {
      if (doExtfReductions(nred))
      {
        return;
      }
    }
    else
    {
      d_needsLastCallCheck = true;
    }
  }
}

bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; }

bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  bool sentLemma = false;
  eq::EqualityEngine* ee = d_equalityEngine;
  std::map<Node, Node> op_map;
  for (unsigned j = 0; j < terms.size(); j++)
  {
    TNode n = terms[j];
    Assert(n.getKind() == kind::BITVECTOR_TO_NAT
           || n.getKind() == kind::INT_TO_BITVECTOR);
    if (n.getKind() == kind::BITVECTOR_TO_NAT)
    {
      // range lemmas
      if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
      {
        d_extf_range_infer.insert(n);
        unsigned bvs = n[0].getType().getBitVectorSize();
        Node min = nm->mkConst(Rational(0));
        Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
        Node lem = nm->mkNode(kind::AND,
                              nm->mkNode(kind::GEQ, n, min),
                              nm->mkNode(kind::LT, n, max));
        Trace("bv-extf-lemma")
            << "BV extf lemma (range) : " << lem << std::endl;
        d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_LEMMA);
        sentLemma = true;
      }
    }
    Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
    op_map[r] = n;
  }
  for (unsigned j = 0; j < terms.size(); j++)
  {
    TNode n = terms[j];
    Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
    std::map<Node, Node>::iterator it = op_map.find(r);
    if (it != op_map.end())
    {
      Node parent = it->second;
      // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
      // n );
      Node cterm = parent[0].eqNode(n);
      Trace("bv-extf-lemma-debug")
          << "BV extf collapse based on : " << cterm << std::endl;
      if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
      {
        d_extf_collapse_infer.insert(cterm);

        Node t = n[0];
        if (t.getType() == parent.getType())
        {
          if (n.getKind() == kind::INT_TO_BITVECTOR)
          {
            Assert(t.getType().isInteger());
            // congruent modulo 2^( bv width )
            unsigned bvs = n.getType().getBitVectorSize();
            Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
            Node k = sm->mkDummySkolem(
                "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
            t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
          }
          Node lem = parent.eqNode(t);

          if (parent[0] != n)
          {
            Assert(ee->areEqual(parent[0], n));
            lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
          }
          // this handles inferences of the form, e.g.:
          //   ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
          //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
          Trace("bv-extf-lemma")
              << "BV extf lemma (collapse) : " << lem << std::endl;
          d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_COLLAPSE);
          sentLemma = true;
        }
      }
      Trace("bv-extf-lemma-debug")
          << "BV extf f collapse based on : " << cterm << std::endl;
    }
  }
  return sentLemma;
}

bool CoreSolver::doExtfReductions(std::vector<Node>& terms)
{
  std::vector<Node> nredr;
  if (d_extTheory->doReductions(0, terms, nredr))
  {
    return true;
  }
  Assert(nredr.empty());
  return false;
}


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_lazy.h"
23		#include "theory/bv/theory_bv_utils.h"
24		#include "theory/ext_theory.h"
25		#include "theory/theory_model.h"
26
27		using namespace std;
28		using namespace cvc5;
29		using namespace cvc5::context;
30		using namespace cvc5::theory;
31		using namespace cvc5::theory::bv;
32		using namespace cvc5::theory::bv::utils;
33
34	127	bool CoreSolverExtTheoryCallback::getCurrentSubstitution(
35		int effort,
36		const std::vector<Node>& vars,
37		std::vector<Node>& subs,
38		std::map<Node, std::vector<Node> >& exp)
39		{
40	127	if (d_equalityEngine == nullptr)
41		{
42	127	return false;
43		}
44		// get the constant equivalence classes
45		bool retVal = false;
46		for (const Node& n : vars)
47		{
48		if (d_equalityEngine->hasTerm(n))
49		{
50		Node nr = d_equalityEngine->getRepresentative(n);
51		if (nr.isConst())
52		{
53		subs.push_back(nr);
54		exp[n].push_back(n.eqNode(nr));
55		retVal = true;
56		}
57		else
58		{
59		subs.push_back(n);
60		}
61		}
62		else
63		{
64		subs.push_back(n);
65		}
66		}
67		// return true if the substitution is non-trivial
68		return retVal;
69		}
70
71	174	bool CoreSolverExtTheoryCallback::getReduction(int effort,
72		Node n,
73		Node& nr,
74		bool& satDep)
75		{
76	174	Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
77	174	if (n.getKind() == kind::BITVECTOR_TO_NAT)
78		{
79	93	nr = utils::eliminateBv2Nat(n);
80	93	satDep = false;
81	93	return true;
82		}
83	81	else if (n.getKind() == kind::INT_TO_BITVECTOR)
84		{
85	81	nr = utils::eliminateInt2Bv(n);
86	81	satDep = false;
87	81	return true;
88		}
89		return false;
90		}
91
92	9403	CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
93		: SubtheorySolver(c, bv),
94		d_notify(*this),
95		d_isComplete(c, true),
96		d_lemmaThreshold(16),
97		d_preregisterCalled(false),
98		d_checkCalled(false),
99		d_bv(bv),
100		d_extTheoryCb(),
101		d_extTheory(new ExtTheory(d_extTheoryCb,
102	9403	bv->d_bv.getSatContext(),
103	9403	bv->d_bv.getUserContext(),
104	18806	bv->d_bv.getOutputChannel())),
105		d_reasons(c),
106		d_needsLastCallCheck(false),
107	9403	d_extf_range_infer(bv->d_bv.getUserContext()),
108	37612	d_extf_collapse_infer(bv->d_bv.getUserContext())
109		{
110	9403	d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
111	9403	d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
112	9403	}
113
114	18806	CoreSolver::~CoreSolver() {}
115
116	9403	bool CoreSolver::needsEqualityEngine(EeSetupInfo& esi)
117		{
118	9403	esi.d_notify = &d_notify;
119	9403	esi.d_name = "theory::bv::ee";
120	9403	return true;
121		}
122
123	9403	void CoreSolver::finishInit()
124		{
125		// use the parent's equality engine, which may be the one we allocated above
126	9403	d_equalityEngine = d_bv->d_bv.getEqualityEngine();
127
128		// The kinds we are treating as function application in congruence
129	9403	d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true);
130		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_AND);
131		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_OR);
132		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_XOR);
133		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOT);
134		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_NAND);
135		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOR);
136		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR);
137		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP);
138	9403	d_equalityEngine->addFunctionKind(kind::BITVECTOR_MULT, true);
139	9403	d_equalityEngine->addFunctionKind(kind::BITVECTOR_ADD, true);
140	9403	d_equalityEngine->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
141		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB);
142		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG);
143		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_UDIV);
144		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_UREM);
145		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SDIV);
146		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SREM);
147		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SMOD);
148		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SHL);
149		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_LSHR);
150		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_ASHR);
151		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULT);
152		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULE);
153		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGT);
154		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGE);
155		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLT);
156		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLE);
157		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGT);
158		// d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGE);
159	9403	d_equalityEngine->addFunctionKind(kind::BITVECTOR_TO_NAT);
160	9403	d_equalityEngine->addFunctionKind(kind::INT_TO_BITVECTOR);
161	9403	}
162
163	221279	void CoreSolver::preRegister(TNode node) {
164	221279	d_preregisterCalled = true;
165	221279	if (node.getKind() == kind::EQUAL) {
166	54604	d_equalityEngine->addTriggerPredicate(node);
167		} else {
168	166675	d_equalityEngine->addTerm(node);
169		// Register with the extended theory, for context-dependent simplification.
170		// Notice we do this for registered terms but not internally generated
171		// equivalence classes. The two should roughly cooincide. Since ExtTheory is
172		// being used as a heuristic, it is good enough to be registered here.
173	166675	d_extTheory->registerTerm(node);
174		}
175	221279	}
176
177
178	3551	void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
179	3551	bool polarity = literal.getKind() != kind::NOT;
180	7102	TNode atom = polarity ? literal : literal[0];
181	3551	if (atom.getKind() == kind::EQUAL) {
182	3551	d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
183		} else {
184		d_equalityEngine->explainPredicate(atom, polarity, assumptions);
185		}
186	3551	}
187
188	238193	bool CoreSolver::check(Theory::Effort e) {
189	238193	Trace("bitvector::core") << "CoreSolver::check \n";
190
191	238193	d_bv->d_im.spendResource(Resource::TheoryCheckStep);
192
193	238193	d_checkCalled = true;
194	238193	Assert(!d_bv->inConflict());
195	238193	++(d_statistics.d_numCallstoCheck);
196	238193	bool ok = true;
197	476386	std::vector<Node> core_eqs;
198	476386	TNodeBoolMap seen;
199	3032703	while (! done()) {
200	2794732	TNode fact = get();
201	1397477	if (d_isComplete && !isCompleteForTerm(fact, seen)) {
202	2724	d_isComplete = false;
203		}
204
205		// only reason about equalities
206	1397477	if (fact.getKind() == kind::EQUAL \|\| (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
207	836283	ok = assertFactToEqualityEngine(fact, fact);
208		} else {
209	561194	ok = assertFactToEqualityEngine(fact, fact);
210		}
211	1397477	if (!ok)
212	222	return false;
213		}
214
215	237971	if (Theory::fullEffort(e) && isComplete()) {
216	20828	buildModel();
217		}
218
219	237971	return true;
220		}
221
222	20828	void CoreSolver::buildModel()
223		{
224	20828	Debug("bv-core") << "CoreSolver::buildModel() \n";
225	20828	NodeManager* nm = NodeManager::currentNM();
226	20828	d_modelValues.clear();
227	41379	TNodeSet constants;
228	41379	TNodeSet constants_in_eq_engine;
229		// collect constants in equality engine
230	20828	eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
231	123478	while (!eqcs_i.isFinished())
232		{
233	102650	TNode repr = *eqcs_i;
234	51325	if (repr.getKind() == kind::CONST_BITVECTOR)
235		{
236		// must check if it's just the constant
237	3570	eq::EqClassIterator it(repr, d_equalityEngine);
238	3570	if (!(++it).isFinished() \|\| true)
239		{
240	3570	constants.insert(repr);
241	3570	constants_in_eq_engine.insert(repr);
242		}
243		}
244	51325	++eqcs_i;
245		}
246
247		// build repr to value map
248
249	20828	eqcs_i = eq::EqClassesIterator(d_equalityEngine);
250	121524	while (!eqcs_i.isFinished())
251		{
252	58015	TNode repr = *eqcs_i;
253	50625	++eqcs_i;
254
255	149251	if (!repr.isVar() && repr.getKind() != kind::CONST_BITVECTOR
256	145709	&& !d_bv->isSharedTerm(repr))
257		{
258	42958	continue;
259		}
260
261	15057	TypeNode type = repr.getType();
262	7667	if (type.isBitVector() && repr.getKind() != kind::CONST_BITVECTOR)
263		{
264	4053	Debug("bv-core-model") << " processing " << repr << "\n";
265		// we need to assign a value for it
266	7829	TypeEnumerator te(type);
267	7829	Node val;
268	6047	do
269		{
270	10100	val = *te;
271	10100	++te;
272		// Debug("bv-core-model") << " trying value " << val << "\n";
273		// Debug("bv-core-model") << " is in set? " << constants.count(val) <<
274		// "\n"; Debug("bv-core-model") << " enumerator done? " <<
275		// te.isFinished() << "\n";
276	10100	} while (constants.count(val) != 0 && !(te.isFinished()));
277
278	4053	if (te.isFinished() && constants.count(val) != 0)
279		{
280		// if we cannot enumerate anymore values we just return the lemma
281		// stating that at least two of the representatives are equal.
282	554	std::vector<TNode> representatives;
283	277	representatives.push_back(repr);
284
285	341	for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
286	341	it != constants_in_eq_engine.end();
287		++it)
288		{
289	128	TNode constant = *it;
290	64	if (utils::getSize(constant) == utils::getSize(repr))
291		{
292	36	representatives.push_back(constant);
293		}
294		}
295	930	for (ModelValue::const_iterator it = d_modelValues.begin();
296	930	it != d_modelValues.end();
297		++it)
298		{
299	653	representatives.push_back(it->first);
300		}
301	554	std::vector<Node> equalities;
302	1243	for (unsigned i = 0; i < representatives.size(); ++i)
303		{
304	2272	for (unsigned j = i + 1; j < representatives.size(); ++j)
305		{
306	2579	TNode a = representatives[i];
307	2579	TNode b = representatives[j];
308	2645	if (a.getKind() == kind::CONST_BITVECTOR
309	1306	&& b.getKind() == kind::CONST_BITVECTOR)
310		{
311	33	Assert(a != b);
312	33	continue;
313		}
314	1273	if (utils::getSize(a) == utils::getSize(b))
315		{
316	1202	equalities.push_back(nm->mkNode(kind::EQUAL, a, b));
317		}
318		}
319		}
320		// better off letting the SAT solver split on values
321	277	if (equalities.size() > d_lemmaThreshold)
322		{
323		d_isComplete = false;
324		return;
325		}
326
327	277	if (equalities.size() == 0)
328		{
329		Debug("bv-core") << " lemma: true (no equalities)" << std::endl;
330		}
331		else
332		{
333	554	Node lemma = utils::mkOr(equalities);
334	277	d_bv->lemma(lemma);
335	277	Debug("bv-core") << " lemma: " << lemma << std::endl;
336		}
337	277	return;
338		}
339
340	3776	Debug("bv-core-model") << " " << repr << " => " << val << "\n";
341	3776	constants.insert(val);
342	3776	d_modelValues[repr] = val;
343		}
344		}
345		}
346
347	1397477	bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
348		// Notify the equality engine
349	2794954	if (!d_bv->inConflict()
350	5347200	&& (!d_bv->wasPropagatedBySubtheory(fact)
351	2025640	\|\| d_bv->getPropagatingSubtheory(fact) != SUB_CORE))
352		{
353	1154769	Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
354		// Debug("bv-slicer-eq") << " reason=" << reason << endl;
355	1154769	bool negated = fact.getKind() == kind::NOT;
356	2309538	TNode predicate = negated ? fact[0] : fact;
357	1154769	if (predicate.getKind() == kind::EQUAL) {
358	593575	if (negated) {
359		// dis-equality
360	198403	d_equalityEngine->assertEquality(predicate, false, reason);
361		} else {
362		// equality
363	395172	d_equalityEngine->assertEquality(predicate, true, reason);
364		}
365		} else {
366		// Adding predicate if the congruence over it is turned on
367	561194	if (d_equalityEngine->isFunctionKind(predicate.getKind()))
368		{
369		d_equalityEngine->assertPredicate(predicate, !negated, reason);
370		}
371		}
372		}
373
374		// checking for a conflict
375	1397477	if (d_bv->inConflict())
376		{
377	222	return false;
378		}
379	1397255	return true;
380		}
381
382	1212547	bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
383	1212547	Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
384	1212547	if (value) {
385	792322	return d_solver.storePropagation(predicate);
386		}
387	420225	return d_solver.storePropagation(predicate.notNode());
388		}
389
390	127942	bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
391	127942	Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
392	127942	if (value) {
393	96667	return d_solver.storePropagation(t1.eqNode(t2));
394		} else {
395	31275	return d_solver.storePropagation(t1.eqNode(t2).notNode());
396		}
397		}
398
399	222	void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
400	222	d_solver.conflict(t1, t2);
401	222	}
402
403	1340489	bool CoreSolver::storePropagation(TNode literal) {
404	1340489	return d_bv->storePropagation(literal, SUB_CORE);
405		}
406
407	222	void CoreSolver::conflict(TNode a, TNode b) {
408	444	std::vector<TNode> assumptions;
409	222	d_equalityEngine->explainEquality(a, b, true, assumptions);
410	444	Node conflict = flattenAnd(assumptions);
411	222	d_bv->setConflict(conflict);
412	222	}
413
414	51144	bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
415	51144	return utils::isEqualityTerm(term, seen);
416		}
417
418	3932	bool CoreSolver::collectModelValues(TheoryModel* m,
419		const std::set<Node>& termSet)
420		{
421	3932	if (Debug.isOn("bitvector-model")) {
422		context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
423		for (; it!= d_assertionQueue.end(); ++it) {
424		Debug("bitvector-model")
425		<< "CoreSolver::collectModelValues (assert " << *it << ")\n";
426		}
427		}
428	3932	if (isComplete()) {
429	3932	Debug("bitvector-model") << "CoreSolver::collectModelValues complete.";
430	4236	for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
431	608	Node a = it->first;
432	608	Node b = it->second;
433	608	Debug("bitvector-model") << "CoreSolver::collectModelValues modelValues "
434	304	<< a << " => " << b << ")\n";
435	304	if (!m->assertEquality(a, b, true))
436		{
437		return false;
438		}
439		}
440		}
441	3932	return true;
442		}
443
444		Node CoreSolver::getModelValue(TNode var) {
445		Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
446		Assert(isComplete());
447		TNode repr = d_equalityEngine->getRepresentative(var);
448		Node result = Node();
449		if (repr.getKind() == kind::CONST_BITVECTOR) {
450		result = repr;
451		} else if (d_modelValues.find(repr) == d_modelValues.end()) {
452		// it may be a shared term that never gets asserted
453		// result is just Null
454		Assert(d_bv->isSharedTerm(var));
455		} else {
456		result = d_modelValues[repr];
457		}
458		Debug("bitvector-model") << " => " << result <<"\n";
459		return result;
460		}
461
462	55014	EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b)
463		{
464	55014	if (d_equalityEngine->areEqual(a, b))
465		{
466		// The terms are implied to be equal
467	2738	return EQUALITY_TRUE;
468		}
469	52276	if (d_equalityEngine->areDisequal(a, b, false))
470		{
471		// The terms are implied to be dis-equal
472	22877	return EQUALITY_FALSE;
473		}
474	29399	return EQUALITY_UNKNOWN;
475		}
476
477		bool CoreSolver::hasTerm(TNode node) const
478		{
479		return d_equalityEngine->hasTerm(node);
480		}
481		void CoreSolver::addTermToEqualityEngine(TNode node)
482		{
483		d_equalityEngine->addTerm(node);
484		}
485
486	9403	CoreSolver::Statistics::Statistics()
487	9403	: d_numCallstoCheck(smtStatisticsRegistry().registerInt(
488	9403	"theory::bv::CoreSolver::NumCallsToCheck"))
489		{
490	9403	}
491
492	25782	void CoreSolver::checkExtf(Theory::Effort e)
493		{
494	25782	if (e == Theory::EFFORT_LAST_CALL)
495		{
496		std::vector<Node> nred = d_extTheory->getActive();
497		doExtfReductions(nred);
498		}
499	25782	Assert(e == Theory::EFFORT_FULL);
500		// do inferences (adds external lemmas) TODO: this can be improved to add
501		// internal inferences
502	51437	std::vector<Node> nred;
503	25782	if (d_extTheory->doInferences(0, nred))
504		{
505		return;
506		}
507	25782	d_needsLastCallCheck = false;
508	25782	if (!nred.empty())
509		{
510		// other inferences involving bv2nat, int2bv
511	254	if (options::bvAlgExtf())
512		{
513	127	if (doExtfInferences(nred))
514		{
515	70	return;
516		}
517		}
518	57	if (!options::bvLazyReduceExtf())
519		{
520	57	if (doExtfReductions(nred))
521		{
522	57	return;
523		}
524		}
525		else
526		{
527		d_needsLastCallCheck = true;
528		}
529		}
530		}
531
532	8438	bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; }
533
534	127	bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
535		{
536	127	NodeManager* nm = NodeManager::currentNM();
537	127	SkolemManager* sm = nm->getSkolemManager();
538	127	bool sentLemma = false;
539	127	eq::EqualityEngine* ee = d_equalityEngine;
540	254	std::map<Node, Node> op_map;
541	502	for (unsigned j = 0; j < terms.size(); j++)
542		{
543	750	TNode n = terms[j];
544	375	Assert(n.getKind() == kind::BITVECTOR_TO_NAT
545		\|\| n.getKind() == kind::INT_TO_BITVECTOR);
546	375	if (n.getKind() == kind::BITVECTOR_TO_NAT)
547		{
548		// range lemmas
549	201	if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
550		{
551	105	d_extf_range_infer.insert(n);
552	105	unsigned bvs = n[0].getType().getBitVectorSize();
553	210	Node min = nm->mkConst(Rational(0));
554	210	Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
555		Node lem = nm->mkNode(kind::AND,
556	210	nm->mkNode(kind::GEQ, n, min),
557	420	nm->mkNode(kind::LT, n, max));
558	210	Trace("bv-extf-lemma")
559	105	<< "BV extf lemma (range) : " << lem << std::endl;
560	105	d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_LEMMA);
561	105	sentLemma = true;
562		}
563		}
564	750	Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
565	375	op_map[r] = n;
566		}
567	502	for (unsigned j = 0; j < terms.size(); j++)
568		{
569	750	TNode n = terms[j];
570	750	Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
571	375	std::map<Node, Node>::iterator it = op_map.find(r);
572	375	if (it != op_map.end())
573		{
574	332	Node parent = it->second;
575		// Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
576		// n );
577	332	Node cterm = parent[0].eqNode(n);
578	332	Trace("bv-extf-lemma-debug")
579	166	<< "BV extf collapse based on : " << cterm << std::endl;
580	166	if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
581		{
582	86	d_extf_collapse_infer.insert(cterm);
583
584	172	Node t = n[0];
585	86	if (t.getType() == parent.getType())
586		{
587	84	if (n.getKind() == kind::INT_TO_BITVECTOR)
588		{
589	64	Assert(t.getType().isInteger());
590		// congruent modulo 2^( bv width )
591	64	unsigned bvs = n.getType().getBitVectorSize();
592	128	Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
593		Node k = sm->mkDummySkolem(
594	128	"int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
595	64	t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
596		}
597	168	Node lem = parent.eqNode(t);
598
599	84	if (parent[0] != n)
600		{
601	22	Assert(ee->areEqual(parent[0], n));
602	22	lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
603		}
604		// this handles inferences of the form, e.g.:
605		// ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
606		// (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
607	168	Trace("bv-extf-lemma")
608	84	<< "BV extf lemma (collapse) : " << lem << std::endl;
609	84	d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_COLLAPSE);
610	84	sentLemma = true;
611		}
612		}
613	332	Trace("bv-extf-lemma-debug")
614	166	<< "BV extf f collapse based on : " << cterm << std::endl;
615		}
616		}
617	254	return sentLemma;
618		}
619
620	57	bool CoreSolver::doExtfReductions(std::vector<Node>& terms)
621		{
622	114	std::vector<Node> nredr;
623	57	if (d_extTheory->doReductions(0, terms, nredr))
624		{
625	57	return true;
626		}
627		Assert(nredr.empty());
628		return false;
629	28318	}