From e06dc9ea6d1bf6cd8b2bd88a7ceff4971ccec368 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Thu, 29 Oct 2009 17:54:48 +0000 Subject: [PATCH] added cryptominisat. the second time git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@360 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat/AUTHORS | 10 + src/sat/cryptominisat/LICENSE | 21 + src/sat/cryptominisat/Logger.C | 748 ++++++++++ src/sat/cryptominisat/Logger.h | 159 +++ .../cryptominisat/MTRand/MersenneTwister.h | 427 ++++++ src/sat/cryptominisat/Makefile | 12 + src/sat/cryptominisat/Solver.C | 1264 +++++++++++++++++ src/sat/cryptominisat/Solver.h | 431 ++++++ src/sat/cryptominisat/SolverTypes.h | 166 +++ src/sat/cryptominisat/clause.cpp | 47 + src/sat/cryptominisat/clause.h | 160 +++ src/sat/cryptominisat/fcopy.cpp | 51 + src/sat/cryptominisat/fcopy.h | 14 + src/sat/cryptominisat/mtl/Alg.h | 62 + src/sat/cryptominisat/mtl/BasicHeap.h | 102 ++ src/sat/cryptominisat/mtl/BoxedVec.h | 151 ++ src/sat/cryptominisat/mtl/Heap.h | 173 +++ src/sat/cryptominisat/mtl/Map.h | 122 ++ src/sat/cryptominisat/mtl/Queue.h | 87 ++ src/sat/cryptominisat/mtl/Sort.h | 94 ++ src/sat/cryptominisat/mtl/Vec.h | 135 ++ src/sat/cryptominisat/mtl/template.mk | 94 ++ 22 files changed, 4530 insertions(+) create mode 100644 src/sat/cryptominisat/AUTHORS create mode 100644 src/sat/cryptominisat/LICENSE create mode 100644 src/sat/cryptominisat/Logger.C create mode 100644 src/sat/cryptominisat/Logger.h create mode 100644 src/sat/cryptominisat/MTRand/MersenneTwister.h create mode 100644 src/sat/cryptominisat/Makefile create mode 100644 src/sat/cryptominisat/Solver.C create mode 100644 src/sat/cryptominisat/Solver.h create mode 100644 src/sat/cryptominisat/SolverTypes.h create mode 100644 src/sat/cryptominisat/clause.cpp create mode 100644 src/sat/cryptominisat/clause.h create mode 100644 src/sat/cryptominisat/fcopy.cpp create mode 100644 src/sat/cryptominisat/fcopy.h create mode 100644 src/sat/cryptominisat/mtl/Alg.h create mode 100644 src/sat/cryptominisat/mtl/BasicHeap.h create mode 100644 src/sat/cryptominisat/mtl/BoxedVec.h create mode 100644 src/sat/cryptominisat/mtl/Heap.h create mode 100644 src/sat/cryptominisat/mtl/Map.h create mode 100644 src/sat/cryptominisat/mtl/Queue.h create mode 100644 src/sat/cryptominisat/mtl/Sort.h create mode 100644 src/sat/cryptominisat/mtl/Vec.h create mode 100644 src/sat/cryptominisat/mtl/template.mk diff --git a/src/sat/cryptominisat/AUTHORS b/src/sat/cryptominisat/AUTHORS new file mode 100644 index 0000000..98599fa --- /dev/null +++ b/src/sat/cryptominisat/AUTHORS @@ -0,0 +1,10 @@ +Niklas Eén +Niklas Sörensson +Mate SOOS +Karsten Nohl + +thanks to: +- the authors' professors for their trust in their PhD students' capabilities +- the gcc compiler team for the excellent C++ compiler +- libstdc team for the excellent standard library +- Bjarne Stroustrup for the excellent C++ diff --git a/src/sat/cryptominisat/LICENSE b/src/sat/cryptominisat/LICENSE new file mode 100644 index 0000000..beb0799 --- /dev/null +++ b/src/sat/cryptominisat/LICENSE @@ -0,0 +1,21 @@ +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 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. diff --git a/src/sat/cryptominisat/Logger.C b/src/sat/cryptominisat/Logger.C new file mode 100644 index 0000000..2bb52d0 --- /dev/null +++ b/src/sat/cryptominisat/Logger.C @@ -0,0 +1,748 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 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 +#include +#include +#include +#include +#include +#include +#include +using std::cout; +using std::endl; +using std::ofstream; + +#include "Logger.h" +#include "fcopy.h" +#include "SolverTypes.h" + +namespace MINISAT +{ + +#define MAX_VAR 1000000 + +#define FST_WIDTH 10 +#define SND_WIDTH 35 +#define TRD_WIDTH 10 + +Logger::Logger(int& _verbosity) : + proof_graph_on(false), + statistics_on(false), + + max_print_lines(20), + uniqueid(1), + level(0), + begin_level(0), + max_group(0), + + proof(NULL), + proof_num(0), + + sum_conflict_depths(0), + no_conflicts(0), + no_decisions(0), + no_propagations(0), + sum_decisions_on_branches(0), + sum_propagations_on_branches(0), + + verbosity(_verbosity) +{ + runid /= 10; + runid=time(NULL)%10000; + if (verbosity >= 1) printf("RunID is: #%d\n",runid); + + sprintf(filename0,"proofs/%d-proof0.dot", runid); +} + +// Adds a new variable to the knowledge of the logger +void Logger::new_var(const Var var) +{ + assert(var < MAX_VAR); + + if (varnames.size() <= var) { + varnames.resize(var+1); + times_var_propagated.resize(var+1); + times_var_guessed.resize(var+1); + depths_of_assigns_for_var.resize(var+1); + } +} + +// Resizes the groupnames and other, related vectors to accomodate for a new group +void Logger::new_group(const uint group) +{ + if (groupnames.size() <= group) { + uint old_size = times_group_caused_propagation.size(); + groupnames.resize(group+1, "Noname"); + times_group_caused_conflict.resize(group+1); + times_group_caused_propagation.resize(group+1); + depths_of_propagations_for_group.resize(group+1); + depths_of_conflicts_for_group.resize(group+1); + for (uint i = old_size; i < times_group_caused_propagation.size(); i++) { + times_group_caused_propagation[i] = 0; + times_group_caused_conflict[i] = 0; + } + } + + max_group = std::max(group, max_group); +} + +// Adds the new clause group's name to the information stored +void Logger::set_group_name(const uint group, const char* name) +{ + new_group(group); + + if (strlen(name) > SND_WIDTH-2) { + cout << "A clause group name cannot have more than " << SND_WIDTH-2 << " number of characters. You gave '" << name << "', which is " << strlen(name) << " long." << endl; + exit(-1); + } + + if (groupnames[group].empty() || groupnames[group] == "Noname") { + groupnames[group] = name; + } else if (name != '\0' && groupnames[group] != name) { + printf("Error! Group no. %d has been named twice. First, as '%s', then second as '%s'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line\n", group, groupnames[group].c_str(), name); + exit(-1); + } +} + +// sets the variable's name +void Logger::set_variable_name(const uint var, const char* name) +{ + if (!proof_graph_on && !statistics_on) return; + + if (strlen(name) > SND_WIDTH-2) { + cout << "A variable name cannot have more than " << SND_WIDTH-2 << " number of characters. You gave '" << name << "', which is " << strlen(name) << " long." << endl; + exit(-1); + } + + new_var(var); + varnames[var] = name; +} + +void Logger::begin() +{ + char filename[80]; + sprintf(filename, "proofs/%d-proof%d.dot", runid, proof_num); + + if (proof_num > 0) { + if (proof_graph_on) { + FileCopy(filename0, filename); + proof = fopen(filename,"a"); + if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename), exit(-1); + } + } else { + history.growTo(10); + history[level] = uniqueid; + + if (proof_graph_on) { + proof = fopen(filename,"w"); + if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename), exit(-1); + fprintf(proof, "digraph G {\n"); + fprintf(proof,"node%d [shape=circle, label=\"BEGIN\", root];\n", uniqueid); + } + } + + if (statistics_on) + reset_statistics(); + + level = begin_level; +} + +// For noting conflicts. Updates the proof graph and the statistics. +void Logger::conflict(const confl_type type, uint goback, const uint group, const vec& learnt_clause) +{ + assert(!(proof == NULL && proof_graph_on)); + assert(goback < level); + + goback += begin_level; + uniqueid++; + + if (proof_graph_on) { + fprintf(proof,"node%d [shape=polygon,sides=5,label=\"",uniqueid); + for (int i = 0; i < learnt_clause.size(); i++) { + if (learnt_clause[i].sign()) fprintf(proof,"-"); + int myvar = learnt_clause[i].var(); + if (varnames.size() <= myvar || varnames[myvar].empty()) + fprintf(proof,"%d\\n",myvar+1); + else fprintf(proof,"%s\\n",varnames[myvar].c_str()); + } + + fprintf(proof,"\"];\n"); + + fprintf(proof,"node%d -> node%d [label=\"",history[level],uniqueid); + + if (type == gauss_confl_type) { + fprintf(proof,"Gauss\",style=bold"); + } else if (group > max_group) fprintf(proof,"**%d\"",group); + else { + if (groupnames.size() <= group || groupnames[group].empty()) + fprintf(proof,"%d\"", group); + else fprintf(proof,"%s\"", groupnames[group].c_str()); + } + + fprintf(proof,"];\n"); + fprintf(proof,"node%d -> node%d [style=bold];\n",uniqueid,history[goback]); + } + + if (statistics_on) { + const uint depth = level - begin_level; + + if (group < max_group) { //TODO make work for learnt clauses + times_group_caused_conflict[group]++; + depths_of_conflicts_for_group[group].push_back(depth); + } + no_conflicts++; + sum_conflict_depths += depth; + sum_decisions_on_branches += decisions[depth]; + sum_propagations_on_branches += propagations[depth]; + branch_depth_distrib[depth]++; + } + + level = goback; +} + +// For the really strange event that the solver is given an empty clause +void Logger::empty_clause(const uint group) +{ + assert(!(proof == NULL && proof_graph_on)); + + if (proof_graph_on) { + fprintf(proof,"node%d -> node%d [label=\"emtpy clause:",history[level],uniqueid+1); + if (group > max_group) fprintf(proof,"**%d\\n",group); + else { + if (groupnames.size() <= group || groupnames[group].empty()) + fprintf(proof,"%d\\n", group); + else fprintf(proof,"%s\\n", groupnames[group].c_str()); + } + + fprintf(proof,"\"];\n"); + } +} + +// Propagating a literal. Type of literal and the (learned clause's)/(propagating clause's)/(etc) group must be given. Updates the proof graph and the statistics. note: the meaning of the variable 'group' depends on the type +void Logger::propagation(const Lit lit, const prop_type type, const uint group) +{ + assert(!(proof == NULL && proof_graph_on)); + uniqueid++; + + //graph + if (proof_graph_on) { + fprintf(proof,"node%d [shape=box, label=\"",uniqueid);; + if (lit.sign()) fprintf(proof,"-"); + if (varnames.size() <= lit.var() || varnames[lit.var()].empty()) + fprintf(proof,"%d\"];\n",lit.var()+1); + else fprintf(proof,"%s\"];\n",varnames[lit.var()].c_str()); + + fprintf(proof,"node%d -> node%d [label=\"",history[level],uniqueid); + switch (type) { + + case revert_guess_type: + case simple_propagation_type: + assert(group != UINT_MAX); + if (group > max_group) fprintf(proof,"**%d\\n",group); + else { + if (groupnames.size() <= group || groupnames[group].empty()) + fprintf(proof,"%d\\n", group); + else fprintf(proof,"%s\\n", groupnames[group].c_str()); + } + + fprintf(proof,"\"];\n"); + break; + + case gauss_propagation_type: + fprintf(proof,"Gauss\",style=bold];\n"); + break; + + case learnt_unit_clause_type: + fprintf(proof,"learnt unit clause\",style=bold];\n"); + break; + + case assumption_type: + fprintf(proof,"assumption\"];\n"); + break; + + case guess_type: + fprintf(proof,"guess\",style=dotted];\n"); + break; + + case addclause_type: + assert(group != UINT_MAX); + if (groupnames.size() <= group || groupnames[group].empty()) + fprintf(proof,"red. from %d\"];\n",group); + else fprintf(proof,"red. from %s\"];\n",groupnames[group].c_str()); + break; + } + } + + if (statistics_on && proof_num > 0) switch (type) { + case gauss_propagation_type: + case simple_propagation_type: + no_propagations++; + times_var_propagated[lit.var()]++; + if (group < max_group) { //TODO make work for learnt clauses + depths_of_propagations_for_group[group].push_back(level - begin_level); + times_group_caused_propagation[group]++; + } + depths_of_assigns_for_var[lit.var()].push_back(level - begin_level); + break; + + case learnt_unit_clause_type: //when learning unit clause + case revert_guess_type: //when, after conflict, a guess gets reverted + if (group < max_group) { //TODO make work for learnt clauses + times_group_caused_propagation[group]++; + depths_of_propagations_for_group[group].push_back(level - begin_level); + } + depths_of_assigns_for_var[lit.var()].push_back(level - begin_level); + case guess_type: + times_var_guessed[lit.var()]++; + depths_of_assigns_for_var[lit.var()].push_back(level - begin_level); + no_decisions++; + break; + + case addclause_type: + case assumption_type: + assert(false); + } + + level++; + + if (proof_num > 0) { + decisions.growTo(level-begin_level+1); + propagations.growTo(level-begin_level+1); + if (level-begin_level == 1) { + decisions[0] = 0; + propagations[0] = 0; + //note: we might reach this place TWICE in the same restart. This is because the first assignement might get reverted + } + if (type == simple_propagation_type) { + decisions[level-begin_level] = decisions[level-begin_level-1]; + propagations[level-begin_level] = propagations[level-begin_level-1]+1; + } else { + decisions[level-begin_level] = decisions[level-begin_level-1]+1; + propagations[level-begin_level] = propagations[level-begin_level-1]; + } + } + + if (history.size() < level+1) history.growTo(level+10); + history[level] = uniqueid; +} + +// Ending of a restart iteration. Also called when ending S.simplify(); +void Logger::end(const finish_type finish) +{ + assert(!(proof == NULL && proof_graph_on)); + + switch (finish) { + case model_found: { + uniqueid++; + if (proof_graph_on) fprintf(proof,"node%d [shape=doublecircle, label=\"MODEL\"];\n",uniqueid); + break; + } + case unsat_model_found: { + uniqueid++; + if (proof_graph_on) fprintf(proof,"node%d [shape=doublecircle, label=\"UNSAT\"];\n",uniqueid); + break; + } + case restarting: { + uniqueid++; + if (proof_graph_on) fprintf(proof,"node%d [shape=doublecircle, label=\"Re-starting\\nsearch\"];\n",uniqueid); + break; + } + case done_adding_clauses: { + begin_level = level; + break; + } + } + + if (proof_graph_on) { + if (proof_num > 0) { + fprintf(proof,"node%d -> node%d;\n",history[level],uniqueid); + fprintf(proof,"}\n"); + } else proof0_lastid = uniqueid; + + proof = (FILE*)fclose(proof); + assert(proof == NULL); + + if (finish == model_found || finish == unsat_model_found) { + proof = fopen(filename0,"a"); + fprintf(proof,"node%d [shape=doublecircle, label=\"Done adding\\nclauses\"];\n",proof0_lastid+1); + fprintf(proof,"node%d -> node%d;\n",proof0_lastid,proof0_lastid+1); + fprintf(proof,"}\n"); + proof = (FILE*)fclose(proof); + assert(proof == NULL); + } + } + + if (statistics_on) printstats(); + + proof_num++; +} + +void Logger::print_footer() const +{ + cout << "+" << std::setfill('-') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << "-" << std::setfill(' ') << "+" << endl; +} + +void Logger::print_assign_var_order() const +{ + vector > prop_ordered; + for (uint i = 0; i < depths_of_assigns_for_var.size(); i++) { + double avg = 0.0; + for (vector::const_iterator it = depths_of_assigns_for_var[i].begin(); it != depths_of_assigns_for_var[i].end(); it++) + avg += *it; + if (depths_of_assigns_for_var[i].size() > 0) { + avg /= (double) depths_of_assigns_for_var[i].size(); + prop_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!prop_ordered.empty()) { + print_footer(); + print_simple_line(" Variables are assigned in the following order"); + print_header("var", "var name", "avg order"); + std::sort(prop_ordered.begin(), prop_ordered.end()); + print_vars(prop_ordered); + } +} + +void Logger::print_prop_order() const +{ + vector > prop_ordered; + for (uint i = 0; i < depths_of_propagations_for_group.size(); i++) { + double avg = 0.0; + for (vector::const_iterator it = depths_of_propagations_for_group[i].begin(); it != depths_of_propagations_for_group[i].end(); it++) + avg += *it; + if (depths_of_propagations_for_group[i].size() > 0) { + avg /= (double) depths_of_propagations_for_group[i].size(); + prop_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!prop_ordered.empty()) { + print_footer(); + print_simple_line(" Propagation depth order of clause groups"); + print_header("group", "group name", "avg order"); + std::sort(prop_ordered.begin(), prop_ordered.end()); + print_groups(prop_ordered); + } +} + +void Logger::print_confl_order() const +{ + vector > confl_ordered; + for (uint i = 0; i < depths_of_conflicts_for_group.size(); i++) { + double avg = 0.0; + for (vector::const_iterator it = depths_of_conflicts_for_group[i].begin(); it != depths_of_conflicts_for_group[i].end(); it++) + avg += *it; + if (depths_of_conflicts_for_group[i].size() > 0) { + avg /= (double) depths_of_conflicts_for_group[i].size(); + confl_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!confl_ordered.empty()) { + print_footer(); + print_simple_line(" Avg. conflict depth order of clause groups"); + print_header("groupno", "group name", "avg. depth"); + std::sort(confl_ordered.begin(), confl_ordered.end()); + print_groups(confl_ordered); + } +} + + +void Logger::print_times_var_guessed() const +{ + vector > times_var_ordered; + for (int i = 0; i < varnames.size(); i++) if (times_var_guessed[i] > 0) + times_var_ordered.push_back(std::make_pair(times_var_guessed[i], i)); + + if (!times_var_ordered.empty()) { + print_footer(); + print_simple_line(" No. times variable branched on"); + print_header("var", "var name", "no. times"); + std::sort(times_var_ordered.rbegin(), times_var_ordered.rend()); + print_vars(times_var_ordered); + } +} + +void Logger::print_times_group_caused_propagation() const +{ + vector > props_group_ordered; + for (uint i = 0; i < times_group_caused_propagation.size(); i++) + if (times_group_caused_propagation[i] > 0) + props_group_ordered.push_back(std::make_pair(times_group_caused_propagation[i], i)); + + if (!props_group_ordered.empty()) { + print_footer(); + print_simple_line(" No. propagations made by clause groups"); + print_header("group", "group name", "no. props"); + std::sort(props_group_ordered.rbegin(),props_group_ordered.rend()); + print_groups(props_group_ordered); + } +} + +void Logger::print_times_group_caused_conflict() const +{ + vector > confls_group_ordered; + for (uint i = 0; i < times_group_caused_conflict.size(); i++) + if (times_group_caused_conflict[i] > 0) + confls_group_ordered.push_back(std::make_pair(times_group_caused_conflict[i], i)); + + if (!confls_group_ordered.empty()) { + print_footer(); + print_simple_line(" No. conflicts made by clause groups"); + print_header("group", "group name", "no. confl"); + std::sort(confls_group_ordered.rbegin(), confls_group_ordered.rend()); + print_groups(confls_group_ordered); + } +} + +template +inline void Logger::print_line(const uint& number, const string& name, const T& value) const +{ + cout << "|" << std::setw(FST_WIDTH) << number << " " << std::setw(SND_WIDTH) << name << " " << std::setw(TRD_WIDTH) << value << "|" << endl; +} + +void Logger::print_header(const string& first, const string& second, const string& third) const +{ + cout << "|" << std::setw(FST_WIDTH) << first << " " << std::setw(SND_WIDTH) << second << " " << std::setw(TRD_WIDTH) << third << "|" << endl; + print_footer(); +} + +void Logger::print_groups(const vector >& to_print) const +{ + uint i = 0; + typedef vector >::const_iterator myiterator; + for (myiterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + string name; + + if (it->second > max_group) + name = "learnt clause"; + else + name = groupnames[it->second]; + + print_line(it->second+1, name, it->first); + } + print_footer(); +} + +void Logger::print_groups(const vector >& to_print) const +{ + uint i = 0; + typedef vector >::const_iterator myiterator; + for (myiterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + string name; + + if (it->second > max_group) + name = "learnt clause"; + else + name = groupnames[it->second]; + + print_line(it->second+1, name, it->first); + } + print_footer(); +} + +void Logger::print_vars(const vector >& to_print) const +{ + uint i = 0; + for (vector >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) + print_line(it->second+1, varnames[it->second], it->first); + + print_footer(); +} + +void Logger::print_vars(const vector >& to_print) const +{ + uint i = 0; + for (vector >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + print_line(it->second+1, varnames[it->second], it->first); + } + + print_footer(); +} + +template +void Logger::print_line(const string& str, const T& num) const +{ + cout << "|" << std::setw(FST_WIDTH+SND_WIDTH+4) << str << std::setw(TRD_WIDTH) << num << "|" << endl; +} + +void Logger::print_simple_line(const string& str) const +{ + cout << "|" << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << str << "|" << endl; +} + +void Logger::print_branch_depth_distrib() const +{ + //cout << "--- Branch depth stats ---" << endl; + + const uint range = 20; + map range_stat; + + for (map::const_iterator it = branch_depth_distrib.begin(); it != branch_depth_distrib.end(); it++) { + //cout << it->first << " : " << it->second << endl; + range_stat[it->first/range] += it->second; + } + //cout << endl; + + print_footer(); + print_simple_line(" No. search branches with branch depth between"); + print_line("Branch depth between", "no. br.-s"); + print_footer(); + + std::stringstream ss; + ss << "branch_depths/branch_depth_file" << runid << "-" << proof_num << ".txt"; + ofstream branch_depth_file; + branch_depth_file.open(ss.str().c_str()); + uint i = 0; + + for (map::iterator it = range_stat.begin(); it != range_stat.end(); it++) { + std::stringstream ss2; + ss2 << it->first*range << " - " << it->first*range + range-1; + print_line(ss2.str(), it->second); + + if (branch_depth_file.is_open()) { + branch_depth_file << i << "\t" << it->second << "\t"; + if (i % 5 == 0) + branch_depth_file << "\"" << it->first*range << "\""; + else + branch_depth_file << "\"\""; + branch_depth_file << endl; + } + i++; + } + if (branch_depth_file.is_open()) + branch_depth_file.close(); + print_footer(); + +} + +void Logger::print_general_stats(uint restarts, uint64_t conflicts, int vars, int noClauses, uint64_t clauses_Literals, int noLearnts, double litsPerLearntCl, double progressEstimate) const +{ + print_footer(); + print_simple_line(" Standard MiniSat restart statistics"); + print_footer(); + print_line("Restart number", restarts); + print_line("Number of conflicts", conflicts); + print_line("Number of variables", vars); + print_line("Number of clauses", noClauses); + print_line("Number of literals in clauses",clauses_Literals); + print_line("Avg. literals per learnt clause",litsPerLearntCl); + print_line("Progress estimate (%):", progressEstimate); + print_footer(); +} + + +// Prints statistics on the console +void Logger::printstats() const +{ + assert(statistics_on); + assert(varnames.size() == times_var_guessed.size()); + assert(varnames.size() == times_var_propagated.size()); + + printf("\n"); + cout << "+" << std::setfill('=') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << "=" << "+" << endl; + cout << "||" << std::setfill('*') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+2) << "********* STATS FOR THIS RESTART BEGIN " << "||" << endl; + cout << "+" << std::setfill('=') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << "=" << std::setfill(' ') << "+" << endl; + cout.setf(std::ios_base::left); + cout.precision(4); + print_times_var_guessed(); + print_times_group_caused_propagation(); + print_times_group_caused_conflict(); + print_prop_order(); + print_confl_order(); + print_assign_var_order(); + print_branch_depth_distrib(); + + print_footer(); + print_simple_line(" Advanced statistics"); + print_footer(); + print_line("No. branches visited", no_conflicts); + print_line("Avg. branch depth", (double)sum_conflict_depths/(double)no_conflicts); + print_line("No. decisions", no_decisions); + print_line("No. propagations",no_propagations); + + //printf("no progatations/no decisions (i.e. one decision gives how many propagations on average *for the whole search graph*): %f\n", (double)no_propagations/(double)no_decisions); + //printf("no propagations/sum decisions on branches (if you look at one specific branch, what is the average number of propagations you will find?): %f\n", (double)no_propagations/(double)sum_decisions_on_branches); + + print_simple_line("sum decisions on branches/no. branches"); + print_simple_line(" (in a given branch, what is the avg."); + print_line(" no. of decisions?)",(double)sum_decisions_on_branches/(double)no_conflicts); + + print_simple_line("sum propagations on branches/no. branches"); + print_simple_line(" (in a given branch, what is the"); + print_line(" avg. no. of propagations?)",(double)sum_propagations_on_branches/(double)no_conflicts); + print_footer(); + + print_footer(); + print_simple_line("Statistics note: If you used CryptoMiniSat as"); + print_simple_line("a library then vars are all shifted by 1 here"); + print_simple_line("and in every printed output of the solver."); + print_simple_line("This does not apply when you use CryptoMiniSat"); + print_simple_line("as a stand-alone program."); + print_footer(); +} + +// resets all stored statistics. Might be useful, to generate statistics for each restart and not for the whole search in general +void Logger::reset_statistics() +{ + assert(times_var_guessed.size() == times_var_propagated.size()); + assert(times_group_caused_conflict.size() == times_group_caused_propagation.size()); + + typedef vector::iterator vecit; + for (vecit it = times_var_guessed.begin(); it != times_var_guessed.end(); it++) + *it = 0; + + for (vecit it = times_var_propagated.begin(); it != times_var_propagated.end(); it++) + *it = 0; + + for (vecit it = times_group_caused_conflict.begin(); it != times_group_caused_conflict.end(); it++) + *it = 0; + + for (vecit it = times_group_caused_propagation.begin(); it != times_group_caused_propagation.end(); it++) + *it = 0; + + for (vecit it = confls_by_group.begin(); it != confls_by_group.end(); it++) + *it = 0; + + for (vecit it = props_by_group.begin(); it != props_by_group.end(); it++) + *it = 0; + + typedef vector >::iterator vecvecit; + + for (vecvecit it = depths_of_propagations_for_group.begin(); it != depths_of_propagations_for_group.end(); it++) + it->clear(); + + for (vecvecit it = depths_of_conflicts_for_group.begin(); it != depths_of_conflicts_for_group.end(); it++) + it->clear(); + + for (vecvecit it = depths_of_assigns_for_var.begin(); it != depths_of_assigns_for_var.end(); it++) + it->clear(); + + sum_conflict_depths = 0; + no_conflicts = 0; + no_decisions = 0; + no_propagations = 0; + decisions.clear(); + propagations.clear(); + sum_decisions_on_branches = 0; + sum_propagations_on_branches = 0; + branch_depth_distrib.clear(); +} +}; diff --git a/src/sat/cryptominisat/Logger.h b/src/sat/cryptominisat/Logger.h new file mode 100644 index 0000000..1fae9a7 --- /dev/null +++ b/src/sat/cryptominisat/Logger.h @@ -0,0 +1,159 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 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. +**************************************************************************************************/ + +#ifndef __LOGGER_H__ +#define __LOGGER_H__ + +#include +#include +//#include +#include + +#include "mtl/Vec.h" +#include "mtl/Heap.h" +#include "mtl/Alg.h" +#include "Logger.h" +#include "SolverTypes.h" +#include +#include +#include "stdint.h" +#include "limits.h" + +using std::vector; +using std::pair; +using std::string; +using std::map; + + +namespace MINISAT +{ +#ifndef uint +#define uint unsigned int +#endif + +class Logger +{ +public: + Logger(int& vebosity); + + //types of props, confl, and finish + enum prop_type { revert_guess_type, learnt_unit_clause_type, assumption_type, guess_type, addclause_type, simple_propagation_type, gauss_propagation_type }; + enum confl_type { simple_confl_type, gauss_confl_type }; + enum finish_type { model_found, unsat_model_found, restarting, done_adding_clauses }; + + //Conflict and propagation(guess is also a proapgation...) + void conflict(const confl_type type, uint goback, const uint group, const vec& learnt_clause); + void propagation(const Lit lit, const prop_type type, const uint group = UINT_MAX); + void empty_clause(const uint group); + + //functions to add/name variables + void new_var(const Var var); + void set_variable_name(const uint var, const char* name); + + //functions to add/name clause groups + void new_group(const uint group); + void set_group_name(const uint group, const char* name); + + void begin(); + void end(const finish_type finish); + void print_general_stats(uint restarts, uint64_t conflicts, int vars, int noClauses, uint64_t clauses_Literals, int noLearnts, double litsPerLearntCl, double progressEstimate) const; + + void newclause(const vec& ps, const bool xor_clause, const uint group); + + bool proof_graph_on; + bool statistics_on; +private: + void print_groups(const vector >& to_print) const; + void print_groups(const vector >& to_print) const; + void print_vars(const vector >& to_print) const; + void print_vars(const vector >& to_print) const; + void print_times_var_guessed() const; + void print_times_group_caused_propagation() const; + void print_times_group_caused_conflict() const; + void print_branch_depth_distrib() const; + + uint max_print_lines; + template + void print_line(const uint& number, const string& name, const T& value) const; + void print_header(const string& first, const string& second, const string& third) const; + void print_footer() const; + template + void print_line(const string& str, const T& num) const; + void print_simple_line(const string& str) const; + void print_confl_order() const; + void print_prop_order() const; + void print_assign_var_order() const; + void printstats() const; + void reset_statistics(); + + //internal data structures + uint uniqueid; //used to store the last unique ID given to a node + vec history; //stores the node uniqueIDs + uint level; //used to know the current level + uint begin_level; + uint max_group; + + //graph drawing + FILE* proof; //The file to store the proof + uint proof_num; + char filename0[80]; + uint runid; + uint proof0_lastid; + + //--------------------- + //statistics collection + //--------------------- + + //group and var names + vector groupnames; + vector varnames; + + //confls and props grouped by clause groups + vector confls_by_group; + vector props_by_group; + + //props and guesses grouped by vars + vector times_var_guessed; + vector times_var_propagated; + + vector times_group_caused_conflict; + vector times_group_caused_propagation; + + vector > depths_of_propagations_for_group; + vector > depths_of_conflicts_for_group; + vector > depths_of_assigns_for_var; + + //the distribution of branch depths. first = depth, second = number of occurances + map branch_depth_distrib; + + uint sum_conflict_depths; + uint no_conflicts; + uint no_decisions; + uint no_propagations; + vec decisions; + vec propagations; + uint sum_decisions_on_branches; + uint sum_propagations_on_branches; + + //message display properties + const int& verbosity; +}; + +}; +#endif //__LOGGER_H__ diff --git a/src/sat/cryptominisat/MTRand/MersenneTwister.h b/src/sat/cryptominisat/MTRand/MersenneTwister.h new file mode 100644 index 0000000..964ecc7 --- /dev/null +++ b/src/sat/cryptominisat/MTRand/MersenneTwister.h @@ -0,0 +1,427 @@ +// MersenneTwister.h +// Mersenne Twister random number generator -- a C++ class MTRand +// Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus +// Richard J. Wagner v1.0 15 May 2003 rjwagner@writeme.com + +// The Mersenne Twister is an algorithm for generating random numbers. It +// was designed with consideration of the flaws in various other generators. +// The period, 2^19937-1, and the order of equidistribution, 623 dimensions, +// are far greater. The generator is also fast; it avoids multiplication and +// division, and it benefits from caches and pipelines. For more information +// see the inventors' web page at http://www.math.keio.ac.jp/~matumoto/emt.html + +// Reference +// M. Matsumoto and T. Nishimura, "Mersenne Twister: A 623-Dimensionally +// Equidistributed Uniform Pseudo-Random Number Generator", ACM Transactions on +// Modeling and Computer Simulation, Vol. 8, No. 1, January 1998, pp 3-30. + +// Copyright (C) 1997 - 2002, Makoto Matsumoto and Takuji Nishimura, +// Copyright (C) 2000 - 2003, Richard J. Wagner +// All rights reserved. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions +// are met: +// +// 1. Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// +// 2. Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// +// 3. The names of its contributors may not be used to endorse or promote +// products derived from this software without specific prior written +// permission. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +// CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +// The original code included the following notice: +// +// When you use this, send an email to: matumoto@math.keio.ac.jp +// with an appropriate reference to your work. +// +// It would be nice to CC: rjwagner@writeme.com and Cokus@math.washington.edu +// when you write. + +#ifndef MERSENNETWISTER_H +#define MERSENNETWISTER_H + +#include +#include +#include +#include +#include + +namespace MINISAT +{ + +// Not thread safe (unless auto-initialization is avoided and each thread has +// its own MTRand object) + +class MTRand { +// Data +public: + typedef unsigned long uint32; // unsigned integer type, at least 32 bits + + enum { N = 624 }; // length of state vector + enum { SAVE = N + 1 }; // length of array for save() + +protected: + enum { M = 397 }; // period parameter + + uint32 state[N]; // internal state + uint32 *pNext; // next value to get from state + int left; // number of values left before reload needed + + +//Methods +public: + MTRand( const uint32& oneSeed ); // initialize with a simple uint32 + MTRand( uint32 *const bigSeed, uint32 const seedLength = N ); // or an array + MTRand(); // auto-initialize with /dev/urandom or time() and clock() + + // Do NOT use for CRYPTOGRAPHY without securely hashing several returned + // values together, otherwise the generator state can be learned after + // reading 624 consecutive values. + + // Access to 32-bit random numbers + double rand(); // real number in [0,1] + double rand( const double& n ); // real number in [0,n] + double randExc(); // real number in [0,1) + double randExc( const double& n ); // real number in [0,n) + double randDblExc(); // real number in (0,1) + double randDblExc( const double& n ); // real number in (0,n) + uint32 randInt(); // integer in [0,2^32-1] + uint32 randInt( const uint32& n ); // integer in [0,n] for n < 2^32 + double operator()() { return rand(); } // same as rand() + + // Access to 53-bit random numbers (capacity of IEEE double precision) + double rand53(); // real number in [0,1) + + // Access to nonuniform random number distributions + double randNorm( const double& mean = 0.0, const double& variance = 0.0 ); + + // Re-seeding functions with same behavior as initializers + void seed( const uint32 oneSeed ); + void seed( uint32 *const bigSeed, const uint32 seedLength = N ); + void seed(); + + // Saving and loading generator state + void save( uint32* saveArray ) const; // to array of size SAVE + void load( uint32 *const loadArray ); // from such array + friend std::ostream& operator<<( std::ostream& os, const MTRand& mtrand ); + friend std::istream& operator>>( std::istream& is, MTRand& mtrand ); + +protected: + void initialize( const uint32 oneSeed ); + void reload(); + uint32 hiBit( const uint32& u ) const { return u & 0x80000000UL; } + uint32 loBit( const uint32& u ) const { return u & 0x00000001UL; } + uint32 loBits( const uint32& u ) const { return u & 0x7fffffffUL; } + uint32 mixBits( const uint32& u, const uint32& v ) const + { return hiBit(u) | loBits(v); } + uint32 twist( const uint32& m, const uint32& s0, const uint32& s1 ) const + { return m ^ (mixBits(s0,s1)>>1) ^ (-loBit(s1) & 0x9908b0dfUL); } + static uint32 hash( time_t t, clock_t c ); +}; + + +inline MTRand::MTRand( const uint32& oneSeed ) + { seed(oneSeed); } + +inline MTRand::MTRand( uint32 *const bigSeed, const uint32 seedLength ) + { seed(bigSeed,seedLength); } + +inline MTRand::MTRand() + { seed(); } + +inline double MTRand::rand() + { return double(randInt()) * (1.0/4294967295.0); } + +inline double MTRand::rand( const double& n ) + { return rand() * n; } + +inline double MTRand::randExc() + { return double(randInt()) * (1.0/4294967296.0); } + +inline double MTRand::randExc( const double& n ) + { return randExc() * n; } + +inline double MTRand::randDblExc() + { return ( double(randInt()) + 0.5 ) * (1.0/4294967296.0); } + +inline double MTRand::randDblExc( const double& n ) + { return randDblExc() * n; } + +inline double MTRand::rand53() +{ + uint32 a = randInt() >> 5, b = randInt() >> 6; + return ( a * 67108864.0 + b ) * (1.0/9007199254740992.0); // by Isaku Wada +} + +inline double MTRand::randNorm( const double& mean, const double& variance ) +{ + // Return a real number from a normal (Gaussian) distribution with given + // mean and variance by Box-Muller method + double r = sqrt( -2.0 * log( 1.0-randDblExc()) ) * variance; + double phi = 2.0 * 3.14159265358979323846264338328 * randExc(); + return mean + r * cos(phi); +} + +inline MTRand::uint32 MTRand::randInt() +{ + // Pull a 32-bit integer from the generator state + // Every other access function simply transforms the numbers extracted here + + if( left == 0 ) reload(); + --left; + + register uint32 s1; + s1 = *pNext++; + s1 ^= (s1 >> 11); + s1 ^= (s1 << 7) & 0x9d2c5680UL; + s1 ^= (s1 << 15) & 0xefc60000UL; + return ( s1 ^ (s1 >> 18) ); +} + +inline MTRand::uint32 MTRand::randInt( const uint32& n ) +{ + // Find which bits are used in n + // Optimized by Magnus Jonsson (magnus@smartelectronix.com) + uint32 used = n; + used |= used >> 1; + used |= used >> 2; + used |= used >> 4; + used |= used >> 8; + used |= used >> 16; + + // Draw numbers until one is found in [0,n] + uint32 i; + do + i = randInt() & used; // toss unused bits to shorten search + while( i > n ); + return i; +} + + +inline void MTRand::seed( const uint32 oneSeed ) +{ + // Seed the generator with a simple uint32 + initialize(oneSeed); + reload(); +} + + +inline void MTRand::seed( uint32 *const bigSeed, const uint32 seedLength ) +{ + // Seed the generator with an array of uint32's + // There are 2^19937-1 possible initial states. This function allows + // all of those to be accessed by providing at least 19937 bits (with a + // default seed length of N = 624 uint32's). Any bits above the lower 32 + // in each element are discarded. + // Just call seed() if you want to get array from /dev/urandom + initialize(19650218UL); + register int i = 1; + register uint32 j = 0; + register int k = ( N > seedLength ? N : seedLength ); + for( ; k; --k ) + { + state[i] = + state[i] ^ ( (state[i-1] ^ (state[i-1] >> 30)) * 1664525UL ); + state[i] += ( bigSeed[j] & 0xffffffffUL ) + j; + state[i] &= 0xffffffffUL; + ++i; ++j; + if( i >= N ) { state[0] = state[N-1]; i = 1; } + if( j >= seedLength ) j = 0; + } + for( k = N - 1; k; --k ) + { + state[i] = + state[i] ^ ( (state[i-1] ^ (state[i-1] >> 30)) * 1566083941UL ); + state[i] -= i; + state[i] &= 0xffffffffUL; + ++i; + if( i >= N ) { state[0] = state[N-1]; i = 1; } + } + state[0] = 0x80000000UL; // MSB is 1, assuring non-zero initial array + reload(); +} + + +inline void MTRand::seed() +{ + // Seed the generator with an array from /dev/urandom if available + // Otherwise use a hash of time() and clock() values + + // First try getting an array from /dev/urandom + FILE* urandom = fopen( "/dev/urandom", "rb" ); + if( urandom ) + { + uint32 bigSeed[N]; + register uint32 *s = bigSeed; + register int i = N; + register bool success = true; + while( success && i-- ) + success = fread( s++, sizeof(uint32), 1, urandom ); + fclose(urandom); + if( success ) { seed( bigSeed, N ); return; } + } + + // Was not successful, so use time() and clock() instead + seed( hash( time(NULL), clock() ) ); +} + + +inline void MTRand::initialize( const uint32 seed ) +{ + // Initialize generator state with seed + // See Knuth TAOCP Vol 2, 3rd Ed, p.106 for multiplier. + // In previous versions, most significant bits (MSBs) of the seed affect + // only MSBs of the state array. Modified 9 Jan 2002 by Makoto Matsumoto. + register uint32 *s = state; + register uint32 *r = state; + register int i = 1; + *s++ = seed & 0xffffffffUL; + for( ; i < N; ++i ) + { + *s++ = ( 1812433253UL * ( *r ^ (*r >> 30) ) + i ) & 0xffffffffUL; + r++; + } +} + + +inline void MTRand::reload() +{ + // Generate N new values in state + // Made clearer and faster by Matthew Bellew (matthew.bellew@home.com) + register uint32 *p = state; + register int i; + for( i = N - M; i--; ++p ) + *p = twist( p[M], p[0], p[1] ); + for( i = M; --i; ++p ) + *p = twist( p[M-N], p[0], p[1] ); + *p = twist( p[M-N], p[0], state[0] ); + + left = N, pNext = state; +} + + +inline MTRand::uint32 MTRand::hash( time_t t, clock_t c ) +{ + // Get a uint32 from t and c + // Better than uint32(x) in case x is floating point in [0,1] + // Based on code by Lawrence Kirby (fred@genesis.demon.co.uk) + + static uint32 differ = 0; // guarantee time-based seeds will change + + uint32 h1 = 0; + unsigned char *p = (unsigned char *) &t; + for( size_t i = 0; i < sizeof(t); ++i ) + { + h1 *= UCHAR_MAX + 2U; + h1 += p[i]; + } + uint32 h2 = 0; + p = (unsigned char *) &c; + for( size_t j = 0; j < sizeof(c); ++j ) + { + h2 *= UCHAR_MAX + 2U; + h2 += p[j]; + } + return ( h1 + differ++ ) ^ h2; +} + + +inline void MTRand::save( uint32* saveArray ) const +{ + register uint32 *sa = saveArray; + register const uint32 *s = state; + register int i = N; + for( ; i--; *sa++ = *s++ ) {} + *sa = left; +} + + +inline void MTRand::load( uint32 *const loadArray ) +{ + register uint32 *s = state; + register uint32 *la = loadArray; + register int i = N; + for( ; i--; *s++ = *la++ ) {} + left = *la; + pNext = &state[N-left]; +} + + +inline std::ostream& operator<<( std::ostream& os, const MTRand& mtrand ) +{ + register const MTRand::uint32 *s = mtrand.state; + register int i = mtrand.N; + for( ; i--; os << *s++ << "\t" ) {} + return os << mtrand.left; +} + + +inline std::istream& operator>>( std::istream& is, MTRand& mtrand ) +{ + register MTRand::uint32 *s = mtrand.state; + register int i = mtrand.N; + for( ; i--; is >> *s++ ) {} + is >> mtrand.left; + mtrand.pNext = &mtrand.state[mtrand.N-mtrand.left]; + return is; +} +}; + +#endif // MERSENNETWISTER_H + +// Change log: +// +// v0.1 - First release on 15 May 2000 +// - Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus +// - Translated from C to C++ +// - Made completely ANSI compliant +// - Designed convenient interface for initialization, seeding, and +// obtaining numbers in default or user-defined ranges +// - Added automatic seeding from /dev/urandom or time() and clock() +// - Provided functions for saving and loading generator state +// +// v0.2 - Fixed bug which reloaded generator one step too late +// +// v0.3 - Switched to clearer, faster reload() code from Matthew Bellew +// +// v0.4 - Removed trailing newline in saved generator format to be consistent +// with output format of built-in types +// +// v0.5 - Improved portability by replacing static const int's with enum's and +// clarifying return values in seed(); suggested by Eric Heimburg +// - Removed MAXINT constant; use 0xffffffffUL instead +// +// v0.6 - Eliminated seed overflow when uint32 is larger than 32 bits +// - Changed integer [0,n] generator to give better uniformity +// +// v0.7 - Fixed operator precedence ambiguity in reload() +// - Added access for real numbers in (0,1) and (0,n) +// +// v0.8 - Included time.h header to properly support time_t and clock_t +// +// v1.0 - Revised seeding to match 26 Jan 2002 update of Nishimura and Matsumoto +// - Allowed for seeding with arrays of any length +// - Added access for real numbers in [0,1) with 53-bit resolution +// - Added access for real numbers from normal (Gaussian) distributions +// - Increased overall speed by optimizing twist() +// - Doubled speed of integer [0,n] generation +// - Fixed out-of-range number generation on 64-bit machines +// - Improved portability by substituting literal constants for long enum's +// - Changed license from GNU LGPL to BSD diff --git a/src/sat/cryptominisat/Makefile b/src/sat/cryptominisat/Makefile new file mode 100644 index 0000000..ffbda1d --- /dev/null +++ b/src/sat/cryptominisat/Makefile @@ -0,0 +1,12 @@ +include ../../../scripts/Makefile.common +MTL = mtl +CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h) +EXEC = minisat +CFLAGS += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) +LFLAGS = -lz + +include mtl/template.mk +all: libminisat.a + ranlib libminisat.a + cp *.o ../ + cp libminisat.a ../ diff --git a/src/sat/cryptominisat/Solver.C b/src/sat/cryptominisat/Solver.C new file mode 100644 index 0000000..5559d75 --- /dev/null +++ b/src/sat/cryptominisat/Solver.C @@ -0,0 +1,1264 @@ +/****************************************************************************************[Solver.C] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 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 "Solver.h" +#include "Sort.h" +#include +#include +#include +#include +#include +#include "clause.h" + +namespace MINISAT +{ + +//================================================================================================= +// Constructor/Destructor: + + +Solver::Solver() : + // Parameters: (formerly in 'SearchParams') + var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) + , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1) + + // More parameters: + // + , expensive_ccmin (true) + , polarity_mode (polarity_user) + , verbosity (0) + , restrictedPickBranch(0) + , useRealUnknowns(false) + + // Statistics: (formerly in 'SolverStats') + // + , starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) + , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) + + , ok (true) + , cla_inc (1) + , var_inc (1) + , qhead (0) + , simpDB_assigns (-1) + , simpDB_props (0) + , order_heap (VarOrderLt(activity)) + , progress_estimate(0) + , remove_satisfied (true) + , mtrand((unsigned long int)0) + , logger(verbosity) + , dynamic_behaviour_analysis(false) //do not document the proof as default + , maxRestarts(UINT_MAX) + , learnt_clause_group(0) +{ +} + + +Solver::~Solver() +{ + for (int i = 0; i < learnts.size(); i++) free(learnts[i]); + for (int i = 0; i < unitary_learnts.size(); i++) free(unitary_learnts[i]); + for (int i = 0; i < clauses.size(); i++) free(clauses[i]); + for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]); +} + +//================================================================================================= +// Minor methods: + + +// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be +// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). +Var Solver::newVar(bool sign, bool dvar) +{ + int v = nVars(); + watches .push(); // (list for positive literal) + watches .push(); // (list for negative literal) + xorwatches.push(); // (list for variables in xors) + reason .push(NULL); + assigns .push(l_Undef); + level .push(-1); + activity .push(0); + seen .push(0); + polarity .push((char)sign); + + polarity .push((char)sign); + decision_var.push((char)dvar); + + insertVarOrder(v); + logger.new_var(v); + + return v; +} + +bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint group, const char* group_name) +{ + assert(decisionLevel() == 0); + + if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name); + + 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++) { + while (ps[i].var() >= nVars()) newVar(); + xor_clause_inverted ^= ps[i].sign(); + ps[i] ^= ps[i].sign(); + + if (ps[i] == p) { + //added, but easily removed + j--; + p = lit_Undef; + if (!assigns[ps[i].var()].isUndef()) + xor_clause_inverted ^= assigns[ps[i].var()].getBool(); + } else if (value(ps[i]) == l_Undef) //just add + ps[j++] = p = ps[i]; + else xor_clause_inverted ^= (value(ps[i]) == l_True); //modify xor_clause_inverted instead of adding + } + ps.shrink(i - j); + + if (ps.size() == 0) { + if (xor_clause_inverted) + return true; + + if (dynamic_behaviour_analysis) logger.empty_clause(group); + return ok = false; + } else if (ps.size() == 1) { + assert(value(ps[0]) == l_Undef); + uncheckedEnqueue( (xor_clause_inverted) ? ~ps[0] : ps[0]); + if (dynamic_behaviour_analysis) + logger.propagation((xor_clause_inverted) ? ~ps[0] : ps[0], Logger::addclause_type, group); + return ok = (propagate() == NULL); + } else { + learnt_clause_group = std::max(group+1, learnt_clause_group); + + XorClause* c = XorClause_new(ps, xor_clause_inverted, group); + + xorclauses.push(c); + attachClause(*c); + } + + return true; +} + +bool Solver::addClause(vec& ps, const uint group, const char* group_name) +{ + assert(decisionLevel() == 0); + + if (dynamic_behaviour_analysis) + logger.set_group_name(group, group_name); + + 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++) { + while (ps[i].var() >= nVars()) newVar(); + + 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) { + if (dynamic_behaviour_analysis) logger.empty_clause(group); + return ok = false; + } else if (ps.size() == 1) { + assert(value(ps[0]) == l_Undef); + uncheckedEnqueue(ps[0]); + if (dynamic_behaviour_analysis) + logger.propagation(ps[0], Logger::addclause_type, group); + return ok = (propagate() == NULL); + } else { + learnt_clause_group = std::max(group+1, learnt_clause_group); + + Clause* c = Clause_new(ps, group); + + clauses.push(c); + attachClause(*c); + } + + return true; +} + +void Solver::attachClause(XorClause& c) +{ + assert(c.size() > 1); + + xorwatches[c[0].var()].push(&c); + xorwatches[c[1].var()].push(&c); + + if (c.learnt()) learnts_literals += c.size(); + else clauses_literals += c.size(); +} + +void Solver::attachClause(Clause& c) +{ + assert(c.size() > 1); + + watches[(~c[0]).toInt()].push(&c); + watches[(~c[1]).toInt()].push(&c); + + if (c.learnt()) learnts_literals += c.size(); + else clauses_literals += c.size(); +} + + +void Solver::detachClause(const XorClause& c) +{ + assert(c.size() > 1); + assert(find(xorwatches[c[0].var()], &c)); + assert(find(xorwatches[c[1].var()], &c)); + remove(xorwatches[c[0].var()], &c); + remove(xorwatches[c[1].var()], &c); + + if (c.learnt()) learnts_literals -= c.size(); + else clauses_literals -= c.size(); +} + +void Solver::detachClause(const Clause& c) +{ + assert(c.size() > 1); + assert(find(watches[(~c[0]).toInt()], &c)); + assert(find(watches[(~c[1]).toInt()], &c)); + remove(watches[(~c[0]).toInt()], &c); + remove(watches[(~c[1]).toInt()], &c); + if (c.learnt()) learnts_literals -= c.size(); + else clauses_literals -= c.size(); +} + +template +void Solver::removeClause(T& c) +{ + detachClause(c); + free(&c); +} + + +bool Solver::satisfied(const Clause& c) const +{ + for (uint i = 0; i < c.size(); i++) + if (value(c[i]) == l_True) + return true; + return false; +} + +bool Solver::satisfied(const XorClause& c) const +{ + bool final = c.xor_clause_inverted(); + for (uint k = 0; k < c.size(); k++ ) { + const lbool& val = assigns[c[k].var()]; + if (val.isUndef()) return false; + final ^= val.getBool(); + } + return final; +} + + +// Revert to the state at given level (keeping all assignment at 'level' but not beyond). +// +void Solver::cancelUntil(int level) +{ + #ifdef VERBOSE_DEBUG + cout << "Canceling until level " << level; + if (level > 0) cout << " sublevel: " << trail_lim[level]; + cout << endl; + #endif + + if (decisionLevel() > level) { + for (int c = trail.size()-1; c >= trail_lim[level]; c--) { + Var x = trail[c].var(); + #ifdef VERBOSE_DEBUG + cout << "Canceling var " << x+1 << " sublevel:" << c << endl; + #endif + assigns[x] = l_Undef; + insertVarOrder(x); + } + qhead = trail_lim[level]; + trail.shrink(trail.size() - trail_lim[level]); + trail_lim.shrink(trail_lim.size() - level); + } + + #ifdef VERBOSE_DEBUG + cout << "Canceling finished. (now at level: " << decisionLevel() << " sublevel:" << trail.size()-1 << ")" << endl; + #endif +} + +//Permutates the clauses in the solver. Very useful to calcuate the average time it takes the solver to solve the prolbem +void Solver::permutateClauses() +{ + for (int i = 0; i < clauses.size(); i++) { + int j = mtrand.randInt(i); + Clause* tmp = clauses[i]; + clauses[i] = clauses[j]; + clauses[j] = tmp; + } + + for (int i = 0; i < xorclauses.size(); i++) { + int j = mtrand.randInt(i); + XorClause* tmp = xorclauses[i]; + xorclauses[i] = xorclauses[j]; + xorclauses[j] = tmp; + } +} + +void Solver::setRealUnknown(const uint var) +{ + if (realUnknowns.size() < var+1) + realUnknowns.resize(var+1, false); + realUnknowns[var] = true; +} + +void Solver::printLit(const Lit l) const +{ + printf("%s%d:%c", l.sign() ? "-" : "", l.var()+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X')); +} + + +void Solver::printClause(const Clause& c) const +{ + printf("(group: %d) ", c.group); + for (uint i = 0; i < c.size();) { + printLit(c[i]); + i++; + if (i < c.size()) printf(" "); + } +} + +void Solver::printClause(const XorClause& c) const +{ + printf("(group: %d) ", c.group); + if (c.xor_clause_inverted()) printf(" /inverted/ "); + for (uint i = 0; i < c.size();) { + printLit(c[i].unsign()); + i++; + if (i < c.size()) printf(" + "); + } +} + +//================================================================================================= +// Major methods: + + +Lit Solver::pickBranchLit(int polarity_mode) +{ + #ifdef VERBOSE_DEBUG + cout << "decision level:" << decisionLevel() << " "; + #endif + + Var next = var_Undef; + + // Random decision: + if (mtrand.randDblExc() < random_var_freq && !order_heap.empty()) { + if (restrictedPickBranch == 0) next = order_heap[mtrand.randInt(order_heap.size()-1)]; + else next = order_heap[mtrand.randInt(std::min((uint32_t)order_heap.size()-1, restrictedPickBranch))]; + + if (assigns[next] == l_Undef && decision_var[next]) + rnd_decisions++; + } + + // Activity based decision: + //bool dont_do_bad_decision = false; + //if (restrictedPickBranch != 0) dont_do_bad_decision = (mtrand.randInt(100) != 0); + while (next == var_Undef || assigns[next] != l_Undef || !decision_var[next]) + if (order_heap.empty()) { + next = var_Undef; + break; + } else { + next = order_heap.removeMin(); + } + + bool sign = false; + switch (polarity_mode) { + case polarity_true: + sign = false; + break; + case polarity_false: + sign = true; + break; + case polarity_user: + if (next != var_Undef) + sign = polarity[next]; + break; + case polarity_rnd: + sign = mtrand.randInt(1); + break; + default: + assert(false); + } + + assert(next == var_Undef || value(next) == l_Undef); + + if (next == var_Undef) { + #ifdef VERBOSE_DEBUG + cout << "SAT!" << endl; + #endif + return lit_Undef; + } else { + Lit lit(next,sign); + #ifdef VERBOSE_DEBUG + cout << "decided on: " << lit.var()+1 << " to set:" << !lit.sign() << endl; + #endif + return lit; + } +} + + +/*_________________________________________________________________________________________________ +| +| 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'. +| +| Effect: +| Will undo part of the trail, upto but not beyond the assumption of the current decision level. +|________________________________________________________________________________________________@*/ +void Solver::analyze(Clause* 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; + out_btlevel = 0; + + do { + assert(confl != NULL); // (otherwise should be UIP) + Clause& c = *confl; + + if (c.learnt()) + claBumpActivity(c); + + for (uint j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) { + const Lit& q = c[j]; + const uint my_var = q.var(); + + if (!seen[my_var] && level[my_var] > 0) { + if (!useRealUnknowns || (my_var < realUnknowns.size() && realUnknowns[my_var])) + varBumpActivity(my_var); + seen[my_var] = 1; + if (level[my_var] >= decisionLevel()) + pathC++; + else { + out_learnt.push(q); + if (level[my_var] > out_btlevel) + out_btlevel = level[my_var]; + } + } + } + + // Select next clause to look at: + while (!seen[trail[index--].var()]); + p = trail[index+1]; + confl = reason[p.var()]; + seen[p.var()] = 0; + pathC--; + + } while (pathC > 0); + out_learnt[0] = ~p; + + // Simplify conflict clause: + // + int i, j; + if (expensive_ccmin) { + uint32_t abstract_level = 0; + for (i = 1; i < out_learnt.size(); i++) + abstract_level |= abstractLevel(out_learnt[i].var()); // (maintain an abstraction of levels involved in conflict) + + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++) + if (reason[out_learnt[i].var()] == NULL || !litRedundant(out_learnt[i], abstract_level)) + out_learnt[j++] = out_learnt[i]; + } else { + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++) { + const Clause& c = *reason[out_learnt[i].var()]; + for (uint k = 1; k < c.size(); k++) + if (!seen[c[k].var()] && level[c[k].var()] > 0) { + out_learnt[j++] = out_learnt[i]; + break; + } + } + } + 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; + for (int i = 2; i < out_learnt.size(); i++) + if (level[out_learnt[i].var()] > level[out_learnt[max_i].var()]) + max_i = i; + Lit p = out_learnt[max_i]; + out_learnt[max_i] = out_learnt[1]; + out_learnt[1] = p; + out_btlevel = level[p.var()]; + } + + + for (int j = 0; j < analyze_toclear.size(); j++) seen[analyze_toclear[j].var()] = 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::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[analyze_stack.last().var()] != NULL); + const Clause& c = *reason[analyze_stack.last().var()]; + analyze_stack.pop(); + + for (uint i = 1; i < c.size(); i++) { + Lit p = c[i]; + if (!seen[p.var()] && level[p.var()] > 0) { + if (reason[p.var()] != NULL && (abstractLevel(p.var()) & abstract_levels) != 0) { + seen[p.var()] = 1; + analyze_stack.push(p); + analyze_toclear.push(p); + } else { + for (int j = top; j < analyze_toclear.size(); j++) + seen[analyze_toclear[j].var()] = 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::analyzeFinal(Lit p, vec& out_conflict) +{ + out_conflict.clear(); + out_conflict.push(p); + + if (decisionLevel() == 0) + return; + + seen[p.var()] = 1; + + for (int i = trail.size()-1; i >= trail_lim[0]; i--) { + Var x = trail[i].var(); + if (seen[x]) { + if (reason[x] == NULL) { + assert(level[x] > 0); + out_conflict.push(~trail[i]); + } else { + const Clause& c = *reason[x]; + for (uint j = 1; j < c.size(); j++) + if (level[c[j].var()] > 0) + seen[c[j].var()] = 1; + } + seen[x] = 0; + } + } + + seen[p.var()] = 0; +} + + +void Solver::uncheckedEnqueue(Lit p, Clause* from) +{ + #ifdef VERBOSE_DEBUG + cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel:" << trail.size() << endl; + #endif + + assert(value(p) == l_Undef); + const Var v = p.var(); + assigns [v] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient + level [v] = decisionLevel(); + reason [v] = from; + polarity[p.var()] = p.sign(); + trail.push(p); +} + + +/*_________________________________________________________________________________________________ +| +| propagate : [void] -> [Clause*] +| +| Description: +| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, +| otherwise NULL. +| +| Post-conditions: +| * the propagation queue is empty, even if there was a conflict. +|________________________________________________________________________________________________@*/ +Clause* Solver::propagate(const bool xor_as_well) +{ + Clause* confl = NULL; + int num_props = 0; + + #ifdef VERBOSE_DEBUG + cout << "Propagation started" << endl; + #endif + + while (qhead < trail.size()) { + Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. + vec& ws = watches[p.toInt()]; + Clause **i, **j, **end; + num_props++; + + #ifdef VERBOSE_DEBUG + cout << "Propagating lit " << (p.sign() ? '-' : ' ') << p.var()+1 << endl; + #endif + + for (i = j = ws.getData(), end = i + ws.size(); i != end;) { + Clause& c = **i++; + + // Make sure the false literal is data[1]: + const Lit false_lit(~p); + if (c[0] == false_lit) + c[0] = c[1], c[1] = false_lit; + + assert(c[1] == false_lit); + + // If 0th watch is true, then clause is already satisfied. + const Lit& first = c[0]; + if (value(first) == l_True) { + *j++ = &c; + } else { + // Look for new watch: + for (uint k = 2; k < c.size(); k++) + if (value(c[k]) != l_False) { + c[1] = c[k]; + c[k] = false_lit; + watches[(~c[1]).toInt()].push(&c); + goto FoundWatch; + } + + // Did not find watch -- clause is unit under assignment: + *j++ = &c; + if (value(first) == l_False) { + confl = &c; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } else { + uncheckedEnqueue(first, &c); + if (dynamic_behaviour_analysis) + logger.propagation(first,Logger::simple_propagation_type,c.group); + } + } +FoundWatch: + ; + } + ws.shrink(i - j); + + if (xor_as_well && !confl) confl = propagate_xors(p); + } + propagations += num_props; + simpDB_props -= num_props; + + #ifdef VERBOSE_DEBUG + cout << "Propagation ended." << endl; + #endif + + return confl; +} + +Clause* Solver::propagate_xors(const Lit& p) +{ + #ifdef VERBOSE_DEBUG_XOR + cout << "Xor-Propagating variable " << p.var()+1 << endl; + #endif + + Clause* confl = NULL; + + vec& ws = xorwatches[p.var()]; + XorClause **i, **j, **end; + for (i = j = ws.getData(), end = i + ws.size(); i != end;) { + XorClause& c = **i++; + + // Make sure the false literal is data[1]: + if (c[0].var() == p.var()) { + Lit tmp(c[0]); + c[0] = c[1]; + c[1] = tmp; + } + assert(c[1].var() == p.var()); + + #ifdef VERBOSE_DEBUG_XOR + cout << "--> xor thing -- " << endl; + printClause(c); + cout << endl; + #endif + bool final = c.xor_clause_inverted(); + for (int k = 0, size = c.size(); k < size; k++ ) { + const lbool& val = assigns[c[k].var()]; + if (val.isUndef() && k >= 2) { + Lit tmp(c[1]); + c[1] = c[k]; + c[k] = tmp; + #ifdef VERBOSE_DEBUG_XOR + cout << "new watch set" << endl << endl; + #endif + xorwatches[c[1].var()].push(&c); + goto FoundWatch; + } + + c[k] = c[k].unsign() ^ val.getBool(); + final ^= val.getBool(); + } + + + { + // Did not find watch -- clause is unit under assignment: + *j++ = &c; + + #ifdef VERBOSE_DEBUG_XOR + cout << "final: " << std::boolalpha << final << " - "; + #endif + if (assigns[c[0].var()].isUndef()) { + c[0] = c[0].unsign()^final; + + #ifdef VERBOSE_DEBUG_XOR + cout << "propagating "; + printLit(c[0]); + cout << endl; + cout << "propagation clause -- "; + printClause(*(Clause*)&c); + cout << endl << endl; + #endif + + uncheckedEnqueue(c[0], (Clause*)&c); + if (dynamic_behaviour_analysis) + logger.propagation(c[0], Logger::simple_propagation_type, c.group); + } else if (!final) { + + #ifdef VERBOSE_DEBUG_XOR + printf("conflict clause -- "); + printClause(*(Clause*)&c); + cout << endl << endl; + #endif + + confl = (Clause*)&c; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } else { + #ifdef VERBOSE_DEBUG_XOR + printf("xor satisfied\n"); + #endif + + Lit tmp(c[0]); + c[0] = c[1]; + c[1] = tmp; + } + } +FoundWatch: + ; + } + ws.shrink(i - j); + + 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 { + bool operator () (Clause* x, Clause* y) { + return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); + } +}; +void Solver::reduceDB() +{ + int i, j; + double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity + + sort(learnts, reduceDB_lt()); + for (i = j = 0; i < learnts.size() / 2; i++) { + if (learnts[i]->size() > 2 && !locked(*learnts[i])) + removeClause(*learnts[i]); + else + learnts[j++] = learnts[i]; + } + for (; i < learnts.size(); i++) { + if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim) + removeClause(*learnts[i]); + else + learnts[j++] = learnts[i]; + } + learnts.shrink(i - j); +} + +const vec& Solver::get_sorted_learnts() +{ + sort(learnts, reduceDB_lt()); + return learnts; +} + +const vec& Solver::get_unitary_learnts() const +{ + return unitary_learnts; +} + +void Solver::setMaxRestarts(const uint num) +{ + maxRestarts = num; +} + +template +void Solver::removeSatisfied(vec& cs) +{ + int i,j; + for (i = j = 0; i < cs.size(); i++) { + if (satisfied(*cs[i])) + removeClause(*cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); +} + +void Solver::cleanClauses(vec& cs) +{ + uint useful = 0; + for (int s = 0; s < cs.size(); s++) { + Clause& c = *cs[s]; + Lit *i, *j, *end; + uint at = 0; + for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { + if (value(*i) == l_Undef) { + *j = *i; + j++; + } else assert(at > 1); + assert(value(*i) != l_True); + } + c.shrink(i-j); + if (i-j > 0) useful++; + } + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(Clause) useful:" << useful << endl; + #endif +} + +void Solver::cleanClauses(vec& cs) +{ + uint useful = 0; + for (int s = 0; s < cs.size(); s++) { + XorClause& c = *cs[s]; + Lit *i, *j, *end; + uint at = 0; + for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { + const lbool& val = assigns[i->var()]; + if (val.isUndef()) { + *j = *i; + j++; + } else /*assert(at>1),*/ c.invert(val.getBool()); + } + c.shrink(i-j); + if (i-j > 0) useful++; + } + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(XorClause) useful:" << useful << endl; + #endif +} + +/*_________________________________________________________________________________________________ +| +| 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. +|________________________________________________________________________________________________@*/ +lbool Solver::simplify() +{ + assert(decisionLevel() == 0); + + if (!ok || propagate() != NULL) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + ok = false; + return l_False; + } + + if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) { + return l_Undef; + } + + // Remove satisfied clauses: + removeSatisfied(learnts); + if (remove_satisfied) { // Can be turned off. + removeSatisfied(clauses); + removeSatisfied(xorclauses); + } + + // Remove fixed variables from the variable heap: + order_heap.filter(VarFilter(*this)); + + simpDB_assigns = nAssigns(); + simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) + + //cleanClauses(clauses); + cleanClauses(xorclauses); + //cleanClauses(learnts); + + return l_Undef; +} + + +/*_________________________________________________________________________________________________ +| +| search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] +| +| Description: +| Search for a model the specified number of conflicts, keeping the number of learnt clauses +| below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to +| 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::search(int nof_conflicts, int nof_learnts) +{ + assert(ok); + int conflictC = 0; + vec learnt_clause; + llbool ret; + + starts++; + + if (dynamic_behaviour_analysis) logger.begin(); + + for (;;) { + Clause* confl = propagate(); + + if (confl != NULL) { + ret = handle_conflict(learnt_clause, confl, conflictC); + if (ret != l_Nothing) return ret; + } else { + ret = new_decision(nof_conflicts, nof_learnts, conflictC); + if (ret != l_Nothing) return ret; + } + } +} + +llbool Solver::new_decision(int& nof_conflicts, int& nof_learnts, int& conflictC) +{ + if (nof_conflicts >= 0 && conflictC >= nof_conflicts) { + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + if (dynamic_behaviour_analysis) { + logger.end(Logger::restarting); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_Undef; + } + + // Simplify the set of problem clauses: + if (decisionLevel() == 0 && simplify() == l_False) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_False; + } + + if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_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(); + if (dynamic_behaviour_analysis) logger.propagation(p, Logger::assumption_type); + } else if (value(p) == l_False) { + analyzeFinal(~p, conflict); + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_False; + } else { + next = p; + break; + } + } + + if (next == lit_Undef) { + // New variable decision: + decisions++; + next = pickBranchLit(polarity_mode); + + if (next == lit_Undef) { + // Model found: + if (dynamic_behaviour_analysis) { + logger.end(Logger::model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_True; + } + } + + // Increase decision level and enqueue 'next' + assert(value(next) == l_Undef); + newDecisionLevel(); + uncheckedEnqueue(next); + if (dynamic_behaviour_analysis) logger.propagation(next, Logger::guess_type); + + return l_Nothing; +} + +llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conflictC) +{ + #ifdef VERBOSE_DEBUG + cout << "Handling conflict: "; + for (uint i = 0; i < learnt_clause.size(); i++) + cout << learnt_clause[i].var()+1 << ","; + cout << endl; + #endif + + int backtrack_level; + + conflicts++; + conflictC++; + if (decisionLevel() == 0) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_False; + } + learnt_clause.clear(); + analyze(confl, learnt_clause, backtrack_level); + cancelUntil(backtrack_level); + if (dynamic_behaviour_analysis) + logger.conflict(Logger::simple_confl_type, backtrack_level, confl->group, learnt_clause); + + #ifdef VERBOSE_DEBUG + cout << "Learning:"; + for (uint i = 0; i < learnt_clause.size(); i++) printLit(learnt_clause[i]), cout << " "; + cout << endl; + cout << "reverting var " << learnt_clause[0].var()+1 << " to " << !learnt_clause[0].sign() << endl; + #endif + + assert(value(learnt_clause[0]) == l_Undef); + //Unitary learnt + if (learnt_clause.size() == 1) { + Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true); + unitary_learnts.push(c); + uncheckedEnqueue(learnt_clause[0]); + if (dynamic_behaviour_analysis) + logger.propagation(learnt_clause[0], Logger::learnt_unit_clause_type); + assert(backtrack_level == 0 && "Unit clause learnt, so must cancel until level 0, right?"); + + #ifdef VERBOSE_DEBUG + cout << "Unit clause learnt." << endl; + #endif + //Normal learnt + } else { + Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true); + learnts.push(c); + attachClause(*c); + claBumpActivity(*c); + uncheckedEnqueue(learnt_clause[0], c); + + if (dynamic_behaviour_analysis) { + logger.propagation(learnt_clause[0], Logger::revert_guess_type, c->group); + logger.new_group(c->group); + logger.set_group_name(c->group, "learnt clause"); + } + } + + varDecayActivity(); + claDecayActivity(); + + return l_Nothing; +} + + +double Solver::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(); +} + + +lbool Solver::solve(const vec& assumps) +{ + model.clear(); + conflict.clear(); + + if (!ok) return l_False; + + assumps.copyTo(assumptions); + + double nof_conflicts = restart_first; + double nof_learnts = nClauses() * learntsize_factor; + 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: + while (status == l_Undef && starts < maxRestarts) { + if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100), fflush(stdout); + printf("\n"); + } + status = search((int)nof_conflicts, (int)nof_learnts); + nof_conflicts *= restart_inc; + nof_learnts *= learntsize_inc; + } + + if (verbosity >= 1) { + printf("==============================================================================="); + printf("\n"); + } + + if (status == l_True) { + // Extend & copy model: + model.growTo(nVars()); + for (int i = 0; i < nVars(); i++) model[i] = value(i); +#ifndef NDEBUG + verifyModel(); +#endif + } if (status == l_False) { + if (conflict.size() == 0) + ok = false; + } + + cancelUntil(0); + return status; +} + +//================================================================================================= +// Debug methods: + + +void Solver::verifyModel() +{ + bool failed = false; + for (int i = 0; i < clauses.size(); i++) { + Clause& c = *clauses[i]; + for (uint j = 0; j < c.size(); j++) + if (modelValue(c[j]) == l_True) + goto next; + + printf("unsatisfied clause: "); + printClause(*clauses[i]); + printf("\n"); + failed = true; +next: + ; + } + + for (int i = 0; i < xorclauses.size(); i++) { + XorClause& c = *xorclauses[i]; + bool final = c.xor_clause_inverted(); + for (uint j = 0; j < c.size(); j++) + final ^= (modelValue(c[j].unsign()) == l_True); + if (!final) { + printf("unsatisfied clause: "); + printClause(*xorclauses[i]); + printf("\n"); + failed = true; + } + } + + assert(!failed); + + printf("Verified %d original clauses.\n", clauses.size() + xorclauses.size()); +} + + +void Solver::checkLiteralCount() +{ + // Check that sizes are calculated correctly: + int cnt = 0; + for (int i = 0; i < clauses.size(); i++) + cnt += clauses[i]->size(); + + for (int i = 0; i < xorclauses.size(); i++) + cnt += xorclauses[i]->size(); + + if ((int)clauses_literals != cnt) { + fprintf(stderr, "literal count: %d, real value = %d\n", (int)clauses_literals, cnt); + assert((int)clauses_literals == cnt); + } +} +}; diff --git a/src/sat/cryptominisat/Solver.h b/src/sat/cryptominisat/Solver.h new file mode 100644 index 0000000..b5a2d78 --- /dev/null +++ b/src/sat/cryptominisat/Solver.h @@ -0,0 +1,431 @@ +/****************************************************************************************[Solver.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 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. +**************************************************************************************************/ + +#ifndef Solver_h +#define Solver_h + +#include +#include "mtl/Vec.h" +#include "mtl/Heap.h" +#include "mtl/Alg.h" +#include "Logger.h" +#include "MTRand/MersenneTwister.h" +#include "SolverTypes.h" +#include "clause.h" +#include + +#ifdef _MSC_VER + #include +#else + #include + #include + #include +#endif + +namespace MINISAT +{ + +//#define VERBOSE_DEBUG_XOR +//#define VERBOSE_DEBUG + +//================================================================================================= +// Solver -- the main class: + + +class Solver +{ +public: + + // Constructor/Destructor: + // + Solver(); + ~Solver(); + + // Problem specification: + // + Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. + bool addClause (vec& ps, const uint group, const char* group_name); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! + bool addXorClause (vec& ps, bool xor_clause_inverted, const uint group, const char* group_name); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! + + // Solving: + // + lbool simplify (); // Removes already satisfied clauses. + lbool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. + lbool solve (); // Search without assumptions. + bool okay () const; // FALSE means solver is in a conflicting state + + // 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. + void setSeed (const uint32_t seed); // Sets the seed to be the given number + void permutateClauses(); // Permutates the clauses using the seed. It updates the seed in mtrand + void needRealUnknowns(); // Uses the "real unknowns" set by setRealUnknown + void setRealUnknown(const uint var); //sets a variable to be 'real', i.e. to preferentially branch on it during solving (when useRealUnknown it turned on) + void setMaxRestarts(const uint num); //sets the maximum number of restarts to given value + + // Read state: + // + lbool value (const Var& x) const; // The current value of a variable. + lbool value (const Lit& p) const; // The current value of a literal. + lbool modelValue (const 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. + + // 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: + // + double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95) + double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999) + double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) + 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) + bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE) + int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false) + int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0) + uint restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all]) + bool useRealUnknowns; // Whether 'real unknown' optimization should be used. If turned on, VarActivity is only bumped for variables for which the real_unknowns[var] == true + vector realUnknowns; // The important variables. This vector stores 'false' at realUnknowns[var] if the var is not a real unknown, and stores a 'true' if it is a real unkown. If var is larger than realUnkowns.size(), then it is not an important variable + + enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 }; + + // Statistics: (read-only member variable) + // + uint64_t starts, decisions, rnd_decisions, propagations, conflicts; + uint64_t clauses_literals, learnts_literals, max_literals, tot_literals; + + //Logging + void needStats(); // Prepares the solver to output statistics + void needProofGraph(); // Prepares the solver to output proof graphs during solving + void setVariableName(int var, const char* name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger') + void startClauseAdding(); // Before adding clauses, but after setting up the Solver (need* functions, verbosity), this should be called + void endFirstSimplify(); // After the clauses are added, and the first simplify() is called, this must be called + const vec& get_sorted_learnts(); //return the set of learned clauses + const vec& get_unitary_learnts() const; //return the set of unitary learned clauses + +protected: + // Helper structures: + // + struct VarOrderLt { + const vec& activity; + bool operator () (Var x, Var y) const { + return activity[x] > activity[y]; + } + VarOrderLt(const vec& act) : activity(act) { } + }; + + friend class VarFilter; + struct VarFilter { + const Solver& s; + VarFilter(const Solver& _s) : s(_s) {} + bool operator()(Var v) const { + return s.assigns[v].isUndef() && s.decision_var[v]; + } + }; + + // 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 xorclauses; // List of problem xor-clauses. + vec learnts; // List of learnt clauses. + vec unitary_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. + vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + vec > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses. + vec assigns; // The current assignments + vec polarity; // The preferred polarity of each variable. + vec decision_var; // 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 reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + vec level; // 'level[var]' contains the level at which the assignment was made. + 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'. + MTRand mtrand; // random number generator + Logger logger; // dynamic logging, statistics + bool dynamic_behaviour_analysis; //should 'logger' be called whenever a propagation/conflict/decision is made? + uint maxRestarts; // More than this number of restarts will not be performed + + // 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; + + //Logging + uint learnt_clause_group; //the group number of learnt clauses. Incremented at each added learnt clause + + // Main internal methods: + // + void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. + Lit pickBranchLit (int polarity_mode); // Return the next decision variable. + void newDecisionLevel (); // Begins a new decision level. + void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined. + bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. + Clause* propagate (const bool xor_as_well = true); // Perform unit propagation. Returns possibly conflicting clause. + Clause* propagate_xors (const Lit& p); + void cancelUntil (int level); // Backtrack until a certain level. + void analyze (Clause* 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, int nof_learnts); // Search for a given number of conflicts. + void reduceDB (); // Reduce the set of learnt clauses. + template + void removeSatisfied (vec& cs); // Shrink 'cs' to contain only non-satisfied clauses. + void cleanClauses (vec& cs); + void cleanClauses (vec& cs); // Remove TRUE or FALSE variables from the xor clauses and remove the FALSE variables from the normal clauses + llbool handle_conflict (vec& learnt_clause, Clause* confl, int& conflictC);// Handles the conflict clause + llbool new_decision (int& nof_conflicts, int& nof_learnts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made + + // Maintaining Variable/Clause activity: + // + void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead. + 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 (XorClause& c); + void attachClause (Clause& c); // Attach a clause to watcher lists. + void detachClause (const XorClause& c); + void detachClause (const Clause& c); // Detach a clause to watcher lists. + template + void removeClause(T& c); // 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 XorClause& c) const; // Returns TRUE if the clause is satisfied in the current state + bool satisfied (const Clause& c) const; // Returns TRUE if the clause is satisfied in the current state. + + // Misc: + // + int decisionLevel () const; // Gives the current decisionlevel. + uint32_t abstractLevel (const Var& x) const; // Used to represent an abstraction of sets of decision levels. + double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... + + // Debug: + void printLit (const Lit l) const; + void printClause (const Clause& c) const; + void printClause (const XorClause& c) const; + void verifyModel (); + void checkLiteralCount(); +}; + + +//================================================================================================= +// Implementation of inline methods: + + +inline void Solver::insertVarOrder(Var x) +{ + if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); +} + +inline void Solver::varDecayActivity() +{ + var_inc *= var_decay; +} +inline void Solver::varBumpActivity(Var v) +{ + if ( (activity[v] += var_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::claDecayActivity() +{ + cla_inc *= clause_decay; +} +inline void Solver::claBumpActivity (Clause& c) +{ + if ( (c.activity() += cla_inc) > 1e20 ) { + // Rescale: + for (int i = 0; i < learnts.size(); i++) + learnts[i]->activity() *= 1e-20; + cla_inc *= 1e-20; + } +} + +inline bool Solver::enqueue (Lit p, Clause* from) +{ + return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); +} +inline bool Solver::locked (const Clause& c) const +{ + return reason[c[0].var()] == &c && value(c[0]) == l_True; +} +inline void Solver::newDecisionLevel() +{ + trail_lim.push(trail.size()); + #ifdef VERBOSE_DEBUG + std::cout << "New decision level:" << trail_lim.size() << std::endl; + #endif +} +inline int Solver::decisionLevel () const +{ + return trail_lim.size(); +} +inline uint32_t Solver::abstractLevel (const Var& x) const +{ + return 1 << (level[x] & 31); +} +inline lbool Solver::value (const Var& x) const +{ + return assigns[x]; +} +inline lbool Solver::value (const Lit& p) const +{ + return assigns[p.var()] ^ p.sign(); +} +inline lbool Solver::modelValue (const Lit& p) const +{ + return model[p.var()] ^ p.sign(); +} +inline int Solver::nAssigns () const +{ + return trail.size(); +} +inline int Solver::nClauses () const +{ + return clauses.size() + xorclauses.size(); +} +inline int Solver::nLearnts () const +{ + return learnts.size(); +} +inline int Solver::nVars () const +{ + return assigns.size(); +} +inline void Solver::setPolarity (Var v, bool b) +{ + polarity [v] = (char)b; +} +inline void Solver::setDecisionVar(Var v, bool b) +{ + decision_var[v] = (char)b; + if (b) { + insertVarOrder(v); + } +} +inline lbool Solver::solve () +{ + vec tmp; + return solve(tmp); +} +inline bool Solver::okay () const +{ + return ok; +} +inline void Solver::setSeed (const uint32_t seed) +{ + mtrand.seed(seed); // Set seed of the variable-selection and clause-permutation(if applicable) +} +inline void Solver::needStats() +{ + dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate statistics + logger.statistics_on = true; +} +inline void Solver::needProofGraph() +{ + dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate proof graphs during solving + logger.proof_graph_on = true; +} +inline void Solver::setVariableName(int var, const char* name) +{ + while (var >= nVars()) newVar(); + logger.set_variable_name(var, name); +} // Sets the varible 'var'-s name to 'name' in the logger +inline void Solver::startClauseAdding() +{ + if (dynamic_behaviour_analysis) logger.begin(); // Needs to be called before adding any clause +} +inline void Solver::endFirstSimplify() +{ + if (dynamic_behaviour_analysis) logger.end(Logger::done_adding_clauses); // Needs to be called before adding any clause +} +inline void Solver::needRealUnknowns() +{ + useRealUnknowns = true; +} + + +//================================================================================================= +// Debug + etc: + +static inline void logLit(FILE* f, Lit l) +{ + fprintf(f, "%sx%d", l.sign() ? "~" : "", l.var()+1); +} + +static inline void logLits(FILE* f, const vec& ls) +{ + fprintf(f, "[ "); + if (ls.size() > 0) { + logLit(f, ls[0]); + for (int i = 1; i < ls.size(); i++) { + fprintf(f, ", "); + logLit(f, ls[i]); + } + } + fprintf(f, "] "); +} + +static inline const char* showBool(bool b) +{ + return b ? "true" : "false"; +} + + +// Just like 'assert()' but expression will be evaluated in the release version as well. +static inline void check(bool expr) +{ + assert(expr); +} + +}; + +//================================================================================================= +#endif diff --git a/src/sat/cryptominisat/SolverTypes.h b/src/sat/cryptominisat/SolverTypes.h new file mode 100644 index 0000000..7031e8c --- /dev/null +++ b/src/sat/cryptominisat/SolverTypes.h @@ -0,0 +1,166 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 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. +**************************************************************************************************/ +#ifndef SolverTypes_h +#define SolverTypes_h + +#include +#include +#include "mtl/Alg.h" + + +namespace MINISAT +{ +//================================================================================================= +// Variables, literals, lifted booleans, clauses: + + +// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, +// so that they can be used as array indices. + +typedef uint32_t Var; +#define var_Undef (0xffffffffU >>1) + +class Lit +{ + uint32_t x; + explicit Lit(uint32_t i) : x(i) { }; +public: + Lit() : x(2*var_Undef) {} // (lit_Undef) + explicit Lit(Var var, bool sign) : x((var+var) + (int)sign) { } + + const uint32_t& toInt() const { // Guarantees small, positive integers suitable for array indexing. + return x; + } + Lit operator~() const { + return Lit(x ^ 1); + } + Lit operator^(const bool b) const { + return Lit(x ^ b); + } + Lit& operator^=(const bool b) { + x ^= b; + return *this; + } + bool sign() const { + return x & 1; + } + Var var() const { + return x >> 1; + } + Lit unsign() const { + return Lit(x & ~1); + } + bool operator==(const Lit& p) const { + return x == p.x; + } + bool operator!= (const Lit& p) const { + return x != p.x; + } + bool operator < (const Lit& p) const { + return x < p.x; // '<' guarantees that p, ~p are adjacent in the ordering. + } +}; + +const Lit lit_Undef(var_Undef, false); // }- Useful special constants. +const Lit lit_Error(var_Undef, true ); // } + +//================================================================================================= +// Lifted booleans: + +class llbool; + +class lbool +{ + char value; + explicit lbool(char v) : value(v) { } + +public: + lbool() : value(0) { }; + inline char getchar() const { + return value; + } + inline lbool(llbool b); + + inline const bool isUndef() const { + return !value; + } + inline const bool isDef() const { + return value; + } + inline const bool getBool() const { + return (value+1) >> 1; + } + inline const bool operator==(lbool b) const { + return value == b.value; + } + inline const bool operator!=(lbool b) const { + return value != b.value; + } + lbool operator^(const bool b) const { + return lbool(value - value*2*b); + } + //lbool operator ^ (const bool b) const { return b ? lbool(-value) : lbool(value); } + + friend lbool toLbool(const char v); + friend lbool boolToLBool(const bool b); + friend class llbool; +}; +inline lbool toLbool(const char v) +{ + return lbool(v); +} +inline lbool boolToLBool(const bool b) +{ + return lbool(2*b-1); +} + +const lbool l_True = toLbool( 1); +const lbool l_False = toLbool(-1); +const lbool l_Undef = toLbool( 0); + + +class llbool +{ + char value; + +public: + llbool(): value(0) {}; + llbool(lbool v) : + value(v.value) {}; + llbool(char a) : + value(a) {} + + inline const bool operator!=(const llbool& v) const { + return (v.value != value); + } + + inline const bool operator==(const llbool& v) const { + return (v.value == value); + } + + friend class lbool; +}; +const llbool l_Nothing = toLbool(2); +const llbool l_Continue = toLbool(3); + +lbool::lbool(llbool b) : value(b.value) {}; +}; + +#endif diff --git a/src/sat/cryptominisat/clause.cpp b/src/sat/cryptominisat/clause.cpp new file mode 100644 index 0000000..23a699e --- /dev/null +++ b/src/sat/cryptominisat/clause.cpp @@ -0,0 +1,47 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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. +**************************************************************************************************/ + +#include "clause.h" + +namespace MINISAT +{ + +Clause* Clause_new(const vec& ps, const uint group, const bool learnt) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; +} + +Clause* Clause_new(const vector& ps, const uint group, const bool learnt) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; +} + +#ifdef USE_GAUSS +Clause* Clause_new(const mpz_class& ps, const vec& assigns, const vector& col_to_var_original, const uint group, const bool learnt) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, assigns, col_to_var_original, group, learnt); + return real; +} +#endif +} diff --git a/src/sat/cryptominisat/clause.h b/src/sat/cryptominisat/clause.h new file mode 100644 index 0000000..c7abb7b --- /dev/null +++ b/src/sat/cryptominisat/clause.h @@ -0,0 +1,160 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 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. +**************************************************************************************************/ + +#ifndef __clause_h__ +#define __clause_h__ + +#include +#include +#include +#include +#include "mtl/Vec.h" +#include "SolverTypes.h" + +namespace MINISAT +{ + +#ifndef uint +#define uint unsigned int +#endif + +using std::vector; + + +//================================================================================================= +// Clause -- a simple class for representing a clause: + + +class Clause +{ +public: + const uint group; +protected: + uint32_t size_etc; + float act; + Lit data[0]; + +public: + Clause(const vec& ps, const uint _group, const bool learnt) : + group(_group) { + size_etc = (ps.size() << 4) | (uint32_t)learnt ; + for (int i = 0; i < ps.size(); i++) data[i] = ps[i]; + if (learnt) act = 0; + } + + Clause(const vector& ps, const uint _group, const bool learnt) : + group(_group) { + size_etc = (ps.size() << 4) | (uint32_t)learnt ; + for (uint i = 0; i < ps.size(); i++) data[i] = ps[i]; + if (learnt) act = 0; + } + + // -- use this function instead: + friend Clause* Clause_new(const vec& ps, const uint group, const bool learnt = false); + friend Clause* Clause_new(const vector& ps, const uint group, const bool learnt = false); + + uint size () const { + return size_etc >> 4; + } + void shrink (uint i) { + assert(i <= size()); + size_etc = (((size_etc >> 4) - i) << 4) | (size_etc & 15); + } + void pop () { + shrink(1); + } + bool learnt () const { + return size_etc & 1; + } + uint32_t mark () const { + return (size_etc >> 1) & 3; + } + void mark (uint32_t m) { + size_etc = (size_etc & ~6) | ((m & 3) << 1); + } + + Lit& operator [] (uint32_t i) { + return data[i]; + } + const Lit& operator [] (uint32_t i) const { + return data[i]; + } + + float& activity () { + return act; + } + + Lit* getData () { + return data; + } + void print() { + Clause& c = *this; + printf("group: %d, size: %d, learnt:%d, lits:\"", c.group, c.size(), c.learnt()); + for (uint i = 0; i < c.size(); i++) { + if (c[i].sign()) printf("-"); + printf("%d ", c[i].var()); + } + printf("\"\n"); + } +}; + +class XorClause : public Clause +{ +public: + // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). + template + XorClause(const V& ps, const bool _xor_clause_inverted, const uint _group, const bool learnt) : + Clause(ps, _group, learnt) { + size_etc |= (((uint32_t)_xor_clause_inverted) << 3); + } + + // -- use this function instead: + template + friend XorClause* XorClause_new(const V& ps, const bool xor_clause_inverted, const uint group, const bool learnt = false) { + void* mem = malloc(sizeof(XorClause) + sizeof(Lit)*(ps.size())); + XorClause* real= new (mem) XorClause(ps, xor_clause_inverted, group, learnt); + return real; + } + + inline bool xor_clause_inverted() const { + return size_etc & 8; + } + inline void invert (bool b) { + size_etc ^= (uint32_t)b << 3; + } + + void print() { + Clause& c = *this; + printf("group: %d, size: %d, learnt:%d, lits:\"", c.group, c.size(), c.learnt()); + for (uint i = 0; i < c.size();) { + assert(!c[i].sign()); + printf("%d", c[i].var()); + i++; + if (i < c.size()) printf(" + "); + } + printf("\"\n"); + } +}; + +Clause* Clause_new(const vec& ps, const uint group, const bool learnt); +Clause* Clause_new(const vector& ps, const uint group, const bool learnt); +}; + +#endif diff --git a/src/sat/cryptominisat/fcopy.cpp b/src/sat/cryptominisat/fcopy.cpp new file mode 100644 index 0000000..79fd312 --- /dev/null +++ b/src/sat/cryptominisat/fcopy.cpp @@ -0,0 +1,51 @@ + +#include +#include +#include "fcopy.h" + + +namespace MINISAT +{ +#define BUFSZ 16000 + +int FileCopy ( const char *src, const char *dst ) +{ + char *buf; + FILE *fi; + FILE *fo; + unsigned amount; + unsigned written; + int result; + + buf = new char[BUFSZ]; + + fi = fopen( src, "rb" ); + fo = fopen( dst, "wb" ); + + result = COPY_OK; + if ((fi == NULL) || (fo == NULL) ) { + result = COPY_ERROR; + if (fi != NULL) fclose(fi); + if (fo != NULL) fclose(fo); + } + + if (result == COPY_OK) { + do { + amount = fread( buf, sizeof(char), BUFSZ, fi ); + if (amount) { + written = fwrite( buf, sizeof(char), amount, fo ); + if (written != amount) + result = COPY_ERROR; // out of disk space or some other disk err? + } + } // when amount read is < BUFSZ, copy + while ((result == COPY_OK) && (amount == BUFSZ)); + fclose(fi); + fclose(fo); + } + + delete[] buf; + + return(result); +} + +}; diff --git a/src/sat/cryptominisat/fcopy.h b/src/sat/cryptominisat/fcopy.h new file mode 100644 index 0000000..a1958eb --- /dev/null +++ b/src/sat/cryptominisat/fcopy.h @@ -0,0 +1,14 @@ +#ifndef __FCOPY_H__ +#define __FCOPY_H__ + +namespace MINISAT +{ + +#define COPY_ERROR -1 +#define COPY_OK 0 + +int FileCopy( const char *src, const char *dst ); + +}; + +#endif diff --git a/src/sat/cryptominisat/mtl/Alg.h b/src/sat/cryptominisat/mtl/Alg.h new file mode 100644 index 0000000..58fc50a --- /dev/null +++ b/src/sat/cryptominisat/mtl/Alg.h @@ -0,0 +1,62 @@ +/*******************************************************************************************[Alg.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 Alg_h +#define Alg_h + +namespace MINISAT +{ + +//================================================================================================= +// Useful functions on vectors + + +#if 1 +template +static inline void remove(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + assert(j < ts.size()); + for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; + ts.pop(); +} +#else +template +static inline void remove(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + assert(j < ts.size()); + ts[j] = ts.last(); + ts.pop(); +} +#endif + +template +static inline bool find(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + return j < ts.size(); +} + +}; + +#endif diff --git a/src/sat/cryptominisat/mtl/BasicHeap.h b/src/sat/cryptominisat/mtl/BasicHeap.h new file mode 100644 index 0000000..4a34e77 --- /dev/null +++ b/src/sat/cryptominisat/mtl/BasicHeap.h @@ -0,0 +1,102 @@ +/******************************************************************************************[Heap.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 BasicHeap_h +#define BasicHeap_h +#include "Vec.h" + + +namespace MINISAT +{ + +//================================================================================================= +// A heap implementation with support for decrease/increase key. + + +template +class BasicHeap { + Comp lt; + vec heap; // heap of ints + + // Index "traversal" functions + static inline int left (int i) { return i*2+1; } + static inline int right (int i) { return (i+1)*2; } + static inline int parent(int i) { return (i-1) >> 1; } + + inline void percolateUp(int i) + { + int x = heap[i]; + while (i != 0 && lt(x, heap[parent(i)])){ + heap[i] = heap[parent(i)]; + i = parent(i); + } + heap [i] = x; + } + + + inline void percolateDown(int i) + { + int x = heap[i]; + while (left(i) < heap.size()){ + int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); + if (!lt(heap[child], x)) break; + heap[i] = heap[child]; + i = child; + } + heap[i] = x; + } + + + bool heapProperty(int i) { + return i >= heap.size() + || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } + + + public: + BasicHeap(const C& c) : comp(c) { } + + int size () const { return heap.size(); } + bool empty () const { return heap.size() == 0; } + int operator[](int index) const { return heap[index+1]; } + void clear (bool dealloc = false) { heap.clear(dealloc); } + void insert (int n) { heap.push(n); percolateUp(heap.size()-1); } + + + int removeMin() { + int r = heap[0]; + heap[0] = heap.last(); + heap.pop(); + if (heap.size() > 1) percolateDown(0); + return r; + } + + + // DEBUG: consistency checking + bool heapProperty() { + return heapProperty(1); } + + + // COMPAT: should be removed + int getmin () { return removeMin(); } +}; + +}; + +//================================================================================================= +#endif diff --git a/src/sat/cryptominisat/mtl/BoxedVec.h b/src/sat/cryptominisat/mtl/BoxedVec.h new file mode 100644 index 0000000..3178856 --- /dev/null +++ b/src/sat/cryptominisat/mtl/BoxedVec.h @@ -0,0 +1,151 @@ +/*******************************************************************************************[Vec.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 BoxedVec_h +#define BoxedVec_h + +#include +#include +#include + +namespace MINISAT +{ + +//================================================================================================= +// Automatically resizable arrays +// +// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) + +template +class bvec { + + static inline int imin(int x, int y) { + int mask = (x-y) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + static inline int imax(int x, int y) { + int mask = (y-x) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + struct Vec_t { + int sz; + int cap; + T data[0]; + + static Vec_t* alloc(Vec_t* x, int size){ + x = (Vec_t*)realloc((void*)x, sizeof(Vec_t) + sizeof(T)*size); + x->cap = size; + return x; + } + + }; + + Vec_t* ref; + + static const int init_size = 2; + static int nextSize (int current) { return (current * 3 + 1) >> 1; } + static int fitSize (int needed) { int x; for (x = init_size; needed > x; x = nextSize(x)); return x; } + + void fill (int size) { + assert(ref != NULL); + for (T* i = ref->data; i < ref->data + size; i++) + new (i) T(); + } + + void fill (int size, const T& pad) { + assert(ref != NULL); + for (T* i = ref->data; i < ref->data + size; i++) + new (i) T(pad); + } + + // Don't allow copying (error prone): + altvec& operator = (altvec& other) { assert(0); } + altvec (altvec& other) { assert(0); } + +public: + void clear (bool dealloc = false) { + if (ref != NULL){ + for (int i = 0; i < ref->sz; i++) + (*ref).data[i].~T(); + + if (dealloc) { + free(ref); ref = NULL; + }else + ref->sz = 0; + } + } + + // Constructors: + altvec(void) : ref (NULL) { } + altvec(int size) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size); ref->sz = size; } + altvec(int size, const T& pad) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size, pad); ref->sz = size; } + ~altvec(void) { clear(true); } + + // Ownership of underlying array: + operator T* (void) { return ref->data; } // (unsafe but convenient) + operator const T* (void) const { return ref->data; } + + // Size operations: + int size (void) const { return ref != NULL ? ref->sz : 0; } + + void pop (void) { assert(ref != NULL && ref->sz > 0); int last = --ref->sz; ref->data[last].~T(); } + void push (const T& elem) { + int size = ref != NULL ? ref->sz : 0; + int cap = ref != NULL ? ref->cap : 0; + if (size == cap){ + cap = cap != 0 ? nextSize(cap) : init_size; + ref = Vec_t::alloc(ref, cap); + } + //new (&ref->data[size]) T(elem); + ref->data[size] = elem; + ref->sz = size+1; + } + + void push () { + int size = ref != NULL ? ref->sz : 0; + int cap = ref != NULL ? ref->cap : 0; + if (size == cap){ + cap = cap != 0 ? nextSize(cap) : init_size; + ref = Vec_t::alloc(ref, cap); + } + new (&ref->data[size]) T(); + ref->sz = size+1; + } + + void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); } + void shrink_(int nelems) { for (int i = 0; i < nelems; i++) pop(); } + void growTo (int size) { while (this->size() < size) push(); } + void growTo (int size, const T& pad) { while (this->size() < size) push(pad); } + void capacity (int size) { growTo(size); } + + const T& last (void) const { return ref->data[ref->sz-1]; } + T& last (void) { return ref->data[ref->sz-1]; } + + // Vector interface: + const T& operator [] (int index) const { return ref->data[index]; } + T& operator [] (int index) { return ref->data[index]; } + + void copyTo(altvec& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); } + void moveTo(altvec& dest) { dest.clear(true); dest.ref = ref; ref = NULL; } + +}; + +}; + +#endif diff --git a/src/sat/cryptominisat/mtl/Heap.h b/src/sat/cryptominisat/mtl/Heap.h new file mode 100644 index 0000000..6647a94 --- /dev/null +++ b/src/sat/cryptominisat/mtl/Heap.h @@ -0,0 +1,173 @@ +/******************************************************************************************[Heap.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 Heap_h +#define Heap_h + +#include "Vec.h" + +namespace MINISAT +{ + +//================================================================================================= +// A heap implementation with support for decrease/increase key. + + +template +class Heap { + Comp lt; + vec heap; // heap of ints + vec indices; // int -> index in heap + + // Index "traversal" functions + static inline int left (int i) { return i*2+1; } + static inline int right (int i) { return (i+1)*2; } + static inline int parent(int i) { return (i-1) >> 1; } + + + inline void percolateUp(int i) + { + int x = heap[i]; + while (i != 0 && lt(x, heap[parent(i)])){ + heap[i] = heap[parent(i)]; + indices[heap[i]] = i; + i = parent(i); + } + heap [i] = x; + indices[x] = i; + } + + + inline void percolateDown(int i) + { + int x = heap[i]; + while (left(i) < heap.size()){ + int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); + if (!lt(heap[child], x)) break; + heap[i] = heap[child]; + indices[heap[i]] = i; + i = child; + } + heap [i] = x; + indices[x] = i; + } + + + bool heapProperty (int i) const { + return i >= heap.size() + || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } + + + public: + Heap(const Comp& c) : lt(c) { } + + int size () const { return heap.size(); } + bool empty () const { return heap.size() == 0; } + bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; } + int operator[](int index) const { assert(index < heap.size()); return heap[index]; } + + void decrease (int n) { assert(inHeap(n)); percolateUp(indices[n]); } + + // RENAME WHEN THE DEPRECATED INCREASE IS REMOVED. + void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); } + + + void insert(int n) + { + indices.growTo(n+1, -1); + assert(!inHeap(n)); + + indices[n] = heap.size(); + heap.push(n); + percolateUp(indices[n]); + } + + + int removeMin() + { + int x = heap[0]; + heap[0] = heap.last(); + indices[heap[0]] = 0; + indices[x] = -1; + heap.pop(); + if (heap.size() > 1) percolateDown(0); + return x; + } + + + void clear(bool dealloc = false) + { + for (int i = 0; i < heap.size(); i++) + indices[heap[i]] = -1; +#ifdef NDEBUG + for (int i = 0; i < indices.size(); i++) + assert(indices[i] == -1); +#endif + heap.clear(dealloc); + } + + + // Fool proof variant of insert/decrease/increase + void update (int n) + { + if (!inHeap(n)) + insert(n); + else { + percolateUp(indices[n]); + percolateDown(indices[n]); + } + } + + + // Delete elements from the heap using a given filter function (-object). + // *** this could probaly be replaced with a more general "buildHeap(vec&)" method *** + template + void filter(const F& filt) { + int i,j; + for (i = j = 0; i < heap.size(); i++) + if (filt(heap[i])){ + heap[j] = heap[i]; + indices[heap[i]] = j++; + }else + indices[heap[i]] = -1; + + heap.shrink(i - j); + for (int i = heap.size() / 2 - 1; i >= 0; i--) + percolateDown(i); + + assert(heapProperty()); + } + + + // DEBUG: consistency checking + bool heapProperty() const { + return heapProperty(1); } + + + // COMPAT: should be removed + void setBounds (int n) { } + void increase (int n) { decrease(n); } + int getmin () { return removeMin(); } + +}; + +}; + +//================================================================================================= +#endif diff --git a/src/sat/cryptominisat/mtl/Map.h b/src/sat/cryptominisat/mtl/Map.h new file mode 100644 index 0000000..302069a --- /dev/null +++ b/src/sat/cryptominisat/mtl/Map.h @@ -0,0 +1,122 @@ +/*******************************************************************************************[Map.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 Map_h +#define Map_h + +#include +#include "Vec.h" + +namespace MINISAT +{ + +//================================================================================================= +// Default hash/equals functions +// + +template struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; +template struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; + +template struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; +template struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; + +//================================================================================================= +// Some primes +// + +static const int nprimes = 25; +static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 }; + +//================================================================================================= +// Hash table implementation of Maps +// + +template, class E = Equal > +class Map { + struct Pair { K key; D data; }; + + H hash; + E equals; + + vec* table; + int cap; + int size; + + // Don't allow copying (error prone): + Map& operator = (Map& other) { assert(0); } + Map (Map& other) { assert(0); } + + int32_t index (const K& k) const { return hash(k) % cap; } + void _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; } + void rehash () { + const vec* old = table; + + int newsize = primes[0]; + for (int i = 1; newsize <= cap && i < nprimes; i++) + newsize = primes[i]; + + table = new vec[newsize]; + + for (int i = 0; i < cap; i++){ + for (int j = 0; j < old[i].size(); j++){ + _insert(old[i][j].key, old[i][j].data); }} + + delete [] old; + + cap = newsize; + } + + + public: + + Map () : table(NULL), cap(0), size(0) {} + Map (const H& h, const E& e) : Map(), hash(h), equals(e) {} + ~Map () { delete [] table; } + + void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; } + bool peek (const K& k, D& d) { + if (size == 0) return false; + const vec& ps = table[index(k)]; + for (int i = 0; i < ps.size(); i++) + if (equals(ps[i].key, k)){ + d = ps[i].data; + return true; } + return false; + } + + void remove (const K& k) { + assert(table != NULL); + vec& ps = table[index(k)]; + int j = 0; + for (; j < ps.size() && !equals(ps[j].key, k); j++); + assert(j < ps.size()); + ps[j] = ps.last(); + ps.pop(); + } + + void clear () { + cap = size = 0; + delete [] table; + table = NULL; + } +}; + +}; + +#endif diff --git a/src/sat/cryptominisat/mtl/Queue.h b/src/sat/cryptominisat/mtl/Queue.h new file mode 100644 index 0000000..52f8fb2 --- /dev/null +++ b/src/sat/cryptominisat/mtl/Queue.h @@ -0,0 +1,87 @@ +/*****************************************************************************************[Queue.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 Queue_h +#define Queue_h + +#include "Vec.h" + +namespace MINISAT +{ + +//================================================================================================= + + +template +class Queue { + vec elems; + int first; + +public: + Queue(void) : first(0) { } + + void insert(T x) { elems.push(x); } + T peek () const { return elems[first]; } + void pop () { first++; } + + void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; } + int size(void) { return elems.size() - first; } + + //bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; } + + const T& operator [] (int index) const { return elems[first + index]; } + +}; + +//template +//class Queue { +// vec buf; +// int first; +// int end; +// +//public: +// typedef T Key; +// +// Queue() : buf(1), first(0), end(0) {} +// +// void clear () { buf.shrinkTo(1); first = end = 0; } +// int size () { return (end >= first) ? end - first : end - first + buf.size(); } +// +// T peek () { assert(first != end); return buf[first]; } +// void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } +// void insert(T elem) { // INVARIANT: buf[end] is always unused +// buf[end++] = elem; +// if (end == buf.size()) end = 0; +// if (first == end){ // Resize: +// vec tmp((buf.size()*3 + 1) >> 1); +// //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0); +// int i = 0; +// for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j]; +// for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j]; +// first = 0; +// end = buf.size(); +// tmp.moveTo(buf); +// } +// } +//}; + +}; + +//================================================================================================= +#endif diff --git a/src/sat/cryptominisat/mtl/Sort.h b/src/sat/cryptominisat/mtl/Sort.h new file mode 100644 index 0000000..76f168f --- /dev/null +++ b/src/sat/cryptominisat/mtl/Sort.h @@ -0,0 +1,94 @@ +/******************************************************************************************[Sort.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 Sort_h +#define Sort_h +#include "Vec.h" + +namespace MINISAT +{ +//================================================================================================= +// Some sorting algorithms for vec's + + +template +struct LessThan_default { + bool operator () (T x, T y) { return x < y; } +}; + + +template +void selectionSort(T* array, int size, LessThan lt) +{ + int i, j, best_i; + T tmp; + + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (lt(array[j], array[best_i])) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } +} +template static inline void selectionSort(T* array, int size) { + selectionSort(array, size, LessThan_default()); } + +template +void sort(T* array, int size, LessThan lt) +{ + if (size <= 15) + selectionSort(array, size, lt); + + else{ + T pivot = array[size / 2]; + T tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(lt(array[i], pivot)); + do j--; while(lt(pivot, array[j])); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sort(array , i , lt); + sort(&array[i], size-i, lt); + } +} +template static inline void sort(T* array, int size) { + sort(array, size, LessThan_default()); } + + +//================================================================================================= +// For 'vec's: + + +template void sort(vec& v, LessThan lt) { + sort(v.getData(), v.size(), lt); } +template void sort(vec& v) { + sort(v, LessThan_default()); } + +}; +//================================================================================================= +#endif diff --git a/src/sat/cryptominisat/mtl/Vec.h b/src/sat/cryptominisat/mtl/Vec.h new file mode 100644 index 0000000..a3c5fca --- /dev/null +++ b/src/sat/cryptominisat/mtl/Vec.h @@ -0,0 +1,135 @@ +/*******************************************************************************************[Vec.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 Vec_h +#define Vec_h +#include +#include +#include + +namespace MINISAT +{ +//================================================================================================= +// Automatically resizable arrays +// +// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) + +template +class vec { + T* data; + int sz; + int cap; + + void init(int size, const T& pad); + void grow(int min_cap); + + // Don't allow copying (error prone): + vec& operator = (vec& other) { assert(0); return *this; } + vec (vec& other) { assert(0); } + + static inline int imin(int x, int y) { + int mask = (x-y) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + static inline int imax(int x, int y) { + int mask = (y-x) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + +public: + // Types: + typedef int Key; + typedef T Datum; + + // Constructors: + vec(void) : data(NULL) , sz(0) , cap(0) { } + vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } + vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } + vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()') + ~vec(void) { clear(true); } + + // Ownership of underlying array: + T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; } + const T* getData() const {return data; } + T* getData() {return data; } + + // Size operations: + int size (void) const { return sz; } + void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } + void shrink_(int nelems) { assert(nelems <= sz); sz -= nelems; } + void pop (void) { sz--, data[sz].~T(); } + void growTo (int size); + void growTo (int size, const T& pad); + void clear (bool dealloc = false); + void capacity (int size) { grow(size); } + + // Stack interface: +#if 1 + void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; } + //void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; } + void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; } + void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } +#else + void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; } + void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; } +#endif + + const T& last (void) const { return data[sz-1]; } + T& last (void) { return data[sz-1]; } + + // Vector interface: + const T& operator [] (int index) const { return data[index]; } + T& operator [] (int index) { return data[index]; } + + + // Duplicatation (preferred instead): + void copyTo(vec& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); } + void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } +}; + +template +void vec::grow(int min_cap) { + if (min_cap <= cap) return; + if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2; + else do cap = (cap*3+1) >> 1; while (cap < min_cap); + data = (T*)realloc(data, cap * sizeof(T)); } + +template +void vec::growTo(int size, const T& pad) { + if (sz >= size) return; + grow(size); + for (int i = sz; i < size; i++) new (&data[i]) T(pad); + sz = size; } + +template +void vec::growTo(int size) { + if (sz >= size) return; + grow(size); + for (int i = sz; i < size; i++) new (&data[i]) T(); + sz = size; } + +template +void vec::clear(bool dealloc) { + if (data != NULL){ + for (int i = 0; i < sz; i++) data[i].~T(); + sz = 0; + if (dealloc) free(data), data = NULL, cap = 0; } } + +}; + +#endif diff --git a/src/sat/cryptominisat/mtl/template.mk b/src/sat/cryptominisat/mtl/template.mk new file mode 100644 index 0000000..565498f --- /dev/null +++ b/src/sat/cryptominisat/mtl/template.mk @@ -0,0 +1,94 @@ +## +## Template makefile for Standard, Profile, Debug, Release, and +## Release-static versions +## +## eg: "make rs" for a statically linked release version. "make d" +## for a debug version (no optimizations). "make" for the +## standard version (optimized, but with debug information and +## assertions active) + +CSRCS ?= $(wildcard *.C *.cpp) +CHDRS ?= $(wildcard *.h) +COBJS ?= $(addsuffix .o, $(basename $(CSRCS))) + +PCOBJS = $(addsuffix p, $(COBJS)) +DCOBJS = $(addsuffix d, $(COBJS)) +RCOBJS = $(addsuffix r, $(COBJS)) + +EXEC ?= $(notdir $(shell pwd)) +LIB ?= $(EXEC) + +CXX ?= g++ +CFLAGS ?= -Wall +LFLAGS ?= -Wall + +COPTIMIZE ?= -O3 + +.PHONY : s p d r rs lib libd clean + +s: $(EXEC) +p: $(EXEC)_profile +d: $(EXEC)_debug +r: $(EXEC)_release +rs: $(EXEC)_static +lib: lib$(LIB).a +libd: lib$(LIB)d.a +libp: lib$(LIB)p.a + +## Compile options +%.op: CFLAGS +=$(COPTIMIZE) -pg -ggdb -D NDEBUG -DEXT_HASH_MAP +%.od: CFLAGS +=-O0 -ggdb -D DEBUG # -D INVARIANTS +%.o: CFLAGS +=$(COPTIMIZE) -D NDEBUG + +## Link options +$(EXEC): LFLAGS := -ggdb $(LFLAGS) +$(EXEC)_profile: LFLAGS := -ggdb -pg $(LFLAGS) +$(EXEC)_debug: LFLAGS := -ggdb $(LFLAGS) +$(EXEC)_release: LFLAGS := $(LFLAGS) +$(EXEC)_static: LFLAGS := --static $(LFLAGS) + +## Dependencies +$(EXEC): $(COBJS) +$(EXEC)_profile: $(PCOBJS) +$(EXEC)_debug: $(DCOBJS) +$(EXEC)_release: $(RCOBJS) +$(EXEC)_static: $(RCOBJS) + +lib$(LIB).a: $(filter-out Main.or, $(COBJS)) +lib$(LIB)d.a: $(filter-out Main.od, $(DCOBJS)) +lib$(LIB)p.a: $(filter-out Main.op, $(PCOBJS)) + + +## Build rule +%.o %.op %.od: %.C %.cpp + @echo Compiling: "$@ ( $< )" + $(CXX) $(CFLAGS) -c -o $@ $< + +## Linking rules (standard/profile/debug/release) +$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static: + @echo Linking: "$@ ( $^ )" + @$(CXX) $^ $(LFLAGS) -o $@ + +## Library rule +lib$(LIB).a lib$(LIB)d.a lib$(LIB)p.a: + @echo Library: "$@ ( $^ )" + @rm -f $@ + @ar cq $@ $^ + +## Clean rule +clean: + @rm -f *~ $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \ + $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk depend.mak lib$(LIB).a \ + lib$(LIB)d.a lib$(LIB)p.a + +## Make dependencies +depend.mk: $(CSRCS) $(CHDRS) + @echo Making dependencies ... + @$(CXX) $(CFLAGS) -MM $(CSRCS) > depend.mk + @cp depend.mk /tmp/depend.mk.tmp + @sed "s/o:/op:/" /tmp/depend.mk.tmp >> depend.mk + @sed "s/o:/od:/" /tmp/depend.mk.tmp >> depend.mk + @sed "s/o:/or:/" /tmp/depend.mk.tmp >> depend.mk + @rm /tmp/depend.mk.tmp + +-include depend.mk -- 2.47.3