diff options
30 files changed, 221 insertions, 213 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index e86b03258..62bd71f6a 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -92,10 +92,17 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat 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; @@ -107,7 +114,6 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat 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"); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 411a0aea1..52d32606b 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1199,7 +1199,7 @@ formula[CVC4::Expr& f] { 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); } ) ; @@ -1219,7 +1219,7 @@ morecomparisons[std::vector<CVC4::Expr>& expressions, { f = addNots(EXPR_MANAGER, n, f); expressions.push_back(f); } - inner=morecomparisons[expressions,operators]? + morecomparisons[expressions,operators]? ) ; @@ -1462,7 +1462,7 @@ recordStore[CVC4::Expr& f] 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) { diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 7e6f4fd93..9bded3db5 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -98,6 +98,7 @@ Solver::Solver(CVC4::context::Context* c) : , 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) @@ -114,7 +115,6 @@ Solver::Solver(CVC4::context::Context* c) : , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) - , only_bcp(false) , d_explanations(c) {} diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 460877a23..3cb5464da 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -325,7 +325,7 @@ Constraint ConstraintValue::getCeiling() { DeltaRational ceiling(getValue().ceiling()); -#warning "Optimize via the iterator" + // TODO: "Optimize via the iterator" return d_database->getConstraint(getVariable(), getType(), ceiling); } @@ -334,7 +334,7 @@ Constraint ConstraintValue::getFloor() { DeltaRational floor(Rational(getValue().floor())); -#warning "Optimize via the iterator" + // TODO: "Optimize via the iterator" return d_database->getConstraint(getVariable(), getType(), floor); } diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 1b3a5cac7..613ce8368 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -504,7 +504,7 @@ SumPair DioSolver::processEquationsForCut(){ 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; @@ -612,7 +612,10 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::solveIndex(DioS 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); @@ -644,7 +647,10 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::decomposeIndex( 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); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e183e0e1b..7f0088f5b 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -53,8 +53,8 @@ namespace arith { 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), @@ -904,7 +904,7 @@ Comparison TheoryArith::mkIntegerEqualityFromAssignment(ArithVar v){ } Node TheoryArith::dioCutting(){ - context::Context::ScopedPush speculativePush(getContext()); + context::Context::ScopedPush speculativePush(getSatContext()); //DO NOT TOUCH THE OUTPUTSTREAM //TODO: Improve this @@ -1043,7 +1043,7 @@ Node TheoryArith::assertionCases(TNode assertion){ //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) @@ -1352,7 +1352,7 @@ void TheoryArith::debugPrintModel(){ 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){ @@ -1387,7 +1387,7 @@ void TheoryArith::propagate(Effort e) { }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{ @@ -1578,9 +1578,6 @@ Node TheoryArith::getValue(TNode n) { } } -void TheoryArith::notifyEq(TNode lhs, TNode rhs) { -} - void TheoryArith::notifyRestart(){ TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer); @@ -1674,7 +1671,7 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){ 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. diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index aa7740c37..59653b62d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -259,7 +259,7 @@ private: 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(); /** @@ -271,8 +271,6 @@ public: void propagate(Effort e); Node explain(TNode n); - void notifyEq(TNode lhs, TNode rhs); - Node getValue(TNode n); void shutdown(){ } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index a62ebed06..80bcb47dd 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -49,8 +49,8 @@ const bool d_solveWrite2 = false; 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), @@ -316,11 +316,11 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs 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; } @@ -332,7 +332,7 @@ bool TheoryArrays::propagate(TNode literal) // 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) { @@ -349,7 +349,7 @@ bool TheoryArrays::propagate(TNode literal) } // 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; @@ -407,7 +407,7 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) { */ 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: @@ -495,17 +495,17 @@ void TheoryArrays::preRegisterTerm(TNode node) 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) { @@ -526,7 +526,7 @@ void TheoryArrays::propagate(Effort e) 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); @@ -539,7 +539,7 @@ Node TheoryArrays::explain(TNode literal) 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); @@ -716,7 +716,7 @@ void TheoryArrays::check(Effort e) { 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 || @@ -777,7 +777,7 @@ void TheoryArrays::check(Effort e) { // 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 { @@ -791,7 +791,7 @@ void TheoryArrays::check(Effort e) { } } - Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::check(): done" << endl; + Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; } @@ -844,7 +844,7 @@ void TheoryArrays::setNonLinear(TNode a) { 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; @@ -873,7 +873,7 @@ void TheoryArrays::setNonLinear(TNode a) 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); } } @@ -969,7 +969,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) 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); @@ -1049,7 +1049,7 @@ void TheoryArrays::checkStore(TNode 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(getSatContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; queueRowLemma(lem); } } @@ -1078,7 +1078,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) 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); } @@ -1090,7 +1090,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) 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); } } @@ -1126,7 +1126,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) 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); } } @@ -1141,7 +1141,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) 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); } } @@ -1177,7 +1177,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType 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(getSatContext()->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) { @@ -1191,7 +1191,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) 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); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 99b976b9d..d18b3abde 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -122,7 +122,7 @@ class TheoryArrays : public Theory { 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"); } @@ -244,13 +244,13 @@ class TheoryArrays : public Theory { 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)) { diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index fedc47aeb..99b5b6007 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -30,8 +30,8 @@ namespace booleans { 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); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index f5a46b799..30d2aaca7 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -29,8 +29,8 @@ namespace builtin { 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 */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index a3f4364ba..b6f12793d 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -36,13 +36,13 @@ const bool d_useEqualityEngine = true; 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), @@ -204,7 +204,7 @@ void TheoryBV::check(Effort e) // 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; } @@ -247,7 +247,7 @@ Node TheoryBV::getValue(TNode n) { 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; @@ -256,13 +256,13 @@ void TheoryBV::propagate(Effort e) { // 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) { @@ -353,11 +353,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu 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; } @@ -369,7 +369,7 @@ bool TheoryBV::propagate(TNode literal) // 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) { @@ -386,7 +386,7 @@ bool TheoryBV::propagate(TNode literal) } // 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; @@ -432,7 +432,7 @@ Node TheoryBV::explain(TNode node) { 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); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 940eaef56..c4953213d 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -69,7 +69,7 @@ private: 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); @@ -86,6 +86,7 @@ public: //Node preprocessTerm(TNode term); PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + private: class Statistics { @@ -107,13 +108,13 @@ private: 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)); diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 5587e25eb..da3fb6554 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -384,18 +384,15 @@ Node RewriteRule<NegMult>::apply(Node node) { 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); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 530949de2..490b413db 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -308,15 +308,17 @@ Node RewriteRule<XorOne>::apply(Node node) { 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; } @@ -344,16 +346,11 @@ template<> inline 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]); } } diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 0ce3fa303..60715ee60 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -33,10 +33,7 @@ struct AllRewriteRules; 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); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6e0d45948..7b1562ada 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -53,8 +53,8 @@ Node TheoryDatatypes::getConstructorForSelector( Node sel ) } -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), @@ -83,13 +83,6 @@ void TheoryDatatypes::addSharedTerm(TNode t) { << 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; @@ -740,8 +733,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) { 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; @@ -862,8 +855,8 @@ void TheoryDatatypes::addTermToLabels( Node t ) { //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 ){ @@ -881,8 +874,8 @@ void TheoryDatatypes::addTermToLabels( Node t ) { 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); } @@ -913,8 +906,8 @@ void TheoryDatatypes::collectTerms( Node n, bool recurse ) { 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; @@ -934,8 +927,8 @@ void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) { 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; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 281b11a93..967000c3e 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -140,13 +140,12 @@ private: 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() { } diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index bccd520f9..2d3b4a43a 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -139,20 +139,21 @@ struct TheoryTraits<${theory_id}> { " # 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" diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index db95edfa0..897c0fa2d 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -21,18 +21,18 @@ using namespace theory; 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()) { @@ -40,24 +40,32 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) const { 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; @@ -65,20 +73,21 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { 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; @@ -88,7 +97,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { } void PreRegisterVisitor::start(TNode node) { - d_theories = 0; d_multipleTheories = false; } diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 74b756a03..11a56ec1e 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -33,26 +33,27 @@ class PreRegisterVisitor { /** 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: @@ -60,12 +61,16 @@ 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. diff --git a/src/theory/theory.h b/src/theory/theory.h index d0218236d..40f72dafc 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -130,19 +130,19 @@ private: 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. @@ -205,19 +205,20 @@ protected: /** * 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); } @@ -264,7 +265,7 @@ protected: } const LogicInfo& getLogicInfo() const { - return *d_logicInfo; + return d_logicInfo; } /** @@ -393,10 +394,10 @@ public: } /** - * 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; } /** @@ -429,7 +430,7 @@ public: * 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)); } @@ -457,19 +458,6 @@ public: 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. * * An implementation of check() is required to either: @@ -629,6 +617,11 @@ public: 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); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 314e3bdb3..1122e09c6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -47,7 +47,7 @@ TheoryEngine::TheoryEngine(context::Context* context, 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), @@ -87,7 +87,6 @@ void TheoryEngine::preRegister(TNode preprocessed) { 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) { @@ -315,13 +314,16 @@ void TheoryEngine::propagate(Theory::Effort effort) { 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()); } } } @@ -366,17 +368,30 @@ bool TheoryEngine::properPropagation(TNode lit) const { } 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; @@ -388,11 +403,6 @@ Node TheoryEngine::getValue(TNode 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 @@ -417,8 +427,6 @@ bool TheoryEngine::presolve() { }/* 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 @@ -454,11 +462,6 @@ void TheoryEngine::notifyRestart() { } 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 @@ -810,7 +813,10 @@ Node TheoryEngine::explain(ExplainTask toExplain) 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)); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 28a1000f1..2b4fd24d1 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -129,7 +129,7 @@ class TheoryEngine { * 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 @@ -471,8 +471,7 @@ public: 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); } /** diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index f53918683..ec28dad75 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -27,8 +27,8 @@ namespace theory { 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), diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 071883e1a..6956390f5 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -102,7 +102,7 @@ private: 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); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index c6d6e3e2e..161329c06 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -48,6 +48,7 @@ class TheoryArithWhite : public CxxTest::TestSuite { NodeManagerScope* d_scope; TestOutputChannel d_outputChannel; + LogicInfo d_logicInfo; Theory::Effort d_level; TheoryArith* d_arith; @@ -98,7 +99,7 @@ public: 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>(); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index a737772ed..1de3854b9 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -101,8 +101,8 @@ public: 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) { @@ -149,6 +149,7 @@ class TheoryBlack : public CxxTest::TestSuite { UserContext* d_uctxt; NodeManager* d_nm; NodeManagerScope* d_scope; + LogicInfo* d_logicInfo; TestOutputChannel d_outputChannel; @@ -164,7 +165,9 @@ public: 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); @@ -174,6 +177,7 @@ public: atom1 = Node::null(); atom0 = Node::null(); delete d_dummy; + delete d_logicInfo; delete d_scope; delete d_nm; delete d_uctxt; diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index a158b167f..1a91364a4 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -71,7 +71,7 @@ public: 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)); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 6bca0c873..ff6cba936 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -107,8 +107,8 @@ class FakeTheory : public Theory { // 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 */ |