[prev in list] [next in list] [prev in thread] [next in thread]
List: fedora-extras-commits
Subject: [csisat] Rebuild for new glpk and new picosat.
From: Jerry James <jjames () fedoraproject ! org>
Date: 2013-07-31 22:50:21
Message-ID: 20130731225021.AD1E123E64 () pkgs01 ! phx2 ! fedoraproject ! org
[Download RAW message or body]
commit 1232bbad68a899de4a45365987e8673a540de171
Author: Jerry James <jamesjer@betterlinux.com>
Date: Wed Jul 31 16:50:07 2013 -0600
Rebuild for new glpk and new picosat.
csisat-glpk.patch | 469 ++++++++++++++++++++++++++++++++++++++++++++++++++
csisat-picosat.patch | 127 ++++++++++++++
csisat.spec | 17 ++-
3 files changed, 611 insertions(+), 2 deletions(-)
---
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 <caml/memory.h>
+ #include <picosat.h>
+
++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 <stdio.h>
+@@ -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 <loganjerry@gmail.com> - 1.2-12
+- Rebuild for new glpk and new picosat
+
* Sat Feb 2 2013 Jerry James <loganjerry@gmail.com> - 1.2-11
- Rebuild for new glpk
--
scm-commits mailing list
scm-commits@lists.fedoraproject.org
https://admin.fedoraproject.org/mailman/listinfo/scm-commits
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic