From e034e268f984394e84f350a83efc327b448eaa9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Sat, 25 Jan 2014 00:03:52 +0100
Subject: [PATCH] Add GMLMIP-0.1 tool
---
GMLMIP-0.1/README.txt | 79 ++++++
GMLMIP-0.1/clean.sh | 15 +
GMLMIP-0.1/compile.sh | 15 +
GMLMIP-0.1/formulas/GML_formula.cpp | 80 ++++++
GMLMIP-0.1/formulas/GML_formula.h | 14 +
GMLMIP-0.1/formulas/PML_formula.cpp | 102 +++++++
GMLMIP-0.1/formulas/PML_formula.h | 14 +
GMLMIP-0.1/formulas/formula.cpp | 284 +++++++++++++++++++
GMLMIP-0.1/formulas/formula.h | 159 +++++++++++
GMLMIP-0.1/formulas/makefile | 22 ++
GMLMIP-0.1/formulas/rational.cpp | 29 ++
GMLMIP-0.1/formulas/rational.h | 26 ++
GMLMIP-0.1/formulas/satisfyingassignment.cpp | 64 +++++
GMLMIP-0.1/formulas/satisfyingassignment.h | 26 ++
GMLMIP-0.1/input | 2 +
GMLMIP-0.1/main.cpp | 70 +++++
GMLMIP-0.1/makefile | 15 +
GMLMIP-0.1/parser/makefile | 34 +++
GMLMIP-0.1/parser/mlf-driver.cpp | 60 ++++
GMLMIP-0.1/parser/mlf-driver.h | 62 ++++
GMLMIP-0.1/parser/mlf-parser.yy | 111 ++++++++
GMLMIP-0.1/parser/mlf-scanner.ll | 124 ++++++++
GMLMIP-0.1/parser/test.cpp | 16 ++
GMLMIP-0.1/rand.pl | 98 +++++++
GMLMIP-0.1/rules/GML_premise.cpp | 251 ++++++++++++++++
GMLMIP-0.1/rules/GML_premise.h | 33 +++
GMLMIP-0.1/rules/PML_premise.cpp | 17 ++
GMLMIP-0.1/rules/PML_premise.h | 26 ++
GMLMIP-0.1/rules/makefile | 34 +++
GMLMIP-0.1/rules/node.cpp | 46 +++
GMLMIP-0.1/rules/node.h | 34 +++
GMLMIP-0.1/rules/premise.cpp | 110 +++++++
GMLMIP-0.1/rules/premise.h | 76 +++++
GMLMIP-0.1/rules/radixtree.cpp | 55 ++++
GMLMIP-0.1/rules/radixtree.h | 36 +++
GMLMIP-0.1/rules/setofconclusions.cpp | 35 +++
GMLMIP-0.1/rules/setofconclusions.h | 38 +++
GMLMIP-0.1/rules/sizefunctions.cpp | 26 ++
GMLMIP-0.1/rules/sizefunctions.h | 11 +
GMLMIP-0.1/rules/test.cpp | 60 ++++
GMLMIP-0.1/rules/valuation.cpp | 71 +++++
GMLMIP-0.1/rules/valuation.h | 34 +++
GMLMIP-0.1/satisfyingstack.h | 12 +
GMLMIP-0.1/timeoutwrapper.sh | 91 ++++++
INSTALL | 8 +-
45 files changed, 2624 insertions(+), 1 deletion(-)
create mode 100644 GMLMIP-0.1/README.txt
create mode 100755 GMLMIP-0.1/clean.sh
create mode 100755 GMLMIP-0.1/compile.sh
create mode 100644 GMLMIP-0.1/formulas/GML_formula.cpp
create mode 100644 GMLMIP-0.1/formulas/GML_formula.h
create mode 100644 GMLMIP-0.1/formulas/PML_formula.cpp
create mode 100644 GMLMIP-0.1/formulas/PML_formula.h
create mode 100644 GMLMIP-0.1/formulas/formula.cpp
create mode 100644 GMLMIP-0.1/formulas/formula.h
create mode 100644 GMLMIP-0.1/formulas/makefile
create mode 100644 GMLMIP-0.1/formulas/rational.cpp
create mode 100644 GMLMIP-0.1/formulas/rational.h
create mode 100644 GMLMIP-0.1/formulas/satisfyingassignment.cpp
create mode 100644 GMLMIP-0.1/formulas/satisfyingassignment.h
create mode 100644 GMLMIP-0.1/input
create mode 100644 GMLMIP-0.1/main.cpp
create mode 100644 GMLMIP-0.1/makefile
create mode 100644 GMLMIP-0.1/parser/makefile
create mode 100644 GMLMIP-0.1/parser/mlf-driver.cpp
create mode 100644 GMLMIP-0.1/parser/mlf-driver.h
create mode 100644 GMLMIP-0.1/parser/mlf-parser.yy
create mode 100644 GMLMIP-0.1/parser/mlf-scanner.ll
create mode 100644 GMLMIP-0.1/parser/test.cpp
create mode 100644 GMLMIP-0.1/rand.pl
create mode 100644 GMLMIP-0.1/rules/GML_premise.cpp
create mode 100644 GMLMIP-0.1/rules/GML_premise.h
create mode 100644 GMLMIP-0.1/rules/PML_premise.cpp
create mode 100644 GMLMIP-0.1/rules/PML_premise.h
create mode 100644 GMLMIP-0.1/rules/makefile
create mode 100644 GMLMIP-0.1/rules/node.cpp
create mode 100644 GMLMIP-0.1/rules/node.h
create mode 100644 GMLMIP-0.1/rules/premise.cpp
create mode 100644 GMLMIP-0.1/rules/premise.h
create mode 100644 GMLMIP-0.1/rules/radixtree.cpp
create mode 100644 GMLMIP-0.1/rules/radixtree.h
create mode 100644 GMLMIP-0.1/rules/setofconclusions.cpp
create mode 100644 GMLMIP-0.1/rules/setofconclusions.h
create mode 100644 GMLMIP-0.1/rules/sizefunctions.cpp
create mode 100644 GMLMIP-0.1/rules/sizefunctions.h
create mode 100644 GMLMIP-0.1/rules/test.cpp
create mode 100644 GMLMIP-0.1/rules/valuation.cpp
create mode 100644 GMLMIP-0.1/rules/valuation.h
create mode 100644 GMLMIP-0.1/satisfyingstack.h
create mode 100755 GMLMIP-0.1/timeoutwrapper.sh
diff --git a/GMLMIP-0.1/README.txt b/GMLMIP-0.1/README.txt
new file mode 100644
index 0000000..f31b51f
--- /dev/null
+++ b/GMLMIP-0.1/README.txt
@@ -0,0 +1,79 @@
+===============================
+Author: William Snell
+Check http://project.williamsnell.co.uk for future updates.
+================================
+
+Requirements:
+
+GNU LPK, Flex, Bison, Googlesparsehash package, BuDDy BDD package.
+
+(Extensively tested with GNU-LPK 4.38)
+
+=================================
+Compiling:
+
+To compile you will need to edit the makefiles in the sub-folders and this folder to point to the location of your compiler/bison/flex.
+
+Also need to edit the include directory and linking directories in all 4 make files to point to where you have installed GLPK, sparsehash and BuDDy. If you install these properly in /bin /usr (unlike the lab set-up) you should be able to just remove these parts and have it compile fine.
+
+Then if you run the compile.sh script, everything should compile properly for you.
+
+=================================
+Usage:
+
+Input is written in a separate file and then this file is is passed as an argument on the command line.
+
+./main input
+
+You can use the -v flag for output. At each step of the top level tableau calculus algorithm it tells you how many satisfying assignments and how many rules it has found.
+
+Included is Dmitry V Golovashkin's timeout script. The following would run the program on the input file with a timeout of 300 seconds.
+
+./timeoutwrapper.sh -t 300 ./src/main input
+
+
+=================================
+Input file specification:
+
+First we specify which logic then use the following notation:
+
+<a> GML diamond ('more than a successors ...')
+[a] GML box ('fails at most a times ...')
+<a/b> PML diamond
+[a/b] PML box
+~ not
+v or
+& and
+(
+)
+
+Examples:
+
+Logic:PML
+<1/2>p0 & ~<1/4>p2 v [1/8]p3
+
+Logic:GML
+<1>p0 & <1>(p0 v p0)
+
+
+=================================
+Known Issues & Notes:
+
+1) The following warning is generated by the C code generated by flex.
+ position.hh:136: warning: suggest parentheses around ‘&&’ within ‘||’
+
+2) Use of deprecated header <ext/hash_map>.
+
+3) You may need to alter the line "using __gnu_cxx::hash;" line in formula.h depending on your compiler.
+
+4) I received "./main: error while loading shared libraries: libbdd.so.0: cannot open shared object file: No such file or directory" errors.
+Fixed by adding "export LD_LIBRARY_PATH=~/lib/lib:$LD_LIBRARY_PATH" to my .bashrc file. Where ~/lib/lib is where I locally installed the required libraries. (No root access for lab machines.)
+
+5) If you receive error "BDD error: unknown variable" you have not declared enough variables in the BDD initialisation in main.cpp. The line "bdd_setvarnum(int)" needs increasing.
+
+6) What report describes as TruthAssignment class is implemented as Valuation.
+
+
+
+
+
diff --git a/GMLMIP-0.1/clean.sh b/GMLMIP-0.1/clean.sh
new file mode 100755
index 0000000..567d321
--- /dev/null
+++ b/GMLMIP-0.1/clean.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cd ./parser/
+make clean
+cd ..
+
+cd ./formulas/
+make clean
+cd ..
+
+cd ./rules/
+make clean
+cd ..
+
+make clean
diff --git a/GMLMIP-0.1/compile.sh b/GMLMIP-0.1/compile.sh
new file mode 100755
index 0000000..f205a8b
--- /dev/null
+++ b/GMLMIP-0.1/compile.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cd ./parser/
+make all
+cd ..
+
+cd ./formulas/
+make all
+cd ..
+
+cd ./rules/
+make all
+cd ..
+
+make
diff --git a/GMLMIP-0.1/formulas/GML_formula.cpp b/GMLMIP-0.1/formulas/GML_formula.cpp
new file mode 100644
index 0000000..1fc45b4
--- /dev/null
+++ b/GMLMIP-0.1/formulas/GML_formula.cpp
@@ -0,0 +1,80 @@
+#include "GML_formula.h"
+
+bdd GML_Formula::modal(bdd *b, int n, int m){
+ return modal_var(b, n);
+}
+
+void GML_Formula::load_linear_program(glp_prob* problem, Premise<int>& prem){
+ int n = prem.get_n();
+ int m = prem.get_m();
+ int no_of_valuations = prem.get_total_valuations();
+
+ //glp_set_obj_dir(sc, GLP_MIN);
+ glp_add_rows(problem, no_of_valuations+1);
+ glp_add_cols(problem, n+m);
+
+ for(int i = 1; i < no_of_valuations+1; i++)
+ glp_set_row_bnds(problem, i, GLP_UP, 0.0, 0.0); // <= 0
+
+ // Set row bounds for side condition
+ glp_set_row_bnds(problem, no_of_valuations+1, GLP_LO, 1.0, 0.0); // >= 1
+
+ for(int i=1; i < (n+m+1); i++){
+ glp_set_col_kind(problem, i, GLP_IV); //integer variables
+ glp_set_col_bnds(problem, i, GLP_LO, 0, 0); // r_i, s_i >= 0
+ }
+
+ // Arrays for inputting into glpk
+ const int size = (no_of_valuations+1)*(n+m);
+ double ar[size+1];
+ int ia[size+1];
+ int ja[size+1];
+
+ // Recall GLKP takes arrays with 1 - size not 0 - size-1.
+ for(int i=0; i < size; i++){
+ ia[i+1] = (i / (n+m)) + 1;
+ ja[i+1] = (i % (n+m)) + 1;
+ }
+
+ int counter=1;
+
+ // Load all valuations
+ for(int i=0; i < no_of_valuations; i++){
+ int temp = i;
+ for(int j=0; j < n; j++){
+ ar[counter] = temp & 1;
+ temp >>= 1;
+ counter++;
+ }
+ for(int j=0; j < m; j++){
+ ar[counter] = -(temp & 1);
+ temp >>= 1;
+ counter++;
+ }
+ }
+
+ // Load side condition at the bottom
+ for(int i=0; i < n; i++){
+ ar[counter]= prem.get_a_i(i)+1;
+ counter++;
+ }
+
+ for(int j=0; j < m; j++){
+ ar[counter]= -(prem.get_b_i(j));
+ counter++;
+ }
+
+ /*
+ for(int i=1; i < size+1; i++)
+ cout << ia[i] << " ";
+ cout << endl;
+ for(int i=1; i < size+1; i++)
+ cout << ja[i] << " ";
+ cout << endl << endl;
+ for(int i=1; i < size+1; i++)
+ cout << ar[i] << " ";
+ cout << endl;
+ */
+
+ glp_load_matrix(problem, size, ia, ja, ar);
+}
diff --git a/GMLMIP-0.1/formulas/GML_formula.h b/GMLMIP-0.1/formulas/GML_formula.h
new file mode 100644
index 0000000..a24a13b
--- /dev/null
+++ b/GMLMIP-0.1/formulas/GML_formula.h
@@ -0,0 +1,14 @@
+#ifndef GML_FORMULA_HH
+#define GML_FORMULA_HH
+
+#include "formula.h"
+
+class GML_Formula : public Formula<int> {
+ private:
+ void load_linear_program(glp_prob* problem, Premise<int>& prem);
+
+ public:
+ bdd modal(bdd *b, int n, int m);
+
+};
+#endif
diff --git a/GMLMIP-0.1/formulas/PML_formula.cpp b/GMLMIP-0.1/formulas/PML_formula.cpp
new file mode 100644
index 0000000..c4c04ab
--- /dev/null
+++ b/GMLMIP-0.1/formulas/PML_formula.cpp
@@ -0,0 +1,102 @@
+#include "PML_formula.h"
+
+bdd PML_Formula::modal(bdd *b, int n, int m){
+ if(n > m){
+ cout << "error: " << n << "/" << m << " is not in [0,1]" << endl;
+ exit(1);
+ }
+ Rational r(n,m);
+ return modal_var(b, r);
+}
+
+
+void PML_Formula::load_linear_program(glp_prob* problem, Premise<Rational>& prem) {
+ int n = prem.get_n();
+ int m = prem.get_m();
+ int no_of_valuations = prem.get_total_valuations();
+
+ // Additional 2 for side condition and requirements that at least one r_i,s_j is non zero
+ glp_add_rows(problem, no_of_valuations+2);
+
+ // Additional column for k
+ glp_add_cols(problem, n+m+1);
+
+ for(int i = 1; i < no_of_valuations+1; i++)
+ glp_set_row_bnds(problem, i, GLP_UP, 0.0, 0.0); // <= 0
+
+ // Set row bounds for side condition - recall we have -k in the extra column.
+ if(m==0)
+ glp_set_row_bnds(problem, no_of_valuations+1, GLP_LO, 1.0, 0.0); // >= 1
+ else
+ glp_set_row_bnds(problem, no_of_valuations+1, GLP_LO, 0.0, 0.0); // >= 0
+
+ // Set row bounds for additional constraint
+ glp_set_row_bnds(problem, no_of_valuations+2, GLP_LO, 1.0, 0.0); // >= 1
+
+ // Set variable bounds
+ for(int i=1; i < (n+m+1); i++){
+ glp_set_col_kind(problem, i, GLP_IV); //integer variables
+ glp_set_col_bnds(problem, i, GLP_LO, 0, 0); // r_i, s_i >= 0
+ }
+
+ // K is positive integer
+ glp_set_col_kind(problem, n+m+1, GLP_IV); //integer k
+ glp_set_col_bnds(problem, n+m+1, GLP_LO, 1.0, 0.0); // k >= 1
+
+
+ // Arrays for inputting into glpk
+ const int size = (no_of_valuations+2)*(n+m+1);
+ double ar[size+1];
+ int ia[size+1];
+ int ja[size+1];
+
+ // Recall GLKP takes arrays with 1 - size not 0 - size-1.
+ for(int i=0; i < size; i++){
+ ia[i+1] = (i / (n+m+1)) + 1;
+ ja[i+1] = (i % (n+m+1)) + 1;
+ }
+
+ int counter=1;
+
+ // Load all valuations
+ for(int i=0; i < no_of_valuations; i++){
+ int temp = i;
+ for(int j=0; j < n; j++){
+ ar[counter] = temp & 1;
+ temp >>= 1;
+ counter++;
+ }
+ for(int j=0; j < m; j++){
+ ar[counter] = -(temp & 1);
+ temp >>= 1;
+ counter++;
+ }
+ ar[counter] = -1; // - k on each valuation.
+ counter++;
+ }
+
+ // Load side condition
+ for(int i=0; i < n; i++){
+ ar[counter] = prem.get_a_i(i).get();
+ counter++;
+ }
+
+ for(int j=0; j < m; j++){
+ ar[counter]= -(prem.get_b_i(j).get());
+ counter++;
+ }
+ //side condition has coefficent k of -1
+ ar[counter] = -1;
+ counter++;
+
+ //Finally load condition that one must be nonzero.
+ for(int i=0; i < n+m; i++){
+ ar[counter] = 1;
+ counter++;
+ }
+ // k coefficient here is zero
+ ar[counter] = 0;
+
+ glp_load_matrix(problem, size, ia, ja, ar);
+ //glp_write_lp(problem, NULL, "testy.txt");
+}
diff --git a/GMLMIP-0.1/formulas/PML_formula.h b/GMLMIP-0.1/formulas/PML_formula.h
new file mode 100644
index 0000000..8e04b3f
--- /dev/null
+++ b/GMLMIP-0.1/formulas/PML_formula.h
@@ -0,0 +1,14 @@
+#ifndef PML_FORMULA_HH
+#define PML_FORMULA_HH
+
+#include "formula.h"
+
+class PML_Formula : public Formula<Rational> {
+ private:
+ void load_linear_program(glp_prob* problem, Premise<Rational>& prem);
+
+ public:
+ bdd modal(bdd *b, int n, int m);
+
+};
+#endif
diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
new file mode 100644
index 0000000..0a9ef1e
--- /dev/null
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -0,0 +1,284 @@
+#include "formula.h"
+
+template<class ModalValueType>
+Formula<ModalValueType>::Formula(){
+ number_of_variables = 0;
+ variables.set_empty_key(-1); //
+ variables_back.set_empty_key(-1); //
+ data d;
+ modal_variables.set_empty_key(d);
+ modal_variables_back.set_empty_key(-1); //
+ Premise<ModalValueType> p;
+ rule_cache.set_empty_key(p);
+}
+
+template<class ModalValueType>
+bdd Formula<ModalValueType>::variable(int n){
+ if(variables.count(n) == 0){
+ variables[n] = number_of_variables;
+ variables_back[number_of_variables] = n;
+ number_of_variables++;
+ }
+ return bdd_ithvarpp(variables[n]);
+}
+
+template<class ModalValueType>
+bdd Formula<ModalValueType>::modal_var(bdd *b, ModalValueType &n){
+ data d(n, b);
+ if(modal_variables.count(d) == 0){
+ modal_variables[d] = number_of_variables;
+ modal_variables_back[number_of_variables] = d;
+ number_of_variables++;
+ }
+ return bdd_ithvarpp(modal_variables[d]);
+}
+
+
+template<class ModalValueType>
+void Formula<ModalValueType>::print_back_vars(){
+ cout << setw(10) << "BDD number " << setw(10) << "Input Number" << endl;
+ for(int i=0; i < 1000; i++)
+ if(variables_back.count(i) > 0 )
+ cout << setw(10) << i << setw(10) << variables_back[i] << endl;
+ cout << endl;
+}
+
+void sat_handler(char *varset, int size){
+ SatisfyingAssignment s(size, varset);
+ sat_ass_stack.push_back(s);
+}
+
+template<class ModalValueType>
+bool Formula<ModalValueType>::check_satisfiability(bdd b){
+ bool sat = false; // handle the case of no satisfying assignments.
+ //bdd_printdot(b);
+ bdd_allsat(b, sat_handler); // pushes satisfying assignment onto stack
+ vector<SatisfyingAssignment> sat_ass = sat_ass_stack;
+ sat_ass_stack.clear();
+ for(unsigned int i=0; i < sat_ass.size() && !sat; i++){ // we break if proved sat
+ sat = apply_rules(sat_ass[i]);
+ }
+ return sat;
+}
+
+template<class ModalValueType>
+bool Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
+ bool result = true;
+
+ int no_of_positive = 0;
+ int no_of_negative = 0;
+ bdd **underlying_formulae;
+ ModalValueType *positive_modal_indices, *negative_modal_indices;
+
+ // We first find the size of the required arrays.
+ for(int v=0; v < sat.get_size(); v++){
+ if(sat.get_array_i(v)==1 && modal_variables_back.count(v)) // if true and represents a modal formula.
+ no_of_positive++;
+ else if(sat.get_array_i(v)==0 && modal_variables_back.count(v)) // if false and ...
+ no_of_negative++;
+ }
+ // cout << no_of_positive + no_of_negative << endl;
+ if(no_of_positive + no_of_negative > 0){
+
+ // We then initialize our new arrays.
+ underlying_formulae = new bdd* [no_of_positive+no_of_negative];
+
+ positive_modal_indices = new ModalValueType[no_of_positive];
+ negative_modal_indices = new ModalValueType[no_of_negative];
+
+ // We then fill our underlying formulae and modal value arrays.
+ int i=0, j=0;
+ for(int v=0; v < sat.get_size(); v++){
+ if(sat.get_array_i(v)==1 && modal_variables_back.count(v)){
+ underlying_formulae[i] = (modal_variables_back[v]).argument;
+ positive_modal_indices[i] = (modal_variables_back[v]).value;
+ i++;
+ }
+ else if(sat.get_array_i(v)==0 && modal_variables_back.count(v)){ //if false and represents a modal formula.
+ underlying_formulae[no_of_positive+j] = (modal_variables_back[v]).argument;
+ negative_modal_indices[j] = (modal_variables_back[v]).value;
+ j++;
+ }
+ }
+
+ // Construct a GML premise
+ Premise<ModalValueType> premise(no_of_positive, no_of_negative, positive_modal_indices, negative_modal_indices);
+ // Check the rule cache
+ if(rule_cache.count(premise)){ // if in cache
+ SetOfConclusions concs = rule_cache[premise];
+ for(int i = 0; i < concs.number_of_conclusions() && result; i++){
+ bdd b = concs.get_jth_conclusion(underlying_formulae, i);
+ result = check_satisfiability(b);
+ }
+ } else {
+ result = enumerate_rules(premise, underlying_formulae);
+ }
+
+ delete [] underlying_formulae;
+ delete [] positive_modal_indices;
+ delete [] negative_modal_indices;
+ }
+
+ return result;
+}
+
+template<class ModalValueType>
+bool Formula<ModalValueType>::enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae){
+ bool result = true;
+ vector<vector<bool> > valid_nodes;
+ vector<pair<vector<bool>, int> > anti_nodes;
+ vector<vector<bool> > node_queue;
+ int total_valuations = prem.get_total_valuations();
+
+ glp_prob *problem = glp_create_prob();
+
+ // Parameters while solving with glpk
+ glp_iocp* parameters = new glp_iocp;
+ glp_init_iocp(parameters);
+ parameters->presolve = GLP_ON;
+
+ parameters->msg_lev = GLP_MSG_ERR;
+ //parameters->msg_lev = GLP_MSG_ALL;
+
+ load_linear_program(problem, prem);
+
+ vector<bool> zero(total_valuations, false);
+
+ if (run_solver(problem, parameters, false, zero, -1)) {
+ if (run_solver(problem, parameters, true, zero, 0))
+ result = false;
+ else {
+ node_queue.push_back(zero);
+ //int i = 0;
+ while(result && node_queue.size()) {
+ //cout << "outer space: " << i++ << " runs: " << test_counter << " queue: " << node_queue.size() << " sols: " << valid_nodes.size() << " antisols: " << anti_nodes.size() << endl;
+ result = enum_rules_intern(problem, parameters, prem, underlying_formulae, node_queue, valid_nodes, anti_nodes);
+ }
+ if (result && !rule_cache.count(prem)) {
+ rule_cache[prem] = SetOfConclusions(prem.get_n() + prem.get_m(), valid_nodes);
+ }
+ //cout << "runs: " << test_counter << " sols: " << valid_nodes.size() << " antisols: " << anti_nodes.size() << endl;
+ }
+ }
+
+ //Clean-up
+ delete parameters;
+ glp_delete_prob(problem);
+
+ return result;
+}
+
+template<class ModalValueType>
+bool Formula<ModalValueType>::enum_rules_intern(glp_prob* problem, glp_iocp* parameters, Premise<ModalValueType>& prem, bdd** underlying_formulae,
+ vector<vector<bool> >& node_queue, vector<vector<bool> >& valid_nodes, vector<pair<vector<bool>, int> >& anti_nodes){
+ bool result = true;
+ vector<vector<bool> > new_node_queue;
+ int total_valuations = prem.get_total_valuations();
+
+ for (unsigned int k = 0; k < node_queue.size() && result; k++) {
+ vector<bool> current_node = node_queue[k];
+
+ int power = total_valuations-1;
+ while(power >= 0 && !current_node[power])
+ power--;
+ for(int i = power+1; i < total_valuations && result; i++){
+ vector<bool> new_node(current_node);
+ new_node[i] = true;
+
+ // Check node isn't superset of something already valid
+ bool isSubnode = false;
+ for(unsigned int i1=0; i1 < valid_nodes.size() && !isSubnode; i1++){
+ bool isSub = true;
+ for(int j1=0; j1 < total_valuations; j1++){
+ if (valid_nodes[i1][j1] && !new_node[j1]) {
+ isSub = false;
+ break;
+ }
+ }
+ if (isSub) isSubnode = true;
+ }
+ // Check node isn't superset of something of an anti-solution
+ for(unsigned int i1=0; i1 < anti_nodes.size() && !isSubnode; i1++){
+ bool isSub = true;
+ int idx = anti_nodes[i1].second;
+ vector<bool> antinode = anti_nodes[i1].first;
+ for(int j1=0; j1 < total_valuations; j1++){
+ if ((j1 <= idx && antinode[j1] != new_node[j1]) || (j1 > idx && antinode[j1] && !new_node[j1])) {
+ isSub = false;
+ break;
+ }
+ }
+ if (isSub) isSubnode = true;
+ }
+
+ if (!isSubnode) {
+ if (run_solver(problem, parameters, false, new_node, i)) {
+ if (run_solver(problem, parameters, true, new_node, 0)) {
+ valid_nodes.push_back(new_node);
+ //cout << "solution found " << valid_nodes.size() << endl;
+ //for (int l = 0; l < total_valuations; l++)
+ // cout << " " << new_node[l] << endl;
+ vector<vector<bool> > singleton;
+ singleton.push_back(new_node);
+ SetOfConclusions temp = SetOfConclusions(prem.get_n() + prem.get_m(), singleton);
+ bdd b = temp.get_jth_conclusion(underlying_formulae, 0);
+ result = check_satisfiability(b);
+ } else {
+ new_node_queue.push_back(new_node);
+ }
+ }
+ else {
+ pair<vector<bool>, int> antipair = pair<vector<bool>, int>(new_node, i);
+ anti_nodes.push_back(antipair);
+ }
+ }
+ }
+ }
+ node_queue = new_node_queue;
+ return result;
+}
+
+template<class ModalValueType>
+bool Formula<ModalValueType>::run_solver(glp_prob *problem, glp_iocp* parameters, bool strict, vector<bool> current_node, int index){
+ test_counter++;
+
+ // Modify glp problem to match node
+ for(unsigned int i = 0; i < current_node.size(); i++){
+ if(current_node[i])
+ glp_set_row_bnds(problem, i+1, GLP_LO, 1.0, 0.0); // > 0
+ //+1 since valuations go zero to 2^(n+m)-1, glpk rows go 1 to 2^(n+m).
+ else if (strict || static_cast<int>(i) <= index)
+ glp_set_row_bnds(problem, i+1, GLP_UP, 0.0, 0.0); // leq 0
+ else
+ glp_set_row_bnds(problem, i+1, GLP_FR, 0.0, 0.0); // don't care
+ }
+
+ if (!strict) {
+ parameters->tm_lim = 1000;
+ } else {
+ parameters->tm_lim = 1000000000;
+ }
+
+ // Solve the LP
+ int result = glp_intopt(problem, parameters);
+
+ if(result == 0 || result == GLP_ENOPFS) { //if no errors from solver or a relaxtion feasibility error
+ if(glp_mip_status(problem)==GLP_OPT || glp_mip_status(problem)==GLP_FEAS){ // if feasible
+ return true;
+ }
+ else {
+ return false;
+ }
+ }
+ else if (!strict && result == GLP_ETMLIM) { // if the solver timed out for non-strict problems
+ //cout << "timeout" << endl;
+ return true;
+ } else { // if error but not a feasibility error
+ cout << "glpk error: " << result << endl;
+ exit(1);
+ }
+}
+
+
+template class Formula<int>;
+template class Formula<Rational>;
diff --git a/GMLMIP-0.1/formulas/formula.h b/GMLMIP-0.1/formulas/formula.h
new file mode 100644
index 0000000..a5931d1
--- /dev/null
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -0,0 +1,159 @@
+#ifndef FORMULA_HH
+#define FORMULA_HH
+
+#include <iostream>
+#include <cstdlib>
+#include <cstring>
+#include <iomanip>
+#include <sstream>
+#include <string>
+#include <time.h>
+
+#include "bdd.h"
+#include "glpk.h"
+
+#include <vector>
+#include <utility>
+
+#include "google/dense_hash_map"
+#include <ext/hash_map>
+/* will become #include <unordered_set> */
+
+#include "rational.h"
+#include "../rules/premise.h"
+#include "../rules/setofconclusions.h"
+#include "../satisfyingstack.h"
+
+using namespace std;
+
+using std::cout;
+using std::endl;
+using std::vector;
+using google::dense_hash_map;
+using __gnu_cxx::hash;
+
+// Formula interface so we can have abstract template class pointers.
+class IFormula {
+ public:
+ virtual bdd variable(int n)=0;
+ virtual void set_bdd(bdd &b)=0;
+ virtual bdd get_bdd()=0;
+ virtual bdd modal(bdd *b, int n, int m)=0;
+ virtual bool satisfiability(int option)=0;
+ virtual void clear_maps()=0;
+};
+
+template<class ModalValueType>
+class Formula : public IFormula{
+ protected:
+ /* REQUIRED DEFINITIONS FOR HASH_MAPS */
+ class data {
+ public:
+ ModalValueType value;
+ bdd* argument;
+ data() : value(-1) {argument = NULL; };
+ data(ModalValueType v, bdd* arg) : value(v){ argument = arg; };
+ ~data(){ if(argument) delete argument; };
+ data& operator=(const data& other){
+ if (this!=&other){
+ if(argument)
+ delete argument;
+ value = other.value;
+ argument = NULL;
+ if(other.argument)
+ argument = new bdd(*(other.argument));
+ }
+ return *this;
+ };
+ data(const data& other){
+ value = other.value;
+ argument = NULL;
+ if(other.argument)
+ argument = new bdd(*(other.argument));
+ };
+ };
+
+ // Required for dense_hash_map - how to compare keys.
+ struct eqkey {
+ bool operator()(const string s1, const string s2) const{
+ return s1 == s2;
+ }
+
+ bool operator()(const int s1, const int s2) const{
+ return (s1 == s2);
+ }
+
+ bool operator()(const data& d1, const data& d2) const{
+ return ((d1.value == d2.value) && ((d1.argument==d2.argument) || (d1.argument && d2.argument && (*(d1.argument) == *(d2.argument)))));
+ }
+ };
+
+ // Number of variables. Set to zero by constructor and
+ // incremented as variables and modal variables are added.
+ // (Used for building the hash_maps).
+ int number_of_variables;
+
+ // Map of parsed variable numbers to BDD package numbers
+ dense_hash_map<int, int, hash<int>, eqkey> variables;
+ // Map of BDD package numbers to input numbers
+ dense_hash_map<int, int, hash<int>, eqkey> variables_back;
+
+ // How to hash data items.
+ struct datahash {
+ hash <const char*> charhash;
+ hash <int> inthash;
+ size_t operator ()(const data& d) const {
+ stringstream ss;
+ string s;
+ ss << d.value << " " << *d.argument << '\0';
+ s = ss.str();
+ char buf[s.size()+1];
+ for(unsigned int i=0; i < s.size(); i++)
+ buf[i] = s[i];
+ buf[s.size()]='\0';
+ return charhash(buf);
+ }
+ };
+
+ dense_hash_map<data, int, datahash, eqkey> modal_variables;
+ dense_hash_map<int, data, hash<int>, eqkey> modal_variables_back;
+
+ dense_hash_map<Premise<ModalValueType>, SetOfConclusions, typename Premise<ModalValueType>::Premise_hash, typename Premise<ModalValueType>::Premise_equal> rule_cache;
+
+ int test_counter;
+
+ bool check_satisfiability(bdd b);
+ bool apply_rules(SatisfyingAssignment& sat);
+ bool enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae);
+ bool enum_rules_intern(glp_prob* problem, glp_iocp* parameters, Premise<ModalValueType>& prem, bdd** underlying_formulae, vector<vector<bool> >& node_queue, vector<vector<bool> >& valid_nodes, vector<pair<vector<bool>, int> >& anti_nodes);
+ bool run_solver(glp_prob *problem, glp_iocp* parameters, bool strict, vector<bool> current_node, int index);
+
+ virtual void load_linear_program(glp_prob* problem, Premise<ModalValueType>& prem)=0;
+
+ public:
+ Formula();
+ // The parsed formula
+ bdd bdd_rep;
+
+ // Used by the driver to set bdd_rep
+ void set_bdd(bdd &b){ bdd_rep=b; };
+ bdd get_bdd(){ return bdd_rep;};
+
+ // Called by parser to construct variable or modal variable.
+ // Also constructs appropriate data structures.
+ bdd variable(int n);
+ bdd modal_var(bdd *b, ModalValueType &n);
+
+ void print_back_vars();
+ //virtual void print_back_modal()=0;
+
+ bool satisfiability(int option){ return check_satisfiability(bdd_rep); };
+
+ void clear_maps(){
+ variables.clear();
+ variables_back.clear();
+ modal_variables.clear();
+ modal_variables_back.clear();
+ rule_cache.clear(); };
+};
+#endif
diff --git a/GMLMIP-0.1/formulas/makefile b/GMLMIP-0.1/formulas/makefile
new file mode 100644
index 0000000..59be103
--- /dev/null
+++ b/GMLMIP-0.1/formulas/makefile
@@ -0,0 +1,22 @@
+GCC = g++
+GCCFLAGS = -Wall -Wno-deprecated
+
+all: formula.o PML_formula.o GML_formula.o rational.o satisfyingassignment.o
+
+satisfyingassignment.o: satisfyingassignment.h satisfyingassignment.cpp
+ $(GCC) $(GCCFLAGS) -c satisfyingassignment.cpp
+
+formula.o: formula.h formula.cpp
+ $(GCC) $(GCCFLAGS) -c formula.cpp
+
+PML_formula.o: formula.h rational.h PML_formula.cpp PML_formula.h ../rules/PML_premise.h ../rules/setofconclusions.h
+ $(GCC) $(GCCFLAGS) -c PML_formula.cpp
+
+GML_formula.o: formula.h GML_formula.cpp GML_formula.h ../rules/GML_premise.h ../rules/setofconclusions.h
+ $(GCC) $(GCCFLAGS) -c GML_formula.cpp
+
+rational.o: rational.h rational.cpp
+ $(GCC) $(GCCFLAGS) -c rational.cpp
+
+clean:
+ rm -rf *~ *.o test
diff --git a/GMLMIP-0.1/formulas/rational.cpp b/GMLMIP-0.1/formulas/rational.cpp
new file mode 100644
index 0000000..a0b5a10
--- /dev/null
+++ b/GMLMIP-0.1/formulas/rational.cpp
@@ -0,0 +1,29 @@
+#include "rational.h"
+
+Rational::Rational(int i){
+ if(i==-1){ //For empty key in hash maps
+ top = 0;
+ bottom = 0;
+ }
+ else{
+ top = i;
+ bottom = 1;
+ }
+}
+
+double Rational::get(){
+ return (static_cast<double>(top)/bottom);
+}
+
+ostream& operator<<(ostream &o, const Rational &r){
+ o << r.top << "/" << r.bottom;
+ return o;
+}
+
+bool operator==(const Rational &r1, const Rational &r2){
+ return((r1.top*r2.bottom) == (r2.top*r1.bottom));
+}
+
+bool operator!=(const Rational &r1, const Rational &r2){
+ return !(r1==r2);
+}
diff --git a/GMLMIP-0.1/formulas/rational.h b/GMLMIP-0.1/formulas/rational.h
new file mode 100644
index 0000000..2e41dd4
--- /dev/null
+++ b/GMLMIP-0.1/formulas/rational.h
@@ -0,0 +1,26 @@
+#ifndef RATIONAL_H
+#define RATIONAL_H
+
+#include <iostream>
+
+using namespace std;
+
+class Rational {
+ private:
+ int top;
+ int bottom;
+ public:
+ Rational(){ top=0; bottom=0; };
+ Rational(int i);
+ Rational(int t, int b){top=t; bottom=b;};
+ int get_top(){ return top;};
+ int get_bot(){ return bottom;};
+ double get();
+
+ friend ostream& operator<<(ostream &o, const Rational &r);
+ friend bool operator==(const Rational &r1, const Rational &r2);
+ friend bool operator!=(const Rational &r1, const Rational &r2);
+};
+
+#endif
+
diff --git a/GMLMIP-0.1/formulas/satisfyingassignment.cpp b/GMLMIP-0.1/formulas/satisfyingassignment.cpp
new file mode 100644
index 0000000..3f9b1b0
--- /dev/null
+++ b/GMLMIP-0.1/formulas/satisfyingassignment.cpp
@@ -0,0 +1,64 @@
+#include "satisfyingassignment.h"
+
+SatisfyingAssignment::SatisfyingAssignment(int _size, char* _array){
+ size = _size;
+
+ if(size)
+ array = new char [size];
+ else
+ array = NULL;
+
+ for(int i=0; i < size; i++)
+ array[i]=_array[i];
+}
+
+SatisfyingAssignment::SatisfyingAssignment(const SatisfyingAssignment& a){
+ size = a.size;
+
+ if(size)
+ array = new char [size];
+ else
+ array = NULL;
+
+ for(int i=0; i < size; i++)
+ array[i]=a.array[i];
+}
+
+SatisfyingAssignment& SatisfyingAssignment::operator=(const SatisfyingAssignment& a){
+ if(this != &a){
+ if(array)
+ delete [] array;
+ size = a.size;
+
+ if(size)
+ array = new char [size];
+ else
+ array = NULL;
+
+ for(int i=0; i < size; i++)
+ array[i]=a.array[i];
+ }
+ return *this;
+}
+
+
+SatisfyingAssignment::~SatisfyingAssignment(){
+ if(array)
+ delete [] array;
+}
+
+char SatisfyingAssignment::get_array_i(int i){
+ if(array)
+ return array[i];
+ return '\0';
+}
+
+bool SatisfyingAssignment::operator==(const SatisfyingAssignment& other) const{
+ if(size == other.size){
+ for(int i = 0; i < size; i++)
+ if(array[i]!=other.array[i])
+ return false;
+ return true;
+ }
+ return false;
+ }
diff --git a/GMLMIP-0.1/formulas/satisfyingassignment.h b/GMLMIP-0.1/formulas/satisfyingassignment.h
new file mode 100644
index 0000000..7ad5565
--- /dev/null
+++ b/GMLMIP-0.1/formulas/satisfyingassignment.h
@@ -0,0 +1,26 @@
+#ifndef SATISFYINGASSIGNMENT_H
+#define SATISFYINGASSIGNMENT_H
+
+#include <iostream>
+
+using namespace std;
+
+class SatisfyingAssignment {
+ private:
+ int size;
+ char* array;
+ public:
+ SatisfyingAssignment(){ size = 0; array = NULL; };
+ SatisfyingAssignment(int _size, char* _array);
+ SatisfyingAssignment(const SatisfyingAssignment& a);
+ SatisfyingAssignment& operator=(const SatisfyingAssignment& a);
+ ~SatisfyingAssignment();
+
+ bool operator==(const SatisfyingAssignment& other) const;
+
+
+ int get_size(){ return size;};
+ char get_array_i(int i);
+};
+
+#endif
diff --git a/GMLMIP-0.1/input b/GMLMIP-0.1/input
new file mode 100644
index 0000000..66bbf4f
--- /dev/null
+++ b/GMLMIP-0.1/input
@@ -0,0 +1,2 @@
+Logic:GML
+<3>p0 & <3>~p0 & ~<5>true
diff --git a/GMLMIP-0.1/main.cpp b/GMLMIP-0.1/main.cpp
new file mode 100644
index 0000000..1e88620
--- /dev/null
+++ b/GMLMIP-0.1/main.cpp
@@ -0,0 +1,70 @@
+#include <iostream>
+#include <vector>
+#include <time.h>
+
+#include "./parser/mlf-driver.h"
+#include "./formulas/formula.h"
+#include "./formulas/satisfyingassignment.h"
+#include "satisfyingstack.h"
+
+#include "bdd.h"
+
+using namespace std;
+
+vector<SatisfyingAssignment> sat_ass_stack;
+
+/* Error handler for running out of BDD nodes */
+void error_handler(int errorcode){
+ if(errorcode==BDD_VAR)
+ bdd_extvarnum(1000);
+ else
+ cout << "BDD package error number " << errorcode << endl;
+}
+
+void parse(IFormula* &formula, int argc, char *argv[], int& verbose);
+
+int main (int argc, char *argv[]){
+ clock_t total_time = clock();
+ IFormula* f = NULL;
+ int verbose = 0;
+ //initalize buddy
+ bdd_init(100000, 10000);
+ bdd_setvarnum(100); // Minimum is two.
+ bdd_error_hook(error_handler);
+ parse(f, argc, argv, verbose);
+ if(f){
+ // bdd_varblockall();
+ // bdd_reorder(BDD_REORDER_WIN3ITE);
+ // bdd_printdot((driver.formula)->bdd_rep);
+ //bdd_printset(f->get_bdd());
+ //cout << endl;
+ //(driver.formula)->print_back_vars();
+ if(f->satisfiability(verbose))
+ cout << "Satisfiable" << endl;
+ else
+ cout << "Unsatisfiable" << endl;
+ f->clear_maps();
+ delete f;
+ }
+ bdd_done();
+ total_time = clock() - total_time;
+ cout << "Total Time: " << static_cast<float>(total_time) / CLOCKS_PER_SEC << endl;
+ return 0;
+}
+
+void parse(IFormula* &formula, int argc, char *argv[], int& option){
+ mlf_driver driver;
+ for (++argv; argv[0]; ++argv)
+ if (*argv == std::string ("-p"))
+ driver.trace_parsing = true;
+ else if (*argv == std::string ("-v"))
+ option = 1;
+ else if (*argv == std::string ("-t"))
+ option = 2;
+ else if (*argv == std::string ("-s"))
+ driver.trace_scanning = true;
+ else if (!driver.parse (*argv))
+ driver.extract_formula(formula);
+}
+
+
diff --git a/GMLMIP-0.1/makefile b/GMLMIP-0.1/makefile
new file mode 100644
index 0000000..9576cd7
--- /dev/null
+++ b/GMLMIP-0.1/makefile
@@ -0,0 +1,15 @@
+GCC = g++
+GCCFLAGS = -Wall -Wno-deprecated
+
+POBJS = ./parser/lex.yy.o ./parser/mlf-parser.tab.o ./parser/mlf-driver.o
+FOBJS = ./formulas/formula.o ./formulas/GML_formula.o ./formulas/PML_formula.o ./formulas/rational.o ./formulas/satisfyingassignment.o
+ROBJS = ./rules/premise.o ./rules/GML_premise.o ./rules/PML_premise.o ./rules/valuation.o ./rules/setofconclusions.o ./rules/sizefunctions.o ./rules/radixtree.o
+
+main: main.o $(POBJS) $(FOBJS) $(ROBJS)
+ $(GCC) $(GCCFLAGS) $(POBJS) $(FOBJS) $(ROBJS) -lbdd -lm -lglpk main.o -o main
+
+main.o: main.cpp ./parser/mlf-driver.h ./formulas/formula.h ./formulas/satisfyingassignment.h
+ $(GCC) $(GCCFLAGS) -c main.cpp
+
+clean:
+ rm -rf *~ *.o main
diff --git a/GMLMIP-0.1/parser/makefile b/GMLMIP-0.1/parser/makefile
new file mode 100644
index 0000000..f39e8ee
--- /dev/null
+++ b/GMLMIP-0.1/parser/makefile
@@ -0,0 +1,34 @@
+BISON = bison
+LEX = flex
+GCC = g++
+
+GCCFLAGS = -Wall -Wno-deprecated
+
+all: parser lex.yy.o mlf-parser.tab.o mlf-driver.o
+
+lex.yy.o: lex.yy.h lex.yy.c
+ $(GCC) $(GCCFLAGS) -c lex.yy.c
+
+mlf-parser.tab.o: mlf-parser.tab.h mlf-parser.tab.cc ../formulas/GML_formula.h ../formulas/PML_formula.h
+ $(GCC) $(GCCFLAGS) -c mlf-parser.tab.cc
+
+mlf-driver.o: mlf-driver.h mlf-driver.cpp mlf-parser.tab.h lex.yy.h ../formulas/formula.h
+ $(GCC) $(GCCFLAGS) -c mlf-driver.cpp
+
+mlf-parser.tab.h: mlf-parser.yy
+ $(BISON) --defines=mlf-parser.tab.h mlf-parser.yy
+
+lex.yy.h: mlf-scanner.ll
+ $(LEX) --header-file=lex.yy.h mlf-scanner.ll
+
+parser: mlf-parser.tab.h lex.yy.h ../formulas/formula.h
+
+
+test: parser lex.yy.o mlf-parser.tab.o mlf-driver.o test.o
+ $(GCC) $(GCCFLAGS) test.o lex.yy.o mlf-parser.tab.o mlf-driver.o -o test
+
+test.o: test.cpp mlf-driver.h
+ $(GCC) $(GCCFLAGS) -c test.cpp
+
+clean:
+ rm -rf *~ *.o location.hh stack.hh mlf-parser.tab.h mlf-parser.tab.cc position.hh lex.yy.c lex.yy.h test
diff --git a/GMLMIP-0.1/parser/mlf-driver.cpp b/GMLMIP-0.1/parser/mlf-driver.cpp
new file mode 100644
index 0000000..09279c6
--- /dev/null
+++ b/GMLMIP-0.1/parser/mlf-driver.cpp
@@ -0,0 +1,60 @@
+#include "mlf-driver.h"
+#include "mlf-parser.tab.h"
+
+mlf_driver::mlf_driver() : trace_scanning (false), trace_parsing (false){
+ formula = NULL;
+}
+
+int mlf_driver::parse (const std::string &f){
+ file = f;
+ scan_begin ();
+ yy::mlf_parser parser (*this);
+ parser.set_debug_level (trace_parsing);
+ int res = parser.parse ();
+ scan_end ();
+ return res;
+}
+
+void mlf_driver::error (const yy::location& l, const std::string& m){
+ std::cerr << l << ": " << m << std::endl;
+}
+
+void mlf_driver::error (const std::string& m){
+ std::cerr << m << std::endl;
+}
+
+bdd mlf_driver::variable(int n){
+ if(!formula){
+ cout << "driver.formula was null!" << endl;
+ exit(1);
+ }
+ return formula->variable(n);
+}
+
+bdd mlf_driver::modal(bdd *b, int n, int m){
+ if(!formula){
+ cout << "driver.formula was null!" << endl;
+ exit(1);
+ }
+ return formula->modal(b, n, m);
+}
+
+
+void mlf_driver::set_formula_bdd(bdd b){
+ if(!formula){
+ cout << "driver.formula was null!" << endl;
+ exit(1);
+ }
+ formula->set_bdd(b);
+}
+
+void mlf_driver::extract_formula(IFormula* &ptr){
+ ptr = formula;
+ formula = NULL;
+}
+
+mlf_driver::~mlf_driver(){
+ if(formula!=NULL)
+ delete formula;
+}
+
diff --git a/GMLMIP-0.1/parser/mlf-driver.h b/GMLMIP-0.1/parser/mlf-driver.h
new file mode 100644
index 0000000..2c6666c
--- /dev/null
+++ b/GMLMIP-0.1/parser/mlf-driver.h
@@ -0,0 +1,62 @@
+#ifndef MLF_DRIVER_HH
+#define MLF_DRIVER_HH
+#include <string>
+#include "mlf-parser.tab.h"
+#include "lex.yy.h"
+#include "../formulas/formula.h"
+
+using namespace std;
+
+
+//Tell Flex the lexer's prototype:
+# define YY_DECL \
+ yy::mlf_parser::token_type \
+yylex (yy::mlf_parser::semantic_type* yylval, \
+ yy::mlf_parser::location_type* yylloc, \
+ mlf_driver& driver)
+// ... and declare it for the parser's sake.
+YY_DECL;
+
+
+class mlf_driver{
+ public:
+ mlf_driver();
+ ~mlf_driver();
+
+ // The parsed formula object will be construced here
+ IFormula* formula;
+
+ private:
+ char logic;
+
+ public:
+ char get_logic(){ return logic; };
+
+ void set_formula_bdd(bdd b);
+ void set_formula_gml(){ logic='g'; formula = new GML_Formula; };
+ void set_formula_pml(){ logic='p'; formula = new PML_Formula; };
+
+ /* Calls formula->variable and formula->modal respectively
+ requires ints to be pre-loaded into upper and lower. In the
+ case of only one integer being required we load it into n.*/
+ bdd variable(int n);
+ bdd modal(bdd *b, int n, int m);
+
+ // Extract the formula object
+ void extract_formula(IFormula* &ptr);
+
+ // Handling the scanner.
+ void scan_begin ();
+ void scan_end ();
+ bool trace_scanning;
+
+ // Run the parser. Return 0 on success.
+ int parse (const std::string& f);
+ std::string file;
+ bool trace_parsing;
+
+ // Error handling.
+ void error (const yy::location& l, const std::string& m);
+ void error (const std::string& m);
+};
+#endif
diff --git a/GMLMIP-0.1/parser/mlf-parser.yy b/GMLMIP-0.1/parser/mlf-parser.yy
new file mode 100644
index 0000000..8a2b9e0
--- /dev/null
+++ b/GMLMIP-0.1/parser/mlf-parser.yy
@@ -0,0 +1,111 @@
+%skeleton "lalr1.cc"
+%require "2.4"
+%defines
+%define parser_class_name "mlf_parser"
+
+%code requires {
+ #include <string>
+ #include "bdd.h"
+ #include "../formulas/GML_formula.h"
+ #include "../formulas/PML_formula.h"
+ #include "../formulas/rational.h"
+
+ using namespace std;
+
+ class mlf_driver;
+ #define YYSTYPE ParserType
+
+ struct ParserType
+{
+ int number;
+ struct fraction {
+ int numerator;
+ int denominator;
+ } fraction;
+ bdd binarydd;
+};
+}
+
+
+
+// Parsing context
+%parse-param { mlf_driver& driver}
+%lex-param { mlf_driver& driver}
+
+%locations
+%initial-action {
+ // Initialize the initial location.
+ @$.begin.filename = @$.end.filename = &driver.file;
+};
+
+%debug
+%error-verbose
+
+%code {
+ #include "mlf-driver.h"
+}
+
+/* operators and precendences */
+ %nonassoc IFF
+ %right IMP
+ %left OR
+ %left AND
+ %nonassoc <number> GMDIA GMBOX
+ %nonassoc <fraction> PMDIA PMBOX
+ %nonassoc <binarydd> PVAR
+ %nonassoc NOT TRUE FALSE
+
+ /* auxiliary */
+ %token END 0 "end of file"
+ %token LPAREN
+ %token RPAREN
+
+ %token GML
+ %token PML
+ //%token PMLI
+
+ // %printer { debug_stream () << $$; } "identifier"
+ %destructor { delete &$$; } "identifier"
+
+ %type <binarydd> formula
+
+%%
+input:
+ spec
+ formula {driver.set_formula_bdd($2); }
+ ;
+
+spec:
+ GML {driver.set_formula_gml();}
+ | PML {driver.set_formula_pml();}
+ //| PMLI {}
+ ;
+
+formula:
+ formula IFF formula { $$ = bdd_biimp($1,$3); }
+ | formula IMP formula { $$ = bdd_imp($1,$3); }
+ | formula OR formula { $$ = bdd_or($1,$3); }
+ | formula AND formula { $$ = bdd_and($1,$3); }
+
+ | GMDIA formula { bdd* b = new bdd($2); $$ = driver.modal(b, $1, 0); }
+ | GMBOX formula { bdd* b = new bdd(bdd_not($2)); $$ = bdd_not(driver.modal(b, $1, 0)); } // box is not-dia-not
+
+ | PMDIA formula { bdd* b = new bdd($2); $$ = driver.modal(b, $1.numerator, $1.denominator); }
+ | PMBOX formula { bdd* b = new bdd(bdd_not($2)); $$ = bdd_not(driver.modal(b, $1.numerator, $1.denominator)); }
+
+ | NOT formula { $$ = bdd_not($2); }
+ | PVAR { $$ = $$; }
+ | TRUE { $$ = bdd_true(); }
+ | FALSE { $$ = bdd_false(); }
+ | LPAREN formula RPAREN { $$ = $2; }
+ ;
+%%
+
+
+void yy::mlf_parser::error (const yy::mlf_parser::location_type& l, const std::string& m){
+ driver.error (l, m);
+}
+
+
+
+
diff --git a/GMLMIP-0.1/parser/mlf-scanner.ll b/GMLMIP-0.1/parser/mlf-scanner.ll
new file mode 100644
index 0000000..acdf0ad
--- /dev/null
+++ b/GMLMIP-0.1/parser/mlf-scanner.ll
@@ -0,0 +1,124 @@
+%{
+# include <cstdlib>
+# include <errno.h>
+# include <limits.h>
+# include <string>
+# include "mlf-driver.h"
+# include "mlf-parser.tab.h"
+
+/* Added since it fixes compile errors */
+#define YY_NEW_FILE yyrestart(yyin )
+
+#define YY_DO_BEFORE_ACTION \
+ (yytext_ptr) = yy_bp; \
+/* %% [2.0] code to fiddle yytext and yyleng for yymore() goes here \ */\
+ yyleng = (size_t) (yy_cp - yy_bp); \
+ (yy_hold_char) = *yy_cp; \
+ *yy_cp = '\0'; \
+/* %% [3.0] code to copy yytext_ptr to yytext[] goes here, if %array \ */\
+ (yy_c_buf_p) = yy_cp;
+/* ----------------------- */
+
+/* Work around an incompatibility in flex (at least versions
+ 2.5.31 through 2.5.33): it generates code that does
+ not conform to C89. See Debian bug 333231
+ <http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=333231>. */
+# undef yywrap
+# define yywrap() 1
+
+/* By default yylex returns int, we use token_type.
+ Unfortunately yyterminate by default returns 0, which is
+ not of token_type. */
+#define yyterminate() return token::END
+%}
+
+%option noyywrap nounput batch debug
+
+
+
+%{
+# define YY_USER_ACTION yylloc->columns (yyleng);
+%}
+
+%{
+ typedef yy::mlf_parser::token token;
+%}
+
+
+%%
+[ \t\n]+ /*eat white space*/
+"Logic:GML" { return token::GML; }
+"Logic:PML" { return token::PML; }
+"Logic: GML" { return token::GML; }
+"Logic: PML" { return token::PML; }
+"&" { return token::AND; }
+"->" { return token::IMP; }
+"<->" { return token::IFF; }
+"<"[0-9]+">" { if(driver.get_logic()!='g')
+ driver.error(*yylloc, "Invalid operator type for specified logic!");
+ else {
+ yylval->number = atoi(yytext + 1);
+ return token::GMDIA;
+ }
+ }
+"["[0-9]+"]" { if(driver.get_logic()!='g')
+ driver.error(*yylloc, "Invalid operator type for specified logic!");
+ else {
+ yylval->number = atoi(yytext + 1);
+ return token::GMBOX;
+ }
+ }
+"<"[0-9]+"/"[0-9]+">" { if(driver.get_logic()!='p')
+ driver.error(*yylloc, "Invalid operator type for specified logic!");
+ else {
+ (yylval->fraction).numerator = atoi(yytext + 1);
+ /*TODO: find more elegant way to perform this - skipping through until "/" */
+ int a = 1;
+ int b = atoi(yytext + 1);
+ while(b > 0){
+ b = b/10;
+ a++;
+ }
+ (yylval->fraction).denominator = atoi(yytext + a + 1);
+ return token::PMDIA;
+ }
+ }
+"["[0-9]+"/"[0-9]+"]" { if(driver.get_logic()!='p')
+ driver.error(*yylloc, "Invalid operator type for specified logic!");
+ else {
+ (yylval->fraction).numerator = atoi(yytext + 1);
+ int a = 1;
+ int b = atoi(yytext + 1);
+ while(b > 0){
+ b = b/10;
+ a++;
+ }
+ (yylval->fraction).denominator = atoi(yytext + a + 1);
+ return token::PMBOX;
+ }
+ }
+"v" { return token::OR; }
+"~" { return token::NOT; }
+p[0-9]+ { yylval->binarydd = driver.variable(atoi(yytext + 1)); return token::PVAR; }
+"(" { return token::LPAREN; }
+")" { return token::RPAREN; }
+"true" { return token::TRUE; }
+"false" { return token::FALSE; }
+. driver.error (*yylloc, "invalid character!");
+%%
+
+void mlf_driver::scan_begin (){
+ yy_flex_debug = trace_scanning;
+ if (file == "-")
+ yyin = stdin;
+ else if (!(yyin = fopen (file.c_str (), "r")))
+ {
+ error (std::string ("cannot open ") + file);
+ exit (1);
+ }
+}
+
+void mlf_driver::scan_end (){
+ fclose (yyin);
+}
+
diff --git a/GMLMIP-0.1/parser/test.cpp b/GMLMIP-0.1/parser/test.cpp
new file mode 100644
index 0000000..8679303
--- /dev/null
+++ b/GMLMIP-0.1/parser/test.cpp
@@ -0,0 +1,16 @@
+#include <iostream>
+#include "mlf-driver.h"
+
+int main (int argc, char *argv[]){
+ mlf_driver driver;
+ for (++argv; argv[0]; ++argv)
+ if (*argv == std::string ("-p"))
+ driver.trace_parsing = true;
+ else if (*argv == std::string ("-s"))
+ driver.trace_scanning = true;
+ else if (!driver.parse (*argv)){
+ std::cout << driver.result << std::endl;
+ std::cout << (driver.formula)->logic << std::endl;
+ }
+ return 0;
+}
diff --git a/GMLMIP-0.1/rand.pl b/GMLMIP-0.1/rand.pl
new file mode 100644
index 0000000..7c54e91
--- /dev/null
+++ b/GMLMIP-0.1/rand.pl
@@ -0,0 +1,98 @@
+#!/usr/bin/perl
+use Switch;
+
+$size = 25;
+$prefix = "test";
+$num_formulas = 1000;
+$num_propvars = 5;
+$max_index = 100;
+
+for ($i = 0; $i < $num_formulas; $i++) {
+ $factfilename = "size" . $size . $prefix . $i . ".fact";
+ $willfilename = "size" . $size . $prefix . $i . ".will";
+ open FACT, ">", $factfilename;
+ # satisfy fact syntax
+ print FACT "(equal_c SAT ";
+ open WILL, ">", $willfilename;
+ # satisfy will syntax
+ print WILL "Logic: GML\n";
+ random_formula($size);
+ print FACT ")\n";
+ close FACT;
+ close WILL;
+}
+
+sub random_formula {
+ local ($size) = $_[0];
+
+ # terminate on size 1 and return prop variable
+ if ($size == 1) {
+ $num = int(rand($num_propvars));
+ print FACT "p" . $num . " ";
+ print WILL "p" . $num . " ";;
+ }
+ if ($size == 2) {
+ # guess unary connective
+ $conn = int(rand(2));
+ switch ($conn) {
+ case 0 {
+ print WILL "(~";
+ print FACT "(not ";
+ random_formula(1);
+ print WILL ")";
+ print FACT ")";
+ }
+ case 1 {
+ $n = int(rand($max_index));
+ print WILL "(<" . $n . ">";
+ print FACT "(min " . ($n+1) . " r ";
+ random_formula(1);
+ print WILL ")";
+ print FACT ")";
+ }
+ }
+ }
+ if ($size > 2) {
+ # guess a connective
+ $conn = int(rand(4));
+ switch ($conn) {
+ case 0 {
+ $split = 1 + int(rand($size - 2));
+ print WILL "(";
+ print FACT "(and ";
+ random_formula($split);
+ print WILL " & ";
+ random_formula ($size - $split - 1);
+ print WILL ")";
+ print FACT ")";
+ }
+ case 1 {
+ $split = 1 + int(rand($size - 2));
+ print WILL "(";
+ print FACT "(or ";
+ random_formula($split);
+ print WILL " v ";
+ random_formula ($size - $split - 1);
+ print WILL ")";
+ print FACT ")";
+ }
+ case 2 {
+ print WILL "(~";
+ print FACT "(not ";
+ random_formula ($size -1);
+ print WILL ")";
+ print FACT ")";
+ }
+ case 3 {
+ $n = int(rand($max_index));
+ print WILL "(<" . $n . ">";
+ print FACT "(min " . ($n+1) . " r ";
+ random_formula($size-1);
+ print WILL ")";
+ print FACT ")";
+ }
+ }
+ }
+}
+
+
diff --git a/GMLMIP-0.1/rules/GML_premise.cpp b/GMLMIP-0.1/rules/GML_premise.cpp
new file mode 100644
index 0000000..3c24658
--- /dev/null
+++ b/GMLMIP-0.1/rules/GML_premise.cpp
@@ -0,0 +1,251 @@
+#include "GML_premise.h"
+
+GML_Premise::GML_Premise() : Premise<int>(){
+}
+
+GML_Premise::GML_Premise(int _n, int _m, int* _a, int *_b) : Premise<int>(_n,_m,_a,_b){
+//test_counter = 0;
+}
+
+
+/* Deprecated Functions which searched for solutions to the side condition first.
+vector<Conclusion> GML_Premise::construct_conclusions(){
+ double limit = bound();
+ vector<Conclusion> set;
+ glp_prob *side_condition = glp_create_prob();
+
+ // Parameters while solving with glpk
+ glp_iocp* parameters = new glp_iocp;
+ glp_init_iocp(parameters);
+ parameters->presolve = GLP_ON;
+ parameters->msg_lev = GLP_MSG_ERR;
+
+ // Load numbers into LP
+ load_side_condition(side_condition, limit);
+
+ // output for testing.
+ //glp_write_lp(side_condition, NULL, "output.txt");
+
+ // Solve depth first
+ solve_side_condition(side_condition, parameters, 0, 0, 0, limit, set);
+
+ //Clean-up
+ delete parameters;
+ glp_delete_prob(side_condition);
+
+ return set;
+}
+
+void GML_Premise::load_side_condition(glp_prob* sc, double limit){
+ glp_set_obj_dir(sc, GLP_MIN);
+ glp_add_rows(sc, 1);
+ glp_set_row_bnds(sc, 1, GLP_LO, 1.0, 0.0);
+
+ glp_add_cols(sc, n+m);
+
+ for(int i=1; i < (n+m+1); i++){
+ glp_set_col_kind(sc, i, GLP_IV); //integer variables
+ glp_set_col_bnds(sc, i, GLP_DB, 0, limit);
+ }
+
+ // Arrays for inputting into glpk
+ double ar[n+m+1];
+ int ia[n+m+1];
+ int ja[n+m+1];
+
+ for(int i=1; i < n+m+1; i++){
+ ia[i]=1;
+ ja[i]=i;
+ }
+
+ int counter=1;
+ for(int i=0; i < n; i++){
+ ar[counter]= a[i]+1;
+ counter++;
+ }
+
+ for(int j=0; j < m; j++){
+ ar[counter]=(-b[j]);
+ counter++;
+ }
+
+ // Set objective function
+ for(int i=1; i < n+m+1; i++)
+ glp_set_obj_coef(sc, i, ar[i]);
+
+ glp_load_matrix(sc, n+m, ia, ja, ar);
+}
+
+void GML_Premise::solve_side_condition(glp_prob* sc, glp_iocp* parameters, int r_or_s, int index, int new_bound, double limit, vector<Conclusion>& set){
+ int r[n];
+ int s[m];
+ int old_bound;
+ Conclusion conc;
+
+ if(r_or_s == 1){
+ if(new_bound < 1)
+ return;
+ // add r_i < bound
+ old_bound = glp_get_col_ub(sc, index+1);
+ if(new_bound == 1)
+ glp_set_col_bnds(sc, index+1, GLP_FX, 0, 0);
+ else
+ glp_set_col_bnds(sc, index+1, GLP_DB, 0, new_bound-1); // Minus once since need strictly less than. Glpk is less or equal.
+ }
+
+ if(r_or_s == 2){
+ if(new_bound+1 > limit)
+ return;
+ // add bound s_j > bound
+ old_bound = glp_get_col_lb(sc, index+n+1);
+ if(new_bound+1 == limit)
+ glp_set_col_bnds(sc, index+n+1, GLP_FX, limit, limit);
+ else
+ glp_set_col_bnds(sc, index+n+1, GLP_DB, new_bound+1, limit);
+ }
+
+ //Test output
+ //char str[15];
+ //sprintf(str, "output%d.txt", test_counter);
+ //glp_write_lp(sc, NULL, str);
+ //test_counter++;
+
+
+ // Solve
+ int result = glp_intopt(sc, parameters);
+
+ if(result == 0) { //if no errors from solver
+ if(glp_mip_status(sc)==GLP_OPT || glp_mip_status(sc)==GLP_FEAS){ // if feasible
+
+ // Load r and s from solution
+ for(int i=0; i < n; i++)
+ r[i] = static_cast<int>(glp_mip_col_val(sc, i+1));
+
+ for(int j=0; j < m; j++)
+ s[j] = static_cast<int>(glp_mip_col_val(sc, j+n+1));
+
+ // do all valuations
+ all_valuations(parameters, r, s, conc);
+
+
+ //if result isnt in list of conclusions then add it
+ bool already_have = false;
+ for(unsigned int i=0; i < set.size(); i++)
+ if( conc == set[i])
+ already_have = true;
+ if(!already_have)
+ set.push_back(conc);
+
+ // Recursively branch and solve the others - depth first
+ for(int i=0; i < n; i++)
+ solve_side_condition(sc, parameters, 1, i, r[i], limit, set);
+ for(int j=0; j < m; j++)
+ solve_side_condition(sc, parameters, 2, j, s[j], limit, set);
+ }
+ }
+ else if (result != GLP_ENOPFS) { // if not a feasibility error
+ cout << "glpk error: " << result << endl;
+ exit(1);
+ }
+ //remove bounds (go back up before branching down again).
+ if(r_or_s == 1)
+ glp_set_col_bnds(sc, index+1, GLP_DB, 0, old_bound);
+
+ if(r_or_s == 2)
+ glp_set_col_bnds(sc, index+n+1, GLP_DB, old_bound, limit);
+}
+
+void GML_Premise::all_valuations(glp_iocp* parameters, int* r, int* s, Conclusion& result){
+//Testing output
+cout << "====================" << endl;
+ for(int i=0; i < n; i++)
+ cout << "r[" << i << "] = " << r[i] << endl;
+
+ for(int j=0; j < m; j++)
+ cout << "s[" << j << "] = " << s[j] << endl;
+
+
+glp_prob *conclusion = glp_create_prob();
+glp_set_obj_dir(conclusion, GLP_MIN);
+glp_add_rows(conclusion, 2);
+glp_set_row_bnds(conclusion, 1, GLP_LO, 1, 0); // strictly greater than zero
+
+glp_add_cols(conclusion, n+m);
+
+for(int i=1; i < (n+m+1); i++)
+ glp_set_col_kind(conclusion, i, GLP_BV);
+
+// Arrays for inputting into glpk
+ double ar[2*(n+m)+1];
+ int ia[2*(n+m)+1];
+ int ja[2*(n+m)+1];
+
+ for(int i=1; i < n+m+1; i++){
+ ia[i]=1;
+ ia[n+m+i]=2;
+ ja[i]=i;
+ ja[n+m+i]=i;
+ }
+
+ int counter=1;
+ for(int i=0; i < n; i++){
+ ar[counter]= r[i];
+ counter++;
+ }
+
+ for(int j=0; j < m; j++){
+ ar[counter]=(-s[j]);
+ counter++;
+ }
+
+ for(int i=0; i < n+m; i++){
+ ar[counter]=pow(2,i);
+ counter++;
+ }
+
+ // Set objective function
+ for(int i=1; i < n+m+1; i++)
+ glp_set_obj_coef(conclusion, i, pow(2,i-1));
+
+ glp_load_matrix(conclusion, 2*(n+m), ia, ja, ar);
+
+ glp_set_row_bnds(conclusion, 2, GLP_LO, 0, 0);
+
+ // output for testing
+ //glp_write_lp(conclusion, NULL, "valuations.txt");
+
+ solve_conclusion_lp(conclusion, parameters, 0, result);
+
+ glp_delete_prob(conclusion);
+}
+
+void GML_Premise::solve_conclusion_lp(glp_prob* conclusion, glp_iocp* parameters, int min_limit, Conclusion& conc){
+ glp_set_row_bnds(conclusion, 2, GLP_LO, min_limit, 0);
+
+ int result = glp_intopt(conclusion, parameters);
+
+ if(result == 0){//if no errors from solver
+ if(glp_mip_status(conclusion)==GLP_OPT || glp_mip_status(conclusion)==GLP_FEAS){ // if feasible
+ int p[n+m];
+ for(int i=0; i<n+m; i++)
+ p[i]=glp_mip_col_val(conclusion, i+1);
+ //cout << glp_mip_col_val(conclusion, i+1);
+ Clause c(n+m,p);
+ conc.push_back(c);
+
+ solve_conclusion_lp(conclusion, parameters, glp_mip_obj_val(conclusion)+1, conc);
+ }
+ }
+ else if (result != GLP_ENOPFS) { // if not a feasibility error
+ cout << "glpk error: " << result << endl;
+ exit(1);
+ }
+}
+
+
+double GML_Premise::bound(){
+ return 2;
+ //return pow(2,6 * sizeoflp(n, m, a, b) * (n+m) * (n+m) * (n+m));
+}
+
+END OF DEPRECATED FUNCTIONS */
diff --git a/GMLMIP-0.1/rules/GML_premise.h b/GMLMIP-0.1/rules/GML_premise.h
new file mode 100644
index 0000000..513012f
--- /dev/null
+++ b/GMLMIP-0.1/rules/GML_premise.h
@@ -0,0 +1,33 @@
+#ifndef GML_PREMISE_H
+#define GML_PREMISE_H
+
+#include <cmath>
+#include <vector>
+
+#include "premise.h"
+#include "sizefunctions.h"
+#include "setofconclusions.h"
+
+class GML_Premise : public Premise<int>{
+ private:
+
+ /* Deprecated Functions which searched for solutions to the side condition first.
+ void load_side_condition(glp_prob* sc, double limit);
+ void solve_side_condition(glp_prob* side_condition, glp_iocp* parameters, int r_or_s, int index, int new_bound, double limit, vector<Conclusion>& set);
+ //r_or_s = 0 for neither, 1 for r, 2 for 2.
+
+ void all_valuations(glp_iocp* parameters, int* r, int* s, Conclusion& result);
+ void solve_conclusion_lp(glp_prob* conclusion, glp_iocp* parameters, int min_limit, Conclusion& conc);
+ */
+
+ // for testing
+ //int test_counter;
+ public:
+ GML_Premise();
+ GML_Premise(int _n, int _m, int* _a, int *_b);
+
+ //double bound(); // Deprecated.
+
+};
+
+#endif
diff --git a/GMLMIP-0.1/rules/PML_premise.cpp b/GMLMIP-0.1/rules/PML_premise.cpp
new file mode 100644
index 0000000..307c6fc
--- /dev/null
+++ b/GMLMIP-0.1/rules/PML_premise.cpp
@@ -0,0 +1,17 @@
+#include "PML_premise.h"
+PML_Premise::PML_Premise() : Premise<Rational>(){
+}
+
+PML_Premise::PML_Premise(int _n, int _m, Rational* _a, Rational* _b) : Premise<Rational>(_n,_m,_a,_b){
+//test_counter = 0;
+}
+
+
+/* Deprecated function
+double PML_Premise::bound(){
+ return pow(2,6 * (sizeoflp(n, m, a, b) + 1) * (n+m+1) * (n+m+1) * (n+m+1));
+ // +1 for the free k.
+}
+*/
+
+
diff --git a/GMLMIP-0.1/rules/PML_premise.h b/GMLMIP-0.1/rules/PML_premise.h
new file mode 100644
index 0000000..acdf0c0
--- /dev/null
+++ b/GMLMIP-0.1/rules/PML_premise.h
@@ -0,0 +1,26 @@
+#ifndef PML_PREMISE_H
+#define PML_PREMISE_H
+
+#include <cmath>
+#include <vector>
+
+#include "premise.h"
+#include "sizefunctions.h"
+
+
+class PML_Premise : public Premise<Rational>{
+ private:
+
+ /* Deprecated function
+ double bound();
+ */
+
+ // for testing
+ //int test_counter;
+ public:
+ PML_Premise();
+ PML_Premise(int _n, int _m, Rational* _a, Rational* _b);
+
+};
+
+#endif
diff --git a/GMLMIP-0.1/rules/makefile b/GMLMIP-0.1/rules/makefile
new file mode 100644
index 0000000..cac0ed3
--- /dev/null
+++ b/GMLMIP-0.1/rules/makefile
@@ -0,0 +1,34 @@
+GCC = g++
+GCCFLAGS = -Wall -Wno-deprecated
+
+all: premise.o GML_premise.o PML_premise.o valuation.o setofconclusions.o sizefunctions.o radixtree.o
+
+sizefunctions.o: sizefunctions.h sizefunctions.cpp
+ $(GCC) $(GCCFLAGS) -c sizefunctions.cpp
+
+premise.o: premise.h premise.cpp
+ $(GCC) $(GCCFLAGS) -c premise.cpp
+
+GML_premise.o: sizefunctions.h premise.h GML_premise.h GML_premise.cpp
+ $(GCC) $(GCCFLAGS) -c GML_premise.cpp
+
+PML_premise.o: sizefunctions.h premise.h PML_premise.h PML_premise.cpp
+ $(GCC) $(GCCFLAGS) -c PML_premise.cpp
+
+valuation.o: valuation.h valuation.cpp
+ $(GCC) $(GCCFLAGS) -c valuation.cpp
+
+setofconclusions.o: setofconclusions.h valuation.h premise.h setofconclusions.cpp
+ $(GCC) $(GCCFLAGS) -c setofconclusions.cpp
+
+radixtree.o: radixtree.h radixtree.cpp
+ $(GCC) $(GCCFLAGS) -c radixtree.cpp
+
+test: all test.o
+ $(GCC) $(GCCFLAGS) -lglpk -lbdd ../formulas/rational.o test.o premise.o GML_premise.o PML_premise.o valuation.o setofconclusions.o sizefunctions.o -o test
+
+test.o: test.cpp GML_premise.h valuation.h
+ $(GCC) $(GCCFLAGS) -c test.cpp
+
+clean:
+ rm -rf *~ *.o test *.txt
diff --git a/GMLMIP-0.1/rules/node.cpp b/GMLMIP-0.1/rules/node.cpp
new file mode 100644
index 0000000..aac26a7
--- /dev/null
+++ b/GMLMIP-0.1/rules/node.cpp
@@ -0,0 +1,46 @@
+#include "node.h"
+
+void Node::allow(int a){
+ valuations[a] = 1;
+}
+
+void Node::disallow(int d){
+ valuations[d] = 0;
+}
+
+Node::Node(int no_of_atoms) : size (static_cast<int>(pow(2, no_of_atoms))), valuations(size, 0){
+ //valuations.resize(size, 0);
+
+ // needs to be replaced with actually initing the stuff
+ //for(int i=0; i < size; i++)
+ //valuations[i]=0;
+}
+
+bool Node::operator==(const Node& other) const{
+ if(size == other.size){
+ for(int i=0; i < size; i++)
+ if(valuations[i] != other.valuations[i])
+ return false;
+ return true;
+ }
+ return false;
+}
+
+
+bool Node::operator<(const Node& other) const{
+ if(size == other.size){
+ for(int i=0; i < size; i++)
+ if(valuations[i]==1 && other.valuations[i]==0)
+ return false;
+ return true;
+ }
+ cout << "you checked for supersets with nodes of different sizes - you probably didn't mean to do this..." << endl;
+ return false;
+}
+
+ostream& operator<<(ostream& out, const Node& n){
+ out << n.size << endl;
+ for(int i=0; i < n.size; i++)
+ out << n.valuations[i] << " ";
+ out << endl;
+}
diff --git a/GMLMIP-0.1/rules/node.h b/GMLMIP-0.1/rules/node.h
new file mode 100644
index 0000000..55d6ec7
--- /dev/null
+++ b/GMLMIP-0.1/rules/node.h
@@ -0,0 +1,34 @@
+#ifndef NODE_H
+#define NODE_H
+
+#include <iostream>
+#include <cmath>
+#include <vector>
+
+using namespace std;
+
+class Node {
+ friend ostream& operator<<(ostream& out, const Node& n);
+ private:
+ //size comes from the premise. Premise with n literals gives 2^n size.
+ int size;
+
+ // bit vector: 0 = valuation not admitted, 1 = valuation is.
+ vector<bool> valuations;
+
+ public:
+ Node(){size = 0;};
+ Node(int no_of_atoms);
+
+ void allow(int a);
+ void disallow(int d);
+
+ //Copyable, assignable and comparable for use in STL
+ bool operator==(const Node& other) const;
+
+ // For checking supersets.
+ bool operator<(const Node& other) const;
+
+};
+
+#endif
diff --git a/GMLMIP-0.1/rules/premise.cpp b/GMLMIP-0.1/rules/premise.cpp
new file mode 100644
index 0000000..0db48b3
--- /dev/null
+++ b/GMLMIP-0.1/rules/premise.cpp
@@ -0,0 +1,110 @@
+#include "premise.h"
+
+template<class T>
+Premise<T>::Premise(){
+ n = 0;
+ m = 0;
+ total_valuations = 1 << (n+m);
+ a = NULL;
+ b = NULL;
+}
+
+template<class T>
+Premise<T>::Premise(int _n, int _m, T* _a, T* _b){
+ n =_n;
+ m =_m;
+ if (n+m > 30) {
+ cout << "Too many (>30) modal formulae in node." << endl;
+ exit(1);
+ }
+ total_valuations = 1 << (n+m);
+
+ if(n)
+ a = new T [n];
+ else
+ a = NULL;
+ if(m)
+ b = new T [m];
+ else
+ b = NULL;
+
+ for(int i=0; i < n; i++)
+ a[i]=_a[i];
+ for(int j=0; j < m; j++)
+ b[j]=_b[j];
+}
+
+template<class T>
+Premise<T>::Premise(const Premise<T>& p){
+ n = p.n;
+ m = p.m;
+ total_valuations = p.total_valuations;
+
+ if(n)
+ a = new T [n];
+ else
+ a = NULL;
+
+ if(m)
+ b = new T [m];
+ else
+ b = NULL;
+
+ for(int i=0; i < n; i++)
+ a[i]=p.a[i];
+ for(int j=0; j < m; j++)
+ b[j]=p.b[j];
+}
+
+template<class T>
+Premise<T>& Premise<T>::operator=(const Premise<T>& p){
+ if(this != &p){
+ if(a)
+ delete [] a;
+ if(b)
+ delete [] b;
+ n = p.n;
+ m = p.m;
+ total_valuations = p.total_valuations;
+
+ if(n)
+ a = new T [n];
+ else
+ a = NULL;
+ if(m)
+ b = new T [m];
+ else
+ b = NULL;
+
+ for(int i=0; i < n; i++)
+ a[i]=p.a[i];
+ for(int j=0; j < m; j++)
+ b[j]=p.b[j];
+ }
+ return *this;
+}
+
+template<class T>
+Premise<T>::~Premise(){
+ if(a)
+ delete [] a;
+ if(b)
+ delete [] b;
+}
+
+template<class T>
+T Premise<T>::get_a_i(int i){
+ if(a)
+ return a[i];
+ return -1;
+}
+
+template<class T>
+T Premise<T>::get_b_i(int i){
+ if(b)
+ return b[i];
+ return -1;
+}
+
+template class Premise<int>;
+template class Premise<Rational>;
diff --git a/GMLMIP-0.1/rules/premise.h b/GMLMIP-0.1/rules/premise.h
new file mode 100644
index 0000000..5f2882f
--- /dev/null
+++ b/GMLMIP-0.1/rules/premise.h
@@ -0,0 +1,76 @@
+#ifndef PREMISE_HH
+#define PREMISE_HH
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include <ext/hash_map>
+
+#include "../formulas/rational.h"
+
+using __gnu_cxx::hash;
+using namespace std;
+
+template<class T>
+class Premise {
+ protected:
+ // Naming follows from the names of the rules - kept as one letter for succinctness.
+ int n; // number of positive
+ int m; // number of negative
+ int total_valuations;
+ T* a; // modal indicies - positive
+ T* b; // modal indicies - negative
+
+ public:
+ Premise();
+ Premise(int _n, int _m, T* _a, T* _b);
+ Premise(const Premise<T>& p);
+ Premise<T>& operator=(const Premise<T>& p);
+ ~Premise();
+
+ int get_n(){ return n; };
+ int get_m(){ return m; };
+ int get_total_valuations(){ return total_valuations; };
+ T get_a_i(int i);
+ T get_b_i(int i);
+
+ struct Premise_hash {
+ hash <const char*> charhash;
+ size_t operator ()(const Premise<T>& p) const {
+ stringstream ss;
+ string s;
+ ss << p.n << " " << p.m << " ";
+ for(int i=0; i < p.n; i++)
+ ss << p.a[i] << " ";
+ for(int j=0; j < p.m; j++)
+ ss << p.b[j] << " ";
+ ss << '\0';
+ s = ss.str();
+ char buf[s.size()+1];
+ for(unsigned int i=0; i < s.size(); i++)
+ buf[i] = s[i];
+ buf[s.size()]='\0';
+ return charhash(buf);
+ }
+ };
+
+ struct Premise_equal { //TODO: this could be improved if we sort them as we input them
+ bool operator()(const Premise<T>& p1, const Premise<T>& p2) const{
+ if(p1.n!=p2.n)
+ return false;
+ if(p1.m!=p2.m)
+ return false;
+ for(int i=0; i < p1.n; i++)
+ if(p1.a[i]!=p2.a[i])
+ return false;
+ for(int j=0; j < p1.m; j++)
+ if(p1.b[j]!=p2.b[j])
+ return false;
+ return true;
+ }
+ };
+};
+
+
+#endif
diff --git a/GMLMIP-0.1/rules/radixtree.cpp b/GMLMIP-0.1/rules/radixtree.cpp
new file mode 100644
index 0000000..d639213
--- /dev/null
+++ b/GMLMIP-0.1/rules/radixtree.cpp
@@ -0,0 +1,55 @@
+#include "radixtree.h"
+
+void Radixtree::removeNodes(node* nd) {
+ if (nd->left)
+ removeNodes(nd->left);
+ if (nd->right)
+ removeNodes(nd->right);
+ delete nd;
+}
+
+void Radixtree::add_element(vector<bool>& elem) {
+ node *index = root;
+ for (int i = 0; i < depth; i++) {
+ if (elem[i]) {
+ if (!index->left)
+ index->left = new node;
+ index = index->left;
+ }
+ else {
+ if (!index->right)
+ index->right = new node;
+ index = index->right;
+ }
+ }
+}
+
+bool Radixtree::contains_element(vector<bool>& elem) {
+ node *index = root;
+ for (int i = 0; i < depth; i++) {
+ if (elem[i])
+ if (!index->left)
+ return false;
+ else
+ index = index->left;
+ else
+ if(!index->right)
+ return false;
+ else
+ index = index->right;
+ }
+ return true;
+}
+
+int Radixtree::size_intern(int d, node* nd) {
+ int size = 0;
+ if (!d)
+ size = 1;
+ else {
+ if (nd->left)
+ size += size_intern(d-1, nd->left);
+ if (nd->right)
+ size += size_intern(d-1, nd->right);
+ }
+ return size;
+}
diff --git a/GMLMIP-0.1/rules/radixtree.h b/GMLMIP-0.1/rules/radixtree.h
new file mode 100644
index 0000000..e78d54f
--- /dev/null
+++ b/GMLMIP-0.1/rules/radixtree.h
@@ -0,0 +1,36 @@
+#ifndef RADIXTREE_HH
+#define RADIXTREE_HH
+
+#include <vector>
+
+using namespace std;
+
+class Radixtree {
+ private:
+ typedef struct nd {
+ struct nd *left;
+ struct nd *right;
+ nd() { left = right = NULL; };
+ } node;
+
+ int depth;
+ node *root;
+
+ void removeNodes(node* nd);
+ int size_intern(int d, node* nd);
+
+ public:
+ Radixtree(int n) {
+ depth = n;
+ root = new node();
+ };
+
+ ~Radixtree(){ removeNodes(root); };
+
+ int size() { return size_intern(depth, root); };
+ void clear() { removeNodes(root); root = new node(); };
+ void add_element(vector<bool>& elem);
+ bool contains_element(vector<bool>& elem);
+};
+
+#endif
diff --git a/GMLMIP-0.1/rules/setofconclusions.cpp b/GMLMIP-0.1/rules/setofconclusions.cpp
new file mode 100644
index 0000000..d85e192
--- /dev/null
+++ b/GMLMIP-0.1/rules/setofconclusions.cpp
@@ -0,0 +1,35 @@
+#include "setofconclusions.h"
+
+SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
+ no_of_literals=n;
+
+ /* To limitate code change the new type given in (vector<unsigned int>) is converted to the old type vector<vector<TruthAssignment>>
+ Each unsigned int corresponds to a rule instance (a node of the tree). Each node is a set of truth assignments. */
+ int limit = 1 << n;
+ for(unsigned int i=0; i < set.size(); i++){
+ vector<bool> node = set[i];
+ vector<TruthAssignment> rule;
+ for(int j=0; j < limit; j++){
+ if(node[j])
+ rule.push_back(TruthAssignment(j,n));
+ }
+ rules.push_back(rule);
+ }
+}
+
+bdd SetOfConclusions::get_jth_conclusion(bdd** underlying, int j){
+ bdd b = bdd_false();
+ for(unsigned int i=0; i < rules[j].size(); i++){
+ bdd clause = bdd_true();
+ for(int k=0; k < no_of_literals; k++){
+ if(rules[j][i].get_p_i(k)==1)
+ clause = bdd_and(clause, *(underlying[k]));
+ if(rules[j][i].get_p_i(k)==0)
+ clause = bdd_and(clause, bdd_not(*(underlying[k])));
+ }
+ b = bdd_or(clause, b);
+
+ }
+ return b;
+}
+
diff --git a/GMLMIP-0.1/rules/setofconclusions.h b/GMLMIP-0.1/rules/setofconclusions.h
new file mode 100644
index 0000000..5a7d2af
--- /dev/null
+++ b/GMLMIP-0.1/rules/setofconclusions.h
@@ -0,0 +1,38 @@
+#ifndef SETOFCONCLUSIONS_H
+#define SETOFCONCLUSIONS_H
+
+
+#include <vector>
+
+#include <stdio.h>
+#include <cmath>
+
+#include "glpk.h"
+#include "bdd.h"
+
+#include "../formulas/rational.h"
+#include "valuation.h"
+
+
+using namespace std;
+
+typedef vector<TruthAssignment> Conclusion;
+
+class SetOfConclusions{
+ private:
+ int no_of_literals;
+ vector<Conclusion> rules;
+
+ public:
+ SetOfConclusions(){no_of_literals = 0;};
+ SetOfConclusions(int n, const vector<vector<bool> >& set);
+
+ int number_of_conclusions(){return rules.size();};
+ bdd get_jth_conclusion(bdd** underlying, int j);
+
+
+
+
+ //bdd get_ith_conclusion(int i, bdd* bddarray);
+};
+#endif
diff --git a/GMLMIP-0.1/rules/sizefunctions.cpp b/GMLMIP-0.1/rules/sizefunctions.cpp
new file mode 100644
index 0000000..bf15efc
--- /dev/null
+++ b/GMLMIP-0.1/rules/sizefunctions.cpp
@@ -0,0 +1,26 @@
+#include "sizefunctions.h"
+
+/* Functions for calculating size of a linear program */
+int sizeofcoef(int a){
+ int result = 1;
+ while (a >>= 1)
+ ++result;
+ return result;
+}
+
+int sizeofcoef(Rational a){
+ return 1 + sizeofcoef(a.get_top()) + sizeofcoef(a.get_bot());
+}
+
+template <class T>
+int sizeoflp(const int n, const int m, T* a, T* b){
+ int sum = 1 + n + m;
+ for(int i=0; i < n; i++)
+ sum+=sizeofcoef(a[i]);
+ for(int j=0; j < m; j++)
+ sum+=sizeofcoef(b[j]);
+ return sum;
+}
+
+template int sizeoflp<int>(const int, const int, int*, int*);
+template int sizeoflp<Rational>(const int, const int, Rational*, Rational*);
diff --git a/GMLMIP-0.1/rules/sizefunctions.h b/GMLMIP-0.1/rules/sizefunctions.h
new file mode 100644
index 0000000..3210fac
--- /dev/null
+++ b/GMLMIP-0.1/rules/sizefunctions.h
@@ -0,0 +1,11 @@
+#ifndef SIZEFUNCTIONS_H
+#define SIZEFUNCTIONS_H
+
+#include "../formulas/rational.h"
+
+int sizeofcoef(int a);
+int sizeofcoef(Rational a);
+template <class T>
+int sizeoflp(const int n, const int m, T* a, T* b);
+
+#endif
diff --git a/GMLMIP-0.1/rules/test.cpp b/GMLMIP-0.1/rules/test.cpp
new file mode 100644
index 0000000..4a48ce3
--- /dev/null
+++ b/GMLMIP-0.1/rules/test.cpp
@@ -0,0 +1,60 @@
+#include "GML_premise.h"
+
+#include "bdd.h"
+
+int main() {
+
+bdd_init(10000, 1000);
+bdd_setvarnum(100);
+
+// Create a premise object
+const int n = 1;
+const int m = 1;
+
+int a[n] = {2};
+int b[m] = {1};
+
+GML_Premise p(n,m,a,b);
+//p.construct_conclusions();
+
+//SetOfConclusions s(p.get_n_plus_m(), p.construct_conclusions());
+
+/*
+bdd underlying[3];
+for(int i = 0; i < 3; i++)
+underlying[i] = bdd_ithvarpp(i);
+
+//bdd_printdot(underlying[0]);
+
+bdd_printdot(s.get_jth_conclusion(underlying,2));
+*/
+
+
+vector<Conclusion> vec = p.construct_conclusions();
+ for(unsigned int i=0; i < vec.size(); i++){
+ cout << "Rule " << i << endl;
+ for(unsigned int j=0; j < vec[i].size(); j++){
+ cout << "Valuation " << j << ": ";
+ for(int k=0; k < vec[i][j].get_n(); k++){
+ cout << "p[" << k << "] = " << vec[i][j].get_p_i(k) << ", ";
+ }
+ cout << endl;
+ }
+ cout << "==================" << endl;
+}
+
+/* Testing new clause/valuation constructor */
+/*
+for(unsigned int j=0; j < 8; j++){
+ Clause c(j,3);
+ for(int k=0; k < 3; k++){
+ cout << "p[" << k << "] = " << c.get_p_i(k) << ", ";
+ }
+ cout << endl;
+}
+*/
+
+
+return 0;
+}
+
diff --git a/GMLMIP-0.1/rules/valuation.cpp b/GMLMIP-0.1/rules/valuation.cpp
new file mode 100644
index 0000000..9bf0ed4
--- /dev/null
+++ b/GMLMIP-0.1/rules/valuation.cpp
@@ -0,0 +1,71 @@
+#include "valuation.h"
+
+Valuation::Valuation(int i, int no_of_vars){
+ int limit = 1 << no_of_vars;
+ if(i >= limit){
+ cout << "cannot make clause " << i << " out of " << limit << endl;
+}
+ n = no_of_vars;
+
+ p = new int [n];
+
+ int ui = i;
+
+ for(int j=0; j < no_of_vars; j++){
+ p[j] = ui & 1;
+ ui >>=1;
+ }
+
+}
+
+
+Valuation::Valuation(int _n, int* _p){
+ n = _n;
+ p = new int [n];
+
+ for(int i=0; i < n; i++)
+ p[i]=_p[i];
+}
+
+Valuation::Valuation(const Valuation& c){
+ n = c.n;
+ p = new int [n];
+
+ for(int i=0; i < n; i++)
+ p[i]=c.p[i];
+}
+
+Valuation& Valuation::operator=(const Valuation& c){
+ if(this != &c){
+ if(p)
+ delete [] p;
+ n = c.n;
+ p = new int [n];
+
+ for(int i=0; i < n; i++)
+ p[i]=c.p[i];
+ }
+ return *this;
+}
+
+
+Valuation::~Valuation(){
+ if(p)
+ delete [] p;
+}
+
+int Valuation::get_p_i(int i){
+ if(p)
+ return p[i];
+ return -1;
+}
+
+bool Valuation::operator==(const Valuation& other) const{
+ if(n == other.n){
+ for(int i = 0; i < n; i++)
+ if(p[i]!=other.p[i])
+ return false;
+ return true;
+ }
+ return false;
+ }
diff --git a/GMLMIP-0.1/rules/valuation.h b/GMLMIP-0.1/rules/valuation.h
new file mode 100644
index 0000000..7f303b0
--- /dev/null
+++ b/GMLMIP-0.1/rules/valuation.h
@@ -0,0 +1,34 @@
+#ifndef VALUATION_H
+#define VALUATION_H
+
+#include <cmath>
+#include<iostream>
+
+using namespace std;
+
+/* This is a truth assignment */
+
+class Valuation {
+ private:
+ int n;
+ int* p;
+ public:
+ Valuation(){n=0; p=NULL;};
+ Valuation(int i, int total); // Gives valuation corresponding to ith valuation.
+ Valuation(int _n, int* p);
+ Valuation(const Valuation& c);
+ Valuation& operator=(const Valuation& c);
+ ~Valuation();
+ bool operator==(const Valuation& other) const;
+
+
+ int get_n(){ return n;};
+ int get_p_i(int i);
+};
+
+typedef Valuation Clause;
+// Since each valuation gives rise to a clause.
+// Valuation is used by deprecated side condition first code.
+typedef Valuation TruthAssignment;
+#endif
+
diff --git a/GMLMIP-0.1/satisfyingstack.h b/GMLMIP-0.1/satisfyingstack.h
new file mode 100644
index 0000000..97021dd
--- /dev/null
+++ b/GMLMIP-0.1/satisfyingstack.h
@@ -0,0 +1,12 @@
+#ifndef SATISFYINGSTACK_H
+#define SATISFYINGSTACK_H
+
+#include <vector>
+#include "./formulas/satisfyingassignment.h"
+
+using namespace std;
+
+//GLOBAL VARIABLE STACK FOR SATISFYING ASSIGNMENTS
+extern vector<SatisfyingAssignment> sat_ass_stack;
+
+#endif
diff --git a/GMLMIP-0.1/timeoutwrapper.sh b/GMLMIP-0.1/timeoutwrapper.sh
new file mode 100755
index 0000000..5c19d2e
--- /dev/null
+++ b/GMLMIP-0.1/timeoutwrapper.sh
@@ -0,0 +1,91 @@
+#!/bin/bash
+#
+# The Bash shell script executes a command with a time-out.
+# Upon time-out expiration SIGTERM (15) is sent to the process. If the signal
+# is blocked, then the subsequent SIGKILL (9) terminates it.
+#
+# Based on the Bash documentation example.
+
+# Hello Chet,
+# please find attached a "little easier" :-) to comprehend
+# time-out example. If you find it suitable, feel free to include
+# anywhere: the very same logic as in the original examples/scripts, a
+# little more transparent implementation to my taste.
+#
+# Dmitry V Golovashkin <Dmitry.Golovashkin@sas.com>
+
+scriptName="${0##*/}"
+
+declare -i DEFAULT_TIMEOUT=9
+declare -i DEFAULT_INTERVAL=1
+declare -i DEFAULT_DELAY=1
+
+# Timeout.
+declare -i timeout=DEFAULT_TIMEOUT
+# Interval between checks if the process is still alive.
+declare -i interval=DEFAULT_INTERVAL
+# Delay between posting the SIGTERM signal and destroying the process by SIGKILL.
+declare -i delay=DEFAULT_DELAY
+
+function printUsage() {
+ cat <<EOF
+
+Synopsis
+ $scriptName [-t timeout] [-i interval] [-d delay] command
+ Execute a command with a time-out.
+ Upon time-out expiration SIGTERM (15) is sent to the process. If SIGTERM
+ signal is blocked, then the subsequent SIGKILL (9) terminates it.
+
+ -t timeout
+ Number of seconds to wait for command completion.
+ Default value: $DEFAULT_TIMEOUT seconds.
+
+ -i interval
+ Interval between checks if the process is still alive.
+ Positive integer, default value: $DEFAULT_INTERVAL seconds.
+
+ -d delay
+ Delay between posting the SIGTERM signal and destroying the
+ process by SIGKILL. Default value: $DEFAULT_DELAY seconds.
+
+As of today, Bash does not support floating point arithmetic (sleep does),
+therefore all delay/time values must be integers.
+EOF
+}
+
+# Options.
+while getopts ":t:i:d:" option; do
+ case "$option" in
+ t) timeout=$OPTARG ;;
+ i) interval=$OPTARG ;;
+ d) delay=$OPTARG ;;
+ *) printUsage; exit 1 ;;
+ esac
+done
+shift $((OPTIND - 1))
+
+# $# should be at least 1 (the command to execute), however it may be strictly
+# greater than 1 if the command itself has options.
+if (($# == 0 || interval <= 0)); then
+ printUsage
+ exit 1
+fi
+
+# kill -0 pid Exit code indicates if a signal may be sent to $pid process.
+(
+ ((t = timeout))
+
+ while ((t > 0)); do
+ sleep $interval
+ kill -0 $$ || exit 0
+ ((t -= interval))
+ done
+
+ # Be nice, post SIGTERM first.
+ # The 'exit 0' below will be executed if any preceeding command fails.
+ kill -s SIGTERM $$ && kill -0 $$ || exit 0
+ sleep $delay
+ kill -s SIGKILL $$
+) 2> /dev/null &
+
+exec "$@"
diff --git a/INSTALL b/INSTALL
index b727996..2bfd33e 100644
--- a/INSTALL
+++ b/INSTALL
@@ -11,6 +11,13 @@ Dependencies:
- ocamlfind (package called ocaml-findlib)
- ocamlgraph (package ocaml-ocamlgraph)
+ - Dependencies for GMLMIP-0.1:
+ * GNU LPK
+ * Flex
+ * Bison
+ * Googlesparsehash package
+ * BuDDy BDD package.
+
Build
-----
@@ -41,7 +48,6 @@ Some formulas are
<{ 1 2 }> C & <{ 1 2 3 4 5 6 7 8 9 }> ~C
<{ 1 2 }> C & <{ 1 2 }> ~C
<{ 1 2 }> C & [{ 1 2 }] ~C
- <{ 1 2 }> C & [{ 1 2 }] ~C
So call for example:
--
GitLab