From 1487ff59f9b42217c43e663a92becca3e75e07aa Mon Sep 17 00:00:00 2001 From: Jerry James Date: Oct 07 2015 03:34:56 +0000 Subject: Dead upstream, no longer used by anything --- diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 10067ef..0000000 --- a/.gitignore +++ /dev/null @@ -1 +0,0 @@ -csisat-1.2.zip diff --git a/csisat-glpk.patch b/csisat-glpk.patch deleted file mode 100644 index 5e3f617..0000000 --- a/csisat-glpk.patch +++ /dev/null @@ -1,469 +0,0 @@ ---- ./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-makefile.patch b/csisat-makefile.patch deleted file mode 100644 index a256f53..0000000 --- a/csisat-makefile.patch +++ /dev/null @@ -1,191 +0,0 @@ -diff -up ./Makefile.ORIG ./Makefile ---- ./Makefile.ORIG 2008-07-08 22:38:05.000000000 -0600 -+++ ./Makefile 2010-01-19 14:23:02.065649539 -0700 -@@ -65,8 +65,8 @@ TARGET = bin/csisat - OCAML_LIB = libcsisat - - --all: glpk pico picosat server $(FILES) $(MAIN) lib -- $(OCAML_OPT_C) $(COMPILE_FLAG) -o $(TARGET) $(LIBS) $(GLPK) $(PWD)/picosat-632/libpicosat.a $(FILES) $(MAIN) -+all: glpk pico server $(FILES) $(MAIN) lib -+ $(OCAML_OPT_C) $(COMPILE_FLAG) -o $(TARGET) $(LIBS) $(GLPK) $(FILES) $(MAIN) - $(shell sed -i 's/Version .*\\n\\n/Version 1.2 (Rev REV, Build DATE)\.\\n\\n/g' $(SRC)/csisatConfig.ml) - - VERSION = $(shell svnversion) -@@ -126,12 +126,12 @@ $(OBJ)/%.cmx: $(SRC)/%.ml - - lib: $(LIB)/$(OCAML_LIB).cma $(LIB)/$(OCAML_LIB).cmxa - --$(LIB)/$(OCAML_LIB).cma: $(OCAML_LIB_OBJ:%=%.cmo) -+$(LIB)/$(OCAML_LIB).cma: $(OCAML_LIB_OBJ:%=%.cmo) $(FILES) - @echo Creating OCAML \(byte code\) library $@ - @mkdir -p $(LIB) - $(OCAML_LD) $(OCAML_LD_FLAGS) -a -o $@ $(patsubst %.cmx, %.cmo, $(FILES)) - --$(LIB)/$(OCAML_LIB).cmxa $(LIB)/$(OCAML_LIB).a: $(OCAML_LIB_OBJ:%=%.cmx) -+$(LIB)/$(OCAML_LIB).cmxa $(LIB)/$(OCAML_LIB).a: $(OCAML_LIB_OBJ:%=%.cmx) $(FILES) - @echo Creating OCAML \(native code\) library $@ - @mkdir -p $(LIB) - $(OCAML_OPT_LD) $(OCAML_LD_FLAGS) -a -o $@ $(FILES) -@@ -155,26 +155,136 @@ odoc: - $(patsubst $(OBJ)/%, $(SRC)/%, $(patsubst %.cmx, %.ml, $(FILES))) - - glpk: -- cd glpk_ml_wrapper; make -+ cd glpk_ml_wrapper; $(MAKE) - @mkdir -p $(LIB) - cp glpk_ml_wrapper/libcamlglpk.a $(LIB)/ - - pico: -- cd pico_ml_wrapper; make -+ cd pico_ml_wrapper; $(MAKE) - @mkdir -p $(LIB) - cp pico_ml_wrapper/libcamlpico.a $(LIB)/ - --picosat: -- cd picosat-632; ./configure; make -- @mkdir -p $(LIB) -- cp picosat-632/libpicosat.a $(LIB)/ -- - server: -- cd server; make -+ cd server; $(MAKE) - - clean: - $(RM) $(TARGET) $(OBJ)/* $(LIB)/* -- cd glpk_ml_wrapper; make clean -- cd pico_ml_wrapper; make clean -- cd picosat-632; make clean -- cd server; make clean -+ cd glpk_ml_wrapper; $(MAKE) clean -+ cd pico_ml_wrapper; $(MAKE) clean -+ cd server; $(MAKE) clean -+ -+# Dependencies from ocamldep: -+$(OBJ)/csisatAstUtil.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatOrdSet.cmo \ -+ $(OBJ)/csisatMessage.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatAstUtil.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatOrdSet.cmx \ -+ $(OBJ)/csisatMessage.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatClpLI.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatMessage.cmo \ -+ $(OBJ)/csisatMatrix.cmo $(OBJ)/csisatLIUtils.cmo \ -+ $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatClpLI.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatMessage.cmx \ -+ $(OBJ)/csisatMatrix.cmx $(OBJ)/csisatLIUtils.cmx \ -+ $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatConfig.cmo: $(OBJ)/csisatSatPL.cmo $(OBJ)/csisatMessage.cmo \ -+ $(OBJ)/csisatLIUtils.cmo -+$(OBJ)/csisatConfig.cmx: $(OBJ)/csisatSatPL.cmx $(OBJ)/csisatMessage.cmx \ -+ $(OBJ)/csisatLIUtils.cmx -+$(OBJ)/csisatDag.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatOrdSet.cmo \ -+ $(OBJ)/csisatMessage.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatDag.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatOrdSet.cmx \ -+ $(OBJ)/csisatMessage.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatDpllClause.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatAstUtil.cmo \ -+ $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatDpllClause.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatAstUtil.cmx \ -+ $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatDpllCore.cmo: $(OBJ)/csisatSatInterface.cmo \ -+ $(OBJ)/csisatOrdSet.cmo $(OBJ)/csisatMessage.cmo \ -+ $(OBJ)/csisatDpllProof.cmo $(OBJ)/csisatDpllClause.cmo \ -+ $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatDpllCore.cmx: $(OBJ)/csisatSatInterface.cmx \ -+ $(OBJ)/csisatOrdSet.cmx $(OBJ)/csisatMessage.cmx \ -+ $(OBJ)/csisatDpllProof.cmx $(OBJ)/csisatDpllClause.cmx \ -+ $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatDpllProof.cmo: $(OBJ)/csisatDpllClause.cmo \ -+ $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatDpllProof.cmx: $(OBJ)/csisatDpllClause.cmx \ -+ $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatFociParse.cmo: $(OBJ)/csisatFociParse.cmi $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatFociParse.cmx: $(OBJ)/csisatFociParse.cmi $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatFociPrinter.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatFociPrinter.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatInfixParse.cmo: $(OBJ)/csisatInfixParse.cmi $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatInfixParse.cmx: $(OBJ)/csisatInfixParse.cmi $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatInterpolate.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatSatUIF.cmo \ -+ $(OBJ)/csisatSatPL.cmo $(OBJ)/csisatSatLI.cmo $(OBJ)/csisatOrdSet.cmo \ -+ $(OBJ)/csisatNelsonOppen.cmo $(OBJ)/csisatMessage.cmo \ -+ $(OBJ)/csisatDpllProof.cmo $(OBJ)/csisatDag.cmo \ -+ $(OBJ)/csisatClpLI.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatInterpolate.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatSatUIF.cmx \ -+ $(OBJ)/csisatSatPL.cmx $(OBJ)/csisatSatLI.cmx $(OBJ)/csisatOrdSet.cmx \ -+ $(OBJ)/csisatNelsonOppen.cmx $(OBJ)/csisatMessage.cmx \ -+ $(OBJ)/csisatDpllProof.cmx $(OBJ)/csisatDag.cmx \ -+ $(OBJ)/csisatClpLI.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatLIUtils.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatOrdSet.cmo \ -+ $(OBJ)/csisatMessage.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatLIUtils.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatOrdSet.cmx \ -+ $(OBJ)/csisatMessage.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatMain.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatSatPL.cmo \ -+ $(OBJ)/csisatOrdSet.cmo $(OBJ)/csisatNelsonOppen.cmo \ -+ $(OBJ)/csisatMessage.cmo $(OBJ)/csisatLIUtils.cmo \ -+ $(OBJ)/csisatInterpolate.cmo $(OBJ)/csisatFociPrinter.cmo \ -+ $(OBJ)/csisatConfig.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatMain.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatSatPL.cmx \ -+ $(OBJ)/csisatOrdSet.cmx $(OBJ)/csisatNelsonOppen.cmx \ -+ $(OBJ)/csisatMessage.cmx $(OBJ)/csisatLIUtils.cmx \ -+ $(OBJ)/csisatInterpolate.cmx $(OBJ)/csisatFociPrinter.cmx \ -+ $(OBJ)/csisatConfig.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatMatrix.cmo: $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatMatrix.cmx: $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatNelsonOppen.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatSatUIF.cmo \ -+ $(OBJ)/csisatSatLI.cmo $(OBJ)/csisatOrdSet.cmo \ -+ $(OBJ)/csisatMessage.cmo $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatNelsonOppen.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatSatUIF.cmx \ -+ $(OBJ)/csisatSatLI.cmx $(OBJ)/csisatOrdSet.cmx \ -+ $(OBJ)/csisatMessage.cmx $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatPicoInterface.cmo: $(OBJ)/csisatSatInterface.cmo \ -+ $(OBJ)/csisatMessage.cmo $(OBJ)/csisatDpllProof.cmo \ -+ $(OBJ)/csisatDpllClause.cmo $(OBJ)/csisatAstUtil.cmo \ -+ $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatPicoInterface.cmx: $(OBJ)/csisatSatInterface.cmx \ -+ $(OBJ)/csisatMessage.cmx $(OBJ)/csisatDpllProof.cmx \ -+ $(OBJ)/csisatDpllClause.cmx $(OBJ)/csisatAstUtil.cmx \ -+ $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatSatInterface.cmo: $(OBJ)/csisatDpllProof.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatSatInterface.cmx: $(OBJ)/csisatDpllProof.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatSatLI.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatMessage.cmo \ -+ $(OBJ)/csisatMatrix.cmo $(OBJ)/csisatLIUtils.cmo \ -+ $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatSatLI.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatMessage.cmx \ -+ $(OBJ)/csisatMatrix.cmx $(OBJ)/csisatLIUtils.cmx \ -+ $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatSatPL.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatPicoInterface.cmo \ -+ $(OBJ)/csisatNelsonOppen.cmo $(OBJ)/csisatDpllProof.cmo \ -+ $(OBJ)/csisatDpllCore.cmo $(OBJ)/csisatDpllClause.cmo \ -+ $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatSatPL.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatPicoInterface.cmx \ -+ $(OBJ)/csisatNelsonOppen.cmx $(OBJ)/csisatDpllProof.cmx \ -+ $(OBJ)/csisatDpllCore.cmx $(OBJ)/csisatDpllClause.cmx \ -+ $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatSatUIF.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatOrdSet.cmo \ -+ $(OBJ)/csisatMessage.cmo $(OBJ)/csisatDag.cmo \ -+ $(OBJ)/csisatAstUtil.cmo $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatSatUIF.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatOrdSet.cmx \ -+ $(OBJ)/csisatMessage.cmx $(OBJ)/csisatDag.cmx \ -+ $(OBJ)/csisatAstUtil.cmx $(OBJ)/csisatAst.cmx -+$(OBJ)/csisatTests.cmo: $(OBJ)/csisatUtils.cmo $(OBJ)/csisatSatUIF.cmo \ -+ $(OBJ)/csisatSatPL.cmo $(OBJ)/csisatSatLI.cmo \ -+ $(OBJ)/csisatNelsonOppen.cmo $(OBJ)/csisatMessage.cmo \ -+ $(OBJ)/csisatLIUtils.cmo $(OBJ)/csisatInterpolate.cmo \ -+ $(OBJ)/csisatFociPrinter.cmo $(OBJ)/csisatAstUtil.cmo \ -+ $(OBJ)/csisatAst.cmo -+$(OBJ)/csisatTests.cmx: $(OBJ)/csisatUtils.cmx $(OBJ)/csisatSatUIF.cmx \ -+ $(OBJ)/csisatSatPL.cmx $(OBJ)/csisatSatLI.cmx \ -+ $(OBJ)/csisatNelsonOppen.cmx $(OBJ)/csisatMessage.cmx \ -+ $(OBJ)/csisatLIUtils.cmx $(OBJ)/csisatInterpolate.cmx \ -+ $(OBJ)/csisatFociPrinter.cmx $(OBJ)/csisatAstUtil.cmx \ -+ $(OBJ)/csisatAst.cmx -diff -up ./pico_ml_wrapper/Makefile.ORIG ./pico_ml_wrapper/Makefile ---- ./pico_ml_wrapper/Makefile.ORIG 2008-07-08 22:38:01.000000000 -0600 -+++ ./pico_ml_wrapper/Makefile 2010-01-19 14:16:01.399524477 -0700 -@@ -1,7 +1,7 @@ - CC=gcc - CFLAGS= -O2 -Wall --INCLUDE= -I../picosat-632 --LIBS= -lpicosat -L../picosat-632 -+INCLUDE= -+LIBS= -lpicosat-trace - RM = /bin/rm -f - - SRC = src/camlpico.c diff --git a/csisat-picosat.patch b/csisat-picosat.patch deleted file mode 100644 index 1bfa6b0..0000000 --- a/csisat-picosat.patch +++ /dev/null @@ -1,127 +0,0 @@ ---- ./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 deleted file mode 100644 index d704d2f..0000000 --- a/csisat.spec +++ /dev/null @@ -1,124 +0,0 @@ -Name: csisat -Version: 1.2 -Release: 17%{?dist} -Summary: Tool for LA+EUF Interpolation - -Group: Applications/Engineering -License: ASL 2.0 -URL: http://csisat.googlecode.com/ -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: %{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 - -%description -CSIsat reads a set of mathematical formulas that may combine variables, -addition, multiplication, comparisons (<,>, etc.), as well as boolean -expressions (and, or, not). It determines if it is possible to set the -variables to values so that the set of formulas are all simultaneously true -(if it can, then the set of formulas is "satisfiable"). - -More technically, CSIsat is an interpolating decision procedure for the -quantifier-free theory of rational linear arithmetic (LA) and equality with -uninterpreted function (EUF) symbols. This implementation combines the -efficiency of linear programming for solving the arithmetic part with the -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 - -# Silence warnings -svn upgrade - -%build -# FIXME: Parallel make sometimes fails -make CFLAGS="$RPM_OPT_FLAGS -I%{_libdir}/ocaml -I%{_includedir}/glpk" - -%install -mkdir -p $RPM_BUILD_ROOT%{_bindir} -cp -p bin/* $RPM_BUILD_ROOT%{_bindir} - -%files -%doc ReadMe.txt ToDo.txt server/README -%license License.txt License_Apache-2.0.txt -%{_bindir}/csisat -%{_bindir}/csisatServer - -%changelog -* Wed Jun 17 2015 Fedora Release Engineering - 1.2-17 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild - -* Fri Nov 7 2014 Jerry James - 1.2-16 -- Rebuild for picosat 960 -- Fix license handling - -* Sat Aug 16 2014 Fedora Release Engineering - 1.2-15 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild - -* Sat Jun 07 2014 Fedora Release Engineering - 1.2-14 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild - -* Fri Apr 18 2014 Jerry James - 1.2-13 -- Remove ocaml_arches macro (bz 1087794) - -* 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 - -* Thu Dec 13 2012 Jerry James - 1.2-10 -- Rebuild for OCaml 4.00.1 - -* Mon Aug 20 2012 Jerry James - 1.2-9 -- Rebuild for new picosat - -* Wed Jul 18 2012 Fedora Release Engineering - 1.2-8 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild - -* Fri Jan 6 2012 Jerry James - 1.2-7 -- Rebuild for GCC 4.7 and Ocaml 3.12.1 - -* Mon Nov 14 2011 Jerry James - 1.2-6 -- Change supported arches list to %%{ocaml_arches} -- Drop unnecessary spec file elements (%%clean, etc.) - -* Tue Feb 08 2011 Fedora Release Engineering - 1.2-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild - -* Mon Jan 31 2011 Jerry James - 1.2-4 -- Don't use the OCaml dependency generators, which find no dependencies -- Update list of supported arches from the ocaml spec file - -* Thu Jan 27 2011 Jerry James - 1.2-3 -- Rebuild for new picosat and new ocaml -- BR subversion to eliminate build noise from svnversion failing -- Parallel make still isn't fixed; disable until I can figure it out - -* Tue Jan 19 2010 Jerry James - 1.2-2 -- Fix parallel make -- Less opaque description - -* Wed Sep 2 2009 Jerry James - 1.2-1 -- Initial RPM diff --git a/dead.package b/dead.package new file mode 100644 index 0000000..f983fcc --- /dev/null +++ b/dead.package @@ -0,0 +1 @@ +Dead upstream, no longer used by anything diff --git a/sources b/sources deleted file mode 100644 index f366332..0000000 --- a/sources +++ /dev/null @@ -1 +0,0 @@ -fa0fec35362b452ba564f0f82086295f csisat-1.2.zip