OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
#OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE
CFLAGS_BASE = $(OPTIMIZE)
-#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT
-#CRYPTOMINISAT = true
+CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT
+CRYPTOMINISAT = true
#CFLAGS_M32 = -m32
SHELL=/bin/bash
.PHONY: cryptominisat
cryptominisat:
- $(MAKE) -C cryptominisat
- cp cryptominisat/libminisat.a .
- cp cryptominisat/CMakeFiles/minisat.dir/Solver/*.o .
+ $(MAKE) -C cryptominisat lib all
.PHONY: clean
clean:
$(MAKE) -C core clean
$(MAKE) -C simp clean
$(MAKE) -C unsound clean
-ifdef CRYPTOMINISAT
$(MAKE) -C cryptominisat clean
-endif
+
--- /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
+include ../../../scripts/Makefile.common
+MTL = mtl
+CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h)
+EXEC = minisat
+CFLAGS += -I$(MTL) -Wall -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
#define SAT_H_
#ifdef CRYPTOMINISAT
-#include "cryptominisat/Solver/Solver.h"
-#include "cryptominisat/Solver/SolverTypes.h"
+#include "cryptominisat/Solver.h"
+#include "cryptominisat/SolverTypes.h"
#else
#include "core/Solver.h"
#include "core/SolverTypes.h"
projects / francis / stp.git / commitdiff