From 020faac03af55e45f09a9df5bed3e4bb028ef69c Mon Sep 17 00:00:00 2001 From: msoos Date: Fri, 16 Apr 2010 15:25:10 +0000 Subject: [PATCH] Removing CryptoMiniSat ver. 1 git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@685 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.in | 3 - src/STPManager/STP.cpp | 2 +- src/main/main.cpp | 2 +- src/sat/cryptominisat/AUTHORS | 10 - src/sat/cryptominisat/LICENSE | 21 - src/sat/cryptominisat/Logger.cpp | 748 ---------- src/sat/cryptominisat/Logger.h | 159 --- .../cryptominisat/MTRand/MersenneTwister.h | 427 ------ src/sat/cryptominisat/Makefile | 27 - src/sat/cryptominisat/Solver.cpp | 1265 ----------------- 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/sat.h | 5 - src/to-sat/ToCNF.cpp | 8 +- src/to-sat/ToSAT.cpp | 4 +- 27 files changed, 8 insertions(+), 4468 deletions(-) delete mode 100644 src/sat/cryptominisat/AUTHORS delete mode 100644 src/sat/cryptominisat/LICENSE delete mode 100644 src/sat/cryptominisat/Logger.cpp delete mode 100644 src/sat/cryptominisat/Logger.h delete mode 100644 src/sat/cryptominisat/MTRand/MersenneTwister.h delete mode 100644 src/sat/cryptominisat/Makefile delete mode 100644 src/sat/cryptominisat/Solver.cpp delete mode 100644 src/sat/cryptominisat/Solver.h delete mode 100644 src/sat/cryptominisat/SolverTypes.h delete mode 100644 src/sat/cryptominisat/clause.cpp delete mode 100644 src/sat/cryptominisat/clause.h delete mode 100644 src/sat/cryptominisat/fcopy.cpp delete mode 100644 src/sat/cryptominisat/fcopy.h delete mode 100644 src/sat/cryptominisat/mtl/Alg.h delete mode 100644 src/sat/cryptominisat/mtl/BasicHeap.h delete mode 100644 src/sat/cryptominisat/mtl/BoxedVec.h delete mode 100644 src/sat/cryptominisat/mtl/Heap.h delete mode 100644 src/sat/cryptominisat/mtl/Map.h delete mode 100644 src/sat/cryptominisat/mtl/Queue.h delete mode 100644 src/sat/cryptominisat/mtl/Sort.h delete mode 100644 src/sat/cryptominisat/mtl/Vec.h diff --git a/scripts/Makefile.in b/scripts/Makefile.in index fda3bc3..6812494 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -22,9 +22,6 @@ HEADERS=$(SRC)/c_interface/*.h .PHONY: all all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interface extlib-constbv extlib-abc -ifdef CRYPTOMINISAT - $(MAKE) -C $(SRC)/sat cryptominisat -endif ifdef CRYPTOMINISAT2 $(MAKE) -C $(SRC)/sat cryptominisat2 endif diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index d81daee..6e46846 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -21,7 +21,7 @@ namespace BEEV { bm->CreateNode(NOT, query)); //solver instantiated here -#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 +#if defined CRYPTOMINISAT2 MINISAT::Solver NewSolver; #endif diff --git a/src/main/main.cpp b/src/main/main.cpp index afae20b..a819c4a 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -129,7 +129,7 @@ int main(int argc, char ** argv) { helpstring += "-s : print function statistics\n"; - #if !defined CRYPTOMINISAT && !defined CRYPTOMINISAT2 + #if !defined CRYPTOMINISAT2 helpstring += "--simplifying-minisat : use simplifying-minisat rather than minisat\n"; #endif diff --git a/src/sat/cryptominisat/AUTHORS b/src/sat/cryptominisat/AUTHORS deleted file mode 100644 index 98599fa..0000000 --- a/src/sat/cryptominisat/AUTHORS +++ /dev/null @@ -1,10 +0,0 @@ -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 deleted file mode 100644 index beb0799..0000000 --- a/src/sat/cryptominisat/LICENSE +++ /dev/null @@ -1,21 +0,0 @@ -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.cpp b/src/sat/cryptominisat/Logger.cpp deleted file mode 100644 index 2bb52d0..0000000 --- a/src/sat/cryptominisat/Logger.cpp +++ /dev/null @@ -1,748 +0,0 @@ -/*********************************************************************************** -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 deleted file mode 100644 index 1fae9a7..0000000 --- a/src/sat/cryptominisat/Logger.h +++ /dev/null @@ -1,159 +0,0 @@ -/*********************************************************************************** -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 deleted file mode 100644 index 964ecc7..0000000 --- a/src/sat/cryptominisat/MTRand/MersenneTwister.h +++ /dev/null @@ -1,427 +0,0 @@ -// 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 deleted file mode 100644 index 416a7a4..0000000 --- a/src/sat/cryptominisat/Makefile +++ /dev/null @@ -1,27 +0,0 @@ -TOP = ../../.. -include $(TOP)/scripts/Makefile.common - -MTL = mtl -MTRAND = MTRand -SOURCES = Solver.cpp clause.cpp fcopy.cpp Logger.cpp -OBJECTS = $(SOURCES:.cpp=.o) -LIB = libminisat.a -CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c -EXEC = minisat -LFLAGS = -lz - -all: $(LIB) #$(EXEC) -lib: $(LIB) - -$(LIB): $(OBJECTS) - rm -f $@ - ar cq $@ $(OBJECTS) - ranlib $@ - cp $(LIB) ../ - cp $(OBJECTS) ../ - -clean: - rm -f $(OBJECTS) $(LIB) - -.cpp.o: - $(CC) $(CFLAGS) $< -o $@ diff --git a/src/sat/cryptominisat/Solver.cpp b/src/sat/cryptominisat/Solver.cpp deleted file mode 100644 index fb83029..0000000 --- a/src/sat/cryptominisat/Solver.cpp +++ /dev/null @@ -1,1265 +0,0 @@ -/****************************************************************************************[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 deleted file mode 100644 index b5a2d78..0000000 --- a/src/sat/cryptominisat/Solver.h +++ /dev/null @@ -1,431 +0,0 @@ -/****************************************************************************************[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 deleted file mode 100644 index 7031e8c..0000000 --- a/src/sat/cryptominisat/SolverTypes.h +++ /dev/null @@ -1,166 +0,0 @@ -/***********************************************************************************[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 deleted file mode 100644 index 23a699e..0000000 --- a/src/sat/cryptominisat/clause.cpp +++ /dev/null @@ -1,47 +0,0 @@ -/***********************************************************************************[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 deleted file mode 100644 index 3674b14..0000000 --- a/src/sat/cryptominisat/clause.h +++ /dev/null @@ -1,160 +0,0 @@ -/***********************************************************************************[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 deleted file mode 100644 index 79fd312..0000000 --- a/src/sat/cryptominisat/fcopy.cpp +++ /dev/null @@ -1,51 +0,0 @@ - -#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 deleted file mode 100644 index a1958eb..0000000 --- a/src/sat/cryptominisat/fcopy.h +++ /dev/null @@ -1,14 +0,0 @@ -#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 deleted file mode 100644 index 58fc50a..0000000 --- a/src/sat/cryptominisat/mtl/Alg.h +++ /dev/null @@ -1,62 +0,0 @@ -/*******************************************************************************************[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 deleted file mode 100644 index 4a34e77..0000000 --- a/src/sat/cryptominisat/mtl/BasicHeap.h +++ /dev/null @@ -1,102 +0,0 @@ -/******************************************************************************************[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 deleted file mode 100644 index 3178856..0000000 --- a/src/sat/cryptominisat/mtl/BoxedVec.h +++ /dev/null @@ -1,151 +0,0 @@ -/*******************************************************************************************[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 deleted file mode 100644 index 6647a94..0000000 --- a/src/sat/cryptominisat/mtl/Heap.h +++ /dev/null @@ -1,173 +0,0 @@ -/******************************************************************************************[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 deleted file mode 100644 index 302069a..0000000 --- a/src/sat/cryptominisat/mtl/Map.h +++ /dev/null @@ -1,122 +0,0 @@ -/*******************************************************************************************[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 deleted file mode 100644 index 52f8fb2..0000000 --- a/src/sat/cryptominisat/mtl/Queue.h +++ /dev/null @@ -1,87 +0,0 @@ -/*****************************************************************************************[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 deleted file mode 100644 index 76f168f..0000000 --- a/src/sat/cryptominisat/mtl/Sort.h +++ /dev/null @@ -1,94 +0,0 @@ -/******************************************************************************************[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 deleted file mode 100644 index a3c5fca..0000000 --- a/src/sat/cryptominisat/mtl/Vec.h +++ /dev/null @@ -1,135 +0,0 @@ -/*******************************************************************************************[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/sat.h b/src/sat/sat.h index bfd6c90..cd6e332 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -1,11 +1,6 @@ #ifndef SAT_H_ #define SAT_H_ -#ifdef CRYPTOMINISAT -#include "cryptominisat/Solver.h" -#include "cryptominisat/SolverTypes.h" -#endif - #ifdef CRYPTOMINISAT2 #include "cryptominisat2/Solver.h" #include "cryptominisat2/SolverTypes.h" diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 0af39f7..84d5ee6 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -485,7 +485,7 @@ namespace BEEV x = info[varphi]; } -#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 +#if defined CRYPTOMINISAT2 if(isXorChild) { setDoRenamePos(*x); @@ -638,7 +638,7 @@ namespace BEEV convertFormulaToCNFPosCases(varphi, defs); } -#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 +#if defined CRYPTOMINISAT2 if ((x->clausespos != NULL && (x->clausespos->size() > 1 || (renameAllSiblings @@ -1347,7 +1347,7 @@ namespace BEEV void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs) { -#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 +#if defined CRYPTOMINISAT2 ASTVec::const_iterator it = varphi.GetChildren().begin(); ClausePtr xor_clause = new vector(); @@ -1716,7 +1716,7 @@ namespace BEEV ClauseList* defs) { //#ifdef FALSE -#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 +#if defined CRYPTOMINISAT2 CNFInfo * xx = info[varphi]; if(NULL != xx && sharesPos(*xx) > 0 diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 70e68f6..8bf3f85 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -118,7 +118,7 @@ namespace BEEV // { // continue; // } -#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 +#if defined CRYPTOMINISAT2 if(add_xor_clauses) { newSolver.addXorClause(satSolverClause, false); @@ -333,7 +333,7 @@ namespace BEEV return sat; } -#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 +#if defined CRYPTOMINISAT2 if(!xorcl->empty()) { sat = toSATandSolve(SatSolver, *xorcl, true); -- 2.47.3