if (checkJustified(node)) return false;
SatValue litVal = tryGetSatValue(node);
+
+#ifdef CVC4_ASSERTIONS
bool litPresent = false;
+#endif
+
if(d_decisionEngine->hasSatLiteral(node) ) {
SatLiteral lit = d_decisionEngine->getSatLiteral(node);
+
+#ifdef CVC4_ASSERTIONS
litPresent = true;
+#endif
SatVariable v = lit.getSatVariable();
// if (lit.isFalse() || lit.isTrue()) return false;
Trace("decision") << "no sat literal for this node" << std::endl;
}
-
/* You'd better know what you want */
Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
{ f = addNots(EXPR_MANAGER, n, f);
expressions.push_back(f);
}
- i=morecomparisons[expressions,operators]?
+ morecomparisons[expressions,operators]?
{ f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
)
;
{ f = addNots(EXPR_MANAGER, n, f);
expressions.push_back(f);
}
- inner=morecomparisons[expressions,operators]?
+ morecomparisons[expressions,operators]?
)
;
if(record.getName() != "__cvc4_record") {
PARSER_STATE->parseError("record-update applied to non-record");
}
- const DatatypeConstructorArg* updateArg;
+ const DatatypeConstructorArg* updateArg = 0;
try {
updateArg = &record[0][id];
} catch(IllegalArgumentException& e) {
, solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
, dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
+ , only_bcp(false)
, ok (true)
, cla_inc (1)
, var_inc (1)
, conflict_budget (-1)
, propagation_budget (-1)
, asynch_interrupt (false)
- , only_bcp(false)
, d_explanations(c)
{}
DeltaRational ceiling(getValue().ceiling());
-#warning "Optimize via the iterator"
+ // TODO: "Optimize via the iterator"
return d_database->getConstraint(getVariable(), getType(), ceiling);
}
DeltaRational floor(Rational(getValue().floor()));
-#warning "Optimize via the iterator"
+ // TODO: "Optimize via the iterator"
return d_database->getConstraint(getVariable(), getType(), floor);
}
SumPair DioSolver::purifyIndex(TrailIndex i){
-#warning "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient."
+ // TODO: "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient."
SumPair curr = d_trail[i].d_eq;
Debug("arith::dio") << "before solveIndex("<<i<<":"<<si.getNode()<< ")" << endl;
+#ifdef CVC4_ASSERTIONS
const Polynomial& p = si.getPolynomial();
+#endif
+
Assert(p.isIntegral());
Assert(p.selectAbsMinimum() == d_trail[i].d_minimalMonomial);
Debug("arith::dio") << "before decomposeIndex("<<i<<":"<<si.getNode()<< ")" << endl;
+#ifdef CVC4_ASSERTIONS
const Polynomial& p = si.getPolynomial();
+#endif
+
Assert(p.isIntegral());
Assert(p.selectAbsMinimum() == d_trail[i].d_minimalMonomial);
const uint32_t RESET_START = 2;
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_ARITH, c, u, out, valuation),
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_ARITH, c, u, out, valuation, logicInfo),
d_hasDoneWorkSinceCut(false),
d_learner(d_pbSubstitutions),
d_setupLiteralCallback(this),
}
Node TheoryArith::dioCutting(){
- context::Context::ScopedPush speculativePush(getContext());
+ context::Context::ScopedPush speculativePush(getSatContext());
//DO NOT TOUCH THE OUTPUTSTREAM
//TODO: Improve this
//Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind));
Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion);
- Debug("arith::assertions") << "arith assertion @" << getContext()->getLevel()
+ Debug("arith::assertions") << "arith assertion @" << getSatContext()->getLevel()
<<"(" << assertion
<< " \\-> "
//<< determineLeftVariable(assertion, simpleKind)
Node TheoryArith::explain(TNode n) {
- Debug("arith::explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
+ Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
Constraint c = d_constraintDatabase.lookup(n);
if(c != NullConstraint){
}else if(!c->assertedToTheTheory()){
Node literal = c->getLiteral();
- Debug("arith::prop") << "propagating @" << getContext()->getLevel() << " " << literal << endl;
+ Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl;
d_out->propagate(literal);
}else{
}
}
-void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
-}
-
void TheoryArith::notifyRestart(){
TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
(!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
-#warning "Policy point"
+ // TODO: "Policy point"
//We are only going to recreate the functionality for now.
//In the future this can be improved to generate a temporary constraint
//if none exists.
DeltaRational getDeltaValue(TNode n);
public:
- TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+ TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
virtual ~TheoryArith();
/**
void propagate(Effort e);
Node explain(TNode n);
- void notifyEq(TNode lhs, TNode rhs);
-
Node getValue(TNode n);
void shutdown(){ }
const bool d_useNonLinearOpt = true;
const bool d_eagerIndexSplitting = true;
-TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_ARRAY, c, u, out, valuation),
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo),
d_numRow("theory::arrays::number of Row lemmas", 0),
d_numExt("theory::arrays::number of Ext lemmas", 0),
d_numProp("theory::arrays::number of propagations", 0),
bool TheoryArrays::propagate(TNode literal)
{
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl;
return false;
}
// If asserted, we're done or in conflict
if (isAsserted) {
if (!satValue) {
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
std::vector<TNode> assumptions;
Node negatedLiteral;
if (normalized != d_false) {
}
// Nothing, just enqueue it for propagation and mark it as asserted already
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
d_literalsToPropagate.push_back(literal);
return true;
*/
void TheoryArrays::preRegisterTerm(TNode node)
{
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
switch (node.getKind()) {
case kind::EQUAL:
void TheoryArrays::propagate(Effort e)
{
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl;
if (!d_conflict) {
for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl;
bool satValue;
Node normalized = Rewriter::rewrite(literal);
if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
d_out->propagate(literal);
} else {
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
Node negatedLiteral;
std::vector<TNode> assumptions;
if (normalized != d_false) {
Node TheoryArrays::explain(TNode literal)
{
++d_numExplain;
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
std::vector<TNode> assumptions;
explain(literal, assumptions);
return mkAnd(assumptions);
void TheoryArrays::addSharedTerm(TNode t) {
- Debug("arrays::sharing") << spaces(getContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
+ Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
d_equalityEngine.addTriggerTerm(t);
if (t.getType().isArray()) {
d_sharedArrays.insert(t,true);
Assertion assertion = get();
TNode fact = assertion.assertion;
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
// If the assertion doesn't have a literal, it's a shared equality
Assert(assertion.isPreregistered ||
// If in conflict, output the conflict
if (d_conflict) {
- Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl;
d_out->conflict(d_conflictNode);
}
else {
}
}
- Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::check(): done" << endl;
+ Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
}
{
if (d_infoMap.isNonLinear(a)) return;
- Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n";
+ Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n";
d_infoMap.setNonLinear(a);
++d_numNonLinear;
TNode j = store[1];
TNode c = store[0];
lem = make_quad(store, c, j, i);
- Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+ Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
queueRowLemma(lem);
}
}
Node n;
while (true) {
- Trace("arrays-merge") << spaces(getContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n";
+ Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n";
checkRIntro1(a, b);
checkRIntro1(b, a);
TNode j = *it;
if (i == j) continue;
lem = make_quad(a,b,i,j);
- Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
+ Trace("arrays-lem") << spaces(get
SatContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
queueRowLemma(lem);
}
}
TNode j = store[1];
if (i == j) continue;
lem = make_quad(store, store[0], j, i);
- Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+ Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
queueRowLemma(lem);
}
TNode j = instore[1];
if (i == j) continue;
lem = make_quad(instore, instore[0], j, i);
- Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+ Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
queueRowLemma(lem);
}
}
TNode j = store[1];
TNode c = store[0];
lem = make_quad(store, c, j, i);
- Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+ Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
queueRowLemma(lem);
}
}
TNode j = store[1];
TNode c = store[0];
lem = make_quad(store, c, j, i);
- Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+ Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
queueRowLemma(lem);
}
}
// If propagating, check propagations
if (d_propagateLemmas) {
if (d_equalityEngine.areDisequal(i,j)) {
- Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
+ Trace("arrays-lem") << spaces(get
SatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
Node reason = nm->mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j));
d_permRef.push_back(reason);
if (!ajExists) {
return;
}
if (bothExist && d_equalityEngine.areDisequal(aj,bj)) {
- Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
+ Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj));
d_permRef.push_back(reason);
d_equalityEngine.addEquality(i, j, reason);
public:
- TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+ TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheoryArrays();
std::string identify() const { return std::string("TheoryArrays"); }
NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
bool notify(TNode propagation) {
- Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+ Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
// Just forward to arrays
return d_arrays.propagate(propagation);
}
void notify(TNode t1, TNode t2) {
- Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+ Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
if (t1.getType().isArray()) {
d_arrays.mergeArrays(t1, t2);
if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
class TheoryBool : public Theory {
public:
- TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_BOOL, c, u, out, valuation) {
+ TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) {
}
Node getValue(TNode n);
class TheoryBuiltin : public Theory {
public:
- TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_BUILTIN, c, u, out, valuation) {}
+ TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
Node getValue(TNode n);
std::string identify() const { return std::string("TheoryBuiltin"); }
};/* class TheoryBuiltin */
const bool d_useSatPropagation = true;
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
- : Theory(THEORY_BV, c, u, out, valuation),
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
+ : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
d_context(c),
d_assertions(c),
d_bitblaster(new Bitblaster(c) ),
- d_statistics(),
d_alreadyPropagatedSet(c),
+ d_statistics(),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
d_conflict(c, false),
// If in conflict, output the conflict
if (d_conflict) {
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
d_out->conflict(d_conflictNode);
return;
}
void TheoryBV::propagate(Effort e) {
- BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate()" << std::endl;
+ BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate()" << std::endl;
if (d_conflict) {
return;
// get new propagations from the equality engine
for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl;
+ BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl;
bool satValue;
Node normalized = Rewriter::rewrite(literal);
if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
d_out->propagate(literal);
} else {
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
Node negatedLiteral;
std::vector<TNode> assumptions;
if (normalized != d_false) {
bool TheoryBV::propagate(TNode literal)
{
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl;
return false;
}
// If asserted, we might be in conflict
if (isAsserted) {
if (!satValue) {
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
std::vector<TNode> assumptions;
Node negatedLiteral;
if (normalized != d_false) {
}
// Nothing, just enqueue it for propagation and mark it as asserted already
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
d_literalsToPropagate.push_back(literal);
return true;
void TheoryBV::addSharedTerm(TNode t) {
- Debug("bitvector::sharing") << spaces(getContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
+ Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
if (d_useEqualityEngine) {
d_equalityEngine.addTriggerTerm(t);
}
public:
- TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+ TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheoryBV();
void preRegisterTerm(TNode n);
//Node preprocessTerm(TNode term);
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+
private:
class Statistics {
NotifyClass(TheoryBV& uf): d_bv(uf) {}
bool notify(TNode propagation) {
- Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+ Debug("bitvector") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
// Just forward to bv
return d_bv.propagate(propagation);
}
void notify(TNode t1, TNode t2) {
- Debug("arrays") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+ Debug("arrays") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
// Propagate equality between shared terms
Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
d_bv.propagate(t1.eqNode(t2));
BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
TNode mult = node[0];
std::vector<Node> children;
- bool has_const = false;
+ BitVector bv(utils::getSize(node), (unsigned)1);
for(unsigned i = 0; i < mult.getNumChildren(); ++i) {
if(mult[i].getKind() == kind::CONST_BITVECTOR) {
- Assert(has_const == false);
- has_const = true;
- BitVector bv = mult[i].getConst<BitVector>();
- children.push_back(utils::mkConst(-bv));
+ bv = bv * mult[i].getConst<BitVector>();
} else {
children.push_back(mult[i]);
}
}
- Assert (has_const);
+ children.push_back(utils::mkConst(-bv));
return utils::mkSortedNode(kind::BITVECTOR_MULT, children);
}
for(unsigned i = 0; i < node.getNumChildren(); ++i) {
if (node[i] == ones) {
// make sure only ones occurs only once
- Assert(!found_ones);
- found_ones = true;
+ found_ones = !found_ones;
} else {
children.push_back(node[i]);
}
}
- children[0] = utils::mkNode(kind::BITVECTOR_NOT, children[0]);
- return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
+ Node result = utils::mkNode(kind::BITVECTOR_XOR, children);
+ if (found_ones) {
+ result = utils::mkNode(kind::BITVECTOR_NOT, result);
+ }
+ return result;
}
Node RewriteRule<XorZero>::apply(Node node) {
BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
std::vector<Node> children;
- bool found_zero = false;
Node zero = utils::mkConst(utils::getSize(node), 0);
// XorSimplify should have been called before
for(unsigned i = 0; i < node.getNumChildren(); ++i) {
- if (node[i] == zero) {
- // make sure zero occurs only once
- Assert(!found_zero);
- found_zero = true;
- } else {
+ if (node[i] != zero) {
children.push_back(node[i]);
}
}
typedef RewriteResponse (*RewriteFunction) (TNode, bool);
class TheoryBVRewriter {
- // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
- // static CVC4_THREADLOCAL(TimerStat*) d_rewriteTimer;
-#warning "TODO: Double check thread safety and make sure the fix compiles on mac."
static RewriteFunction d_rewriteTable[kind::LAST_KIND];
static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
}
-TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_DATATYPES, c, u, out, valuation),
+TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
d_currAsserts(c),
d_currEqualities(c),
d_selectors(c),
<< t << endl;
}
-
-void TheoryDatatypes::notifyEq(TNode lhs, TNode rhs) {
- Debug("datatypes") << "TheoryDatatypes::notifyEq(): "
- << lhs << " = " << rhs << endl;
-
-}
-
void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) {
Debug("datatypes") << "TheoryDatatypes::notifyCongruent(): "
<< lhs << " = " << rhs << endl;
EqListsN::iterator sel_b_i = d_selector_eq.find( b );
EqListN* sel_b;
if( sel_b_i == d_selector_eq.end() ) {
- sel_b = new(getContext()->getCMM()) EqListN(true, getContext(), false,
- ContextMemoryAllocator<Node>(getContext()->getCMM()));
+ sel_b = new(getSatContext()->getCMM()) EqListN(true, getSatContext(), false,
+ ContextMemoryAllocator<Node>(getSatContext()->getCMM()));
d_selector_eq.insertDataFromContextMemory(b, sel_b);
} else {
sel_b = (*sel_b_i).second;
//add to labels
EqLists::iterator lbl_i = d_labels.find(t);
if(lbl_i == d_labels.end()) {
- EqList* lbl = new(getContext()->getCMM()) EqList(true, getContext(), false,
- ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+ EqList* lbl = new(getSatContext()->getCMM()) EqList(true, getSatContext(), false,
+ ContextMemoryAllocator<TNode>(getSatContext()->getCMM()));
//if there is only one constructor, then it must be
const Datatype& dt = ((DatatypeType)(t.getType()).toType()).getDatatype();
if( dt.getNumConstructors()==1 ){
void TheoryDatatypes::initializeEqClass( Node t ) {
EqListsN::iterator eqc_i = d_equivalence_class.find( t );
if( eqc_i == d_equivalence_class.end() ) {
- EqListN* eqc = new(getContext()->getCMM()) EqListN(true, getContext(), false,
- ContextMemoryAllocator<Node>(getContext()->getCMM()));
+ EqListN* eqc = new(getSatContext()->getCMM()) EqListN(true, getSatContext(), false,
+ ContextMemoryAllocator<Node>(getSatContext()->getCMM()));
eqc->push_back( t );
d_equivalence_class.insertDataFromContextMemory(t, eqc);
}
EqListsN::iterator sel_i = d_selector_eq.find( tmp );
EqListN* sel;
if( sel_i == d_selector_eq.end() ) {
- sel = new(getContext()->getCMM()) EqListN(true, getContext(), false,
- ContextMemoryAllocator<Node>(getContext()->getCMM()));
+ sel = new(getSatContext()->getCMM()) EqListN(true, getSatContext(), false,
+ ContextMemoryAllocator<Node>(getSatContext()->getCMM()));
d_selector_eq.insertDataFromContextMemory(tmp, sel);
} else {
sel = (*sel_i).second;
EqLists::iterator deq_i = d_disequalities.find(of);
EqList* deq;
if(deq_i == d_disequalities.end()) {
- deq = new(getContext()->getCMM()) EqList(true, getContext(), false,
- ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+ deq = new(getSatContext()->getCMM()) EqList(true, getSatContext(), false,
+ ContextMemoryAllocator<TNode>(getSatContext()->getCMM()));
d_disequalities.insertDataFromContextMemory(of, deq);
} else {
deq = (*deq_i).second;
CongruenceClosureExplainer<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cce;
public:
- TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+ TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheoryDatatypes();
void preRegisterTerm(TNode n);
void presolve();
void addSharedTerm(TNode t);
- void notifyEq(TNode lhs, TNode rhs);
void check(Effort e);
Node getValue(TNode n);
void shutdown() { }
"
# warnings about theory content and properties
- dir="$(dirname "$kf")/../../"
- if [ -e "$dir/$theory_header" ]; then
- for function in check propagate staticLearning notifyRestart presolve postsolve; do
- if eval "\$theory_has_$function"; then
- grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' ||
- echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2
- else
- grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' &&
- echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2
- fi
- done
- else
- echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2
- fi
+ # TODO: fix, not corresponding to staticLearning anymore
+ # dir="$(dirname "$kf")/../../"
+ # if [ -e "$dir/$theory_header" ]; then
+ # for function in check propagate staticLearning notifyRestart presolve postsolve; do
+ # if eval "\$theory_has_$function"; then
+ # grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' ||
+ # echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2
+ # else
+ # grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' &&
+ # echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2
+ # fi
+ # done
+ # else
+ # echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2
+ # fi
theory_has_check="false"
theory_has_propagate="false"
std::string PreRegisterVisitor::toString() const {
std::stringstream ss;
- TNodeVisitedMap::const_iterator it = d_visited.begin();
+ TNodeToTheorySetMap::const_iterator it = d_visited.begin();
for (; it != d_visited.end(); ++ it) {
ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
}
return ss.str();
}
-bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) const {
+bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => ";
- TNodeVisitedMap::iterator find = d_visited.find(current);
+ TNodeToTheorySetMap::iterator find = d_visited.find(current);
// If node is not visited at all, just return false
if (find == d_visited.end()) {
return false;
}
- Theory::Set theories = (*find).second;
+ Theory::Set theories;
TheoryId currentTheoryId = Theory::theoryOf(current);
TheoryId parentTheoryId = Theory::theoryOf(parent);
+ // Remember the theories interested in this term
+ d_theories[parent] = theories = Theory::setInsert(currentTheoryId, d_theories[parent]);
+ // Check if there are multiple of those
+ d_multipleTheories = d_multipleTheories || Theory::setRemove(parentTheoryId, theories);
+
+ theories = (*find).second;
if (Theory::setContains(currentTheoryId, theories)) {
// The current theory has already visited it, so now it depends on the parent
Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl;
return Theory::setContains(parentTheoryId, theories);
} else {
// If the current theory is not registered, it still needs to be visited
- Debug("register::internal") << "2:false" << std::endl;
+ Debug("register::internal") << "3:false" << std::endl;
return false;
}
}
void PreRegisterVisitor::visit(TNode current, TNode parent) {
+ Theory::Set theories;
+
Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
Debug("register::internal") << toString() << std::endl;
TheoryId currentTheoryId = Theory::theoryOf(current);
TheoryId parentTheoryId = Theory::theoryOf(parent);
- Theory::Set theories = d_visited[current];
+ // Remember the theories interested in this term
+ d_theories[parent] = theories = Theory::setInsert(currentTheoryId, d_theories[parent]);
+ // If there are theories other than the parent itself, we are in multi-theory case
+ d_multipleTheories = d_multipleTheories || Theory::setRemove(parentTheoryId, theories);
+
+ theories = d_visited[current];
Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl;
if (!Theory::setContains(currentTheoryId, theories)) {
- d_multipleTheories = d_multipleTheories || (theories != 0);
d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories);
d_engine->theoryOf(currentTheoryId)->preRegisterTerm(current);
- d_theories = Theory::setInsert(currentTheoryId, d_theories);
Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
}
if (!Theory::setContains(parentTheoryId, theories)) {
- d_multipleTheories = d_multipleTheories || (theories != 0);
d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories);
d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current);
- d_theories = Theory::setInsert(parentTheoryId, d_theories);
Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
}
Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl;
}
void PreRegisterVisitor::start(TNode node) {
- d_theories = 0;
d_multipleTheories = false;
}
/** The engine */
TheoryEngine* d_engine;
+ typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeToTheorySetMap;
+
/**
- * Map from nodes to the theories that have already seen them.
+ * Map from terms to the theories that have already had this term pre-registered.
*/
- typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
- TNodeVisitedMap d_visited;
+ TNodeToTheorySetMap d_visited;
/**
- * All the theories of the visitation.
+ * Map from terms to the theories that have have a sub-term in it.
*/
- theory::Theory::Set d_theories;
+ TNodeToTheorySetMap d_theories;
/**
- * String representation of the visited map, for debugging purposes.
+ * Is true if the term we're traversing involves multiple theories.
*/
- std::string toString() const;
+ bool d_multipleTheories;
/**
- * Is there more than one theory involved.
+ * String representation of the visited map, for debugging purposes.
*/
- bool d_multipleTheories;
+ std::string toString() const;
public:
typedef bool return_type;
PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
- : d_engine(engine), d_visited(context), d_theories(0) {}
+ : d_engine(engine)
+ , d_visited(context)
+ , d_theories(context)
+ , d_multipleTheories(false)
+ {}
/**
* Returns true is current has already been pre-registered with both current and parent theories.
*/
- bool alreadyVisited(TNode current, TNode parent) const;
+ bool alreadyVisited(TNode current, TNode parent);
/**
* Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
TheoryId d_id;
/**
- * The context for the Theory.
+ * The SAT search context for the Theory.
*/
- context::Context* d_context;
+ context::Context* d_satContext;
/**
- * The user context for the Theory.
+ * The user level assertion context for the Theory.
*/
context::UserContext* d_userContext;
/**
* Information about the logic we're operating within.
*/
- const LogicInfo* d_logicInfo;
+ const LogicInfo& d_logicInfo;
/**
* The assertFact() queue.
/**
* Construct a Theory.
*/
- Theory(TheoryId id, context::Context* context, context::UserContext* userContext,
- OutputChannel& out, Valuation valuation) throw() :
- d_id(id),
- d_context(context),
- d_userContext(userContext),
- d_facts(context),
- d_factsHead(context, 0),
- d_sharedTermsIndex(context, 0),
- d_careGraph(0),
- d_computeCareGraphTime(statName(id, "computeCareGraphTime")),
- d_sharedTerms(context),
- d_out(&out),
- d_valuation(valuation)
+ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
+ OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw()
+ : d_id(id)
+ , d_satContext(satContext)
+ , d_userContext(userContext)
+ , d_logicInfo(logicInfo)
+ , d_facts(satContext)
+ , d_factsHead(satContext, 0)
+ , d_sharedTermsIndex(satContext, 0)
+ , d_careGraph(0)
+ , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
+ , d_sharedTerms(satContext)
+ , d_out(&out)
+ , d_valuation(valuation)
{
StatisticsRegistry::registerStat(&d_computeCareGraphTime);
}
}
const LogicInfo& getLogicInfo() const {
- return *d_logicInfo;
+ return d_logicInfo;
}
/**
}
/**
- * Get the context associated to this Theory.
+ * Get the SAT context associated to this Theory.
*/
- context::Context* getContext() const {
- return d_context;
+ context::Context* getSatContext() const {
+ return d_satContext;
}
/**
* Assert a fact in the current context.
*/
void assertFact(TNode assertion, bool isPreregistered) {
- Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_context->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl;
+ Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_satContext->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl;
d_facts.push_back(Assertion(assertion, isPreregistered));
}
*/
virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
- /**
- * This method is called by the shared term manager when a shared
- * term lhs which this theory cares about (either because it
- * received a previous addSharedTerm call with lhs or because it
- * received a previous notifyEq call with lhs as the second
- * argument) becomes equal to another shared term rhs. This call
- * also serves as notice to the theory that the shared term manager
- * now considers rhs the representative for this equivalence class
- * of shared terms, so future notifications for this class will be
- * based on rhs not lhs.
- */
- virtual void notifyEq(TNode lhs, TNode rhs) { }
-
/**
* Check the current assignment's consistency.
*
return set | (1 << theory);
}
+ /** Add the theory to the set. If no set specified, just returns a singleton set */
+ static inline Set setRemove(TheoryId theory, Set set = 0) {
+ return set ^ (1 << theory);
+ }
+
/** Check if the set contains the theory */
static inline bool setContains(TheoryId theory, Set set) {
return set & (1 << theory);
d_notify(*this),
d_sharedTerms(d_notify, context),
d_ppCache(),
- d_possiblePropagations(),
+ d_possiblePropagations(context),
d_hasPropagated(context),
d_inConflict(context, false),
d_hasShutDown(false),
if(Dump.isOn("missed-t-propagations")) {
d_possiblePropagations.push_back(preprocessed);
}
-
// Pre-register the terms in the atom
bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
if (multipleTheories) {
CVC4_FOR_EACH_THEORY;
if(Dump.isOn("missed-t-propagations")) {
- for(vector<TNode>::iterator i = d_possiblePropagations.begin();
- i != d_possiblePropagations.end();
- ++i) {
- if(d_hasPropagated.find(*i) == d_hasPropagated.end()) {
+ for(unsigned i = 0; i < d_possiblePropagations.size(); ++ i) {
+ Node atom = d_possiblePropagations[i];
+ bool value;
+ if (d_propEngine->hasValue(atom, value)) continue;
+ // Doesn't have a value, check it (and the negation)
+ if(d_hasPropagated.find(atom) == d_hasPropagated.end()) {
Dump("missed-t-propagations")
<< CommentCommand("Completeness check for T-propagations; expect invalid")
- << QueryCommand((*i).toExpr());
+ << QueryCommand(atom.toExpr())
+ << QueryCommand(atom.notNode().toExpr());
}
}
}
}
bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
- Assert(!node.isNull() && !expl.isNull());
-#warning implement TheoryEngine::properExplanation()
+ // Explanation must be either a conjunction of true literals that have true SAT values already
+ // or a singled literal that has a true SAT value already.
+ if (expl.getKind() == kind::AND) {
+ for (unsigned i = 0; i < expl.getNumChildren(); ++ i) {
+ bool value;
+ if (!d_propEngine->hasValue(expl[i], value) || !value) {
+ return false;
+ }
+ }
+ } else {
+ bool value;
+ return d_propEngine->hasValue(expl, value) && value;
+ }
return true;
}
Node TheoryEngine::getValue(TNode node) {
kind::MetaKind metakind = node.getMetaKind();
+
// special case: prop engine handles boolean vars
if(metakind == kind::metakind::VARIABLE && node.getType().isBoolean()) {
return d_propEngine->getValue(node);
}
+
// special case: value of a constant == itself
if(metakind == kind::metakind::CONSTANT) {
return node;
}/* TheoryEngine::getValue(TNode node) */
bool TheoryEngine::presolve() {
- // NOTE that we don't look at d_theoryIsActive[] here. First of
- // all, we haven't done any pre-registration yet, so we don't know
- // which theories are active. Second, let's give each theory a shot
- // at doing something with the input formula, even if it wouldn't
- // otherwise be active.
try {
// Definition of the statement that is to be run by every theory
}/* TheoryEngine::presolve() */
void TheoryEngine::postsolve() {
- // NOTE that we don't look at d_theoryIsActive[] here (for symmetry
- // with presolve()).
try {
// Definition of the statement that is to be run by every theory
}
void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
- // NOTE that we don't look at d_theoryIsActive[] here. First of
- // all, we haven't done any pre-registration yet, so we don't know
- // which theories are active. Second, let's give each theory a shot
- // at doing something with the input formula, even if it wouldn't
- // otherwise be active.
// Definition of the statement that is to be run by every theory
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
std::deque<ExplainTask> explainQueue;
// TODO: benchmark whether this helps
std::hash_set<ExplainTask, ExplainTaskHashFunction> explained;
+
+#ifdef CVC4_ASSERTIONS
bool value;
+#endif
// No need to explain "true"
explained.insert(ExplainTask(NodeManager::currentNM()->mkConst<bool>(true), SHARED_DATABASE_EXPLANATION));
* Used for "missed-t-propagations" dumping mode only. A set of all
* theory-propagable literals.
*/
- std::vector<TNode> d_possiblePropagations;
+ context::CDList<TNode> d_possiblePropagations;
/**
* Used for "missed-t-propagations" dumping mode only. A
inline void addTheory(theory::TheoryId theoryId) {
Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
- d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this));
- d_theoryTable[theoryId]->d_logicInfo = &d_logicInfo;
+ d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo);
}
/**
namespace uf {
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_UF, c, u, out, valuation),
+TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_UF, c, u, out, valuation, logicInfo),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
d_conflict(c, false),
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
void check(Effort);
void propagate(Effort);
NodeManagerScope* d_scope;
TestOutputChannel d_outputChannel;
+ LogicInfo d_logicInfo;
Theory::Effort d_level;
TheoryArith* d_arith;
d_nm = new NodeManager(d_ctxt, NULL);
d_scope = new NodeManagerScope(d_nm);
d_outputChannel.clear();
- d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
+ d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo);
preregistered = new std::set<Node>();
set<Node> d_registered;
vector<Node> d_getSequence;
- DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation) :
- Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation) {
+ DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) {
}
void registerTerm(TNode n) {
UserContext* d_uctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
+ LogicInfo* d_logicInfo;
TestOutputChannel d_outputChannel;
d_uctxt = new UserContext();
d_nm = new NodeManager(d_ctxt, NULL);
d_scope = new NodeManagerScope(d_nm);
- d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
+ d_logicInfo = new LogicInfo();
+
+ d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
d_outputChannel.clear();
atom0 = d_nm->mkConst(true);
atom1 = d_nm->mkConst(false);
atom1 = Node::null();
atom0 = Node::null();
delete d_dummy;
+ delete d_logicInfo;
delete d_scope;
delete d_nm;
delete d_uctxt;
Context* ctx = new Context();
Bitblaster* bb = new Bitblaster(ctx);
- NodeManager* nm = NodeManager::currentNM();
+ // NodeManager* nm = NodeManager::currentNM();
// TODO: update this
// Node a = nm->mkVar("a", nm->mkBitVectorType(4));
// Node b = nm->mkVar("b", nm->mkBitVectorType(4));
// static std::deque<RewriteItem> s_expected;
public:
- FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation) :
- Theory(theoryId, ctxt, uctxt, out, valuation)
+ FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
{ }
/** Register an expected rewrite call */
projects / cvc5.git / commitdiff