From 1232bbad68a899de4a45365987e8673a540de171 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Jul 31 2013 22:50:07 +0000 Subject: Rebuild for new glpk and new picosat. --- diff --git a/csisat-glpk.patch b/csisat-glpk.patch new file mode 100644 index 0000000..5e3f617 --- /dev/null +++ b/csisat-glpk.patch @@ -0,0 +1,469 @@ +--- ./glpk_ml_wrapper/src/camlglpk.c.orig 2008-07-08 22:38:04.000000000 -0600 ++++ ./glpk_ml_wrapper/src/camlglpk.c 2013-07-31 15:57:11.000000000 -0600 +@@ -60,14 +60,14 @@ void to_std_out() + value lp_create(value unit) + { + CAMLparam1(unit); +- LPX* lp = lpx_create_prob(); ++ glp_prob* lp = glp_create_prob(); + CAMLreturn ((value)lp); + } + + value lp_delete(value lp) + { + CAMLparam1(lp); +- lpx_delete_prob((LPX*)lp); ++ glp_delete_prob((glp_prob*)lp); + CAMLreturn (Val_unit); + } + +@@ -75,105 +75,105 @@ value lp_delete(value lp) + value lp_set_maximize(value lp) + { + CAMLparam1(lp); +- lpx_set_obj_dir((LPX*)lp, LPX_MAX); ++ glp_set_obj_dir((glp_prob*)lp, GLP_MAX); + CAMLreturn (Val_unit); + } + + value lp_set_minimize(value lp) + { + CAMLparam1(lp); +- lpx_set_obj_dir((LPX*)lp, LPX_MIN); ++ glp_set_obj_dir((glp_prob*)lp, GLP_MIN); + CAMLreturn (Val_unit); + } + + value lp_add_row(value lp, value i) + { + CAMLparam2(lp,i); +- lpx_add_rows((LPX*)lp, Int_val(i)); ++ glp_add_rows((glp_prob*)lp, Int_val(i)); + CAMLreturn (Val_unit); + } + + value lp_add_col(value lp, value i) + { + CAMLparam2(lp,i); +- lpx_add_cols((LPX*)lp, Int_val(i)); ++ glp_add_cols((glp_prob*)lp, Int_val(i)); + CAMLreturn (Val_unit); + } + + value lp_set_row_bnd_free(value lp, value i) + { + CAMLparam2(lp,i); +- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_FR, 0.0, 0.0 ); ++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_FR, 0.0, 0.0 ); + CAMLreturn (Val_unit); + } + + value lp_set_row_bnd_lower(value lp, value i, value lo) + { + CAMLparam3(lp,i,lo); +- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_LO, Double_val(lo), 0.0 ); ++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_LO, Double_val(lo), 0.0 ); + CAMLreturn (Val_unit); + } + + value lp_set_row_bnd_upper(value lp, value i, value up) + { + CAMLparam3(lp,i,up); +- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_UP, 0.0, Double_val(up) ); ++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_UP, 0.0, Double_val(up) ); + CAMLreturn (Val_unit); + } + + value lp_set_row_bnd_double(value lp, value i, value lo, value up) + { + CAMLparam4(lp,i,lo,up); +- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_DB, Double_val(lo), Double_val(up) ); ++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_DB, Double_val(lo), Double_val(up) ); + CAMLreturn (Val_unit); + } + + value lp_set_row_bnd_fixed(value lp, value i, value x) + { + CAMLparam3(lp,i,x); +- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_FX, Double_val(x), Double_val(x) ); ++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_FX, Double_val(x), Double_val(x) ); + CAMLreturn (Val_unit); + } + + value lp_set_col_bnd_free(value lp, value i) + { + CAMLparam2(lp,i); +- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_FR, 0.0, 0.0 ); ++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_FR, 0.0, 0.0 ); + CAMLreturn (Val_unit); + } + + value lp_set_col_bnd_lower(value lp, value i, value lo) + { + CAMLparam3(lp,i,lo); +- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_LO, Double_val(lo), 0.0 ); ++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_LO, Double_val(lo), 0.0 ); + CAMLreturn (Val_unit); + } + + value lp_set_col_bnd_upper(value lp, value i, value up) + { + CAMLparam3(lp,i,up); +- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_UP, 0.0, Double_val(up) ); ++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_UP, 0.0, Double_val(up) ); + CAMLreturn (Val_unit); + } + + value lp_set_col_bnd_double(value lp, value i, value lo, value up) + { + CAMLparam4(lp,i,lo,up); +- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_DB, Double_val(lo), Double_val(up) ); ++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_DB, Double_val(lo), Double_val(up) ); + CAMLreturn (Val_unit); + } + + value lp_set_col_bnd_fixed(value lp, value i, value x) + { + CAMLparam3(lp,i,x); +- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_FX, Double_val(x), Double_val(x) ); ++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_FX, Double_val(x), Double_val(x) ); + CAMLreturn (Val_unit); + } + + value lp_set_obj_coef(value lp, value i, value coeff) + { + CAMLparam3(lp,i,coeff); +- lpx_set_obj_coef((LPX*)lp, Int_val(i) + 1, Double_val(coeff)); ++ glp_set_obj_coef((glp_prob*)lp, Int_val(i) + 1, Double_val(coeff)); + CAMLreturn (Val_unit); + } + +@@ -194,7 +194,7 @@ value lp_set_mat_row(value lp, value i, + } + } + if(non_zero > 0){ +- lpx_set_mat_row((LPX*)lp, Int_val(i) + 1, non_zero, indexes, val); ++ glp_set_mat_row((glp_prob*)lp, Int_val(i) + 1, non_zero, indexes, val); + } + free(indexes); + free(val); +@@ -218,7 +218,7 @@ value lp_set_mat_col(value lp, value i, + } + } + if(non_zero > 0){ +- lpx_set_mat_col((LPX*)lp, Int_val(i) + 1, non_zero, indexes, val); ++ glp_set_mat_col((glp_prob*)lp, Int_val(i) + 1, non_zero, indexes, val); + } + free(indexes); + free(val); +@@ -229,32 +229,30 @@ value lp_set_mat_col(value lp, value i, + value lp_simplex(value lp, value presolve) + { + CAMLparam2(lp,presolve); +- if(Bool_val(presolve)){ +- lpx_set_int_parm((LPX*)lp, LPX_K_PRESOL, 1); +- }else{ +- lpx_set_int_parm((LPX*)lp, LPX_K_PRESOL, 0); +- } ++ glp_smcp params; ++ glp_init_smcp(¶ms); ++ params.presolve = (Bool_val(presolve)) ? GLP_ON : GLP_OFF; + to_dev_null(); +- int status = lpx_simplex((LPX*)lp); ++ int status = glp_simplex((glp_prob*)lp, ¶ms); + to_std_out(); + value val = Val_false; +- if(status == LPX_E_OK){ ++ if(status == 0){ + val = Val_true; +- }else if (status == LPX_E_FAULT){ ++ }else if (status == GLP_EBADB || status == GLP_ECOND || status == GLP_EBOUND){ + //fprintf(stderr, "solving failed \n"); +- }else if (status == LPX_E_OBJLL){ ++ }else if (status == GLP_EOBJLL){ + //fprintf(stderr, "unbounded (lower)\n"); +- }else if (status == LPX_E_OBJUL){ ++ }else if (status == GLP_EOBJUL){ + //fprintf(stderr, "unbounded (upper)\n"); +- }else if (status == LPX_E_ITLIM){ ++ }else if (status == GLP_EITLIM){ + //fprintf(stderr, "iteration limit reached\n"); +- }else if (status == LPX_E_TMLIM){ ++ }else if (status == GLP_ETMLIM){ + //fprintf(stderr, "time limit reached\n"); +- }else if (status == LPX_E_SING){ ++ }else if (status == GLP_ESING){ + fprintf(stderr, "singular or ill-conditionned matrix\n"); +- }else if (status == LPX_E_NOPFS){ ++ }else if (status == GLP_ENOPFS){ + //fprintf(stderr, "no primal solution\n"); +- }else if (status == LPX_E_NODFS){ ++ }else if (status == GLP_ENODFS){ + //fprintf(stderr, "no dual solution\n"); + }else{ + fprintf(stderr, "unknown status: %d\n", status); +@@ -265,28 +263,30 @@ value lp_simplex(value lp, value presolv + value lp_simplex_exact(value lp) + { + CAMLparam1(lp); ++ glp_smcp params; ++ glp_init_smcp(¶ms); + to_dev_null(); +- lpx_simplex((LPX*)lp); +- int status = lpx_exact((LPX*)lp); ++ glp_simplex((glp_prob*)lp, ¶ms); ++ int status = glp_exact((glp_prob*)lp, ¶ms); + to_std_out(); + value val = Val_false; +- if(status == LPX_E_OK){ ++ if(status == 0){ + val = Val_true; +- }else if (status == LPX_E_FAULT){ ++ }else if (status == GLP_EBADB || status == GLP_ECOND || status == GLP_EBOUND){ + //fprintf(stderr, "solving failed \n"); +- }else if (status == LPX_E_OBJLL){ ++ }else if (status == GLP_EOBJLL){ + //fprintf(stderr, "unbounded (lower)\n"); +- }else if (status == LPX_E_OBJUL){ ++ }else if (status == GLP_EOBJUL){ + //fprintf(stderr, "unbounded (upper)\n"); +- }else if (status == LPX_E_ITLIM){ ++ }else if (status == GLP_EITLIM){ + //fprintf(stderr, "iteration limit reached\n"); +- }else if (status == LPX_E_TMLIM){ ++ }else if (status == GLP_ETMLIM){ + //fprintf(stderr, "time limit reached\n"); +- }else if (status == LPX_E_SING){ ++ }else if (status == GLP_ESING){ + fprintf(stderr, "singular or ill-conditionned matrix\n"); +- }else if (status == LPX_E_NOPFS){ ++ }else if (status == GLP_ENOPFS){ + //fprintf(stderr, "no primal solution\n"); +- }else if (status == LPX_E_NODFS){ ++ }else if (status == GLP_ENODFS){ + //fprintf(stderr, "no dual solution\n"); + }else{ + fprintf(stderr, "unknown status: %d\n", status); +@@ -296,7 +296,7 @@ value lp_simplex_exact(value lp) + value lp_get_stat(value lp) + { + CAMLparam1(lp); +- int status = lpx_get_status((LPX*)lp); ++ int status = glp_get_status((glp_prob*)lp); + CAMLreturn (Val_int(status)); + } + +@@ -304,21 +304,21 @@ value lp_get_stat(value lp) + value lp_get_obj_val(value lp) + { + CAMLparam1(lp); +- double status = lpx_get_obj_val((LPX*)lp); ++ double status = glp_get_obj_val((glp_prob*)lp); + CAMLreturn (caml_copy_double(status)); + } + + value lp_get_row_stat(value lp, value i) + { + CAMLparam2(lp,i); +- int status = lpx_get_row_stat((LPX*)lp, Int_val(i) + 1); ++ int status = glp_get_row_stat((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (Val_int(status)); + } + + value lp_get_row_primal(value lp, value i) + { + CAMLparam2(lp,i); +- double val = lpx_get_row_prim((LPX*)lp, Int_val(i) + 1); ++ double val = glp_get_row_prim((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (caml_copy_double(val)); + } + +@@ -327,7 +327,7 @@ value lp_get_rows_primal(value lp, value + CAMLparam3(lp,length,array); + int i; + for(i = 0; i < Int_val(length); ++i){ +- double val = lpx_get_row_prim((LPX*)lp, i + 1); ++ double val = glp_get_row_prim((glp_prob*)lp, i + 1); + Store_double_field(array, i, val); + } + CAMLreturn (Val_unit); +@@ -337,7 +337,7 @@ value lp_get_rows_primal(value lp, value + value lp_get_row_dual(value lp, value i) + { + CAMLparam2(lp,i); +- double val = lpx_get_row_dual((LPX*)lp, Int_val(i) + 1); ++ double val = glp_get_row_dual((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (caml_copy_double(val)); + } + +@@ -346,7 +346,7 @@ value lp_get_rows_dual(value lp, value l + CAMLparam3(lp,length,array); + int i; + for(i = 0; i < Int_val(length); ++i){ +- double val = lpx_get_row_dual((LPX*)lp, i + 1); ++ double val = glp_get_row_dual((glp_prob*)lp, i + 1); + Store_double_field(array, i, val); + } + CAMLreturn (Val_unit); +@@ -355,14 +355,14 @@ value lp_get_rows_dual(value lp, value l + value lp_get_col_stat(value lp, value i) + { + CAMLparam2(lp,i); +- int status = lpx_get_col_stat((LPX*)lp, Int_val(i) + 1); ++ int status = glp_get_col_stat((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (Val_int(status)); + } + + value lp_get_col_primal(value lp, value i) + { + CAMLparam2(lp,i); +- double val = lpx_get_col_prim((LPX*)lp, Int_val(i) + 1); ++ double val = glp_get_col_prim((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (caml_copy_double(val)); + } + +@@ -371,7 +371,7 @@ value lp_get_cols_primal(value lp, value + CAMLparam3(lp,length,array); + int i; + for(i = 0; i < Int_val(length); ++i){ +- double val = lpx_get_col_prim((LPX*)lp, i + 1); ++ double val = glp_get_col_prim((glp_prob*)lp, i + 1); + Store_double_field(array, i, val); + } + CAMLreturn (Val_unit); +@@ -380,7 +380,7 @@ value lp_get_cols_primal(value lp, value + value lp_get_col_dual(value lp, value i) + { + CAMLparam2(lp,i); +- double val = lpx_get_col_dual((LPX*)lp, Int_val(i) + 1); ++ double val = glp_get_col_dual((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (caml_copy_double(val)); + } + +@@ -389,7 +389,7 @@ value lp_get_cols_dual(value lp, value l + CAMLparam3(lp,length,array); + int i; + for(i = 0; i < Int_val(length); ++i){ +- double val = lpx_get_col_dual((LPX*)lp, i + 1); ++ double val = glp_get_col_dual((glp_prob*)lp, i + 1); + Store_double_field(array, i, val); + } + CAMLreturn (Val_unit); +@@ -399,20 +399,20 @@ value lp_interior(value lp) + { + CAMLparam1(lp); + to_dev_null(); +- int status = lpx_interior((LPX*)lp); ++ int status = glp_interior((glp_prob*)lp, NULL); + to_std_out(); + value val = Val_false; +- if(status == LPX_E_OK){ ++ if(status == 0){ + val = Val_true; +- }else if (status == LPX_E_FAULT){ ++ }else if (status == GLP_EFAIL){ + //fprintf(stderr, "solving failed \n"); +- }else if (status == LPX_E_NOFEAS){ ++ }else if (status == GLP_ENOFEAS){ + //fprintf(stderr, "unfeasible system\n"); +- }else if (status == LPX_E_NOCONV){ ++ }else if (status == GLP_ENOCVG){ + fprintf(stderr, "slow convergence (or diverge)\n"); +- }else if (status == LPX_E_ITLIM){ ++ }else if (status == GLP_EITLIM){ + fprintf(stderr, "iteration limit reached\n"); +- }else if (status == LPX_E_INSTAB){ ++ }else if (status == GLP_EINSTAB){ + fprintf(stderr, "numerical instability\n"); + }else{ + fprintf(stderr, "unknown status: %d\n", status); +@@ -423,14 +423,14 @@ value lp_interior(value lp) + value lp_ipt_obj_val(value lp) + { + CAMLparam1(lp); +- double status = lpx_ipt_obj_val((LPX*)lp); ++ double status = glp_ipt_obj_val((glp_prob*)lp); + CAMLreturn (caml_copy_double(status)); + } + + value lp_ipt_row_primal(value lp, value i) + { + CAMLparam2(lp,i); +- double val = lpx_ipt_row_prim((LPX*)lp, Int_val(i) + 1); ++ double val = glp_ipt_row_prim((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (caml_copy_double(val)); + } + +@@ -439,7 +439,7 @@ value lp_ipt_rows_primal(value lp, value + CAMLparam3(lp,length,array); + int i; + for(i = 0; i < Int_val(length); ++i){ +- double val = lpx_ipt_row_prim((LPX*)lp, i + 1); ++ double val = glp_ipt_row_prim((glp_prob*)lp, i + 1); + Store_double_field(array, i, val); + } + CAMLreturn (Val_unit); +@@ -448,7 +448,7 @@ value lp_ipt_rows_primal(value lp, value + value lp_ipt_row_dual(value lp, value i) + { + CAMLparam2(lp,i); +- double val = lpx_ipt_row_dual((LPX*)lp, Int_val(i) + 1); ++ double val = glp_ipt_row_dual((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (caml_copy_double(val)); + } + +@@ -457,7 +457,7 @@ value lp_ipt_rows_dual(value lp, value l + CAMLparam3(lp,length,array); + int i; + for(i = 0; i < Int_val(length); ++i){ +- double val = lpx_ipt_row_dual((LPX*)lp, i + 1); ++ double val = glp_ipt_row_dual((glp_prob*)lp, i + 1); + Store_double_field(array, i, val); + } + CAMLreturn (Val_unit); +@@ -466,7 +466,7 @@ value lp_ipt_rows_dual(value lp, value l + value lp_ipt_col_primal(value lp, value i) + { + CAMLparam2(lp,i); +- double val = lpx_ipt_col_prim((LPX*)lp, Int_val(i) + 1); ++ double val = glp_ipt_col_prim((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (caml_copy_double(val)); + } + +@@ -475,7 +475,7 @@ value lp_ipt_cols_primal(value lp, value + CAMLparam3(lp,length,array); + int i; + for(i = 0; i < Int_val(length); ++i){ +- double val = lpx_ipt_col_prim((LPX*)lp, i + 1); ++ double val = glp_ipt_col_prim((glp_prob*)lp, i + 1); + Store_double_field(array, i, val); + } + CAMLreturn (Val_unit); +@@ -484,7 +484,7 @@ value lp_ipt_cols_primal(value lp, value + value lp_ipt_col_dual(value lp, value i) + { + CAMLparam2(lp,i); +- double val = lpx_ipt_col_dual((LPX*)lp, Int_val(i) + 1); ++ double val = glp_ipt_col_dual((glp_prob*)lp, Int_val(i) + 1); + CAMLreturn (caml_copy_double(val)); + } + +@@ -493,7 +493,7 @@ value lp_ipt_cols_dual(value lp, value l + CAMLparam3(lp,length,array); + int i; + for(i = 0; i < Int_val(length); ++i){ +- double val = lpx_ipt_col_dual((LPX*)lp, i + 1); ++ double val = glp_ipt_col_dual((glp_prob*)lp, i + 1); + Store_double_field(array, i, val); + } + CAMLreturn (Val_unit); +@@ -502,7 +502,7 @@ value lp_ipt_cols_dual(value lp, value l + value lp_dump_problem(value lp) + { + CAMLparam1(lp); +- lpx_print_prob((LPX*)lp, "lp_error.debug"); +- lpx_write_cpxlp((LPX*)lp, "cpxlp_error.debug"); ++ glp_write_lp((glp_prob*)lp, NULL, "lp_error.debug"); ++ glp_write_lp((glp_prob*)lp, NULL, "cpxlp_error.debug"); + CAMLreturn (Val_unit); + } diff --git a/csisat-picosat.patch b/csisat-picosat.patch new file mode 100644 index 0000000..1bfa6b0 --- /dev/null +++ b/csisat-picosat.patch @@ -0,0 +1,127 @@ +--- ./pico_ml_wrapper/src/camlpico.c.orig 2008-07-08 22:38:01.000000000 -0600 ++++ ./pico_ml_wrapper/src/camlpico.c 2013-07-31 16:11:40.000000000 -0600 +@@ -26,6 +26,8 @@ + #include + #include + ++static PicoSAT *my_picosat; ++ + /* the methods comment were directly taken from 'picosat.h' */ + + CAMLprim value unknown(){ return Val_int(PICOSAT_UNKNOWN);} +@@ -35,13 +37,14 @@ CAMLprim value unsatisfiable(){ return V + + CAMLprim value init(value unit) + { +- picosat_init(); ++ my_picosat = picosat_init(); + return Val_unit; + } + + CAMLprim value reset(value unit) + { +- picosat_reset(); ++ picosat_reset(my_picosat); ++ my_picosat = NULL; + return Val_unit; + } + +@@ -55,7 +58,7 @@ CAMLprim value reset(value unit) + */ + CAMLprim value set_seed(value seed) + { +- picosat_set_seed(Unsigned_int_val(seed)); ++ picosat_set_seed(my_picosat, Unsigned_int_val(seed)); + return Val_unit; + } + +@@ -65,7 +68,7 @@ CAMLprim value set_seed(value seed) + */ + CAMLprim value enable_trace(value unit) + { +- picosat_enable_trace_generation(); ++ picosat_enable_trace_generation(my_picosat); + return Val_unit; + } + +@@ -76,7 +79,7 @@ CAMLprim value enable_trace(value unit) + */ + CAMLprim value adjust(value n) + { +- picosat_adjust(Int_val(n)); ++ picosat_adjust(my_picosat, Int_val(n)); + return Val_unit; + } + +@@ -85,7 +88,7 @@ CAMLprim value adjust(value n) + */ + CAMLprim value second(value unit) + { +- return caml_copy_double(picosat_seconds()); ++ return caml_copy_double(picosat_seconds(my_picosat)); + } + + /*------------------------------------------------------------------------*/ +@@ -95,7 +98,7 @@ CAMLprim value second(value unit) + */ + CAMLprim value add(value i) + { +- picosat_add(Int_val(i)); ++ picosat_add(my_picosat, Int_val(i)); + return Val_unit; + } + +@@ -106,7 +109,7 @@ CAMLprim value add(value i) + */ + CAMLprim value assume(value i) + { +- picosat_assume(Int_val(i)); ++ picosat_assume(my_picosat, Int_val(i)); + return Val_unit; + } + +@@ -117,7 +120,7 @@ CAMLprim value assume(value i) + */ + CAMLprim value sat(value limit) + { +- return Val_int(picosat_sat(Int_val(limit))); ++ return Val_int(picosat_sat(my_picosat, Int_val(limit))); + } + + /* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE', then +@@ -127,7 +130,7 @@ CAMLprim value sat(value limit) + */ + CAMLprim value deref(value lit) + { +- return Val_int(picosat_deref(Int_val(lit))); ++ return Val_int(picosat_deref(my_picosat, Int_val(lit))); + } + + /* A cheap way of determining an over-approximation of a variable core is to +@@ -138,7 +141,7 @@ CAMLprim value deref(value lit) + */ + CAMLprim value usedlit(value lit) + { +- return Val_int(picosat_usedlit(Int_val(lit))); ++ return Val_int(picosat_usedlit(my_picosat, Int_val(lit))); + } + + /*------------------------------------------------------------------------*/ +@@ -155,7 +158,7 @@ CAMLprim value usedlit(value lit) + */ + CAMLprim value corelit(value lit) + { +- return Val_int(picosat_corelit(Int_val(lit))); ++ return Val_int(picosat_corelit(my_picosat, Int_val(lit))); + } + + //#include +@@ -165,7 +168,7 @@ value get_proof(value unit) + { + CAMLparam0(); + CAMLlocal1 (array); +- int* proof = picosat_get_proof(); ++ int* proof = picosat_get_proof(my_picosat); + int size = 0; + while(proof[size] != EOP){ + size++; diff --git a/csisat.spec b/csisat.spec index b3c896c..76fa4a1 100644 --- a/csisat.spec +++ b/csisat.spec @@ -1,6 +1,6 @@ Name: csisat Version: 1.2 -Release: 11%{?dist} +Release: 12%{?dist} Summary: Tool for LA+EUF Interpolation Group: Applications/Engineering @@ -10,7 +10,11 @@ Source0: http://csisat.googlecode.com/files/%{name}-%{version}.zip # This patch has not been sent upstream. Upstream wishes to distribute the # picosat sources with their code. This patch builds with the system picosat # instead, and also adds missing dependencies so that parallel make works. -Patch0: csisat-makefile.patch +Patch0: %{name}-makefile.patch +# Adapt to new glpk API +Patch1: %{name}-glpk.patch +# Adapt to new picosat API +Patch2: %{name}-picosat.patch BuildRequires: glpk-devel, ocaml, picosat-devel, subversion @@ -32,10 +36,16 @@ efficiency of a SAT solver to reason about the boolean structure. %prep %setup -q %patch0 +%patch1 +%patch2 # Make sure we don't use the bundled version of picosat rm -fr picosat-* +# We need the picosat version with trace enabled +sed -i 's/lpicosat/lpicosat-trace/' \ + Makefile pico_ml_wrapper/Makefile pico_ml_wrapper/compile.sh + # Get rid of inappropriate executable bits chmod a-x *.txt find . -name \*.c | xargs chmod a-x @@ -54,6 +64,9 @@ cp -p bin/* $RPM_BUILD_ROOT%{_bindir} %{_bindir}/csisatServer %changelog +* Wed Jul 31 2013 Jerry James - 1.2-12 +- Rebuild for new glpk and new picosat + * Sat Feb 2 2013 Jerry James - 1.2-11 - Rebuild for new glpk