diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index d8e6e536a..85f250933 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -63,6 +63,7 @@ void MainSolver::initialize() { frameTerms.push(logic.getTerm_true()); preprocessor.initialize(); preprocessedAssertionsCountPerFrame.push_back(0); + preprocessedAssertionsPerFrame.push_back(PTRef_Undef); smt_solver->initialize(); pair iorefs{CRef_Undef, CRef_Undef}; smt_solver->addOriginalSMTClause({term_mapper->getOrCreateLit(logic.getTerm_true())}, iorefs); @@ -78,6 +79,7 @@ void MainSolver::push() { preprocessor.push(); frameTerms.push(newFrameTerm(frames.last().getId())); preprocessedAssertionsCountPerFrame.push_back(0); + preprocessedAssertionsPerFrame.push_back(PTRef_Undef); termNames.pushScope(); if (alreadyUnsat) { rememberLastFrameUnsat(); } } @@ -97,6 +99,7 @@ bool MainSolver::pop() { frames.pop(); preprocessor.pop(); preprocessedAssertionsCountPerFrame.pop_back(); + preprocessedAssertionsPerFrame.pop_back(); termNames.popScope(); // goes back to frames.frameCount()-1 only if a formula is added via addAssertion firstNotPreprocessedFrame = std::min(firstNotPreprocessedFrame, frames.frameCount()); @@ -113,8 +116,12 @@ void MainSolver::insertFormula(PTRef fla) { if (logic.getSortRef(fla) != logic.getSort_bool()) { throw ApiException("Top-level assertion sort must be Bool, got " + logic.sortToString(logic.getSortRef(fla))); } - // TODO: Move this to preprocessing of the formulas - fla = IteHandler(logic, getPartitionManager().getNofPartitions()).rewrite(fla); + + if (preprocessItesWhenAsserting()) { + assert(not trackPartitions()); + // Do not use preprocessFormulaItes which assumes to be used within the preprocessing pipeline + fla = IteHandler(logic, pmanager.getNofPartitions()).rewrite(fla); + } if (trackPartitions()) { // MB: Important for HiFrog! partition index is the index of the formula in an virtual array of inserted @@ -165,9 +172,11 @@ bool MainSolver::tryPreprocessFormulasOfFrame(std::size_t i) { auto & frame = frames[i]; FrameId const frameId = frame.getId(); auto & preprocessedFrameAssertionsCount = preprocessedAssertionsCountPerFrame[i]; + auto & preprocessedFrameAssertions = preprocessedAssertionsPerFrame[i]; assert(frame.formulas.size() == 0 or std::size_t(frame.formulas.size()) > preprocessedFrameAssertionsCount); PreprocessingContext context{.frameCount = i, .preprocessedFrameAssertionsCount = preprocessedFrameAssertionsCount, + .preprocessedFrameAssertions = preprocessedFrameAssertions, .perPartition = trackPartitions()}; preprocessor.prepareForProcessingFrame(i); firstNotPreprocessedFrame = i + 1; @@ -178,10 +187,13 @@ bool MainSolver::tryPreprocessFormulasOfFrame(std::size_t i) { if (not context.perPartition) { PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context); status = giveToSolver(frameFormula, frameId); - return status != s_False; + if (status == s_False) { return false; } + preprocessedFrameAssertions = frameFormula; + return true; } vec processedFormulas = preprocessFormulasPerPartition(frame.formulas, context); + // no need to update preprocessedFrameAssertions, not used here for (PTRef fla : processedFormulas) { status = giveToSolver(fla, frameId); if (status == s_False) { return false; } @@ -194,11 +206,38 @@ bool MainSolver::tryPreprocessFormulasOfFrame(std::size_t i) { PTRef MainSolver::preprocessFormulasDefault(vec const & frameFormulas, PreprocessingContext const & context) { assert(not context.perPartition); - if (frameFormulas.size() == 0) { return logic.getTerm_true(); } + std::size_t const frameFormulasCount = frameFormulas.size(); + static_assert(std::is_unsigned_v); + assert(context.preprocessedFrameAssertionsCount <= frameFormulasCount); + std::size_t const formulasCountToProcess = frameFormulasCount - context.preprocessedFrameAssertionsCount; + if (formulasCountToProcess == 0) { return logic.getTerm_true(); } + + bool const processAll = formulasCountToProcess == frameFormulasCount; + + PTRef frameFormula = [&] { + if (processAll) { return logic.mkAnd(frameFormulas); } + + vec processedFormulas; + for (std::size_t i = context.preprocessedFrameAssertionsCount; i < frameFormulasCount; ++i) { + processedFormulas.push(frameFormulas[i]); + } + return logic.mkAnd(std::move(processedFormulas)); + }(); + + // All frame formulas are always somehow preprocessed + preprocessedAssertionsCount += frameFormulas.size(); + + if (processAll) { + assert(context.preprocessedFrameAssertions == PTRef_Undef or + context.preprocessedFrameAssertions == logic.getTerm_true()); + return preprocessFormula(frameFormula, context, {.useCache = true}); + } - // Include even already preprocessed formulas which can still benefit from the new ones - PTRef frameFormula = logic.mkAnd(frameFormulas); - return preprocessFormula(frameFormula, context); + // Still put together with already preprocessed formulas which can still benefit from the new ones + frameFormula = preprocessFormulaItes(frameFormula, context, {.useCache = true}); + assert(context.preprocessedFrameAssertions != PTRef_Undef); + frameFormula = logic.mkAnd(context.preprocessedFrameAssertions, frameFormula); + return preprocessFormula(frameFormula, context, {.skip = true}); } vec MainSolver::preprocessFormulasPerPartition(vec const & frameFormulas, @@ -214,10 +253,16 @@ vec MainSolver::preprocessFormulasPerPartition(vec const & frameFo vec processedFormulas; for (std::size_t i = context.preprocessedFrameAssertionsCount; i < frameFormulasCount; ++i) { PTRef fla = frameFormulas[i]; - PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context); + PTRef processed = fla; + assert(not preprocessItesWhenAsserting()); + // Do not use the cache, it is processed for the first time + processed = preprocessFormulaItes(processed, context, {.useCache = false}); + processed = preprocessFormulaBeforeFinalTheoryPreprocessing(processed, context); processedFormulas.push(processed); } + preprocessedAssertionsCount += processedFormulas.size(); + assert(std::size_t(processedFormulas.size()) == formulasCountToProcess); assert(std::size_t(processedFormulas.size()) > 0); if (std::all_of(processedFormulas.begin(), processedFormulas.end(), @@ -235,8 +280,39 @@ vec MainSolver::preprocessFormulasPerPartition(vec const & frameFo return processedFormulas; } -PTRef MainSolver::preprocessFormula(PTRef fla, PreprocessingContext const & context) { - PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context); +PTRef MainSolver::preprocessFormulaItes(PTRef fla, PreprocessingContext const & context, + PreprocessFormulaItesConfig const & conf) { + if (conf.skip) { return fla; } + if (not conf.useCache) { return preprocessFormulaItesImpl(fla, context); } + + // Ensure that it is not looked up more than once + auto [it, inserted] = iteHandlerCache.try_emplace(fla, PTRef_Undef); + if (not inserted) { return it->second; } + + assert(it->first == fla); + fla = preprocessFormulaItesImpl(fla, context); + assert(fla != PTRef_Undef); + it->second = fla; + return fla; +} + +PTRef MainSolver::preprocessFormulaItesImpl(PTRef fla, PreprocessingContext const & context) { + assert(fla != PTRef_Undef); + + bool const perPartition = context.perPartition; + + std::size_t const partitionNumber = perPartition ? pmanager.getPartitionIndex(fla) : preprocessedAssertionsCount; + PTRef processed = IteHandler(logic, partitionNumber).rewrite(fla); + assert(processed != PTRef_Undef); + if (perPartition) { pmanager.transferPartitionMembership(fla, processed); } + return processed; +} + +PTRef MainSolver::preprocessFormula(PTRef fla, PreprocessingContext const & context, + PreprocessFormulaItesConfig const & iteConfig) { + PTRef processed = fla; + if (not preprocessItesWhenAsserting()) { processed = preprocessFormulaItes(processed, context, iteConfig); } + processed = preprocessFormulaBeforeFinalTheoryPreprocessing(processed, context); preprocessFormulaDoFinalTheoryPreprocessing(context); processed = preprocessFormulaAfterFinalTheoryPreprocessing(processed, context); return processed; @@ -581,6 +657,7 @@ PTRef MainSolver::applyLearntSubstitutions(PTRef fla) { } PTRef MainSolver::substitutionPass(PTRef fla, PreprocessingContext const & context) { + assert(not trackPartitions()); if (not config.do_substitutions()) { return fla; } auto res = computeSubstitutions(fla); vec args; diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 46921daf9..e97ae1c54 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -19,7 +19,11 @@ #include #include +#include #include +#include +#include +#include namespace opensmt { class Logic; @@ -264,7 +268,6 @@ class MainSolver { Theory & getTheory() { return *theory; } Theory const & getTheory() const { return *theory; } TermMapper & getTermMapper() const { return *term_mapper; } - PartitionManager & getPartitionManager() { return pmanager; } // TODO: inefficient vec getCurrentAssertionsViewImpl() const { return getCurrentAssertions(); } @@ -291,12 +294,27 @@ class MainSolver { inline bool trackPartitions() const; + inline bool preprocessItesWhenAsserting() const; + virtual bool tryPreprocessFormulasOfFrame(std::size_t); virtual PTRef preprocessFormulasDefault(vec const & frameFormulas, PreprocessingContext const &); virtual vec preprocessFormulasPerPartition(vec const & frameFormulas, PreprocessingContext const &); - virtual PTRef preprocessFormula(PTRef, PreprocessingContext const &); + struct PreprocessFormulaItesConfig { + bool skip{false}; + bool useCache{false}; + }; + PTRef preprocessFormulaItes(PTRef, PreprocessingContext const &, PreprocessFormulaItesConfig const &); + PTRef preprocessFormulaItes(PTRef fla, PreprocessingContext const & context) { + return preprocessFormulaItes(fla, context, {}); + } + PTRef preprocessFormulaItesImpl(PTRef, PreprocessingContext const &); + + virtual PTRef preprocessFormula(PTRef, PreprocessingContext const &, PreprocessFormulaItesConfig const &); + PTRef preprocessFormula(PTRef fla, PreprocessingContext const & context) { + return preprocessFormula(fla, context, {}); + } virtual PTRef preprocessFormulaBeforeFinalTheoryPreprocessing(PTRef, PreprocessingContext const &); virtual void preprocessFormulaDoFinalTheoryPreprocessing(PreprocessingContext const &); virtual PTRef preprocessFormulaAfterFinalTheoryPreprocessing(PTRef, PreprocessingContext const &); @@ -336,7 +354,11 @@ class MainSolver { vec frameTerms; std::size_t firstNotPreprocessedFrame = 0; std::size_t insertedAssertionsCount = 0; + std::size_t preprocessedAssertionsCount = 0; std::vector preprocessedAssertionsCountPerFrame; + + std::vector preprocessedAssertionsPerFrame; + std::unordered_map iteHandlerCache; }; bool MainSolver::trackPartitions() const { @@ -350,6 +372,21 @@ bool MainSolver::trackPartitions() const { return false; } + +bool MainSolver::preprocessItesWhenAsserting() const { + // We still must keep tracking the terms which only happens in the pipeline + if (trackPartitions()) { return false; } + + // If combining UF, it may be beneficial to introduce the auxiliary ITE variables right away, especially when sat + if (logic.hasUFs()) { + // In UFLIA, it significantly improves + if (logic.hasIntegers()) { return true; } + // In UFLRA, it slightly improves, so it is still worth + if (logic.hasReals()) { return true; } + } + + return false; +} } // namespace opensmt #endif // MAINSOLVER_H diff --git a/src/logics/Theory.h b/src/logics/Theory.h index e1cb4faa3..315e22a31 100644 --- a/src/logics/Theory.h +++ b/src/logics/Theory.h @@ -37,6 +37,7 @@ namespace opensmt { struct PreprocessingContext { std::size_t frameCount {0}; std::size_t preprocessedFrameAssertionsCount{0}; + PTRef preprocessedFrameAssertions{PTRef_Undef}; bool perPartition {false}; }; diff --git a/test/regression/unsatcores/QF_LIA/calypto-1.smt2 b/test/regression/unsatcores/QF_LIA/calypto-1.smt2 new file mode 100644 index 000000000..e9eeba982 --- /dev/null +++ b/test/regression/unsatcores/QF_LIA/calypto-1.smt2 @@ -0,0 +1,26 @@ +(set-option :produce-unsat-cores true) +(set-logic QF_LIA) +(declare-fun x83 () Bool) +(declare-fun x60 () Bool) +(declare-fun x113 () Bool) +(declare-fun x58 () Bool) +(declare-fun x51 () Bool) +(declare-fun x65 () Bool) +(declare-fun x46 () Bool) +(declare-fun x5 () Bool) +(declare-fun x59 () Bool) +(declare-fun x138 () Bool) +(declare-fun x95 () Bool) +(declare-fun x54 () Bool) +(declare-fun x62 () Bool) +(declare-fun x112 () Bool) +(declare-fun x9 () Bool) +(declare-fun x116 () Int) +(declare-fun x49 () Bool) +(declare-fun x40 () Int) +(assert (! (let ((x66 (ite (not x62) x138 false)) (x21 (not x54)) (x26 (not x59))) (let ((x19 (ite x26 (ite x21 x66 true) x66)) (x2 (not x113))) (let ((x64 (not (not x19))) (x50 (ite x2 true false)) (x89 (not x51))) (let ((x82 (ite x64 false (ite x89 x50 true))) (x13 (not x95))) (let ((x80 (ite x13 true false)) (x130 (not x82)) (x121 (not x46))) (let ((x125 (ite x66 1 0)) (x36 (not x66)) (x110 (ite x130 false (ite x121 x80 true)))) (let ((x7 (+ 1 x125))) (let ((x88 (ite x64 x7 (ite (ite x89 (ite x2 x66 false) x66) 1 0)))) (let ((x17 (+ x88 1))) (let ((x102 (ite x130 x17 (ite x121 (ite x13 x88 0) x88)))) (let ((x119 (not x110)) (x123 (+ 1 x102)) (x61 (not x36)) (x37 (not x83)) (x108 (not x5))) (let ((x15 (ite x119 (ite x61 (ite x108 (ite x37 x123 0) x123) x123) (ite x108 (ite x37 x102 0) x102)))) (let ((x107 (+ x15 1))) (let ((x124 (= 2 x107)) (x33 (= x123 2)) (x133 (ite x37 true false))) (let ((x104 (ite x108 x133 true))) (let ((x56 (not x9)) (x8 (ite x119 (ite x61 x104 false) x104))) (let ((x44 (not x60)) (x106 (ite x56 true false))) (let ((x72 (ite x44 x106 true)) (x30 (not x8)) (x32 (not (> 4 x107)))) (let ((x137 (ite x30 (ite x32 x72 false) x72))) (let ((x115 (or (ite x44 (ite x108 (ite x121 (ite x89 (ite x26 x66 false) false) false) false) false) x112)) (x10 (not (or x137 x33))) (x43 (not x65))) (let ((x39 (or (or x10 x115) x65))) (let ((x79 (= 2 x17)) (x122 (not (or (ite x43 (ite x44 (ite x108 (ite x121 (ite x89 (ite x26 x54 false) false) false) false) false) false) x49))) (x63 (not x39)) (x12 (not x115))) (let ((x45 (not (or x79 x8))) (x78 (and x119 x36))) (let ((x28 (and (not x78) (or x78 (not (ite x108 x83 false)))))) (let ((x100 (not x28))) (let ((x29 (and (not x79) x100))) (let ((x68 (not x29))) (let ((x105 (and (or (not (ite x44 x9 false)) x45) x68))) (let ((x134 (not x105))) (let ((x135 (and (not x33) x134))) (let ((x118 (not x135))) (let ((x129 (not x124)) (x23 (and (or (or x65 x12) x10) x118))) (let ((x67 (and x129 (not x23)))) (let ((x93 (ite x21 x125 x7)) (x57 (not x67)) (x114 (not x49))) (let ((x3 (ite x61 x93 (ite x26 x93 0)))) (let ((x42 (ite x2 x3 (+ x3 1)))) (let ((x117 (ite x64 x42 (ite x89 x42 0)))) (let ((x98 (ite x13 x117 (+ x117 1)))) (let ((x127 (ite x130 x98 (ite x121 x98 0)))) (let ((x47 (ite x37 x127 (+ 1 x127)))) (let ((x31 (ite x108 x47 0))) (let ((x1 (ite x119 (ite x61 x31 x47) x31))) (let ((x91 (ite x56 x1 (+ x1 1)))) (let ((x14 (ite x44 x91 0))) (let ((x131 (ite x30 (ite x32 x14 x91) x14))) (let ((x4 (not (ite x61 (ite x21 x66 false) x19))) (x109 (< (ite (< x131 4) x131 (- x131 8)) 0)) (x86 (not (or x50 x82)))) (let ((x71 (not (or (not (or x86 x4)) (and x86 x4))))) (let ((x25 (or (not (or x71 (not (and x80 x119)))) (and (not (or x80 x110)) x71)))) (let ((x84 (not x25)) (x74 (not (or x78 x108)))) (let ((x140 (or (or (not (or (not (and x133 x100)) x84)) (and x25 x74)) (and x84 (not (or x133 x28))))) (x126 (not (or x5 (or x78 x83))))) (let ((x101 (not (and (not (and x140 x79)) (not (and x126 (and x66 x25))))))) (let ((x136 (and (not (and x29 x140)) (not (and x101 x68))))) (let ((x97 (not (or x133 x84))) (x55 (not (or x71 x80))) (x6 (not (or (not (or x21 x36)) (not (or x50 x4))))) (x120 (not (or x106 x136)))) (let ((x76 (or (not (or x55 x6)) (and x55 x6)))) (let ((x18 (not x76))) (let ((x52 (not (and (or (not (or (and x18 x97) (not (or x18 x97)))) x28) (not (and x74 x76))))) (x35 (and (and x76 x66) x126))) (let ((x96 (not (and (not (and x35 x126)) (not (and x79 x52)))))) (let ((x69 (or x60 (or x45 x9))) (x75 (and (not (and x96 x68)) (not (and x29 x52))))) (let ((x85 (and x105 x69))) (let ((x73 (or x105 x106)) (x38 (not (and (not (and x52 x85)) (or (not (or (and x75 x120) (not (or x120 x75)))) x105)))) (x16 (not x69))) (let ((x22 (not x112)) (x48 (or (and x136 (not x73)) (or (not (or (not (and x106 x134)) x136)) (and x140 x85))))) (let ((x20 (and (not (or (and (not (and (not (and (not (and x33 x48)) (not (and x101 x16)))) x118)) (not (and x48 x135))) x22)) (not (and (not (and x118 (not (and (not (and x16 (not (and (not (and x85 x35)) (not (and x16 x96)))))) (not (and x38 x33)))))) (not (and x38 x135)))))) (x53 (> 0 (ite (> 4 x127) x127 (- x127 8))))) (let ((x70 (and x53 x126)) (x92 (not (and (not (and x53 x74)) (or (and (not (and x76 x97)) (not x53)) x28))))) (let ((x24 (not (and (not x70) (not (and x79 x92)))))) (let ((x77 (and (not x75) x120)) (x87 (and (not (and x24 x68)) (not (and x29 x92))))) (let ((x34 (not (and (or x105 (and (not (and (not x87) (not x77))) (not (and x87 x77)))) (not (and x92 x85))))) (x132 (not (and x24 x16)))) (let ((x139 (and x39 x23)) (x90 (not (and x132 (not (and x33 x34)))))) (let ((x27 (ite x30 (ite x32 (ite x44 (ite x56 x107 0) x107) x107) (ite x44 (ite x56 x15 0) x15))) (x94 (not (and (or (and (not (and x109 (not x20))) (not (and x20 (and (not (and x90 x118)) (not (and x34 x135)))))) x23) (not (and x139 x34)))))) (let ((x103 (+ x27 1))) (let ((x141 (ite x22 false x109)) (x11 (ite x22 x131 (+ x131 1))) (x41 (not x137)) (x99 (not (< x103 4)))) (let ((x111 (ite x43 x11 0))) (let ((x81 (ite x41 (ite x99 x111 x11) x111))) (let ((x128 (ite x114 false (< (ite (< x81 4) x81 (- x81 8)) 0)))) (= (- (ite (not (or (or x114 (and (or (not (or x124 (or x63 (not (or x10 x43))))) (or x122 x58)) x57)) (and (not (and x67 x94)) (not (and (not (and (not (and x124 x94)) (not (and (not (and (not (and (not (and (not (and x70 x85)) x132)) x139)) (not (and x63 x90)))) (and x63 x129))))) x57))))) 1 0) (ite (ite (not (< (+ (ite x41 (ite x99 (ite x43 (ite x12 x103 0) x103) x103) (ite x43 (ite x12 x27 0) x27)) 1) 4)) (ite (not x58) (ite x122 (ite x99 (ite x43 (ite x12 (not (or x73 x87)) x141) false) x141) x128) false) x128) 1 0)) (+ x116 (* 128 x40)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) :named smtcomp1)) +(assert (! (> 128 x116) :named smtcomp2)) +(assert (! (< 0 x116) :named smtcomp3)) +(check-sat) +(get-unsat-core) +(exit) diff --git a/test/regression/unsatcores/QF_LIA/calypto-1.smt2.expected.err b/test/regression/unsatcores/QF_LIA/calypto-1.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/unsatcores/QF_LIA/calypto-1.smt2.expected.out b/test/regression/unsatcores/QF_LIA/calypto-1.smt2.expected.out new file mode 100644 index 000000000..afea5bb78 --- /dev/null +++ b/test/regression/unsatcores/QF_LIA/calypto-1.smt2.expected.out @@ -0,0 +1,6 @@ +unsat +( +smtcomp1 +smtcomp2 +smtcomp3 +) diff --git a/test/regression/unsatcores/QF_LIA/calypto-1_min.smt2 b/test/regression/unsatcores/QF_LIA/calypto-1_min.smt2 new file mode 100644 index 000000000..3682b3430 --- /dev/null +++ b/test/regression/unsatcores/QF_LIA/calypto-1_min.smt2 @@ -0,0 +1,27 @@ +(set-option :produce-unsat-cores true) +(set-option :minimal-unsat-cores true) +(set-logic QF_LIA) +(declare-fun x83 () Bool) +(declare-fun x60 () Bool) +(declare-fun x113 () Bool) +(declare-fun x58 () Bool) +(declare-fun x51 () Bool) +(declare-fun x65 () Bool) +(declare-fun x46 () Bool) +(declare-fun x5 () Bool) +(declare-fun x59 () Bool) +(declare-fun x138 () Bool) +(declare-fun x95 () Bool) +(declare-fun x54 () Bool) +(declare-fun x62 () Bool) +(declare-fun x112 () Bool) +(declare-fun x9 () Bool) +(declare-fun x116 () Int) +(declare-fun x49 () Bool) +(declare-fun x40 () Int) +(assert (! (let ((x66 (ite (not x62) x138 false)) (x21 (not x54)) (x26 (not x59))) (let ((x19 (ite x26 (ite x21 x66 true) x66)) (x2 (not x113))) (let ((x64 (not (not x19))) (x50 (ite x2 true false)) (x89 (not x51))) (let ((x82 (ite x64 false (ite x89 x50 true))) (x13 (not x95))) (let ((x80 (ite x13 true false)) (x130 (not x82)) (x121 (not x46))) (let ((x125 (ite x66 1 0)) (x36 (not x66)) (x110 (ite x130 false (ite x121 x80 true)))) (let ((x7 (+ 1 x125))) (let ((x88 (ite x64 x7 (ite (ite x89 (ite x2 x66 false) x66) 1 0)))) (let ((x17 (+ x88 1))) (let ((x102 (ite x130 x17 (ite x121 (ite x13 x88 0) x88)))) (let ((x119 (not x110)) (x123 (+ 1 x102)) (x61 (not x36)) (x37 (not x83)) (x108 (not x5))) (let ((x15 (ite x119 (ite x61 (ite x108 (ite x37 x123 0) x123) x123) (ite x108 (ite x37 x102 0) x102)))) (let ((x107 (+ x15 1))) (let ((x124 (= 2 x107)) (x33 (= x123 2)) (x133 (ite x37 true false))) (let ((x104 (ite x108 x133 true))) (let ((x56 (not x9)) (x8 (ite x119 (ite x61 x104 false) x104))) (let ((x44 (not x60)) (x106 (ite x56 true false))) (let ((x72 (ite x44 x106 true)) (x30 (not x8)) (x32 (not (> 4 x107)))) (let ((x137 (ite x30 (ite x32 x72 false) x72))) (let ((x115 (or (ite x44 (ite x108 (ite x121 (ite x89 (ite x26 x66 false) false) false) false) false) x112)) (x10 (not (or x137 x33))) (x43 (not x65))) (let ((x39 (or (or x10 x115) x65))) (let ((x79 (= 2 x17)) (x122 (not (or (ite x43 (ite x44 (ite x108 (ite x121 (ite x89 (ite x26 x54 false) false) false) false) false) false) x49))) (x63 (not x39)) (x12 (not x115))) (let ((x45 (not (or x79 x8))) (x78 (and x119 x36))) (let ((x28 (and (not x78) (or x78 (not (ite x108 x83 false)))))) (let ((x100 (not x28))) (let ((x29 (and (not x79) x100))) (let ((x68 (not x29))) (let ((x105 (and (or (not (ite x44 x9 false)) x45) x68))) (let ((x134 (not x105))) (let ((x135 (and (not x33) x134))) (let ((x118 (not x135))) (let ((x129 (not x124)) (x23 (and (or (or x65 x12) x10) x118))) (let ((x67 (and x129 (not x23)))) (let ((x93 (ite x21 x125 x7)) (x57 (not x67)) (x114 (not x49))) (let ((x3 (ite x61 x93 (ite x26 x93 0)))) (let ((x42 (ite x2 x3 (+ x3 1)))) (let ((x117 (ite x64 x42 (ite x89 x42 0)))) (let ((x98 (ite x13 x117 (+ x117 1)))) (let ((x127 (ite x130 x98 (ite x121 x98 0)))) (let ((x47 (ite x37 x127 (+ 1 x127)))) (let ((x31 (ite x108 x47 0))) (let ((x1 (ite x119 (ite x61 x31 x47) x31))) (let ((x91 (ite x56 x1 (+ x1 1)))) (let ((x14 (ite x44 x91 0))) (let ((x131 (ite x30 (ite x32 x14 x91) x14))) (let ((x4 (not (ite x61 (ite x21 x66 false) x19))) (x109 (< (ite (< x131 4) x131 (- x131 8)) 0)) (x86 (not (or x50 x82)))) (let ((x71 (not (or (not (or x86 x4)) (and x86 x4))))) (let ((x25 (or (not (or x71 (not (and x80 x119)))) (and (not (or x80 x110)) x71)))) (let ((x84 (not x25)) (x74 (not (or x78 x108)))) (let ((x140 (or (or (not (or (not (and x133 x100)) x84)) (and x25 x74)) (and x84 (not (or x133 x28))))) (x126 (not (or x5 (or x78 x83))))) (let ((x101 (not (and (not (and x140 x79)) (not (and x126 (and x66 x25))))))) (let ((x136 (and (not (and x29 x140)) (not (and x101 x68))))) (let ((x97 (not (or x133 x84))) (x55 (not (or x71 x80))) (x6 (not (or (not (or x21 x36)) (not (or x50 x4))))) (x120 (not (or x106 x136)))) (let ((x76 (or (not (or x55 x6)) (and x55 x6)))) (let ((x18 (not x76))) (let ((x52 (not (and (or (not (or (and x18 x97) (not (or x18 x97)))) x28) (not (and x74 x76))))) (x35 (and (and x76 x66) x126))) (let ((x96 (not (and (not (and x35 x126)) (not (and x79 x52)))))) (let ((x69 (or x60 (or x45 x9))) (x75 (and (not (and x96 x68)) (not (and x29 x52))))) (let ((x85 (and x105 x69))) (let ((x73 (or x105 x106)) (x38 (not (and (not (and x52 x85)) (or (not (or (and x75 x120) (not (or x120 x75)))) x105)))) (x16 (not x69))) (let ((x22 (not x112)) (x48 (or (and x136 (not x73)) (or (not (or (not (and x106 x134)) x136)) (and x140 x85))))) (let ((x20 (and (not (or (and (not (and (not (and (not (and x33 x48)) (not (and x101 x16)))) x118)) (not (and x48 x135))) x22)) (not (and (not (and x118 (not (and (not (and x16 (not (and (not (and x85 x35)) (not (and x16 x96)))))) (not (and x38 x33)))))) (not (and x38 x135)))))) (x53 (> 0 (ite (> 4 x127) x127 (- x127 8))))) (let ((x70 (and x53 x126)) (x92 (not (and (not (and x53 x74)) (or (and (not (and x76 x97)) (not x53)) x28))))) (let ((x24 (not (and (not x70) (not (and x79 x92)))))) (let ((x77 (and (not x75) x120)) (x87 (and (not (and x24 x68)) (not (and x29 x92))))) (let ((x34 (not (and (or x105 (and (not (and (not x87) (not x77))) (not (and x87 x77)))) (not (and x92 x85))))) (x132 (not (and x24 x16)))) (let ((x139 (and x39 x23)) (x90 (not (and x132 (not (and x33 x34)))))) (let ((x27 (ite x30 (ite x32 (ite x44 (ite x56 x107 0) x107) x107) (ite x44 (ite x56 x15 0) x15))) (x94 (not (and (or (and (not (and x109 (not x20))) (not (and x20 (and (not (and x90 x118)) (not (and x34 x135)))))) x23) (not (and x139 x34)))))) (let ((x103 (+ x27 1))) (let ((x141 (ite x22 false x109)) (x11 (ite x22 x131 (+ x131 1))) (x41 (not x137)) (x99 (not (< x103 4)))) (let ((x111 (ite x43 x11 0))) (let ((x81 (ite x41 (ite x99 x111 x11) x111))) (let ((x128 (ite x114 false (< (ite (< x81 4) x81 (- x81 8)) 0)))) (= (- (ite (not (or (or x114 (and (or (not (or x124 (or x63 (not (or x10 x43))))) (or x122 x58)) x57)) (and (not (and x67 x94)) (not (and (not (and (not (and x124 x94)) (not (and (not (and (not (and (not (and (not (and x70 x85)) x132)) x139)) (not (and x63 x90)))) (and x63 x129))))) x57))))) 1 0) (ite (ite (not (< (+ (ite x41 (ite x99 (ite x43 (ite x12 x103 0) x103) x103) (ite x43 (ite x12 x27 0) x27)) 1) 4)) (ite (not x58) (ite x122 (ite x99 (ite x43 (ite x12 (not (or x73 x87)) x141) false) x141) x128) false) x128) 1 0)) (+ x116 (* 128 x40)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) :named smtcomp1)) +(assert (! (> 128 x116) :named smtcomp2)) +(assert (! (< 0 x116) :named smtcomp3)) +(check-sat) +(get-unsat-core) +(exit) diff --git a/test/regression/unsatcores/QF_LIA/calypto-1_min.smt2.expected.err b/test/regression/unsatcores/QF_LIA/calypto-1_min.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/unsatcores/QF_LIA/calypto-1_min.smt2.expected.out b/test/regression/unsatcores/QF_LIA/calypto-1_min.smt2.expected.out new file mode 100644 index 000000000..afea5bb78 --- /dev/null +++ b/test/regression/unsatcores/QF_LIA/calypto-1_min.smt2.expected.out @@ -0,0 +1,6 @@ +unsat +( +smtcomp1 +smtcomp2 +smtcomp3 +) diff --git a/test/regression/unsatcores/generic/ite-1.smt2 b/test/regression/unsatcores/generic/ite-1.smt2 new file mode 100644 index 000000000..84b637d5c --- /dev/null +++ b/test/regression/unsatcores/generic/ite-1.smt2 @@ -0,0 +1,6 @@ +(set-option :produce-unsat-cores true) +(set-logic QF_UF) +(declare-const A Bool) +(assert (! (ite A (not A) A) :named n)) +(check-sat) +(get-unsat-core) diff --git a/test/regression/unsatcores/generic/ite-1.smt2.expected.err b/test/regression/unsatcores/generic/ite-1.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/unsatcores/generic/ite-1.smt2.expected.out b/test/regression/unsatcores/generic/ite-1.smt2.expected.out new file mode 100644 index 000000000..629143400 --- /dev/null +++ b/test/regression/unsatcores/generic/ite-1.smt2.expected.out @@ -0,0 +1,4 @@ +unsat +( +n +) diff --git a/test/regression/unsatcores/generic/ite-2.smt2 b/test/regression/unsatcores/generic/ite-2.smt2 new file mode 100644 index 000000000..e7f00481a --- /dev/null +++ b/test/regression/unsatcores/generic/ite-2.smt2 @@ -0,0 +1,9 @@ +(set-option :produce-unsat-cores true) +(set-logic QF_UF) +(declare-const A Bool) +(declare-const B Bool) +(declare-const C Bool) +(assert (! (= A B) :named n1)) +(assert (! (ite C (not (=> A B)) (not (=> B A))) :named n2)) +(check-sat) +(get-unsat-core) diff --git a/test/regression/unsatcores/generic/ite-2.smt2.expected.err b/test/regression/unsatcores/generic/ite-2.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/unsatcores/generic/ite-2.smt2.expected.out b/test/regression/unsatcores/generic/ite-2.smt2.expected.out new file mode 100644 index 000000000..139e56e41 --- /dev/null +++ b/test/regression/unsatcores/generic/ite-2.smt2.expected.out @@ -0,0 +1,5 @@ +unsat +( +n1 +n2 +) diff --git a/test/unit/test_UnsatCore.cc b/test/unit/test_UnsatCore.cc index 73275562c..cee9909ac 100644 --- a/test/unit/test_UnsatCore.cc +++ b/test/unit/test_UnsatCore.cc @@ -383,6 +383,245 @@ TEST_F(FullUFUnsatCoreTest, Full_Bool_ReuseProofChain) { EXPECT_FALSE(isInCore(b4, coreTerms)); } +TEST_F(UFUnsatCoreTest, Bool_Trivial_ITE) { + MainSolver solver = makeSolver(); + PTRef ite = logic.mkIte(b1, nb1, b1); + solver.tryAddNamedAssertion(ite, "a"); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 1); + EXPECT_TRUE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 1); + EXPECT_TRUE(isNameInCore("a", coreNames)); +} + +TEST_F(UFUnsatCoreTest, Bool_Trivial_ITE_Unnamed) { + MainSolver solver = makeSolver(); + PTRef ite = logic.mkIte(b1, nb1, b1); + solver.addAssertion(ite); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 0); + EXPECT_FALSE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 0); + EXPECT_FALSE(isNameInCore("a", coreNames)); +} + +TEST_F(MinUFUnsatCoreTest, Min_Bool_Trivial_ITE) { + MainSolver solver = makeSolver(); + PTRef ite = logic.mkIte(b1, nb1, b1); + solver.tryAddNamedAssertion(ite, "a"); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 1); + EXPECT_TRUE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 1); + EXPECT_TRUE(isNameInCore("a", coreNames)); +} + +TEST_F(MinUFUnsatCoreTest, Min_Bool_Trivial_ITE_Unnamed) { + MainSolver solver = makeSolver(); + PTRef ite = logic.mkIte(b1, nb1, b1); + solver.addAssertion(ite); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 0); + EXPECT_FALSE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 0); + EXPECT_FALSE(isNameInCore("a", coreNames)); +} + +TEST_F(FullUFUnsatCoreTest, Full_Bool_Trivial_ITE) { + MainSolver solver = makeSolver(); + PTRef ite = logic.mkIte(b1, nb1, b1); + solver.addAssertion(ite); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 1); + EXPECT_TRUE(isInCore(ite, coreTerms)); +} + +TEST_F(UFUnsatCoreTest, Bool_Simple_ITE) { + MainSolver solver = makeSolver(); + PTRef eq = logic.mkEq(b1, b2); + PTRef impl1 = logic.mkImpl(b1, b2); + PTRef impl2 = logic.mkImpl(b2, b1); + PTRef nimpl1 = logic.mkNot(impl1); + PTRef nimpl2 = logic.mkNot(impl2); + PTRef ite = logic.mkIte(b3, nimpl1, nimpl2); + solver.tryAddNamedAssertion(eq, "a1"); + solver.tryAddNamedAssertion(ite, "a2"); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 2); + EXPECT_TRUE(isInCore(eq, coreTerms)); + EXPECT_TRUE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 2); + EXPECT_TRUE(isNameInCore("a1", coreNames)); + EXPECT_TRUE(isNameInCore("a2", coreNames)); +} + +TEST_F(UFUnsatCoreTest, Bool_Simple_ITE_Unnamed1) { + MainSolver solver = makeSolver(); + PTRef eq = logic.mkEq(b1, b2); + PTRef impl1 = logic.mkImpl(b1, b2); + PTRef impl2 = logic.mkImpl(b2, b1); + PTRef nimpl1 = logic.mkNot(impl1); + PTRef nimpl2 = logic.mkNot(impl2); + PTRef ite = logic.mkIte(b3, nimpl1, nimpl2); + solver.addAssertion(eq); + solver.tryAddNamedAssertion(ite, "a2"); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 1); + EXPECT_FALSE(isInCore(eq, coreTerms)); + EXPECT_TRUE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 1); + EXPECT_FALSE(isNameInCore("a1", coreNames)); + EXPECT_TRUE(isNameInCore("a2", coreNames)); +} + +TEST_F(UFUnsatCoreTest, Bool_Simple_ITE_Unnamed2) { + MainSolver solver = makeSolver(); + PTRef eq = logic.mkEq(b1, b2); + PTRef impl1 = logic.mkImpl(b1, b2); + PTRef impl2 = logic.mkImpl(b2, b1); + PTRef nimpl1 = logic.mkNot(impl1); + PTRef nimpl2 = logic.mkNot(impl2); + PTRef ite = logic.mkIte(b3, nimpl1, nimpl2); + solver.tryAddNamedAssertion(eq, "a1"); + solver.addAssertion(ite); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 1); + EXPECT_TRUE(isInCore(eq, coreTerms)); + EXPECT_FALSE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 1); + EXPECT_TRUE(isNameInCore("a1", coreNames)); + EXPECT_FALSE(isNameInCore("a2", coreNames)); +} + +TEST_F(MinUFUnsatCoreTest, Min_Bool_Simple_ITE) { + MainSolver solver = makeSolver(); + PTRef eq = logic.mkEq(b1, b2); + PTRef impl1 = logic.mkImpl(b1, b2); + PTRef impl2 = logic.mkImpl(b2, b1); + PTRef nimpl1 = logic.mkNot(impl1); + PTRef nimpl2 = logic.mkNot(impl2); + PTRef ite = logic.mkIte(b3, nimpl1, nimpl2); + solver.tryAddNamedAssertion(eq, "a1"); + solver.tryAddNamedAssertion(ite, "a2"); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 2); + EXPECT_TRUE(isInCore(eq, coreTerms)); + EXPECT_TRUE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 2); + EXPECT_TRUE(isNameInCore("a1", coreNames)); + EXPECT_TRUE(isNameInCore("a2", coreNames)); +} + +TEST_F(MinUFUnsatCoreTest, Min_Bool_Simple_ITE_Unnamed1) { + MainSolver solver = makeSolver(); + PTRef eq = logic.mkEq(b1, b2); + PTRef impl1 = logic.mkImpl(b1, b2); + PTRef impl2 = logic.mkImpl(b2, b1); + PTRef nimpl1 = logic.mkNot(impl1); + PTRef nimpl2 = logic.mkNot(impl2); + PTRef ite = logic.mkIte(b3, nimpl1, nimpl2); + solver.addAssertion(eq); + solver.tryAddNamedAssertion(ite, "a2"); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 1); + EXPECT_FALSE(isInCore(eq, coreTerms)); + EXPECT_TRUE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 1); + EXPECT_FALSE(isNameInCore("a1", coreNames)); + EXPECT_TRUE(isNameInCore("a2", coreNames)); +} + +TEST_F(MinUFUnsatCoreTest, Min_Bool_Simple_ITE_Unnamed2) { + MainSolver solver = makeSolver(); + PTRef eq = logic.mkEq(b1, b2); + PTRef impl1 = logic.mkImpl(b1, b2); + PTRef impl2 = logic.mkImpl(b2, b1); + PTRef nimpl1 = logic.mkNot(impl1); + PTRef nimpl2 = logic.mkNot(impl2); + PTRef ite = logic.mkIte(b3, nimpl1, nimpl2); + solver.tryAddNamedAssertion(eq, "a1"); + solver.addAssertion(ite); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 1); + EXPECT_TRUE(isInCore(eq, coreTerms)); + EXPECT_FALSE(isInCore(ite, coreTerms)); + auto const & namedCore = static_cast(*core); + auto coreNames = namedCore.makeTermNames(); + ASSERT_EQ(coreNames.size(), 1); + EXPECT_TRUE(isNameInCore("a1", coreNames)); + EXPECT_FALSE(isNameInCore("a2", coreNames)); +} + +TEST_F(FullUFUnsatCoreTest, Full_Bool_Simple_ITE) { + MainSolver solver = makeSolver(); + PTRef eq = logic.mkEq(b1, b2); + PTRef impl1 = logic.mkImpl(b1, b2); + PTRef impl2 = logic.mkImpl(b2, b1); + PTRef nimpl1 = logic.mkNot(impl1); + PTRef nimpl2 = logic.mkNot(impl2); + PTRef ite = logic.mkIte(b3, nimpl1, nimpl2); + solver.addAssertion(eq); + solver.addAssertion(ite); + auto res = solver.check(); + ASSERT_EQ(res, s_False); + auto core = solver.getUnsatCore(); + auto & coreTerms = core->getTerms(); + ASSERT_EQ(coreTerms.size(), 2); + EXPECT_TRUE(isInCore(eq, coreTerms)); + EXPECT_TRUE(isInCore(ite, coreTerms)); +} + TEST_F(UFUnsatCoreTest, UF_Simple) { // a1 := x = y // a2 := g(x,y) = g(y,x)