Commit 907cc0f7 authored by Masahiko Sakai's avatar Masahiko Sakai

fixed several bugs

parent 5956838a
......@@ -419,7 +419,7 @@ namespace FEnv {
extern vec<int> stack;
macro void clear() { nodes.clear(); uniqueness_table.clear(); }
macro void push() { stack.push(nodes.size()); }
macro void pop() {
macro void pop() {
while (nodes.size() > stack.last())
uniqueness_table.remove(nodes.last()),
nodes.pop(); }
......
......@@ -60,35 +60,49 @@ void dump(const vec<int>& base)
}
void dump(const vec<Lit>& ps, const vec<Int>& Cs)
{
{ int i;
assert(ps.size() == Cs.size());
reportf("(%d)",ps.size());
for (int i = 0; i < truncSize(ps.size()); i++){
for (i = 0; i < truncSize(ps.size()); i++){
dump(Cs[i]);
reportf("*");
dump(ps[i]);
if (i+1 < ps.size()) reportf("...");
reportf(" ");
}
if (i+1 < ps.size()) reportf("...");
}
void dump(const vec<Pair<Int,Lit> >& Csls)
{ int i;
reportf("(%d)",Csls.size());
for (i = 0; i < truncSize(Csls.size()); i++){
dump(Csls[i].fst);
reportf("*");
dump(Csls[i].snd);
reportf(" ");
}
if (i+1 < Csls.size()) reportf("...");
}
void dump(const vec<Formula>& ps, const vec<Int>& Cs)
{
{ int i;
assert(ps.size() == Cs.size());
reportf("(%d)",ps.size());
for (int i = 0; i < truncSize(ps.size()); i++){
for (i = 0; i < truncSize(ps.size()); i++){
dump(Cs[i]);
reportf("*");
dump(ps[i]);
if (i+1 < ps.size()) reportf("...");
reportf(" ");
}
if (i+1 < ps.size()) reportf("...");
}
void dump(const vec<Lit>& ps, const vec<Int>& Cs, const vec<int>& assigns)
{
{ int i;
assert(ps.size() == Cs.size());
reportf("(%d)",ps.size());
for (int i = 0; i < truncSize(ps.size()); i++){
for (i = 0; i < truncSize(ps.size()); i++){
dump(Cs[i]);
reportf("*");
dump(ps[i]);
......@@ -98,8 +112,9 @@ void dump(const vec<Lit>& ps, const vec<Int>& Cs, const vec<int>& assigns)
reportf(":1");
else
reportf(":0");
if (i+1 < ps.size()) reportf("...");
reportf(" ");
}
if (i+1 < ps.size()) reportf("...");
}
......
......@@ -34,6 +34,7 @@ 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<Pair<Int,Lit> >& Csls);
void dump(const vec<Lit>& ps, const vec<Int>& Cs, const vec<int>& assigns);
void dump(const vec<Formula>& ps, const vec<Int>& Cs);
void dump(const Linear& pb, const vec<int>& assigns);
......
1 x1 -1 x2 1 x3 -1 x4 >= -1 ;
3 x1 4 x2 5 x3 6 x4 >= 8 ;
......@@ -66,7 +66,8 @@ ConvertT opt_convert_goal = ct_Sorters; //ct_Undef;
bool opt_convert_goal_reusing = true;
bool opt_convert_weak = true;
//bool opt_avoid_band_constraint = false;
int opt_opt_base_method = 2; // 0: original 1: BB, 2: hashBB
int opt_optbase_construction_alg = 2; // 0: original 1: BB, 2: hashBB
int opt_optbase_measure = 2; // 0:obt_digits, 1:obt_comb, 2:obt_kind, 3:obt_new
int opt_avoid_band_constraint = 0;
// 0: band form, 1: band form if not-eq constraint, 2: only standard form
bool opt_split = false;
......@@ -149,7 +150,10 @@ cchar* doc =
// " -cm2 -mixed2 Convert PB-constrs to clauses by another mix mode of the above.\n"
" -ga/gs/gb/gm Override conversion for goal function (long name: -goal-xxx). (default: gs)\n"
" -w -weak-off Clausify with equivalences instead of implications.\n"
" -or-detection-off Don't detect OR clause.\n"
" -om= Opt_base construction method (0: original 1: BB, 2: hashBB (default)).\n"
" -bdd-d-digits Minimizing total digits for opt_base measure for BDD.\n"
" -bdd-d-comb Minimizing total digits and carry for opt_base measure for BDD.\n"
" -bdd-d-kind Minimizing kinds for opt_base measure for BDD.\n"
" -es1, -es1-detection Produce ES1 clause if possible.\n"
" -cc, -cc-detection Produce cardinarity clause if possible.\n"
" -ccs, -cc-sort Convert cardinarity clause by sorting network.\n"
......@@ -170,7 +174,7 @@ cchar* doc =
" -bdd-dN Clausify BDDs after multi-based-decomposition of coefficients by strategy N=1,2,3.\n"
" -bdd-d-off Clausify BDDs without multi-based-decomposition of coefficients.\n"
" -bdd-i-off Construct non-ROBDDs.\n"
" -bdd-r Construct BDDs in reverse (increasing) order.\n"
" -bdd-r Construct BDDs from reverse (increasing) ordered constraints.\n"
"\n"
" -cc-thres= Threshold for prefering CC-clause. [def: %d]\n"
" -bdd-thres= Threshold for prefering BDDs in mixed mode. [def: %g]\n"
......@@ -271,7 +275,11 @@ void parseOptions(int argc, char** argv)
else if (oneof(arg, "ngr,goal-non-reusing")) opt_convert_goal_reusing = false;
else if (oneof(arg, "w,weak-off" )) opt_convert_weak = false;
else if (strncmp(arg, "-om=", 4) == 0) opt_opt_base_method = atoi(arg+4);
else if (strncmp(arg, "-om=", 4) == 0) opt_optbase_construction_alg = atoi(arg+4);
else if (oneof(arg, "bdd-d-digits")) opt_optbase_measure = 0; //obt/_digits
else if (oneof(arg, "bdd-d-comb")) opt_optbase_measure = 1; //obt_comb
else if (oneof(arg, "bdd-d-kind")) opt_optbase_measure = 2; //obt_kind (default)
else if (oneof(arg, "bdd-d-new")) opt_optbase_measure = 3; //obt_new
else if (oneof(arg, "or-detection-off")) opt_or_detection = false;
else if (oneof(arg, "es1,es1-detection")) opt_es1_detection = true;
else if (oneof(arg, "cc,cc-detection")) opt_cc_detection = true;
......@@ -311,7 +319,7 @@ void parseOptions(int argc, char** argv)
//(end)
else if (oneof(arg, "1,first" )) opt_command = cmd_FirstSolution;
else if (oneof(arg, "A,all" )) opt_command = cmd_AllSolutions, opt_model_check=false;
else if (oneof(arg, "A,all" )) opt_command = cmd_AllSolutions, opt_model_check=false; //, opt_simp_solver=false;
else if (oneof(arg, "AI,all-interest")) opt_command = cmd_InterestSolutions, opt_model_check=false;
else if (oneof(arg, "seq" )) opt_minimization = 0;
else if (oneof(arg, "bin" )) opt_minimization = 1;
......@@ -331,7 +339,7 @@ void parseOptions(int argc, char** argv)
else if (oneof(arg, "of,old-fmt")) opt_old_format = true;
else if (oneof(arg, "dm,dimacs" )) opt_dimacs = true;
else if (oneof(arg, "ec" )) opt_eager_cl = false;
else if (oneof(arg, "mx,max-sat")) opt_maxsat = true, opt_dimacs = true;
else if (oneof(arg, "mx,max-sat")) opt_maxsat = true, opt_dimacs = true, opt_convert_goal = ct_Undef, opt_convert_bdd_decomposition = 2, opt_bdd_thres = 100;
else if (oneof(arg, "u,ucore=" )) opt_extract_ucore = true;
else if (strncmp(arg, "-ucore-mode=", 12) == 0) opt_ucore_mode = atof(arg+12);
......@@ -351,6 +359,7 @@ void parseOptions(int argc, char** argv)
args.push(arg);
}
if (!opt_avoid_band_constraint && opt_convert_bdd_monotonic && !opt_convert_bdd_interval)
reportf("We set -m because of -bdd-i-off.\n"), opt_avoid_band_constraint = 2; // only standard form
......@@ -360,9 +369,14 @@ void parseOptions(int argc, char** argv)
&& opt_solver != st_Glucose10)
reportf("We set -GM because of -extract-ucore.\n"), opt_solver = st_GlueMiniSat;
/*
if (opt_cnf != NULL && (opt_solver == st_ES1Sat || opt_solver == st_CCMiniSat))
reportf("-cnf option is not handled by ES1Sat/CCMiniSat. We set -M2 instead.\n"), opt_solver = st_MiniSat22;
if (opt_cnf != NULL && opt_simp_solver)
reportf("We set -noSimp because of -cnf.\n"), opt_simp_solver = false;
*/
if (opt_es1_detection && opt_cc_detection)
reportf("Conflict between -es1 and -cc. We ignore the latter.\n"), opt_cc_detection = false;
......@@ -371,7 +385,7 @@ void parseOptions(int argc, char** argv)
if (opt_cc_detection && opt_solver != st_CCMiniSat)
reportf("We set -C because of -cc-detection.\n"), opt_solver = st_CCMiniSat;
if (opt_simp_solver && opt_solver != st_CCMiniSat && opt_solver != st_GlueMiniSat)
if (opt_simp_solver && (opt_solver == st_MiniSat || opt_solver == st_SatELite))
reportf("We set -noSimp.\n"), opt_simp_solver = false;
if (args.size() == 0)
......@@ -513,6 +527,7 @@ void outputResult(PbSolver& S, bool normalExit = true)
// if (opt_verbosity >= 1) {
{
if (S.sat_solver.solving) S.sat_solver.solving_time += (cpuTime() - S.sat_solver.starting_time);
printStats(S.stats, cpuTime(), S.sat_solver.solving_time);
}
......@@ -585,7 +600,7 @@ int main(int argc, char** argv)
pb_solver = new PbSolver(); // (must be constructed AFTER parsing commandline options -- constructor uses 'opt_solver' to determinte which SAT solver to use)
// signal(SIGINT , SIGINT_handler);
signal(SIGINT , SIGTERM_handler); // 2, SIGINT, terminate process, interrupt program
signal(SIGABRT , SIGTERM_handler); // 6, SIGABRT, create core image, abort program (formerly SIGIOT)
// signal(SIGABRT , SIGTERM_handler); // 6, SIGABRT, create core image, abort program (formerly SIGIOT)
signal(SIGSEGV , SIGTERM_handler); // 11, SIGSEGV, create core image, segmentation violation
signal(SIGTERM, SIGTERM_handler); // 15, SIGTERM, terminate process, software termination signal
signal(SIGUSR1, SIGTERM_handler); // 30, SIGUSR1, terminate process, User defined signal 1
......
......@@ -60,7 +60,8 @@ 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 int opt_optbase_construction_alg;
extern int opt_optbase_measure;
extern bool opt_or_detection;
extern bool opt_es1_detection;
extern bool opt_cc_detection;
......
......@@ -6,7 +6,13 @@ CSRCS = $(wildcard *.C)
CHDRS = $(wildcard *.h)
#COBJS = $(addsuffix .o, $(basename $(CSRCS))) ADTs/Global.o ADTs/FEnv.o ADTs/File.o glueminisat/core/Solver.o es1sat/core/Solver.o
#COBJS = $(addsuffix .o, $(basename $(CSRCS))) ADTs/Global.o ADTs/FEnv.o ADTs/File.o glueminisat/core/Solver.o es1sat/core/Solver.o ccminisat/core/Solver.o
COBJS = $(addsuffix .o, $(basename $(CSRCS))) ADTs/Global.o ADTs/FEnv.o ADTs/File.o glueminisat/core/Solver.o glueminisat/simp/SimpSolver.o glueminisat/utils/System.o es1sat/core/Solver.o es1sat/simp/SimpSolver.o ccminisat/core/Solver.o ccminisat/simp/SimpSolver.o
COBJSPB = $(addsuffix .o, $(basename $(CSRCS))) ADTs/Global.o ADTs/FEnv.o ADTs/File.o
PCOBJSPB = $(addsuffix p, $(COBJSPB))
DCOBJSPB = $(addsuffix d, $(COBJSPB))
RCOBJSPB = $(addsuffix r, $(COBJSPB))
R64COBJSPB= $(addsuffix x, $(COBJSPB))
COBJS = $(COBJSPB) glueminisat/core/Solver.o glueminisat/simp/SimpSolver.o glueminisat/utils/System.o es1sat/core/Solver.o es1sat/simp/SimpSolver.o ccminisat/core/Solver.o ccminisat/simp/SimpSolver.o
PCOBJS = $(addsuffix p, $(COBJS))
DCOBJS = $(addsuffix d, $(COBJS))
RCOBJS = $(addsuffix r, $(COBJS))
......@@ -14,6 +20,8 @@ R64COBJS = $(addsuffix x, $(COBJS))
EXEC = naps
#CXX = g++6
#LDFLAGS += -Wl,-rpath=/usr/local/lib/gcc6
CXX = g++
#CXX = icpc
CFLAGS = -Wall -ffloat-store
......@@ -27,7 +35,7 @@ COPTIMIZE = -O3 -fomit-frame-pointer -falign-loops=4 -falign-functions=16 -fopti
LDFLAGS += -L/usr/local/lib -L/opt/local/lib
LDFLAGS += -L/usr/lib
.PHONY : s p d r x build clean depend
.PHONY : s p d r x build clean cleanPB depend
s: WAY=standard
p: WAY=profile
......@@ -36,10 +44,13 @@ r: WAY=release
rs: WAY="release static / bignums"
rx: WAY="release static / 64-bit integers"
s: CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG
p: CFLAGS+=$(COPTIMIZE) -pg -ggdb -D DEBUG
s: CFLAGS+=$(COPTIMIZE) -ggdb3 -D DEBUG
s: LDFLAGS+=-ggdb3
p: CFLAGS+=$(COPTIMIZE) -pg -ggdb3 -D DEBUG
p: LDFLAGS+=-ggdb3
#d: CFLAGS+=-O0 -ggdb -D DEBUG -D PARANOID -D NO_GMP
d: CFLAGS+=-O0 -ggdb -D DEBUG -D PARANOID
d: LDFLAGS+=-ggdb3
r: CFLAGS+=$(COPTIMIZE) -D NDEBUG
#r: CFLAGS+=$(COPTIMIZE) -D ND_GMP
rs: CFLAGS+=$(COPTIMIZE) -D NDEBUG
......@@ -57,9 +68,12 @@ rx: build $(EXEC)_64-bit_static
build:
@echo Building $(EXEC) "("$(WAY)")"
clean:
cleanPB:
@rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
$(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) $(R64COBJS) depend.mak
$(COBJSPB) $(PCOBJSPB) $(DCOBJSPB) $(RCOBJSPB) $(R64COBJSPB) depend.mak
clean:
$(MAKE) cleanPB
MROOT=$(CURDIR)/glueminisat $(MAKE) -C $(CURDIR)/glueminisat/core clean
MROOT=$(CURDIR)/glueminisat $(MAKE) -C $(CURDIR)/glueminisat/simp clean
MROOT=$(CURDIR)/es1sat $(MAKE) -C $(CURDIR)/es1sat/core clean
......@@ -147,15 +161,15 @@ ccminisat/simp/SimpSolver.ox: ccminisat/simp/SimpSolver.cc
## Linking rules (standard/profile/debug/release)
$(EXEC): $(COBJS)
@echo Linking $(EXEC)
@$(CXX) $(COBJS) $(LDFLAGS) -lz -lgmp -ggdb -Wall -o $@
@$(CXX) $(COBJS) $(LDFLAGS) -lz -lgmp -Wall -o $@
$(EXEC)_profile: $(PCOBJS)
@echo Linking $@
@$(CXX) $(PCOBJS) $(LDFLAGS) -lz -lgmp -ggdb -Wall -pg -o $@
@$(CXX) $(PCOBJS) $(LDFLAGS) -lz -lgmp -Wall -pg -o $@
$(EXEC)_debug: $(DCOBJS)
@echo Linking $@
@$(CXX) $(DCOBJS) $(LDFLAGS) -lz -lgmp -ggdb -Wall -o $@
@$(CXX) $(DCOBJS) $(LDFLAGS) -lz -lgmp -Wall -o $@
$(EXEC)_release: $(RCOBJS)
@echo Linking $@
......
This diff is collapsed.
......@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
//=================================================================================================
enum OptBaseT { obt_digits, obt_comb, obt_kind };
enum OptBaseT { obt_digits, obt_comb, obt_kind, opt_new };
// returns the cardinarity of the given sorted sequence as a set.
template <class T>
......
......@@ -1063,9 +1063,16 @@ void PbSolver::solve(const PbSolver& S, solve_Command cmd)
if (!convertPbs(true)){ assert(!ok); solver_status = sst_unsat; return; } // unsat
// Freeze goal function variables (for SatELite and Simplification solvers):
if (goal != NULL && opt_simp_solver){
if (goal != NULL && opt_simp_solver && cmd != sc_AllModels){
for (int i = 0; i < goal->size; i++)
sat_solver.freeze(var((*goal)[i]));
//reportf("FreeZing %d\n",var((*goal)[i])),
sat_solver.freeze(var((*goal)[i]));
}
// Freeze all input variables (for SatELite and Simplification solvers):
if (opt_simp_solver && cmd == sc_AllModels){
for (int i = 0; i < pb_n_vars; i++)
//reportf("FreeZing %d\n",i),
sat_solver.freeze(i);
}
// Solver (optimize):
......
......@@ -90,7 +90,7 @@ bool PbSolver::convertPbs(bool first_call)
}
if(!converted) {
vec<int> dummy1;
vec<int> dummy1, dummy2;
if (opt_convert == ct_Sorters) {
converted_constrs.push( buildConstraint(c, ((!first_call) ? goal_multi_base_sort : dummy1) ) );
if( !first_call && opt_verbosity >= 1) reportf("Sorter: base: "),dump(goal_multi_base_sort),reportf("\n");
......@@ -105,15 +105,15 @@ bool PbSolver::convertPbs(bool first_call)
Formula result = convertToBdd(c, ((!first_call) ? goal_multi_base_bdd : dummy1), opt_convert_bdd_decomposition, !first_call && opt_convert_goal_reusing, (int)(adder_cost * opt_bdd_thres));
if( !first_call && opt_verbosity >= 1) reportf("Bdd: base: "),dump(goal_multi_base_bdd),reportf("\n");
if (result == _undef_) {
if(opt_verbosity >=1 && !first_call) reportf("Switching to sorting network\n");
result = buildConstraint(c, ((!first_call) ? goal_multi_base_sort : dummy1), (int)(adder_cost * opt_sort_thres));
if( !first_call && opt_verbosity >= 1) reportf("Sorter: base: "),dump(goal_multi_base_sort),reportf("\n");
if(opt_verbosity >=2) reportf("Switching to sorting network\n");
result = buildConstraint(c, ((!first_call) ? goal_multi_base_sort : dummy2), (int)(adder_cost * opt_sort_thres));
if( !first_call && opt_verbosity >= 1) reportf("Sorter: base: "),dump(goal_multi_base_sort),reportf("\n");
}
if (result == _undef_) {
if(opt_verbosity >=1 && !first_call) reportf("Switching to adder coding\n");
linearAddition(c, converted_constrs);
if(opt_verbosity >=2) reportf("Switching to adder coding\n");
linearAddition(c, converted_constrs);
} else
converted_constrs.push(result);
converted_constrs.push(result);
/*
}else if (opt_convert == ct_Mixed2){
int adder_cost = estimatedAdderCost(c);
......
......@@ -277,25 +277,29 @@ Formula convertToBdd_one(vec<Lit>& ls, vec<Int>& Cs, Int lo, Int hi, vec<int>& b
vec<Int> norm_Cs;
// vec<int> base;
bool perform_decomposition = false;
static int lastPsCs_size = 0;
if (decomp_mode == 1) { // binary-base decomposition
// decompose terms; e.g. 11x into x + 2x + 8x
// reportf("B");
for (int i = 0; i < ls.size(); i++) {
Int div, rem, co = 1;
// div = c(i);
div = Cs[i];
while( div > 0 ) {
//reportf("div=%d, rem=%d, co=%d\n",toint(div),toint(rem),toint(co));
// reportf("div=%d, rem=%d, co=%d\n",toint(div),toint(rem),toint(co));
rem = div % 2; div = div / 2;
if(rem != 0) {
// Csls.push(Pair_new(co, c[i]));
Csls.push(Pair_new(co, ls[i]));
//reportf("BDD-cost:%5d\n", FEnv::topSize());
//reportf("ps[%d]=", i),dump(c[i]),reportf(", Cs[%d]=", i),dump(co),reportf("\n");
// reportf("A: ps[%d]=", i),dump(ls[i]),reportf(", Cs[%d]=", i),dump(co),reportf("\n");
}
co *= 2;
}
}
// reportf("\nBin:Be ls,Cs="),dump(Csls); reportf(", lo="),dump(lo),reportf(", hi="),dump(hi),reportf("\n");
if(opt_convert_bdd_increasing_order) sortr(Csls); else sort(Csls);
//reportf("Bin:Af ls,Cs="),dump(Csls); reportf(", lo="),dump(lo),reportf(", hi="),dump(hi),reportf("\n");
} else if (decomp_mode >= 2) { // multi-base decomposition
//==================
......@@ -348,6 +352,7 @@ Formula convertToBdd_one(vec<Lit>& ls, vec<Int>& Cs, Int lo, Int hi, vec<int>& b
gettimeofday(&s, NULL); // for time evaluation
#endif
optimizeBase(Cs, dummy, cost, base, obt_kind); // the last argument declares non-carryimportant
// optimizeBase(Cs, dummy, cost, base, opt_optbase_measure); // the last argument declares non-carryimportant
#ifdef DEBUG
gettimeofday(&t, NULL); // for time evaluation
if(opt_verbosity >= 2)
......@@ -404,14 +409,18 @@ Formula convertToBdd_one(vec<Lit>& ls, vec<Int>& Cs, Int lo, Int hi, vec<int>& b
reportf("ls,Cs="),dump(norm_ls,norm_Cs);
*/
if(opt_convert_bdd_increasing_order) sortr(Csls); else sort(Csls);
// reportf("\nDec:Be ls,Cs="),dump(Csls); reportf(", lo="),dump(lo),reportf(", hi="),dump(hi),reportf("\n");
if(opt_convert_bdd_increasing_order) sortr(Csls); else sort(Csls);
// reportf("Dec:Af ls,Cs="),dump(Csls); reportf(", lo="),dump(lo),reportf(", hi="),dump(hi),reportf("\n");
} else {
//reportf("count=%d kind=%d max_coef=",count_weight,kind_weight); dump(Cs[Cs.size()-1]); reportf(" non-decomposition \n\n");
if(opt_verbosity >=1) reportf("d");
for (int i = 0; i < ls.size(); i++) {
Csls.push(Pair_new(Cs[i], ls[i]));
}
// reportf("\nNon:Be ls,Cs="),dump(Csls); reportf(", lo="),dump(lo),reportf(", hi="),dump(hi),reportf("\n");
if(opt_convert_bdd_increasing_order) sortr(Csls);
// reportf("Non:Af ls,Cs="),dump(Csls); reportf(", lo="),dump(lo),reportf(", hi="),dump(hi),reportf("\n");
}
} else { // non-decomposition // decomp_mode: 0 /////////////////
......@@ -421,7 +430,9 @@ Formula convertToBdd_one(vec<Lit>& ls, vec<Int>& Cs, Int lo, Int hi, vec<int>& b
for (int i = 0; i < ls.size(); i++) {
Csls.push(Pair_new(Cs[i], ls[i]));
}
// reportf("\nNon:Be ls,Cs="),dump(Csls); reportf(", lo="),dump(lo),reportf(", hi="),dump(hi),reportf("\n");
if(opt_convert_bdd_increasing_order) sortr(Csls);
// reportf("Non:Af ls,Cs="),dump(Csls); reportf(", lo="),dump(lo),reportf(", hi="),dump(hi),reportf("\n");
}
for (int i = 0; i < Csls.size(); i++)
......@@ -433,6 +444,11 @@ Formula convertToBdd_one(vec<Lit>& ls, vec<Int>& Cs, Int lo, Int hi, vec<int>& b
FEnv::push();
if(minimization_mode) {
if(Csls.size() != lastPsCs_size) {
lastPsCs_size = Csls.size();
memo_bdd_conv_int_in_min_mode.clear();
if(opt_verbosity >=1) reportf("mem for reusing cleared.\n");
}
if(opt_convert_bdd_interval)
ret = buildBDD_i(norm_ls, norm_Cs, lo, hi, Csls.size(), 0, sum, memo_bdd_conv_int_in_min_mode, max_cost).snd;
else
......
......@@ -54,14 +54,16 @@ void buildSorter(vec<Formula>& ps, vec<Int>& Cs, vec<Formula>& out_sorter)
}
class Exception_TooBig {};
//class Exception_TooBig {};
static
void buildConstraint(vec<Formula>& ps, vec<Int>& Cs, vec<Formula>& carry, vec<int>& base, int digit_no, vec<vec<Formula> >& out_digits, int max_cost)
bool buildConstraint(vec<Formula>& ps, vec<Int>& Cs, vec<Formula>& carry, vec<int>& base, int digit_no, vec<vec<Formula> >& out_digits, int max_cost)
{
bool ret=true;
assert(ps.size() == Cs.size());
if (FEnv::topSize() > max_cost) throw Exception_TooBig();
// if (FEnv::topSize() > max_cost) throw Exception_TooBig();
if (FEnv::topSize() > max_cost) return false;
//**/reportf("buildConstraint("); for (int i = 0; i < ps.size(); i++) reportf("%d*%d ", toint(Cs[i]), (*debug_names)[index(ps[i])]); reportf("+ %d carry)\n", carry.size()); index==-1 --- true
......@@ -120,8 +122,9 @@ void buildConstraint(vec<Formula>& ps, vec<Int>& Cs, vec<Formula>& carry, vec<in
out_digits.last().push(out);
}
buildConstraint(ps_div, Cs_div, carry, base, digit_no+1, out_digits, max_cost); // <<== change to normal loop
ret = buildConstraint(ps_div, Cs_div, carry, base, digit_no+1, out_digits, max_cost); // <<== change to normal loop
}
return ret;
}
/*
......@@ -178,8 +181,9 @@ Formula buildConstraint(vec<Formula>& ps, vec<Int>& Cs, vec<int>& base, Int lo,
{
vec<Formula> carry;
vec<vec<Formula> > digits;
buildConstraint(ps, Cs, carry, base, 0, digits, max_cost);
if (FEnv::topSize() > max_cost) throw Exception_TooBig();
if( ! buildConstraint(ps, Cs, carry, base, 0, digits, max_cost)) return _undef_;
// (buildConstraint(ps, Cs, carry, base, 0, digits, max_cost)== _undef_);
// if (FEnv::topSize() > max_cost) throw Exception_TooBig();
vec<int> lo_digs;
vec<int> hi_digs;
......@@ -211,7 +215,7 @@ Num: 2 0 5 6
stats_sort_constraints++;
Formula ret = ((lo == Int_MIN) ? _1_ : lexComp(lo_digs, digits))
& ((hi == Int_MAX) ? _1_ : ~lexComp(hi_digs, digits));
if (FEnv::topSize() > max_cost) throw Exception_TooBig();
// if (FEnv::topSize() > max_cost) throw Exception_TooBig();
return ret;
}
......@@ -238,7 +242,8 @@ Formula buildConstraintGpw(vec<Formula>& ps, vec<Int>& Cs, vec<int>& base, Int l
vec<Formula> carry;
vec<vec<Formula> > digits;
buildConstraint(ps, Cs, carry, base, 0, digits, max_cost);
if( ! buildConstraint(ps, Cs, carry, base, 0, digits, max_cost)) return _undef_;
// buildConstraint(ps, Cs, carry, base, 0, digits, max_cost);
/**/ if (opt_verbosity >= 3){reportf("Networks:"); for (int i = 0; i < digits.size(); i++) reportf(" %d", digits[i].size()); reportf("\n");}
......@@ -263,12 +268,17 @@ Formula buildConstraint(const Linear& c, vec<int>& base, int max_cost)
Cs.push(c(j)),
csum += c(j);
//reportf("InitialBase"); for (int i = 0; i < base.size(); i++) reportf(" %d", base[i]); reportf("\n");
if(base.size() == 0) {
vec<Int> dummy;
int cost;
//vec<int> base;
optimizeBase(Cs, dummy, cost, base, obt_comb); // the last arugument declares carry_important
//reportf("OptBase"); for (int i = 0; i < base.size(); i++) reportf(" %d", base[i]); reportf("\n");
}
FEnv::push();
......@@ -279,7 +289,7 @@ Formula buildConstraint(const Linear& c, vec<int>& base, int max_cost)
if(c.lo > 0) {
if(opt_convert_gpw==gt_none) { // original minisatp conversion
// reportf("non-GPW\n");
try {
// try {
if(opt_avoid_band_constraint==0 ||
(opt_avoid_band_constraint==1 && c.lo != c.hi)){
ret = buildConstraint(ps, Cs, base, c.lo, c.hi, max_cost);
......@@ -292,22 +302,25 @@ Formula buildConstraint(const Linear& c, vec<int>& base, int max_cost)
ret &= buildConstraint(ps, Cs, base, csum - c.hi, Int_MAX, max_cost);
}
}
}catch (Exception_TooBig){
if(ret == _undef_){
// }catch (Exception_TooBig){
if (opt_verbosity >= 2){
reportf("Sorter-cost:%5d ", FEnv::topSize());
}
FEnv::pop();
return _undef_;
}
stats_sort_cost = max(stats_sort_cost, FEnv::topSize());
if (opt_verbosity >= 2){
reportf("Sorter-cost:%5d ", FEnv::topSize());
reportf("Base:"); for (int i = 0; i < base.size(); i++) reportf(" %d", base[i]); reportf("\n");
}
FEnv::keep();
// FEnv::keep();
} else { // GPW
// reportf("GPW\n");
try {
// try {
ret = _1_ ;
bool lowp= c.lo <= (csum - c.lo + 1) ;
......@@ -362,7 +375,11 @@ Formula buildConstraint(const Linear& c, vec<int>& base, int max_cost)
//negative
}
}
}catch (Exception_TooBig){
if(ret == _undef_){
// }catch (Exception_TooBig){
if (opt_verbosity >= 2){
reportf("Sorter-cost:%5d ", FEnv::topSize());
}
FEnv::pop();
return _undef_;
}
......@@ -372,10 +389,12 @@ Formula buildConstraint(const Linear& c, vec<int>& base, int max_cost)
reportf("Sorter-cost:%5d ", FEnv::topSize());
reportf("Base:"); for (int i = 0; i < base.size(); i++) reportf(" %d", base[i]); reportf("\n");
}
FEnv::keep();
// FEnv::keep();
}
}
FEnv::keep();
assert(ret != _undef_);
/*
if(c.dlt!=lit_Undef) {
......
naps-1.02-maxsat is equivalent to naps-1.02 with -max-sat option
==== NaPS 1.x solver ====
Overall:
......@@ -66,8 +62,10 @@ The solver tries to find a model with minimum sum of penalties.
[dimacs inputs]
-dimacs option enables to read dimacs cnf files.
[maxsat mode]
======================
[maxsat mode] ========
-max-sat option states to solve maxsat cnf/wcnf.
======================
===
......@@ -89,11 +87,19 @@ For showing its usage, try
See INSTALL for its installation.
Known BUG:
Known BUGs:
- -S may result wrong answer.
- Combination of -Simp and -es1 may result wrong answer.
Version 1.02 Apr 13, 2016
Modified on Oct 31, 2016
- Fixed a bug showing unaccurate SAT-solving time when interrupted.
- Fixed a bug on switching bdd/sort/adder strategies.
- Fixed a bug on combinating -A and -Simp
Modified on Jul 27, 2016
- Fixed a bug related to -ngr option.
Version 1.02b Apr 13, 2016
- Modulo reduction for optimized-base [TACAS 2011]
with primes up to 10000.
- New cost function for optimized-base calculation (kind_digits).
......
......@@ -108,7 +108,8 @@ class Solver {
}
public:
double solving_time;
double solving_time, starting_time;
bool solving;
bool& ok_ref() {
if (minisat) return minisat->ok;
if (satelite) return satelite->ok;
......@@ -374,9 +375,9 @@ public:
return false;
}
bool solve(const vec<Lit>& assumps) {
double start_time = cpuTime();
starting_time = cpuTime(); solving = true;
bool result = solve_(assumps);
solving_time += (cpuTime() - start_time);
solving_time += (cpuTime() - starting_time), solving = false;
return result;
}
bool solve() {
......@@ -487,7 +488,9 @@ public:
simp_es1sat (opt_simp_solver && type == st_ES1Sat ? new ES1Sat::SimpSolver : NULL),
ccminisat (!opt_simp_solver && type == st_CCMiniSat? new CCMiniSat::Solver : NULL),
simp_ccminisat (opt_simp_solver && type == st_CCMiniSat? new CCMiniSat::SimpSolver : NULL),
solving_time (0.0)
solving_time (0.0),
starting_time (0.0),
solving (false)
{
if (opt_extract_ucore) glueminisat->setUcoreExtract(opt_ucore_mode);
// if (type == st_MiniSat22) glueminisat->setMiniSat22Params();
......
/********* NaPS (Nagoya Pesudo-Boolena Solver) ***********/
#define naps_version "1.02b"
#define naps_version "1.02b1"
//
// naps-1.02a7-bdd-d3-bdd-thres=180-gs
......@@ -1833,6 +1833,11 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
// Assumptions are added as unit clauses:
cnt += assumptions.size();
// added by nabesima
// Unit clauses are added
assert(decisionLevel() == 0);
cnt += trail.size();
fprintf(f, "p cnf %d %d\n", max, cnt);
for (int i = 0; i < assumptions.size(); i++){
......@@ -1840,6 +1845,13 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
}
// added by nabesima
// Unit clauses are added
for (int i = 0; i < trail.size(); i++){
assert(value(trail[i]) != l_False);
fprintf(f, "%s%d 0\n", sign(trail[i]) ? "-" : "", mapVar(var(trail[i]), map, max)+1);
}
for (int i = 0; i < clauses.size(); i++)
toDimacs(f, ca[clauses[i]], map, max);
......
......@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
// added by nabesima
#include "RecentVals.h"
#define GLUEGlueMiniSat_VERSION "glueminisat2.2.6-ucore-g"
#define GLUEGlueMiniSat_VERSION "glueminisat2.2.6-ucore-h"
namespace GlueMiniSat {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment