From: trevor_hansen Date: Sat, 22 Oct 2011 12:12:28 +0000 (+0000) Subject: Improvement. The default array solver is now built into the SAT solver so SAT solving... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ffae411c13c5a062151c3b838ec19cc10a289683;p=francis%2Fstp.git Improvement. The default array solver is now built into the SAT solver so SAT solving doesn't need to start/stop to do refinement. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1407 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 1fc735d..de7950c 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -15,6 +15,8 @@ #include "../sat/SimplifyingMinisat.h" #include "../sat/MinisatCore.h" #include "../sat/CryptoMinisat.h" +#include "../sat/MinisatCore_prop.h" +#include "../sat/core_prop/Solver_prop.h" #include "../simplifier/RemoveUnconstrained.h" #include "../simplifier/FindPureLiterals.h" #include "../simplifier/EstablishIntervals.h" @@ -55,8 +57,10 @@ namespace BEEV { newS = new SimplifyingMinisat(); else if (bm->UserFlags.solver_to_use == UserDefinedFlags::CRYPTOMINISAT_SOLVER) newS = new CryptoMinisat(); - else + else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER) newS = new MinisatCore(); + else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) + newS = new MinisatCore_prop(); @@ -487,9 +491,7 @@ namespace BEEV { assert(arrayops); // should only go to abstraction refinement if there are array ops. assert(bm->UserFlags.arrayread_refinement_flag); // Refinement must be enabled too. - - // Unfortunately how I implemented the incremental CNF generator in ABC means that - // cryptominisat and simplifying minisat may simplify away variables that we later need. + assert (bm->UserFlags.solver_to_use != UserDefinedFlags::MINISAT_PROPAGATORS); // The array solver shouldn't have returned undecided.. res = Ctr_Example->SATBased_ArrayReadRefinement(NewSolver, simplified_solved_InputToSAT, orig_input, satBase); if (SOLVER_UNDECIDED != res) diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index e01533e..a3faf09 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -127,7 +127,8 @@ namespace BEEV { MINISAT_SOLVER =0, SIMPLIFYING_MINISAT_SOLVER, - CRYPTOMINISAT_SOLVER + CRYPTOMINISAT_SOLVER, + MINISAT_PROPAGATORS }; enum SATSolvers solver_to_use; @@ -249,7 +250,7 @@ namespace BEEV tseitin_are_decision_variables_flag=true; // use minisat by default. - solver_to_use = MINISAT_SOLVER; + solver_to_use = MINISAT_PROPAGATORS; // The special Cryptominisat2 CNF generation with this flag enabled seems to go into an infinite loop. // beware of turning this on if you are using cryptominsat2. diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 8d5476b..f633774 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -912,6 +912,8 @@ namespace BEEV PrintCounterExample(true); } + assert (bm->UserFlags.solver_to_use != UserDefinedFlags::MINISAT_PROPAGATORS); // The array solver shouldn't have returned undecided.. + return SOLVER_UNDECIDED; } } diff --git a/src/main/main.cpp b/src/main/main.cpp index 72d5288..ab94c36 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -78,7 +78,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; * step 5. Call SAT to determine if input is SAT or UNSAT ********************************************************************/ -typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS} OptionType; +typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT} OptionType; int main(int argc, char ** argv) { char * infile = NULL; @@ -149,6 +149,8 @@ int main(int argc, char ** argv) { helpstring += "--minisat : use minisat 2.2 as the solver\n"; helpstring += + "--oldstyle-refinement : Do abstraction-refinement outside the SAT solver.\n"; + helpstring += "--output-CNF : save the CNF into output_[0..n].cnf\n"; helpstring += "--output-bench : save in ABC's bench format to output.bench\n"; @@ -165,7 +167,7 @@ int main(int argc, char ** argv) { helpstring += "--print-back-dot : print dotty/neato's graph format, then exit\n"; helpstring += - "-r : switch refinement off (optimizations are ON by default)\n"; + "-r : turn of abstraction-refinement of arrays.\n"; helpstring += "-s : print function statistics\n"; helpstring += @@ -210,7 +212,7 @@ int main(int argc, char ** argv) { lookup.insert(make_pair(tolower("--SMTLIB1"),SMT_LIB1_FORMAT)); lookup.insert(make_pair(tolower("--disable-cbitp"),DISABLE_CBITP)); lookup.insert(make_pair(tolower("--disable-simplify"),DISABLE_SIMPLIFICATIONS)); - + lookup.insert(make_pair(tolower("--oldstyle-refinement"),OLDSTYLE_REFINEMENT)); if (!strncmp(argv[i],"--config_",strlen("--config_"))) { @@ -295,6 +297,9 @@ int main(int argc, char ** argv) { case USE_MINISAT_SOLVER: bm->UserFlags.solver_to_use = UserDefinedFlags::MINISAT_SOLVER; break; + case OLDSTYLE_REFINEMENT: + bm->UserFlags.solver_to_use = UserDefinedFlags::MINISAT_SOLVER; + break; case DISABLE_SIMPLIFICATIONS: bm->UserFlags.optimize_flag = false; bm->UserFlags.bitConstantProp_flag = false; diff --git a/src/sat/Makefile b/src/sat/Makefile index 4a4f3f2..57bb88b 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -13,11 +13,13 @@ export COPTIMIZE=$(CFLAGS_M32) $(CFLAGS_FPIC) -O3 core: $(LIB) # $(LIB) depends on */lib_release.a and will be rebuilt only if they have been updated -$(LIB): core/lib_release.a simp/lib_release.a utils/lib_release.a cryptominisat2/libminisat.a $(OBJS) +$(LIB): core/lib_release.a core_prop/lib_release.a simp/lib_release.a utils/lib_release.a cryptominisat2/libminisat.a $(OBJS) $(RM) $@ $(call arcat,$@,$(filter %.a,$^)) $(AR) qcs $@ $(filter %.o,$^) +core_prop/lib_release.a: FORCE + $(MAKE) -C core_prop libr core/lib_release.a: FORCE $(MAKE) -C core libr simp/lib_release.a: FORCE @@ -32,6 +34,7 @@ FORCE: clean: $(RM) *.o *~ *.a .#* $(MAKE) -C core clean + $(MAKE) -C core_prop clean $(MAKE) -C simp clean $(MAKE) -C utils clean $(MAKE) -C cryptominisat2 clean diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp index b85fd1b..9733bdf 100644 --- a/src/sat/MinisatCore.cpp +++ b/src/sat/MinisatCore.cpp @@ -18,10 +18,9 @@ namespace BEEV delete s; } - template bool - MinisatCore::addClause(const vec_literals& ps) // Add a clause to the solver. + MinisatCore::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver. { s->addClause(ps); } diff --git a/src/sat/MinisatCore_prop.cpp b/src/sat/MinisatCore_prop.cpp new file mode 100644 index 0000000..1a01b7f --- /dev/null +++ b/src/sat/MinisatCore_prop.cpp @@ -0,0 +1,93 @@ +#include "core_prop/Solver_prop.h" +#include "MinisatCore_prop.h" +#include "utils/System.h" + +namespace BEEV +{ + + template + MinisatCore_prop::MinisatCore_prop() + { + s = new T(); + }; + + template + MinisatCore_prop::~MinisatCore_prop() + { + delete s; + } + + template + bool + MinisatCore_prop::addArray(int array_id, const SATSolver::vec_literals& i, const SATSolver::vec_literals& v, const Minisat::vec & ki, const Minisat::vec & kv ) + { + s->addArray(array_id, i,v, ki,kv); + return true; + } + + + template + bool + MinisatCore_prop::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver. + { + s->addClause(ps); + } + + template + bool + MinisatCore_prop::okay() const // FALSE means solver is in a conflicting state + { + return s->okay(); + } + + template + bool + MinisatCore_prop::solve() // Search without assumptions. + { + if (!s->simplify()) + return false; + + return s->solve(); + + } + + template + uint8_t + MinisatCore_prop::modelValue(Var x) const + { + return Minisat::toInt(s->modelValue(x)); + } + + template + Minisat::Var + MinisatCore_prop::newVar() + { + return s->newVar(); + } + + template + int MinisatCore_prop::setVerbosity(int v) + { + s->verbosity = v; + } + + template + int MinisatCore_prop::nVars() + {return s->nVars();} + + template + void MinisatCore_prop::printStats() + { + double cpu_time = Minisat::cpuTime(); + double mem_used = Minisat::memUsedPeak(); + printf("restarts : %"PRIu64"\n", s->starts); + printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s->conflicts , s->conflicts /cpu_time); + printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", s->decisions, (float)s->rnd_decisions*100 / (float)s->decisions, s->decisions /cpu_time); + printf("propagations : %-12"PRIu64" (%.0f /sec)\n", s->propagations, s->propagations/cpu_time); + printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s->tot_literals, (s->max_literals - s->tot_literals)*100 / (double)s->max_literals); + if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); + printf("CPU time : %g s\n", cpu_time); + } + + template class MinisatCore_prop; +}; diff --git a/src/sat/MinisatCore_prop.h b/src/sat/MinisatCore_prop.h new file mode 100644 index 0000000..9145bb3 --- /dev/null +++ b/src/sat/MinisatCore_prop.h @@ -0,0 +1,61 @@ +/* + * Wraps around CORE minisat. + */ +#ifndef MINISATCORE_H_ +#define MINIASTCORE_H_ + +#include "SATSolver.h" + +namespace Minisat +{ + class MinisatCore_prop; +} + +namespace BEEV +{ + template + class MinisatCore_prop: public SATSolver + { + T * s; + + public: + MinisatCore_prop(); + + ~MinisatCore_prop(); + + bool + addClause(const vec_literals& ps); // Add a clause to the solver. + + bool + okay() const; // FALSE means solver is in a conflicting state + + virtual + bool addArray(int array_id, const SATSolver::vec_literals& i, const SATSolver::vec_literals& v, const Minisat::vec&, const Minisat::vec &); + + + bool + solve(); // Search without assumptions. + + bool + simplify(); // Removes already satisfied clauses. + + virtual uint8_t modelValue(Var x) const; + + virtual Var newVar(); + + int setVerbosity(int v); + + int nVars(); + + void printStats(); + + virtual lbool true_literal() {return ((uint8_t)0);} + virtual lbool false_literal() {return ((uint8_t)1);} + virtual lbool undef_literal() {return ((uint8_t)2);} + + + }; +} +; + +#endif diff --git a/src/sat/SATSolver.h b/src/sat/SATSolver.h index ea3aba5..38839df 100644 --- a/src/sat/SATSolver.h +++ b/src/sat/SATSolver.h @@ -3,6 +3,7 @@ #include "mtl/Vec.h" #include "core/SolverTypes.h" +#include // Don't let the defines escape outside. @@ -25,7 +26,15 @@ namespace BEEV {}; virtual bool - addClause(const vec_literals& ps)=0; // Add a clause to the solver. + addClause(const SATSolver::vec_literals& ps)=0; // Add a clause to the solver. + + virtual + bool addArray(int array_id, const SATSolver::vec_literals& i, const SATSolver::vec_literals& v, const Minisat::vec&, const Minisat::vec& ) + { + std::cerr << "Not implemented"; + exit(1); + } + virtual bool okay() const=0; // FALSE means solver is in a conflicting state diff --git a/src/sat/core_prop/Makefile b/src/sat/core_prop/Makefile new file mode 100644 index 0000000..e4ce3dd --- /dev/null +++ b/src/sat/core_prop/Makefile @@ -0,0 +1,5 @@ +EXEC = minisat +DEPDIR = mtl utils +MROOT=.. + +include $(MROOT)/mtl/template.mk diff --git a/src/sat/core_prop/Solver_prop.cc b/src/sat/core_prop/Solver_prop.cc new file mode 100644 index 0000000..acae00e --- /dev/null +++ b/src/sat/core_prop/Solver_prop.cc @@ -0,0 +1,1849 @@ +/***************************************************************************************[Solver_prop.cc] +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +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. +**************************************************************************************************/ + +/* + * + * This is a modified version of minisat 2.2 that has a propagator for function congruence built into the + * normal propatate()/search() loop. + */ + + + +#include +#include + +#include "../mtl/Sort.h" +#include "../core_prop/Solver_prop.h" + +using namespace Minisat; + +//================================================================================================= +// Options: + + +static const char* _cat = "CORE"; + +static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); +static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false)); +static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true)); +static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false)); +static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2)); +static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); +static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false); +static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true); +static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX)); +static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false)); +static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); + + +//================================================================================================= +// Constructor/Destructor: + +Solver_prop::Solver_prop() : + + // Parameters (user settable): + // + aa_id(0) + , last_id(-1) + , number_of_arrays(0) + , array_trail(0) + , watched_indexes(0) + , top_level_var(0) + , alternate_trail_sorted_to(0) + , val_to_aa(NULL) + , verbosity (0) + , var_decay (opt_var_decay) + , clause_decay (opt_clause_decay) + , random_var_freq (opt_random_var_freq) + , random_seed (opt_random_seed) + , luby_restart (opt_luby_restart) + , ccmin_mode (opt_ccmin_mode) + , phase_saving (opt_phase_saving) + , rnd_pol (false) + , rnd_init_act (opt_rnd_init_act) + , garbage_frac (opt_garbage_frac) + , restart_first (opt_restart_first) + , restart_inc (opt_restart_inc) + + // Parameters (the rest): + // + , learntsize_factor((double)1/(double)3), learntsize_inc(1.1) + + // Parameters (experimental): + // + , learntsize_adjust_start_confl (100) + , learntsize_adjust_inc (1.5) + + // Statistics: (formerly in 'SolverStats') + // + , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) + , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) + + , ok (true) + , cla_inc (1) + , var_inc (1) + , watches (WatcherDeleted(ca)) + , qhead (0) + , simpDB_assigns (-1) + , simpDB_props (0) + , order_heap (VarOrderLt(activity)) + , progress_estimate (0) + , remove_satisfied (true) + + // Resource constraints: + // + , conflict_budget (-1) + , propagation_budget (-1) + , asynch_interrupt (false) +{} + + +Solver_prop::~Solver_prop() +{ + delete[] val_to_aa; + for (int i=0; i < (int)arrayData.size(); i++) + { + delete arrayData[i]; + } +} +//================================================================================================= +// Methods for the array propagator: + +const bool debug_print = false; + +bool +sortByLevel(const Minisat::Solver_prop::Assignment& a, + const Minisat::Solver_prop::Assignment& b) +{ + return a.decisionLevel < b.decisionLevel; +} + + +// Literals that are l_Undef come first, then the rest are sorted by decreasing decision level. +void +Solver_prop::sortVecByLevel(vec & c) +{ + LessThan_Level l(this); + sort(c, l); +} + +// Inplace sort of the alternate trail. +void +Solver_prop::sortAlternateTrail() +{ + int length = alternate_trail.size(); + assert(alternate_trail_sorted_to <= length); + + if (alternate_trail_sorted_to == length) + return; + + std::sort(alternate_trail.begin()+alternate_trail_sorted_to, alternate_trail.end(), sortByLevel); + std::inplace_merge(alternate_trail.begin(), alternate_trail.begin()+alternate_trail_sorted_to, alternate_trail.end(), sortByLevel); + + alternate_trail_sorted_to = length; +} + + +// array_id must grow monotonically. +// returns false if it's already a conflict. +bool +Solver_prop::addArray(int array_id, const vec& i, const vec& v, const vec& ki, const vec& kv) +{ + assert((i.size() > 0) ^ (ki.size() > 0)); + assert((v.size() > 0) ^ (kv.size() > 0)); + + if (!ok) return false; + + bool startOfNewArray = false; + if (array_id != last_id) + { + assert(array_id > last_id); + number_of_arrays++; + + // Map doesn't have a copy constructor, so we create one on the heap. + // Some constant indexes will already have been copied into the val_to_aa map. + Map >* t = new Map > [number_of_arrays]; + + for (int j=0; j < number_of_arrays-1 ; j++) + val_to_aa[j].moveTo(t[j]); + + delete[] val_to_aa; + val_to_aa = t; + last_id = array_id; + startOfNewArray = true; + } + + assert(number_of_arrays > 0); + + ArrayAccess * iv = new ArrayAccess(aa_id++,i,v,ki,kv, number_of_arrays-1); + assert (!iv->known_index); // Not already added. + + if (!startOfNewArray) + { + assert(arrayData.last()->indexSize() == iv->indexSize()); + assert(arrayData.last()->valueSize() == iv->valueSize()); + } + arrayData.push(iv); + + // Adds it into the map if the index is known. + if (iv->isIndexConstant()) + { + CRef r = writeOutArrayAxiom(*iv); + if (r != CRef_Undef) + { + ok = false; + return ok; + } + assert (iv->known_index); // No added. + } + else + { + int & ii = iv->index_index ; + for (ii=0; ii < iv->indexSize(); ii++) + { + if (value(iv->index[ii]) == l_Undef) + { + break; + } + } + if (ii < iv->indexSize()) + startWatchOfIndexVariable(iv); + else + { + // The index has been determined by unit propagation already. + // We can't add it to the watchlist yet though, because when + // we add it. It creates new variables. These variables might + // conflict with clauses that have yet to be added. So we + // need to save this and add it during solve(). + iv->index_index = 0; + toAddAtStartup.push(iv); + } + assert (!iv->known_index); // No added. + } + return true; +} + +// Assumes the index of the access has at least one unset variable. +void Solver_prop::startWatchOfIndexVariable(ArrayAccess* iv) +{ + assert(!iv->isIndexConstant()); + assert(!iv->known_index); + assert(!IndexIsSet(*iv)); + const int indexSize = iv->indexSize(); + + if (value(iv->index[iv->index_index]) != l_Undef) + { + // Loop around checking for the next unset index. + + int j; + for (j = iv->index_index+1; j < indexSize; j++) + if (value(iv->index[j]) == l_Undef) + break; + + if (j == indexSize) + for (j = 0; j < indexSize; j++) + if (value(iv->index[j]) == l_Undef) + break; + + assert(j < indexSize); + iv->index_index = j; + } + + Var v = var(iv->index[iv->index_index]); + assert (value(iv->index[iv->index_index]) == l_Undef); + + array_of_interest[v] = 1; + if (!watchedLiterals.has(v)) + watchedLiterals.insert(v, std::vector()); + + watchedLiterals[v].push_back(iv); + watched_indexes++; +} + + +// Reads out the array index as an integer. It is completely specified. +uint64_t +Solver_prop::index_as_int(const ArrayAccess& iv) +{ + if (iv.isIndexConstant()) + return iv.constantIndex(); + + uint64_t t = 0; + assert(64 >= iv.indexSize()); + + for (int i = 0; i < iv.indexSize(); i++) + { + lbool v = accessIndex(iv, i); + assert(v == l_True || v == l_False); + if (v == l_True) + t += (1 << i); + } + + return t; +} + +// What is the value of iv->index[i]? +lbool +Solver_prop::accessIndex(const ArrayAccess& iv, int i) +{ + assert(i < iv.indexSize()); + assert(i >=0); + if (iv.isIndexConstant()) + return iv.constant_index[i]; + return value(iv.index[i]); +} + +lbool +Solver_prop::accessValue(const ArrayAccess& iv, int i) +{ + assert(i < iv.valueSize()); + assert(i >=0); + if (iv.isValueConstant()) + return iv.constant_value[i]; + return value(iv.value[i]); +} + + +void Solver_prop::assertIndexesEqual(ArrayAccess &a, ArrayAccess &b) +{ + assert(a.indexSize() == b.indexSize()); + assert(a.array_id == b.array_id); + for (int i=0; i < a.indexSize();i++) + { + assert(accessIndex(a,i) == accessIndex(b,i)); + } +} + +const bool debug_equals_lit=false; + +CRef +Solver_prop::addExtraClause(vec& c) +{ + sortVecByLevel(c); + CRef f = ca.alloc(c, false); + clauses.push(f); + attachClause(f); + + return f; +} + + +// Given two array accesses, builds up an equals formula for use on the lhs of an array axiom instance. +CRef Solver_prop::getEqualsLit( ArrayAccess &a, ArrayAccess &b, Lit & result, bool& alreadyCreated) +{ + assert(&a != &b); + assert(a.id != b.id); // Can't compare the same accesses. + assert(a.array_id == b.array_id); + assertIndexesEqual(a, b); + assert(IndexIsSet(a)); + + const int indexSize = a.indexSize(); + + alreadyCreated = false; + + { + ArrayAccess& lookup = (a.id < b.id) ? a : b; + ArrayAccess& other = (a.id < b.id) ? b : a; + EqualityVariables evss(lookup.id, other.id); + + // Lookup the already created equality variables. Maybe we've created it already. + if (equality_variables.peek(evss,result)) + { + alreadyCreated = true; + assert(value(result) == l_True); + return CRef_Undef; + } + + // Create the result variable. Store so we can reuse later. + result = mkLit(newVar(false,true),false); + equality_variables.insert(evss, result); + } + + if (a.isIndexConstant() && b.isIndexConstant()) + { + // We know already they are equal. + assert(decisionLevel() == 0); + uncheckedEnqueue(result); + return propagate(); + } + + vec clause; + clause.capacity(indexSize+1); + clause.push(result); + + if (a.isIndexConstant() || b.isIndexConstant()) + { + ArrayAccess & constantIndex = a.isIndexConstant()? a:b; + ArrayAccess & other = a.isIndexConstant()? b:a; + + // Because one of the indexes is completely known (at decision level 0), + // we include the other one in the clause. + for (int i = 0; i < indexSize; i++) + { + if (accessIndex(constantIndex,i) == l_True) + clause.push(~other.index[i]); + else + clause.push(other.index[i]); + } + } + else + { + assert (!a.isIndexConstant()); + assert (!b.isIndexConstant()); + + for (int i=0; i < indexSize;i++) + clause.push(mkLit(newVar(false,true),true)); + + // Add clauses for 1,1 => true, and 0,0 => true. + for (int i = 0; i < indexSize; i++) + { + assert (accessIndex(a,i) == accessIndex(b,i)); + assert (accessIndex(a,i) != l_Undef); + + // One of these two is used to set the intermediate value. + eqLitHelper(~a.index[i], ~b.index[i], ~clause[i+1]); + eqLitHelper(a.index[i], b.index[i], ~clause[i+1]); + } + } + assert((int)clause.size() == (indexSize+1)); + + #ifndef NDEBUG + int lvl =0; + for (int i=1; i <= indexSize;i++) + { + lvl = std::max(lvl,level(var(clause[i]))); + // All the immediates should now be true. + // But we store the "Not" of them into the clause.. + assert(value(clause[i]) == l_False); + } + assert(lvl == decisionLevel()); + #endif + + CRef from = addExtraClause(clause); + uncheckedEnqueue(result, from); + assert(value(result) == l_True); + + return propagate(); +} + +void +Solver_prop::eqLitHelper(const Lit& l0, const Lit& l1, const Lit& intermed) +{ + vec c; + c.push(intermed); + c.push(l0); + c.push(l1); + CRef f = addExtraClause(c); + + // It's only when l0 and l1 are false that anything more happens. + if (value(l0) == l_False) + { + assert(value(l1) == l_False); + assert(value(intermed) == l_Undef); + + int lvl = std::max(level(var(l0)),level(var(l1))); + assert (lvl <= decisionLevel()); + + assigns[var(intermed)] = l_True; + vardata[var(intermed)] = mkVarData(f, lvl); + + assert((ca[f][0])==intermed); + + for (int i=1; i < c.size();i++) + { + assert (value(ca[f][i]) == l_False); + assert ((level(var(ca[f][i]))) <= lvl); + } + + alternate_trail.push_back(Assignment(intermed, lvl)); + assert(level(var(intermed)) == lvl); + assert(watches[intermed].size() ==0); + } + return ; +} + +// Index is completely known. +bool Solver_prop::IndexIsSet(const ArrayAccess& iv) +{ + if (iv.isIndexConstant()) + return true; + + for (int i=0; i < iv.indexSize();i++) + { + if (value(iv.index[i]) == l_Undef) + return false; + } + return true; +} + +void +Solver_prop::printClauses() +{ + for (int i = 0; i < clauses.size(); i++) + { + const Clause &c = ca[clauses[i]]; + for (int j = 0; j < c.size(); j++) + { + printf("%c%d[%c:%d] ", sign(c[j]) ? '-' : ' ', var(c[j]), printValue(value(c[j])), level(var(c[j]))); + } + printf("\n"); + } +} + +// Assuming the index is known. Add the clauses to enforce that +// it's the same as the zeroeth array access with the same index. +CRef +Solver_prop::writeOutArrayAxiom(ArrayAccess& iv) +{ + assert(IndexIsSet(iv)); + + const uint64_t asInt = index_as_int(iv); + + if (!val_to_aa[iv.array_id].has(asInt)) + val_to_aa[iv.array_id].insert(asInt, std::vector()); + + std::vector& aa = val_to_aa[iv.array_id][asInt]; + + bool alreadyAdded = false; // Already in the bucket with the other values with the same index?? + + for (int j = 0; j < (int) aa.size(); j++) + if (&iv == aa[j]) + { + assert(!alreadyAdded); // only once. + assert(index_as_int(iv) == asInt); + alreadyAdded = true; + } + + if (!alreadyAdded) + { + assert(!iv.known_index); + + aa.push_back(&iv); + + if (arrayHistory_stack.size() > 0) + { + assert(arrayHistory_stack.last().decisionLevel <= decisionLevel()); + } + + + // So it can be removed when we cancel. + ArrayHistory h(&iv, decisionLevel()); + arrayHistory_stack.push(h); + + iv.known_index = true; + } + + if (aa.size() == 1) + return CRef_Undef; + + bool alreadyCreated = false; // Are the clauses constraining them in there. + + ArrayAccess& aa_0 = *aa[0]; + ArrayAccess& aa_back = *aa.back(); + + Lit eq; + CRef conflict = getEqualsLit(aa_0, aa_back, eq, alreadyCreated); + + if (alreadyCreated) + return CRef_Undef; // All the clauses have been created already for these guys. + + assert(value(eq) == l_True); + // Add the rhs of the equality. + + vec c; + + for (int i = 0; i < iv.valueSize(); i++) + { + c.clear(); + c.push(~eq); + + lbool a0_v = accessValue(aa_0,i); + lbool aback_v = accessValue(aa_back,i); + + CRef f; + + if (aa_0.isValueConstant() && aa_back.isValueConstant()) + { + if (a0_v != aback_v) + { + return ca.alloc(c); + } + else + continue; + } + else if (aa_0.isValueConstant()) + { + assert (a0_v != l_Undef); + + if (a0_v == l_True) + c.push(aa_back.value[i]); + else + c.push(~aa_back.value[i]); + } + else if (aa_back.isValueConstant()) + { + assert (aback_v != l_Undef); + + if (aback_v == l_True) + c.push(aa_0.value[i]); + else + c.push(~aa_0.value[i]); + } + else + { + c.push(aa_0.value[i]); + c.push(~(aa_back.value[i])); + + f = addExtraClause(c); + + assert(ca[f].size() ==3); + if ((value(ca[f][1]) == l_False) && (value(ca[f][2]) == l_False)) + { + const lbool first= value(ca[f][0]); + if (first == l_Undef) + uncheckedEnqueue(ca[f][0], f); + else if (first == l_False) + conflict = f; + } + + c.clear(); + c.push(~eq); + c.push(~aa_0.value[i]); + c.push(aa_back.value[i]); + } + + f = addExtraClause(c); + const Clause& newC = ca[f]; + + bool restFalse = true; + for (int j=1; j< newC.size();j++) + { + if (value(newC[j]) != l_False) + { + restFalse = false; + break; + } + } + + bool conflicted=false; + if (restFalse) + { + if (value(newC[0]) == l_Undef) + uncheckedEnqueue(newC[0],f); + else if (value(newC[0]) == l_False) + conflicted=true; + } + + + // We save up the conflicts because we want all of the clauses to be added. + if (conflicted) + { + int maxLevel=0; + if (!aa_0.isValueConstant()) + maxLevel = level(var(aa_0.value[i])); + + if (!aa_back.isValueConstant()) + maxLevel = std::max(level(var(aa_back.value[i])),maxLevel); + + if (maxLevel ==0) + { + c.clear(); + c.push(~eq); + return ca.alloc(c); + } + + conflict = f; + } + } + + + CRef rr = propagate(); + if (rr!=CRef_Undef) + conflict = rr; + + return conflict; +} + +// Look through each of the variables that have been set and see if they watch variables on array indexes. +CRef Solver_prop::arrayPropagate() +{ + if (watched_indexes ==0) + { + // either there are no arrays, or, + array_trail = trail.size(); + return CRef_Undef; + } + + for (; array_trail < trail.size(); array_trail++) + { + // check whether we are interested in any of the literals in the trail. + Var trail_variable = var(trail[array_trail]); + if (array_of_interest[trail_variable]) + { + Var variable = var(trail[array_trail]); + assert(watchedLiterals.has(variable)); + + // Initially I had this v as a reference. However, this instance is contained in a map, that can be rehashed and hence the vector moved around + // in memory (causing the reference to point to memory that no longer contains the vector. + std::vector v = watchedLiterals[variable]; // Take a copy. + assert(v.size() >0); + int initial_vector_size = (int)v.size(); // because more can be added in by the startWatchOfIndexVariable function. + + for (int i=0; i < (int)initial_vector_size;i++) + { + watched_indexes--; + ArrayAccess& iv = *(v[i]); + + assert(!iv.known_index); // Not already added. + assert(!iv.isIndexConstant()); // Completely known. So it should be in the map already. + assert(iv.indexSize() > 0); + + assert(var(iv.index[iv.index_index]) == trail_variable); + assert(value(iv.index[iv.index_index]) != l_Undef); + + // Checks each of the indexes around the loop!!. + int end = ((iv.index_index == 0)? iv.indexSize()-1 : iv.index_index-1); + bool first = true; // so 1-bit indexes are checked. + for (; (iv.index_index != end) || first ; iv.index_index = ((iv.index_index+1) % iv.indexSize())) + { + assert(iv.index_index < iv.indexSize()); + + lbool val = value(iv.index[iv.index_index]); + if (val == l_Undef) + break; + first = false; + } + assert(iv.index_index < iv.indexSize()); + + if (iv.index_index == end && l_Undef != value(iv.index[iv.index_index])) + { + //All of the bits are set to either true or false. + for (int w=0; w< iv.indexSize();w++) + { + assert(value(iv.index[w]) != l_Undef); + } + + CRef r = writeOutArrayAxiom(iv); + if (r != CRef_Undef) + { + std::vector& vec = watchedLiterals[variable]; + assert(vec.size() >= v.size()); + vec.erase(vec.begin(), vec.begin()+i+1); + + if(vec.size() ==0) + { + watchedLiterals.remove(variable); + array_of_interest[variable] = 0; + } + return r; + } + + assert(iv.known_index); + } + else + { + assert (value(iv.index[iv.index_index]) == l_Undef); + startWatchOfIndexVariable(&iv); + assert (!iv.known_index); // Not already added. + } + } + + std::vector& vec = watchedLiterals[variable]; // Reference. + assert(vec.size() >= v.size()); + + if((int)vec.size() == initial_vector_size) + { + // + watchedLiterals.remove(variable); + array_of_interest[variable] = 0; + } + else + { + vec.erase(vec.begin(),vec.begin() + initial_vector_size); + } + } + } + return CRef_Undef; + } + +//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +////////////////////////////////////////////////////////////////// + + +//================================================================================================= +// Minor methods: + + +// Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be +// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). +// +Var Solver_prop::newVar(bool sign, bool dvar) +{ + int v = nVars(); + watches .init(mkLit(v, false)); + watches .init(mkLit(v, true )); + assigns .push(l_Undef); + vardata .push(mkVarData(CRef_Undef, 0)); + //activity .push(0); + activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); + seen .push(0); + array_of_interest.push(0); + polarity .push(sign); + decision .push(); + trail .capacity(v+1); + setDecisionVar(v, dvar); + return v; +} + + +bool Solver_prop::addClause_(vec& ps) +{ + assert(decisionLevel() == 0); + if (!ok) return false; + + // Check if clause is satisfied and remove false/duplicate literals: + sort(ps); + Lit p; int i, j; + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) + if (value(ps[i]) == l_True || ps[i] == ~p) + return true; + else if (value(ps[i]) != l_False && ps[i] != p) + ps[j++] = p = ps[i]; + ps.shrink(i - j); + + if (ps.size() == 0) + return ok = false; + else if (ps.size() == 1){ + uncheckedEnqueue(ps[0]); + return ok = (propagate() == CRef_Undef); + }else{ + CRef cr = ca.alloc(ps, false); + clauses.push(cr); + attachClause(cr); + } + + return true; +} + + +void Solver_prop::attachClause(CRef cr) { + const Clause& c = ca[cr]; + assert(c.size() > 1); + watches[~c[0]].push(Watcher(cr, c[1])); + watches[~c[1]].push(Watcher(cr, c[0])); + if (c.learnt()) learnts_literals += c.size(); + else clauses_literals += c.size(); } + + +void Solver_prop::detachClause(CRef cr, bool strict) { + const Clause& c = ca[cr]; + assert(c.size() > 1); + + if (strict){ + remove(watches[~c[0]], Watcher(cr, c[1])); + remove(watches[~c[1]], Watcher(cr, c[0])); + }else{ + // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause) + watches.smudge(~c[0]); + watches.smudge(~c[1]); + } + + if (c.learnt()) learnts_literals -= c.size(); + else clauses_literals -= c.size(); } + + +void Solver_prop::removeClause(CRef cr) { + Clause& c = ca[cr]; + detachClause(cr); + // Don't leave pointers to free'd memory! + if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; + c.mark(1); + ca.free(cr); +} + + +bool Solver_prop::satisfied(const Clause& c) const { + for (int i = 0; i < c.size(); i++) + if (value(c[i]) == l_True) + return true; + return false; } + + +// Revert to the state at given level (keeping all assignment at 'level' but not beyond). +// +void Solver_prop::cancelUntil(int level) { + if (decisionLevel() > level){ + + struct to_re_add + { + uint64_t index_value; + int array_id; + }; + + vec toRep; + vec aaRep; + + vec toReAdd; + + // look through the map, and remove it. + while ((arrayHistory_stack.size() > 0) && (arrayHistory_stack.last().decisionLevel > level)) + { + ArrayAccess& aa = *(arrayHistory_stack.last().aa); + assert(aa.known_index); + assert(!aa.isIndexConstant()); // Shouldn't remove known indexes. + assert(IndexIsSet(aa)); // The index shouldn't be unset yet. + + // Get the integer. + uint64_t asInt = index_as_int(aa); + assert(val_to_aa[aa.array_id].has(asInt)); + + std::vector& aaV = val_to_aa[aa.array_id][asInt]; + + // We'll remove the zeroeth array access, so need to re-add all of the array axioms. + if (aaV[0] == &aa) + { + toRep.push(asInt); + aaRep.push(&aa); + } + + bool found = false; + for (int i = 0; i < (int) aaV.size(); i++) + if (aaV[i] == &aa) + { + //Find the same pointer and erase it. + aaV.erase(aaV.begin() + i); + found = true; + break; + } + assert(found); + + if (aaV.size() == 0) + val_to_aa[aa.array_id].remove(asInt); + + aa.known_index = false; + toReAdd.push(&aa); + arrayHistory_stack.shrink(1); + } + + // The zeroeth of these numbers has been deleted, so we might need to redo the implications. + for (int i=0; i < toRep.size(); i++) + { + uint64_t asInt = toRep[i]; + ArrayAccess& aa = *aaRep[i]; + + if (val_to_aa[aa.array_id].has(asInt)) + { + + std::vector& aaV = val_to_aa[aa.array_id][asInt]; + for (int j=1;j<(int)aaV.size();j++) + { + assert(aa.known_index); + writeOutArrayAxiom(*aaV[j]); + } + } + } + + sortAlternateTrail(); + while (alternate_trail.size() > 0 && (alternate_trail.back().decisionLevel > level)) + { + Var x = var( alternate_trail.back().l); + assigns [x] = l_Undef; + alternate_trail.erase(alternate_trail.end()-1); + } + alternate_trail_sorted_to = alternate_trail.size(); + + for (int c = trail.size()-1; c >= trail_lim[level]; c--){ + Var x = var(trail[c]); + assigns [x] = l_Undef; + if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) + polarity[x] = sign(trail[c]); + insertVarOrder(x); } + qhead = trail_lim[level]; + trail.shrink(trail.size() - trail_lim[level]); + trail_lim.shrink(trail_lim.size() - level); + + for (int i=0; i < toReAdd.size(); i++) + { + ArrayAccess* aa = toReAdd[i]; + startWatchOfIndexVariable(aa); + } + + array_trail = std::min(trail.size(), array_trail); + } +} + + +//================================================================================================= +// Major methods: + + +Lit Solver_prop::pickBranchLit() +{ + Var next = var_Undef; + + // Random decision: + if (drand(random_seed) < random_var_freq && !order_heap.empty()){ + next = order_heap[irand(random_seed,order_heap.size())]; + if (value(next) == l_Undef && decision[next]) + rnd_decisions++; } + + // Activity based decision: + while (next == var_Undef || value(next) != l_Undef || !decision[next]) + if (order_heap.empty()){ + next = var_Undef; + break; + }else + next = order_heap.removeMin(); + + return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]); +} + + +/*_________________________________________________________________________________________________ +| +| analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel : int&) -> [void] +| +| Description: +| Analyze conflict and produce a reason clause. +| +| Pre-conditions: +| * 'out_learnt' is assumed to be cleared. +| * Current decision level must be greater than root level. +| +| Post-conditions: +| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. +| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the +| rest of literals. There may be others from the same level though. +| +|________________________________________________________________________________________________@*/ +void Solver_prop::analyze(CRef confl, vec& out_learnt, int& out_btlevel) +{ + int pathC = 0; + Lit p = lit_Undef; + + + // Generate conflict clause: + // + out_learnt.push(); // (leave room for the asserting literal) + int index = trail.size() - 1; + + // If this is false, then we don't need to check the alternate_trail. + bool bigFound =false; + +#ifndef NDEBUG + // The conflict needs to be discovered before additional decisions are made. + int max_level2 =0; + Clause& c1 = ca[confl]; + for (int j=0; j < c1.size();j++) + { + if (max_level2 < level(var(c1[j]))) + max_level2 = level(var(c1[j])); + } + + assert (max_level2 == decisionLevel()); +#endif + + if (debug_print) + { + printf("!!starting %d\n", decisionLevel()); + printf("!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\n"); + } + do{ + assert(confl != CRef_Undef); // (otherwise should be UIP) + Clause& c = ca[confl]; + + if (c.learnt()) + claBumpActivity(c); + + for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ + Lit q = c[j]; + + if (!seen[var(q)] && level(var(q)) > 0){ + varBumpActivity(var(q)); + seen[var(q)] = 1; + + if (toInt(var(q)) >= top_level_var) + bigFound=true; + + if (level(var(q)) >= decisionLevel()) + pathC++; + else + out_learnt.push(q); + } + } + + p = lit_Undef; + + // This looks for the literal in either of the watchlists with the highest level. It's slow because + // in the worst case it will iterate completely through both lists. strcmp32.c.smt is much slower + // because of this implementation.. However most of the time alternate_trail is small because it + // only grown when a new intermediate variable is added. That variable is only added once, and + // is removed when the level it was set at is Cancelled below. + if (bigFound && alternate_trail.size() > 0) + { + sortAlternateTrail(); + + int unset_index = alternate_trail.size() - 1; + while (unset_index >= 0 && !seen[(var(alternate_trail[unset_index].l))]) + unset_index--; + + if (unset_index >= 0) + p = alternate_trail[unset_index].l; + if (debug_print && p != lit_Undef) + printf("Found unsat var: %d\n", var(p)); + + } + + + if (p == lit_Undef) + { + while (!seen[var(trail[index--])]); + p = trail[index+1]; + + if (debug_print && p != lit_Undef) + printf("(1) Found trail var: %d\n", var(p)); + + } + else + { + int t_index = index; + while (t_index>= 0 && !seen[var(trail[t_index--])]); + if (t_index >= 0) + { + if (debug_print) + printf("::%d %d\n", level(var(p)) , level(var(trail[t_index+1]))); + + if (level(var(p)) < level(var(trail[t_index+1]))) + { + p = trail[t_index+1]; + index = t_index; + } + } + if (debug_print && p != lit_Undef) + printf("(2) Found trail var: %d\n", var(p)); + + } + + + confl = reason(var(p)); + seen[var(p)] = 0; + if (debug_print) + printf("Var %d, pathC %d, level %d, isUndef %d\n",toInt(var(p)),pathC, level(var(p)), (reason(var(p)) == CRef_Undef)); + pathC--; + + if (pathC >0) + { + assert(confl != CRef_Undef); // (otherwise should be UIP) + + if (debug_print) + printf("%d %d\n", toInt(p), toInt(var(p))); + Minisat::Clause cl= ca[confl]; + + assert(ca[confl][0] ==p); + assert(value(p) != l_Undef); + } + + if (debug_print) + { + printf("Learnt Clauses:\n"); + printClause(out_learnt); + } + }while (pathC > 0); + out_learnt[0] = ~p; + + // Simplify conflict clause: + // + int i, j; + out_learnt.copyTo(analyze_toclear); + if (ccmin_mode == 2){ + uint32_t abstract_level = 0; + for (i = 1; i < out_learnt.size(); i++) + abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) + + for (i = j = 1; i < out_learnt.size(); i++) + if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level)) + out_learnt[j++] = out_learnt[i]; + + }else if (ccmin_mode == 1){ + for (i = j = 1; i < out_learnt.size(); i++){ + Var x = var(out_learnt[i]); + + if (reason(x) == CRef_Undef) + out_learnt[j++] = out_learnt[i]; + else{ + Clause& c = ca[reason(var(out_learnt[i]))]; + for (int k = 1; k < c.size(); k++) + if (!seen[var(c[k])] && level(var(c[k])) > 0){ + out_learnt[j++] = out_learnt[i]; + break; } + } + } + }else + i = j = out_learnt.size(); + + max_literals += out_learnt.size(); + out_learnt.shrink(i - j); + tot_literals += out_learnt.size(); + + // Find correct backtrack level: + // + if (out_learnt.size() == 1) + out_btlevel = 0; + else{ + int max_i = 1; + // Find the first literal assigned at the next-highest level: + for (int i = 2; i < out_learnt.size(); i++) + if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) + max_i = i; + // Swap-in this literal at index 1: + Lit p = out_learnt[max_i]; + out_learnt[max_i] = out_learnt[1]; + out_learnt[1] = p; + out_btlevel = level(var(p)); + } + + for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) +} + + +// Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is +// visiting literals at levels that cannot be removed later. +bool Solver_prop::litRedundant(Lit p, uint32_t abstract_levels) +{ + analyze_stack.clear(); analyze_stack.push(p); + int top = analyze_toclear.size(); + while (analyze_stack.size() > 0){ + assert(reason(var(analyze_stack.last())) != CRef_Undef); + Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop(); + + for (int i = 1; i < c.size(); i++){ + Lit p = c[i]; + if (!seen[var(p)] && level(var(p)) > 0){ + if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ + seen[var(p)] = 1; + analyze_stack.push(p); + analyze_toclear.push(p); + }else{ + for (int j = top; j < analyze_toclear.size(); j++) + seen[var(analyze_toclear[j])] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; + } + } + } + } + + return true; +} + + +/*_________________________________________________________________________________________________ +| +| analyzeFinal : (p : Lit) -> [void] +| +| Description: +| Specialized analysis procedure to express the final conflict in terms of assumptions. +| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and +| stores the result in 'out_conflict'. +|________________________________________________________________________________________________@*/ +void Solver_prop::analyzeFinal(Lit p, vec& out_conflict) +{ + out_conflict.clear(); + out_conflict.push(p); + + if (decisionLevel() == 0) + return; + + seen[var(p)] = 1; + + for (int i = trail.size()-1; i >= trail_lim[0]; i--){ + Var x = var(trail[i]); + if (seen[x]){ + if (reason(x) == CRef_Undef){ + assert(level(x) > 0); + out_conflict.push(~trail[i]); + }else{ + Clause& c = ca[reason(x)]; + for (int j = 1; j < c.size(); j++) + if (level(var(c[j])) > 0) + seen[var(c[j])] = 1; + } + seen[x] = 0; + } + } + + seen[var(p)] = 0; +} + + +void Solver_prop::uncheckedEnqueue(Lit p, CRef from) +{ + assert(value(p) == l_Undef); // Shouldn't be set already. + if (from != CRef_Undef) + { + assert((ca[from][0])==(p)); + + const Clause& c = ca[from]; + for (int i=1; i < c.size();i++) + { + assert (value(c[i]) != l_Undef); + assert ((level(var(c[i]))) <= decisionLevel()); + } + } + + assigns[var(p)] = lbool(!sign(p)); + vardata[var(p)] = mkVarData(from, decisionLevel()); + // + //printf("Enqueu %d with reasons %c %d\n", var(p), from == CRef_Undef?'u':'c', decisionLevel()); + trail.push_(p); + + if (from != CRef_Undef) + { + assert(ca[from][0] == p); + } + + if (false &&from != CRef_Undef) + { + Clause& c = ca[from]; + for (int i = 0; i < c.size(); i++) + { + printf("%c", printValue(value(c[i]))); + } + printf("\n"); + } +} + + +/*_________________________________________________________________________________________________ +| +| propagate : [void] -> [Clause*] +| +| Description: +| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, +| otherwise CRef_Undef. +| +| Post-conditions: +| * the propagation queue is empty, even if there was a conflict. +|________________________________________________________________________________________________@*/ +CRef Solver_prop::propagate() +{ + CRef confl = CRef_Undef; + int num_props = 0; + watches.cleanAll(); + + while (qhead < trail.size()){ + Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. + vec& ws = watches[p]; + Watcher *i, *j, *end; + num_props++; + + for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){ + // Try to avoid inspecting the clause: + Lit blocker = i->blocker; + if (value(blocker) == l_True){ + *j++ = *i++; continue; } + + // Make sure the false literal is data[1]: + CRef cr = i->cref; + Clause& c = ca[cr]; + Lit false_lit = ~p; + if (c[0] == false_lit) + c[0] = c[1], c[1] = false_lit; + assert(c[1] == false_lit); + i++; + + // If 0th watch is true, then clause is already satisfied. + Lit first = c[0]; + Watcher w = Watcher(cr, first); + if (first != blocker && value(first) == l_True){ + *j++ = w; continue; } + + // Look for new watch: + for (int k = 2; k < c.size(); k++) + if (value(c[k]) != l_False){ + c[1] = c[k]; c[k] = false_lit; + watches[~c[1]].push(w); + goto NextClause; } + + // Did not find watch -- clause is unit under assignment: + *j++ = w; + if (value(first) == l_False){ + confl = cr; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + }else + uncheckedEnqueue(first, cr); + + NextClause:; + } + ws.shrink(i - j); + } + propagations += num_props; + simpDB_props -= num_props; + + return confl; +} + + + +/*_________________________________________________________________________________________________ +| +| reduceDB : () -> [void] +| +| Description: +| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked +| clauses are clauses that are reason to some assignment. Binary clauses are never removed. +|________________________________________________________________________________________________@*/ +struct reduceDB_lt { + ClauseAllocator& ca; + reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} + bool operator () (CRef x, CRef y) { + return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } +}; +void Solver_prop::reduceDB() +{ + int i, j; + double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity + + sort(learnts, reduceDB_lt(ca)); + // Don't delete binary or locked clauses. From the rest, delete clauses from the first half + // and clauses with activity smaller than 'extra_lim': + for (i = j = 0; i < learnts.size(); i++){ + Clause& c = ca[learnts[i]]; + if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) + removeClause(learnts[i]); + else + learnts[j++] = learnts[i]; + } + learnts.shrink(i - j); + checkGarbage(); +} + + +void Solver_prop::removeSatisfied(vec& cs) +{ + int i, j; + for (i = j = 0; i < cs.size(); i++){ + Clause& c = ca[cs[i]]; + if (satisfied(c)) + removeClause(cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); +} + + +void Solver_prop::rebuildOrderHeap() +{ + vec vs; + for (Var v = 0; v < nVars(); v++) + if (decision[v] && value(v) == l_Undef) + vs.push(v); + order_heap.build(vs); +} + + +/*_________________________________________________________________________________________________ +| +| simplify : [void] -> [bool] +| +| Description: +| Simplify the clause database according to the current top-level assigment. Currently, the only +| thing done here is the removal of satisfied clauses, but more things can be put here. +|________________________________________________________________________________________________@*/ +bool Solver_prop::simplify() +{ + assert(decisionLevel() == 0); + + if (!ok || propagate() != CRef_Undef) + return ok = false; + + if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) + return true; + + // Remove satisfied clauses: + removeSatisfied(learnts); + if (remove_satisfied) // Can be turned off. + removeSatisfied(clauses); + checkGarbage(); + rebuildOrderHeap(); + + simpDB_assigns = nAssigns(); + simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) + + return true; +} + +/*_________________________________________________________________________________________________ +| +| search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] +| +| Description: +| Search for a model the specified number of conflicts. +| NOTE! Use negative value for 'nof_conflicts' indicate infinity. +| +| Output: +| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If +| all variables are decision variables, this means that the clause set is satisfiable. 'l_False' +| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. +|________________________________________________________________________________________________@*/ +lbool Solver_prop::search(int nof_conflicts) +{ + assert(ok); + int backtrack_level; + int conflictC = 0; + vec learnt_clause; + starts++; + + for (;;){ + CRef confl = propagate(); + if (confl== CRef_Undef) + confl = arrayPropagate(); + + + if (confl != CRef_Undef){ + // CONFLICT + conflicts++; conflictC++; + if (decisionLevel() == 0) return l_False; + + learnt_clause.clear(); + analyze(confl, learnt_clause, backtrack_level); + cancelUntil(backtrack_level); + if (debug_print) + { + printClause(learnt_clause); + printf("Backtrack %d\n", backtrack_level); + } + assert(value(learnt_clause[0]) == l_Undef); + + if (learnt_clause.size() == 1){ + uncheckedEnqueue(learnt_clause[0]); + }else{ + CRef cr = ca.alloc(learnt_clause, true); + learnts.push(cr); + attachClause(cr); + claBumpActivity(ca[cr]); + uncheckedEnqueue(learnt_clause[0], cr); + } + + varDecayActivity(); + claDecayActivity(); + + if (--learntsize_adjust_cnt == 0){ + learntsize_adjust_confl *= learntsize_adjust_inc; + learntsize_adjust_cnt = (int)learntsize_adjust_confl; + max_learnts *= learntsize_inc; + + if (verbosity >= 1) + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", + (int)conflicts, + (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, + (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); + } + + }else{ + // NO CONFLICT + if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + return l_Undef; } + + // Simplify the set of problem clauses: + if (decisionLevel() == 0 && !simplify()) + return l_False; + + if (learnts.size()-nAssigns() >= max_learnts) + // Reduce the set of learnt clauses: + reduceDB(); + + Lit next = lit_Undef; + while (decisionLevel() < assumptions.size()){ + // Perform user provided assumption: + Lit p = assumptions[decisionLevel()]; + if (value(p) == l_True){ + // Dummy decision level: + newDecisionLevel(); + }else if (value(p) == l_False){ + analyzeFinal(~p, conflict); + return l_False; + }else{ + next = p; + break; + } + } + + if (next == lit_Undef){ + // New variable decision: + decisions++; + next = pickBranchLit(); + + if (next == lit_Undef) + // Model found: + return l_True; + } + + // Increase decision level and enqueue 'next' + newDecisionLevel(); + uncheckedEnqueue(next); + } + } +} + + +double Solver_prop::progressEstimate() const +{ + double progress = 0; + double F = 1.0 / nVars(); + + for (int i = 0; i <= decisionLevel(); i++){ + int beg = i == 0 ? 0 : trail_lim[i - 1]; + int end = i == decisionLevel() ? trail.size() : trail_lim[i]; + progress += pow(F, i) * (end - beg); + } + + return progress / nVars(); +} + +/* + Finite subsequences of the Luby-sequence: + + 0: 1 + 1: 1 1 2 + 2: 1 1 2 1 1 2 4 + 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8 + ... + + + */ + +static double luby(double y, int x){ + + // Find the finite subsequence that contains index 'x', and the + // size of that subsequence: + int size, seq; + for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1); + + while (size-1 != x){ + size = (size-1)>>1; + seq--; + x = x % size; + } + + return pow(y, seq); +} + +// NOTE: assumptions passed in member-variable 'assumptions'. +lbool Solver_prop::solve_() +{ + model.clear(); + conflict.clear(); + if (!ok) return l_False; + + top_level_var = nVars(); + + for (int i = 0; i < toAddAtStartup.size(); i++) + { + ArrayAccess* iv = toAddAtStartup[i]; + CRef r = writeOutArrayAxiom(*iv); + if (r != CRef_Undef) + { + ok = false; + return l_False; + } + } + toAddAtStartup.clear(); + + + solves++; + + max_learnts = nClauses() * learntsize_factor; + learntsize_adjust_confl = learntsize_adjust_start_confl; + learntsize_adjust_cnt = (int)learntsize_adjust_confl; + lbool status = l_Undef; + + if (verbosity >= 1){ + printf("============================[ Search Statistics ]==============================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); + printf("===============================================================================\n"); + } + + // Search: + int curr_restarts = 0; + while (status == l_Undef){ + double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts); + status = search(rest_base * restart_first); + if (!withinBudget()) break; + curr_restarts++; + } + + if (verbosity >= 1) + printf("===============================================================================\n"); + + + if (status == l_True){ + // Extend & copy model: + model.growTo(nVars()); + for (int i = 0; i < nVars(); i++) model[i] = value(i); + + assert(watched_indexes==0); + }else if (status == l_False && conflict.size() == 0) + ok = false; + + cancelUntil(0); + return status; +} + +//================================================================================================= +// Writing CNF to DIMACS: +// +// FIXME: this needs to be rewritten completely. + +static Var mapVar(Var x, vec& map, Var& max) +{ + if (map.size() <= x || map[x] == -1){ + map.growTo(x+1, -1); + map[x] = max++; + } + return map[x]; +} + + +void Solver_prop::toDimacs(FILE* f, Clause& c, vec& map, Var& max) +{ + if (satisfied(c)) return; + + for (int i = 0; i < c.size(); i++) + if (value(c[i]) != l_False) + fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1); + fprintf(f, "0\n"); +} + + +void Solver_prop::toDimacs(const char *file, const vec& assumps) +{ + FILE* f = fopen(file, "wr"); + if (f == NULL) + fprintf(stderr, "could not open file %s\n", file), exit(1); + toDimacs(f, assumps); + fclose(f); +} + + +void Solver_prop::toDimacs(FILE* f, const vec& assumps) +{ + // Handle case when solver is in contradictory state: + if (!ok){ + fprintf(f, "p cnf 1 2\n1 0\n-1 0\n"); + return; } + + vec map; Var max = 0; + + // Cannot use removeClauses here because it is not safe + // to deallocate them at this point. Could be improved. + int cnt = 0; + for (int i = 0; i < clauses.size(); i++) + if (!satisfied(ca[clauses[i]])) + cnt++; + + for (int i = 0; i < clauses.size(); i++) + if (!satisfied(ca[clauses[i]])){ + Clause& c = ca[clauses[i]]; + for (int j = 0; j < c.size(); j++) + if (value(c[j]) != l_False) + mapVar(var(c[j]), map, max); + } + + // Assumptions are added as unit clauses: + cnt += assumptions.size(); + + fprintf(f, "p cnf %d %d\n", max, cnt); + + for (int i = 0; i < assumptions.size(); i++){ + assert(value(assumptions[i]) != l_False); + fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1); + } + + for (int i = 0; i < clauses.size(); i++) + toDimacs(f, ca[clauses[i]], map, max); + + if (verbosity > 0) + printf("Wrote %d clauses with %d variables.\n", cnt, max); +} + + +//================================================================================================= +// Garbage Collection methods: + +void Solver_prop::relocAll(ClauseAllocator& to) +{ + // All watchers: + // + // for (int i = 0; i < watches.size(); i++) + watches.cleanAll(); + for (int v = 0; v < nVars(); v++) + for (int s = 0; s < 2; s++){ + Lit p = mkLit(v, s); + // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1); + vec& ws = watches[p]; + for (int j = 0; j < ws.size(); j++) + ca.reloc(ws[j].cref, to); + } + + // All reasons: + // + for (int i = 0; i < trail.size(); i++){ + Var v = var(trail[i]); + + if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) + ca.reloc(vardata[v].reason, to); + } + + // All learnt: + // + for (int i = 0; i < learnts.size(); i++) + ca.reloc(learnts[i], to); + + // All original: + // + for (int i = 0; i < clauses.size(); i++) + ca.reloc(clauses[i], to); +} + + +void Solver_prop::garbageCollect() +{ + + // Initialize the next region to a size corresponding to the estimated utilization degree. This + // is not precise but should avoid some unnecessary reallocations for the new region: + assert(ca.wasted() <= ca.size()); + ClauseAllocator to(ca.size() - ca.wasted()); + + relocAll(to); + if (verbosity >= 2) + printf("| Garbage collection: %12d bytes => %12d bytes |\n", + ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); + to.moveTo(ca); +} diff --git a/src/sat/core_prop/Solver_prop.h b/src/sat/core_prop/Solver_prop.h new file mode 100644 index 0000000..68b86db --- /dev/null +++ b/src/sat/core_prop/Solver_prop.h @@ -0,0 +1,638 @@ +/****************************************************************************************[Solver.h] +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +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 Minisat_Solver_h +#define Minisat_Solver_h + +#include "../mtl/Vec.h" +#include "../mtl/Heap.h" +#include "../mtl/Alg.h" +#include "../utils/Options.h" +#include "../core/SolverTypes.h" +#include + + +namespace Minisat { + +//================================================================================================= +// Solver -- the main class: + +class Solver_prop { +public: + + //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////// + + // Changes for the array Propagator... +private: + + struct LessThan_Level { + Solver_prop* parent; + LessThan_Level(Solver_prop* parent_) + { + parent = parent_; + } + bool operator () (const Lit& x, const Lit& y) + { + if( parent->value(var(x)) == l_Undef) + return true; + if( parent->value(var(y)) == l_Undef) + return false; + + return parent->level(var(x)) > parent->level(var(y)); + } + }; + + + static char printValue(const lbool v) { + if (v == l_True) + return '1'; + else if (v == l_False) + return '0'; + else + return '.'; + } + + void printClause(const vec &c) { + for (int i = 0; i < c.size(); i++) { + printf("%s%d:[%c:%d] ", sign(c[i]) ? "-" : "", var(c[i]), + printValue(value(c[i])), level(var(c[i]))); + } + printf("\n"); + } + + static void printClause2(const vec &c) { + for (int i = 0; i < c.size(); i++) { + printf("%s%d ", sign(c[i]) ? "-" : "", var(c[i]) ); + } + printf("\n"); + } + + + struct EqualityVariables + { + int my_id; + int id; // other array id. + + EqualityVariables() + { + } + + EqualityVariables(int me_, int other_) + { + my_id = me_; + id = other_; + assert(me_ < other_); + } + + bool + operator==(const EqualityVariables& other) const + { + return other.my_id == my_id && other.id == id; + } + }; + + struct EqualityVariable_Hash + { + uint32_t operator()(const Minisat::Solver_prop::EqualityVariables & e) const + { return Minisat::hash(e.my_id + e.id); } + }; + + + struct ArrayAccess + { + vec index; + vec value; + + int array_id; + const int id; // unique id. + + private: + const int index_size; // bit-width of the index. + const int value_size; // bit-width of the value. + + const bool is_value_constant; // Whether the value is a constant at the start. + const bool is_index_constant; + + uint64_t index_constant; + public: + + //The index/value is entirely known in advance. + vec constant_index; + vec constant_value; + + // Whether the current object is in the watchlist. To be in the watchlist, + // the index must be known. + bool known_index; + + // Used by the watchlist to check whether the index is still unfixed. + int index_index; + + ArrayAccess(int id_, const vec& i, const vec& v, const vec& ki, const vec& kv, int arrayID): + array_id(arrayID), + id(id_), + index_size(std::max(ki.size(), i.size())), + value_size(std::max(kv.size(), v.size())), + is_value_constant(kv.size() > 0), + is_index_constant(ki.size() > 0), + index_constant(0), + index_index(0) + { + i.copyTo(index); + v.copyTo(value); + ki.copyTo(constant_index); + kv.copyTo(constant_value); + + known_index = false; + + if (is_index_constant) + { + assert(index_size <=64); + for (int i = 0; i < index_size; i++) + { + lbool v = constant_index[i]; + assert(v == l_True || v == l_False); + if (v == l_True) + index_constant += (1 << i); + } + } + } + uint64_t constantIndex() const + { + assert (is_index_constant); + return index_constant; + } + + bool + isIndexConstant() const + { + return is_index_constant; + } + + bool + isValueConstant() const + { + return is_value_constant; + } + + int + indexSize() const + { + return index_size; + } + + int + valueSize() const + { + return value_size; + } + + void + print() + { + printf("------------\n"); + + printf("Index Size: %d\n", index.size()); + printClause2(index); + + printf("Value Size: %d\n", value.size()); + printClause2(value); + + printf("Known Index: %ld ", isIndexConstant() ? index_constant : -1); + printf("Known Value: %c\n", isValueConstant() ? 't' : 'f'); + printf("Array ID:%d\n", array_id); + printf("------------\n"); + } + }; + + // We keep the decision level that an index of an array access became fixed. + // We use this to remove the access from the list of fixed indexes. + struct ArrayHistory + { + ArrayHistory(ArrayAccess*aa_, int dl) + { + aa = aa_; + decisionLevel =dl; + } + + ArrayAccess *aa; + int decisionLevel; + }; + +public: + // Holds assignments to literals that should be in trail prior to the current decision level. + struct Assignment + { + Lit l; + int decisionLevel; + Assignment(Lit l_, int dl) + { + l =l_; + decisionLevel = dl; + } + }; +private: + + CRef arrayPropagate(); // top level. + + void eqLitHelper(const Lit& l0, const Lit& l1, const Lit& intermed); + bool IndexIsSet(const ArrayAccess& iv); + + lbool accessIndex(const ArrayAccess& iv, int i); + lbool accessValue(const ArrayAccess& iv, int i); + uint64_t index_as_int(const ArrayAccess& iv); + + void startWatchOfIndexVariable(ArrayAccess* iv); + + void printClauses(); + + void assertIndexesEqual(ArrayAccess &a, ArrayAccess &b); + CRef writeOutArrayAxiom(ArrayAccess& iv); + CRef getEqualsLit(ArrayAccess &a, ArrayAccess &b, Lit & eqLit, bool &alreadyCreated); + CRef addExtraClause(vec& l); + + + + void sortVecByLevel(vec & c); + void sortAlternateTrail(); + +public: + bool addArray(int array_id, const vec& i, const vec& v, const vec& ki, const vec& kv); +private: + + vec arrayData; // So we can cleanup. + int aa_id; // next globally unique id for an array access. + int last_id; // last id for the array. + int number_of_arrays; + int array_trail; // We have checked upto this index in the trail. + int watched_indexes; + int top_level_var; + int alternate_trail_sorted_to; + + Map >* val_to_aa; // Maps from the index value of fixed indexes to the array accesses. + Map > watchedLiterals; // The literals that are watched. + vec toAddAtStartup; // These need to be added in at startup. + vec arrayHistory_stack; // When the index is fixed it's added into here. + std::vector alternate_trail; // These literals were assigned below the current decisionLevel. + + Map equality_variables; + + //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////// + +public: + // Constructor/Destructor: + // + Solver_prop(); + virtual ~Solver_prop(); + + // Problem specification: + // + Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. + + bool addClause (const vec& ps); // Add a clause to the solver. + bool addEmptyClause(); // Add the empty clause, making the solver contradictory. + bool addClause (Lit p); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver. + bool addClause_( vec& ps); // Add a clause to the solver without making superflous internal copy. Will + // change the passed vector 'ps'. + + // Solving: + // + bool simplify (); // Removes already satisfied clauses. + bool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. + lbool solveLimited (const vec& assumps); // Search for a model that respects a given set of assumptions (With resource constraints). + bool solve (); // Search without assumptions. + bool solve (Lit p); // Search for a model that respects a single assumption. + bool solve (Lit p, Lit q); // Search for a model that respects two assumptions. + bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. + bool okay () const; // FALSE means solver is in a conflicting state + + void toDimacs (FILE* f, const vec& assumps); // Write CNF to file in DIMACS-format. + void toDimacs (const char *file, const vec& assumps); + void toDimacs (FILE* f, Clause& c, vec& map, Var& max); + + // Convenience versions of 'toDimacs()': + void toDimacs (const char* file); + void toDimacs (const char* file, Lit p); + void toDimacs (const char* file, Lit p, Lit q); + void toDimacs (const char* file, Lit p, Lit q, Lit r); + + // Variable mode: + // + void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. + void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. + + // Read state: + // + lbool value (Var x) const; // The current value of a variable. + lbool value (Lit p) const; // The current value of a literal. + lbool modelValue (Var x) const; // The value of a variable in the last model. The last call to solve must have been satisfiable. + lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable. + int nAssigns () const; // The current number of assigned literals. + int nClauses () const; // The current number of original clauses. + int nLearnts () const; // The current number of learnt clauses. + int nVars () const; // The current number of variables. + int nFreeVars () const; + + // Resource contraints: + // + void setConfBudget(int64_t x); + void setPropBudget(int64_t x); + void budgetOff(); + void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver. + void clearInterrupt(); // Clear interrupt indicator flag. + + // Memory managment: + // + virtual void garbageCollect(); + void checkGarbage(double gf); + void checkGarbage(); + + // Extra results: (read-only member variable) + // + vec model; // If problem is satisfiable, this vector contains the model (if any). + vec conflict; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + + // Mode of operation: + // + int verbosity; + double var_decay; + double clause_decay; + double random_var_freq; + double random_seed; + bool luby_restart; + int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep). + int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full). + bool rnd_pol; // Use random polarities for branching heuristics. + bool rnd_init_act; // Initialize variable activities with a small random value. + double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered. + + int restart_first; // The initial restart limit. (default 100) + double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5) + double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3) + double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1) + + int learntsize_adjust_start_confl; + double learntsize_adjust_inc; + + // Statistics: (read-only member variable) + // + uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts; + uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; + +protected: + + // Helper structures: + // + struct VarData { CRef reason; int level; }; + static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; } + + struct Watcher { + CRef cref; + Lit blocker; + Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {} + bool operator==(const Watcher& w) const { return cref == w.cref; } + bool operator!=(const Watcher& w) const { return cref != w.cref; } + }; + + struct WatcherDeleted + { + const ClauseAllocator& ca; + WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {} + bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; } + }; + + struct VarOrderLt { + const vec& activity; + bool operator () (Var x, Var y) const { return activity[x] > activity[y]; } + VarOrderLt(const vec& act) : activity(act) { } + }; + + // Solver state: + // + bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! + vec clauses; // List of problem clauses. + vec learnts; // List of learnt clauses. + double cla_inc; // Amount to bump next clause with. + vec activity; // A heuristic measurement of the activity of a variable. + double var_inc; // Amount to bump next variable with. + OccLists, WatcherDeleted> + watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + vec assigns; // The current assignments. + vec polarity; // The preferred polarity of each variable. + vec decision; // Declares if a variable is eligible for selection in the decision heuristic. + vec trail; // Assignment stack; stores all assigments made in the order they were made. + vec trail_lim; // Separator indices for different decision levels in 'trail'. + vec vardata; // Stores reason and level for each variable. + int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). + int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. + int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'. + vec assumptions; // Current set of assumptions provided to solve by the user. + Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. + double progress_estimate;// Set by 'search()'. + bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. + + ClauseAllocator ca; + + // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is + // used, exept 'seen' wich is used in several places. + // + vec seen; + vec analyze_stack; + vec analyze_toclear; + vec add_tmp; + vec array_of_interest; + + double max_learnts; + double learntsize_adjust_confl; + int learntsize_adjust_cnt; + + // Resource contraints: + // + int64_t conflict_budget; // -1 means no budget. + int64_t propagation_budget; // -1 means no budget. + bool asynch_interrupt; + + // Main internal methods: + // + void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. + Lit pickBranchLit (); // Return the next decision variable. + void newDecisionLevel (); // Begins a new decision level. + void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined. + bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise. + CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause. + void cancelUntil (int level); // Backtrack until a certain level. + void analyze (CRef confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) + void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? + bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') + lbool search (int nof_conflicts); // Search for a given number of conflicts. + lbool solve_ (); // Main solve method (assumptions given in 'assumptions'). + void reduceDB (); // Reduce the set of learnt clauses. + void removeSatisfied (vec& cs); // Shrink 'cs' to contain only non-satisfied clauses. + void rebuildOrderHeap (); + + // Maintaining Variable/Clause activity: + // + void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead. + void varBumpActivity (Var v, double inc); // Increase a variable with the current 'bump' value. + void varBumpActivity (Var v); // Increase a variable with the current 'bump' value. + void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead. + void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value. + + // Operations on clauses: + // + void attachClause (CRef cr); // Attach a clause to watcher lists. + void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists. + void removeClause (CRef cr); // Detach and free a clause. + bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. + bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state. + + void relocAll (ClauseAllocator& to); + + // Misc: + // + int decisionLevel () const; // Gives the current decisionlevel. + uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels. + CRef reason (Var x) const; + int level (Var x) const; + double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... + bool withinBudget () const; + + // Static helpers: + // + + // Returns a random float 0 <= x < 1. Seed must never be 0. + static inline double drand(double& seed) { + seed *= 1389796; + int q = (int)(seed / 2147483647); + seed -= (double)q * 2147483647; + return seed / 2147483647; } + + // Returns a random integer 0 <= x < size. Seed must never be 0. + static inline int irand(double& seed, int size) { + return (int)(drand(seed) * size); } +}; + + +//================================================================================================= +// Implementation of inline methods: + +inline CRef Solver_prop::reason(Var x) const { return vardata[x].reason; } +inline int Solver_prop::level (Var x) const { return vardata[x].level; } + +inline void Solver_prop::insertVarOrder(Var x) { + if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); } + +inline void Solver_prop::varDecayActivity() { var_inc *= (1 / var_decay); } +inline void Solver_prop::varBumpActivity(Var v) { varBumpActivity(v, var_inc); } +inline void Solver_prop::varBumpActivity(Var v, double inc) { + if ( (activity[v] += inc) > 1e100 ) { + // Rescale: + for (int i = 0; i < nVars(); i++) + activity[i] *= 1e-100; + var_inc *= 1e-100; } + + // Update order_heap with respect to new activity: + if (order_heap.inHeap(v)) + order_heap.decrease(v); } + +inline void Solver_prop::claDecayActivity() { cla_inc *= (1 / clause_decay); } +inline void Solver_prop::claBumpActivity (Clause& c) { + if ( (c.activity() += cla_inc) > 1e20 ) { + // Rescale: + for (int i = 0; i < learnts.size(); i++) + ca[learnts[i]].activity() *= 1e-20; + cla_inc *= 1e-20; } } + +inline void Solver_prop::checkGarbage(void){ return checkGarbage(garbage_frac); } +inline void Solver_prop::checkGarbage(double gf){ + if (ca.wasted() > ca.size() * gf) + garbageCollect(); } + +// NOTE: enqueue does not set the ok flag! (only public methods do) +inline bool Solver_prop::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } +inline bool Solver_prop::addClause (const vec& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); } +inline bool Solver_prop::addEmptyClause () { add_tmp.clear(); return addClause_(add_tmp); } +inline bool Solver_prop::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); } +inline bool Solver_prop::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } +inline bool Solver_prop::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } +inline bool Solver_prop::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; } +inline void Solver_prop::newDecisionLevel() { trail_lim.push(trail.size()); } + +inline int Solver_prop::decisionLevel () const { return trail_lim.size(); } +inline uint32_t Solver_prop::abstractLevel (Var x) const { return 1 << (level(x) & 31); } +inline lbool Solver_prop::value (Var x) const { return assigns[x]; } +inline lbool Solver_prop::value (Lit p) const { return assigns[var(p)] ^ sign(p); } +inline lbool Solver_prop::modelValue (Var x) const { return model[x]; } +inline lbool Solver_prop::modelValue (Lit p) const { return model[var(p)] ^ sign(p); } +inline int Solver_prop::nAssigns () const { return trail.size(); } +inline int Solver_prop::nClauses () const { return clauses.size(); } +inline int Solver_prop::nLearnts () const { return learnts.size(); } +inline int Solver_prop::nVars () const { return vardata.size(); } +inline int Solver_prop::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } +inline void Solver_prop::setPolarity (Var v, bool b) { polarity[v] = b; } +inline void Solver_prop::setDecisionVar(Var v, bool b) +{ + if ( b && !decision[v]) dec_vars++; + else if (!b && decision[v]) dec_vars--; + + decision[v] = b; + insertVarOrder(v); +} +inline void Solver_prop::setConfBudget(int64_t x){ conflict_budget = conflicts + x; } +inline void Solver_prop::setPropBudget(int64_t x){ propagation_budget = propagations + x; } +inline void Solver_prop::interrupt(){ asynch_interrupt = true; } +inline void Solver_prop::clearInterrupt(){ asynch_interrupt = false; } +inline void Solver_prop::budgetOff(){ conflict_budget = propagation_budget = -1; } +inline bool Solver_prop::withinBudget() const { + return !asynch_interrupt && + (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && + (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); } + +// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a +// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or +// all calls to solve must return an 'lbool'. I'm not yet sure which I prefer. +inline bool Solver_prop::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; } +inline bool Solver_prop::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; } +inline bool Solver_prop::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; } +inline bool Solver_prop::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; } +inline bool Solver_prop::solve (const vec& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; } +inline lbool Solver_prop::solveLimited (const vec& assumps){ assumps.copyTo(assumptions); return solve_(); } +inline bool Solver_prop::okay () const { return ok; } + +inline void Solver_prop::toDimacs (const char* file){ vec as; toDimacs(file, as); } +inline void Solver_prop::toDimacs (const char* file, Lit p){ vec as; as.push(p); toDimacs(file, as); } +inline void Solver_prop::toDimacs (const char* file, Lit p, Lit q){ vec as; as.push(p); as.push(q); toDimacs(file, as); } +inline void Solver_prop::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); } + + +//================================================================================================= +// Debug etc: + + +//================================================================================================= +} + +#endif diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index 7d53053..1dc48c1 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -111,36 +111,156 @@ namespace BEEV Cnf_DataFree(cnfData); cnfData = NULL; - // Minisat doesn't, but simplifying minisat and cryptominsat eliminate variables during their - // simplification phases. The problem is that we may later add clauses in that refer to those - // simplified-away variables. Here we mark them as frozen which prevents them from being removed. - for (ArrayTransformer::ArrType::iterator it = arrayTransformer->arrayToIndexToRead.begin(); it - != arrayTransformer->arrayToIndexToRead.end(); it++) + // Minisat doesn't, but simplifying minisat and cryptominsat eliminate variables during their + // simplification phases. The problem is that we may later add clauses in that refer to those + // simplified-away variables. Here we mark them as frozen which prevents them from being removed. + for (ArrayTransformer::ArrType::iterator it = arrayTransformer->arrayToIndexToRead.begin(); + it != arrayTransformer->arrayToIndexToRead.end(); it++) { - ArrayTransformer::arrTypeMap& atm = it->second; + const ArrayTransformer::arrTypeMap& atm = it->second; - for (ArrayTransformer::arrTypeMap::const_iterator it2 = atm.begin(); it2 != atm.end(); it2++) + for (ArrayTransformer::arrTypeMap::const_iterator arr_it = atm.begin(); arr_it != atm.end(); arr_it++) { - const ArrayTransformer::ArrayRead& ar = it2->second; + const ArrayTransformer::ArrayRead& ar = arr_it->second; ASTNodeToSATVar::iterator it = nodeToSATVar.find(ar.index_symbol); if (it != nodeToSATVar.end()) { - vector& v = it->second; - for (int i=0; i < v.size(); i++) + const vector& v = it->second; + for (int i = 0; i < v.size(); i++) satSolver.setFrozen(v[i]); } - it = nodeToSATVar.find(ar.symbol); - if (it != nodeToSATVar.end()) + ASTNodeToSATVar::iterator it2 = nodeToSATVar.find(ar.symbol); + if (it2 != nodeToSATVar.end()) { - vector& v = it->second; - for (int i=0; i < v.size(); i++) + const vector& v = it2->second; + for (int i = 0; i < v.size(); i++) satSolver.setFrozen(v[i]); } } } + // One modified version of Minisat has an array propagator based solver built in. So this block sends the details of the arrays to it. + if ((bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) && bm->UserFlags.arrayread_refinement_flag ) + { + int array_id = 0; // Is incremented for each distinct array. + bool found = false; + for (ArrayTransformer::ArrType::iterator it = arrayTransformer->arrayToIndexToRead.begin(); + it != arrayTransformer->arrayToIndexToRead.end(); it++) + { + const ArrayTransformer::arrTypeMap& atm = it->second; + for (ArrayTransformer::arrTypeMap::const_iterator arr_it = atm.begin(); arr_it != atm.end(); arr_it++) + { + const ArrayTransformer::ArrayRead& ar = arr_it->second; + + // Get the the SAT solver variable numbers of the index, but, + // if it's a constant, use that instead, + // if we don't have anything, then add some new stuff in. + + ASTNodeToSATVar::iterator it = nodeToSATVar.find(ar.index_symbol); + SATSolver::vec_literals index; + Minisat::vec index_constants; + const int index_width = arr_it->first.GetValueWidth(); + if (index_width > 64) + FatalError("The array propagators unfortunately don't do arbitary precision integers yet." + " They use 64-bit integers internally to store values. Your problem has array indexes > 64 bits." + " Until this is fixed you need to run STP with the '--oldstyle-refinement' or the '-r' flag."); + if (it != nodeToSATVar.end()) + { + const vector& v = it->second; + for (int i = 0; i < index_width; i++) + index.push(SATSolver::mkLit(v[i], false)); + } + else if (ar.index_symbol.isConstant()) + { + const CBV c = ar.index_symbol.GetBVConst(); + for (int i = 0; i < index_width; i++) + if (CONSTANTBV::BitVector_bit_test(c, i)) + index_constants.push((Minisat::lbool) satSolver.true_literal()); + else + index_constants.push((Minisat::lbool) satSolver.false_literal()); + } + else + { + + // The index is ommitted from the problem. + + vector v_a; + assert(ar.index_symbol.GetKind() == SYMBOL); + // It was ommitted from the initial problem, so assign it freshly. + for (int i = 0; i < ar.index_symbol.GetValueWidth(); i++) + { + SATSolver::Var v = satSolver.newVar(); + // We probably don't want the variable eliminated. + satSolver.setFrozen(v); + v_a.push_back(v); + } + nodeToSATVar.insert(make_pair(ar.index_symbol, v_a)); + + for (int i = 0; i < v_a.size(); i++) + { + SATSolver::Var var = v_a[i]; + index.push(SATSolver::mkLit(var, false)); + } + } + + assert((index.size() > 0) ^ (index_constants.size() > 0)); + + SATSolver::vec_literals value; + Minisat::vec value_constants; + it = nodeToSATVar.find(ar.symbol); + + if (it != nodeToSATVar.end()) + { + vector& v = it->second; + for (int i = 0; i < v.size(); i++) + { + SATSolver::Var var = v[i]; + value.push(SATSolver::mkLit(var, false)); + } + } + else if (ar.symbol.isConstant()) + { + CBV c = ar.symbol.GetBVConst(); + for (int i = 0; i < ar.symbol.GetValueWidth(); i++) + if (CONSTANTBV::BitVector_bit_test(c, i)) + value_constants.push((Minisat::lbool) satSolver.true_literal()); + else + value_constants.push((Minisat::lbool) satSolver.false_literal()); + } + else + { + // The value has been ommitted.. + // I'm not sure this is needed (really). + vector v_a; + + assert(ar.symbol.GetKind() == SYMBOL); + // It was ommitted from the initial problem, so assign it freshly. + for (int i = 0; i < ar.symbol.GetValueWidth(); i++) + { + SATSolver::Var v = satSolver.newVar(); + // We probably don't want the variable eliminated. + satSolver.setFrozen(v); + v_a.push_back(v); + } + nodeToSATVar.insert(make_pair(ar.symbol, v_a)); + + for (int i = 0; i < v_a.size(); i++) + { + SATSolver::Var var = v_a[i]; + value.push(SATSolver::mkLit(var, false)); + } + } + + satSolver.addArray(array_id, index, value, index_constants, value_constants); + found = true; + } + if (found) + array_id++; + found = false; + } + } bm->GetRunTimes()->start(RunTimes::Solving); satSolver.solve(); bm->GetRunTimes()->stop(RunTimes::Solving);