From 97fff65ef6a37396d82e155c768d7578f5ac1905 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 20 Jan 2025 21:31:29 +0100 Subject: [PATCH] Fixing FRAT at least --- scripts/build_scripts | 2 +- src/cryptominisat.cpp | 5 +---- src/frat.h | 2 -- src/idrup.h | 18 ++++++------------ src/intree.cpp | 10 +++------- src/main.cpp | 12 ++---------- src/main_common.cpp | 25 ++++++++++--------------- src/occsimplifier.cpp | 4 ++-- src/searcher.cpp | 2 +- src/solver.cpp | 13 ++++++++++--- src/solver.h | 6 ------ src/solverconf.cpp | 1 - src/solverconf.h | 3 +-- utils/OutputCheck | 2 +- utils/gtest | 2 +- utils/sha1-sat | 2 +- 16 files changed, 40 insertions(+), 69 deletions(-) diff --git a/scripts/build_scripts b/scripts/build_scripts index 6143e19e0..e7abb4976 160000 --- a/scripts/build_scripts +++ b/scripts/build_scripts @@ -1 +1 @@ -Subproject commit 6143e19e02fcf69b1c50927a29e9c6347fb351cc +Subproject commit e7abb49769d0c8be288cf32102983d3fa3b7f734 diff --git a/src/cryptominisat.cpp b/src/cryptominisat.cpp index 4cf362f3d..e8a629404 100644 --- a/src/cryptominisat.cpp +++ b/src/cryptominisat.cpp @@ -400,9 +400,7 @@ DLL_PUBLIC void SATSolver::set_num_threads(unsigned num) throw std::runtime_error(err); } - if (data->solvers[0]->frat->enabled() || - data->solvers[0]->conf.simulate_frat - ) { + if (data->solvers[0]->frat->enabled()) { const char err[] = "ERROR: FRAT cannot be used in multi-threaded mode"; std::cerr << err << endl; throw std::runtime_error(err); @@ -938,7 +936,6 @@ lbool calc( } data->okay = data->solvers[0]->okay(); data->cpu_times[0] = cpuTime(); - data->solvers[0]->conclude_idrup(ret); return ret; } diff --git a/src/frat.h b/src/frat.h index ba5fc1542..9235ef659 100644 --- a/src/frat.h +++ b/src/frat.h @@ -26,7 +26,6 @@ THE SOFTWARE. #include #include -#include "constants.h" #include "clause.h" #include "sqlstats.h" #include "xor.h" @@ -45,7 +44,6 @@ using std::vector; #define FRAT_PRINT(...) do {} while (0) #endif - namespace CMSat { enum FratFlag{fin, deldelay, deldelayx, del, delx, findelay, add, addx, origcl, origclx, fratchain, finalcl, finalx, reloc, implyclfromx, implyxfromcls, weakencl, restorecl, assump, unsatcore, modelF}; diff --git a/src/idrup.h b/src/idrup.h index aad967619..370b861ce 100644 --- a/src/idrup.h +++ b/src/idrup.h @@ -20,17 +20,14 @@ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ***********************************************/ -#ifndef __IDRUP_H__ -#define __IDRUP_H__ +#pragma once -#include "constants.h" #include "clause.h" #include "frat.h" #include "sqlstats.h" #include -#include -#include +#include using std::vector; #define DEBUG_IDRUP @@ -67,24 +64,23 @@ class IdrupFile: public Frat del_len = 0; } - virtual ~IdrupFile() - { + ~IdrupFile() override { flush(); delete[] drup_buf; delete[] del_buf; } - virtual void set_sumconflicts_ptr(uint64_t* _sumConflicts) override + void set_sumconflicts_ptr(uint64_t* _sumConflicts) override { sumConflicts = _sumConflicts; } - virtual void set_sqlstats_ptr(SQLStats* _sqlStats) override + void set_sqlstats_ptr(SQLStats* _sqlStats) override { sqlStats = _sqlStats; } - virtual FILE* getFile() override + FILE* getFile() override { return drup_file; } @@ -510,5 +506,3 @@ class IdrupFile: public Frat }; } - -#endif //__IDRUP_H__ diff --git a/src/intree.cpp b/src/intree.cpp index ecf8216aa..ec47d0437 100644 --- a/src/intree.cpp +++ b/src/intree.cpp @@ -90,11 +90,9 @@ bool InTree::watches_only_contains_nonbin(const Lit lit) const bool InTree::check_timeout_due_to_hyperbin() { assert(!(solver->timedOutPropagateFull && solver->frat->enabled())); - assert(!(solver->timedOutPropagateFull && solver->conf.simulate_frat)); + assert(!(solver->timedOutPropagateFull)); - if (solver->timedOutPropagateFull - && !(solver->frat->enabled() || solver->conf.simulate_frat) - ) { + if (solver->timedOutPropagateFull && !solver->frat->enabled()) { verb_print(1, "[intree] intra-propagation timeout, turning off OTF hyper-bin&trans-red"); solver->conf.do_hyperbin_and_transred = false; return true; @@ -307,9 +305,7 @@ bool InTree::handle_lit_popped_from_queue( bool ok; if (solver->conf.do_hyperbin_and_transred) { uint64_t max_hyper_time = numeric_limits::max(); - if (!solver->frat->enabled() && - !solver->conf.simulate_frat - ) { + if (!solver->frat->enabled()) { max_hyper_time = solver->propStats.otfHyperTime + solver->propStats.bogoProps diff --git a/src/main.cpp b/src/main.cpp index 8c20fc8a4..2ea22ac90 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -936,10 +936,6 @@ void Main::add_supported_options() { .action([&](const auto& a) {conf.max_scc_depth = std::atoi(a.c_str());}) .default_value(conf.max_scc_depth) .help("The maximum for scc search depth"); - program.add_argument("--simfrat") - .action([&](const auto& a) {conf.simulate_frat = std::atoi(a.c_str());}) - .default_value(conf.simulate_frat) - .help("Simulate FRAT"); program.add_argument("--idrup") .action([&](const auto& a) {conf.idrup = std::atoi(a.c_str());}) .default_value(conf.idrup) @@ -1172,11 +1168,8 @@ void Main::manually_parse_some_options() fileNamePresent = true; } else assert(false && "The try() should not have succeeded"); - if ((files.size() > 1 || conf.simulate_frat) && !conf.idrup) { - if (files.size() > 1) { - assert(!conf.simulate_frat && "You can't have both simulation of FRAT and frat"); - frat_fname = files[1]; - } + if ((files.size() > 1) && !conf.idrup) { + if (files.size() > 1) frat_fname = files[1]; handle_frat_option(); } else if (files.size() > 1 && conf.idrup) { idrup_fname = files[1]; @@ -1320,7 +1313,6 @@ lbool Main::multi_solutions() { if (max_nr_of_solutions == 1 && fratf == nullptr - && !conf.simulate_frat && debugLib.empty() ) { solver->set_single_run(); diff --git a/src/main_common.cpp b/src/main_common.cpp index b1157d846..b8991e065 100644 --- a/src/main_common.cpp +++ b/src/main_common.cpp @@ -30,10 +30,7 @@ using std::endl; using namespace CMSat; -void MainCommon::handle_frat_option() -{ - if (conf.simulate_frat) return; - +void MainCommon::handle_frat_option() { FILE* fratfTmp = fopen(frat_fname.c_str(), "wb"); if (fratfTmp == nullptr) { std::cerr @@ -45,19 +42,17 @@ void MainCommon::handle_frat_option() fratf = fratfTmp; } -void MainCommon::handle_idrup_option() -{ - if (conf.idrup) { - FILE* idrupfTmp = fopen(idrup_fname.c_str(), "w"); - if (idrupfTmp == NULL) { - std::cerr - << "ERROR: Could not open IDRUP file '" << idrup_fname << "' for writing" - << endl; +void MainCommon::handle_idrup_option() { + assert(conf.idrup); + FILE* idrupfTmp = fopen(idrup_fname.c_str(), "w"); + if (idrupfTmp == NULL) { + std::cerr + << "ERROR: Could not open IDRUP file '" << idrup_fname << "' for writing" + << endl; - std::exit(-1); - } - idrupf = idrupfTmp; + std::exit(-1); } + idrupf = idrupfTmp; } uint32_t MainCommon::print_model(CMSat::SATSolver* solver, std::ostream* os, const std::vector* only) diff --git a/src/occsimplifier.cpp b/src/occsimplifier.cpp index de4c030cc..2668d94cf 100644 --- a/src/occsimplifier.cpp +++ b/src/occsimplifier.cpp @@ -284,7 +284,7 @@ void OccSimplifier::unlink_clause( , bool only_set_is_removed ) { Clause& cl = *solver->cl_alloc.ptr(offset); - if (do_frat && (solver->frat->enabled() || solver->conf.simulate_frat)) { + if (do_frat && (solver->frat->enabled())) { (*solver->frat) << del << cl << fin; } @@ -3013,7 +3013,7 @@ bool OccSimplifier::uneliminate(uint32_t var) void OccSimplifier::remove_by_frat_recently_elimed_clauses(size_t origElimedSize) { - if (! (solver->frat->enabled() || solver->conf.simulate_frat) ) { + if (!solver->frat->enabled()) { newly_elimed_cls_IDs.clear(); return; } diff --git a/src/searcher.cpp b/src/searcher.cpp index 5fda1a39a..bd04730b4 100644 --- a/src/searcher.cpp +++ b/src/searcher.cpp @@ -3007,7 +3007,7 @@ PropBy Searcher::propagate() { PropBy ret = propagate_any_order(); //Drat -- If declevel 0 propagation, we have to add the unitaries - if (decisionLevel() == 0 && (frat->enabled() || conf.simulate_frat)) { + if (decisionLevel() == 0 && (frat->enabled())) { if (!ret.isnullptr()) { int32_t ID; for(size_t i = last_trail; i < trail.size(); i++) { diff --git a/src/solver.cpp b/src/solver.cpp index baab4590b..b5f068cec 100644 --- a/src/solver.cpp +++ b/src/solver.cpp @@ -1255,7 +1255,7 @@ void Solver::check_and_upd_config_parameters() exit(-1); } - if ((frat->enabled() || conf.simulate_frat)) { + if ((frat->enabled())) { if (!conf.do_hyperbin_and_transred) { if (conf.verbosity) { cout @@ -1438,7 +1438,7 @@ lbool Solver::solve_with_assumptions( } write_final_frat_clauses(); - + conclude_idrup(status); return status; } @@ -1883,7 +1883,6 @@ lbool Solver::execute_inprocess_strategy( } else if (token == "breakid") { if (conf.doBreakid && frat->enabled() - && !conf.simulate_frat && (solveStats.num_simplify == 0 || (solveStats.num_simplify % conf.breakid_every_n == (conf.breakid_every_n-1))) ) { @@ -3699,8 +3698,16 @@ void Solver::detach_clauses_in_xors() { << conf.print_times(cpuTime() - my_time)); } +bool Solver::removed_var_ext(uint32_t var) const { + var = map_outer_to_inter(var); + if (value(var) != l_Undef) return true; + if (varData[var].removed != Removed::none) return true; + return false; +} + void Solver::conclude_idrup (lbool result) { + if (!conf.idrup) return; if (result == l_True) { *frat << satisfiable; *frat << modelF; diff --git a/src/solver.h b/src/solver.h index 428cc8255..924a57b32 100644 --- a/src/solver.h +++ b/src/solver.h @@ -615,10 +615,4 @@ inline void Solver::free_cl( cl_alloc.clauseFree(offs); } -inline bool Solver::removed_var_ext(uint32_t var) const -{ - var = map_outer_to_inter(var); - return value(var) != l_Undef || varData[var].removed != Removed::none; -} - } //end namespace diff --git a/src/solverconf.cpp b/src/solverconf.cpp index c471d6682..6f82c120a 100644 --- a/src/solverconf.cpp +++ b/src/solverconf.cpp @@ -372,7 +372,6 @@ DLL_PUBLIC SolverConf::SolverConf() : //misc , origSeed(0) - , simulate_frat(false) { ratio_keep_clauses[clean_to_int(ClauseClean::glue)] = 0; ratio_keep_clauses[clean_to_int(ClauseClean::activity)] = 0.44; diff --git a/src/solverconf.h b/src/solverconf.h index 1203f2f6d..609ac4c03 100644 --- a/src/solverconf.h +++ b/src/solverconf.h @@ -518,8 +518,7 @@ class DLL_PUBLIC SolverConf //Misc unsigned origSeed; - int simulate_frat; - int idrup; + int idrup = 0; int conf_needed = true; }; diff --git a/utils/OutputCheck b/utils/OutputCheck index 80d077dd6..3232d0937 160000 --- a/utils/OutputCheck +++ b/utils/OutputCheck @@ -1 +1 @@ -Subproject commit 80d077dd600c98245c49d92049b02999fd7e703d +Subproject commit 3232d0937dcabf59df7ceb776f27b4d5cff6194d diff --git a/utils/gtest b/utils/gtest index 456574145..1d17ea141 160000 --- a/utils/gtest +++ b/utils/gtest @@ -1 +1 @@ -Subproject commit 456574145cf71a5375777cab58453acfd92a920b +Subproject commit 1d17ea141d2c11b8917d2c7d029f1c4e2b9769b2 diff --git a/utils/sha1-sat b/utils/sha1-sat index 96bfd7862..56faee993 160000 --- a/utils/sha1-sat +++ b/utils/sha1-sat @@ -1 +1 @@ -Subproject commit 96bfd7862963da289126927d452ef1368914faf3 +Subproject commit 56faee9939c9315206d455435029e6493aec0b54