Commit 5956838a authored by Masahiko Sakai's avatar Masahiko Sakai

version1.02b

parent b15c685e
......@@ -35,6 +35,7 @@ Contains types, macros, and inline functions generally useful in a C++ program.
#include <climits>
#include <cfloat>
#include <new>
#include <string>
#include <map>
......@@ -214,6 +215,10 @@ inline bool operator < (const Pair<Fst, Snd>& x, const Pair<Fst, Snd>& y) {
return x.fst < y.fst ||
(!(y.fst < x.fst) && x.snd < y.snd); }
//template <class Fst, class Snd>
//inline bool less_fst (const Pair<Fst, Snd>& x, const Pair<Fst, Snd>& y) {
// return x.fst < y.fst; }
template <class Fst, class Snd>
inline Pair<Fst, Snd> Pair_new(const Fst& x, const Snd& y) {
return Pair<Fst, Snd>(x, y); }
......
......@@ -53,6 +53,12 @@ void dump(Formula f) {
}
void dump(const vec<int>& base)
{
for (int i = 0; i < base.size(); i++)
reportf("%d ", base[i]);
}
void dump(const vec<Lit>& ps, const vec<Int>& Cs)
{
assert(ps.size() == Cs.size());
......
......@@ -32,6 +32,7 @@ extern vec<cchar*>* debug_names;
void dump(Int num);
void dump(Lit p);
void dump(Formula f);
void dump(const vec<int>& base);
void dump(const vec<Lit>& ps, const vec<Int>& Cs);
void dump(const vec<Lit>& ps, const vec<Int>& Cs, const vec<int>& assigns);
void dump(const vec<Formula>& ps, const vec<Int>& Cs);
......
* #variable= 701 #constraint= 351
*
* Euclidean Cycle (EC) formula as constructed by
* Markstrom and described in the paper available at
* http://jsat.ewi.tudelft.nl/content/volume2/JSAT2_11_Markstrom.pdf .
* Generated by running graph2ec on grid5x70split.graph.
*
* VERTEX 1 : x_{1, 6} + x_{1, 2} + x_{1, 346} + x_{1, 5} = 2
*
+1 x1 +1 x2 +1 x3 +1 x4 = 2;
*
* VERTEX 1 : x_{1, 6} + x_{1, 2} + x_{1, 346} + x_{1, 5} = 2
+1 x5 +1 x6 +1 x7 +1 x2 = 2;
*
1 x1 -1 x2 1 x3 -1 x4 >= -1 ;
1 x1 -1 x2 1 x3 -1 x4 >= ~2 ;
c
c comments Max-SAT
c
p cnf 3 7
1 -2 0
-1 2 -3 0
-3 2 0
1 3 0
-1 -2 3 0
-1 2 3 0
-1 -2 -3 0
c
c comments Max-SAT
c
p wcnf 3 7 99
99 1 -2 0
99 -1 2 -3 0
1 -3 2 0
1 1 3 0
1 -1 -2 3 0
1 -1 2 3 0
1 -1 -2 -3 0
1 x1 -1 x2 1 x3 -1 x4 >= -1 ;
d x0 <=> 1 x1 >= 2 ;
1 x1 1 x2 2 x3 2 x4 = 3 ;
d x0 <=> 1 x1 >= 2 ;
c
c comments Max-SAT
c
p wcnf 3 7
2 1 -2 0
10 -1 2 -3 0
4 -3 2 0
30 1 3 0
2 -1 -2 3 0
c
1 -1 2 3 0
5 -1 -2 -3 0
c
c comments Max-SAT
c
p wcnf 3 7 99
99 1 -2 0
99 -1 2 -3 0
4 -3 2 0
30 1 3 0
2 -1 -2 3 0
1 -1 2 3 0
5 -1 -2 -3 0
......@@ -110,11 +110,13 @@ Lit Clausifier::polarityClausify(Formula f)
}else
#endif
result = Lit(index(f),sign(f));
}else if (vmapp.at(f) != lit_Undef && !s.varElimed(var(vmapp.at(f)))){
result = vmapp.at(f);
}else{
result = (vmapp.at(~f) != lit_Undef && !s.varElimed(var(vmapp.at(~f)))) ?
Lit(var(vmapp.at(~f))) : Lit(s.newVar(!opt_branch_pbvars));
}else if (vmapp.at(f) != lit_Undef &&
( !opt_simp_solver || !s.varElimed(var(vmapp.at(f))) ) ){
result = vmapp.at(f);
}else{
result = (vmapp.at(~f) != lit_Undef &&
(!opt_simp_solver || !s.varElimed(var(vmapp.at(~f)))) ) ?
Lit(var(vmapp.at(~f))) : Lit(s.newVar(!opt_branch_pbvars));
if (Bin_p(f)){
if (op(f) == op_And){
vec<Formula> conj;
......
......@@ -12,8 +12,13 @@ To make the BigNum version, type
make rs
To use them together (trying the faster 64-bit version first), use the script
gpw_script
-----
TIPS:
For compile error related to gmp.h, install libgmp3-dev library.
For compile error related to gmp.h, install libgmp3-dev gmp-devel library.
For compile error related to zlib.h, install zlib-devel library.
On FreeBSD, use gmake for make.
This diff is collapsed.
......@@ -21,6 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#define Main_h
#include "Int.h"
#include "Version.h"
#include "FEnv.h"
//=================================================================================================
......@@ -30,6 +32,11 @@ enum ConvertT { ct_Sorters, ct_Adders, ct_BDDs, ct_Mixed, ct_Mixed2, ct_Undef };
enum Command { cmd_Minimize, cmd_FirstSolution, cmd_AllSolutions, cmd_InterestSolutions, cmd_Soft };
enum GpwT { gt_none, gt_positive, gt_negative, gt_low, gt_high, gt_both };
// Controlling optimization
extern bool minimization_mode; // turned on after first SAT-solver execution
extern std::map<Pair< int, Pair< Interval<Int> , Interval<Int> > >, Pair<Pair< Interval<Int> , Interval<Int> >, Formula> > memo_bdd_conv_int_in_min_mode;
extern Map<Pair<int,Int>, Formula> memo_bdd_conv_in_min_mode;
// -- output options:
extern bool opt_satlive;
extern bool opt_ansi;
......@@ -37,11 +44,15 @@ extern char* opt_cnf;
extern int opt_verbosity;
extern bool opt_try;
extern bool opt_model_out;
extern bool opt_dimacs;
extern bool opt_eager_cl;
// -- solver options:
extern SolverT opt_solver;
extern bool opt_simp_solver;
extern ConvertT opt_convert;
extern ConvertT opt_convert_goal;
extern bool opt_convert_goal_reusing;
extern GpwT opt_convert_gpw;
extern bool opt_convert_bdd_monotonic;
//extern bool opt_convert_bdd_binary_decomposition;
......@@ -49,6 +60,7 @@ extern int opt_convert_bdd_decomposition;
extern bool opt_convert_bdd_interval;
extern bool opt_convert_bdd_increasing_order;
extern bool opt_convert_weak;
extern int opt_opt_base_method;
extern bool opt_or_detection;
extern bool opt_es1_detection;
extern bool opt_cc_detection;
......@@ -59,11 +71,13 @@ extern int opt_cc_thres;
extern double opt_bdd_thres;
extern double opt_sort_thres;
extern double opt_goal_bias;
extern int opt_max_bdd_cost;
extern int opt_bdd_max_const;
extern Int opt_goal;
extern Command opt_command;
//extern bool opt_binary_minimization;
extern int opt_minimization;
extern int opt_bin_coeff;
extern int opt_seq_thres;
extern bool opt_band_for_goal;
extern bool opt_goal_gcd;
extern bool opt_branch_pbvars;
......@@ -88,6 +102,7 @@ extern int stats_bdd_nodes;
extern int stats_es1_detection;
extern int stats_cc_detection;
extern double stats_cnf_coding_time;
extern double stats_opt_base_calc_time;
// -- debug:
extern bool opt_model_check;
......
......@@ -38,13 +38,14 @@ rx: WAY="release static / 64-bit integers"
s: CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG
p: CFLAGS+=$(COPTIMIZE) -pg -ggdb -D DEBUG
d: CFLAGS+=-O0 -ggdb -D DEBUG -D PARANOID -D NO_GMP
#d: CFLAGS+=-O0 -ggdb -D DEBUG -D PARANOID
#r: CFLAGS+=$(COPTIMIZE) -D NDEBUG
r: CFLAGS+=$(COPTIMIZE) -D ND_GMP
rs: CFLAGS+=$(COPTIMIZE)
#rx: CFLAGS+=$(COPTIMIZE) -D NDEBUG -D NO_GMP
rx: CFLAGS+=$(COPTIMIZE) -D NO_GMP
#d: CFLAGS+=-O0 -ggdb -D DEBUG -D PARANOID -D NO_GMP
d: CFLAGS+=-O0 -ggdb -D DEBUG -D PARANOID
r: CFLAGS+=$(COPTIMIZE) -D NDEBUG
#r: CFLAGS+=$(COPTIMIZE) -D ND_GMP
rs: CFLAGS+=$(COPTIMIZE) -D NDEBUG
#rs: CFLAGS+=$(COPTIMIZE) -D NO_GMP
rx: CFLAGS+=$(COPTIMIZE) -D NO_GMP -D NDEBUG
#rx: CFLAGS+=$(COPTIMIZE) -D NO_GMP
s: build $(EXEC)
p: build $(EXEC)_profile
......@@ -154,7 +155,7 @@ $(EXEC)_profile: $(PCOBJS)
$(EXEC)_debug: $(DCOBJS)
@echo Linking $@
@$(CXX) $(DCOBJS) $(LDFLAGS) -lz -ggdb -Wall -o $@
@$(CXX) $(DCOBJS) $(LDFLAGS) -lz -lgmp -ggdb -Wall -o $@
$(EXEC)_release: $(RCOBJS)
@echo Linking $@
......
This diff is collapsed.
/**************************************************************************[PbSolver_convertSort.C]
/**************************************************************************[OptimalBase.h]
Copyright (c) 2005-2010, Niklas Een, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
......@@ -21,13 +21,45 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#define OptimalBase_h
#include "PbSolver.h"
#include "Global.h"
//=================================================================================================
int CountKind_Sort(vec<Int>& seq);
enum OptBaseT { obt_digits, obt_comb, obt_kind };
void optimizeBase(vec<Int>& seq, int carry_ins, vec<Int>& rhs, int cost, vec<int>& base, int& cost_bestfound, vec<int>& base_bestfound);
// returns the cardinarity of the given sorted sequence as a set.
template <class T>
int CountKind_Sort(const vec<T>& seq)
{
assert(seq.size()>0);
int i,c=1;
for(i=0;i<(seq.size()-1);i++){
if(seq[i]!=seq[i+1])
c++;
}
return(c);
}
void optimizeBase(vec<Int>& seq, vec<Int>& rhs, int& cost_bestfound, vec<int>& base_bestfound);
template <class T>
int count_weighted_sort(const vec<T>& seq) // assuming seq is sorted
{
assert(seq.size() > 0);
double sum = 0;
int num_succ_dig = 1;
for(int i = 1; i < seq.size(); i++) {
if(seq[i-1] == seq[i])
num_succ_dig++;
else {
sum += 1.0 / (double)num_succ_dig;
num_succ_dig = 1;
}
}
sum += 1.0 / (double)num_succ_dig;
return (int)(sum*10);
}
//void optimizeBase(vec<Int>& seq, int carry_ins, vec<Int>& rhs, int cost, vec<int>& base, int& cost_bestfound, vec<int>& base_bestfound, bool carry_important);
void optimizeBase(vec<Int>& seq, vec<Int>& rhs, int& cost_bestfound, vec<int>& base_bestfound, OptBaseT obt);
#endif
......@@ -21,9 +21,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "File.h"
#include "Debug.h"
// For soft constraint handling
int n_defsofts=0;
vec<Lit> soft_goal_ps; vec<Int> soft_goal_Cs; // literls and coefficients for soft goal.
// For Dimacs format
bool wcnf_mode = false;
Int top_weight = Int_MAX;
//=================================================================================================
// Parser buffers (streams):
......@@ -91,7 +96,7 @@ The 'S' (Solver) parameter should implement:
template<class B>
static void skipWhitespace(B& in) { // not including newline
while (*in == ' ' || *in == '\t')
while (*in == ' ' || *in == '\t' || *in == '\r')
++in; }
template<class B>
......@@ -103,13 +108,15 @@ static void skipLine(B& in) {
template<class B>
static void skipComments(B& in) { // skip comment and empty lines (assuming we are at beginning of line)
// reportf("skipComments (%c)\n", *in);
while (*in == '*' || *in == '\n') skipLine(in); }
template<class B>
static bool skipEndOfLine(B& in) { // skip newline AND trailing comment/empty lines
//reportf("skipEndOfLine (%c)\n", *in);
skipWhitespace(in);
if (*in == '\n') ++in;
else return false;
skipComments(in);
return true; }
template<class B>
......@@ -217,19 +224,20 @@ void parseInterestVars(B& in, S& solver)
vec<Var> vs;
skipWhitespace(in);
if (*in == ';'){
++in;
++in; skipWhitespace(in);
skipLine(in);
}else{
vec<char> tmp;
for(;;){
skipWhitespace(in);
if (!('a' <= *in && *in <= 'z') && !('A' <= *in && *in <= 'Z')) break;
// if (!('a' <= *in && *in <= 'z') && !('A' <= *in && *in <= 'Z')) throw xstrdup("Invalid literal.");
vs.push(solver.getVar(parseIdent(in, tmp)));
}
skipWhitespace(in);
if (!skipText(in, ";")) throw xstrdup("Expecting ';' after variable sequence.");
}
skipEndOfLine(in);
//skipEndOfLine(in);
if (!skipEndOfLine(in)) throw xstrdup("Garbage after ';'.");
if(opt_verbosity >= 2) {
/**/reportf("interest vars: ");
......@@ -256,7 +264,8 @@ void parseGoal(B& in, S& solver, bool old_format)
skipWhitespace(in);
if (!skipText(in, ";")) throw xstrdup("Expecting ';' after goal function.");
}
skipEndOfLine(in);
//skipEndOfLine(in);
if (!skipEndOfLine(in)) throw xstrdup("Garbage after ';'.");
return;
} else if (!skipText(in, "min:")) return; // No goal specified. If file is syntactically correct, no characters will have been consumed (expecting integer).
......@@ -270,7 +279,8 @@ void parseGoal(B& in, S& solver, bool old_format)
skipWhitespace(in);
if (!skipText(in, ";")) throw xstrdup("Expecting ';' after goal function.");
}
skipEndOfLine(in);
//skipEndOfLine(in);
if (!skipEndOfLine(in)) throw xstrdup("Garbage after ';'.");
solver.addGoal(ps, Cs);
solver.addInterestVars(ps.size());
......@@ -308,8 +318,10 @@ bool parseConstrs(B& in, S& solver, bool old_format)
int ineq;
Int rhs;
while (*in != EOF){
Lit dlt1=lit_Undef,dlt2=lit_Undef;
Lit dlt1=lit_Undef,dlt2=lit_Undef; //reportf("(%c)",*in);
if (*in == '*' || *in == '\n') {skipComments(in); continue;}
if (*in == 'd') { // definition of constraint
Lit tl;
//**/ reportf("Definition detected");
++in;
skipWhitespace(in);
......@@ -317,13 +329,28 @@ bool parseConstrs(B& in, S& solver, bool old_format)
++in;
// dlp = new (xmalloc<Lit>(1))
// Lit(solver.getVar(parseIdent(in, tmp)),true);
dlt1 = Lit(solver.getVar(parseIdent(in, tmp)),true);
tl = Lit(solver.getVar(parseIdent(in, tmp)),true);
// } else dlp = new (xmalloc<Lit>(1))
// Lit(solver.getVar(parseIdent(in, tmp)));
} else dlt1 = Lit(solver.getVar(parseIdent(in, tmp)));
dlt2 = dlt1 ;
} else tl = Lit(solver.getVar(parseIdent(in, tmp)));
skipWhitespace(in);
if (!skipText(in, "<=>")) throw xstrdup("Expecting '<=>' in definition.");
if (*in == '<'){
++in;
if (*in == '='){
++in;
dlt2=tl;
if (*in == '>'){
++in;
dlt1=tl;
}
} else throw nsprintf("Expecting '<=>' or '<=' in definition.");
} else if (*in == '='){
++in;
if (*in == '>'){
++in;
dlt1=tl;
} else throw nsprintf("Expecting '=>' in definition.");
} else throw nsprintf("Expecting '<=>', '<=', or '=>' in definition.");
} else if (*in == '[') { // soft constraint
//**/ reportf("Soft constraint detected. ");
++in;
......@@ -345,9 +372,10 @@ bool parseConstrs(B& in, S& solver, bool old_format)
rhs = parseInt(in);
skipWhitespace(in);
if (!skipText(in, ";")) throw xstrdup("Expecting ';' after constraint.");
skipEndOfLine(in);
if (!skipText(in, ";")) throw xstrdup("Expecting ';' after constraint.");
// skipEndOfLine(in);
if (!skipEndOfLine(in)) throw xstrdup("Garbage after ';'.");
if (!solver.addConstr(ps, Cs, rhs, ineq, Int_MAX, -2, dlt1, dlt2))
return false;
ps.clear();
......@@ -430,3 +458,160 @@ void test(void)
parseFile_PB("test.pb", solver, true);
}
#endif
//================================================================================================
// Dimacs Parser:
template<class B>
static void skipDimacsComments(B& in) { // skip comment and empty lines (assuming we are at beginning of line)
// reportf("skipDimacsComments (%c)\n", *in);
while (*in == 'c' || *in == '\n') skipLine(in); }
template<class B>
static bool skipDimacsEndOfLine(B& in) { // skip newline AND trailing comment/empty lines
// reportf("skipDimacsEndOfLine (%c)\n", *in);
skipWhitespace(in);
if (*in == '\n') ++in;
else return false;
skipDimacsComments(in);
return true; }
template<class B, class S>
void parseDimacsSize(B& in, S& solver) // return true if wcnf mode
{
int n_vars, n_constrs;
skipDimacsComments(in);
if (*in != 'p') return;
++in;
skipWhitespace(in);
if (!skipText(in, "cnf")) {
if (skipText(in, "wcnf"))
wcnf_mode=true;
else goto Abort;
}
skipWhitespace(in);
n_vars = toint(parseInt(in));
skipWhitespace(in);
n_constrs = toint(parseInt(in));
solver.allocConstrs(n_vars, n_constrs);
skipWhitespace(in);
if (*in != '\n')
top_weight = parseInt(in);
reportf("DimacsSize: n_vars=%d, n_constrs=%d, top_weight=", n_vars, n_constrs); dump(top_weight); reportf("\n");
Abort:
skipLine(in);
skipDimacsComments(in);
}
template<class B>
static char* parseIntAsIdent(B& in, vec<char>& tmp) { // 'tmp' is cleared, then filled with the parsed string. '(char*)tmp' is returned for convenience.
skipWhitespace(in);
if (*in < '1' || *in > '9') throw nsprintf("Expected start of variable, not: %c", *in);
tmp.clear();
tmp.push(*in);
++in;
while (*in >= '0' && *in <= '9')
tmp.push(*in),
++in;
tmp.push(0);
return (char*)tmp; }
template<class B, class S>
bool parseDimacsConstrs(B& in, S& solver, bool max_sat_mode)
{
vec<Lit> ps; vec<Int> Cs; Int weight; vec<char> tmp;
while (*in != EOF){
Lit dlt1=lit_Undef;
bool empty = true;
// reportf("reading clause:%c\n", *in);
skipWhitespace(in);
// if ((*in < '0' || *in > '9') && *in != '-') throw xstrdup("Invalid literal.");
if (max_sat_mode) {
weight = 1;
if (wcnf_mode)
weight = parseInt(in);
// reportf("clause with weight "),dump(weight),reportf("\n");
if(weight < top_weight) {
char buf[30];
sprintf(buf, "@defsofts%d", n_defsofts++);
dlt1 = Lit(solver.getVar(buf),true); // negative literal
// Add a code to register (weight,dlt1) into the goal.
// reportf("adding a literal for goal with weight "),dump(weight),reportf("\n");
soft_goal_ps.push(~dlt1),soft_goal_Cs.push(weight);
}
}
// normal constraint
for(;;){
skipWhitespace(in);
if(*in == '0') { ++in; break; }
if(*in == '-') {
++in;
ps.push(Lit(solver.getVar(parseIntAsIdent(in, tmp)),true));
} else
ps.push(Lit(solver.getVar(parseIntAsIdent(in, tmp))));
Cs.push(1);
empty = false;
}
if (empty) throw xstrdup("Empty constraint.");
skipDimacsEndOfLine(in);
assert(ps.size() > 0);
// reportf("addConstr\n");
if (!solver.addConstr(ps, Cs, 1, 1, Int_MAX, -2, dlt1, lit_Undef))
return false;
ps.clear(); Cs.clear();
// reportf("NextConstr\n");
}
return true;
}
//================================================================================================
// Dimacs main parser functions:
template<class B, class S>
static bool parse_Dimacs(B& in, S& solver, bool max_sat_mode, bool abort_on_error)
{
Pair<bool,Int> style; Int top_weight;
try{
parseDimacsSize(in, solver);
solver.var_dec_mode = !opt_branch_goal_vars;
bool result = parseDimacsConstrs(in, solver, max_sat_mode);
if(max_sat_mode && result)
solver.addGoal(soft_goal_ps, soft_goal_Cs);
return result;
}catch (cchar* msg){
if (abort_on_error){
reportf("PARSE ERROR! [line %d] %s\n", in.line, msg);
xfree(msg);
if (opt_satlive && !opt_try)
printf("s UNSUPPORTED\n");
exit(opt_try ? 5 : 0);
}else
throw msg;
}
}
// PB parser functions: Returns TRUE if successful, FALSE if conflict detected during parsing.
// If 'abort_on_error' is false, a 'cchar*' error message may be thrown.
//
void parse_Dimacs_file(cchar* filename, PbSolver& solver, bool max_sat_mode, bool abort_on_error) {
FileBuffer buf(filename);
parse_Dimacs(buf, solver, max_sat_mode, abort_on_error); }
......@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
void parse_PB_file(cchar* filename, PbSolver& solver, bool old_format = (false), bool abort_on_error = (true));
void parse_Dimacs_file(cchar* filename, PbSolver& solver, bool max_sat_mode = (false), bool abort_on_error = (true));
//=================================================================================================
......
This diff is collapsed.
......@@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef PbSolver_h
#define PbSolver_h
#include <string>
#include "Global.h"
#include "Solver.h"
#include "Map.h"
......@@ -60,8 +61,9 @@ public:
class PbSolver {
protected:
public:
Solver sat_solver; // Underlying SAT solver.
protected:
bool& ok; // True means unsatisfiability has not been detected.
// vec<int>& assigns; // Var -> lbool: The current assignments (lbool:s stored as char:s). ('atype' is 'char' or 'int' depending on solver)
// vec<Lit>& trail; // Chronological assignment stack.
......@@ -70,9 +72,14 @@ protected:
public:
vec<Linear*> constrs; // Vector with all constraints.
vec<Linear*> constrs_bk; // Vector with all constraints for model check.
Int goal_coeff; // Real goal is goal_coeff*goal
Linear* goal; // Non-normalized goal function (used in optimization). NULL means no goal function specified. NOTE! We are always minimizing.
protected:
vec<int> goal_multi_base_sort; // Multi-base for sorting network
vec<int> goal_multi_base_bdd; // Multi-base for bdd expansion
// std::string solver_name;
protected:
int pb_i_vars; // Actual number of interest variables.
vec<int> n_occurs; // Lit -> int: Number of occurrences.
vec<vec<int> > occur; // Lit -> vec<int>: Occur lists. Left empty until 'setupOccurs()' is called.
......@@ -93,11 +100,14 @@ protected:
bool rewriteCC(Linear& c);
Formula rewriteCCbySorter(Linear& c);
bool rewriteAlmostClauses();
bool rewritePureClause(const vec<Lit>& ps, const vec<Int>& Cs, Int lo, Int hi, Lit llt);
bool convertPbs(bool first_call); // Called from 'solve()' to convert PB constraints to clauses.
bool model_check();
public:
// PbSolver() : sat_solver(opt_solver == st_MiniSat)
PbSolver() : sat_solver(opt_solver)
// , solver_name(sat_solver.solver_name)
, ok(sat_solver.ok_ref())
// , assigns(sat_solver.assigns_ref())
// , trail (sat_solver.trail_ref())
......@@ -111,6 +121,7 @@ public:
, best_goalvalue(Int_MAX)
, number_models(0)
, var_dec_mode(true)
// , minimization_mode(false)
{}
// Helpers (semi-internal):
......@@ -170,6 +181,12 @@ public:
// Exporting Variable table into CNF
void exportVar (cchar* filename);
/* // Controlling optimization
bool minimization_mode; // turned on after first SAT-solver execution
std::map<Pair< int, Pair< Interval<Int> , Interval<Int> > >, Pair<Pair< Interval<Int> , Interval<Int> >, Formula> > memo_bdd_conv_int_in_min_mode;
Map<Pair<int,Int>, Formula> memo_bdd_conv_in_min_mode;
*/
};
......
......@@ -23,8 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
//-------------------------------------------------------------------------------------------------
void linearAddition (const Linear& c, vec<Formula>& out); // From: PbSolver_convertAdd.C
Formula buildConstraint(const Linear& c, int max_cost = INT_MAX); // From: PbSolver_convertSort.C
Formula convertToBdd (const Linear& c, int decomp_mode = 0, int max_cost = INT_MAX); // From: PbSolver_convertBdd.C
Formula buildConstraint(const Linear& c, vec<int>& multi_base, int max_cost = INT_MAX); // From: PbSolver_convertSort.C
Formula convertToBdd (const Linear& c, vec<int>& multi_base, int decomp_mode = 0, bool reuse_memo = false, int max_cost = INT_MAX); // From: PbSolver_convertBdd.C
//-------------------------------------------------------------------------------------------------
Formula PbSolver::rewriteCCbySorter(Linear& c)
......@@ -34,8 +34,9 @@ Formula PbSolver::rewriteCCbySorter(Linear& c)
if(c(c.size-1) == 1) {
assert(c.lo <= Int(c.size));
assert(c.hi == Int_MAX || c.hi <= Int(c.size));
return buildConstraint(c);
vec<int> dummy;
return buildConstraint(c, dummy);
} else return _undef_ ;
}
......@@ -45,6 +46,7 @@ bool PbSolver::convertPbs(bool first_call)
vec<Formula> converted_constrs;
// if (first_call && opt_or_detection && !opt_es1_detection){
// reportf("first_call: "); if(first_call) reportf("true\n"); else reportf("false\n");
if (first_call && opt_or_detection && !opt_es1_detection){
if (!rewriteAlmostClauses()){
......@@ -88,21 +90,29 @@ bool PbSolver::convertPbs(bool first_call)
}
if(!converted) {
if (opt_convert == ct_Sorters)
converted_constrs.push(buildConstraint(c));
else if (opt_convert == ct_Adders)