Skip to content

Commit

Permalink
remove extra line cause checks to crash
Browse files Browse the repository at this point in the history
  • Loading branch information
Robin Coutelier committed Apr 22, 2024
1 parent fd6fa06 commit e732f12
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 3 deletions.
2 changes: 1 addition & 1 deletion SATSubsumption/SATSubsumptionAndResolution.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
* - 2024: "SAT Solving for Variants of First-Order Subsumption" by Robin Coutelier, Jakob Rath,
* Michael Rawson, Armin Biere and Laura Kovács
*
* Note that in this implementation, we removed the indirect encoding for subumption resolution
* Note that in this implementation, we removed the indirect encoding for subsumption resolution
* because it does not bring a significant improvement.
* The indirect encoding described in "SAT Solving for Variants of First-Order Subsumption" was
* improved by ignoring the cⱼ variables for which there exists only b⁻ᵢⱼ variables. This reduces
Expand Down
2 changes: 0 additions & 2 deletions Saturation/SaturationAlgorithm.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1644,12 +1644,10 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
if (opt.forwardSubsumptionResolution()) {
ForwardSubsumptionAndResolution* fwd = new ForwardSubsumptionAndResolution(true);
res->addForwardSimplifierToFront(fwd);
cout << endl;
}
else {
ForwardSubsumptionAndResolution* fwd = new ForwardSubsumptionAndResolution(false);
res->addForwardSimplifierToFront(fwd);
cout << endl;
}
}
else if (opt.forwardSubsumptionResolution()) {
Expand Down

0 comments on commit e732f12

Please sign in to comment.