From e575257fdbbd343951ea8d160e76dd256645e1a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Thu, 6 Nov 2025 11:24:40 +0100 Subject: [PATCH 1/3] Split simplifyFormulas to sub-functions This makes the preprocessing more maintainable, allows overriding particular parts and also allows preprocessing single formulas without necessarily giving them to the SMT solver Also added `preprocess` as an alias to `simplifyFormulas` --- src/api/MainSolver.cc | 155 ++++++++++++++++++++++++++++++------------ src/api/MainSolver.h | 10 +++ 2 files changed, 121 insertions(+), 44 deletions(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 4aa9afe73..56aa3bf7e 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -140,63 +140,126 @@ bool MainSolver::tryAddTermNameFor(PTRef fla, std::string const & name) { sstat MainSolver::simplifyFormulas() { status = s_Undef; - for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount() && status != s_False; i++) { + for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount(); ++i) { + auto & frame = frames[i]; + FrameId const frameId = frame.getId(); PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()}; preprocessor.prepareForProcessingFrame(i); firstNotSimplifiedFrame = i + 1; - if (context.perPartition) { - vec frameFormulas; - for (PTRef fla : frames[i].formulas) { - PTRef processed = theory->preprocessAfterSubstitutions(fla, context); - pmanager.transferPartitionMembership(fla, processed); - frameFormulas.push(processed); - preprocessor.addPreprocessedFormula(processed); - } - if (frameFormulas.size() == 0 or std::all_of(frameFormulas.begin(), frameFormulas.end(), - [&](PTRef fla) { return fla == logic.getTerm_true(); })) { - continue; - } - theory->afterPreprocessing(preprocessor.getPreprocessedFormulas()); - for (PTRef fla : frameFormulas) { - if (fla == logic.getTerm_true()) { continue; } - assert(pmanager.getPartitionIndex(fla) != -1); - // Optimize the dag for cnfization - if (logic.isBooleanOperator(fla)) { - PTRef old = fla; - fla = rewriteMaxArity(fla); - pmanager.transferPartitionMembership(old, fla); - } - assert(pmanager.getPartitionIndex(fla) != -1); - pmanager.propagatePartitionMask(fla); - status = giveToSolver(fla, frames[i].getId()); - if (status == s_False) { break; } - } + + if (not context.perPartition) { + PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context); + status = giveToSolver(frameFormula, frameId); } else { - PTRef frameFormula = logic.mkAnd(frames[i].formulas); - if (context.frameCount > 0) { frameFormula = applyLearntSubstitutions(frameFormula); } - frameFormula = theory->preprocessBeforeSubstitutions(frameFormula, context); - frameFormula = substitutionPass(frameFormula, context); - frameFormula = theory->preprocessAfterSubstitutions(frameFormula, context); - - if (logic.isFalse(frameFormula)) { - giveToSolver(logic.getTerm_false(), frames[i].getId()); - status = s_False; - break; + vec processedFormulas = preprocessFormulasPerPartition(frame.formulas, context); + for (PTRef fla : processedFormulas) { + status = giveToSolver(fla, frameId); + if (status == s_False) { break; } } - preprocessor.addPreprocessedFormula(frameFormula); - theory->afterPreprocessing(preprocessor.getPreprocessedFormulas()); - // Optimize the dag for cnfization - if (logic.isBooleanOperator(frameFormula)) { frameFormula = rewriteMaxArity(frameFormula); } - status = giveToSolver(frameFormula, frames[i].getId()); } + if (status == s_False) { break; } } + if (status == s_False) { assert(firstNotSimplifiedFrame > 0); rememberUnsatFrame(firstNotSimplifiedFrame - 1); } + return status; } +PTRef MainSolver::preprocessFormulasDefault(vec const & frameFormulas, PreprocessingContext const & context) { + assert(not context.perPartition); + + if (frameFormulas.size() == 0) { return logic.getTerm_true(); } + + PTRef frameFormula = logic.mkAnd(frameFormulas); + return preprocessFormula(frameFormula, context); +} + +vec MainSolver::preprocessFormulasPerPartition(vec const & frameFormulas, + PreprocessingContext const & context) { + assert(context.perPartition); + + if (frameFormulas.size() == 0) { return {}; } + + vec processedFormulas; + for (PTRef fla : frameFormulas) { + PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context); + processedFormulas.push(processed); + } + + assert(processedFormulas.size() == frameFormulas.size()); + assert(processedFormulas.size() > 0); + if (std::all_of(processedFormulas.begin(), processedFormulas.end(), + [&](PTRef fla) { return fla == logic.getTerm_true(); })) { + return {}; + } + + preprocessFormulaDoFinalTheoryPreprocessing(context); + + for (PTRef & fla : processedFormulas) { + if (fla == logic.getTerm_true()) { continue; } + fla = preprocessFormulaAfterFinalTheoryPreprocessing(fla, context); + } + + return processedFormulas; +} + +PTRef MainSolver::preprocessFormula(PTRef fla, PreprocessingContext const & context) { + PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context); + preprocessFormulaDoFinalTheoryPreprocessing(context); + processed = preprocessFormulaAfterFinalTheoryPreprocessing(processed, context); + return processed; +} + +PTRef MainSolver::preprocessFormulaBeforeFinalTheoryPreprocessing(PTRef fla, PreprocessingContext const & context) { + bool const perPartition = context.perPartition; + PTRef processed = fla; + + if (not perPartition) { + if (context.frameCount > 0) { processed = applyLearntSubstitutions(processed); } + processed = theory->preprocessBeforeSubstitutions(processed, context); + processed = substitutionPass(processed, context); + } + + processed = theory->preprocessAfterSubstitutions(processed, context); + + if (perPartition) { + pmanager.transferPartitionMembership(fla, processed); + } else if (logic.isFalse(processed)) { + return logic.getTerm_false(); + } + + preprocessor.addPreprocessedFormula(processed); + + return processed; +} + +void MainSolver::preprocessFormulaDoFinalTheoryPreprocessing(PreprocessingContext const &) { + theory->afterPreprocessing(preprocessor.getPreprocessedFormulas()); +} + +PTRef MainSolver::preprocessFormulaAfterFinalTheoryPreprocessing(PTRef fla, PreprocessingContext const & context) { + bool const perPartition = context.perPartition; + PTRef processed = fla; + + assert(not perPartition or pmanager.getPartitionIndex(processed) != -1); + + // Optimize the dag for cnfization + if (logic.isBooleanOperator(processed)) { + processed = rewriteMaxArity(processed); + if (perPartition) { pmanager.transferPartitionMembership(fla, processed); } + } + + if (perPartition) { + assert(pmanager.getPartitionIndex(processed) != -1); + pmanager.propagatePartitionMask(processed); + } + + return processed; +} + vec MainSolver::getCurrentAssertions() const { vec assertions; size_t const cnt = frames.frameCount(); @@ -316,11 +379,15 @@ sstat MainSolver::giveToSolver(PTRef root, FrameId push_id) { std::vector> clauses; void operator()(vec && c) override { clauses.push_back(std::move(c)); } }; + + if (root == logic.getTerm_true()) { return s_Undef; } + ClauseCallBack callBack; ts.setClauseCallBack(&callBack); ts.Cnfizer::cnfize(root, push_id); bool const keepPartitionsSeparate = trackPartitions(); - Lit frameLit = push_id == 0 ? Lit{} : term_mapper->getOrCreateLit(frameTerms[push_id]); + Lit frameLit; + if (push_id != 0) { frameLit = term_mapper->getOrCreateLit(frameTerms[push_id]); } int partitionIndex = keepPartitionsSeparate ? pmanager.getPartitionIndex(root) : -1; for (auto & clause : callBack.clauses) { if (push_id != 0) { clause.push(frameLit); } diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 396fff93a..996860ec6 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -105,6 +105,8 @@ class MainSolver { // Simplify formulas until all are simplified or the instance is detected unsat // Skip assertion levels that have already been simplified sstat simplifyFormulas(); + // Alias for `simplifyFormulas`, reserved for future use + sstat preprocess() { return simplifyFormulas(); } [[nodiscard]] sstat getStatus() const { return status; } @@ -289,6 +291,14 @@ class MainSolver { inline bool trackPartitions() const; + virtual PTRef preprocessFormulasDefault(vec const & frameFormulas, PreprocessingContext const &); + virtual vec preprocessFormulasPerPartition(vec const & frameFormulas, PreprocessingContext const &); + + virtual PTRef preprocessFormula(PTRef, PreprocessingContext const &); + virtual PTRef preprocessFormulaBeforeFinalTheoryPreprocessing(PTRef, PreprocessingContext const &); + virtual void preprocessFormulaDoFinalTheoryPreprocessing(PreprocessingContext const &); + virtual PTRef preprocessFormulaAfterFinalTheoryPreprocessing(PTRef, PreprocessingContext const &); + PTRef rewriteMaxArity(PTRef root); virtual sstat solve_(vec const & enabledFrames); From 118750e4b49e5e8e37cb16417ee49c0a3efe9f1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Tue, 18 Nov 2025 17:28:02 +0100 Subject: [PATCH 2/3] Renamed internal MainSolver::firstNotSimplifiedFrame and insertedFormulasCount --- src/api/MainSolver.cc | 16 ++++++++-------- src/api/MainSolver.h | 6 +++--- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 56aa3bf7e..a7d8526c1 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -93,7 +93,7 @@ bool MainSolver::pop() { frames.pop(); preprocessor.pop(); termNames.popScope(); - firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount()); + firstNotPreprocessedFrame = std::min(firstNotPreprocessedFrame, frames.frameCount()); if (not isLastFrameUnsat()) { getSMTSolver().restoreOK(); } return true; } @@ -115,15 +115,15 @@ void MainSolver::insertFormula(PTRef fla) { // formulas, // thus we need the old value of count. TODO: Find a good interface for this so it cannot be broken this // easily - unsigned int partition_index = insertedFormulasCount++; + unsigned int partition_index = insertedAssertionsCount++; pmanager.assignTopLevelPartitionIndex(partition_index, fla); assert(pmanager.getPartitionIndex(fla) != -1); } else { - ++insertedFormulasCount; + ++insertedAssertionsCount; } frames.add(fla); - firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount() - 1); + firstNotPreprocessedFrame = std::min(firstNotPreprocessedFrame, frames.frameCount() - 1); } bool MainSolver::tryAddNamedAssertion(PTRef fla, std::string const & name) { @@ -140,12 +140,12 @@ bool MainSolver::tryAddTermNameFor(PTRef fla, std::string const & name) { sstat MainSolver::simplifyFormulas() { status = s_Undef; - for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount(); ++i) { + for (std::size_t i = firstNotPreprocessedFrame; i < frames.frameCount(); ++i) { auto & frame = frames[i]; FrameId const frameId = frame.getId(); PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()}; preprocessor.prepareForProcessingFrame(i); - firstNotSimplifiedFrame = i + 1; + firstNotPreprocessedFrame = i + 1; if (not context.perPartition) { PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context); @@ -161,8 +161,8 @@ sstat MainSolver::simplifyFormulas() { } if (status == s_False) { - assert(firstNotSimplifiedFrame > 0); - rememberUnsatFrame(firstNotSimplifiedFrame - 1); + assert(firstNotPreprocessedFrame > 0); + rememberUnsatFrame(firstNotPreprocessedFrame - 1); } return status; diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 996860ec6..d22b62c49 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -89,7 +89,7 @@ class MainSolver { void insertFormula(PTRef fla); // Alias for `insertFormula`, reserved for future use void addAssertion(PTRef fla) { return insertFormula(fla); } - std::size_t getInsertedFormulasCount() const { return insertedFormulasCount; } + std::size_t getInsertedFormulasCount() const { return insertedAssertionsCount; } // Alias for `getInsertedFormulasCount`, reserved for future use std::size_t getAssertionsCount() const { return getInsertedFormulasCount(); } @@ -332,8 +332,8 @@ class MainSolver { int check_called = 0; // A counter on how many times check was called. vec frameTerms; - std::size_t firstNotSimplifiedFrame = 0; - unsigned int insertedFormulasCount = 0; + std::size_t firstNotPreprocessedFrame = 0; + std::size_t insertedAssertionsCount = 0; }; bool MainSolver::trackPartitions() const { From fcbdc29f5dc6121246aa98ad9d2c616f8035167a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Sat, 6 Dec 2025 14:17:38 +0100 Subject: [PATCH 3/3] Placed the loop body of simplifyFormulas into another separate function --- src/api/MainSolver.cc | 46 +++++++++++++++++++++++++++---------------- src/api/MainSolver.h | 2 ++ 2 files changed, 31 insertions(+), 17 deletions(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index a7d8526c1..09c67268d 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -141,23 +141,10 @@ bool MainSolver::tryAddTermNameFor(PTRef fla, std::string const & name) { sstat MainSolver::simplifyFormulas() { status = s_Undef; for (std::size_t i = firstNotPreprocessedFrame; i < frames.frameCount(); ++i) { - auto & frame = frames[i]; - FrameId const frameId = frame.getId(); - PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()}; - preprocessor.prepareForProcessingFrame(i); - firstNotPreprocessedFrame = i + 1; - - if (not context.perPartition) { - PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context); - status = giveToSolver(frameFormula, frameId); - } else { - vec processedFormulas = preprocessFormulasPerPartition(frame.formulas, context); - for (PTRef fla : processedFormulas) { - status = giveToSolver(fla, frameId); - if (status == s_False) { break; } - } - } - if (status == s_False) { break; } + assert(status != s_False); + if (tryPreprocessFormulasOfFrame(i)) { continue; } + assert(status == s_False); + break; } if (status == s_False) { @@ -168,6 +155,31 @@ sstat MainSolver::simplifyFormulas() { return status; } +bool MainSolver::tryPreprocessFormulasOfFrame(std::size_t i) { + auto & frame = frames[i]; + FrameId const frameId = frame.getId(); + PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()}; + preprocessor.prepareForProcessingFrame(i); + firstNotPreprocessedFrame = i + 1; + + assert(status != s_False); + + if (not context.perPartition) { + PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context); + status = giveToSolver(frameFormula, frameId); + return status != s_False; + } + + vec processedFormulas = preprocessFormulasPerPartition(frame.formulas, context); + for (PTRef fla : processedFormulas) { + status = giveToSolver(fla, frameId); + if (status == s_False) { return false; } + } + + assert(status != s_False); + return true; +} + PTRef MainSolver::preprocessFormulasDefault(vec const & frameFormulas, PreprocessingContext const & context) { assert(not context.perPartition); diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index d22b62c49..20f9c9f84 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -291,6 +291,8 @@ class MainSolver { inline bool trackPartitions() const; + virtual bool tryPreprocessFormulasOfFrame(std::size_t); + virtual PTRef preprocessFormulasDefault(vec const & frameFormulas, PreprocessingContext const &); virtual vec preprocessFormulasPerPartition(vec const & frameFormulas, PreprocessingContext const &);