summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/arith/callbacks.cpp4
-rw-r--r--src/theory/arith/callbacks.h3
-rw-r--r--src/theory/arith/constraint.cpp2
-rw-r--r--src/theory/arith/nl/nonlinear_extension.cpp2
-rw-r--r--src/theory/arith/simplex.cpp4
-rw-r--r--src/theory/arith/soi_simplex.cpp2
-rw-r--r--src/theory/arith/theory_arith.cpp12
-rw-r--r--src/theory/arith/theory_arith.h4
-rw-r--r--src/theory/arith/theory_arith_private.cpp85
-rw-r--r--src/theory/arith/theory_arith_private.h12
-rw-r--r--src/theory/inference_id.h22
-rw-r--r--src/theory/theory.h7
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() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback