/*! \file bv_subtheory_core.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Aina Niemetz, Andrew Reynolds
+ ** Andrew Reynolds, Liana Hadarean, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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.\endverbatim
**
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/bv/theory_bv.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 CVC4::theory::bv;
using namespace CVC4::theory::bv::utils;
-CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt)
+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_preregisterCalled(false),
d_checkCalled(false),
d_bv(bv),
- d_extTheory(extt),
- d_reasons(c)
+ 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() {}
void CoreSolver::finishInit()
{
// use the parent's equality engine, which may be the one we allocated above
- d_equalityEngine = d_bv->getEqualityEngine();
+ d_equalityEngine = d_bv->d_bv.getEqualityEngine();
// The kinds we are treating as function application in congruence
d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true);
bool CoreSolver::check(Theory::Effort e) {
Trace("bitvector::core") << "CoreSolver::check \n";
- d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep);
+ d_bv->d_im.spendResource(ResourceManager::Resource::TheoryCheckStep);
d_checkCalled = true;
Assert(!d_bv->inConflict());
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)) {
+ 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;
}
// checking for a conflict
- if (d_bv->inConflict()) {
+ if (d_bv->inConflict())
+ {
return false;
}
return true;
return utils::isEqualityTerm(term, seen);
}
-bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+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::collectModelInfo (assert "
- << *it << ")\n";
+ Debug("bitvector-model")
+ << "CoreSolver::collectModelValues (assert " << *it << ")\n";
}
}
- set<Node> termSet;
- const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
- d_bv->computeAssertedTerms(termSet, irrKinds, true);
- if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
- {
- return false;
- }
if (isComplete()) {
- Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
+ 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::collectModelInfo modelValues "
- << a << " => " << b <<")\n";
+ Debug("bitvector-model") << "CoreSolver::collectModelValues modelValues "
+ << a << " => " << b << ")\n";
if (!m->assertEquality(a, b, true))
{
return false;
return result;
}
-void CoreSolver::addSharedTerm(TNode t)
-{
- d_equalityEngine->addTriggerTerm(t, THEORY_BV);
-}
-
EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b)
{
if (d_equalityEngine->areEqual(a, b))
CoreSolver::Statistics::~Statistics() {
smtStatisticsRegistry()->unregisterStat(&d_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();
+ 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::UNKNOWN);
+ 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 = nm->mkSkolem(
+ "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::UNKNOWN);
+ 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;
+}
projects / cvc5.git / blobdiff