/** The bit-vector theory */
TheoryBV* d_bv;
AssertionQueue d_assertionQueue;
- context::CDO<uint32_t> d_assertionIndex;
+ context::CDO<uint32_t> d_assertionIndex;
public:
SubtheorySolver(context::Context* c, TheoryBV* bv) :
virtual void collectModelInfo(TheoryModel* m) = 0;
virtual bool isComplete() = 0;
virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
-
+ virtual void addSharedTerm(TNode node) {}
bool done() { return d_assertionQueue.size() == d_assertionIndex; }
TNode get() {
Assert (!done());
BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
: SubtheorySolver(c, bv),
d_bitblaster(new Bitblaster(c, bv)),
- d_bitblastQueue(c)
+ d_bitblastQueue(c),
+ d_statistics()
{}
BitblastSolver::~BitblastSolver() {
delete d_bitblaster;
}
+BitblastSolver::Statistics::Statistics()
+ : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
+{
+ StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+BitblastSolver::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
+
void BitblastSolver::preRegister(TNode node) {
if ((node.getKind() == kind::EQUAL ||
node.getKind() == kind::BITVECTOR_ULT ||
bool BitblastSolver::check(Theory::Effort e) {
+ ++(d_statistics.d_numCallstoCheck);
//// Eager bit-blasting
if (options::bitvectorEagerBitblast()) {
while (!done()) {
// Processing assertions
while (!done()) {
TNode fact = get();
- if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) {
+ if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
// Some atoms have not been bit-blasted yet
d_bitblaster->bbAtom(fact);
// Assert to sat
* BitblastSolver
*/
class BitblastSolver : public SubtheorySolver {
-
+ struct Statistics {
+ IntStat d_numCallstoCheck;
+ Statistics();
+ ~Statistics();
+ };
/** Bitblaster */
Bitblaster* d_bitblaster;
/** Nodes that still need to be bit-blasted */
context::CDQueue<TNode> d_bitblastQueue;
-
+ Statistics d_statistics;
public:
BitblastSolver(context::Context* c, TheoryBV* bv);
~BitblastSolver();
bool CoreSolver::check(Theory::Effort e) {
Trace("bitvector::core") << "CoreSolver::check \n";
Assert (!d_bv->inConflict());
-
+ ++(d_statistics.d_numCallstoCheck);
bool ok = true;
std::vector<Node> core_eqs;
while (! done()) {
bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
// Notify the equality engine
- if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) {
+ if (d_useEqualityEngine && !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;
d_bv->computeRelevantTerms(termSet);
m->assertEqualityEngine(&d_equalityEngine, &termSet);
}
+
+CoreSolver::Statistics::Statistics()
+ : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
+{
+ StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+CoreSolver::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
* Bitvector equality solver
*/
class CoreSolver : public SubtheorySolver {
-
+ struct Statistics {
+ IntStat d_numCallstoCheck;
+ Statistics();
+ ~Statistics();
+ };
+
// NotifyClass: handles call-back from congruence closure module
class NotifyClass : public eq::EqualityEngineNotify {
CoreSolver& d_solver;
bool assertFactToEqualityEngine(TNode fact, TNode reason);
bool decomposeFact(TNode fact);
Node getBaseDecomposition(TNode a, std::vector<TNode>& explanation);
+ Statistics d_statistics;
public:
CoreSolver(context::Context* c, TheoryBV* bv);
~CoreSolver();
using namespace CVC4::theory::bv::utils;
bool InequalitySolver::check(Theory::Effort e) {
- Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
+ Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
+ ++(d_statistics.d_numCallstoCheck);
+
bool ok = true;
while (!done() && ok) {
TNode fact = get();
void InequalitySolver::assertFact(TNode fact) {
d_assertionQueue.push_back(fact);
- d_assertionSet.insert(fact);
+ d_assertionSet.insert(fact);
+ if (!isInequalityOnly(fact)) {
+ d_isComplete = false;
+ }
+}
+
+bool InequalitySolver::isInequalityOnly(TNode node) {
+ if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) {
+ return d_ineqTermCache[node];
+ }
+
+ if (node.getKind() == kind::NOT) {
+ node = node[0];
+ }
+
+ 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) {
+ return false;
+ }
+ bool res = true;
+ for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+ res = res && isInequalityOnly(node[i]);
+ }
+ d_ineqTermCache[node] = res;
+ return res;
}
void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
Assert (false);
}
+InequalitySolver::Statistics::Statistics()
+ : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
+{
+ StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+InequalitySolver::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
+
namespace bv {
class InequalitySolver: public SubtheorySolver {
+ struct Statistics {
+ IntStat d_numCallstoCheck;
+ Statistics();
+ ~Statistics();
+ };
+
context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
InequalityGraph d_inequalityGraph;
+ context::CDO<bool> d_isComplete;
+ __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache;
+ bool isInequalityOnly(TNode node);
+ Statistics d_statistics;
public:
-
InequalitySolver(context::Context* c, TheoryBV* bv)
: SubtheorySolver(c, bv),
d_assertionSet(c),
- d_inequalityGraph(c)
+ d_inequalityGraph(c),
+ d_isComplete(c, true),
+ d_ineqTermCache(),
+ d_statistics()
{}
bool check(Theory::Effort e);
void propagate(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
- bool isComplete() { return true; }
+ bool isComplete() { return d_isComplete; }
void collectModelInfo(TheoryModel* m) {}
EqualityStatus getEqualityStatus(TNode a, TNode b);
void assertFact(TNode fact);
#include "theory/bv/bitblaster.h"
#include "theory/bv/options.h"
#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/bv_subtheory_core.h"
+#include "theory/bv/bv_subtheory_inequality.h"
+#include "theory/bv/bv_subtheory_bitblast.h"
#include "theory/model.h"
using namespace CVC4;
d_context(c),
d_alreadyPropagatedSet(c),
d_sharedTermsSet(c),
- d_coreSolver(c, this),
- d_inequalitySolver(c, this),
- d_bitblastSolver(c, this),
+ d_subtheories(),
+ d_subtheoryMap(),
d_statistics(),
d_conflict(c, false),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
d_propagatedBy(c)
- {}
-
-TheoryBV::~TheoryBV() {}
+ {
+ SubtheorySolver* core_solver = new CoreSolver(c, this);
+ d_subtheories.push_back(core_solver);
+ d_subtheoryMap[SUB_CORE] = core_solver;
+
+ SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
+ d_subtheories.push_back(ineq_solver);
+ d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
+
+ SubtheorySolver* bb_solver = new BitblastSolver(c, this);
+ d_subtheories.push_back(bb_solver);
+ d_subtheoryMap[SUB_BITBLAST] = bb_solver;
+ }
+TheoryBV::~TheoryBV() {
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+ delete d_subtheories[i];
+ }
+}
void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_coreSolver.setMasterEqualityEngine(eq);
+ dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
}
TheoryBV::Statistics::Statistics():
d_avgConflictSize("theory::bv::AvgBVConflictSize"),
d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
- d_solveTimer("theory::bv::solveTimer")
+ d_solveTimer("theory::bv::solveTimer"),
+ d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
+ d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0)
{
StatisticsRegistry::registerStat(&d_avgConflictSize);
StatisticsRegistry::registerStat(&d_solveSubstitutions);
StatisticsRegistry::registerStat(&d_solveTimer);
+ StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort);
+ StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort);
}
TheoryBV::Statistics::~Statistics() {
StatisticsRegistry::unregisterStat(&d_avgConflictSize);
StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
StatisticsRegistry::unregisterStat(&d_solveTimer);
+ StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort);
+ StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort);
}
// don't use the equality engine in the eager bit-blasting
return;
}
-
- d_bitblastSolver.preRegister(node);
- d_coreSolver.preRegister(node);
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+ d_subtheories[i]->preRegister(node);
+ }
}
void TheoryBV::sendConflict() {
void TheoryBV::check(Effort e)
{
Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-
+ if (Theory::fullEffort(e)) {
+ ++(d_statistics.d_numCallsToCheckFullEffort);
+ } else {
+ ++(d_statistics.d_numCallsToCheckStandardEffort);
+ }
// if we are already in conflict just return the conflict
if (inConflict()) {
sendConflict();
while (!done()) {
TNode fact = get().assertion;
- d_coreSolver.assertFact(fact);
- d_inequalitySolver.assertFact(fact);
- d_bitblastSolver.assertFact(fact);
- }
-
- bool ok = true;
- if (!inConflict()) {
- ok = d_coreSolver.check(e);
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+ d_subtheories[i]->assertFact(fact);
+ }
}
- Assert (!ok == inConflict());
- if (!inConflict() && !d_coreSolver.isComplete()) {
- ok = d_inequalitySolver.check(e);
- }
+ bool ok = true;
+ bool complete = false;
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+ Assert (!inConflict());
+ ok = d_subtheories[i]->check(e);
+ complete = d_subtheories[i]->isComplete();
- // Assert (!ok == inConflict());
- // if (!inConflict() && !d_coreSolver.isCoreTheory()) {
- // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) {
- // ok = d_bitblastSolver.check(e);
- // }
-
- Assert (!ok == inConflict());
- if (inConflict()) {
- sendConflict();
+ if (!ok) {
+ // if we are in a conflict no need to check with other theories
+ Assert (inConflict());
+ sendConflict();
+ return;
+ }
+ if (complete) {
+ // if the last subtheory was complete we stop
+ return;
+ }
}
}
void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
Assert(!inConflict());
// Assert (fullModel); // can only query full model
- d_coreSolver.collectModelInfo(m);
- d_bitblastSolver.collectModelInfo(m);
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+ d_subtheories[i]->collectModelInfo(m);
+ }
}
void TheoryBV::propagate(Effort e) {
void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
- // Ask the appropriate subtheory for the explanation
- if (propagatedBy(literal, SUB_CORE)) {
- Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): CORE" << std::endl;
- d_coreSolver.explain(literal, assumptions);
- } else {
- Assert(propagatedBy(literal, SUB_BITBLAST));
- Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
- d_bitblastSolver.explain(literal, assumptions);
- }
+ Assert (wasPropagatedBySubtheory(literal));
+ SubTheory sub = getPropagatingSubtheory(literal);
+ d_subtheoryMap[sub]->explain(literal, assumptions);
}
Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
d_sharedTermsSet.insert(t);
if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) {
- d_coreSolver.addSharedTerm(t);
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+ d_subtheories[i]->addSharedTerm(t);
+ }
}
}
if (options::bitvectorEagerBitblast()) {
return EQUALITY_UNKNOWN;
}
-
- EqualityStatus status = d_coreSolver.getEqualityStatus(a, b);
- if (status == EQUALITY_UNKNOWN) {
- status = d_inequalitySolver.getEqualityStatus(a, b);
- }
- if (status == EQUALITY_UNKNOWN) {
- status = d_bitblastSolver.getEqualityStatus(a, b);
+
+ for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+ EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
+ if (status != EQUALITY_UNKNOWN) {
+ return status;
+ }
}
-
- return status;
+ return EQUALITY_UNKNOWN; ;
}
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
#include "theory/bv/bv_subtheory.h"
-#include "theory/bv/bv_subtheory_core.h"
-#include "theory/bv/bv_subtheory_bitblast.h"
-#include "theory/bv/bv_subtheory_inequality.h"
-#include "theory/bv/slicer.h"
namespace CVC4 {
namespace theory {
namespace bv {
+class CoreSolver;
+class InequalitySolver;
+class BitblastSolver;
+
class TheoryBV : public Theory {
/** The context we are using */
context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
- CoreSolver d_coreSolver;
- InequalitySolver d_inequalitySolver;
- BitblastSolver d_bitblastSolver;
+ std::vector<SubtheorySolver*> d_subtheories;
+ __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
public:
TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
AverageStat d_avgConflictSize;
IntStat d_solveSubstitutions;
TimerStat d_solveTimer;
+ IntStat d_numCallsToCheckFullEffort;
+ IntStat d_numCallsToCheckStandardEffort;
Statistics();
~Statistics();
};
typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
PropagatedMap d_propagatedBy;
- bool propagatedBy(TNode literal, SubTheory subtheory) const {
+ bool wasPropagatedBySubtheory(TNode literal) const {
+ return d_propagatedBy.find(literal) != d_propagatedBy.end();
+ }
+
+ SubTheory getPropagatingSubtheory(TNode literal) const {
+ Assert(wasPropagatedBySubtheory(literal));
PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
- if (find == d_propagatedBy.end()) return false;
- else return (*find).second == subtheory;
+ return (*find).second;
}
/** Should be called to propagate the literal. */
projects / cvc5.git / commitdiff