diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/callbacks.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/callbacks.h | 3 | ||||
-rw-r--r-- | src/theory/arith/constraint.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/soi_simplex.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 12 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 85 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 12 | ||||
-rw-r--r-- | src/theory/inference_id.h | 22 | ||||
-rw-r--r-- | src/theory/theory.h | 7 |
12 files changed, 88 insertions, 71 deletions
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index ee412483b..81f48ad00 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -64,9 +64,9 @@ RaiseConflict::RaiseConflict(TheoryArithPrivate& ta) : d_ta(ta) {} -void RaiseConflict::raiseConflict(ConstraintCP c) const{ +void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{ Assert(c->inConflict()); - d_ta.raiseConflict(c); + d_ta.raiseConflict(c, id); } FarkasConflictBuilder::FarkasConflictBuilder() diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 574d289b0..9f0ae1017 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -21,6 +21,7 @@ #include "theory/arith/arithvar.h" #include "theory/arith/bound_counts.h" #include "theory/arith/constraint_forward.h" +#include "theory/inference_id.h" #include "util/rational.h" namespace CVC4 { @@ -111,7 +112,7 @@ public: RaiseConflict(TheoryArithPrivate& ta); /** Calls d_ta.raiseConflict(c) */ - void raiseConflict(ConstraintCP c) const; + void raiseConflict(ConstraintCP c, InferenceId id) const; }; class FarkasConflictBuilder { diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index bafd4d682..f2de5da6c 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -2236,7 +2236,7 @@ bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons){ if(cons->negationHasProof()){ Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl; cons->impliedByUnate(ant, true); - d_raiseConflict.raiseConflict(cons); + d_raiseConflict.raiseConflict(cons, InferenceId::UNKNOWN); return true; }else if(!cons->isTrue()){ ++d_statistics.d_unatePropagateImplications; diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 3f32e7075..671c3f44a 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -244,6 +244,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions) void NonlinearExtension::check(Theory::Effort e) { + d_im.reset(); Trace("nl-ext") << std::endl; Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << ", built model = " << d_builtModel.get() << std::endl; @@ -277,7 +278,6 @@ void NonlinearExtension::check(Theory::Effort e) d_im.doPendingFacts(); d_im.doPendingLemmas(); d_im.doPendingPhaseRequirements(); - d_im.reset(); return; } // Otherwise, we will answer SAT. The values that we approximated are diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index df399d686..d93e42215 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -94,7 +94,7 @@ void SimplexDecisionProcedure::reportConflict(ArithVar basic){ ConstraintCP conflicted = generateConflictForBasic(basic); Assert(conflicted != NullConstraint); - d_conflictChannel.raiseConflict(conflicted); + d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN); d_conflictVariables.add(basic); } @@ -117,7 +117,7 @@ ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const { if(checkBasicForConflict(basic)){ ConstraintCP conflicted = generateConflictForBasic(basic); - d_conflictChannel.raiseConflict(conflicted); + d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN); return true; }else{ return false; diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 79136e77c..2ea3fd546 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -846,7 +846,7 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ d_conflictBuilder->addConstraint(c, coeff); } ConstraintCP conflicted = d_conflictBuilder->commitConflict(); - d_conflictChannel.raiseConflict(conflicted); + d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN); } tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e3c4919a3..83337dd90 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -47,15 +47,15 @@ TheoryArith::TheoryArith(context::Context* c, d_ppRewriteTimer("theory::arith::ppRewriteTimer"), d_ppPfGen(pnm, c, "Arith::ppRewrite"), d_astate(*d_internal, c, u, valuation), - d_inferenceManager(*this, d_astate, pnm), + d_im(*this, d_astate, pnm), d_nonlinearExtension(nullptr), - d_arithPreproc(d_astate, d_inferenceManager, pnm, logicInfo) + d_arithPreproc(d_astate, d_im, pnm, logicInfo) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); // indicate we are using the theory state object and inference manager d_theoryState = &d_astate; - d_inferManager = &d_inferenceManager; + d_inferManager = &d_im; } TheoryArith::~TheoryArith(){ @@ -199,7 +199,7 @@ void TheoryArith::postCheck(Effort level) else if (d_internal->foundNonlinear()) { // set incomplete - d_inferenceManager.setIncomplete(); + d_im.setIncomplete(); } } } @@ -270,7 +270,7 @@ bool TheoryArith::collectModelValues(TheoryModel* m, { Node eq = p.first.eqNode(p.second); Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate()); - d_out->lemma(lem); + d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL); } return false; } @@ -307,7 +307,7 @@ std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit) } eq::ProofEqEngine* TheoryArith::getProofEqEngine() { - return d_inferenceManager.getProofEqEngine(); + return d_im.getProofEqEngine(); } }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 41cc9591d..e0fa1b2d0 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -135,7 +135,7 @@ class TheoryArith : public Theory { /** Return a reference to the arith::InferenceManager. */ InferenceManager& getInferenceManager() { - return d_inferenceManager; + return d_im; } private: @@ -149,7 +149,7 @@ class TheoryArith : public Theory { /** The state object wrapping TheoryArithPrivate */ ArithState d_astate; /** The arith::InferenceManager. */ - InferenceManager d_inferenceManager; + InferenceManager d_im; /** * The non-linear extension, responsible for all approaches for non-linear diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 1faad2a7a..74b13aed1 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -535,9 +535,9 @@ bool TheoryArithPrivate::isProofEnabled() const return d_pnm != nullptr; } -void TheoryArithPrivate::raiseConflict(ConstraintCP a){ +void TheoryArithPrivate::raiseConflict(ConstraintCP a, InferenceId id){ Assert(a->inConflict()); - d_conflicts.push_back(a); + d_conflicts.push_back(std::make_pair(a, id)); } void TheoryArithPrivate::raiseBlackBoxConflict(Node bb, @@ -654,7 +654,7 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){ ConstraintP negation = constraint->getNegation(); negation->impliedByUnate(ubc, true); - raiseConflict(constraint); + raiseConflict(constraint, InferenceId::ARITH_CONF_LOWER); ++(d_statistics.d_statAssertLowerConflicts); return true; @@ -690,7 +690,7 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){ } if(triConflict){ ++(d_statistics.d_statDisequalityConflicts); - raiseConflict(eq); + raiseConflict(eq, InferenceId::ARITH_CONF_TRICHOTOMY); return true; } } @@ -714,7 +714,7 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){ negUb->tryToPropagate(); } if(ubInConflict){ - raiseConflict(ub); + raiseConflict(ub, InferenceId::ARITH_CONF_TRICHOTOMY); return true; }else if(learnNegUb){ d_learnedBounds.push_back(negUb); @@ -795,7 +795,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){ ConstraintP lbc = d_partialModel.getLowerBoundConstraint(x_i); ConstraintP negConstraint = constraint->getNegation(); negConstraint->impliedByUnate(lbc, true); - raiseConflict(constraint); + raiseConflict(constraint, InferenceId::ARITH_CONF_UPPER); ++(d_statistics.d_statAssertUpperConflicts); return true; }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i) @@ -829,7 +829,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){ } if(triConflict){ ++(d_statistics.d_statDisequalityConflicts); - raiseConflict(eq); + raiseConflict(eq, InferenceId::ARITH_CONF_TRICHOTOMY); return true; } } @@ -853,7 +853,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){ negLb->tryToPropagate(); } if(lbInConflict){ - raiseConflict(lb); + raiseConflict(lb, InferenceId::ARITH_CONF_TRICHOTOMY); return true; }else if(learnNegLb){ d_learnedBounds.push_back(negLb); @@ -935,7 +935,7 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){ ConstraintP diseq = constraint->getNegation(); Assert(!diseq->isTrue()); diseq->impliedByUnate(cb, true); - raiseConflict(constraint); + raiseConflict(constraint, InferenceId::ARITH_CONF_EQ); return true; } @@ -1027,7 +1027,7 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){ if(lb->isTrue() && ub->isTrue()){ ConstraintP eq = constraint->getNegation(); eq->impliedByTrichotomy(lb, ub, true); - raiseConflict(constraint); + raiseConflict(constraint, InferenceId::ARITH_CONF_TRICHOTOMY); //in conflict ++(d_statistics.d_statDisequalityConflicts); return true; @@ -1067,7 +1067,7 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){ if(!split && c_i == d_partialModel.getAssignment(x_i)){ Debug("arith::eq") << "lemma now! " << constraint << endl; - outputTrustedLemma(constraint->split()); + outputTrustedLemma(constraint->split(), InferenceId::ARITH_SPLIT_DEQ); return false; }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){ Debug("arith::eq") << "can drop as less than lb" << constraint << endl; @@ -1780,7 +1780,7 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion) Debug("arith::eq") << "negation has proof" << endl; Debug("arith::eq") << constraint << endl; Debug("arith::eq") << negation << endl; - raiseConflict(negation); + raiseConflict(negation, InferenceId::UNKNOWN); return NullConstraint; }else{ return constraint; @@ -1806,7 +1806,7 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){ floorConstraint->impliedByIntTighten(constraint, inConflict); floorConstraint->tryToPropagate(); if(inConflict){ - raiseConflict(floorConstraint); + raiseConflict(floorConstraint, InferenceId::ARITH_TIGHTEN_FLOOR); return true; } } @@ -1826,7 +1826,7 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){ ceilingConstraint->impliedByIntTighten(constraint, inConflict); ceilingConstraint->tryToPropagate(); if(inConflict){ - raiseConflict(ceilingConstraint); + raiseConflict(ceilingConstraint, InferenceId::ARITH_TIGHTEN_CEIL); return true; } } @@ -1932,7 +1932,8 @@ void TheoryArithPrivate::outputConflicts(){ if(!conflictQueueEmpty()){ Assert(!d_conflicts.empty()); for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){ - ConstraintCP confConstraint = d_conflicts[i]; + const std::pair<ConstraintCP, InferenceId>& conf = d_conflicts[i]; + const ConstraintCP& confConstraint = conf.first; bool hasProof = confConstraint->hasProof(); Assert(confConstraint->inConflict()); const ConstraintRule& pf = confConstraint->getConstraintRule(); @@ -1961,11 +1962,11 @@ void TheoryArithPrivate::outputConflicts(){ if (isProofEnabled()) { - outputTrustedConflict(trustedConflict); + outputTrustedConflict(trustedConflict, conf.second); } else { - outputConflict(conflict); + outputConflict(conflict, conf.second); } } } @@ -1982,41 +1983,41 @@ void TheoryArithPrivate::outputConflicts(){ if (isProofEnabled() && d_blackBoxConflictPf.get()) { auto confPf = d_blackBoxConflictPf.get(); - outputTrustedConflict(d_pfGen->mkTrustNode(bb, confPf, true)); + outputTrustedConflict(d_pfGen->mkTrustNode(bb, confPf, true), InferenceId::ARITH_BLACK_BOX); } else { - outputConflict(bb); + outputConflict(bb, InferenceId::ARITH_BLACK_BOX); } } } -void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma) +void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma, InferenceId id) { Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl; - (d_containing.d_out)->trustedLemma(lemma); + d_containing.d_im.trustedLemma(lemma, id); } -void TheoryArithPrivate::outputLemma(TNode lem) { +void TheoryArithPrivate::outputLemma(TNode lem, InferenceId id) { Debug("arith::channel") << "Arith lemma: " << lem << std::endl; - (d_containing.d_out)->lemma(lem); + d_containing.d_im.lemma(lem, id); } -void TheoryArithPrivate::outputTrustedConflict(TrustNode conf) +void TheoryArithPrivate::outputTrustedConflict(TrustNode conf, InferenceId id) { Debug("arith::channel") << "Arith trusted conflict: " << conf << std::endl; - (d_containing.d_out)->trustedConflict(conf); + d_containing.d_im.trustedConflict(conf, id); } -void TheoryArithPrivate::outputConflict(TNode lit) { +void TheoryArithPrivate::outputConflict(TNode lit, InferenceId id) { Debug("arith::channel") << "Arith conflict: " << lit << std::endl; - (d_containing.d_out)->conflict(lit); + d_containing.d_im.conflict(lit, id); } void TheoryArithPrivate::outputPropagate(TNode lit) { Debug("arith::channel") << "Arith propagation: " << lit << std::endl; // call the propagate lit method of the - (d_containing.d_out)->propagate(lit); + d_containing.d_im.propagateLit(lit); } void TheoryArithPrivate::outputRestart() { @@ -2113,7 +2114,7 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){ << " (" << neg_at_j->isTrue() <<") " << neg_at_j << endl << " (" << at_j->isTrue() <<") " << at_j << endl; neg_at_j->impliedByIntHole(vec, true); - raiseConflict(at_j); + raiseConflict(at_j, InferenceId::UNKNOWN); break; } } @@ -2339,7 +2340,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){ conflicts.push_back(ConstraintCPVec()); - intHoleConflictToVector(d_conflicts[i], conflicts.back()); + intHoleConflictToVector(d_conflicts[i].first, conflicts.back()); Constraint::assertionFringe(conflicts.back()); // ConstraintCP conflicting = d_conflicts[i]; @@ -2371,7 +2372,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc if(!contains(conf, bcneg)){ Debug("approx::branch") << "reraise " << conf << endl; ConstraintCP conflicting = vectorToIntHoleConflict(conf); - raiseConflict(conflicting); + raiseConflict(conflicting, InferenceId::UNKNOWN); }else if(!bci.proven()){ drop(conf, bcneg); bci.setExplanation(conf); @@ -2391,7 +2392,7 @@ void TheoryArithPrivate::replayAssert(ConstraintP c) { } Debug("approx::replayAssert") << "replayAssertion " << c << endl; if(inConflict){ - raiseConflict(c); + raiseConflict(c, InferenceId::UNKNOWN); }else{ assertionCases(c); } @@ -2541,7 +2542,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex }else { con->impliedByIntHole(exp, true); Debug("approx::replayLogRec") << "cut into conflict " << con << endl; - raiseConflict(con); + raiseConflict(con, InferenceId::UNKNOWN); } }else{ ++d_statistics.d_cutsProofFailed; @@ -2579,7 +2580,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex /* if a conflict has been found stop */ for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){ res.push_back(ConstraintCPVec()); - intHoleConflictToVector(d_conflicts[i], res.back()); + intHoleConflictToVector(d_conflicts[i].first, res.back()); } ++d_statistics.d_replayLogRecEarlyExit; }else if(nl.isBranch()){ @@ -3552,7 +3553,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) Debug("arith::approx::cuts") << "approximate cut:" << lem << endl; anyFresh = anyFresh || hasFreshArithLiteral(lem.getNode()); Debug("arith::lemma") << "approximate cut:" << lem << endl; - outputTrustedLemma(lem); + outputTrustedLemma(lem, InferenceId::ARITH_APPROX_CUT); } if(anyFresh){ emmittedConflictOrSplit = true; @@ -3669,7 +3670,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) d_hasDoneWorkSinceCut = false; d_cutCount = d_cutCount + 1; Debug("arith::lemma") << "dio cut " << possibleLemma << endl; - outputTrustedLemma(possibleLemma); + outputTrustedLemma(possibleLemma, InferenceId::ARITH_DIO_CUT); } } } @@ -3683,7 +3684,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) emmittedConflictOrSplit = true; Debug("arith::lemma") << "rrbranch lemma" << possibleLemma << endl; - outputTrustedLemma(possibleLemma); + outputTrustedLemma(possibleLemma, InferenceId::ARITH_BB_LEMMA); } } @@ -3693,7 +3694,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) Node decompositionLemma = d_diosolver.nextDecompositionLemma(); Debug("arith::lemma") << "dio decomposition lemma " << decompositionLemma << endl; - outputLemma(decompositionLemma); + outputLemma(decompositionLemma, InferenceId::ARITH_DIO_DECOMPOSITION); } }else{ Debug("arith::restart") << "arith restart!" << endl; @@ -3909,7 +3910,7 @@ bool TheoryArithPrivate::splitDisequalities(){ Debug("arith::lemma") << "Now " << Rewriter::rewrite(lemma.getNode()) << endl; - outputTrustedLemma(lemma); + outputTrustedLemma(lemma, InferenceId::ARITH_SPLIT_DEQ); //cout << "Now " << Rewriter::rewrite(lemma) << endl; splitSomething = true; }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){ @@ -4398,7 +4399,7 @@ void TheoryArithPrivate::presolve(){ for(; i != i_end; ++i){ TrustNode lem = *i; Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl; - outputTrustedLemma(lem); + outputTrustedLemma(lem, InferenceId::UNKNOWN); } } @@ -4843,11 +4844,11 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C // Output it TrustNode trustedClause = d_pfGen->mkTrustNode(clause, clausePf); - outputTrustedLemma(trustedClause); + outputTrustedLemma(trustedClause, InferenceId::UNKNOWN); } else { - outputLemma(clause); + outputLemma(clause, InferenceId::UNKNOWN); } }else{ Assert(!implied->negationHasProof()); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 55a2472b3..5cbf95760 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -309,7 +309,7 @@ private: /** This is only used by simplex at the moment. */ - context::CDList<ConstraintCP> d_conflicts; + context::CDList<std::pair<ConstraintCP, InferenceId>> d_conflicts; /** This is only used by simplex at the moment. */ context::CDO<Node> d_blackBoxConflict; @@ -323,7 +323,7 @@ private: * This adds the constraint a to the queue of conflicts in d_conflicts. * Both a and ~a must have a proof. */ - void raiseConflict(ConstraintCP a); + void raiseConflict(ConstraintCP a, InferenceId id); // inline void raiseConflict(const ConstraintCPVec& cv){ // d_conflicts.push_back(cv); @@ -693,10 +693,10 @@ private: inline TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); } inline void debugPrintFacts() const { d_containing.debugPrintFacts(); } inline context::Context* getSatContext() const { return d_containing.getSatContext(); } - void outputTrustedLemma(TrustNode lem); - void outputLemma(TNode lem); - void outputTrustedConflict(TrustNode conf); - void outputConflict(TNode lit); + void outputTrustedLemma(TrustNode lem, InferenceId id); + void outputLemma(TNode lem, InferenceId id); + void outputTrustedConflict(TrustNode conf, InferenceId id); + void outputConflict(TNode lit, InferenceId id); void outputPropagate(TNode lit); void outputRestart(); diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index f5fda1747..b6d0d3c25 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -38,6 +38,28 @@ namespace theory { enum class InferenceId { // ---------------------------------- arith theory + //-------------------- linear core + // black box conflicts. It's magic. + ARITH_BLACK_BOX, + // conflicting equality + ARITH_CONF_EQ, + // conflicting lower bound + ARITH_CONF_LOWER, + // conflict due to trichotomy + ARITH_CONF_TRICHOTOMY, + // conflicting upper bound + ARITH_CONF_UPPER, + // introduces split on a disequality + ARITH_SPLIT_DEQ, + // tighten integer inequalities to ceiling + ARITH_TIGHTEN_CEIL, + // tighten integer inequalities to floor + ARITH_TIGHTEN_FLOOR, + ARITH_APPROX_CUT, + ARITH_BB_LEMMA, + ARITH_DIO_CUT, + ARITH_DIO_DECOMPOSITION, + ARITH_SPLIT_FOR_NL_MODEL, //-------------------- preprocessing // equivalence of term and its preprocessed form ARITH_PP_ELIM_OPERATORS, diff --git a/src/theory/theory.h b/src/theory/theory.h index 1c23d9041..3a90a8ace 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -458,13 +458,6 @@ class Theory { } /** - * Set the output channel associated to this theory. - */ - void setOutputChannel(OutputChannel& out) { - d_out = &out; - } - - /** * Get the output channel associated to this theory. */ OutputChannel& getOutputChannel() { |