--- /dev/null
+Niklas Eén
+Niklas Sörensson
+Mate SOOS <mate.soos@inrialpes.fr>
+Karsten Nohl <honk98@web.de>
+
+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++
--- /dev/null
+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.
--- /dev/null
+/***********************************************************************************
+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 <time.h>
+#include <cstring>
+#include <algorithm>
+#include <vector>
+#include <iostream>
+#include <iomanip>
+#include <fstream>
+#include <sstream>
+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<Lit>& 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<pair<double, uint> > prop_ordered;
+ for (uint i = 0; i < depths_of_assigns_for_var.size(); i++) {
+ double avg = 0.0;
+ for (vector<uint>::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<pair<double, uint> > prop_ordered;
+ for (uint i = 0; i < depths_of_propagations_for_group.size(); i++) {
+ double avg = 0.0;
+ for (vector<uint>::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<pair<double, uint> > confl_ordered;
+ for (uint i = 0; i < depths_of_conflicts_for_group.size(); i++) {
+ double avg = 0.0;
+ for (vector<uint>::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<pair<uint, uint> > 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<pair<uint, uint> > 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<pair<uint, uint> > 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<class T>
+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<pair<double, uint> >& to_print) const
+{
+ uint i = 0;
+ typedef vector<pair<double, uint> >::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<pair<uint, uint> >& to_print) const
+{
+ uint i = 0;
+ typedef vector<pair<uint, uint> >::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<pair<double, uint> >& to_print) const
+{
+ uint i = 0;
+ for (vector<pair<double, uint> >::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<pair<uint, uint> >& to_print) const
+{
+ uint i = 0;
+ for (vector<pair<uint, uint> >::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<class T>
+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<uint, uint> range_stat;
+
+ for (map<uint, uint>::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<uint, uint>::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<uint>::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<vector<uint> >::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();
+}
+};
--- /dev/null
+/***********************************************************************************
+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 <stdio.h>
+#include <set>
+//#include <Vec.h>
+#include <vector>
+
+#include "mtl/Vec.h"
+#include "mtl/Heap.h"
+#include "mtl/Alg.h"
+#include "Logger.h"
+#include "SolverTypes.h"
+#include <string>
+#include <map>
+#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<Lit>& 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<Lit>& ps, const bool xor_clause, const uint group);
+
+ bool proof_graph_on;
+ bool statistics_on;
+private:
+ void print_groups(const vector<pair<uint, uint> >& to_print) const;
+ void print_groups(const vector<pair<double, uint> >& to_print) const;
+ void print_vars(const vector<pair<uint, uint> >& to_print) const;
+ void print_vars(const vector<pair<double, uint> >& 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<class T>
+ 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<class T>
+ 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<uint> 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<string> groupnames;
+ vector<string> varnames;
+
+ //confls and props grouped by clause groups
+ vector<uint> confls_by_group;
+ vector<uint> props_by_group;
+
+ //props and guesses grouped by vars
+ vector<uint> times_var_guessed;
+ vector<uint> times_var_propagated;
+
+ vector<uint> times_group_caused_conflict;
+ vector<uint> times_group_caused_propagation;
+
+ vector<vector<uint> > depths_of_propagations_for_group;
+ vector<vector<uint> > depths_of_conflicts_for_group;
+ vector<vector<uint> > depths_of_assigns_for_var;
+
+ //the distribution of branch depths. first = depth, second = number of occurances
+ map<uint, uint> branch_depth_distrib;
+
+ uint sum_conflict_depths;
+ uint no_conflicts;
+ uint no_decisions;
+ uint no_propagations;
+ vec<uint> decisions;
+ vec<uint> propagations;
+ uint sum_decisions_on_branches;
+ uint sum_propagations_on_branches;
+
+ //message display properties
+ const int& verbosity;
+};
+
+};
+#endif //__LOGGER_H__
--- /dev/null
+// 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 <iostream>
+#include <limits.h>
+#include <stdio.h>
+#include <time.h>
+#include <math.h>
+
+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
--- /dev/null
+include ../../../scripts/Makefile.common
+MTL = mtl
+CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h)
+EXEC = minisat
+CFLAGS += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32)
+LFLAGS = -lz
+
+include mtl/template.mk
+all: libminisat.a
+ ranlib libminisat.a
+ cp *.o ../
+ cp libminisat.a ../
--- /dev/null
+/****************************************************************************************[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 <cmath>
+#include <string.h>
+#include <algorithm>
+#include <limits.h>
+#include <vector>
+#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<Lit>& 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<Lit>& 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<class T>
+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<Lit>&) (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<Lit>& 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<Lit>& 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<Clause*>& 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<XorClause*>& 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<Clause*>& Solver::get_sorted_learnts()
+{
+ sort(learnts, reduceDB_lt());
+ return learnts;
+}
+
+const vec<Clause*>& Solver::get_unitary_learnts() const
+{
+ return unitary_learnts;
+}
+
+void Solver::setMaxRestarts(const uint num)
+{
+ maxRestarts = num;
+}
+
+template<class T>
+void Solver::removeSatisfied(vec<T*>& 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<Clause*>& 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<XorClause*>& 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<Lit> 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<Lit>& 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<Lit>& 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);
+ }
+}
+};
--- /dev/null
+/****************************************************************************************[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 <cstdio>
+#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 <string.h>
+
+#ifdef _MSC_VER
+ #include <ctime>
+#else
+ #include <sys/time.h>
+ #include <sys/resource.h>
+ #include <unistd.h>
+#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<Lit>& 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<Lit>& 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<Lit>& 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<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
+ vec<Lit> 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<bool> 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<Clause*>& get_sorted_learnts(); //return the set of learned clauses
+ const vec<Clause*>& get_unitary_learnts() const; //return the set of unitary learned clauses
+
+protected:
+ // Helper structures:
+ //
+ struct VarOrderLt {
+ const vec<double>& activity;
+ bool operator () (Var x, Var y) const {
+ return activity[x] > activity[y];
+ }
+ VarOrderLt(const vec<double>& 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<Clause*> clauses; // List of problem clauses.
+ vec<XorClause*> xorclauses; // List of problem xor-clauses.
+ vec<Clause*> learnts; // List of learnt clauses.
+ vec<Clause*> unitary_learnts; // List of learnt clauses.
+ double cla_inc; // Amount to bump next clause with.
+ vec<double> activity; // A heuristic measurement of the activity of a variable.
+ double var_inc; // Amount to bump next variable with.
+ vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+ vec<vec<XorClause*> > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses.
+ vec<lbool> assigns; // The current assignments
+ vec<char> polarity; // The preferred polarity of each variable.
+ vec<char> decision_var; // Declares if a variable is eligible for selection in the decision heuristic.
+ vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
+ vec<int32_t> trail_lim; // Separator indices for different decision levels in 'trail'.
+ vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
+ vec<int32_t> 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<Lit> assumptions; // Current set of assumptions provided to solve by the user.
+ Heap<VarOrderLt> 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<char> seen;
+ vec<Lit> analyze_stack;
+ vec<Lit> analyze_toclear;
+ vec<Lit> 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<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
+ void analyzeFinal (Lit p, vec<Lit>& 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<class T>
+ void removeSatisfied (vec<T*>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
+ void cleanClauses (vec<XorClause*>& cs);
+ void cleanClauses (vec<Clause*>& cs); // Remove TRUE or FALSE variables from the xor clauses and remove the FALSE variables from the normal clauses
+ llbool handle_conflict (vec<Lit>& 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<class T>
+ 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<Lit> 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<Lit>& 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
--- /dev/null
+/***********************************************************************************[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 <cassert>
+#include <stdint.h>
+#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
--- /dev/null
+/***********************************************************************************[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<Lit>& 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<Lit>& 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<lbool>& assigns, const vector<uint>& 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
+}
--- /dev/null
+/***********************************************************************************[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 <stdint.h>
+#include <cstdio>
+#include <vector>
+#include <sys/types.h>
+#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<Lit>& 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<Lit>& 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<Lit>& ps, const uint group, const bool learnt = false);
+ friend Clause* Clause_new(const vector<Lit>& 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<class V>
+ 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<class V>
+ 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<Lit>& ps, const uint group, const bool learnt);
+Clause* Clause_new(const vector<Lit>& ps, const uint group, const bool learnt);
+};
+
+#endif
--- /dev/null
+
+#include <stdio.h>
+#include <string.h>
+#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);
+}
+
+};
--- /dev/null
+#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
--- /dev/null
+/*******************************************************************************************[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<class V, class T>
+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<class V, class T>
+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<class V, class T>
+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
--- /dev/null
+/******************************************************************************************[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 Comp>
+class BasicHeap {
+ Comp lt;
+ vec<int> 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
--- /dev/null
+/*******************************************************************************************[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 <cstdlib>
+#include <cassert>
+#include <new>
+
+namespace MINISAT
+{
+
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T>
+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<T>& operator = (altvec<T>& other) { assert(0); }
+ altvec (altvec<T>& 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<T>& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); }
+ void moveTo(altvec<T>& dest) { dest.clear(true); dest.ref = ref; ref = NULL; }
+
+};
+
+};
+
+#endif
--- /dev/null
+/******************************************************************************************[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 Comp>
+class Heap {
+ Comp lt;
+ vec<int> heap; // heap of ints
+ vec<int> 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<int>&)" method ***
+ template <class F>
+ 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
--- /dev/null
+/*******************************************************************************************[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 <stdint.h>
+#include "Vec.h"
+
+namespace MINISAT
+{
+
+//=================================================================================================
+// Default hash/equals functions
+//
+
+template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
+template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
+
+template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
+template<class K> 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 K, class D, class H = Hash<K>, class E = Equal<K> >
+class Map {
+ struct Pair { K key; D data; };
+
+ H hash;
+ E equals;
+
+ vec<Pair>* table;
+ int cap;
+ int size;
+
+ // Don't allow copying (error prone):
+ Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); }
+ Map (Map<K,D,H,E>& 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<Pair>* old = table;
+
+ int newsize = primes[0];
+ for (int i = 1; newsize <= cap && i < nprimes; i++)
+ newsize = primes[i];
+
+ table = new vec<Pair>[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<Pair>& 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<Pair>& 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
--- /dev/null
+/*****************************************************************************************[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 T>
+class Queue {
+ vec<T> 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 T>
+//class Queue {
+// vec<T> 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<T> 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
--- /dev/null
+/******************************************************************************************[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<class T>
+struct LessThan_default {
+ bool operator () (T x, T y) { return x < y; }
+};
+
+
+template <class T, class LessThan>
+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 <class T> static inline void selectionSort(T* array, int size) {
+ selectionSort(array, size, LessThan_default<T>()); }
+
+template <class T, class LessThan>
+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 <class T> static inline void sort(T* array, int size) {
+ sort(array, size, LessThan_default<T>()); }
+
+
+//=================================================================================================
+// For 'vec's:
+
+
+template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {
+ sort(v.getData(), v.size(), lt); }
+template <class T> void sort(vec<T>& v) {
+ sort(v, LessThan_default<T>()); }
+
+};
+//=================================================================================================
+#endif
--- /dev/null
+/*******************************************************************************************[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 <cstdlib>
+#include <cassert>
+#include <new>
+
+namespace MINISAT
+{
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T>
+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<T>& operator = (vec<T>& other) { assert(0); return *this; }
+ vec (vec<T>& 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<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); }
+ void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
+};
+
+template<class T>
+void vec<T>::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<class T>
+void vec<T>::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<class T>
+void vec<T>::growTo(int size) {
+ if (sz >= size) return;
+ grow(size);
+ for (int i = sz; i < size; i++) new (&data[i]) T();
+ sz = size; }
+
+template<class T>
+void vec<T>::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
--- /dev/null
+##
+## Template makefile for Standard, Profile, Debug, Release, and
+## Release-static versions
+##
+## eg: "make rs" for a statically linked release version. "make d"
+## for a debug version (no optimizations). "make" for the
+## standard version (optimized, but with debug information and
+## assertions active)
+
+CSRCS ?= $(wildcard *.C *.cpp)
+CHDRS ?= $(wildcard *.h)
+COBJS ?= $(addsuffix .o, $(basename $(CSRCS)))
+
+PCOBJS = $(addsuffix p, $(COBJS))
+DCOBJS = $(addsuffix d, $(COBJS))
+RCOBJS = $(addsuffix r, $(COBJS))
+
+EXEC ?= $(notdir $(shell pwd))
+LIB ?= $(EXEC)
+
+CXX ?= g++
+CFLAGS ?= -Wall
+LFLAGS ?= -Wall
+
+COPTIMIZE ?= -O3
+
+.PHONY : s p d r rs lib libd clean
+
+s: $(EXEC)
+p: $(EXEC)_profile
+d: $(EXEC)_debug
+r: $(EXEC)_release
+rs: $(EXEC)_static
+lib: lib$(LIB).a
+libd: lib$(LIB)d.a
+libp: lib$(LIB)p.a
+
+## Compile options
+%.op: CFLAGS +=$(COPTIMIZE) -pg -ggdb -D NDEBUG -DEXT_HASH_MAP
+%.od: CFLAGS +=-O0 -ggdb -D DEBUG # -D INVARIANTS
+%.o: CFLAGS +=$(COPTIMIZE) -D NDEBUG
+
+## Link options
+$(EXEC): LFLAGS := -ggdb $(LFLAGS)
+$(EXEC)_profile: LFLAGS := -ggdb -pg $(LFLAGS)
+$(EXEC)_debug: LFLAGS := -ggdb $(LFLAGS)
+$(EXEC)_release: LFLAGS := $(LFLAGS)
+$(EXEC)_static: LFLAGS := --static $(LFLAGS)
+
+## Dependencies
+$(EXEC): $(COBJS)
+$(EXEC)_profile: $(PCOBJS)
+$(EXEC)_debug: $(DCOBJS)
+$(EXEC)_release: $(RCOBJS)
+$(EXEC)_static: $(RCOBJS)
+
+lib$(LIB).a: $(filter-out Main.or, $(COBJS))
+lib$(LIB)d.a: $(filter-out Main.od, $(DCOBJS))
+lib$(LIB)p.a: $(filter-out Main.op, $(PCOBJS))
+
+
+## Build rule
+%.o %.op %.od: %.C %.cpp
+ @echo Compiling: "$@ ( $< )"
+ $(CXX) $(CFLAGS) -c -o $@ $<
+
+## Linking rules (standard/profile/debug/release)
+$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
+ @echo Linking: "$@ ( $^ )"
+ @$(CXX) $^ $(LFLAGS) -o $@
+
+## Library rule
+lib$(LIB).a lib$(LIB)d.a lib$(LIB)p.a:
+ @echo Library: "$@ ( $^ )"
+ @rm -f $@
+ @ar cq $@ $^
+
+## Clean rule
+clean:
+ @rm -f *~ $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
+ $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk depend.mak lib$(LIB).a \
+ lib$(LIB)d.a lib$(LIB)p.a
+
+## Make dependencies
+depend.mk: $(CSRCS) $(CHDRS)
+ @echo Making dependencies ...
+ @$(CXX) $(CFLAGS) -MM $(CSRCS) > depend.mk
+ @cp depend.mk /tmp/depend.mk.tmp
+ @sed "s/o:/op:/" /tmp/depend.mk.tmp >> depend.mk
+ @sed "s/o:/od:/" /tmp/depend.mk.tmp >> depend.mk
+ @sed "s/o:/or:/" /tmp/depend.mk.tmp >> depend.mk
+ @rm /tmp/depend.mk.tmp
+
+-include depend.mk
projects / francis / stp.git / commitdiff