summaryrefslogtreecommitdiff
path: root/cryptominisat5/cryptominisat-5.6.3/src/occsimplifier.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'cryptominisat5/cryptominisat-5.6.3/src/occsimplifier.cpp')
-rw-r--r--cryptominisat5/cryptominisat-5.6.3/src/occsimplifier.cpp3086
1 files changed, 3086 insertions, 0 deletions
diff --git a/cryptominisat5/cryptominisat-5.6.3/src/occsimplifier.cpp b/cryptominisat5/cryptominisat-5.6.3/src/occsimplifier.cpp
new file mode 100644
index 000000000..c0459eb91
--- /dev/null
+++ b/cryptominisat5/cryptominisat-5.6.3/src/occsimplifier.cpp
@@ -0,0 +1,3086 @@
+/******************************************
+Copyright (c) 2016, Mate Soos
+
+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 "time_mem.h"
+#include <cassert>
+#include <iomanip>
+#include <cmath>
+#include <algorithm>
+#include <set>
+#include <algorithm>
+#include <fstream>
+#include <set>
+#include <iostream>
+#include <limits>
+#include <cmath>
+#include <functional>
+
+
+#include "popcnt.h"
+#include "occsimplifier.h"
+#include "clause.h"
+#include "solver.h"
+#include "clausecleaner.h"
+#include "constants.h"
+#include "solutionextender.h"
+#include "varreplacer.h"
+#include "varupdatehelper.h"
+#include "completedetachreattacher.h"
+#include "subsumestrengthen.h"
+#include "watchalgos.h"
+#include "clauseallocator.h"
+#include "toplevelgaussabst.h"
+#include "subsumeimplicit.h"
+#include "sqlstats.h"
+#include "datasync.h"
+#include "xorfinder.h"
+#include "bva.h"
+#include "trim.h"
+
+#ifdef USE_M4RI
+#include "toplevelgauss.h"
+#endif
+
+//#define VERBOSE_DEBUG
+#ifdef VERBOSE_DEBUG
+#define BIT_MORE_VERBOSITY
+#define VERBOSE_ORGATE_REPLACE
+#define VERBOSE_ASYMTE
+#define VERBOSE_GATE_REMOVAL
+#define VERBOSE_XORGATE_MIX
+#define VERBOSE_DEBUG_XOR_FINDER
+#define VERBOSE_DEBUG_VARELIM
+#endif
+
+using namespace CMSat;
+using std::cout;
+using std::endl;
+
+//#define VERBOSE_DEBUG_VARELIM
+//#define VERBOSE_DEBUG_XOR_FINDER
+//#define BIT_MORE_VERBOSITY
+//#define TOUCH_LESS
+//#define VERBOSE_ORGATE_REPLACE
+//#define VERBOSE_DEBUG_ASYMTE
+//#define VERBOSE_GATE_REMOVAL
+//#define VERBOSE_XORGATE_MIX
+//#define CHECK_N_OCCUR
+//#define DEBUG_VARELIM
+
+OccSimplifier::OccSimplifier(Solver* _solver):
+ solver(_solver)
+ , seen(solver->seen)
+ , seen2(solver->seen2)
+ , toClear(solver->toClear)
+ , velim_order(VarOrderLt(varElimComplexity))
+ , topLevelGauss(NULL)
+ //, gateFinder(NULL)
+ , anythingHasBeenBlocked(false)
+ , blockedMapBuilt(false)
+{
+ bva = new BVA(solver, this);
+ topLevelGauss = new TopLevelGaussAbst;
+ #ifdef USE_M4RI
+ delete topLevelGauss;
+ topLevelGauss = new TopLevelGauss(solver);
+ #endif
+ sub_str = new SubsumeStrengthen(this, solver);
+
+ if (solver->conf.doGateFind) {
+ //gateFinder = new GateFinder(this, solver);
+ }
+ tmp_bin_cl.resize(2);
+}
+
+OccSimplifier::~OccSimplifier()
+{
+ delete bva;
+ delete topLevelGauss;
+ delete sub_str;
+ //delete gateFinder;
+}
+
+void OccSimplifier::new_var(const uint32_t /*orig_outer*/)
+{
+ n_occurs.insert(n_occurs.end(), 2, 0);
+ if (solver->conf.independent_vars) {
+ indep_vars.insert(indep_vars.end(), 1, 0);
+ }
+}
+
+void OccSimplifier::new_vars(size_t n)
+{
+ n_occurs.insert(n_occurs.end(), n*2ULL, 0);
+ if (solver->conf.independent_vars) {
+ indep_vars.insert(indep_vars.end(), n, 0);
+ }
+}
+
+void OccSimplifier::save_on_var_memory()
+{
+ clauses.clear();
+ clauses.shrink_to_fit();
+ blkcls.shrink_to_fit();
+
+ cl_to_free_later.shrink_to_fit();
+
+ elim_calc_need_update.shrink_to_fit();
+ blockedClauses.shrink_to_fit();;
+}
+
+void OccSimplifier::print_blocked_clauses_reverse() const
+{
+ for(vector<BlockedClauses>::const_reverse_iterator
+ it = blockedClauses.rbegin(), end = blockedClauses.rend()
+ ; it != end
+ ; ++it
+ ) {
+ size_t at = 1;
+ vector<Lit> lits;
+ while(at < it->size()) {
+ Lit l = it->at(at, blkcls);
+ if (l == lit_Undef) {
+ cout
+ << "blocked clause (internal number):";
+ for(size_t i = 0; i < it->size(); i++) {
+ cout << it->at(i, blkcls) << " ";
+ }
+ cout << endl;
+ lits.clear();
+ } else {
+ lits.push_back(l);
+ }
+ at++;
+ }
+
+ cout
+ << "dummy blocked clause for var (internal number) " << it->at(0, blkcls).var()
+ << endl;
+
+ }
+}
+
+void OccSimplifier::dump_blocked_clauses(std::ostream* outfile) const
+{
+ for (BlockedClauses blocked: blockedClauses) {
+ if (blocked.toRemove)
+ continue;
+
+ for (size_t i = 0; i < blocked.size(); i++) {
+ //It's blocked on this variable
+ if (i == 0) {
+ continue;
+ }
+ Lit l = blocked.at(i, blkcls);
+ if (l == lit_Undef) {
+ *outfile
+ << " 0"
+ << endl;
+ } else {
+ *outfile
+ << l << " ";
+ }
+ }
+ }
+}
+
+void OccSimplifier::extend_model(SolutionExtender* extender)
+{
+ //Either a variable is not eliminated, or its value is undef
+ for(size_t i = 0; i < solver->nVarsOuter(); i++) {
+ const uint32_t outer = solver->map_inter_to_outer(i);
+ assert(solver->varData[i].removed != Removed::elimed
+ || (solver->value(i) == l_Undef && solver->model_value(outer) == l_Undef)
+ );
+ }
+
+ #ifdef VERBOSE_DEBUG_RECONSTRUCT
+ cout << "Number of blocked clauses:" << blockedClauses.size() << endl;
+ print_blocked_clauses_reverse();
+ #endif
+
+ //go through in reverse order
+ vector<Lit> lits;
+ for (int i = (int)blockedClauses.size()-1; i >= 0; i--) {
+ BlockedClauses* it = &blockedClauses[i];
+ if (it->toRemove) {
+ continue;
+ }
+
+ Lit blockedOn = solver->varReplacer->get_lit_replaced_with_outer(it->at(0, blkcls));
+ size_t at = 1;
+ bool satisfied = false;
+ while(at < it->size()) {
+ if (it->at(at, blkcls) == lit_Undef) {
+ if (!satisfied) {
+ bool var_set = extender->addClause(lits, blockedOn.var());
+
+ #ifndef DEBUG_VARELIM
+ //all should be satisfied in fact
+ //no need to go any further
+ if (var_set)
+ break;
+ #endif
+ }
+ satisfied = false;
+ lits.clear();
+ } else if (!satisfied) {
+ Lit l = it->at(at, blkcls);
+ l = solver->varReplacer->get_lit_replaced_with_outer(l);
+
+ //Blocked clause can be skipped, it's satisfied
+ if (solver->model_value(l) == l_True) {
+ satisfied = true;
+ }
+ lits.push_back(l);
+ }
+ at++;
+ }
+ extender->dummyBlocked(blockedOn.var());
+ }
+ if (solver->conf.verbosity >= 2) {
+ cout << "c [extend] Extended " << blockedClauses.size() << " var-elim clauses" << endl;
+ }
+}
+
+void OccSimplifier::unlink_clause(
+ const ClOffset offset
+ , bool doDrat
+ , bool allow_empty_watch
+ , bool only_set_is_removed
+) {
+ Clause& cl = *solver->cl_alloc.ptr(offset);
+ if (doDrat && (solver->drat->enabled() || solver->conf.simulate_drat)) {
+ (*solver->drat) << del << cl << fin;
+ }
+
+ if (!cl.red()) {
+ for (const Lit lit: cl) {
+ elim_calc_need_update.touch(lit.var());
+#ifdef CHECK_N_OCCUR
+ assert(n_occurs[lit.toInt()]>0);
+#endif
+ n_occurs[lit.toInt()]--;
+ removed_cl_with_var.touch(lit.var());
+ }
+ }
+
+ if (!only_set_is_removed) {
+ for (const Lit lit: cl) {
+ if (!(allow_empty_watch && solver->watches[lit].empty())) {
+ *limit_to_decrease -= 2*(long)solver->watches[lit].size();
+ removeWCl(solver->watches[lit], offset);
+ }
+ }
+ } else {
+ for (const Lit lit: cl) {
+ solver->watches.smudge(lit);
+ }
+ }
+ cl.setRemoved();
+
+ if (cl.red()) {
+ solver->litStats.redLits -= cl.size();
+ } else {
+ solver->litStats.irredLits -= cl.size();
+ }
+
+ if (!only_set_is_removed) {
+ solver->cl_alloc.clauseFree(&cl);
+ } else {
+ cl_to_free_later.push_back(offset);
+ }
+}
+
+lbool OccSimplifier::clean_clause(ClOffset offset)
+{
+ assert(!solver->drat->something_delayed());
+ assert(solver->ok);
+
+ bool satisfied = false;
+ Clause& cl = *solver->cl_alloc.ptr(offset);
+ (*solver->drat) << deldelay << cl << fin;
+
+ Lit* i = cl.begin();
+ Lit* j = cl.begin();
+ const Lit* end = cl.end();
+ *limit_to_decrease -= (long)cl.size();
+ for(; i != end; i++) {
+ if (solver->value(*i) == l_Undef) {
+ //clean_clause() is called when the clause changed, so this is relevant
+ added_cl_to_var.touch(i->var());
+ *j++ = *i;
+ continue;
+ }
+
+ if (solver->value(*i) == l_True)
+ satisfied = true;
+
+ if (solver->value(*i) == l_True
+ || solver->value(*i) == l_False
+ ) {
+ removeWCl(solver->watches[*i], offset);
+ if (!cl.red()) {
+ removed_cl_with_var.touch(i->var());
+ elim_calc_need_update.touch(i->var());
+ n_occurs[i->toInt()]--;
+ }
+ }
+ }
+ cl.shrink(i-j);
+ cl.recalc_abst_if_needed();
+
+ //Update lits stat
+ if (cl.red()) {
+ solver->litStats.redLits -= i-j;
+ } else {
+ solver->litStats.irredLits -= i-j;
+ }
+
+ if (satisfied) {
+ (*solver->drat) << findelay;
+ unlink_clause(offset, false);
+ return l_True;
+ }
+
+ if (solver->conf.verbosity >= 6) {
+ cout << "-> Clause became after cleaning:" << cl << endl;
+ }
+
+ if (i-j > 0) {
+ (*solver->drat) << add << cl
+ #ifdef STATS_NEEDED
+ << solver->sumConflicts
+ #endif
+ << fin << findelay;
+ } else {
+ solver->drat->forget_delay();
+ }
+
+ switch(cl.size()) {
+ case 0:
+ unlink_clause(offset, false);
+ solver->ok = false;
+ return l_False;
+
+ case 1:
+ solver->enqueue(cl[0]);
+ #ifdef STATS_NEEDED
+ solver->propStats.propsUnit++;
+ #endif
+ unlink_clause(offset, false);
+ return l_True;
+
+ case 2: {
+ solver->attach_bin_clause(cl[0], cl[1], cl.red());
+ if (!cl.red()) {
+ std::pair<Lit, Lit> tmp = {cl[0], cl[1]};
+ added_bin_cl.push_back(tmp);
+ n_occurs[tmp.first.toInt()]++;
+ n_occurs[tmp.second.toInt()]++;
+ }
+ unlink_clause(offset, false);
+ return l_True;
+ }
+ default:
+ cl.setStrenghtened();
+ cl.recalc_abst_if_needed();
+ if (!cl.red()) {
+ added_long_cl.push_back(offset);
+ }
+ return l_Undef;
+ }
+}
+
+
+bool OccSimplifier::complete_clean_clause(Clause& cl)
+{
+ assert(!solver->drat->something_delayed());
+ assert(cl.size() > 2);
+ (*solver->drat) << deldelay << cl << fin;
+
+ //Remove all lits from stats
+ //we will re-attach the clause either way
+ if (cl.red()) {
+ solver->litStats.redLits -= cl.size();
+ } else {
+ solver->litStats.irredLits -= cl.size();
+ }
+
+ Lit *i = cl.begin();
+ Lit *j = i;
+ for (Lit *end = cl.end(); i != end; i++) {
+ if (solver->value(*i) == l_True) {
+
+ (*solver->drat) << findelay;
+ return false;
+ }
+
+ if (solver->value(*i) == l_Undef) {
+ *j++ = *i;
+ }
+ }
+ cl.shrink(i-j);
+ cl.recalc_abst_if_needed();
+
+ //Drat
+ if (i - j > 0) {
+ (*solver->drat) << add << cl
+ #ifdef STATS_NEEDED
+ << solver->sumConflicts
+ #endif
+ << fin << findelay;
+ } else {
+ solver->drat->forget_delay();
+ }
+
+ switch (cl.size()) {
+ case 0:
+ solver->ok = false;
+ return false;
+
+ case 1:
+ solver->enqueue(cl[0]);
+ #ifdef STATS_NEEDED
+ solver->propStats.propsUnit++;
+ #endif
+ return false;
+
+ case 2:
+ solver->attach_bin_clause(cl[0], cl[1], cl.red());
+ return false;
+
+ default:
+ return true;
+ }
+}
+
+uint64_t OccSimplifier::calc_mem_usage_of_occur(const vector<ClOffset>& toAdd) const
+{
+ uint64_t memUsage = 0;
+ for (vector<ClOffset>::const_iterator
+ it = toAdd.begin(), end = toAdd.end()
+ ; it != end
+ ; ++it
+ ) {
+ Clause* cl = solver->cl_alloc.ptr(*it);
+ //*2 because of the overhead of allocation
+ memUsage += cl->size()*sizeof(Watched)*2;
+ }
+
+ //Estimate malloc overhead
+ memUsage += solver->num_active_vars()*2*40;
+
+ return memUsage;
+}
+
+void OccSimplifier::print_mem_usage_of_occur(uint64_t memUsage) const
+{
+ if (solver->conf.verbosity) {
+ cout
+ << "c [occ] mem usage for occur "
+ << std::setw(6) << memUsage/(1024ULL*1024ULL) << " MB"
+ << endl;
+ }
+}
+
+void OccSimplifier::print_linkin_data(const LinkInData link_in_data) const
+{
+ if (solver->conf.verbosity < 2)
+ return;
+
+ double val;
+ if (link_in_data.cl_linked + link_in_data.cl_not_linked == 0) {
+ val = 0;
+ } else {
+ val = float_div(link_in_data.cl_not_linked, link_in_data.cl_linked+link_in_data.cl_not_linked)*100.0;
+ }
+
+ cout
+ << "c [occ] Not linked in "
+ << link_in_data.cl_not_linked << "/"
+ << (link_in_data.cl_linked + link_in_data.cl_not_linked)
+ << " ("
+ << std::setprecision(2) << std::fixed
+ << val
+ << " %)"
+ << endl;
+}
+
+
+OccSimplifier::LinkInData OccSimplifier::link_in_clauses(
+ const vector<ClOffset>& toAdd
+ , bool alsoOccur
+ , uint32_t max_size
+ , int64_t link_in_lit_limit
+) {
+ LinkInData link_in_data;
+ for (const ClOffset offs: toAdd) {
+ Clause* cl = solver->cl_alloc.ptr(offs);
+ cl->recalc_abst_if_needed();
+ assert(cl->abst == calcAbstraction(*cl));
+
+ if (alsoOccur
+ && cl->size() < max_size
+ && link_in_lit_limit > 0
+ ) {
+ linkInClause(*cl);
+ link_in_data.cl_linked++;
+ link_in_lit_limit -= cl->size();
+ clause_lits_added += cl->size();
+ } else {
+ /*cout << "alsoOccur: " << alsoOccur
+ << " cl->size() < max_size: " << (cl->size() < max_size)
+ << " link_in_lit_limit: " << link_in_lit_limit << endl;*/
+ //assert(cl->red());
+ cl->setOccurLinked(false);
+ link_in_data.cl_not_linked++;
+ std::sort(cl->begin(), cl->end());
+ }
+
+ clauses.push_back(offs);
+ }
+
+ return link_in_data;
+}
+
+bool OccSimplifier::decide_occur_limit(bool irred, uint64_t memUsage)
+{
+ //over + irred -> exit
+ if (irred
+ && (double)memUsage/(1024.0*1024.0) >= solver->conf.maxOccurIrredMB
+ ) {
+ if (solver->conf.verbosity) {
+ cout
+ << "c [simp] Not linking in irred due to excessive expected memory usage"
+ << endl;
+ }
+ return false;
+ }
+
+ //over + red -> don't link
+ if (!irred
+ && (double)memUsage/(1024.0*1024.0) >= solver->conf.maxOccurRedMB
+ ) {
+ if (solver->conf.verbosity) {
+ cout
+ << "c [simp] Not linking in red due to excessive expected memory usage"
+ << endl;
+ }
+
+ return false;
+ }
+
+ return true;
+}
+
+bool OccSimplifier::check_varelim_when_adding_back_cl(const Clause* cl) const
+{
+ bool notLinkedNeedFree = false;
+ for (Clause::const_iterator
+ it2 = cl->begin(), end2 = cl->end()
+ ; it2 != end2
+ ; it2++
+ ) {
+ //The clause was too long, and wasn't linked in
+ //but has been var-elimed, so remove it
+ if (!cl->getOccurLinked()
+ && solver->varData[it2->var()].removed == Removed::elimed
+ ) {
+ notLinkedNeedFree = true;
+ }
+
+ if (cl->getOccurLinked()
+ && solver->varData[it2->var()].removed != Removed::none
+ ) {
+ std::cerr
+ << "ERROR! Clause " << *cl
+ << " red: " << cl->red()
+ << " contains lit " << *it2
+ << " which has removed status"
+ << removed_type_to_string(solver->varData[it2->var()].removed)
+ << endl;
+
+ assert(false);
+ std::exit(-1);
+ }
+ }
+
+ return notLinkedNeedFree;
+}
+
+void OccSimplifier::add_back_to_solver()
+{
+ for (ClOffset offs: clauses) {
+ Clause* cl = solver->cl_alloc.ptr(offs);
+ if (cl->freed())
+ continue;
+
+ assert(!cl->getRemoved());
+
+ //All clauses are larger than 2-long
+ assert(cl->size() > 2);
+
+ if (check_varelim_when_adding_back_cl(cl)) {
+ //The clause wasn't linked in but needs removal now
+ if (cl->red()) {
+ solver->litStats.redLits -= cl->size();
+ } else {
+ solver->litStats.irredLits -= cl->size();
+ }
+ solver->cl_alloc.clauseFree(cl);
+ continue;
+ }
+
+ if (complete_clean_clause(*cl)) {
+ solver->attachClause(*cl);
+ if (cl->red()) {
+ if (cl->stats.glue <= solver->conf.glue_put_lev0_if_below_or_eq) {
+ cl->stats.which_red_array = 0;
+ } else if (
+ cl->stats.glue <= solver->conf.glue_put_lev1_if_below_or_eq
+ && solver->conf.glue_put_lev1_if_below_or_eq != 0
+ ) {
+ cl->stats.which_red_array = 1;
+ }
+ solver->longRedCls[cl->stats.which_red_array].push_back(offs);
+ } else {
+ solver->longIrredCls.push_back(offs);
+ }
+ } else {
+ solver->cl_alloc.clauseFree(cl);
+ }
+ }
+}
+
+void OccSimplifier::remove_all_longs_from_watches()
+{
+ for (watch_array::iterator
+ it = solver->watches.begin(), end = solver->watches.end()
+ ; it != end
+ ; ++it
+ ) {
+ watch_subarray ws = *it;
+
+ Watched* i = ws.begin();
+ Watched* j = i;
+ for (Watched *end2 = ws.end(); i != end2; i++) {
+ if (i->isClause()) {
+ continue;
+ } else {
+ assert(i->isBin());
+ *j++ = *i;
+ }
+ }
+ ws.shrink(i - j);
+ }
+}
+
+void OccSimplifier::eliminate_empty_resolvent_vars()
+{
+ uint32_t var_elimed = 0;
+ double myTime = cpuTime();
+ const int64_t orig_empty_varelim_time_limit = empty_varelim_time_limit;
+ limit_to_decrease = &empty_varelim_time_limit;
+ assert(cl_to_free_later.empty());
+ assert(solver->watches.get_smudged_list().empty());
+
+ ///Nothing to do
+ if (solver->nVars() == 0)
+ return;
+
+ for(size_t var = solver->mtrand.randInt(solver->nVars()-1), num = 0
+ ; num < solver->nVars() && *limit_to_decrease > 0
+ ; var = (var + 1) % solver->nVars(), num++
+ ) {
+ assert(var == var % solver->nVars());
+ if (!can_eliminate_var(var))
+ continue;
+
+ const Lit lit = Lit(var, false);
+ if (!check_empty_resolvent(lit))
+ continue;
+
+ create_dummy_blocked_clause(lit);
+ rem_cls_from_watch_due_to_varelim(solver->watches[lit], lit);
+ rem_cls_from_watch_due_to_varelim(solver->watches[~lit], ~lit);
+ set_var_as_eliminated(var, lit);
+ var_elimed++;
+ }
+
+ solver->clean_occur_from_removed_clauses_only_smudged();
+ free_clauses_to_free();
+ const double time_used = cpuTime() - myTime;
+ const bool time_out = (*limit_to_decrease <= 0);
+ const double time_remain = float_div(*limit_to_decrease, orig_empty_varelim_time_limit);
+ if (solver->conf.verbosity) {
+ cout
+ << "c [occ-empty-res] Empty resolvent elimed: " << var_elimed
+ << solver->conf.print_times(time_used, time_out)
+ << endl;
+ }
+ if (solver->sqlStats) {
+ solver->sqlStats->time_passed(
+ solver
+ , "empty resolvent"
+ , time_used
+ , time_out
+ , time_remain
+ );
+ }
+}
+
+bool OccSimplifier::can_eliminate_var(const uint32_t var) const
+{
+ #ifdef SLOW_DEBUG
+ if (solver->conf.independent_vars) {
+ assert(var < solver->nVars());
+ assert(var < indep_vars.size());
+ }
+ #endif
+
+ assert(var < solver->nVars());
+ if (solver->value(var) != l_Undef
+ || solver->varData[var].removed != Removed::none
+ || solver->var_inside_assumptions(var)
+ || (solver->conf.independent_vars && indep_vars[var])
+ //|| (!solver->conf.allow_elim_xor_vars && solver->varData[var].added_for_xor)
+ ) {
+ return false;
+ }
+
+ return true;
+}
+
+uint32_t OccSimplifier::sum_irred_cls_longs() const
+{
+ uint32_t sum = 0;
+ for (ClOffset offs: clauses) {
+ Clause* cl = solver->cl_alloc.ptr(offs);
+ if (cl->freed() || cl->getRemoved() || cl->red())
+ continue;
+
+ assert(cl->size() > 2);
+ sum++;
+ }
+ return sum;
+}
+
+uint32_t OccSimplifier::sum_irred_cls_longs_lits() const
+{
+ uint32_t sum = 0;
+ for (ClOffset offs: clauses) {
+ Clause* cl = solver->cl_alloc.ptr(offs);
+ if (cl->freed() || cl->getRemoved() || cl->red())
+ continue;
+
+ assert(cl->size() > 2);
+ sum += cl->size();
+ }
+ return sum;
+}
+
+bool OccSimplifier::deal_with_added_long_and_bin(const bool main)
+{
+ while (!added_long_cl.empty() && !added_bin_cl.empty())
+ {
+ if (!sub_str->handle_added_long_cl(limit_to_decrease, main)) {
+ return false;
+ }
+ added_long_cl.clear();
+
+ //NOTE: added_bin_cl CAN CHANGE while this is running!!
+ for (size_t i = 0; i < added_bin_cl.size(); i++) {
+ tmp_bin_cl[0] = added_bin_cl[i].first;
+ tmp_bin_cl[1] = added_bin_cl[i].second;
+
+ sub_str->backw_sub_str_long_with_implicit(tmp_bin_cl);
+ if (!solver->okay()) {
+ return false;
+ }
+ }
+ added_bin_cl.clear();
+ }
+ return true;
+}
+
+bool OccSimplifier::clear_vars_from_cls_that_have_been_set(size_t& last_trail)
+{
+ //BUG TODO
+ //solver->clauseCleaner->clean_implicit_clauses();
+
+ vector<ClOffset> cls_to_clean;
+ while(last_trail < solver->trail_size()) {
+ Lit l = solver->trail_at(last_trail++);
+ watch_subarray ws = solver->watches[l];
+ for (Watched& w: ws) {
+ if (w.isClause()) {
+ ClOffset offs = w.get_offset();
+ Clause* cl = solver->cl_alloc.ptr(offs);
+ if (cl->getRemoved() || cl->freed()) {
+ continue;
+ }
+ cls_to_clean.push_back(offs);
+ }
+ }
+
+ l = ~l;
+ watch_subarray ws2 = solver->watches[l];
+ for(Watched& w: ws2) {
+ if (w.isClause()) {
+ ClOffset offs = w.get_offset();
+ Clause* cl = solver->cl_alloc.ptr(offs);
+ if (cl->getRemoved() || cl->freed()) {
+ continue;
+ }
+ cls_to_clean.push_back(offs);
+ }
+ }
+ }
+ for(ClOffset offs: cls_to_clean) {
+ Clause* cl = solver->cl_alloc.ptr(offs);
+ if (!cl->getRemoved() && !cl->freed()) {
+ lbool ret = clean_clause(offs);
+ if (ret == l_False) {
+ return false;
+ }
+ }
+ }
+
+ return true;
+}
+
+bool OccSimplifier::deal_with_added_cl_to_var_lit(const Lit lit)
+{
+ watch_subarray_const cs = solver->watches[lit];
+ *limit_to_decrease -= (long)cs.size()*2+ 40;
+ for (const Watched *it = cs.begin(), *end = cs.end()
+ ; it != end
+ ; ++it
+ ) {
+ if (it->isClause()) {
+ ClOffset offs = it->get_offset();
+ Clause* cl = solver->cl_alloc.ptr(offs);
+
+ //Has already been removed or added to "added_long_cl"
+ if (cl->freed() || cl->getRemoved() || cl->stats.marked_clause)
+ continue;
+
+ cl->stats.marked_clause = 1;
+ added_long_cl.push_back(offs);
+ }
+ }
+ return true;
+}
+
+bool OccSimplifier::prop_and_clean_long_and_impl_clauses()
+{
+ solver->ok = solver->propagate_occur();
+ if (!solver->okay()) {
+ return false;
+ }
+
+ for(ClOffset offs: clauses) {
+ Clause* cl = solver->cl_alloc.ptr(offs);
+ if (!cl->getRemoved() && !cl->freed() && cl->getOccurLinked()) {
+ lbool ret = clean_clause(offs);
+ if (ret == l_False) {
+ return false;
+ }
+ }
+ }
+
+ //BUG TODO
+ //solver->clauseCleaner->clean_implicit_clauses();
+
+ solver->clean_occur_from_removed_clauses_only_smudged();
+ return true;
+}
+
+bool OccSimplifier::simulate_frw_sub_str_with_added_cl_to_var()
+{
+ limit_to_decrease = &varelim_sub_str_limit;
+
+ //during the deal_with_added_cl_to_var_lit() below, we mark the clauses
+ //so we don't add the same clause twice
+ for(uint32_t i = 0
+ ; i < added_cl_to_var.getTouchedList().size()
+ && *limit_to_decrease > 0
+ && !solver->must_interrupt_asap()
+ ; i++
+ ) {
+ uint32_t var = added_cl_to_var.getTouchedList()[i];
+ Lit lit = Lit(var, true);
+ if (!sub_str->backw_sub_str_long_with_bins_watch(lit, false)) {
+ return false;
+ }
+ if (!deal_with_added_cl_to_var_lit(lit)) {
+ return false;
+ }
+
+ lit = ~lit;
+ if (!sub_str->backw_sub_str_long_with_bins_watch(lit, false)) {
+ return false;
+ }
+ if (!deal_with_added_cl_to_var_lit(lit)) {
+ return false;
+ }
+ }
+ added_cl_to_var.clear();
+
+ //here, we clean the marks on the clauses, even in case of timeout/abort
+ if (!sub_str->handle_added_long_cl(&varelim_sub_str_limit, false)) {
+ return false;
+ }
+ limit_to_decrease = &norm_varelim_time_limit;
+
+ return true;
+}
+
+bool OccSimplifier::eliminate_vars()
+{
+ //solver->conf.verbosity = 1;
+ //Set-up
+ size_t last_trail = solver->trail_size();
+ double myTime = cpuTime();
+ size_t vars_elimed = 0;
+ size_t wenThrough = 0;
+ time_spent_on_calc_otf_update = 0;
+ num_otf_update_until_now = 0;
+ int64_t orig_norm_varelim_time_limit = norm_varelim_time_limit;
+ limit_to_decrease = &norm_varelim_time_limit;
+ cl_to_free_later.clear();
+ assert(solver->watches.get_smudged_list().empty());
+ bvestats.clear();
+ bvestats.numCalls = 1;
+
+ //Go through the ordered list of variables to eliminate
+ int64_t last_elimed = 1;
+ grow = 0;
+ uint32_t n_cls_last = sum_irred_cls_longs() + solver->binTri.irredBins;
+ uint32_t n_cls_init = n_cls_last;
+ uint32_t n_vars_last = solver->get_num_free_vars();
+
+
+ added_bin_cl.clear();
+
+ //For debug ONLY
+ // subsume with bins everywhere first
+// for(uint32_t i = 0; i < solver->nVars(); i++) {
+// Lit lit = Lit(i, false);
+// if (!sub_str->backw_sub_str_long_with_bins_watch(lit, false)) {
+// goto end;
+// }
+//
+// lit = Lit(i, true);
+// if (!sub_str->backw_sub_str_long_with_bins_watch(lit, false)) {
+// goto end;
+// }
+// if (*limit_to_decrease <= 0)
+// break;
+// }
+ //
+
+ if (!prop_and_clean_long_and_impl_clauses()) {
+ goto end;
+ }
+ last_trail = solver->trail_size();
+
+ while(varelim_num_limit > 0
+ && *limit_to_decrease > 0
+ && grow < (uint32_t)solver->conf.min_bva_gain
+ //&& grow < 1 //solver->conf.min_bva_gain
+ ) {
+ if (solver->conf.verbosity >= 2) {
+ cout << "c x n vars : " << solver->get_num_free_vars() << endl;
+ #ifdef DEBUG_VARELIM
+ cout << "c x cls long : " << sum_irred_cls_longs() << endl;
+ cout << "c x cls bin : " << solver->binTri.irredBins << endl;
+ cout << "c x long cls lits: " << sum_irred_cls_longs_lits() << endl;
+ #endif
+ }
+
+ last_elimed = 0;
+ limit_to_decrease = &norm_varelim_time_limit;
+ order_vars_for_elim();
+
+ added_cl_to_var.clear();
+ removed_cl_with_var.touch(Lit(0, false));
+ while(!removed_cl_with_var.getTouchedList().empty()
+ && *limit_to_decrease > 0
+ && !solver->must_interrupt_asap()
+ ) {
+ removed_cl_with_var.clear();
+ while(!velim_order.empty()
+ && *limit_to_decrease > 0
+ && varelim_num_limit > 0
+ && !solver->must_interrupt_asap()
+ ) {
+ assert(limit_to_decrease == &norm_varelim_time_limit);
+ uint32_t var = velim_order.removeMin();
+
+ //Stats
+ *limit_to_decrease -= 20;
+ wenThrough++;
+
+ if (!can_eliminate_var(var))
+ continue;
+
+ //Try to eliminate
+ elim_calc_need_update.clear();
+ if (maybe_eliminate(var)) {
+ vars_elimed++;
+ varelim_num_limit--;
+ last_elimed++;
+ }
+ if (!solver->ok)
+ goto end;
+
+ //SUB and STR for long and short
+ limit_to_decrease = &varelim_sub_str_limit;
+ if (!deal_with_added_long_and_bin(false)) {
+ limit_to_decrease = &norm_varelim_time_limit;
+ goto end;
+ }
+ limit_to_decrease = &norm_varelim_time_limit;
+
+ solver->ok = solver->propagate_occur();
+ if (!solver->okay()) {
+ goto end;
+ }
+
+ update_varelim_complexity_heap();
+ }
+
+ //Clean clauses that have vars that have been set
+ if (last_trail != solver->trail_size()) {
+ if (!clear_vars_from_cls_that_have_been_set(last_trail)) {
+ goto end;
+ }
+ }
+
+ solver->clean_occur_from_removed_clauses_only_smudged();
+ update_varelim_complexity_heap();
+
+
+ if (solver->conf.verbosity >= 2) {
+ cout <<"c size of added_cl_to_var : " << added_cl_to_var.getTouchedList().size() << endl;
+ cout <<"c size of removed_cl_with_var: " << removed_cl_with_var.getTouchedList().size() << endl;
+ }
+
+ if (!simulate_frw_sub_str_with_added_cl_to_var()) {
+ goto end;
+ }
+
+ for(uint32_t var: removed_cl_with_var.getTouchedList()) {
+ if (!can_eliminate_var(var)) {
+ continue;
+ }
+ varElimComplexity[var] = heuristicCalcVarElimScore(var);
+ velim_order.update(var);
+ }
+
+ if (solver->conf.verbosity >= 2) {
+ cout << "c x n vars : " << solver->get_num_free_vars() << endl;
+ #ifdef DEBUG_VARELIM
+ cout << "c x cls long : " << sum_irred_cls_longs() << endl;
+ cout << "c x cls bin : " << solver->binTri.irredBins << endl;
+ cout << "c x long cls lits: " << sum_irred_cls_longs_lits() << endl;
+ #endif
+ cout << "c another run ?"<< endl;
+ }
+ }
+ #ifdef DEBUG_VARELIM
+ if (solver->conf.verbosity >= 2) {
+ cout << "c finished here" << endl;
+ }
+ #endif
+ solver->clean_occur_from_removed_clauses_only_smudged();
+
+ //For debug ONLY
+ ///////////////
+// free_clauses_to_free();
+// // backward_sub_str();
+// // limit_to_decrease = &norm_varelim_time_limit;
+// solver->clauseCleaner->clean_implicit_clauses();
+// solver->clean_occur_from_removed_clauses();
+ ///////////////
+
+ uint32_t n_cls_now = sum_irred_cls_longs() + solver->binTri.irredBins;
+ uint32_t n_vars_now = solver->get_num_free_vars();
+ double cl_inc_rate = 2.0;
+ if (n_cls_last != 0) {
+ cl_inc_rate = (double)n_cls_now / n_cls_last;
+ }
+
+ double var_dec_rate = 1.0;
+ if (n_vars_now != 0) {
+ var_dec_rate = (double)n_vars_last / n_vars_now;
+ }
+ if (solver->conf.verbosity) {
+ cout << "c [occ-bve] iter v-elim " << last_elimed << endl;
+ cout << "c cl_inc_rate=" << cl_inc_rate
+ << ", var_dec_rate=" << var_dec_rate
+ << " (grow=" << grow << ")" << endl;
+
+ cout << "c Reduced to " << solver->get_num_free_vars() << " vars"
+ << ", " << sum_irred_cls_longs() + solver->binTri.irredBins
+ << " cls (grow=" << grow << ")" << endl;
+ }
+
+
+ if (n_cls_now > n_cls_init || cl_inc_rate > (var_dec_rate)) {
+ break;
+ }
+ n_cls_last = n_cls_now;
+ n_vars_last = n_vars_now;
+
+ if (grow == 0) {
+ grow = 8;
+ } else {
+ grow *= 2;
+ }
+ }
+
+ if (solver->conf.verbosity) {
+ cout << "c x n vars : " << solver->get_num_free_vars() << endl;
+ #ifdef DEBUG_VARELIM
+ cout << "c x cls long : " << sum_irred_cls_longs() << endl;
+ cout << "c x cls bin : " << solver->binTri.irredBins << endl;
+ cout << "c x long cls lits: " << sum_irred_cls_longs_lits() << endl;
+ #endif
+ }
+
+end:
+ free_clauses_to_free();
+ const double time_used = cpuTime() - myTime;
+ const bool time_out = (*limit_to_decrease <= 0);
+ const double time_remain = float_div(*limit_to_decrease, orig_norm_varelim_time_limit);
+
+ if (solver->conf.verbosity) {
+ cout
+ << "c #try to eliminate: "; print_value_kilo_mega(wenThrough); cout << endl
+ << "c #var-elim : "; print_value_kilo_mega(vars_elimed); cout << endl
+ << "c #T-o: " << (time_out ? "Y" : "N") << endl
+ << "c #T-r: " << std::fixed << std::setprecision(2) << (time_remain*100.0) << "%" << endl
+ << "c #T : " << time_used << endl;
+ }
+ if (solver->conf.verbosity) {
+ if (solver->conf.verbosity >= 3)
+ runStats.print(solver->nVars());
+ else
+ runStats.print_short();
+ }
+ if (solver->sqlStats) {
+ solver->sqlStats->time_passed(
+ solver
+ , "bve"
+ , time_used
+ , time_out
+ , time_remain
+ );
+ }
+
+ assert(limit_to_decrease == &norm_varelim_time_limit);
+ bvestats.varElimTimeOut += time_out;
+ bvestats.timeUsed = cpuTime() - myTime;
+ bvestats_global += bvestats;
+
+ //exit(0);
+ return solver->okay();
+}
+
+void OccSimplifier::free_clauses_to_free()
+{
+ for(ClOffset off: cl_to_free_later) {
+ Clause* cl = solver->cl_alloc.ptr(off);
+ solver->cl_alloc.clauseFree(cl);
+ }
+ cl_to_free_later.clear();
+}
+
+bool OccSimplifier::fill_occur_and_print_stats()
+{
+ double myTime = cpuTime();
+ remove_all_longs_from_watches();
+ if (!fill_occur()) {
+ return false;
+ }
+ sanityCheckElimedVars();
+ const double linkInTime = cpuTime() - myTime;
+ runStats.linkInTime += linkInTime;
+ if (solver->sqlStats) {
+ solver->sqlStats->time_passed_min(
+ solver
+ , "occur build"
+ , linkInTime
+ );
+ }
+
+ //Print memory usage after occur link-in
+ if (solver->conf.verbosity) {
+ double vm_usage = 0;
+ solver->print_watch_mem_used(memUsedTotal(vm_usage));
+ }
+
+ return true;
+}
+
+struct MyOccSorter
+{
+ MyOccSorter(const Solver* _solver) :
+ solver(_solver)
+ {
+ }
+ bool operator()(const Watched& w1, const Watched& w2)
+ {
+ if (w2.isBin())
+ return false;
+
+ if (w1.isBin() && !w2.isBin())
+ return true;
+
+ //both are non-bin
+ const Clause* cl1 = solver->cl_alloc.ptr(w1.get_offset());
+ const Clause* cl2 = solver->cl_alloc.ptr(w2.get_offset());
+
+ //The other is at least as good, this is removed
+ if (cl1->freed() || cl1->getRemoved())
+ return false;
+
+ //The other is not removed, so it's better
+ if (cl2->freed() || cl2->getRemoved())
+ return true;
+
+ const uint32_t sz1 = cl1->size();
+ const uint32_t sz2 = cl2->size();
+ return sz1 < sz2;
+ }
+
+ const Solver* solver;
+};
+
+void OccSimplifier::sort_occurs_and_set_abst()
+{
+ for(auto& ws: solver->watches) {
+ std::sort(ws.begin(), ws.end(), MyOccSorter(solver));
+
+ for(Watched& w: ws) {
+ if (w.isClause()) {
+ Clause* cl = solver->cl_alloc.ptr(w.get_offset());
+ if (cl->freed() || cl->getRemoved()) {
+ w.setBlockedLit(lit_Error);
+ } else if (cl->size() >solver->conf.maxXorToFind) {
+ w.setBlockedLit(lit_Undef);
+ } else {
+ w.setBlockedLit(Lit::toLit(cl->abst));
+ }
+ }
+ }
+ }
+}
+
+bool OccSimplifier::execute_simplifier_strategy(const string& strategy)
+{
+ std::istringstream ss(strategy);
+ std::string token;
+
+ while(std::getline(ss, token, ',')) {
+ if (cpuTime() > solver->conf.maxTime
+ || solver->must_interrupt_asap()
+ || solver->nVars() == 0
+ || !solver->ok
+ ) {
+ return solver->okay();
+ }
+
+ #ifdef SLOW_DEBUG
+ check_clid_correct();
+ solver->check_implicit_stats(true);
+ #endif
+ if (!solver->propagate_occur()) {
+ solver->ok = false;
+ return false;
+ }
+ set_limits();
+
+ token = trim(token);
+ std::transform(token.begin(), token.end(), token.begin(), ::tolower);
+ if (token != "" && solver->conf.verbosity) {
+ cout << "c --> Executing OCC strategy token: " << token << '\n';
+ }
+ if (token == "occ-backw-sub-str") {
+ backward_sub_str();
+ } else if (token == "occ-xor") {
+ if (solver->conf.doFindXors) {
+ XorFinder finder(this, solver);
+ finder.find_xors();
+ vector<Xor> xors = finder.xors;
+ if (!finder.xor_together_xors(xors))
+ return false;
+
+ vector<Lit> out_changed_occur;
+ solver->ok = finder.add_new_truths_from_xors(xors, &out_changed_occur);
+ if (!solver->ok)
+ return false;
+
+ #ifdef USE_M4RI
+ if (topLevelGauss != NULL) {
+ xors = finder.remove_xors_without_connecting_vars(xors);
+ topLevelGauss->toplevelgauss(xors, &out_changed_occur);
+ }
+ #endif
+ finder.add_xors_to_solver();
+
+ //these may have changed, recalculating occur
+ for(Lit lit: out_changed_occur) {
+ n_occurs[lit.toInt()] = calc_occ_data(lit);
+ n_occurs[(~lit).toInt()] = calc_occ_data(~lit);
+ }
+ }
+ } else if (token == "occ-clean-implicit") {
+ //BUG TODO
+ //solver->clauseCleaner->clean_implicit_clauses();
+ } else if (token == "occ-bve") {
+ if (solver->conf.doVarElim && solver->conf.do_empty_varelim) {
+ solver->xorclauses.clear();
+ #ifdef USE_GAUSS
+ solver->clearEnGaussMatrixes();
+ #endif
+
+ eliminate_empty_resolvent_vars();
+ eliminate_vars();
+ }
+ } else if (token == "occ-bva") {
+ bva->bounded_var_addition();
+ added_bin_cl.clear();
+ added_cl_to_var.clear();
+ added_long_cl.clear();
+ solver->clean_occur_from_removed_clauses_only_smudged();
+ } /*else if (token == "occ-gates") {
+ if (solver->conf.doCache
+ && solver->conf.doGateFind
+ ) {
+ gateFinder->doAll();
+ }
+ }*/ else if (token == "") {
+ //nothing, ignore empty token
+ } else {
+ cout << "ERROR: occur strategy '" << token << "' not recognised!" << endl;
+ exit(-1);
+ }
+
+#ifdef CHECK_N_OCCUR
+ check_n_occur();
+#endif //CHECK_N_OCCUR
+ }
+
+ if (solver->okay() &&
+ !solver->propagate_occur()
+ ) {
+ solver->ok = false;
+ return false;
+ }
+
+ return solver->okay();
+}
+
+bool OccSimplifier::setup()
+{
+ assert(solver->okay());
+ assert(toClear.empty());
+ added_long_cl.clear();
+ added_bin_cl.clear();
+ added_cl_to_var.clear();
+ n_occurs.clear();
+ n_occurs.resize(solver->nVars()*2, 0);
+
+ //Test & debug
+ #ifdef DEBUG_ATTACH_MORE
+ solver->test_all_clause_attached();
+ solver->check_wrong_attach();
+ #endif
+
+ //Clean the clauses before playing with them
+ solver->clauseCleaner->remove_and_clean_all();
+
+ //If too many clauses, don't do it
+ if (solver->getNumLongClauses() > 40ULL*1000ULL*1000ULL*solver->conf.var_and_mem_out_mult
+ || solver->litStats.irredLits > 100ULL*1000ULL*1000ULL*solver->conf.var_and_mem_out_mult
+ ) {
+ if (solver->conf.verbosity) {
+ cout << "c [occ] will not link in occur, CNF has too many clauses/irred lits" << endl;
+ }
+ return false;
+ }
+
+ //Setup
+ clause_lits_added = 0;
+ runStats.clear();
+ runStats.numCalls++;
+ clauses.clear();
+ set_limits(); //to calculate strengthening_time_limit
+ limit_to_decrease = &strengthening_time_limit;
+ if (!fill_occur_and_print_stats()) {
+ return false;
+ }
+
+ set_limits();
+ return solver->okay();
+}
+
+bool OccSimplifier::simplify(const bool _startup, const std::string schedule)
+{
+ #ifdef DEBUG_MARKED_CLAUSE
+ assert(solver->no_marked_clauses());
+ #endif
+
+ startup = _startup;
+ if (!setup()) {
+ return solver->okay();
+ }
+
+ const size_t origBlockedSize = blockedClauses.size();
+ const size_t origTrailSize = solver->trail_size();
+
+
+ indep_vars.clear();
+ if (solver->conf.independent_vars) {
+ indep_vars.resize(solver->nVars(), false);
+ for(uint32_t outside_var: *solver->conf.independent_vars) {
+ uint32_t outer_var = solver->map_to_with_bva(outside_var);
+ outer_var = solver->varReplacer->get_var_replaced_with_outer(outer_var);
+ uint32_t int_var = solver->map_outer_to_inter(outer_var);
+ if (int_var < solver->nVars()) {
+ indep_vars[int_var] = true;
+ }
+ }
+ } else {
+ indep_vars.shrink_to_fit();
+ }
+
+ execute_simplifier_strategy(schedule);
+
+ remove_by_drat_recently_blocked_clauses(origBlockedSize);
+ finishUp(origTrailSize);
+
+ return solver->okay();
+}
+
+bool OccSimplifier::backward_sub_str()
+{
+ limit_to_decrease = &subsumption_time_limit;
+ assert(cl_to_free_later.empty());
+ assert(solver->watches.get_smudged_list().empty());
+
+ if (!sub_str->backw_sub_str_long_with_bins()
+ || solver->must_interrupt_asap()
+ ) {
+ goto end;
+ }
+
+ sub_str->backw_sub_long_with_long();
+ if (solver->must_interrupt_asap())
+ goto end;
+
+ limit_to_decrease = &strengthening_time_limit;
+ if (!sub_str->backw_str_long_with_long()
+ || solver->must_interrupt_asap()
+ ) {
+ goto end;
+ }
+
+ if (!deal_with_added_long_and_bin(true)
+ || solver->must_interrupt_asap()
+ ) {
+ goto end;
+ }
+
+ end:
+ added_long_cl.clear();
+ free_clauses_to_free();
+ solver->clean_occur_from_removed_clauses_only_smudged();
+
+ return solver->okay();
+}
+
+bool OccSimplifier::fill_occur()
+{
+ //Calculate binary clauses' contribution to n_occurs
+ size_t wsLit = 0;
+ for (watch_array::const_iterator
+ it = solver->watches.begin(), end = solver->watches.end()
+ ; it != end
+ ; ++it, wsLit++
+ ) {
+ Lit lit = Lit::toLit(wsLit);
+ watch_subarray_const ws = *it;
+ for (const Watched* it2 = ws.begin(), *end2 = ws.end()
+ ; it2 != end2
+ ; it2++
+ ) {
+ if (it2->isBin() && !it2->red() && lit < it2->lit2()) {
+ n_occurs[lit.toInt()]++;
+ n_occurs[it2->lit2().toInt()]++;
+ }
+ }
+ }
+
+ //Add irredundant to occur
+ uint64_t memUsage = calc_mem_usage_of_occur(solver->longIrredCls);
+ print_mem_usage_of_occur(memUsage);
+ if (memUsage > solver->conf.maxOccurIrredMB*1000ULL*1000ULL*solver->conf.var_and_mem_out_mult) {
+ if (solver->conf.verbosity) {
+ cout << "c [occ] Memory usage of occur is too high, unlinking and skipping occur" << endl;
+ }
+ CompleteDetachReatacher detRet(solver);
+ detRet.reattachLongs(true);
+ return false;
+ }
+
+ link_in_data_irred = link_in_clauses(
+ solver->longIrredCls
+ , true //add to occur list
+ , std::numeric_limits<uint32_t>::max()
+ , std::numeric_limits<int64_t>::max()
+ );
+ solver->longIrredCls.clear();
+ print_linkin_data(link_in_data_irred);
+
+ //Add redundant to occur
+ memUsage = calc_mem_usage_of_occur(solver->longRedCls[0]);
+ print_mem_usage_of_occur(memUsage);
+ bool linkin = true;
+ if (memUsage > solver->conf.maxOccurRedMB*1000ULL*1000ULL*solver->conf.var_and_mem_out_mult) {
+ linkin = false;
+ }
+ //Sort, so we get the shortest ones in at least
+ std::sort(solver->longRedCls[0].begin(), solver->longRedCls[0].end()
+ , ClauseSizeSorter(solver->cl_alloc));
+
+ link_in_data_red = link_in_clauses(
+ solver->longRedCls[0]
+ , linkin
+ , solver->conf.maxRedLinkInSize
+ , solver->conf.maxOccurRedLitLinkedM*1000ULL*1000ULL*solver->conf.var_and_mem_out_mult
+ );
+ solver->longRedCls[0].clear();
+
+ //Don't really link in the rest
+ for(auto& lredcls: solver->longRedCls) {
+ link_in_clauses(lredcls, linkin, 0, 0);
+ }
+ for(auto& lredcls: solver->longRedCls) {
+ lredcls.clear();
+ }
+
+ LinkInData combined(link_in_data_irred);
+ combined.combine(link_in_data_red);
+ print_linkin_data(combined);
+
+ return true;
+}
+
+//This must NEVER be called during solve. Only JUST BEFORE Solver::solve() is called
+//otherwise, uneliminated_vars_since_last_solve will be wrong
+bool OccSimplifier::uneliminate(uint32_t var)
+{
+ #ifdef VERBOSE_DEBUG_RECONSTRUCT
+ cout << "calling uneliminate() on var" << var+1 << endl;
+ #endif
+ assert(solver->decisionLevel() == 0);
+ assert(solver->okay());
+
+ //Check that it was really eliminated
+ //NOTE: it's already been made a decision var, as the variable has been re-added already
+ solver->set_decision_var(var);
+ assert(solver->varData[var].removed == Removed::elimed);
+ assert(solver->value(var) == l_Undef);
+
+ if (!blockedMapBuilt) {
+ cleanBlockedClauses();
+ buildBlockedMap();
+ }
+
+ //Uneliminate it in theory
+ bvestats_global.numVarsElimed--;
+ solver->varData[var].removed = Removed::none;
+ solver->set_decision_var(var);
+
+ //Find if variable is really needed to be eliminated
+ var = solver->map_inter_to_outer(var);
+ uint32_t at_blocked_cls = blk_var_to_cls[var];
+ if (at_blocked_cls == std::numeric_limits<uint32_t>::max())
+ return solver->okay();
+
+ //Eliminate it in practice
+ //NOTE: Need to eliminate in theory first to avoid infinite loops
+
+ //Mark for removal from blocked list
+ blockedClauses[at_blocked_cls].toRemove = true;
+ can_remove_blocked_clauses = true;
+ assert(blockedClauses[at_blocked_cls].at(0, blkcls).var() == var);
+
+ //Re-insert into Solver
+ #ifdef VERBOSE_DEBUG_RECONSTRUCT
+ cout
+ << "Uneliminating cl ";
+ for(size_t i=0; i< blockedClauses[at_blocked_cls].size(); i++){
+ cout << blockedClauses[at_blocked_cls].at(i, blkcls) << " ";
+ }
+ cout << " on var " << var+1
+ << endl;
+ #endif
+
+ vector<Lit> lits;
+ size_t bat = 1;
+ while(bat < blockedClauses[at_blocked_cls].size()) {
+ Lit l = blockedClauses[at_blocked_cls].at(bat, blkcls);
+ if (l == lit_Undef) {
+ solver->addClause(lits);
+ if (!solver->okay()) {
+ return false;
+ }
+ lits.clear();
+ } else {
+ lits.push_back(l);
+ }
+ bat++;
+ }
+
+ return solver->okay();
+}
+
+void OccSimplifier::remove_by_drat_recently_blocked_clauses(size_t origBlockedSize)
+{
+ if (!(*solver->drat).enabled())
+ return;
+
+ if (solver->conf.verbosity >= 6) {
+ cout << "c Deleting blocked clauses for DRAT" << endl;
+ }
+
+ for(size_t i = origBlockedSize; i < blockedClauses.size(); i++) {
+ //If doing stamping or caching, we cannot delete binary redundant
+ //clauses, because they are stored in the stamp/cache and so
+ //will be used -- and DRAT will complain when used
+ vector<Lit> lits;
+ size_t at = 1;
+ while(at < blockedClauses[i].size()) {
+ const Lit l = blockedClauses[i].at(at, blkcls);
+ if (l == lit_Undef) {
+ if (!(lits.size() <= 2 && (solver->conf.doCache|| solver->conf.doStamp))) {
+ (*solver->drat) << del << lits << fin;
+ }
+
+ lits.clear();
+ } else {
+ lits.push_back(l);
+ }
+ at++;
+ }
+ }
+}
+
+void OccSimplifier::buildBlockedMap()
+{
+ blk_var_to_cls.clear();
+ blk_var_to_cls.resize(solver->nVarsOuter(), std::numeric_limits<uint32_t>::max());
+ for(size_t i = 0; i < blockedClauses.size(); i++) {
+ const BlockedClauses& blocked = blockedClauses[i];
+ uint32_t blockedon = blocked.at(0, blkcls).var();
+ assert(blockedon < blk_var_to_cls.size());
+ blk_var_to_cls[blockedon] = i;
+ }
+ blockedMapBuilt = true;
+}
+
+void OccSimplifier::finishUp(
+ size_t origTrailSize
+) {
+ bool somethingSet = (solver->trail_size() - origTrailSize) > 0;
+ runStats.zeroDepthAssings = solver->trail_size() - origTrailSize;
+ const double myTime = cpuTime();
+
+ //Add back clauses to solver
+ if (solver->ok) {
+ solver-> ok = solver->propagate_occur();
+ }
+ remove_all_longs_from_watches();
+ add_back_to_solver();
+ if (solver->ok) {
+ solver->ok = solver->propagate<false>().isNULL();
+ }
+
+ //Update global stats
+ const double time_used = cpuTime() - myTime;
+ runStats.finalCleanupTime += time_used;
+ if (solver->sqlStats) {
+ solver->sqlStats->time_passed_min(
+ solver
+ , "occur cleanup"
+ , time_used
+ );
+ }
+ globalStats += runStats;
+ sub_str->finishedRun();
+
+ //Sanity checks
+ if (solver->ok && somethingSet) {
+ solver->test_all_clause_attached();
+ solver->check_wrong_attach();
+ solver->check_stats();
+ solver->check_implicit_propagated();
+ }
+
+ if (solver->ok) {
+ check_elimed_vars_are_unassignedAndStats();
+ }
+}
+
+void OccSimplifier::sanityCheckElimedVars()
+{
+ //First, sanity-check the long clauses
+ for (vector<ClOffset>::const_iterator
+ it = clauses.begin(), end = clauses.end()
+ ; it != end
+ ; ++it
+ ) {
+ const Clause* cl = solver->cl_alloc.ptr(*it);
+
+ //Already removed
+ if (cl->freed())
+ continue;
+
+ for (const Lit lit: *cl) {
+ if (solver->varData[lit.var()].removed == Removed::elimed) {
+ cout
+ << "Error: elimed var -- Lit " << lit << " in clause"
+ << endl
+ << "wrongly left in clause: " << *cl
+ << endl;
+ std::exit(-1);
+ }
+ }
+ }
+
+ //Then, sanity-check the binary clauses
+ size_t wsLit = 0;
+ for (watch_array::const_iterator
+ it = solver->watches.begin(), end = solver->watches.end()
+ ; it != end
+ ; ++it, wsLit++
+ ) {
+ Lit lit = Lit::toLit(wsLit);
+ watch_subarray_const ws = *it;
+ for (const Watched* it2 = ws.begin(), *end2 = ws.end()
+ ; it2 != end2
+ ; it2++
+ ) {
+ if (it2->isBin()) {
+ if (solver->varData[lit.var()].removed == Removed::elimed
+ || solver->varData[it2->lit2().var()].removed == Removed::elimed
+ ) {
+ cout
+ << "Error: A var is elimed in a binary clause: "
+ << lit << " , " << it2->lit2()
+ << endl;
+ std::exit(-1);
+ }
+ }
+ }
+ }
+}
+
+void OccSimplifier::set_limits()
+{
+ subsumption_time_limit = 450LL*1000LL*solver->conf.subsumption_time_limitM
+ *solver->conf.global_timeout_multiplier;
+ strengthening_time_limit = 200LL*1000LL*solver->conf.strengthening_time_limitM
+ *solver->conf.global_timeout_multiplier;
+ norm_varelim_time_limit = 4ULL*1000LL*1000LL*solver->conf.varelim_time_limitM
+ *solver->conf.global_timeout_multiplier;
+ empty_varelim_time_limit = 200LL*1000LL*solver->conf.empty_varelim_time_limitM
+ *solver->conf.global_timeout_multiplier;
+ varelim_sub_str_limit = 1000ULL*1000ULL*solver->conf.varelim_sub_str_limit
+ *solver->conf.global_timeout_multiplier;
+
+ //If variable elimination isn't going so well
+ if (bvestats_global.testedToElimVars > 0
+ && float_div(bvestats_global.numVarsElimed, bvestats_global.testedToElimVars) < 0.1
+ ) {
+ norm_varelim_time_limit /= 2;
+ }
+
+ #ifdef BIT_MORE_VERBOSITY
+ cout << "c clause_lits_added: " << clause_lits_added << endl;
+ #endif
+
+ norm_varelim_time_limit *= 4;
+ empty_varelim_time_limit *= 4;
+ subsumption_time_limit *= 2;
+ strengthening_time_limit *= 2;
+ varelim_sub_str_limit *= 10;
+
+ varelim_num_limit = ((double)solver->get_num_free_vars() * solver->conf.varElimRatioPerIter);
+
+ if (!solver->conf.do_strengthen_with_occur) {
+ strengthening_time_limit = 0;
+ }
+
+ //For debugging
+// subsumption_time_limit = 0;
+// strengthening_time_limit = 0;
+// norm_varelim_time_limit = 0;
+// empty_varelim_time_limit = 0;
+// varelim_num_limit = 0;
+// subsumption_time_limit = std::numeric_limits<int64_t>::max();
+// strengthening_time_limit = std::numeric_limits<int64_t>::max();
+// norm_varelim_time_limit = std::numeric_limits<int64_t>::max();
+// empty_varelim_time_limit = std::numeric_limits<int64_t>::max();
+// varelim_num_limit = std::numeric_limits<int64_t>::max();
+// varelim_sub_str_limit = std::numeric_limits<int64_t>::max();
+}
+
+void OccSimplifier::cleanBlockedClausesIfDirty()
+{
+ if (can_remove_blocked_clauses) {
+ cleanBlockedClauses();
+ }
+}
+
+void OccSimplifier::cleanBlockedClauses()
+{
+ assert(solver->decisionLevel() == 0);
+ vector<BlockedClauses>::iterator i = blockedClauses.begin();
+ vector<BlockedClauses>::iterator j = blockedClauses.begin();
+
+ uint64_t i_blkcls = 0;
+ uint64_t j_blkcls = 0;
+ for (vector<BlockedClauses>::iterator
+ end = blockedClauses.end()
+ ; i != end
+ ; i++
+ ) {
+ const uint32_t blockedOn = solver->map_outer_to_inter(i->at(0, blkcls).var());
+ if (solver->varData[blockedOn].removed == Removed::elimed
+ && solver->value(blockedOn) != l_Undef
+ ) {
+ std::cerr
+ << "ERROR: var " << Lit(blockedOn, false) << " elimed,"
+ << " value: " << solver->value(blockedOn)
+ << endl;
+ assert(false);
+ std::exit(-1);
+ }
+
+ if (i->toRemove) {
+ blockedMapBuilt = false;
+ i_blkcls += i->size();
+ assert(i_blkcls == i->end);
+ i->start = std::numeric_limits<uint64_t>::max();
+ i->end = std::numeric_limits<uint64_t>::max();
+ } else {
+ assert(solver->varData[blockedOn].removed == Removed::elimed);
+
+ //beware we might change this
+ const size_t sz = i->size();
+
+ //don't copy if we don't need to
+ if (!blockedMapBuilt) {
+ for(size_t x = 0; x < sz; x++) {
+ blkcls[j_blkcls++] = blkcls[i_blkcls++];
+ }
+ } else {
+ i_blkcls += sz;
+ j_blkcls += sz;
+ }
+ assert(i_blkcls == i->end);
+ i->start = j_blkcls-sz;
+ i->end = j_blkcls;
+ *j++ = *i;
+ }
+ }
+ blkcls.resize(j_blkcls);
+ blockedClauses.resize(blockedClauses.size()-(i-j));
+ can_remove_blocked_clauses = false;
+}
+
+void OccSimplifier::rem_cls_from_watch_due_to_varelim(
+ watch_subarray todo
+ , const Lit lit
+) {
+ blockedMapBuilt = false;
+
+ //Copy&clear i.e. MOVE
+ todo.moveTo(tmp_rem_cls_copy);
+ assert(solver->watches[lit].empty());
+
+ vector<Lit>& lits = tmp_rem_lits;
+ for (const Watched watch :tmp_rem_cls_copy) {
+ lits.clear();
+ bool red = false;
+
+ if (watch.isClause()) {
+ const ClOffset offset = watch.get_offset();
+ const Clause& cl = *solver->cl_alloc.ptr(offset);
+ if (cl.getRemoved()) {
+ continue;
+ }
+ assert(!cl.freed());
+
+ //Update stats
+ if (!cl.red()) {
+ bvestats.clauses_elimed_long++;
+ bvestats.clauses_elimed_sumsize += cl.size();
+
+ lits.resize(cl.size());
+ std::copy(cl.begin(), cl.end(), lits.begin());
+ add_clause_to_blck(lits);
+ } else {
+ red = true;
+ bvestats.longRedClRemThroughElim++;
+ }
+
+ //Remove -- only DRAT the ones that are redundant
+ //The irred will be removed thanks to 'blocked' system
+ unlink_clause(offset, cl.red(), true, true);
+ }
+
+ if (watch.isBin()) {
+
+ //Update stats
+ if (!watch.red()) {
+ bvestats.clauses_elimed_bin++;
+ bvestats.clauses_elimed_sumsize += 2;
+ } else {
+ red = true;
+ bvestats.binRedClRemThroughElim++;
+ }
+
+ //Put clause into blocked status
+ lits.resize(2);
+ lits[0] = lit;
+ lits[1] = watch.lit2();
+ if (!watch.red()) {
+ add_clause_to_blck(lits);
+ n_occurs[lits[0].toInt()]--;
+ n_occurs[lits[1].toInt()]--;
+ } else {
+ //If redundant, delayed blocked-based DRAT deletion will not work
+ //so delete explicitly
+
+ //Drat
+ if (!solver->conf.doStamp && !solver->conf.doCache) {
+ (*solver->drat) << del << lits[0] << lits[1] << fin;
+ }
+ }
+
+ //Remove
+ //*limit_to_decrease -= (long)solver->watches[lits[0]].size()/4; //This is zero
+ *limit_to_decrease -= (long)solver->watches[lits[1]].size()/4;
+ solver->detach_bin_clause(lits[0], lits[1], red, true, true);
+ }
+
+ if (solver->conf.verbosity >= 3 && !lits.empty()) {
+ cout
+ << "Eliminated clause " << lits << " (red: " << red << ")"
+ << " on var " << lit.var()+1
+ << endl;
+ }
+ }
+}
+
+void OccSimplifier::add_clause_to_blck(const vector<Lit>& lits)
+{
+ for(const Lit& l: lits) {
+ removed_cl_with_var.touch(l.var());
+ elim_calc_need_update.touch(l.var());
+ }
+
+ vector<Lit> lits_outer = lits;
+ solver->map_inter_to_outer(lits_outer);
+ for(Lit l: lits_outer) {
+ blkcls.push_back(l);
+ }
+ blkcls.push_back(lit_Undef);
+ blockedClauses.back().end = blkcls.size();
+}
+
+void OccSimplifier::find_gate(
+ Lit elim_lit
+ , watch_subarray_const a
+ , watch_subarray_const b
+) {
+ assert(toClear.empty());
+ for(const Watched w: a) {
+ if (w.isBin() && !w.red()) {
+ seen[(~w.lit2()).toInt()] = 1;
+ toClear.push_back(~w.lit2());
+ }
+ }
+
+ //Have to find the corresponding gate. Finding one is good enough
+ for(const Watched w: b) {
+ if (w.isBin()) {
+ continue;
+ }
+
+ if (w.isClause()) {
+ Clause* cl = solver->cl_alloc.ptr(w.get_offset());
+ if (cl->getRemoved()) {
+ continue;
+ }
+
+ assert(cl->size() > 2);
+ if (!cl->red()) {
+ bool OK = true;
+ for(const Lit lit: *cl) {
+ if (lit != ~elim_lit) {
+ if (!seen[lit.toInt()]) {
+ OK = false;
+ break;
+ }
+ }
+ }
+
+ //Found all lits inside
+ if (OK) {
+ cl->stats.marked_clause = true;
+ gate_varelim_clause = cl;
+ break;
+ }
+ }
+ }
+ }
+
+ for(Lit l: toClear) {
+ seen[l.toInt()] = 0;
+ }
+ toClear.clear();
+}
+
+void OccSimplifier::mark_gate_in_poss_negs(
+ Lit elim_lit
+ , watch_subarray_const poss
+ , watch_subarray_const negs
+) {
+ //Either of the two is OK. Let's just find ONE, not the biggest one.
+ //We could find the biggest one, but it's expensive.
+ bool found_pos = false;
+ gate_varelim_clause = NULL;
+ find_gate(elim_lit, poss, negs);
+ if (gate_varelim_clause == NULL) {
+ find_gate(~elim_lit, negs, poss);
+ found_pos = true;
+ }
+
+ if (gate_varelim_clause != NULL && solver->conf.verbosity >= 10) {
+ cout
+ << "Lit: " << elim_lit
+ << " gate_found_elim_pos:" << found_pos
+ << endl;
+ }
+}
+
+int OccSimplifier::test_elim_and_fill_resolvents(const uint32_t var)
+{
+ assert(solver->ok);
+ assert(solver->varData[var].removed == Removed::none);
+ assert(solver->value(var) == l_Undef);
+
+ //Gather data
+ #ifdef CHECK_N_OCCUR
+ if (n_occurs[Lit(var, false).toInt()] != calc_data_for_heuristic(Lit(var, false))) {
+ cout << "lit " << Lit(var, false) << endl;
+ cout << "n_occ is: " << n_occurs[Lit(var, false).toInt()] << endl;
+ cout << "calc is: " << calc_data_for_heuristic(Lit(var, false)) << endl;
+ assert(false);
+ }
+
+ if (n_occurs[Lit(var, true).toInt()] != calc_data_for_heuristic(Lit(var, true))) {
+ cout << "lit " << Lit(var, true) << endl;
+ cout << "n_occ is: " << n_occurs[Lit(var, true).toInt()] << endl;
+ cout << "calc is: " << calc_data_for_heuristic(Lit(var, true)) << endl;
+ }
+ #endif
+ const uint32_t pos = n_occurs[Lit(var, false).toInt()];
+ const uint32_t neg = n_occurs[Lit(var, true).toInt()];
+
+ //Heuristic calculation took too much time
+ if (*limit_to_decrease < 0) {
+ return std::numeric_limits<int>::max();
+ }
+
+ //set-up
+ const Lit lit = Lit(var, false);
+ watch_subarray poss = solver->watches[lit];
+ watch_subarray negs = solver->watches[~lit];
+ std::sort(poss.begin(), poss.end(), watch_sort_smallest_first());
+ std::sort(negs.begin(), negs.end(), watch_sort_smallest_first());
+ resolvents.clear();
+
+ //Pure literal, no resolvents
+ //we look at "pos" and "neg" (and not poss&negs) because we don't care about redundant clauses
+ if (pos == 0 || neg == 0) {
+ return -100;
+ }
+
+ //Too expensive to check, it's futile
+ if ((uint64_t)neg * (uint64_t)pos
+ >= solver->conf.varelim_cutoff_too_many_clauses
+ ) {
+ return std::numeric_limits<int>::max();
+ }
+
+ gate_varelim_clause = NULL;
+ if (solver->conf.skip_some_bve_resolvents) {
+ mark_gate_in_poss_negs(lit, poss, negs);
+ }
+
+ // Count clauses/literals after elimination
+ uint32_t before_clauses = pos + neg;
+ uint32_t after_clauses = 0;
+
+ size_t at_poss = 0;
+ for (const Watched* it = poss.begin(), *end = poss.end()
+ ; it != end
+ ; ++it, at_poss++
+ ) {
+ *limit_to_decrease -= 3;
+ if (solver->redundant_or_removed(*it))
+ continue;
+
+ size_t at_negs = 0;
+ for (const Watched *it2 = negs.begin(), *end2 = negs.end()
+ ; it2 != end2
+ ; it2++, at_negs++
+ ) {
+ *limit_to_decrease -= 3;
+ if (solver->redundant_or_removed(*it2))
+ continue;
+
+ //Resolve the two clauses
+ bool tautological = resolve_clauses(*it, *it2, lit);
+ if (tautological) {
+ continue;
+ }
+
+ if (solver->satisfied_cl(dummy)) {
+ continue;
+ }
+
+ #ifdef VERBOSE_DEBUG_VARELIM
+ cout << "Adding new clause due to varelim: " << dummy << endl;
+ #endif
+
+ after_clauses++;
+ //Early-abort or over time
+ if (after_clauses > (before_clauses + grow)
+ //Too long resolvent
+ || (solver->conf.velim_resolvent_too_large != -1
+ && ((int)dummy.size() > solver->conf.velim_resolvent_too_large))
+ //Over-time
+ || *limit_to_decrease < -10LL*1000LL
+
+ ) {
+ if (gate_varelim_clause) {
+ gate_varelim_clause->stats.marked_clause = false;
+ }
+ return std::numeric_limits<int>::max();
+ }
+
+ //Calculate new clause stats
+ ClauseStats stats;
+ bool is_xor = false;
+ #if defined(USE_GAUSS) || defined(STATS_NEEDED)
+ if (it->isBin() && it2->isClause()) {
+ Clause* c = solver->cl_alloc.ptr(it2->get_offset());
+ stats = c->stats;
+ is_xor |= c->used_in_xor();
+ } else if (it2->isBin() && it->isClause()) {
+ Clause* c = solver->cl_alloc.ptr(it->get_offset());
+ stats = c->stats;
+ is_xor |= c->used_in_xor();
+ } else if (it2->isClause() && it->isClause()) {
+ Clause* c1 = solver->cl_alloc.ptr(it->get_offset());
+ Clause* c2 = solver->cl_alloc.ptr(it2->get_offset());
+ stats = ClauseStats::combineStats(c1->stats, c2->stats);
+ is_xor |= c1->used_in_xor();
+ is_xor |= c2->used_in_xor();
+ }
+ #endif
+ //must clear marking that has been set due to gate
+ stats.marked_clause = 0;
+ resolvents.add_resolvent(dummy, stats, is_xor);
+ }
+ }
+
+ if (gate_varelim_clause) {
+ gate_varelim_clause->stats.marked_clause = false;
+ }
+
+ return -1;
+}
+
+void OccSimplifier::printOccur(const Lit lit) const
+{
+ for(size_t i = 0; i < solver->watches[lit].size(); i++) {
+ const Watched& w = solver->watches[lit][i];
+ if (w.isBin()) {
+ cout
+ << "Bin --> "
+ << lit << ", "
+ << w.lit2()
+ << "(red: " << w.red()
+ << ")"
+ << endl;
+ }
+
+ if (w.isClause()) {
+ const Clause& cl = *solver->cl_alloc.ptr(w.get_offset());
+ if (cl.getRemoved())
+ continue;
+ cout
+ << "Clause--> "
+ << cl
+ << "(red: " << cl.red()
+ << ")"
+ << "(rem: " << cl.getRemoved()
+ << ")"
+ << endl;
+ }
+ }
+}
+
+void OccSimplifier::print_var_eliminate_stat(const Lit lit) const
+{
+ //Eliminate:
+ if (solver->conf.verbosity < 5)
+ return;
+
+ cout
+ << "Eliminating var " << lit
+ << " with occur sizes "
+ << solver->watches[lit].size() << " , "
+ << solver->watches[~lit].size()
+ << endl;
+
+ cout << "POS: " << endl;
+ printOccur(lit);
+ cout << "NEG: " << endl;
+ printOccur(~lit);
+}
+
+bool OccSimplifier::add_varelim_resolvent(
+ vector<Lit>& finalLits
+ , const ClauseStats& stats
+ , const bool is_xor
+) {
+ bvestats.newClauses++;
+ Clause* newCl = NULL;
+
+ if (solver->conf.verbosity >= 5) {
+ cout
+ << "adding v-elim resolvent: "
+ << finalLits
+ << endl;
+ }
+
+ newCl = solver->add_clause_int(
+ finalLits //Literals in new clause
+ , false //Is the new clause redundant?
+ , stats //Statistics for this new clause (usage, etc.)
+ , false //Should clause be attached?
+ , &finalLits //Return final set of literals here
+ );
+
+ if (!solver->ok)
+ return false;
+
+ if (newCl != NULL) {
+ newCl->set_used_in_xor(is_xor);
+ linkInClause(*newCl);
+ ClOffset offset = solver->cl_alloc.get_offset(newCl);
+ clauses.push_back(offset);
+ added_long_cl.push_back(offset);
+ } else if (finalLits.size() == 2) {
+ added_bin_cl.push_back(std::make_pair(finalLits[0], finalLits[1]));
+ n_occurs[finalLits[0].toInt()]++;
+ n_occurs[finalLits[1].toInt()]++;
+ if (!solver->ok) {
+ return false;
+ }
+ }
+
+ //Touch every var of the new clause, so we re-estimate
+ //elimination complexity for this var
+ for(Lit lit: finalLits) {
+ #ifdef CHECK_N_OCCUR
+ if(n_occurs[lit.toInt()] != calc_data_for_heuristic(lit)) {
+ cout << "n_occurs[lit.toInt()]:" << n_occurs[lit.toInt()] << endl;
+ cout << "calc_data_for_heuristic(lit): " << calc_data_for_heuristic(lit) << endl;
+ cout << "cl: " << finalLits << endl;
+ cout << "lit: " << lit << endl;
+ assert(false);
+ }
+ #endif
+ elim_calc_need_update.touch(lit.var());
+ added_cl_to_var.touch(lit.var());
+ }
+
+ return true;
+}
+
+void OccSimplifier::check_n_occur()
+{
+ for (size_t i=0; i < solver->nVars(); i++) {
+ Lit lit(i, false);
+ const uint32_t pos = calc_occ_data(lit);
+ if (pos != n_occurs[lit.toInt()]) {
+ cout << "for lit: " << lit << endl;
+ cout << "pos is: " << pos
+ << " n_occurs is:" << n_occurs[lit.toInt()] << endl;
+ assert(false);
+ }
+
+ const uint32_t neg = calc_occ_data(~lit);
+ if (neg != n_occurs[(~lit).toInt()]) {
+ cout << "for lit: " << lit << endl;
+ cout << "neg is: " << neg
+ << " n_occurs is:" << n_occurs[(~lit).toInt()] << endl;
+ assert(false);
+ }
+ }
+}
+
+void OccSimplifier::update_varelim_complexity_heap()
+{
+ num_otf_update_until_now++;
+ for(uint32_t var: elim_calc_need_update.getTouchedList()) {
+ //No point in updating the score of this var
+ if (!can_eliminate_var(var) || !velim_order.inHeap(var)) {
+ continue;
+ }
+
+ //cout << "updating var " << var+1 << endl;
+ varElimComplexity[var] = heuristicCalcVarElimScore(var);
+ velim_order.update(var);
+ }
+}
+
+void OccSimplifier::print_var_elim_complexity_stats(const uint32_t var) const
+{
+ if (solver->conf.verbosity >= 5) {
+ cout << "var " << var +1 << " trying complexity: " << varElimComplexity[var] << endl;
+ }
+}
+
+void OccSimplifier::set_var_as_eliminated(const uint32_t var, const Lit lit)
+{
+ if (solver->conf.verbosity >= 5) {
+ cout << "Elimination of var "
+ << solver->map_inter_to_outer(lit)
+ << " finished " << endl;
+ }
+ assert(solver->varData[var].removed == Removed::none);
+ solver->varData[var].removed = Removed::elimed;
+
+ bvestats_global.numVarsElimed++;
+}
+
+void OccSimplifier::create_dummy_blocked_clause(const Lit lit)
+{
+ blkcls.push_back(solver->map_inter_to_outer(lit));
+ blockedClauses.push_back(
+ BlockedClauses(blkcls.size()-1, blkcls.size())
+ );
+ blockedMapBuilt = false;
+}
+
+bool OccSimplifier::maybe_eliminate(const uint32_t var)
+{
+ assert(solver->ok);
+ print_var_elim_complexity_stats(var);
+ bvestats.testedToElimVars++;
+ const Lit lit = Lit(var, false);
+
+ //Heuristic says no, or we ran out of time
+ if (test_elim_and_fill_resolvents(var) > 0
+ || *limit_to_decrease < 0
+ ) {
+ return false; //didn't eliminate :(
+ }
+ bvestats.triedToElimVars++;
+
+ print_var_eliminate_stat(lit);
+
+ //Remove clauses
+ create_dummy_blocked_clause(lit);
+ rem_cls_from_watch_due_to_varelim(solver->watches[lit], lit);
+ rem_cls_from_watch_due_to_varelim(solver->watches[~lit], ~lit);
+
+ //Add resolvents
+ while(!resolvents.empty()) {
+ if (!add_varelim_resolvent(resolvents.back_lits(),
+ resolvents.back_stats(), resolvents.back_xor())
+ ) {
+ goto end;
+ }
+ resolvents.pop();
+ }
+ limit_to_decrease = &norm_varelim_time_limit;
+
+end:
+ set_var_as_eliminated(var, lit);
+
+ return true; //eliminated!
+}
+
+void OccSimplifier::add_pos_lits_to_dummy_and_seen(
+ const Watched ps
+ , const Lit posLit
+) {
+ if (ps.isBin()) {
+ *limit_to_decrease -= 1;
+ assert(ps.lit2() != posLit);
+
+ seen[ps.lit2().toInt()] = 1;
+ dummy.push_back(ps.lit2());
+ }
+
+ if (ps.isClause()) {
+ Clause& cl = *solver->cl_alloc.ptr(ps.get_offset());
+ *limit_to_decrease -= (long)cl.size()/2;
+ for (const Lit lit : cl){
+ if (lit != posLit) {
+ seen[lit.toInt()] = 1;
+ dummy.push_back(lit);
+ }
+ }
+ }
+}
+
+bool OccSimplifier::add_neg_lits_to_dummy_and_seen(
+ const Watched qs
+ , const Lit posLit
+) {
+ if (qs.isBin()) {
+ *limit_to_decrease -= 1;
+ assert(qs.lit2() != ~posLit);
+
+ if (seen[(~qs.lit2()).toInt()]) {
+ return true;
+ }
+ if (!seen[qs.lit2().toInt()]) {
+ dummy.push_back(qs.lit2());
+ seen[qs.lit2().toInt()] = 1;
+ }
+ }
+
+ if (qs.isClause()) {
+ Clause& cl = *solver->cl_alloc.ptr(qs.get_offset());
+ *limit_to_decrease -= (long)cl.size()/2;
+ for (const Lit lit: cl) {
+ if (lit == ~posLit)
+ continue;
+
+ if (seen[(~lit).toInt()]) {
+ return true;
+ }
+
+ if (!seen[lit.toInt()]) {
+ dummy.push_back(lit);
+ seen[lit.toInt()] = 1;
+ }
+ }
+ }
+
+ return false;
+}
+
+bool OccSimplifier::resolve_clauses(
+ const Watched ps
+ , const Watched qs
+ , const Lit posLit
+) {
+ //If clause has already been freed, skip
+ Clause *cl1 = NULL;
+ if (ps.isClause()) {
+ cl1 = solver->cl_alloc.ptr(ps.get_offset());
+ if (cl1->freed()) {
+ return true;
+ }
+ }
+
+ Clause *cl2 = NULL;
+ if (qs.isClause()) {
+ cl2 = solver->cl_alloc.ptr(qs.get_offset());
+ if (cl2->freed()) {
+ return true;
+ }
+ }
+ if (gate_varelim_clause
+ && cl1 && cl2
+ && !cl1->stats.marked_clause
+ && !cl2->stats.marked_clause
+ ) {
+ //for G (U) R, we only neede to resolve to
+ // (Gx * R!x) (U) (G!x * Rx)
+ // So Rx * R!x is skipped
+ //
+ // Here: Both are long clauses, so only one could be in G. But neither
+ // are marked, hence neither are in G, so both are in R.
+ // see: http://baldur.iti.kit.edu/sat/files/ex04.pdf
+ return true;
+ }
+
+ dummy.clear();
+ add_pos_lits_to_dummy_and_seen(ps, posLit);
+ bool tautological = add_neg_lits_to_dummy_and_seen(qs, posLit);
+
+ *limit_to_decrease -= (long)dummy.size()/2 + 1;
+ for (const Lit lit: dummy) {
+ seen[lit.toInt()] = 0;
+ }
+
+ return tautological;
+}
+
+uint32_t OccSimplifier::calc_data_for_heuristic(const Lit lit)
+{
+ uint32_t ret = 0;
+ watch_subarray_const ws_list = solver->watches[lit];
+
+ //BUT WATCHES ARE SMUDGED!!
+ //THIS IS WRONG!!
+ /*if (link_in_data_red.cl_linked < 100) {
+ ret = ws_list.size();
+ return ret;
+ }*/
+
+ *limit_to_decrease -= (long)ws_list.size()*3 + 100;
+ for (const Watched ws: ws_list) {
+ //Skip redundant clauses
+ if (solver->redundant(ws))
+ continue;
+
+ switch(ws.getType()) {
+ case watch_binary_t:
+ ret++;
+ break;
+
+ case watch_clause_t: {
+ const Clause* cl = solver->cl_alloc.ptr(ws.get_offset());
+ if (!cl->getRemoved()) {
+ assert(!cl->freed() && "Inside occur, so cannot be freed");
+ ret++;
+ }
+ break;
+ }
+
+ default:
+ assert(false);
+ break;
+ }
+ }
+ return ret;
+}
+
+uint32_t OccSimplifier::calc_occ_data(const Lit lit)
+{
+ uint32_t ret = 0;
+ watch_subarray_const ws_list = solver->watches[lit];
+ for (const Watched ws: ws_list) {
+ //Skip redundant clauses
+ if (solver->redundant(ws))
+ continue;
+
+ switch(ws.getType()) {
+ case watch_binary_t:
+ ret++;
+ break;
+
+ case watch_clause_t: {
+ const Clause* cl = solver->cl_alloc.ptr(ws.get_offset());
+ if (!cl->getRemoved()) {
+ assert(!cl->freed() && "Inside occur, so cannot be freed");
+ ret++;
+ }
+ break;
+ }
+
+ default:
+ assert(false);
+ break;
+ }
+ }
+ return ret;
+}
+
+bool OccSimplifier::check_empty_resolvent(Lit lit)
+{
+ //Take the smaller of the two
+ if (solver->watches[~lit].size() < solver->watches[lit].size())
+ lit = ~lit;
+
+ int num_bits_set = check_empty_resolvent_action(
+ lit
+ , ResolvCount::set
+ , 0
+ );
+
+ int num_resolvents = std::numeric_limits<int>::max();
+
+ //Can only count if the POS was small enough
+ //otherwise 'seen' cannot properly store the data
+ if (num_bits_set < 16) {
+ num_resolvents = check_empty_resolvent_action(
+ ~lit
+ , ResolvCount::count
+ , num_bits_set
+ );
+ }
+
+ //Clear the 'seen' array
+ check_empty_resolvent_action(
+ lit
+ , ResolvCount::unset
+ , 0
+ );
+
+ //Okay, this would be great
+ return (num_resolvents == 0);
+}
+
+
+int OccSimplifier::check_empty_resolvent_action(
+ const Lit lit
+ , const ResolvCount action
+ , const int otherSize
+) {
+ uint16_t at = 1;
+ int count = 0;
+ size_t numCls = 0;
+
+ watch_subarray_const watch_list = solver->watches[lit];
+ *limit_to_decrease -= (long)watch_list.size()*2;
+ for (const Watched& ws: watch_list) {
+ if (numCls >= 16
+ && (action == ResolvCount::set
+ || action == ResolvCount::unset)
+ ) {
+ break;
+ }
+
+ if (count > 0
+ && action == ResolvCount::count
+ ) {
+ break;
+ }
+
+ //Handle binary
+ if (ws.isBin()){
+ //Only count irred
+ if (!ws.red()) {
+ *limit_to_decrease -= 4;
+ switch(action) {
+ case ResolvCount::set:
+ seen[ws.lit2().toInt()] |= at;
+ break;
+
+ case ResolvCount::unset:
+ seen[ws.lit2().toInt()] = 0;
+ break;
+
+ case ResolvCount::count:
+ int num = my_popcnt(seen[(~ws.lit2()).toInt()]);
+ assert(num <= otherSize);
+ count += otherSize - num;
+ break;
+ }
+ at <<= 1;
+ numCls++;
+ }
+ continue;
+ }
+
+ if (ws.isClause()) {
+ const Clause* cl = solver->cl_alloc.ptr(ws.get_offset());
+ if (cl->getRemoved()) {
+ continue;
+ }
+
+ //If in occur then it cannot be freed
+ assert(!cl->freed());
+
+ //Only irred is of relevance
+ if (!cl->red()) {
+ *limit_to_decrease -= (long)cl->size()*2;
+ uint16_t tmp = 0;
+ for(const Lit l: *cl) {
+
+ //Ignore orig
+ if (l == lit)
+ continue;
+
+ switch (action) {
+ case ResolvCount::set:
+ seen[l.toInt()] |= at;
+ break;
+
+ case ResolvCount::unset:
+ seen[l.toInt()] = 0;
+ break;
+
+ case ResolvCount::count:
+ tmp |= seen[(~l).toInt()];
+ break;
+ }
+ }
+ at <<= 1;
+ numCls++;
+
+ //Count using tmp
+ if (action == ResolvCount::count) {
+ int num = my_popcnt(tmp);
+ assert(num <= otherSize);
+ count += otherSize - num;
+ }
+ }
+
+ continue;
+ }
+
+ //Only these types are possible
+ assert(false);
+ }
+
+ switch(action) {
+ case ResolvCount::count:
+ return count;
+
+ case ResolvCount::set:
+ return numCls;
+
+ case ResolvCount::unset:
+ return 0;
+ }
+
+ assert(false);
+ return std::numeric_limits<int>::max();
+}
+
+uint64_t OccSimplifier::heuristicCalcVarElimScore(const uint32_t var)
+{
+ const Lit lit(var, false);
+ #ifdef CHECK_N_OCCUR
+ const uint32_t pos = calc_data_for_heuristic(lit);
+ if (pos != n_occurs[lit.toInt()]) {
+ cout << "for lit: " << lit << endl;
+ cout << "pos is: " << pos
+ << " n_occurs is:" << n_occurs[lit.toInt()] << endl;
+ assert(false);
+ }
+
+ const uint32_t neg = calc_data_for_heuristic(~lit);
+ if (neg != n_occurs[(~lit).toInt()]) {
+ cout << "for lit: " << lit << endl;
+ cout << "neg is: " << neg
+ << " n_occurs is:" << n_occurs[(~lit).toInt()] << endl;
+ assert(false);
+ }
+ #endif
+
+ return (uint64_t)n_occurs[lit.toInt()] * (uint64_t)n_occurs[(~lit).toInt()];
+}
+
+void OccSimplifier::order_vars_for_elim()
+{
+ velim_order.clear();
+ varElimComplexity.clear();
+ varElimComplexity.resize(solver->nVars(), 0);
+ elim_calc_need_update.clear();
+
+ //Go through all vars
+ for (
+ size_t var = 0
+ ; var < solver->nVars() && *limit_to_decrease > 0
+ ; var++
+ ) {
+ if (!can_eliminate_var(var))
+ continue;
+
+ *limit_to_decrease -= 50;
+ assert(!velim_order.inHeap(var));
+ varElimComplexity[var] = heuristicCalcVarElimScore(var);
+ velim_order.insert(var);
+ }
+ assert(velim_order.heap_property());
+
+ //Print sorted listed list
+ #ifdef VERBOSE_DEBUG_VARELIM
+ /*cout << "-----------" << endl;
+ for(size_t i = 0; i < velim_order.size(); i++) {
+ cout
+ << "velim_order[" << i << "]: "
+ << " var: " << velim_order[i]+1
+ << " val: " << varElimComplexity[velim_order[i]].first
+ << " , " << varElimComplexity[velim_order[i]].second
+ << endl;
+ }*/
+ #endif
+}
+
+void OccSimplifier::check_elimed_vars_are_unassigned() const
+{
+ for (size_t i = 0; i < solver->nVarsOuter(); i++) {
+ if (solver->varData[i].removed == Removed::elimed) {
+ assert(solver->value(i) == l_Undef);
+ }
+ }
+}
+
+void OccSimplifier::check_elimed_vars_are_unassignedAndStats() const
+{
+ assert(solver->ok);
+ int64_t checkNumElimed = 0;
+ for (size_t i = 0; i < solver->nVarsOuter(); i++) {
+ if (solver->varData[i].removed == Removed::elimed) {
+ checkNumElimed++;
+ assert(solver->value(i) == l_Undef);
+ }
+ }
+ if (bvestats_global.numVarsElimed != checkNumElimed) {
+ std::cerr
+ << "ERROR: globalStats.numVarsElimed is "<<
+ bvestats_global.numVarsElimed
+ << " but checkNumElimed is: " << checkNumElimed
+ << endl;
+
+ assert(false);
+ }
+}
+
+size_t OccSimplifier::mem_used() const
+{
+ size_t b = 0;
+ b += dummy.capacity()*sizeof(char);
+ b += added_long_cl.capacity()*sizeof(ClOffset);
+ b += sub_str->mem_used();
+ b += blockedClauses.capacity()*sizeof(BlockedClauses);
+ b += blkcls.capacity()*sizeof(Lit);
+ b += blk_var_to_cls.size()*sizeof(uint32_t);
+ b += velim_order.mem_used();
+ b += varElimComplexity.capacity()*sizeof(int)*2;
+ b += elim_calc_need_update.mem_used();
+ b += clauses.capacity()*sizeof(ClOffset);
+ b += indep_vars.capacity();
+
+ return b;
+}
+
+size_t OccSimplifier::mem_used_xor() const
+{
+ if (topLevelGauss)
+ return topLevelGauss->mem_used();
+ else
+ return 0;
+}
+
+size_t OccSimplifier::mem_used_bva() const
+{
+ if (bva)
+ return bva->mem_used();
+ else
+ return 0;
+}
+
+
+void OccSimplifier::freeXorMem()
+{
+ delete topLevelGauss;
+ topLevelGauss = NULL;
+}
+
+void OccSimplifier::linkInClause(Clause& cl)
+{
+ assert(cl.size() > 2);
+ ClOffset offset = solver->cl_alloc.get_offset(&cl);
+ cl.recalc_abst_if_needed();
+ if (!cl.red()) {
+ for(const Lit l: cl){
+ n_occurs[l.toInt()]++;
+ added_cl_to_var.touch(l.var());
+ }
+ }
+ assert(cl.stats.marked_clause == 0 && "marks must always be zero at linkin");
+
+ std::sort(cl.begin(), cl.end());
+ for (const Lit lit: cl) {
+ watch_subarray ws = solver->watches[lit];
+ ws.push(Watched(offset, cl.abst));
+ }
+ cl.setOccurLinked(true);
+}
+
+
+/*void OccSimplifier::print_gatefinder_stats() const
+{
+ if (gateFinder) {
+ gateFinder->get_stats().print(solver->nVarsOuter());
+ }
+}*/
+
+double OccSimplifier::Stats::total_time() const
+{
+ return linkInTime + blockTime
+ + varElimTime + finalCleanupTime;
+}
+
+void OccSimplifier::Stats::clear()
+{
+ Stats stats;
+ *this = stats;
+}
+
+OccSimplifier::Stats& OccSimplifier::Stats::operator+=(const Stats& other)
+{
+ numCalls += other.numCalls;
+
+ //Time
+ linkInTime += other.linkInTime;
+ blockTime += other.blockTime;
+ varElimTime += other.varElimTime;
+ finalCleanupTime += other.finalCleanupTime;
+ zeroDepthAssings += other.zeroDepthAssings;
+
+ return *this;
+}
+
+BVEStats& BVEStats::operator+=(const BVEStats& other)
+{
+ numVarsElimed += other.numVarsElimed;
+ varElimTimeOut += other.varElimTimeOut;
+ clauses_elimed_long += other.clauses_elimed_long;
+ clauses_elimed_tri += other.clauses_elimed_tri;
+ clauses_elimed_bin += other.clauses_elimed_bin;
+ clauses_elimed_sumsize += other.clauses_elimed_sumsize;
+ longRedClRemThroughElim += other.longRedClRemThroughElim;
+ binRedClRemThroughElim += other.binRedClRemThroughElim;
+ numRedBinVarRemAdded += other.numRedBinVarRemAdded;
+ testedToElimVars += other.testedToElimVars;
+ triedToElimVars += other.triedToElimVars;
+ newClauses += other.newClauses;
+ subsumedByVE += other.subsumedByVE;
+
+ return *this;
+}
+
+void OccSimplifier::Stats::print_short() const
+{
+
+ cout
+ << "c [occur] " << linkInTime+finalCleanupTime << " is overhead"
+ << endl;
+
+ cout
+ << "c [occur] link-in T: " << linkInTime
+ << " cleanup T: " << finalCleanupTime
+ << endl;
+}
+
+void OccSimplifier::Stats::print(const size_t nVars) const
+{
+ cout << "c -------- OccSimplifier STATS ----------" << endl;
+ print_stats_line("c time"
+ , total_time()
+ , stats_line_percent(varElimTime, total_time())
+ , "% var-elim"
+ );
+
+ print_stats_line("c called"
+ , numCalls
+ , float_div(total_time(), numCalls)
+ , "s per call"
+ );
+
+
+
+
+ print_stats_line("c 0-depth assigns"
+ , zeroDepthAssings
+ , stats_line_percent(zeroDepthAssings, nVars)
+ , "% vars"
+ );
+
+ cout << "c -------- OccSimplifier STATS END ----------" << endl;
+}
+
+void OccSimplifier::save_state(SimpleOutFile& f)
+{
+ assert(solver->decisionLevel() == 0);
+ cleanBlockedClauses();
+ f.put_uint64_t(blockedClauses.size());
+ for(const BlockedClauses& c: blockedClauses) {
+ c.save_to_file(f);
+ }
+ f.put_vector(blkcls);
+ f.put_struct(globalStats);
+ f.put_uint32_t(anythingHasBeenBlocked);
+
+
+}
+void OccSimplifier::load_state(SimpleInFile& f)
+{
+ const uint64_t sz = f.get_uint64_t();
+ for(uint64_t i = 0; i < sz; i++) {
+ BlockedClauses b;
+ b.load_from_file(f);
+ blockedClauses.push_back(b);
+ }
+ f.get_vector(blkcls);
+ f.get_struct(globalStats);
+ anythingHasBeenBlocked = f.get_uint32_t();
+
+ blockedMapBuilt = false;
+ buildBlockedMap();
+
+ //Sanity check
+ for(size_t i = 0; i < solver->nVars(); i++) {
+ if (solver->varData[i].removed == Removed::elimed) {
+ assert(solver->value(i) == l_Undef);
+ }
+ }
+}
+
+void OccSimplifier::check_clid_correct() const
+{
+ #ifdef STATS_NEEDED
+ for(auto offs: clauses) {
+ Clause * cl = solver->cl_alloc.ptr(offs);
+ if (!cl->freed() && !cl->getRemoved()) {
+ assert(!(cl->stats.ID == 0 && cl->red()));
+ }
+ }
+ #endif
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback