}
}
-void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma, InferenceId id)
+bool TheoryArithPrivate::outputTrustedLemma(TrustNode lemma, InferenceId id)
{
Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl;
- d_containing.d_im.trustedLemma(lemma, id);
+ return d_containing.d_im.trustedLemma(lemma, id);
}
-void TheoryArithPrivate::outputLemma(TNode lem, InferenceId id) {
+bool TheoryArithPrivate::outputLemma(TNode lem, InferenceId id) {
Debug("arith::channel") << "Arith lemma: " << lem << std::endl;
- d_containing.d_im.lemma(lem, id);
+ return d_containing.d_im.lemma(lem, id);
}
void TheoryArithPrivate::outputTrustedConflict(TrustNode conf, InferenceId id)
if(getDioCuttingResource()){
TrustNode possibleLemma = dioCutting();
if(!possibleLemma.isNull()){
- emmittedConflictOrSplit = true;
d_hasDoneWorkSinceCut = false;
d_cutCount = d_cutCount + 1;
Debug("arith::lemma") << "dio cut " << possibleLemma << endl;
- outputTrustedLemma(possibleLemma, InferenceId::ARITH_DIO_CUT);
+ if (outputTrustedLemma(possibleLemma, InferenceId::ARITH_DIO_CUT))
+ {
+ emmittedConflictOrSplit = true;
+ }
}
}
}
{
++(d_statistics.d_externalBranchAndBounds);
d_cutCount = d_cutCount + 1;
- emmittedConflictOrSplit = true;
Debug("arith::lemma") << "rrbranch lemma"
<< possibleLemma << endl;
- outputTrustedLemma(possibleLemma, InferenceId::ARITH_BB_LEMMA);
+ if (outputTrustedLemma(possibleLemma, InferenceId::ARITH_BB_LEMMA))
+ {
+ emmittedConflictOrSplit = true;
+ }
}
}
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, InferenceId id);
- void outputLemma(TNode lem, InferenceId id);
+ bool outputTrustedLemma(TrustNode lem, InferenceId id);
+ bool outputLemma(TNode lem, InferenceId id);
void outputTrustedConflict(TrustNode conf, InferenceId id);
void outputConflict(TNode lit, InferenceId id);
void outputPropagate(TNode lit);
regress1/push-pop/fuzz_7.smt2
regress1/push-pop/fuzz_8.smt2
regress1/push-pop/fuzz_9.smt2
+ regress1/push-pop/issue6773-arith-no-check.smt2
regress1/push-pop/model-unsound-ania.smt2
regress1/push-pop/quant-fun-proc-unmacro.smt2
regress1/push-pop/quant-fun-proc.smt2