Fixing FRAT at least

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;
     }
 

src/frat.h

@@ -26,7 +26,6 @@ THE SOFTWARE.
 #include <iostream>
 #include <stdio.h>
 
-#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};

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 <vector>
-#include <iostream>
-#include <stdio.h>
+#include <cstdio>
 
 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__

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<uint64_t>::max();
-            if (!solver->frat->enabled() &&
-                !solver->conf.simulate_frat
-            ) {
+            if (!solver->frat->enabled()) {
                 max_hyper_time =
                 solver->propStats.otfHyperTime
                 + solver->propStats.bogoProps

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();

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<uint32_t>* only)

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;
     }

src/searcher.cpp

@@ -3007,7 +3007,7 @@ PropBy Searcher::propagate() {
     PropBy ret = propagate_any_order<inprocess, red_also, distill_use>();
 
     //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++) {

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;

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

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;

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;
 };