Skip to content

Split simplifyFormulas to sub-functions #888

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Tomaqa wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Split simplifyFormulas to sub-functions #888

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e575257
Split simplifyFormulas to sub-functions
Tomaqa Nov 6, 2025
118750e
Renamed internal MainSolver::firstNotSimplifiedFrame and insertedForm…
Tomaqa Nov 18, 2025
fcbdc29
Placed the loop body of simplifyFormulas into another separate function
Tomaqa Dec 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
191 changes: 135 additions & 56 deletions src/api/MainSolver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand All @@ -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) {
Expand All @@ -140,63 +140,138 @@ 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++) {
PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()};
preprocessor.prepareForProcessingFrame(i);
firstNotSimplifiedFrame = i + 1;
if (context.perPartition) {
vec<PTRef> 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; }
}
} 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;
}
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());
}
for (std::size_t i = firstNotPreprocessedFrame; i < frames.frameCount(); ++i) {
assert(status != s_False);
if (tryPreprocessFormulasOfFrame(i)) { continue; }
assert(status == s_False);
break;
}

if (status == s_False) {
assert(firstNotSimplifiedFrame > 0);
rememberUnsatFrame(firstNotSimplifiedFrame - 1);
assert(firstNotPreprocessedFrame > 0);
rememberUnsatFrame(firstNotPreprocessedFrame - 1);
}

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<PTRef> 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<PTRef> 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<PTRef> MainSolver::preprocessFormulasPerPartition(vec<PTRef> const & frameFormulas,
PreprocessingContext const & context) {
assert(context.perPartition);

if (frameFormulas.size() == 0) { return {}; }

vec<PTRef> 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) {
Copy link
Member

@BritikovKI BritikovKI Dec 9, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's too big of a name... I see that there is a naming convention, but that can be a pain to use inside the code...
Functionality can be described with a comment or documentation, but using this long func names feels a bit too much 🤔

Why not
initialPreprocessing
corePreprocessing
finalPreprocessing
or smth shorter...

Copy link
Member Author

@Tomaqa Tomaqa Dec 12, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wanted to use sth. like that, but I do not like that corePreprocessing (or body or whatever) would be just that one call, which is actually just a minor step within the whole process. The whole reason why it is separated is that in preprocessFormulasPerPartition, both preprocessFormulaBeforeFinalTheoryPreprocessing and preprocessFormulaAfterFinalTheoryPreprocessing are called on each particular frame formula, while preprocessFormulaDoFinalTheoryPreprocessing is called just once. In preprocessFormulasDefault, i.e., in preprocessFormula, all is called just once (because we mix all formulas into one conjunction).

What could potentially work is preprocessFormulaBegin, preprocessFormulaMiddle, preprocessFormulaEnd. This way, middle does not make the impression that it is the main part.
What do you think?

Copy link
Member

@BritikovKI BritikovKI Dec 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like your idea here!
Middle looks a little bit off, but I don't have a better idea for the name
There is also an option to ask LLM for the recommendation))

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 &) {
Copy link
Member

@BritikovKI BritikovKI Dec 9, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is a function which calls one function, why not use original function call?
(Also imho name's a bit too long)

Copy link
Member Author

@Tomaqa Tomaqa Dec 12, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This way, it is clearer that this part must not be omitted. Without the auxiliary function, it could be missed. Besides, connecting the theory and preprocessor is not completely useless, prevents code duplication.

Copy link
Member

@BritikovKI BritikovKI Dec 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I understand 🤔 Why would one assume this part can be ommited? It can also be highlighted by the comment in the code, what theory->afterPreprocessing does...

Can you elaborate on code duplication point? Because as I understand a single function function call is being replaced by a different function call + additional lines of code in MainSolver.cc and MainSolver.h

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<PTRef> MainSolver::getCurrentAssertions() const {
vec<PTRef> assertions;
size_t const cnt = frames.frameCount();
Expand Down Expand Up @@ -316,11 +391,15 @@ sstat MainSolver::giveToSolver(PTRef root, FrameId push_id) {
std::vector<vec<Lit>> clauses;
void operator()(vec<Lit> && 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]);
Copy link
Member

@BritikovKI BritikovKI Dec 9, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not lambda?
(Not important, but tbh I just like lambdas 😊)

Copy link
Member Author

@Tomaqa Tomaqa Dec 12, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To not use the variable at all if push_id == 0 (i.e., do not even initialize it on the stack). Maybe it would be worth to also add the [[maybe_unused]] attribute to the variable, to make it more explicit.

Copy link
Member

@BritikovKI BritikovKI Dec 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, wouldn't it get optimized by compiler?
Main reason I like lambda is because it looks a little bit more compact here, it is not a major point of contention though...

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); }
Expand Down
18 changes: 15 additions & 3 deletions src/api/MainSolver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(); }

Expand All @@ -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; }

Expand Down Expand Up @@ -289,6 +291,16 @@ class MainSolver {

inline bool trackPartitions() const;

virtual bool tryPreprocessFormulasOfFrame(std::size_t);

virtual PTRef preprocessFormulasDefault(vec<PTRef> const & frameFormulas, PreprocessingContext const &);
virtual vec<PTRef> preprocessFormulasPerPartition(vec<PTRef> 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<FrameId> const & enabledFrames);
Expand Down Expand Up @@ -322,8 +334,8 @@ class MainSolver {
int check_called = 0; // A counter on how many times check was called.

vec<PTRef> frameTerms;
std::size_t firstNotSimplifiedFrame = 0;
unsigned int insertedFormulasCount = 0;
std::size_t firstNotPreprocessedFrame = 0;
std::size_t insertedAssertionsCount = 0;
};

bool MainSolver::trackPartitions() const {
Expand Down