diff --git a/setup.py b/setup.py index 629aa3edf..d6859b6c5 100644 --- a/setup.py +++ b/setup.py @@ -81,6 +81,7 @@ def gen_modules(version): "src/gaussian.cpp", "src/get_clause_query.cpp", "src/hyperengine.cpp", + "src/idrup.cpp", "src/intree.cpp", "src/lucky.cpp", "src/matrixfinder.cpp", diff --git a/src/cnf.cpp b/src/cnf.cpp index c48a07aa0..e3d3f76ef 100644 --- a/src/cnf.cpp +++ b/src/cnf.cpp @@ -675,6 +675,14 @@ void CNF::add_frat(FILE* os) { frat->set_sqlstats_ptr(sqlStats); } +void CNF::add_idrup(FILE* os) { + if (frat) delete frat; + frat = new IdrupFile(inter_to_outerMain); + frat->setFile(os); + frat->set_sumconflicts_ptr(&sumConflicts); + frat->set_sqlstats_ptr(sqlStats); +} + vector CNF::get_outside_lit_incidence() { vector inc; diff --git a/src/cnf.h b/src/cnf.h index ff536a8ff..565415555 100644 --- a/src/cnf.h +++ b/src/cnf.h @@ -34,6 +34,7 @@ THE SOFTWARE. #include "solvertypes.h" #include "watcharray.h" #include "frat.h" +#include "idrup.h" #include "clauseallocator.h" #include "varupdatehelper.h" #include "gausswatched.h" @@ -135,6 +136,7 @@ class CNF //frat Frat* frat; void add_frat(FILE* os); + void add_idrup(FILE* os); //Clauses vector longIrredCls; diff --git a/src/cryptominisat.cpp b/src/cryptominisat.cpp index 25ef1b993..4cf362f3d 100644 --- a/src/cryptominisat.cpp +++ b/src/cryptominisat.cpp @@ -938,6 +938,7 @@ lbool calc( } data->okay = data->solvers[0]->okay(); data->cpu_times[0] = cpuTime(); + data->solvers[0]->conclude_idrup(ret); return ret; } @@ -1141,6 +1142,24 @@ DLL_PUBLIC void SATSolver::set_frat(FILE* os) data->solvers[0]->conf.do_hyperbin_and_transred = true; } +DLL_PUBLIC void SATSolver::set_idrup(FILE* os) +{ + if (data->solvers.size() > 1) { + std::cerr << "ERROR: IDRUP cannot be used in multi-threaded mode" << endl; + exit(-1); + } + if (nVars() > 0) { + std::cerr << "ERROR: IDRUP cannot be set after variables have been added" << endl; + exit(-1); + } + data->solvers[0]->conf.doBreakid = false; + data->solvers[0]->conf.doFindXors = false; + data->solvers[0]->add_idrup(os); + data->solvers[0]->conf.gaussconf.max_matrix_rows = 0; + data->solvers[0]->conf.gaussconf.max_matrix_columns = 0; + data->solvers[0]->conf.do_hyperbin_and_transred = true; +} + DLL_PUBLIC void SATSolver::interrupt_asap() { data->must_interrupt->store(true, std::memory_order_relaxed); diff --git a/src/cryptominisat.h b/src/cryptominisat.h index ee8d804ec..806e6bc77 100644 --- a/src/cryptominisat.h +++ b/src/cryptominisat.h @@ -205,6 +205,8 @@ namespace CMSat { void print_stats(double wallclock_time_started = 0) const; //print solving stats. Call after solve()/simplify() void set_frat(FILE* os); //set frat to ostream, e.g. stdout or a file + void set_idrup(FILE* os); //set idrup to ostream, e.g. stdout or a file + void add_empty_cl_to_frat(); // allows to treat SAT as UNSAT and perform learning void interrupt_asap(); //call this asynchronously, and the solver will try to cleanly abort asap void add_in_partial_solving_stats(); //used only by Ctrl+C handler. Ignore. diff --git a/src/frat.h b/src/frat.h index 8b2ec71c0..ba5fc1542 100644 --- a/src/frat.h +++ b/src/frat.h @@ -48,7 +48,8 @@ using std::vector; namespace CMSat { -enum FratFlag{fin, deldelay, deldelayx, del, delx, findelay, add, addx, origcl, origclx, fratchain, finalcl, finalx, reloc, implyclfromx, implyxfromcls}; + enum FratFlag{fin, deldelay, deldelayx, del, delx, findelay, add, addx, origcl, origclx, fratchain, finalcl, finalx, reloc, implyclfromx, implyxfromcls, weakencl, restorecl, assump, unsatcore, modelF}; + enum FratOutcome{satisfiable, unsatisfiable, unknown}; class Frat { @@ -67,10 +68,12 @@ class Frat virtual Frat& operator<<(const Xor&) { return *this; } virtual Frat& operator<<(const vector&) { return *this; } virtual Frat& operator<<(const char*) { return *this; } + virtual Frat& operator<<(const FratOutcome) { return *this; } virtual Frat& operator<<(const FratFlag) { return *this; } virtual void setFile(FILE*) { } virtual FILE* getFile() { return nullptr; } virtual void flush(); + virtual bool incremental() {return false;} int buf_len; unsigned char* drup_buf = nullptr; @@ -275,6 +278,7 @@ class FratFile: public Frat } break; + case FratFlag::weakencl: case FratFlag::del: adding = false; buf_add('d'); @@ -327,6 +331,10 @@ class FratFile: public Frat buf_add('x'); buf_nonbin_move(); break; + + default: + __builtin_unreachable(); + break; } return *this; diff --git a/src/idrup.cc b/src/idrup.cc new file mode 100644 index 000000000..aef7ddce1 --- /dev/null +++ b/src/idrup.cc @@ -0,0 +1,25 @@ +/****************************************** +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. +***********************************************/ + +#include "idrup.h" + +namespace CMSat { + void Drat::flush() {} +} diff --git a/src/idrup.h b/src/idrup.h new file mode 100644 index 000000000..aad967619 --- /dev/null +++ b/src/idrup.h @@ -0,0 +1,514 @@ +/****************************************** +Copyright (C) 2009-2024 Authors of CryptoMiniSat, see AUTHORS file + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. +***********************************************/ + +#ifndef __IDRUP_H__ +#define __IDRUP_H__ + +#include "constants.h" +#include "clause.h" +#include "frat.h" +#include "sqlstats.h" + +#include +#include +#include + +using std::vector; +#define DEBUG_IDRUP + +#if 0 +#define IDRUP_PRINT((...) \ + do { \ + const uint32_t tmp_num = sprintf((char*)buf_ptr, __VA_ARGS__); \ + buf_ptr+=tmp_num; \ + buf_len+=tmp_num; \ + } while (0) +#else +#define IDRUP_PRINT(...) do {} while (0) +#endif + + +namespace CMSat { + +template +class IdrupFile: public Frat +{ + const int flush_bound = 32768; // original value: 1048576; +public: + IdrupFile(vector& _interToOuterMain) : + interToOuterMain(_interToOuterMain) + { + drup_buf = new unsigned char[2 * 1024 * 1024]; + buf_ptr = drup_buf; + buf_len = 0; + memset(drup_buf, 0, 2 * 1024 * 1024); + + del_buf = new unsigned char[2 * 1024 * 1024]; + del_ptr = del_buf; + del_len = 0; + } + + virtual ~IdrupFile() + { + flush(); + delete[] drup_buf; + delete[] del_buf; + } + + virtual void set_sumconflicts_ptr(uint64_t* _sumConflicts) override + { + sumConflicts = _sumConflicts; + } + + virtual void set_sqlstats_ptr(SQLStats* _sqlStats) override + { + sqlStats = _sqlStats; + } + + virtual FILE* getFile() override + { + return drup_file; + } + + void flush() override + { + binDRUP_flush(); + } + + void binDRUP_flush() { + fwrite(drup_buf, sizeof(unsigned char), buf_len, drup_file); + fflush (drup_file); + buf_ptr = drup_buf; + buf_len = 0; + } + + void setFile(FILE* _file) override + { + drup_file = _file; + } + + bool something_delayed() override + { + return delete_filled; + } + + void forget_delay() override + { + del_ptr = del_buf; + del_len = 0; + must_delete_next = false; + delete_filled = false; + } + + bool enabled() override + { + return true; + } + + bool incremental() override + { + return true; + } + int del_len = 0; + unsigned char* del_buf; + unsigned char* del_ptr; + + bool delete_filled = false; + bool must_delete_next = false; + + virtual Frat& operator<<(const int32_t) override + { +#if 0 // clauseID + if (must_delete_next) { + byteDRUPdID(clauseID); + } else { + byteDRUPaID(clauseID); + } +#endif + return *this; + } + + Frat& operator<<(const Clause& cl) override + { + if (skipnextclause) return *this; + if (must_delete_next) { + byteDRUPdID(cl.stats.ID); + for(const Lit l: cl) byteDRUPd(l); + } else { + byteDRUPaID(cl.stats.ID); + for(const Lit l: cl) byteDRUPa(l); + } + + return *this; + } + + Frat& operator<<(const vector& cl) override { + if (skipnextclause) return *this; + if (must_delete_next) { + for(const Lit l: cl) { + byteDRUPd(l); + } + } else { + for(const Lit l: cl) { + byteDRUPa(l); + } + } + + return *this; + } + + Frat& operator<<(const FratOutcome o) override + { + uint32_t num; + switch(o) { + case unsatisfiable: + this->flush(); + num = sprintf((char*)buf_ptr, "s UNSATISFIABLE\n"); + buf_ptr+=num; + buf_len+=num; + this->flush(); + break; + case satisfiable: + this->flush(); + num = sprintf((char*)buf_ptr, "s SATISFIABLE\n"); + buf_ptr+=num; + buf_len+=num; + this->flush(); + break; + case unknown: + this->flush(); + num = sprintf((char*)buf_ptr, "s UNKNOWN\n"); + buf_ptr+=num; + buf_len+=num; + this->flush(); + break; + } + return *this; + } + + Frat& operator<<(const FratFlag flag) override + { + const bool old = skipnextclause; + skipnextclause = false; + + switch (flag) + { + case FratFlag::fin: + if (old) break; + if (must_delete_next) { + if (binidrup) { + *del_ptr++ = 0; + del_len++; + } else { + *del_ptr++ = '0'; + *del_ptr++ = '\n'; + del_len+=2; + } + delete_filled = true; + } else { + if (binidrup) { + *buf_ptr++ = 0; + buf_len++; + } else { + *buf_ptr++ = '0'; + *buf_ptr++ = '\n'; + buf_len+=2; + } + if (buf_len > flush_bound) { + binDRUP_flush(); + } + if (adding && sqlStats) sqlStats->set_id_confl(cl_id, *sumConflicts); + IDRUP_PRINT("c set_id_confl (%d, %lld), adding: %d\n", cl_id, *sumConflicts, adding); + } + cl_id = 0; + must_delete_next = false; + if (flushing) + this->flush(), --flushing; + break; + + case FratFlag::deldelay: + adding = false; + assert(!delete_filled); + forget_delay(); + *del_ptr++ = 'd'; + del_len++; + if (!binidrup) { + *del_ptr++ = ' '; + del_len++; + } + delete_filled = false; + must_delete_next = true; + break; + + case FratFlag::findelay: + assert(delete_filled); + memcpy(buf_ptr, del_buf, del_len); + buf_len += del_len; + buf_ptr += del_len; + if (buf_len > flush_bound) { + binDRUP_flush(); + } + + forget_delay(); + break; + + case FratFlag::add: + adding = true; + cl_id = 0; + *buf_ptr++ = 'l'; + buf_len++; + if (!binidrup) { + *buf_ptr++ = ' '; + buf_len++; + } + break; + + case FratFlag::fratchain: + break; + + case FratFlag::del: + adding = false; + *buf_ptr++ = 'd'; + buf_len++; + if (!binidrup) { + *buf_ptr++ = ' '; + buf_len++; + } + break; + + case FratFlag::reloc: + skipnextclause = true; + // adding = false; + // forget_delay(); + // *buf_ptr++ = 'r'; + // buf_len++; + // if (!binidrup) { + // *buf_ptr++ = ' '; + // buf_len++; + // } + break; + + case FratFlag::finalcl: + assert (false); + break; + + case FratFlag::origcl: + adding = false; + forget_delay(); + *buf_ptr++ = 'i'; + buf_len++; + if (!binidrup) { + *buf_ptr++ = ' '; + buf_len++; + } + + break; + case FratFlag::weakencl: + adding = false; + forget_delay(); + *buf_ptr++ = 'w'; + buf_len++; + if (!binidrup) { + *buf_ptr++ = ' '; + buf_len++; + } + + break; + case FratFlag::restorecl: + adding = false; + forget_delay(); + *buf_ptr++ = 'r'; + buf_len++; + if (!binidrup) { + *buf_ptr++ = ' '; + buf_len++; + } + + break; + case FratFlag::assump: + this->flush(); + adding = false, flushing = 2; + forget_delay(); + *buf_ptr++ = 'q'; + buf_len++; + if (!binidrup) { + *buf_ptr++ = ' '; + buf_len++; + } + + break; + case FratFlag::modelF: + this->flush(); + adding = false, flushing = 2; + forget_delay(); + *buf_ptr++ = 'm'; + buf_len++; + if (!binidrup) { + *buf_ptr++ = ' '; + buf_len++; + } + break; + case FratFlag::unsatcore: + this->flush(); + adding = false, flushing = 2; + forget_delay(); + *buf_ptr++ = 'u'; + buf_len++; + if (!binidrup) { + *buf_ptr++ = ' '; + buf_len++; + } + + break; + case FratFlag::deldelayx: + case FratFlag::delx: + case FratFlag::finalx: + case FratFlag::implyclfromx: + case FratFlag::implyxfromcls: + case FratFlag::origclx: + skipnextclause = true; + break; + default: + __builtin_unreachable(); + break; + } + + return *this; + } + +private: + Frat& operator<<(const Lit lit) override + { + if (skipnextclause) return *this; + if (must_delete_next) { + byteDRUPd(lit); + } else { + byteDRUPa(lit); + } + + return *this; + } + + void byteDRUPa(const Lit l) + { + uint32_t v = l.var(); + v = interToOuterMain[v]; + if (binidrup) { + unsigned int u = 2 * (v + 1) + l.sign(); + do { + *buf_ptr++ = (u & 0x7f) | 0x80; + buf_len++; + u = u >> 7; + } while (u); + // End marker of this unsigned number + *(buf_ptr - 1) &= 0x7f; + } else { + uint32_t num = sprintf( + (char*)buf_ptr, "%s%d ", (l.sign() ? "-": ""), l.var()+1); + buf_ptr+=num; + buf_len+=num; + } + } + + virtual Frat& operator<<([[maybe_unused]] const char* str) override + { +#ifdef DEBUG_IDRUP + this->flush(); + uint32_t num = sprintf((char*)buf_ptr, "c %s", str); + buf_ptr+=num; + buf_len+=num; + this->flush(); +#endif + + return *this; + } + + + + void byteDRUPaID(const int32_t) + { +#if 0 + if (adding && cl_id == 0) cl_id = id; + if (binidrup) { + for(unsigned i = 0; i < 6; i++) { + *buf_ptr++ = (id>>(8*i))&0xff; + buf_len++; + } + } else { + uint32_t num = sprintf((char*)buf_ptr, "%d ", id); + buf_ptr+=num; + buf_len+=num; + } +#endif + } + + void byteDRUPdID(const int32_t) + { +#if 0 + if (binidrup) { + for(unsigned i = 0; i < 6; i++) { + *del_ptr++ = (id>>(8*i))&0xff; + del_len++; + } + } else { + uint32_t num = sprintf((char*)del_ptr, "%d ", id); + del_ptr+=num; + del_len+=num; + } +#endif + } + + void byteDRUPd(Lit l) + { + uint32_t v = l.var(); + v = interToOuterMain[v]; + if (binidrup) { + unsigned int u = 2 * (v + 1) + l.sign(); + do { + *del_ptr++ = (u & 0x7f) | 0x80; + del_len++; + u = u >> 7; + } while (u); + + // End marker of this unsigned number + *(del_ptr - 1) &= 0x7f; + } else { + uint32_t num = sprintf( + (char*)del_ptr, "%s%d ", (l.sign() ? "-": ""), l.var()+1); + del_ptr+=num; + del_len+=num; + } + } + + bool adding = false; + int flushing = 0; + int32_t cl_id = 0; + FILE* drup_file = nullptr; + vector& interToOuterMain; + uint64_t* sumConflicts = nullptr; + SQLStats* sqlStats = NULL; + bool skipnextclause = false; +}; + +} + +#endif //__IDRUP_H__ diff --git a/src/ipasir.cpp b/src/ipasir.cpp index 035819259..eac6b8b0f 100644 --- a/src/ipasir.cpp +++ b/src/ipasir.cpp @@ -55,6 +55,12 @@ struct MySolver { extern "C" { + DLL_PUBLIC void ipasir_trace_proof (void * solver, FILE *f) + { + + MySolver* s = (MySolver*)solver; + s->solver->set_idrup(f); + } DLL_PUBLIC const char * ipasir_signature () { static char tmp[200]; @@ -259,4 +265,36 @@ DLL_PUBLIC void ipasir_set_learn (void * /*solver*/, void * /*state*/, int /*max //this is complicated } +DLL_PUBLIC int ipasir_simplify (void * solver) +{ + MySolver* s = (MySolver*)solver; + + //Cleanup last_conflict + for(auto x: s->last_conflict) { + s->conflict_cl_map[x.toInt()] = 0; + } + s->last_conflict.clear(); + + //solve + lbool ret = s->solver->simplify(&(s->assumptions), nullptr); + s->assumptions.clear(); + + if (ret == l_True) { + return 10; + } + if (ret == l_False) { + s->conflict_cl_map.resize(s->solver->nVars()*2, 0); + s->last_conflict = s->solver->get_conflict(); + for(auto x: s->last_conflict) { + s->conflict_cl_map[x.toInt()] = 1; + } + return 20; + } + if (ret == l_Undef) { + return 0; + } + assert(false); + exit(-1); +} + } diff --git a/src/ipasir.h b/src/ipasir.h index 30cd490cb..f966e75fa 100644 --- a/src/ipasir.h +++ b/src/ipasir.h @@ -27,7 +27,7 @@ IN THE SOFTWARE. */ #ifndef ipasir_h_INCLUDED #define ipasir_h_INCLUDED - +#include /*------------------------------------------------------------------------*/ #ifdef __cplusplus extern "C" { @@ -155,6 +155,11 @@ void ipasir_set_terminate (void * solver, void * state, int (*terminate)(void * */ void ipasir_set_learn (void * solver, void * state, int max_length, void (*learn)(void * state, int * clause)); +int ipasir_simplify (void * solver); +/* + * Sets the proof file + */ +void ipasir_trace_proof(void *s, FILE *f); /*------------------------------------------------------------------------*/ #ifdef __cplusplus } diff --git a/src/main.cpp b/src/main.cpp index d8f78ab53..0abb55aa3 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -951,6 +951,10 @@ void Main::add_supported_options() { .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) + .help("idrup"); program.add_argument("--onlysampling") .flag() .action([&](const auto&) {only_sampl_solution = true;}) @@ -1177,12 +1181,17 @@ void Main::manually_parse_some_options() #endif fileNamePresent = true; } else assert(false && "The try() should not have succeeded"); - if (files.size() > 1 || conf.simulate_frat) { + 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]; } handle_frat_option(); + } else { + if (files.size() > 1 && conf.idrup) { + idrup_fname = files[1]; + } + handle_idrup_option(); } } catch (std::logic_error& e) { fileNamePresent = false; @@ -1239,6 +1248,7 @@ int Main::solve() solver = new SATSolver((void*)&conf); solverToInterrupt = solver; if (fratf) solver->set_frat(fratf); + if (idrupf) solver->set_idrup(idrupf); if (program.is_used("maxtime")) solver->set_max_time(program.get("maxtime")); if (program.is_used("maxconfl")) solver->set_max_confl(program.get("maxconfl")); diff --git a/src/main_common.cpp b/src/main_common.cpp index 493707102..a52890549 100644 --- a/src/main_common.cpp +++ b/src/main_common.cpp @@ -47,6 +47,23 @@ void MainCommon::handle_frat_option() } } +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; + + std::exit(-1); + } + idrupf = idrupfTmp; + } +} + uint32_t MainCommon::print_model(CMSat::SATSolver* solver, std::ostream* os, const std::vector* only) { *os << "v "; diff --git a/src/main_common.h b/src/main_common.h index 0676384b1..39a473fa4 100644 --- a/src/main_common.h +++ b/src/main_common.h @@ -36,9 +36,12 @@ class MainCommon std::ostream* os, const std::vector* only = nullptr); void handle_frat_option(); + void handle_idrup_option(); string frat_fname; + string idrup_fname; FILE* fratf = nullptr; + FILE* idrupf = nullptr; bool zero_exit_status = false; CMSat::SolverConf conf; unsigned num_threads = 1; diff --git a/src/occsimplifier.cpp b/src/occsimplifier.cpp index 000171b02..de4c030cc 100644 --- a/src/occsimplifier.cpp +++ b/src/occsimplifier.cpp @@ -2999,7 +2999,7 @@ bool OccSimplifier::uneliminate(uint32_t var) Lit l = elimed_cls[at_elimed_cls].at(bat, elimed_cls_lits); if (l == lit_Undef) { if (is_xor) solver->add_xor_clause_outside(lits, true); - else solver->add_clause_outside(lits); + else solver->add_clause_outside(lits, false, true); if (!solver->okay()) return false; lits.clear(); } else { @@ -3029,7 +3029,7 @@ void OccSimplifier::remove_by_frat_recently_elimed_clauses(size_t origElimedSize if (l == lit_Undef) { const int32_t id = newly_elimed_cls_IDs[at_ID++]; if (elimed_cls[i].is_xor) *solver->frat << delx << id << lits << fin; - else *solver->frat << del << id << lits << fin; + else *solver->frat << weakencl << id << lits << fin; lits.clear(); } else { lits.push_back(solver->map_outer_to_inter(l)); diff --git a/src/propengine.h b/src/propengine.h index 5f45f7ae6..6ab32bee2 100644 --- a/src/propengine.h +++ b/src/propengine.h @@ -589,7 +589,8 @@ void PropEngine::enqueue(const Lit p, const uint32_t level, const PropBy from, b } *frat << add << ID << p << fin; - *frat << implyxfromcls << XID << p << fratchain << ID << fin; + if (frat && !frat->incremental()) + *frat << implyxfromcls << XID << p << fratchain << ID << fin; assert(unit_cl_IDs[v] == 0); assert(unit_cl_XIDs[v] == 0); diff --git a/src/searcher.cpp b/src/searcher.cpp index cade83d64..5fda1a39a 100644 --- a/src/searcher.cpp +++ b/src/searcher.cpp @@ -1444,7 +1444,8 @@ void Searcher::attach_and_enqueue_learnt_clause( assert(ID != 0); unit_cl_IDs[v] = ID; const auto XID = ++clauseXID; - *frat << implyxfromcls << XID << learnt_clause[0] << fratchain << ID << fin; + if (!frat->incremental()) + *frat << implyxfromcls << XID << learnt_clause[0] << fratchain << ID << fin; unit_cl_XIDs[v] = XID; } enqueue(learnt_clause[0], level, PropBy(), false); diff --git a/src/solver.cpp b/src/solver.cpp index 1b81d8742..33f21bd80 100644 --- a/src/solver.cpp +++ b/src/solver.cpp @@ -67,6 +67,7 @@ THE SOFTWARE. #include "gaussian.h" #include "sqlstats.h" #include "frat.h" +#include "idrup.h" #include "xorfinder.h" #include "cardfinder.h" #include "sls.h" @@ -729,12 +730,14 @@ bool Solver::add_clause_helper(vector& ps) { return true; } - -bool Solver::add_clause_outer(vector& ps, bool red) +// Takes OUTER (NOT *outside*) variables +// Input is ORIGINAL clause. +bool Solver::add_clause_outer(vector& ps, const vector& outer_ps, bool red, bool restore) { ClauseStats clstats; clstats.ID = ++clauseID; - *frat << origcl << clstats.ID << ps << fin; + if (!restore) + *frat << "add_clause_outer\n" << origcl << clstats.ID << outer_ps << fin; if (red) clstats.which_red_array = 2; VERBOSE_PRINT("Adding clause " << ps); @@ -745,6 +748,9 @@ bool Solver::add_clause_outer(vector& ps, bool red) return false; } + if (frat->incremental()) // import the "inner version with duplicates removed" + *frat << "learning renumbered\n" << add << clstats.ID << ps << fin; + std::sort(ps.begin(), ps.end()); if (red) assert(!frat->enabled() && "Cannot have both FRAT and adding of redundant clauses"); Clause *cl = add_clause_int( @@ -756,9 +762,18 @@ bool Solver::add_clause_outer(vector& ps, bool red) , true //add frat? , lit_Undef , true //sorted - , true //remove old clause from proof if we changed it + , !frat->incremental() //remove old clause from proof if we changed it ); + if (frat->incremental()) {// del the "inner version with duplicates removed" + if (cl) { + *frat << "learning renumbered clause\n" << add << *cl << fin; + } + *frat << "deleting old\n" << del << clstats.ID << ps << fin; + if (!restore) + *frat << "deleting old i\n" << del << clstats.ID << outer_ps << fin; + } + if (cl != nullptr) { ClOffset offset = cl_alloc.get_offset(cl); if (!red) longIrredCls.push_back(offset); @@ -1429,6 +1444,7 @@ lbool Solver::solve_with_assumptions( void Solver::write_final_frat_clauses() { if (!frat->enabled()) return; + if (frat->incremental()) return; assert(decisionLevel() == 0); frat_func_start(); @@ -2716,13 +2732,19 @@ void Solver::add_in_partial_solving_stats() sumPropStats += propStats; } -bool Solver::add_clause_outside(const vector& lits, bool red) +bool Solver::add_clause_outside(const vector& lits, bool red, bool restore) { - if (!ok) return false; + if (!ok) { + if (frat->incremental()) + *frat << "new outside\n" << origcl << lits << fin; + return false; + }; + if (restore && frat->incremental() && !lits.empty()) + *frat << restorecl << lits << fin; SLOW_DEBUG_DO(check_too_large_variable_number(lits)); //we check for this during back-numbering vector tmp(lits); - return add_clause_outer(tmp, red); + return add_clause_outer(tmp, lits, red, restore); } bool Solver::add_xor_clause_outside(const vector& lits_out, bool rhs) { @@ -3698,6 +3720,29 @@ void Solver::detach_clauses_in_xors() { << conf.print_times(cpuTime() - my_time)); } +void Solver::conclude_idrup (lbool result) +{ + if (result == l_True) { + *frat << satisfiable; + *frat << modelF; + for (size_t cmVar = 0; cmVar < nVars(); ++cmVar) { + lbool value = model_value(cmVar); + *frat << Lit(cmVar, value != l_True); + } + *frat << fin; + } + else if (result == l_False) { + *frat << unsatisfiable; + *frat << unsatcore; + for (auto x: get_final_conflict()) { + *frat << ~x; + } + *frat << fin; + } + else + *frat << unknown; +} + /* // This needs to be an AIG actually, with an order of what to calculate first. */ /* void Solver::get_var_map(vector& var_map, map& var_set) const { */ diff --git a/src/solver.h b/src/solver.h index a6fbaeda4..92e08a338 100644 --- a/src/solver.h +++ b/src/solver.h @@ -93,7 +93,7 @@ class Solver : public Searcher const vector >& get_sql_tags() const; void new_external_var(); void new_external_vars(size_t n); - bool add_clause_outside(const vector& lits, bool red = false); + bool add_clause_outside(const vector& lits, bool red = false, bool restore = false); bool add_xor_clause_outside(const vector& vars, const bool rhs); bool add_xor_clause_outside(const vector& lits_out, bool rhs); bool add_bnn_clause_outside( @@ -113,6 +113,9 @@ class Solver : public Searcher vector probe_inter_tmp; lbool probe_outside(Lit l, uint32_t& min_props); void set_max_confl(uint64_t max_confl); + //frat for SAT problems + void add_empty_cl_to_frat(); + void conclude_idrup (lbool); void changed_sampling_vars(); //Querying model @@ -462,7 +465,7 @@ class Solver : public Searcher ///////////////////// // Clauses bool add_clause_helper(vector& ps); - bool add_clause_outer(vector& ps, bool red = false); + bool add_clause_outer(vector& ps, const vector& outer_ps, bool red = false, bool restore = false); ///////////////// // Debug @@ -540,6 +543,7 @@ inline void Solver::copy_assumptions(const vector* assumps) { } assumptions.push_back(lit); } + if (frat->incremental()) { *frat << assump << *assumps << fin; } } } diff --git a/src/solverconf.h b/src/solverconf.h index 7b5f18914..1203f2f6d 100644 --- a/src/solverconf.h +++ b/src/solverconf.h @@ -519,6 +519,7 @@ class DLL_PUBLIC SolverConf //Misc unsigned origSeed; int simulate_frat; + int idrup; int conf_needed = true; }; diff --git a/src/varreplacer.cpp b/src/varreplacer.cpp index 508e49a16..4dab64cb8 100644 --- a/src/varreplacer.cpp +++ b/src/varreplacer.cpp @@ -291,9 +291,10 @@ bool VarReplacer::perform_replace() { void VarReplacer::delete_frat_cls() { - for(const auto& f: bins_for_frat) { - *solver->frat << del << std::get<0>(f) << std::get<1>(f) << std::get<2>(f) << fin; - } + if (!solver->frat->incremental()) // for incremental we need to keep the reason for equivalences + for(const auto& f: bins_for_frat) { + *solver->frat << del << std::get<0>(f) << std::get<1>(f) << std::get<2>(f) << fin; + } bins_for_frat.clear(); }