diff --git a/_oasis b/_oasis
index 707258ad5d3999092020f6af8b711e11b5852a64..f68d16d6c46edb07cffdc13979539ca4637f7fb4 100644
--- a/_oasis
+++ b/_oasis
@@ -25,48 +25,9 @@ Library libcool
ByteOpt: -cc g++
CCOpt: -std=c++98 -x c++
# TODO: activate glpk_stub.c again
- CSources: gmlmip_stub.c,
- minisat_stub.c,
- GMLMIP-0.1/rules/sizefunctions.c,
- GMLMIP-0.1/rules/setofconclusions.c,
- GMLMIP-0.1/rules/PML_premise.c,
- GMLMIP-0.1/rules/valuation.c,
- GMLMIP-0.1/rules/node.c,
- GMLMIP-0.1/rules/premise.c,
- GMLMIP-0.1/rules/radixtree.c,
- GMLMIP-0.1/rules/GML_premise.c,
- GMLMIP-0.1/parser/mlf-parser.tab.c,
- GMLMIP-0.1/parser/mlf-driver.c,
- GMLMIP-0.1/parser/lex.yy.c,
- GMLMIP-0.1/formulas/GML_formula.c,
- GMLMIP-0.1/formulas/rational.c,
- GMLMIP-0.1/formulas/formula.c,
- GMLMIP-0.1/formulas/satisfyingassignment.c,
- GMLMIP-0.1/formulas/PML_formula.c,
- GMLMIP-0.1/onestep.c,
- GMLMIP-0.1/onestep.h,
- GMLMIP-0.1/rules/premise.h,
- GMLMIP-0.1/rules/node.h,
- GMLMIP-0.1/rules/radixtree.h,
- GMLMIP-0.1/rules/setofconclusions.h,
- GMLMIP-0.1/rules/valuation.h,
- GMLMIP-0.1/rules/PML_premise.h,
- GMLMIP-0.1/rules/sizefunctions.h,
- GMLMIP-0.1/rules/GML_premise.h,
- GMLMIP-0.1/parser/stack.h,
- GMLMIP-0.1/parser/mlf-driver.h,
- GMLMIP-0.1/parser/mlf-parser.tab.h,
- GMLMIP-0.1/parser/lex.yy.h,
- GMLMIP-0.1/parser/location.h,
- GMLMIP-0.1/parser/position.h,
- GMLMIP-0.1/formulas/satisfyingassignment.h,
- GMLMIP-0.1/formulas/GML_formula.h,
- GMLMIP-0.1/formulas/formula.h,
- GMLMIP-0.1/formulas/PML_formula.h,
- GMLMIP-0.1/formulas/rational.h,
- GMLMIP-0.1/satisfyingstack.h
+ CSources: minisat_stub.c
InternalModules: ALCFormula, ALCGraph, ALCMisc, CoAlgLogicUtils,
- CoAlgLogics, HashConsing, MiscSolver, AltGenlex, Gmlmip,
+ CoAlgLogics, HashConsing, MiscSolver, AltGenlex,
Minisat
Modules: CoAlgMisc,
CoAlgFormula,
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index 30f4ec3a0d94466609ec0b2834704f752422fae0..2bfbf206c16f339affdb9ead83fd1fa5522404e6 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -53,14 +53,12 @@ let printUsage () =
print_endline " CoalitionLogic (or equivalently CL)";
print_endline " Const id1 ... idn (or equivalently Constant id1 ... idn)";
print_endline " Id (or equivalently Identity)";
- print_endline " PML";
- print_endline " GML";
print_endline " }";
print_endline " where you can compose functors by:";
print_endline " <functor> + <functor> (weakest precedence)";
print_endline " or <functor> * <functor>";
print_endline " or <functor> . <functor> (binds strongest)";
- print_endline " (so K+KD.CL*PML stand for (K + ((KD.CL) * PML)))";
+ print_endline " (so K+KD.CL*Id stand for (K + ((KD.CL) * Id)))";
print_endline " <flags> = a list of the following items";
print_endline " --agents AGLIST";
print_endline " expects the next argument AGLIST to be a list of integers";
@@ -78,7 +76,6 @@ let printUsage () =
print_endline " @ ident' (satisfaction operator)";
print_endline " [R], <R> (universal/existential restrictions along role R";
print_endline " [{ aglist }], <{ aglist }> (aglist can force / cannot avoid)";
- print_endline " {<= n}, {>= n}, {< n}, {> n} (number / probability of successors)";
print_endline " =ident (constant value)";
print_endline " O (identity operator)";
print_endline " _ + _ (choice)";
@@ -97,6 +94,9 @@ let verbose = ref false
let choiceSat () =
let verb = !verbose in
let sorts = (FE.sortTableFromString Sys.argv.(2)) in
+ if Array.exists (fun (func,_) -> func == CM.GML || func == CM.PML) sorts then
+ raise (CF.CoAlgException "GML and PML are currently not supported")
+ else ();
let printRes sat =
if not verb then
print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index fd46280ae2faeba53026db0dc5be8ff2cccccaf3..4b899652462f15b70b303de0f6de64c4d1f5450a 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -6,7 +6,6 @@
open CoAlgMisc
open CoolUtils
open CoAlgLogicUtils
-open Gmlmip
module S = MiscSolver
@@ -463,99 +462,16 @@ let mkRule_CL sort bs defer sl : stateExpander =
*)
lazylistFromList rules
+(* PML and GML are currently disabled, because they required GMLMIP, which
+ complicated the build process and had issues.
+
+ The implementation can still be found in the git history.
+ *)
let mkRule_GML sort bs defer sl : stateExpander =
- assert (List.length sl = 1);
- let defer1 = bsetMake () in (* TODO: track deferrals *)
- let s1 = List.hd sl in (* [s1] = List.hd sl *)
- let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
- let boxes = bsetFilter bs (fun f -> lfGetType sort f = MaxExceptF) in
- let roles = S.makeBS () in
- (* step 1: for each diamond/box add R *)
- let addRole formula =
- ignore (S.addBSNoChk roles (lfGetDest3 sort formula))
- in
- bsetIter addRole boxes;
- bsetIter addRole diamonds;
- let addRule role acc =
- let premise: (bool*int*int) list =
- let modality isDiamond m acc =
- if lfGetDest3 sort m = role
- then (isDiamond,lfGetDestNum sort m,lfToInt (lfGetDest1 sort m))::acc
- else acc
- in
- List.append
- (bsetFold (modality true) diamonds [])
- (bsetFold (modality false) boxes [])
- in
- let conclusion = gml_rules premise in
- (* conclusion is a set of rules, *each* of the form \/ /\ lit *)
- let handleRuleConcl rc acc =
- let handleConjunction conj =
- let res = bsetMake () in
- List.iter (fun (f,positive) ->
- let f = lfFromInt f in
- let f = if positive then f else
- match lfGetNeg sort f with
- | Some nf -> nf
- | None -> raise (CoAlgFormula.CoAlgException ("Negation of formula missing"))
- in
- bsetAdd res f)
- conj;
- (s1,res, defer1)
- in
- let rc = List.map handleConjunction rc in
- ((fun bs1 -> bs),lazylistFromList rc)::acc
- in List.fold_right handleRuleConcl conclusion acc
- in
- let rules = S.foldBS addRule roles [] in
- lazylistFromList rules
+ raise (CoAlgFormula.CoAlgException "GML is currently not implemented.")
let mkRule_PML sort bs defer sl : stateExpander =
- assert (List.length sl = 1);
- let defer1 = bsetMake () in (* TODO: track deferrals *)
- let s1 = List.hd sl in (* [s1] = List.hd sl *)
- let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AtLeastProbF) in
- let boxes = bsetFilter bs (fun f -> lfGetType sort f = LessProbFailF) in
- let premise: (bool*int*int*int) list =
- let modality isDiamond m acc =
- let nominator = lfGetDestNum sort m in
- let denominator = lfGetDestNum2 sort m in
- let nestedFormula = lfToInt (lfGetDest1 sort m) in
- (*print_endline ("putting formula "^(string_of_int nestedFormula)); *)
- (isDiamond,nominator,denominator,nestedFormula)::acc
- in
- List.append
- (bsetFold (modality true) diamonds [])
- (bsetFold (modality false) boxes [])
- in
- let conclusion = pml_rules premise in
- let error message = raise (CoAlgFormula.CoAlgException message) in
- (* conclusion is a set of rules, *each* of the form \/ /\ lit *)
- let handleRuleConcl rc acc =
- let handleConjunction conj =
- let res = bsetMake () in
- let handleLiteral = fun (f_int,positive) -> begin
- let f = lfFromInt f_int in
- let f = if positive
- then f
- else begin
- (*print_endline ("getting "^(string_of_int f_int)); *)
- match lfGetNeg sort f with
- | Some nf -> nf
- | None -> error ("Negation of formula missing")
- end
- in
- bsetAdd res f
- end
- in
- List.iter handleLiteral conj;
- (s1,res, defer1)
- in
- let rc = List.map handleConjunction rc in
- ((fun bs1 -> bs),lazylistFromList rc)::acc
- in
- let rules = List.fold_right handleRuleConcl conclusion [] in
- lazylistFromList rules
+ raise (CoAlgFormula.CoAlgException "PML is currently not implemented.")
(* constant functor *)
let mkRule_Const colors sort bs defer sl : stateExpander =
diff --git a/src/lib/GMLMIP-0.1/.gitignore b/src/lib/GMLMIP-0.1/.gitignore
deleted file mode 100644
index bc7e2fddd40691c8f790a1872dd29c364c1f6507..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-main
-onestep
diff --git a/src/lib/GMLMIP-0.1/README.txt b/src/lib/GMLMIP-0.1/README.txt
deleted file mode 100644
index f31b51f625a5240f816b238c73d54c3cb3cd79ea..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/README.txt
+++ /dev/null
@@ -1,79 +0,0 @@
-===============================
-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/src/lib/GMLMIP-0.1/config.mk b/src/lib/GMLMIP-0.1/config.mk
deleted file mode 100644
index 9b5d1ab09da6e141d8d07225fa3ec4abf8dd22b2..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/config.mk
+++ /dev/null
@@ -1,7 +0,0 @@
-
-BISON = bison
-LEX = flex
-GCC = g++
-
-GCCFLAGS = -Wall -Wno-deprecated
-
diff --git a/src/lib/GMLMIP-0.1/formulas/GML_formula.c b/src/lib/GMLMIP-0.1/formulas/GML_formula.c
deleted file mode 100644
index 1fc45b47ada7a65239bd308748c2159f67006d9a..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/GML_formula.c
+++ /dev/null
@@ -1,80 +0,0 @@
-#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/src/lib/GMLMIP-0.1/formulas/GML_formula.h b/src/lib/GMLMIP-0.1/formulas/GML_formula.h
deleted file mode 100644
index a24a13b74cba0677258f271facce1a5096e348ae..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/GML_formula.h
+++ /dev/null
@@ -1,14 +0,0 @@
-#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/src/lib/GMLMIP-0.1/formulas/PML_formula.c b/src/lib/GMLMIP-0.1/formulas/PML_formula.c
deleted file mode 100644
index c4c04ab4c11b508e5771fe6a1376f4f5b3071fd1..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/PML_formula.c
+++ /dev/null
@@ -1,102 +0,0 @@
-#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/src/lib/GMLMIP-0.1/formulas/PML_formula.h b/src/lib/GMLMIP-0.1/formulas/PML_formula.h
deleted file mode 100644
index 8e04b3fed720d5f4b466d87852c35f9d938c6ace..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/PML_formula.h
+++ /dev/null
@@ -1,14 +0,0 @@
-#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/src/lib/GMLMIP-0.1/formulas/formula.c b/src/lib/GMLMIP-0.1/formulas/formula.c
deleted file mode 100644
index 06bd40c0e81478cccf78f23ee002c8a2ccc82e42..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/formula.c
+++ /dev/null
@@ -1,324 +0,0 @@
-#include "formula.h"
-
-#include <set>
-#include <cassert>
-
-IFormula::~IFormula() {
-}
-
-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;
-}
-
-vector<SatisfyingAssignment> gatherer_stack;
-
-void sat_handler_gatherer(char *varset, int size){
- SatisfyingAssignment s(size, varset);
- gatherer_stack.push_back(s);
-}
-
-template<class ModalValueType>
-set<set<int> > Formula<ModalValueType>::gatherRules(bdd b) {
- bdd_allsat(b, sat_handler_gatherer);
- vector<SatisfyingAssignment> sat_ass = gatherer_stack;
- gatherer_stack.clear();
- set<set<int> > disj;
- for (vector<SatisfyingAssignment>::iterator it = sat_ass.begin();
- it != sat_ass.end(); ++it)
- {
- set<int> conj;
- SatisfyingAssignment& sat = *it;
- for (int v = 0; v < sat.get_size(); v++) {
- if (sat.get_array_i(v) != 1 && sat.get_array_i(v) != 0) continue;
- if (!variables_back.count(v)) continue;
- int sgn = ((sat.get_array_i(v)==1) ? 1 : (-1));
- conj.insert(variables_back[v] * sgn);
- }
- disj.insert(conj);
- }
- return disj;
-}
-
-void sat_handler(char *varset, int size){
- SatisfyingAssignment s(size, varset);
- sat_ass_stack.push_back(s);
-}
-
-template<class ModalValueType>
-RuleCollection Formula<ModalValueType>::check_satisfiability(bdd b){
- //bdd_printdot(b);
- bdd_allsat(b, sat_handler); // pushes satisfying assignment onto stack
- vector<SatisfyingAssignment> sat_ass = sat_ass_stack;
- sat_ass_stack.clear();
- // it might be zero if already on the syntactic level there is something like A /\ ~A
- assert(sat_ass.size() <= 1);
- if (sat_ass.size() == 1) {
- return apply_rules(sat_ass[0]);
- } else {
- // TODO: return {} or { {} }?
- // the secound one would mean { False }
- return set<set<set<int> > >();
- }
-}
-
-template<class ModalValueType>
-RuleCollection Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
- RuleCollection result;
-
- 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(); i++){
- bdd b = concs.get_jth_conclusion(underlying_formulae, i);
- result.insert(gatherRules(b));
- }
- } else {
- RuleCollection r = enumerate_rules(premise, underlying_formulae);
- result.insert(r.begin(), r.end());
- }
-
- delete [] underlying_formulae;
- delete [] positive_modal_indices;
- delete [] negative_modal_indices;
- }
-
- return result;
-}
-
-template<class ModalValueType>
-RuleCollection Formula<ModalValueType>::enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae){
- RuleCollection result;
- 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)) {
- } else {
- node_queue.push_back(zero);
- //int i = 0;
- while(node_queue.size()) {
- //cout << "outer space: " << i++ << " runs: " << test_counter << " queue: " << node_queue.size() << " sols: " << valid_nodes.size() << " antisols: " << anti_nodes.size() << endl;
- RuleCollection r = enum_rules_intern(problem, parameters, prem, underlying_formulae, node_queue, valid_nodes, anti_nodes);
- result.insert(r.begin(), r.end());
- }
- if (!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>
-RuleCollection 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){
- RuleCollection result;
- vector<vector<bool> > new_node_queue;
- int total_valuations = prem.get_total_valuations();
-
- for (unsigned int k = 0; k < node_queue.size(); 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; 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.insert(gatherRules(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/src/lib/GMLMIP-0.1/formulas/formula.h b/src/lib/GMLMIP-0.1/formulas/formula.h
deleted file mode 100644
index e7a50c40173a128afda7a8b55f9399a84d888c2b..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/formula.h
+++ /dev/null
@@ -1,168 +0,0 @@
-#ifndef FORMULA_HH
-#define FORMULA_HH
-
-#include <iostream>
-#include <cstdlib>
-#include <cstring>
-#include <iomanip>
-#include <sstream>
-#include <string>
-#include <set>
-#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;
-
-typedef set<set<set<int> > > RuleCollection;
-
-// Formula interface so we can have abstract template class pointers.
-class IFormula {
- public:
- virtual ~IFormula();
- 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;
- virtual RuleCollection onestep() = 0;
- virtual int get_variables_back(int bddvar) = 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;
-
- RuleCollection check_satisfiability(bdd b);
- RuleCollection apply_rules(SatisfyingAssignment& sat);
- RuleCollection enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae);
- RuleCollection 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;
- int get_variables_back(int bddvar) { return variables_back[bddvar]; }
- set<set<int> > gatherRules(bdd b);
-
- bool satisfiability(int option){ assert(0=="patched GMLMIP\n"); return true;};
- RuleCollection onestep() { 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/src/lib/GMLMIP-0.1/formulas/makefile b/src/lib/GMLMIP-0.1/formulas/makefile
deleted file mode 100644
index f2465b1a0a23f29f993a8f8708f71b55175569f6..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/makefile
+++ /dev/null
@@ -1,21 +0,0 @@
-include ../config.mk
-
-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/src/lib/GMLMIP-0.1/formulas/rational.c b/src/lib/GMLMIP-0.1/formulas/rational.c
deleted file mode 100644
index a0b5a1022c50f976cc6e2c1e05e4ce7a4ddfab77..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/rational.c
+++ /dev/null
@@ -1,29 +0,0 @@
-#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/src/lib/GMLMIP-0.1/formulas/rational.h b/src/lib/GMLMIP-0.1/formulas/rational.h
deleted file mode 100644
index 2e41dd433a31d340aa66c824443d7545246fea92..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/rational.h
+++ /dev/null
@@ -1,26 +0,0 @@
-#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/src/lib/GMLMIP-0.1/formulas/satisfyingassignment.c b/src/lib/GMLMIP-0.1/formulas/satisfyingassignment.c
deleted file mode 100644
index 3f9b1b050f6c0590606e789a96b3c7c0762f1573..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/satisfyingassignment.c
+++ /dev/null
@@ -1,64 +0,0 @@
-#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/src/lib/GMLMIP-0.1/formulas/satisfyingassignment.h b/src/lib/GMLMIP-0.1/formulas/satisfyingassignment.h
deleted file mode 100644
index 7ad55650722760a69481739f9ab34ba0ed054369..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/formulas/satisfyingassignment.h
+++ /dev/null
@@ -1,26 +0,0 @@
-#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/src/lib/GMLMIP-0.1/input b/src/lib/GMLMIP-0.1/input
deleted file mode 100644
index 66bbf4fa593e43fca7a83b7d7f3c30ecd3d4adef..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/input
+++ /dev/null
@@ -1,2 +0,0 @@
-Logic:GML
-<3>p0 & <3>~p0 & ~<5>true
diff --git a/src/lib/GMLMIP-0.1/main.c b/src/lib/GMLMIP-0.1/main.c
deleted file mode 100644
index 219c05539b0d7d21a9673edf774a5681242bdeb7..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/main.c
+++ /dev/null
@@ -1,70 +0,0 @@
-#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();
- fprintf(stderr,"Cannot check satisfiability due to patched GMLMIP\n");
- //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/src/lib/GMLMIP-0.1/makefile b/src/lib/GMLMIP-0.1/makefile
deleted file mode 100644
index 934e0e7a2eaefa0ffff0a9122059b6d56afa3842..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/makefile
+++ /dev/null
@@ -1,51 +0,0 @@
-
-include config.mk
-
-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
-
-HEADERS = parser/mlf-parser.tab.h \
-parser/mlf-driver.h \
-formulas/formula.h \
-formulas/satisfyingassignment.h \
-parser/lex.yy.h
-
-.PHONY: all clean parser/% formulas/% rules/%
-
-all: main onestep-example onestep.o
-
-.PHONY: phony
-# don't do anything here
-phony:
- @:
-
-
-parser/%: phony
- @make --no-print-directory -C parser/ $(@:parser/%=%)
-
-formulas/%: phony
- @make --no-print-directory -C formulas/ $(@:formulas/%=%)
-
-rules/%: phony
- @make --no-print-directory -C rules/ $(@:rules/%=%)
-
-
-main: main.o $(POBJS) $(FOBJS) $(ROBJS)
- $(GCC) $(GCCFLAGS) $(POBJS) $(FOBJS) $(ROBJS) -lbdd -lm -lglpk $< -o $@
-
-onestep-example: onestep-example.o $(POBJS) $(FOBJS) $(ROBJS) onestep.o
- $(GCC) $(GCCFLAGS) $(POBJS) $(FOBJS) $(ROBJS) onestep.o -lbdd -lm -lglpk $< -o $@
-
-
-main.o: main.cpp $(HEADERS)
- $(GCC) $(GCCFLAGS) -c $< -o $@
-
-onestep-example.o: onestep-example.cpp $(HEADERS)
- $(GCC) $(GCCFLAGS) -c $<
-
-onestep.o: onestep.cpp $(HEADERS)
- $(GCC) $(GCCFLAGS) -c $<
-
-clean: parser/clean formulas/clean rules/clean
- rm -rf *.o main
diff --git a/src/lib/GMLMIP-0.1/onestep-example.c b/src/lib/GMLMIP-0.1/onestep-example.c
deleted file mode 100644
index 3283733cc50733ff89e8e894f4f5846e74d97118..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/onestep-example.c
+++ /dev/null
@@ -1,68 +0,0 @@
-#include <iostream>
-#include <vector>
-#include <time.h>
-
-#include "bdd.h"
-#include "./formulas/formula.h"
-#include "./formulas/GML_formula.h"
-#include "./formulas/PML_formula.h"
-#include "./formulas/rational.h"
-#include "./formulas/satisfyingassignment.h"
-#include "satisfyingstack.h"
-#include "./parser/mlf-driver.h"
-#include "onestep.h"
-
-using namespace std;
-
-int main (int argc, char *argv[]){
- clock_t total_time = clock();
- IFormula* f = NULL;
- // this turns into an endless loop
- //bdd b = bdd_and(f->modal(new bdd(f->variable(0)), 4, 0),
- // bdd_not(f->modal(new bdd(f->variable(0)), 6, 0)));
- if (true) {
- mlf_driver driver;
- driver.set_formula_gml();
- if (!driver.parse ("-")) {
- driver.extract_formula(f);
- }
- } else {
- f = new GML_Formula;
- bdd b = bdd_and(bdd_and(f->modal(new bdd(f->variable(8)), 4, 0),
- bdd_not(f->modal(new bdd(bdd_not(f->variable(7))), 3, 0))),
- bdd_not(f->modal(new bdd(bdd_not(f->variable(9))), 3, 0)));
- f->set_bdd(b);
- }
- // 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();
- //vector<RuleChild> res = f->onestep_rules(b);
- //cout << res.size() << " childs" << endl;
- //for (unsigned int r = 0; r < res.size(); r++) {
- // RuleChild& rc = res[r];
- // for (unsigned int i = 0; i < rc.size(); i++) {
- // cout << "\\/ (";
- // for (unsigned int j = 0; j < rc[i].size(); j++) {
- // pair<bool,int>& p = rc[i][j];
- // if (j != 0) cout << ", ";
- // if (!p.first) cout << "~";
- // cout << p.second;
- // }
- // cout << ")";
- // }
- // cout << endl;
- //}
- if (f) {
- RuleCollection vsa = f->onestep();
- printRuleCollection(vsa);
- f->clear_maps();
- delete f;
- }
- total_time = clock() - total_time;
- cout << "Total Time: " << static_cast<float>(total_time) / CLOCKS_PER_SEC << endl;
- return 0;
-}
-
diff --git a/src/lib/GMLMIP-0.1/onestep.c b/src/lib/GMLMIP-0.1/onestep.c
deleted file mode 100644
index ddc0e8b8153a9afa96aeccc09f48d7ec953a79ae..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/onestep.c
+++ /dev/null
@@ -1,143 +0,0 @@
-#include <iostream>
-#include <vector>
-#include <time.h>
-#include "onestep.h"
-
-#include "bdd.h"
-#include "./formulas/formula.h"
-#include "./formulas/GML_formula.h"
-#include "./formulas/PML_formula.h"
-#include "./formulas/rational.h"
-#include "./formulas/satisfyingassignment.h"
-#include "./rules/setofconclusions.h"
-#include "satisfyingstack.h"
-
-using namespace std;
-
-vector<SatisfyingAssignment> sat_ass_stack;
-
-/* Error handler for running out of BDD nodes */
-static void error_handler(int errorcode){
- if(errorcode==BDD_VAR)
- bdd_extvarnum(1000);
- else
- cerr << "BDD package error number " << errorcode << endl;
-}
-
-// use C++-Magic to initialize and destroy bdd library
-class BDDInitializer { public:
- BDDInitializer() {
- bdd_init(100000, 10000);
- bdd_setvarnum(100); // Minimum is two.
- bdd_error_hook(error_handler);
- };
- ~BDDInitializer() {
- bdd_done();
- };
-};
-
-BDDInitializer initializeBddLibrary;
-
-/*
- * FOR GML
- */
-
-// some utils
-static bdd tupleModality2Bdd_GML(IFormula* f, const pair<pair<bool,int>,int>& t) {
- if (t.first.first) {
- /* diamond */
- bdd* b = new bdd(f->variable(t.second));
- return f->modal(b, t.first.second, 0);
- } else {
- /* box */
- bdd* b = new bdd(bdd_not(f->variable(t.second)));
- return bdd_not(f->modal(b, t.first.second, 0));
- }
-}
-
-
-GMLConclusion gmlmip_onestep_gml(GMLPremise modvec) {
- IFormula* f = NULL;
- if (modvec.size() <= 0) {
- // Nothing to do -> no rules
- GMLConclusion rulevec;
- return rulevec;
- } else {
- f = new GML_Formula;
- bdd b = tupleModality2Bdd_GML(f, modvec[0]);
- for (unsigned int i = 1; i < modvec.size(); i++) {
- b = bdd_and(b, tupleModality2Bdd_GML(f, modvec[i]));
- }
- f->set_bdd(b);
- RuleCollection vsa = f->onestep();
- f->clear_maps();
- delete f;
- return vsa;
- }
-}
-
-/*
- * FOR PML
- */
-
-static bdd tupleModality2Bdd_PML(IFormula* f, const pair<pair<bool,pair<int,int> >,int>& t) {
- if (t.first.first) {
- /* diamond */
- bdd* b = new bdd(f->variable(t.second));
- return f->modal(b, t.first.second.first, t.first.second.second);
- } else {
- /* box */
- bdd* b = new bdd(bdd_not(f->variable(t.second)));
- return bdd_not(f->modal(b, t.first.second.first, t.first.second.second));
- }
-}
-
-
-GMLConclusion gmlmip_onestep_pml(PMLPremise modvec) {
- IFormula* f = NULL;
- if (modvec.size() <= 0) {
- // Nothing to do -> no rules
- GMLConclusion rulevec;
- return rulevec;
- } else {
- f = new PML_Formula;
- bdd b = tupleModality2Bdd_PML(f, modvec[0]);
- for (unsigned int i = 1; i < modvec.size(); i++) {
- b = bdd_and(b, tupleModality2Bdd_PML(f, modvec[i]));
- }
- f->set_bdd(b);
- RuleCollection vsa = f->onestep();
- f->clear_maps();
- delete f;
- return vsa;
- }
-}
-
-/*
- * Debug output:
- */
-void printRuleCollection(const RuleCollection& rc) {
- cout << rc.size() << " rules\n";
- for (RuleCollection::iterator it = rc.begin(); it != rc.end(); ++it) {
- const set<set<int> > &r = *it;
- bool first = true;
- cout << "(\\/ ";
- for (set<set<int> >::iterator jt = r.begin(); jt != r.end(); ++jt) {
- const set<int>& clause = *jt;
- if (first) first = false; else cout << "\n ";
- cout << "(/\\";
- for (set<int>::iterator kt = clause.begin(); kt != clause.end(); ++kt) {
- int v = *kt;
- if (v > 0) {
- cout << " p" << v;
- } else {
- cout << " ¬p" << (-v);
- }
- }
- cout << " )";
- }
- cout << ")";
- cout << endl << endl;
- }
-}
-
diff --git a/src/lib/GMLMIP-0.1/onestep.h b/src/lib/GMLMIP-0.1/onestep.h
deleted file mode 100644
index efefbe0776d8fb3efe5a3f4d9b4e9b6f196bf716..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/onestep.h
+++ /dev/null
@@ -1,33 +0,0 @@
-#ifndef __GMLMIP_ONESTEP_H_
-#define __GMLMIP_ONESTEP_H_
-
-#include <vector>
-#include <set>
-#include <utility> // for pair
-#include "formulas/formula.h"
-
-
-/* transforms list of gml formulas (diamond?,number,formula)
- to list of consequences (formula,positive?),
- here positive? means that the formula must be true in order to make the
- given conjunct of modalities true
-*/
-typedef std::vector<std::pair<std::pair<bool,int>,int> > GMLPremise;
-/*
- * For PML, the premise is a list of modal formulas:
- * ((diamond?,(nominator,denominator)),formula)
- */
-typedef std::vector<std::pair<std::pair<bool,std::pair<int,int> >,int> > PMLPremise;
-/*
- * The Conclusion is the same for PML and GML:
- * It is a set of rule conclusions. One rule conclusions is of the form \/ /\ lit
- * where lit is encoded by: (formula,positive?)
- */
-typedef std::set<std::set<std::set<int> > > GMLConclusion;
-
-GMLConclusion gmlmip_onestep_gml(GMLPremise modvec);
-GMLConclusion gmlmip_onestep_pml(PMLPremise modvec);
-
-void printRuleCollection(const RuleCollection& rc);
-
-#endif
diff --git a/src/lib/GMLMIP-0.1/parser/lex.yy.c b/src/lib/GMLMIP-0.1/parser/lex.yy.c
deleted file mode 100644
index f5d55a4d8890f64e4dd13997f729326b382ae7d8..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/lex.yy.c
+++ /dev/null
@@ -1,2233 +0,0 @@
-
-#line 3 "lex.yy.c"
-
-#define YY_INT_ALIGNED short int
-
-/* A lexical scanner generated by flex */
-
-/* %not-for-header */
-
-/* %if-c-only */
-/* %if-not-reentrant */
-
-/* %endif */
-/* %endif */
-/* %ok-for-header */
-
-#define FLEX_SCANNER
-#define YY_FLEX_MAJOR_VERSION 2
-#define YY_FLEX_MINOR_VERSION 5
-#define YY_FLEX_SUBMINOR_VERSION 39
-#if YY_FLEX_SUBMINOR_VERSION > 0
-#define FLEX_BETA
-#endif
-
-/* %if-c++-only */
-/* %endif */
-
-/* %if-c-only */
-
-/* %endif */
-
-/* %if-c-only */
-
-/* %endif */
-
-/* First, we deal with platform-specific or compiler-specific issues. */
-
-/* begin standard C headers. */
-/* %if-c-only */
-#include <stdio.h>
-#include <string.h>
-#include <errno.h>
-#include <stdlib.h>
-/* %endif */
-
-/* %if-tables-serialization */
-/* %endif */
-/* end standard C headers. */
-
-/* %if-c-or-c++ */
-/* flex integer type definitions */
-
-#ifndef FLEXINT_H
-#define FLEXINT_H
-
-/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
-
-#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L
-
-/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h,
- * if you want the limit (max/min) macros for int types.
- */
-#ifndef __STDC_LIMIT_MACROS
-#define __STDC_LIMIT_MACROS 1
-#endif
-
-#include <inttypes.h>
-typedef int8_t flex_int8_t;
-typedef uint8_t flex_uint8_t;
-typedef int16_t flex_int16_t;
-typedef uint16_t flex_uint16_t;
-typedef int32_t flex_int32_t;
-typedef uint32_t flex_uint32_t;
-#else
-typedef signed char flex_int8_t;
-typedef short int flex_int16_t;
-typedef int flex_int32_t;
-typedef unsigned char flex_uint8_t;
-typedef unsigned short int flex_uint16_t;
-typedef unsigned int flex_uint32_t;
-
-/* Limits of integral types. */
-#ifndef INT8_MIN
-#define INT8_MIN (-128)
-#endif
-#ifndef INT16_MIN
-#define INT16_MIN (-32767-1)
-#endif
-#ifndef INT32_MIN
-#define INT32_MIN (-2147483647-1)
-#endif
-#ifndef INT8_MAX
-#define INT8_MAX (127)
-#endif
-#ifndef INT16_MAX
-#define INT16_MAX (32767)
-#endif
-#ifndef INT32_MAX
-#define INT32_MAX (2147483647)
-#endif
-#ifndef UINT8_MAX
-#define UINT8_MAX (255U)
-#endif
-#ifndef UINT16_MAX
-#define UINT16_MAX (65535U)
-#endif
-#ifndef UINT32_MAX
-#define UINT32_MAX (4294967295U)
-#endif
-
-#endif /* ! C99 */
-
-#endif /* ! FLEXINT_H */
-
-/* %endif */
-
-/* %if-c++-only */
-/* %endif */
-
-#ifdef __cplusplus
-
-/* The "const" storage-class-modifier is valid. */
-#define YY_USE_CONST
-
-#else /* ! __cplusplus */
-
-/* C99 requires __STDC__ to be defined as 1. */
-#if defined (__STDC__)
-
-#define YY_USE_CONST
-
-#endif /* defined (__STDC__) */
-#endif /* ! __cplusplus */
-
-#ifdef YY_USE_CONST
-#define yyconst const
-#else
-#define yyconst
-#endif
-
-/* %not-for-header */
-
-/* Returned upon end-of-file. */
-#define YY_NULL 0
-/* %ok-for-header */
-
-/* %not-for-header */
-
-/* Promotes a possibly negative, possibly signed char to an unsigned
- * integer for use as an array index. If the signed char is negative,
- * we want to instead treat it as an 8-bit unsigned char, hence the
- * double cast.
- */
-#define YY_SC_TO_UI(c) ((unsigned int) (unsigned char) c)
-/* %ok-for-header */
-
-/* %if-reentrant */
-/* %endif */
-
-/* %if-not-reentrant */
-
-/* %endif */
-
-/* Enter a start condition. This macro really ought to take a parameter,
- * but we do it the disgusting crufty way forced on us by the ()-less
- * definition of BEGIN.
- */
-#define BEGIN (yy_start) = 1 + 2 *
-
-/* Translate the current start state into a value that can be later handed
- * to BEGIN to return to the state. The YYSTATE alias is for lex
- * compatibility.
- */
-#define YY_START (((yy_start) - 1) / 2)
-#define YYSTATE YY_START
-
-/* Action number for EOF rule of a given start state. */
-#define YY_STATE_EOF(state) (YY_END_OF_BUFFER + state + 1)
-
-/* Special action meaning "start processing a new file". */
-#define YY_NEW_FILE yyrestart(yyin )
-
-#define YY_END_OF_BUFFER_CHAR 0
-
-/* Size of default input buffer. */
-#ifndef YY_BUF_SIZE
-#define YY_BUF_SIZE 16384
-#endif
-
-/* The state buf must be large enough to hold one state per character in the main buffer.
- */
-#define YY_STATE_BUF_SIZE ((YY_BUF_SIZE + 2) * sizeof(yy_state_type))
-
-#ifndef YY_TYPEDEF_YY_BUFFER_STATE
-#define YY_TYPEDEF_YY_BUFFER_STATE
-typedef struct yy_buffer_state *YY_BUFFER_STATE;
-#endif
-
-#ifndef YY_TYPEDEF_YY_SIZE_T
-#define YY_TYPEDEF_YY_SIZE_T
-typedef size_t yy_size_t;
-#endif
-
-/* %if-not-reentrant */
-extern yy_size_t yyleng;
-/* %endif */
-
-/* %if-c-only */
-/* %if-not-reentrant */
-extern FILE *yyin, *yyout;
-/* %endif */
-/* %endif */
-
-#define EOB_ACT_CONTINUE_SCAN 0
-#define EOB_ACT_END_OF_FILE 1
-#define EOB_ACT_LAST_MATCH 2
-
- #define YY_LESS_LINENO(n)
- #define YY_LINENO_REWIND_TO(ptr)
-
-/* Return all but the first "n" matched characters back to the input stream. */
-#define yyless(n) \
- do \
- { \
- /* Undo effects of setting up yytext. */ \
- int yyless_macro_arg = (n); \
- YY_LESS_LINENO(yyless_macro_arg);\
- *yy_cp = (yy_hold_char); \
- YY_RESTORE_YY_MORE_OFFSET \
- (yy_c_buf_p) = yy_cp = yy_bp + yyless_macro_arg - YY_MORE_ADJ; \
- YY_DO_BEFORE_ACTION; /* set up yytext again */ \
- } \
- while ( 0 )
-
-#define unput(c) yyunput( c, (yytext_ptr) )
-
-#ifndef YY_STRUCT_YY_BUFFER_STATE
-#define YY_STRUCT_YY_BUFFER_STATE
-struct yy_buffer_state
- {
-/* %if-c-only */
- FILE *yy_input_file;
-/* %endif */
-
-/* %if-c++-only */
-/* %endif */
-
- char *yy_ch_buf; /* input buffer */
- char *yy_buf_pos; /* current position in input buffer */
-
- /* Size of input buffer in bytes, not including room for EOB
- * characters.
- */
- yy_size_t yy_buf_size;
-
- /* Number of characters read into yy_ch_buf, not including EOB
- * characters.
- */
- yy_size_t yy_n_chars;
-
- /* Whether we "own" the buffer - i.e., we know we created it,
- * and can realloc() it to grow it, and should free() it to
- * delete it.
- */
- int yy_is_our_buffer;
-
- /* Whether this is an "interactive" input source; if so, and
- * if we're using stdio for input, then we want to use getc()
- * instead of fread(), to make sure we stop fetching input after
- * each newline.
- */
- int yy_is_interactive;
-
- /* Whether we're considered to be at the beginning of a line.
- * If so, '^' rules will be active on the next match, otherwise
- * not.
- */
- int yy_at_bol;
-
- int yy_bs_lineno; /**< The line count. */
- int yy_bs_column; /**< The column count. */
-
- /* Whether to try to fill the input buffer when we reach the
- * end of it.
- */
- int yy_fill_buffer;
-
- int yy_buffer_status;
-
-#define YY_BUFFER_NEW 0
-#define YY_BUFFER_NORMAL 1
- /* When an EOF's been seen but there's still some text to process
- * then we mark the buffer as YY_EOF_PENDING, to indicate that we
- * shouldn't try reading from the input source any more. We might
- * still have a bunch of tokens to match, though, because of
- * possible backing-up.
- *
- * When we actually see the EOF, we change the status to "new"
- * (via yyrestart()), so that the user can continue scanning by
- * just pointing yyin at a new input file.
- */
-#define YY_BUFFER_EOF_PENDING 2
-
- };
-#endif /* !YY_STRUCT_YY_BUFFER_STATE */
-
-/* %if-c-only Standard (non-C++) definition */
-/* %not-for-header */
-
-/* %if-not-reentrant */
-
-/* Stack of input buffers. */
-static size_t yy_buffer_stack_top = 0; /**< index of top of stack. */
-static size_t yy_buffer_stack_max = 0; /**< capacity of stack. */
-static YY_BUFFER_STATE * yy_buffer_stack = 0; /**< Stack as an array. */
-/* %endif */
-/* %ok-for-header */
-
-/* %endif */
-
-/* We provide macros for accessing buffer states in case in the
- * future we want to put the buffer states in a more general
- * "scanner state".
- *
- * Returns the top of the stack, or NULL.
- */
-#define YY_CURRENT_BUFFER ( (yy_buffer_stack) \
- ? (yy_buffer_stack)[(yy_buffer_stack_top)] \
- : NULL)
-
-/* Same as previous macro, but useful when we know that the buffer stack is not
- * NULL or when we need an lvalue. For internal use only.
- */
-#define YY_CURRENT_BUFFER_LVALUE (yy_buffer_stack)[(yy_buffer_stack_top)]
-
-/* %if-c-only Standard (non-C++) definition */
-
-/* %if-not-reentrant */
-/* %not-for-header */
-
-/* yy_hold_char holds the character lost when yytext is formed. */
-static char yy_hold_char;
-static yy_size_t yy_n_chars; /* number of characters read into yy_ch_buf */
-yy_size_t yyleng;
-
-/* Points to current character in buffer. */
-static char *yy_c_buf_p = (char *) 0;
-static int yy_init = 0; /* whether we need to initialize */
-static int yy_start = 0; /* start state number */
-
-/* Flag which is used to allow yywrap()'s to do buffer switches
- * instead of setting up a fresh yyin. A bit of a hack ...
- */
-static int yy_did_buffer_switch_on_eof;
-/* %ok-for-header */
-
-/* %endif */
-
-void yyrestart (FILE *input_file );
-void yy_switch_to_buffer (YY_BUFFER_STATE new_buffer );
-YY_BUFFER_STATE yy_create_buffer (FILE *file,int size );
-void yy_delete_buffer (YY_BUFFER_STATE b );
-void yy_flush_buffer (YY_BUFFER_STATE b );
-void yypush_buffer_state (YY_BUFFER_STATE new_buffer );
-void yypop_buffer_state (void );
-
-static void yyensure_buffer_stack (void );
-static void yy_load_buffer_state (void );
-static void yy_init_buffer (YY_BUFFER_STATE b,FILE *file );
-
-#define YY_FLUSH_BUFFER yy_flush_buffer(YY_CURRENT_BUFFER )
-
-YY_BUFFER_STATE yy_scan_buffer (char *base,yy_size_t size );
-YY_BUFFER_STATE yy_scan_string (yyconst char *yy_str );
-YY_BUFFER_STATE yy_scan_bytes (yyconst char *bytes,yy_size_t len );
-
-/* %endif */
-
-void *yyalloc (yy_size_t );
-void *yyrealloc (void *,yy_size_t );
-void yyfree (void * );
-
-#define yy_new_buffer yy_create_buffer
-
-#define yy_set_interactive(is_interactive) \
- { \
- if ( ! YY_CURRENT_BUFFER ){ \
- yyensure_buffer_stack (); \
- YY_CURRENT_BUFFER_LVALUE = \
- yy_create_buffer(yyin,YY_BUF_SIZE ); \
- } \
- YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \
- }
-
-#define yy_set_bol(at_bol) \
- { \
- if ( ! YY_CURRENT_BUFFER ){\
- yyensure_buffer_stack (); \
- YY_CURRENT_BUFFER_LVALUE = \
- yy_create_buffer(yyin,YY_BUF_SIZE ); \
- } \
- YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \
- }
-
-#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol)
-
-/* %% [1.0] yytext/yyin/yyout/yy_state_type/yylineno etc. def's & init go here */
-/* Begin user sect3 */
-
-#define yywrap() 1
-#define YY_SKIP_YYWRAP
-
-#define FLEX_DEBUG
-
-typedef unsigned char YY_CHAR;
-
-FILE *yyin = (FILE *) 0, *yyout = (FILE *) 0;
-
-typedef int yy_state_type;
-
-extern int yylineno;
-
-int yylineno = 1;
-
-extern char *yytext;
-#define yytext_ptr yytext
-
-/* %% [1.5] DFA */
-
-/* %if-c-only Standard (non-C++) definition */
-
-static yy_state_type yy_get_previous_state (void );
-static yy_state_type yy_try_NUL_trans (yy_state_type current_state );
-static int yy_get_next_buffer (void );
-static void yy_fatal_error (yyconst char msg[] );
-
-/* %endif */
-
-/* Done after the current pattern has been matched and before the
- * corresponding action - sets up yytext.
- */
-#define YY_DO_BEFORE_ACTION \
- (yytext_ptr) = yy_bp; \
-/* %% [2.0] code to fiddle yytext and yyleng for yymore() goes here \ */\
- (yytext_ptr) -= (yy_more_len); \
- yyleng = (size_t) (yy_cp - (yytext_ptr)); \
- (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;
-
-/* %% [4.0] data tables for the DFA and the user's section 1 definitions go here */
-#define YY_NUM_RULES 21
-#define YY_END_OF_BUFFER 22
-/* This struct is not used in this scanner,
- but its presence is necessary. */
-struct yy_trans_info
- {
- flex_int32_t yy_verify;
- flex_int32_t yy_nxt;
- };
-static yyconst flex_int16_t yy_accept[60] =
- { 0,
- 0, 0, 22, 20, 1, 1, 6, 16, 17, 20,
- 20, 20, 20, 20, 20, 20, 13, 14, 1, 7,
- 0, 0, 0, 0, 0, 15, 0, 8, 0, 9,
- 0, 0, 10, 0, 0, 0, 0, 0, 0, 18,
- 11, 0, 12, 19, 0, 0, 0, 0, 0, 0,
- 0, 0, 0, 0, 2, 3, 4, 5, 0
- } ;
-
-static yyconst flex_int32_t yy_ec[256] =
- { 0,
- 1, 1, 1, 1, 1, 1, 1, 1, 2, 3,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 4, 1, 1, 1, 1, 1, 5, 1, 6,
- 7, 1, 1, 1, 8, 1, 9, 10, 10, 10,
- 10, 10, 10, 10, 10, 10, 10, 11, 1, 12,
- 1, 13, 1, 1, 1, 1, 1, 1, 1, 1,
- 14, 1, 1, 1, 1, 15, 16, 1, 1, 17,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 18, 1, 19, 1, 1, 1, 20, 1, 21, 1,
-
- 22, 23, 24, 1, 25, 1, 1, 26, 1, 1,
- 27, 28, 1, 29, 30, 31, 32, 33, 1, 1,
- 1, 1, 1, 1, 1, 34, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
-
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1
- } ;
-
-static yyconst flex_int32_t yy_meta[35] =
- { 0,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1
- } ;
-
-static yyconst flex_int16_t yy_base[60] =
- { 0,
- 0, 0, 88, 89, 33, 36, 89, 89, 89, 74,
- 33, 59, 75, 64, 73, 53, 89, 89, 42, 89,
- 68, 38, 56, 40, 53, 68, 45, 89, 66, 89,
- 50, 64, 89, 43, 50, 42, 50, 43, 48, 89,
- 89, 58, 89, 89, 50, 43, 52, 50, 49, 47,
- 46, 43, 41, 27, 89, 89, 89, 89, 89
- } ;
-
-static yyconst flex_int16_t yy_def[60] =
- { 0,
- 59, 1, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 0
- } ;
-
-static yyconst flex_int16_t yy_nxt[124] =
- { 0,
- 4, 5, 6, 5, 7, 8, 9, 10, 4, 4,
- 4, 11, 4, 4, 12, 4, 4, 13, 4, 4,
- 4, 4, 14, 4, 4, 4, 4, 15, 4, 4,
- 16, 4, 17, 18, 19, 19, 19, 19, 19, 19,
- 21, 58, 22, 19, 19, 19, 29, 22, 32, 24,
- 30, 36, 38, 46, 41, 57, 49, 56, 33, 50,
- 55, 43, 54, 47, 53, 52, 48, 51, 45, 44,
- 42, 40, 39, 38, 37, 36, 35, 26, 34, 31,
- 28, 27, 26, 25, 24, 23, 20, 59, 3, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
-
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59
- } ;
-
-static yyconst flex_int16_t yy_chk[124] =
- { 0,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
- 1, 1, 1, 1, 5, 5, 5, 6, 6, 6,
- 11, 54, 11, 19, 19, 19, 22, 22, 24, 24,
- 22, 36, 38, 45, 36, 53, 46, 52, 24, 46,
- 51, 38, 50, 45, 49, 48, 45, 47, 42, 39,
- 37, 35, 34, 32, 31, 29, 27, 26, 25, 23,
- 21, 16, 15, 14, 13, 12, 10, 3, 59, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
-
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59, 59, 59, 59, 59, 59, 59, 59,
- 59, 59, 59
- } ;
-
-static yy_state_type yy_last_accepting_state;
-static char *yy_last_accepting_cpos;
-
-extern int yy_flex_debug;
-int yy_flex_debug = 1;
-
-static yyconst flex_int16_t yy_rule_linenum[21] =
- { 0,
- 49, 50, 51, 52, 53, 54, 55, 56, 57, 64,
- 71, 86, 100, 101, 102, 103, 104, 105, 106, 107
- } ;
-
-/* The intent behind this definition is that it'll catch
- * any uses of REJECT which flex missed.
- */
-#define REJECT reject_used_but_not_detected
-static int yy_more_flag = 0;
-static int yy_more_len = 0;
-#define yymore() ((yy_more_flag) = 1)
-#define YY_MORE_ADJ (yy_more_len)
-#define YY_RESTORE_YY_MORE_OFFSET
-char *yytext;
-#line 1 "mlf-scanner.ll"
-#line 2 "mlf-scanner.ll"
-# 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
-#line 40 "mlf-scanner.ll"
-# define YY_USER_ACTION yylloc->columns (yyleng);
-#line 44 "mlf-scanner.ll"
- typedef yy::mlf_parser::token token;
-#line 628 "lex.yy.c"
-
-#define INITIAL 0
-
-#ifndef YY_NO_UNISTD_H
-/* Special case for "unistd.h", since it is non-ANSI. We include it way
- * down here because we want the user's section 1 to have been scanned first.
- * The user has a chance to override it with an option.
- */
-/* %if-c-only */
-#include <unistd.h>
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-#endif
-
-#ifndef YY_EXTRA_TYPE
-#define YY_EXTRA_TYPE void *
-#endif
-
-/* %if-c-only Reentrant structure and macros (non-C++). */
-/* %if-reentrant */
-/* %if-c-only */
-
-static int yy_init_globals (void );
-
-/* %endif */
-/* %if-reentrant */
-/* %endif */
-/* %endif End reentrant structures and macros. */
-
-/* Accessor methods to globals.
- These are made visible to non-reentrant scanners for convenience. */
-
-int yylex_destroy (void );
-
-int yyget_debug (void );
-
-void yyset_debug (int debug_flag );
-
-YY_EXTRA_TYPE yyget_extra (void );
-
-void yyset_extra (YY_EXTRA_TYPE user_defined );
-
-FILE *yyget_in (void );
-
-void yyset_in (FILE * in_str );
-
-FILE *yyget_out (void );
-
-void yyset_out (FILE * out_str );
-
-yy_size_t yyget_leng (void );
-
-char *yyget_text (void );
-
-int yyget_lineno (void );
-
-void yyset_lineno (int line_number );
-
-/* %if-bison-bridge */
-/* %endif */
-
-/* Macros after this point can all be overridden by user definitions in
- * section 1.
- */
-
-#ifndef YY_SKIP_YYWRAP
-#ifdef __cplusplus
-extern "C" int yywrap (void );
-#else
-extern int yywrap (void );
-#endif
-#endif
-
-/* %not-for-header */
-
-/* %ok-for-header */
-
-/* %endif */
-
-#ifndef yytext_ptr
-static void yy_flex_strncpy (char *,yyconst char *,int );
-#endif
-
-#ifdef YY_NEED_STRLEN
-static int yy_flex_strlen (yyconst char * );
-#endif
-
-#ifndef YY_NO_INPUT
-/* %if-c-only Standard (non-C++) definition */
-/* %not-for-header */
-
-#ifdef __cplusplus
-static int yyinput (void );
-#else
-static int input (void );
-#endif
-/* %ok-for-header */
-
-/* %endif */
-#endif
-
-/* %if-c-only */
-
-/* %endif */
-
-/* Amount of stuff to slurp up with each read. */
-#ifndef YY_READ_BUF_SIZE
-#define YY_READ_BUF_SIZE 8192
-#endif
-
-/* Copy whatever the last rule matched to the standard output. */
-#ifndef ECHO
-/* %if-c-only Standard (non-C++) definition */
-/* This used to be an fputs(), but since the string might contain NUL's,
- * we now use fwrite().
- */
-#define ECHO do { if (fwrite( yytext, yyleng, 1, yyout )) {} } while (0)
-/* %endif */
-/* %if-c++-only C++ definition */
-/* %endif */
-#endif
-
-/* Gets input and stuffs it into "buf". number of characters read, or YY_NULL,
- * is returned in "result".
- */
-#ifndef YY_INPUT
-#define YY_INPUT(buf,result,max_size) \
-/* %% [5.0] fread()/read() definition of YY_INPUT goes here unless we're doing C++ \ */\
- if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \
- { \
- int c = '*'; \
- size_t n; \
- for ( n = 0; n < max_size && \
- (c = getc( yyin )) != EOF && c != '\n'; ++n ) \
- buf[n] = (char) c; \
- if ( c == '\n' ) \
- buf[n++] = (char) c; \
- if ( c == EOF && ferror( yyin ) ) \
- YY_FATAL_ERROR( "input in flex scanner failed" ); \
- result = n; \
- } \
- else \
- { \
- errno=0; \
- while ( (result = fread(buf, 1, max_size, yyin))==0 && ferror(yyin)) \
- { \
- if( errno != EINTR) \
- { \
- YY_FATAL_ERROR( "input in flex scanner failed" ); \
- break; \
- } \
- errno=0; \
- clearerr(yyin); \
- } \
- }\
-\
-/* %if-c++-only C++ definition \ */\
-/* %endif */
-
-#endif
-
-/* No semi-colon after return; correct usage is to write "yyterminate();" -
- * we don't want an extra ';' after the "return" because that will cause
- * some compilers to complain about unreachable statements.
- */
-#ifndef yyterminate
-#define yyterminate() return YY_NULL
-#endif
-
-/* Number of entries by which start-condition stack grows. */
-#ifndef YY_START_STACK_INCR
-#define YY_START_STACK_INCR 25
-#endif
-
-/* Report a fatal error. */
-#ifndef YY_FATAL_ERROR
-/* %if-c-only */
-#define YY_FATAL_ERROR(msg) yy_fatal_error( msg )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-#endif
-
-/* %if-tables-serialization structures and prototypes */
-/* %not-for-header */
-
-/* %ok-for-header */
-
-/* %not-for-header */
-
-/* %tables-yydmap generated elements */
-/* %endif */
-/* end tables serialization structures and prototypes */
-
-/* %ok-for-header */
-
-/* Default declaration of generated scanner - a define so the user can
- * easily add parameters.
- */
-#ifndef YY_DECL
-#define YY_DECL_IS_OURS 1
-/* %if-c-only Standard (non-C++) definition */
-
-extern int yylex (void);
-
-#define YY_DECL int yylex (void)
-/* %endif */
-/* %if-c++-only C++ definition */
-/* %endif */
-#endif /* !YY_DECL */
-
-/* Code executed at the beginning of each rule, after yytext and yyleng
- * have been set up.
- */
-#ifndef YY_USER_ACTION
-#define YY_USER_ACTION
-#endif
-
-/* Code executed at the end of each rule. */
-#ifndef YY_BREAK
-#define YY_BREAK break;
-#endif
-
-/* %% [6.0] YY_RULE_SETUP definition goes here */
-#define YY_RULE_SETUP \
- YY_USER_ACTION
-
-/* %not-for-header */
-
-/** The main scanner function which does all the work.
- */
-YY_DECL
-{
- register yy_state_type yy_current_state;
- register char *yy_cp, *yy_bp;
- register int yy_act;
-
- if ( !(yy_init) )
- {
- (yy_init) = 1;
-
-#ifdef YY_USER_INIT
- YY_USER_INIT;
-#endif
-
- if ( ! (yy_start) )
- (yy_start) = 1; /* first start state */
-
- if ( ! yyin )
-/* %if-c-only */
- yyin = stdin;
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-
- if ( ! yyout )
-/* %if-c-only */
- yyout = stdout;
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-
- if ( ! YY_CURRENT_BUFFER ) {
- yyensure_buffer_stack ();
- YY_CURRENT_BUFFER_LVALUE =
- yy_create_buffer(yyin,YY_BUF_SIZE );
- }
-
- yy_load_buffer_state( );
- }
-
- {
-/* %% [7.0] user's declarations go here */
-#line 48 "mlf-scanner.ll"
-
-#line 905 "lex.yy.c"
-
- while ( 1 ) /* loops until end-of-file is reached */
- {
-/* %% [8.0] yymore()-related code goes here */
- (yy_more_len) = 0;
- if ( (yy_more_flag) )
- {
- (yy_more_len) = (yy_c_buf_p) - (yytext_ptr);
- (yy_more_flag) = 0;
- }
- yy_cp = (yy_c_buf_p);
-
- /* Support of yytext. */
- *yy_cp = (yy_hold_char);
-
- /* yy_bp points to the position in yy_ch_buf of the start of
- * the current run.
- */
- yy_bp = yy_cp;
-
-/* %% [9.0] code to set up and find next match goes here */
- yy_current_state = (yy_start);
-yy_match:
- do
- {
- register YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)] ;
- if ( yy_accept[yy_current_state] )
- {
- (yy_last_accepting_state) = yy_current_state;
- (yy_last_accepting_cpos) = yy_cp;
- }
- while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
- {
- yy_current_state = (int) yy_def[yy_current_state];
- if ( yy_current_state >= 60 )
- yy_c = yy_meta[(unsigned int) yy_c];
- }
- yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
- ++yy_cp;
- }
- while ( yy_current_state != 59 );
- yy_cp = (yy_last_accepting_cpos);
- yy_current_state = (yy_last_accepting_state);
-
-yy_find_action:
-/* %% [10.0] code to find the action number goes here */
- yy_act = yy_accept[yy_current_state];
-
- YY_DO_BEFORE_ACTION;
-
-/* %% [11.0] code for yylineno update goes here */
-
-do_action: /* This label is used only to access EOF actions. */
-
-/* %% [12.0] debug code goes here */
- if ( yy_flex_debug )
- {
- if ( yy_act == 0 )
- fprintf( stderr, "--scanner backing up\n" );
- else if ( yy_act < 21 )
- fprintf( stderr, "--accepting rule at line %ld (\"%s\")\n",
- (long)yy_rule_linenum[yy_act], yytext );
- else if ( yy_act == 21 )
- fprintf( stderr, "--accepting default rule (\"%s\")\n",
- yytext );
- else if ( yy_act == 22 )
- fprintf( stderr, "--(end of buffer or a NUL)\n" );
- else
- fprintf( stderr, "--EOF (start condition %d)\n", YY_START );
- }
-
- switch ( yy_act )
- { /* beginning of action switch */
-/* %% [13.0] actions go here */
- case 0: /* must back up */
- /* undo the effects of YY_DO_BEFORE_ACTION */
- *yy_cp = (yy_hold_char);
- yy_cp = (yy_last_accepting_cpos);
- yy_current_state = (yy_last_accepting_state);
- goto yy_find_action;
-
-case 1:
-/* rule 1 can match eol */
-YY_RULE_SETUP
-#line 49 "mlf-scanner.ll"
-/*eat white space*/
- YY_BREAK
-case 2:
-YY_RULE_SETUP
-#line 50 "mlf-scanner.ll"
-{ return token::GML; }
- YY_BREAK
-case 3:
-YY_RULE_SETUP
-#line 51 "mlf-scanner.ll"
-{ return token::PML; }
- YY_BREAK
-case 4:
-YY_RULE_SETUP
-#line 52 "mlf-scanner.ll"
-{ return token::GML; }
- YY_BREAK
-case 5:
-YY_RULE_SETUP
-#line 53 "mlf-scanner.ll"
-{ return token::PML; }
- YY_BREAK
-case 6:
-YY_RULE_SETUP
-#line 54 "mlf-scanner.ll"
-{ return token::AND; }
- YY_BREAK
-case 7:
-YY_RULE_SETUP
-#line 55 "mlf-scanner.ll"
-{ return token::IMP; }
- YY_BREAK
-case 8:
-YY_RULE_SETUP
-#line 56 "mlf-scanner.ll"
-{ return token::IFF; }
- YY_BREAK
-case 9:
-YY_RULE_SETUP
-#line 57 "mlf-scanner.ll"
-{ if(driver.get_logic()!='g')
- driver.error(*yylloc, "Invalid operator type for specified logic!");
- else {
- yylval->number = atoi(yytext + 1);
- return token::GMDIA;
- }
- }
- YY_BREAK
-case 10:
-YY_RULE_SETUP
-#line 64 "mlf-scanner.ll"
-{ if(driver.get_logic()!='g')
- driver.error(*yylloc, "Invalid operator type for specified logic!");
- else {
- yylval->number = atoi(yytext + 1);
- return token::GMBOX;
- }
- }
- YY_BREAK
-case 11:
-YY_RULE_SETUP
-#line 71 "mlf-scanner.ll"
-{ 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;
- }
- }
- YY_BREAK
-case 12:
-YY_RULE_SETUP
-#line 86 "mlf-scanner.ll"
-{ 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;
- }
- }
- YY_BREAK
-case 13:
-YY_RULE_SETUP
-#line 100 "mlf-scanner.ll"
-{ return token::OR; }
- YY_BREAK
-case 14:
-YY_RULE_SETUP
-#line 101 "mlf-scanner.ll"
-{ return token::NOT; }
- YY_BREAK
-case 15:
-YY_RULE_SETUP
-#line 102 "mlf-scanner.ll"
-{ yylval->binarydd = driver.variable(atoi(yytext + 1)); return token::PVAR; }
- YY_BREAK
-case 16:
-YY_RULE_SETUP
-#line 103 "mlf-scanner.ll"
-{ return token::LPAREN; }
- YY_BREAK
-case 17:
-YY_RULE_SETUP
-#line 104 "mlf-scanner.ll"
-{ return token::RPAREN; }
- YY_BREAK
-case 18:
-YY_RULE_SETUP
-#line 105 "mlf-scanner.ll"
-{ return token::TRUE; }
- YY_BREAK
-case 19:
-YY_RULE_SETUP
-#line 106 "mlf-scanner.ll"
-{ return token::FALSE; }
- YY_BREAK
-case 20:
-YY_RULE_SETUP
-#line 107 "mlf-scanner.ll"
-driver.error (*yylloc, "invalid character!");
- YY_BREAK
-case 21:
-YY_RULE_SETUP
-#line 108 "mlf-scanner.ll"
-ECHO;
- YY_BREAK
-#line 1132 "lex.yy.c"
-case YY_STATE_EOF(INITIAL):
- yyterminate();
-
- case YY_END_OF_BUFFER:
- {
- /* Amount of text matched not including the EOB char. */
- int yy_amount_of_matched_text = (int) (yy_cp - (yytext_ptr)) - 1;
-
- /* Undo the effects of YY_DO_BEFORE_ACTION. */
- *yy_cp = (yy_hold_char);
- YY_RESTORE_YY_MORE_OFFSET
-
- if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW )
- {
- /* We're scanning a new file or input source. It's
- * possible that this happened because the user
- * just pointed yyin at a new source and called
- * yylex(). If so, then we have to assure
- * consistency between YY_CURRENT_BUFFER and our
- * globals. Here is the right place to do so, because
- * this is the first action (other than possibly a
- * back-up) that will match for the new input source.
- */
- (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
- YY_CURRENT_BUFFER_LVALUE->yy_input_file = yyin;
- YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL;
- }
-
- /* Note that here we test for yy_c_buf_p "<=" to the position
- * of the first EOB in the buffer, since yy_c_buf_p will
- * already have been incremented past the NUL character
- * (since all states make transitions on EOB to the
- * end-of-buffer state). Contrast this with the test
- * in input().
- */
- if ( (yy_c_buf_p) <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
- { /* This was really a NUL. */
- yy_state_type yy_next_state;
-
- (yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text;
-
- yy_current_state = yy_get_previous_state( );
-
- /* Okay, we're now positioned to make the NUL
- * transition. We couldn't have
- * yy_get_previous_state() go ahead and do it
- * for us because it doesn't know how to deal
- * with the possibility of jamming (and we don't
- * want to build jamming into it because then it
- * will run more slowly).
- */
-
- yy_next_state = yy_try_NUL_trans( yy_current_state );
-
- yy_bp = (yytext_ptr) + YY_MORE_ADJ;
-
- if ( yy_next_state )
- {
- /* Consume the NUL. */
- yy_cp = ++(yy_c_buf_p);
- yy_current_state = yy_next_state;
- goto yy_match;
- }
-
- else
- {
-/* %% [14.0] code to do back-up for compressed tables and set up yy_cp goes here */
- yy_cp = (yy_last_accepting_cpos);
- yy_current_state = (yy_last_accepting_state);
- goto yy_find_action;
- }
- }
-
- else switch ( yy_get_next_buffer( ) )
- {
- case EOB_ACT_END_OF_FILE:
- {
- (yy_did_buffer_switch_on_eof) = 0;
-
- if ( yywrap( ) )
- {
- /* Note: because we've taken care in
- * yy_get_next_buffer() to have set up
- * yytext, we can now set up
- * yy_c_buf_p so that if some total
- * hoser (like flex itself) wants to
- * call the scanner after we return the
- * YY_NULL, it'll still work - another
- * YY_NULL will get returned.
- */
- (yy_c_buf_p) = (yytext_ptr) + YY_MORE_ADJ;
-
- yy_act = YY_STATE_EOF(YY_START);
- goto do_action;
- }
-
- else
- {
- if ( ! (yy_did_buffer_switch_on_eof) )
- YY_NEW_FILE;
- }
- break;
- }
-
- case EOB_ACT_CONTINUE_SCAN:
- (yy_c_buf_p) =
- (yytext_ptr) + yy_amount_of_matched_text;
-
- yy_current_state = yy_get_previous_state( );
-
- yy_cp = (yy_c_buf_p);
- yy_bp = (yytext_ptr) + YY_MORE_ADJ;
- goto yy_match;
-
- case EOB_ACT_LAST_MATCH:
- (yy_c_buf_p) =
- &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)];
-
- yy_current_state = yy_get_previous_state( );
-
- yy_cp = (yy_c_buf_p);
- yy_bp = (yytext_ptr) + YY_MORE_ADJ;
- goto yy_find_action;
- }
- break;
- }
-
- default:
- YY_FATAL_ERROR(
- "fatal flex scanner internal error--no action found" );
- } /* end of action switch */
- } /* end of scanning one token */
- } /* end of user's declarations */
-} /* end of yylex */
-/* %ok-for-header */
-
-/* %if-c++-only */
-/* %not-for-header */
-
-/* %ok-for-header */
-
-/* %endif */
-
-/* yy_get_next_buffer - try to read in a new buffer
- *
- * Returns a code representing an action:
- * EOB_ACT_LAST_MATCH -
- * EOB_ACT_CONTINUE_SCAN - continue scanning from current position
- * EOB_ACT_END_OF_FILE - end of file
- */
-/* %if-c-only */
-static int yy_get_next_buffer (void)
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- register char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf;
- register char *source = (yytext_ptr);
- register int number_to_move, i;
- int ret_val;
-
- if ( (yy_c_buf_p) > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] )
- YY_FATAL_ERROR(
- "fatal flex scanner internal error--end of buffer missed" );
-
- if ( YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == 0 )
- { /* Don't try to fill the buffer, so this is an EOF. */
- if ( (yy_c_buf_p) - (yytext_ptr) - YY_MORE_ADJ == 1 )
- {
- /* We matched a single character, the EOB, so
- * treat this as a final EOF.
- */
- return EOB_ACT_END_OF_FILE;
- }
-
- else
- {
- /* We matched some text prior to the EOB, first
- * process it.
- */
- return EOB_ACT_LAST_MATCH;
- }
- }
-
- /* Try to read more data. */
-
- /* First move last chars to start of buffer. */
- number_to_move = (int) ((yy_c_buf_p) - (yytext_ptr)) - 1;
-
- for ( i = 0; i < number_to_move; ++i )
- *(dest++) = *(source++);
-
- if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_EOF_PENDING )
- /* don't do the read, it's not guaranteed to return an EOF,
- * just force an EOF
- */
- YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars) = 0;
-
- else
- {
- yy_size_t num_to_read =
- YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1;
-
- while ( num_to_read <= 0 )
- { /* Not enough room in the buffer - grow it. */
-
- /* just a shorter name for the current buffer */
- YY_BUFFER_STATE b = YY_CURRENT_BUFFER_LVALUE;
-
- int yy_c_buf_p_offset =
- (int) ((yy_c_buf_p) - b->yy_ch_buf);
-
- if ( b->yy_is_our_buffer )
- {
- yy_size_t new_size = b->yy_buf_size * 2;
-
- if ( new_size <= 0 )
- b->yy_buf_size += b->yy_buf_size / 8;
- else
- b->yy_buf_size *= 2;
-
- b->yy_ch_buf = (char *)
- /* Include room in for 2 EOB chars. */
- yyrealloc((void *) b->yy_ch_buf,b->yy_buf_size + 2 );
- }
- else
- /* Can't grow it, we don't own it. */
- b->yy_ch_buf = 0;
-
- if ( ! b->yy_ch_buf )
- YY_FATAL_ERROR(
- "fatal error - scanner input buffer overflow" );
-
- (yy_c_buf_p) = &b->yy_ch_buf[yy_c_buf_p_offset];
-
- num_to_read = YY_CURRENT_BUFFER_LVALUE->yy_buf_size -
- number_to_move - 1;
-
- }
-
- if ( num_to_read > YY_READ_BUF_SIZE )
- num_to_read = YY_READ_BUF_SIZE;
-
- /* Read in more data. */
- YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]),
- (yy_n_chars), num_to_read );
-
- YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
- }
-
- if ( (yy_n_chars) == 0 )
- {
- if ( number_to_move == YY_MORE_ADJ )
- {
- ret_val = EOB_ACT_END_OF_FILE;
- yyrestart(yyin );
- }
-
- else
- {
- ret_val = EOB_ACT_LAST_MATCH;
- YY_CURRENT_BUFFER_LVALUE->yy_buffer_status =
- YY_BUFFER_EOF_PENDING;
- }
- }
-
- else
- ret_val = EOB_ACT_CONTINUE_SCAN;
-
- if ((yy_size_t) ((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) {
- /* Extend the array by 50%, plus the number we really need. */
- yy_size_t new_size = (yy_n_chars) + number_to_move + ((yy_n_chars) >> 1);
- YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) yyrealloc((void *) YY_CURRENT_BUFFER_LVALUE->yy_ch_buf,new_size );
- if ( ! YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
- YY_FATAL_ERROR( "out of dynamic memory in yy_get_next_buffer()" );
- }
-
- (yy_n_chars) += number_to_move;
- YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] = YY_END_OF_BUFFER_CHAR;
- YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] = YY_END_OF_BUFFER_CHAR;
-
- (yytext_ptr) = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0];
-
- return ret_val;
-}
-
-/* yy_get_previous_state - get the state just before the EOB char was reached */
-
-/* %if-c-only */
-/* %not-for-header */
-
- static yy_state_type yy_get_previous_state (void)
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- register yy_state_type yy_current_state;
- register char *yy_cp;
-
-/* %% [15.0] code to get the start state into yy_current_state goes here */
- yy_current_state = (yy_start);
-
- for ( yy_cp = (yytext_ptr) + YY_MORE_ADJ; yy_cp < (yy_c_buf_p); ++yy_cp )
- {
-/* %% [16.0] code to find the next state goes here */
- register YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1);
- if ( yy_accept[yy_current_state] )
- {
- (yy_last_accepting_state) = yy_current_state;
- (yy_last_accepting_cpos) = yy_cp;
- }
- while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
- {
- yy_current_state = (int) yy_def[yy_current_state];
- if ( yy_current_state >= 60 )
- yy_c = yy_meta[(unsigned int) yy_c];
- }
- yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
- }
-
- return yy_current_state;
-}
-
-/* yy_try_NUL_trans - try to make a transition on the NUL character
- *
- * synopsis
- * next_state = yy_try_NUL_trans( current_state );
- */
-/* %if-c-only */
- static yy_state_type yy_try_NUL_trans (yy_state_type yy_current_state )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- register int yy_is_jam;
- /* %% [17.0] code to find the next state, and perhaps do backing up, goes here */
- register char *yy_cp = (yy_c_buf_p);
-
- register YY_CHAR yy_c = 1;
- if ( yy_accept[yy_current_state] )
- {
- (yy_last_accepting_state) = yy_current_state;
- (yy_last_accepting_cpos) = yy_cp;
- }
- while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
- {
- yy_current_state = (int) yy_def[yy_current_state];
- if ( yy_current_state >= 60 )
- yy_c = yy_meta[(unsigned int) yy_c];
- }
- yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
- yy_is_jam = (yy_current_state == 59);
-
- return yy_is_jam ? 0 : yy_current_state;
-}
-
-/* %if-c-only */
-
-/* %endif */
-
-/* %if-c-only */
-#ifndef YY_NO_INPUT
-#ifdef __cplusplus
- static int yyinput (void)
-#else
- static int input (void)
-#endif
-
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- int c;
-
- *(yy_c_buf_p) = (yy_hold_char);
-
- if ( *(yy_c_buf_p) == YY_END_OF_BUFFER_CHAR )
- {
- /* yy_c_buf_p now points to the character we want to return.
- * If this occurs *before* the EOB characters, then it's a
- * valid NUL; if not, then we've hit the end of the buffer.
- */
- if ( (yy_c_buf_p) < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
- /* This was really a NUL. */
- *(yy_c_buf_p) = '\0';
-
- else
- { /* need more input */
- yy_size_t offset = (yy_c_buf_p) - (yytext_ptr);
- ++(yy_c_buf_p);
-
- switch ( yy_get_next_buffer( ) )
- {
- case EOB_ACT_LAST_MATCH:
- /* This happens because yy_g_n_b()
- * sees that we've accumulated a
- * token and flags that we need to
- * try matching the token before
- * proceeding. But for input(),
- * there's no matching to consider.
- * So convert the EOB_ACT_LAST_MATCH
- * to EOB_ACT_END_OF_FILE.
- */
-
- /* Reset buffer status. */
- yyrestart(yyin );
-
- /*FALLTHROUGH*/
-
- case EOB_ACT_END_OF_FILE:
- {
- if ( yywrap( ) )
- return EOF;
-
- if ( ! (yy_did_buffer_switch_on_eof) )
- YY_NEW_FILE;
-#ifdef __cplusplus
- return yyinput();
-#else
- return input();
-#endif
- }
-
- case EOB_ACT_CONTINUE_SCAN:
- (yy_c_buf_p) = (yytext_ptr) + offset;
- break;
- }
- }
- }
-
- c = *(unsigned char *) (yy_c_buf_p); /* cast for 8-bit char's */
- *(yy_c_buf_p) = '\0'; /* preserve yytext */
- (yy_hold_char) = *++(yy_c_buf_p);
-
-/* %% [19.0] update BOL and yylineno */
-
- return c;
-}
-/* %if-c-only */
-#endif /* ifndef YY_NO_INPUT */
-/* %endif */
-
-/** Immediately switch to a different input stream.
- * @param input_file A readable stream.
- *
- * @note This function does not reset the start condition to @c INITIAL .
- */
-/* %if-c-only */
- void yyrestart (FILE * input_file )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
-
- if ( ! YY_CURRENT_BUFFER ){
- yyensure_buffer_stack ();
- YY_CURRENT_BUFFER_LVALUE =
- yy_create_buffer(yyin,YY_BUF_SIZE );
- }
-
- yy_init_buffer(YY_CURRENT_BUFFER,input_file );
- yy_load_buffer_state( );
-}
-
-/** Switch to a different input buffer.
- * @param new_buffer The new input buffer.
- *
- */
-/* %if-c-only */
- void yy_switch_to_buffer (YY_BUFFER_STATE new_buffer )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
-
- /* TODO. We should be able to replace this entire function body
- * with
- * yypop_buffer_state();
- * yypush_buffer_state(new_buffer);
- */
- yyensure_buffer_stack ();
- if ( YY_CURRENT_BUFFER == new_buffer )
- return;
-
- if ( YY_CURRENT_BUFFER )
- {
- /* Flush out information for old buffer. */
- *(yy_c_buf_p) = (yy_hold_char);
- YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
- YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
- }
-
- YY_CURRENT_BUFFER_LVALUE = new_buffer;
- yy_load_buffer_state( );
-
- /* We don't actually know whether we did this switch during
- * EOF (yywrap()) processing, but the only time this flag
- * is looked at is after yywrap() is called, so it's safe
- * to go ahead and always set it.
- */
- (yy_did_buffer_switch_on_eof) = 1;
-}
-
-/* %if-c-only */
-static void yy_load_buffer_state (void)
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
- (yytext_ptr) = (yy_c_buf_p) = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos;
- yyin = YY_CURRENT_BUFFER_LVALUE->yy_input_file;
- (yy_hold_char) = *(yy_c_buf_p);
-}
-
-/** Allocate and initialize an input buffer state.
- * @param file A readable stream.
- * @param size The character buffer size in bytes. When in doubt, use @c YY_BUF_SIZE.
- *
- * @return the allocated buffer state.
- */
-/* %if-c-only */
- YY_BUFFER_STATE yy_create_buffer (FILE * file, int size )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- YY_BUFFER_STATE b;
-
- b = (YY_BUFFER_STATE) yyalloc(sizeof( struct yy_buffer_state ) );
- if ( ! b )
- YY_FATAL_ERROR( "out of dynamic memory in yy_create_buffer()" );
-
- b->yy_buf_size = size;
-
- /* yy_ch_buf has to be 2 characters longer than the size given because
- * we need to put in 2 end-of-buffer characters.
- */
- b->yy_ch_buf = (char *) yyalloc(b->yy_buf_size + 2 );
- if ( ! b->yy_ch_buf )
- YY_FATAL_ERROR( "out of dynamic memory in yy_create_buffer()" );
-
- b->yy_is_our_buffer = 1;
-
- yy_init_buffer(b,file );
-
- return b;
-}
-
-/** Destroy the buffer.
- * @param b a buffer created with yy_create_buffer()
- *
- */
-/* %if-c-only */
- void yy_delete_buffer (YY_BUFFER_STATE b )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
-
- if ( ! b )
- return;
-
- if ( b == YY_CURRENT_BUFFER ) /* Not sure if we should pop here. */
- YY_CURRENT_BUFFER_LVALUE = (YY_BUFFER_STATE) 0;
-
- if ( b->yy_is_our_buffer )
- yyfree((void *) b->yy_ch_buf );
-
- yyfree((void *) b );
-}
-
-/* Initializes or reinitializes a buffer.
- * This function is sometimes called more than once on the same buffer,
- * such as during a yyrestart() or at EOF.
- */
-/* %if-c-only */
- static void yy_init_buffer (YY_BUFFER_STATE b, FILE * file )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-
-{
- int oerrno = errno;
-
- yy_flush_buffer(b );
-
- b->yy_input_file = file;
- b->yy_fill_buffer = 1;
-
- /* If b is the current buffer, then yy_init_buffer was _probably_
- * called from yyrestart() or through yy_get_next_buffer.
- * In that case, we don't want to reset the lineno or column.
- */
- if (b != YY_CURRENT_BUFFER){
- b->yy_bs_lineno = 1;
- b->yy_bs_column = 0;
- }
-
-/* %if-c-only */
-
- b->yy_is_interactive = file ? (isatty( fileno(file) ) > 0) : 0;
-
-/* %endif */
-/* %if-c++-only */
-/* %endif */
- errno = oerrno;
-}
-
-/** Discard all buffered characters. On the next scan, YY_INPUT will be called.
- * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER.
- *
- */
-/* %if-c-only */
- void yy_flush_buffer (YY_BUFFER_STATE b )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- if ( ! b )
- return;
-
- b->yy_n_chars = 0;
-
- /* We always need two end-of-buffer characters. The first causes
- * a transition to the end-of-buffer state. The second causes
- * a jam in that state.
- */
- b->yy_ch_buf[0] = YY_END_OF_BUFFER_CHAR;
- b->yy_ch_buf[1] = YY_END_OF_BUFFER_CHAR;
-
- b->yy_buf_pos = &b->yy_ch_buf[0];
-
- b->yy_at_bol = 1;
- b->yy_buffer_status = YY_BUFFER_NEW;
-
- if ( b == YY_CURRENT_BUFFER )
- yy_load_buffer_state( );
-}
-
-/* %if-c-or-c++ */
-/** Pushes the new state onto the stack. The new state becomes
- * the current state. This function will allocate the stack
- * if necessary.
- * @param new_buffer The new state.
- *
- */
-/* %if-c-only */
-void yypush_buffer_state (YY_BUFFER_STATE new_buffer )
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- if (new_buffer == NULL)
- return;
-
- yyensure_buffer_stack();
-
- /* This block is copied from yy_switch_to_buffer. */
- if ( YY_CURRENT_BUFFER )
- {
- /* Flush out information for old buffer. */
- *(yy_c_buf_p) = (yy_hold_char);
- YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
- YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
- }
-
- /* Only push if top exists. Otherwise, replace top. */
- if (YY_CURRENT_BUFFER)
- (yy_buffer_stack_top)++;
- YY_CURRENT_BUFFER_LVALUE = new_buffer;
-
- /* copied from yy_switch_to_buffer. */
- yy_load_buffer_state( );
- (yy_did_buffer_switch_on_eof) = 1;
-}
-/* %endif */
-
-/* %if-c-or-c++ */
-/** Removes and deletes the top of the stack, if present.
- * The next element becomes the new top.
- *
- */
-/* %if-c-only */
-void yypop_buffer_state (void)
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- if (!YY_CURRENT_BUFFER)
- return;
-
- yy_delete_buffer(YY_CURRENT_BUFFER );
- YY_CURRENT_BUFFER_LVALUE = NULL;
- if ((yy_buffer_stack_top) > 0)
- --(yy_buffer_stack_top);
-
- if (YY_CURRENT_BUFFER) {
- yy_load_buffer_state( );
- (yy_did_buffer_switch_on_eof) = 1;
- }
-}
-/* %endif */
-
-/* %if-c-or-c++ */
-/* Allocates the stack if it does not exist.
- * Guarantees space for at least one push.
- */
-/* %if-c-only */
-static void yyensure_buffer_stack (void)
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-{
- yy_size_t num_to_alloc;
-
- if (!(yy_buffer_stack)) {
-
- /* First allocation is just for 2 elements, since we don't know if this
- * scanner will even need a stack. We use 2 instead of 1 to avoid an
- * immediate realloc on the next call.
- */
- num_to_alloc = 1;
- (yy_buffer_stack) = (struct yy_buffer_state**)yyalloc
- (num_to_alloc * sizeof(struct yy_buffer_state*)
- );
- if ( ! (yy_buffer_stack) )
- YY_FATAL_ERROR( "out of dynamic memory in yyensure_buffer_stack()" );
-
- memset((yy_buffer_stack), 0, num_to_alloc * sizeof(struct yy_buffer_state*));
-
- (yy_buffer_stack_max) = num_to_alloc;
- (yy_buffer_stack_top) = 0;
- return;
- }
-
- if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1){
-
- /* Increase the buffer to prepare for a possible push. */
- int grow_size = 8 /* arbitrary grow size */;
-
- num_to_alloc = (yy_buffer_stack_max) + grow_size;
- (yy_buffer_stack) = (struct yy_buffer_state**)yyrealloc
- ((yy_buffer_stack),
- num_to_alloc * sizeof(struct yy_buffer_state*)
- );
- if ( ! (yy_buffer_stack) )
- YY_FATAL_ERROR( "out of dynamic memory in yyensure_buffer_stack()" );
-
- /* zero only the new slots.*/
- memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, grow_size * sizeof(struct yy_buffer_state*));
- (yy_buffer_stack_max) = num_to_alloc;
- }
-}
-/* %endif */
-
-/* %if-c-only */
-/** Setup the input buffer state to scan directly from a user-specified character buffer.
- * @param base the character buffer
- * @param size the size in bytes of the character buffer
- *
- * @return the newly allocated buffer state object.
- */
-YY_BUFFER_STATE yy_scan_buffer (char * base, yy_size_t size )
-{
- YY_BUFFER_STATE b;
-
- if ( size < 2 ||
- base[size-2] != YY_END_OF_BUFFER_CHAR ||
- base[size-1] != YY_END_OF_BUFFER_CHAR )
- /* They forgot to leave room for the EOB's. */
- return 0;
-
- b = (YY_BUFFER_STATE) yyalloc(sizeof( struct yy_buffer_state ) );
- if ( ! b )
- YY_FATAL_ERROR( "out of dynamic memory in yy_scan_buffer()" );
-
- b->yy_buf_size = size - 2; /* "- 2" to take care of EOB's */
- b->yy_buf_pos = b->yy_ch_buf = base;
- b->yy_is_our_buffer = 0;
- b->yy_input_file = 0;
- b->yy_n_chars = b->yy_buf_size;
- b->yy_is_interactive = 0;
- b->yy_at_bol = 1;
- b->yy_fill_buffer = 0;
- b->yy_buffer_status = YY_BUFFER_NEW;
-
- yy_switch_to_buffer(b );
-
- return b;
-}
-/* %endif */
-
-/* %if-c-only */
-/** Setup the input buffer state to scan a string. The next call to yylex() will
- * scan from a @e copy of @a str.
- * @param yystr a NUL-terminated string to scan
- *
- * @return the newly allocated buffer state object.
- * @note If you want to scan bytes that may contain NUL values, then use
- * yy_scan_bytes() instead.
- */
-YY_BUFFER_STATE yy_scan_string (yyconst char * yystr )
-{
-
- return yy_scan_bytes(yystr,strlen(yystr) );
-}
-/* %endif */
-
-/* %if-c-only */
-/** Setup the input buffer state to scan the given bytes. The next call to yylex() will
- * scan from a @e copy of @a bytes.
- * @param yybytes the byte buffer to scan
- * @param _yybytes_len the number of bytes in the buffer pointed to by @a bytes.
- *
- * @return the newly allocated buffer state object.
- */
-YY_BUFFER_STATE yy_scan_bytes (yyconst char * yybytes, yy_size_t _yybytes_len )
-{
- YY_BUFFER_STATE b;
- char *buf;
- yy_size_t n;
- yy_size_t i;
-
- /* Get memory for full buffer, including space for trailing EOB's. */
- n = _yybytes_len + 2;
- buf = (char *) yyalloc(n );
- if ( ! buf )
- YY_FATAL_ERROR( "out of dynamic memory in yy_scan_bytes()" );
-
- for ( i = 0; i < _yybytes_len; ++i )
- buf[i] = yybytes[i];
-
- buf[_yybytes_len] = buf[_yybytes_len+1] = YY_END_OF_BUFFER_CHAR;
-
- b = yy_scan_buffer(buf,n );
- if ( ! b )
- YY_FATAL_ERROR( "bad buffer in yy_scan_bytes()" );
-
- /* It's okay to grow etc. this buffer, and we should throw it
- * away when we're done.
- */
- b->yy_is_our_buffer = 1;
-
- return b;
-}
-/* %endif */
-
-#ifndef YY_EXIT_FAILURE
-#define YY_EXIT_FAILURE 2
-#endif
-
-/* %if-c-only */
-static void yy_fatal_error (yyconst char* msg )
-{
- (void) fprintf( stderr, "%s\n", msg );
- exit( YY_EXIT_FAILURE );
-}
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-
-/* Redefine yyless() so it works in section 3 code. */
-
-#undef yyless
-#define yyless(n) \
- do \
- { \
- /* Undo effects of setting up yytext. */ \
- int yyless_macro_arg = (n); \
- YY_LESS_LINENO(yyless_macro_arg);\
- yytext[yyleng] = (yy_hold_char); \
- (yy_c_buf_p) = yytext + yyless_macro_arg; \
- (yy_hold_char) = *(yy_c_buf_p); \
- *(yy_c_buf_p) = '\0'; \
- yyleng = yyless_macro_arg; \
- } \
- while ( 0 )
-
-/* Accessor methods (get/set functions) to struct members. */
-
-/* %if-c-only */
-/* %if-reentrant */
-/* %endif */
-
-/** Get the current line number.
- *
- */
-int yyget_lineno (void)
-{
-
- return yylineno;
-}
-
-/** Get the input stream.
- *
- */
-FILE *yyget_in (void)
-{
- return yyin;
-}
-
-/** Get the output stream.
- *
- */
-FILE *yyget_out (void)
-{
- return yyout;
-}
-
-/** Get the length of the current token.
- *
- */
-yy_size_t yyget_leng (void)
-{
- return yyleng;
-}
-
-/** Get the current token.
- *
- */
-
-char *yyget_text (void)
-{
- return yytext;
-}
-
-/* %if-reentrant */
-/* %endif */
-
-/** Set the current line number.
- * @param line_number
- *
- */
-void yyset_lineno (int line_number )
-{
-
- yylineno = line_number;
-}
-
-/** Set the input stream. This does not discard the current
- * input buffer.
- * @param in_str A readable stream.
- *
- * @see yy_switch_to_buffer
- */
-void yyset_in (FILE * in_str )
-{
- yyin = in_str ;
-}
-
-void yyset_out (FILE * out_str )
-{
- yyout = out_str ;
-}
-
-int yyget_debug (void)
-{
- return yy_flex_debug;
-}
-
-void yyset_debug (int bdebug )
-{
- yy_flex_debug = bdebug ;
-}
-
-/* %endif */
-
-/* %if-reentrant */
-/* %if-bison-bridge */
-/* %endif */
-/* %endif if-c-only */
-
-/* %if-c-only */
-static int yy_init_globals (void)
-{
- /* Initialization is the same as for the non-reentrant scanner.
- * This function is called from yylex_destroy(), so don't allocate here.
- */
-
- (yy_buffer_stack) = 0;
- (yy_buffer_stack_top) = 0;
- (yy_buffer_stack_max) = 0;
- (yy_c_buf_p) = (char *) 0;
- (yy_init) = 0;
- (yy_start) = 0;
-
-/* Defined in main.c */
-#ifdef YY_STDINIT
- yyin = stdin;
- yyout = stdout;
-#else
- yyin = (FILE *) 0;
- yyout = (FILE *) 0;
-#endif
-
- /* For future reference: Set errno on error, since we are called by
- * yylex_init()
- */
- return 0;
-}
-/* %endif */
-
-/* %if-c-only SNIP! this currently causes conflicts with the c++ scanner */
-/* yylex_destroy is for both reentrant and non-reentrant scanners. */
-int yylex_destroy (void)
-{
-
- /* Pop the buffer stack, destroying each element. */
- while(YY_CURRENT_BUFFER){
- yy_delete_buffer(YY_CURRENT_BUFFER );
- YY_CURRENT_BUFFER_LVALUE = NULL;
- yypop_buffer_state();
- }
-
- /* Destroy the stack itself. */
- yyfree((yy_buffer_stack) );
- (yy_buffer_stack) = NULL;
-
- /* Reset the globals. This is important in a non-reentrant scanner so the next time
- * yylex() is called, initialization will occur. */
- yy_init_globals( );
-
-/* %if-reentrant */
-/* %endif */
- return 0;
-}
-/* %endif */
-
-/*
- * Internal utility routines.
- */
-
-#ifndef yytext_ptr
-static void yy_flex_strncpy (char* s1, yyconst char * s2, int n )
-{
- register int i;
- for ( i = 0; i < n; ++i )
- s1[i] = s2[i];
-}
-#endif
-
-#ifdef YY_NEED_STRLEN
-static int yy_flex_strlen (yyconst char * s )
-{
- register int n;
- for ( n = 0; s[n]; ++n )
- ;
-
- return n;
-}
-#endif
-
-void *yyalloc (yy_size_t size )
-{
- return (void *) malloc( size );
-}
-
-void *yyrealloc (void * ptr, yy_size_t size )
-{
- /* The cast to (char *) in the following accommodates both
- * implementations that use char* generic pointers, and those
- * that use void* generic pointers. It works with the latter
- * because both ANSI C and C++ allow castless assignment from
- * any pointer type to void*, and deal with argument conversions
- * as though doing an assignment.
- */
- return (void *) realloc( (char *) ptr, size );
-}
-
-void yyfree (void * ptr )
-{
- free( (char *) ptr ); /* see yyrealloc() for (char *) cast */
-}
-
-/* %if-tables-serialization definitions */
-/* %define-yytables The name for this specific scanner's tables. */
-#define YYTABLES_NAME "yytables"
-/* %endif */
-
-/* %ok-for-header */
-
-#line 108 "mlf-scanner.ll"
-
-
-
-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/src/lib/GMLMIP-0.1/parser/lex.yy.h b/src/lib/GMLMIP-0.1/parser/lex.yy.h
deleted file mode 100644
index ed75b0e02cfe09bf3e505955a172ab0478736366..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/lex.yy.h
+++ /dev/null
@@ -1,432 +0,0 @@
-#ifndef yyHEADER_H
-#define yyHEADER_H 1
-#define yyIN_HEADER 1
-
-#line 6 "lex.yy.h"
-
-#define YY_INT_ALIGNED short int
-
-/* A lexical scanner generated by flex */
-
-/* %not-for-header */
-
-#define FLEX_SCANNER
-#define YY_FLEX_MAJOR_VERSION 2
-#define YY_FLEX_MINOR_VERSION 5
-#define YY_FLEX_SUBMINOR_VERSION 39
-#if YY_FLEX_SUBMINOR_VERSION > 0
-#define FLEX_BETA
-#endif
-
-/* %if-c++-only */
-/* %endif */
-
-/* %if-c-only */
-
-/* %endif */
-
-/* %if-c-only */
-
-/* %endif */
-
-/* First, we deal with platform-specific or compiler-specific issues. */
-
-/* begin standard C headers. */
-/* %if-c-only */
-#include <stdio.h>
-#include <string.h>
-#include <errno.h>
-#include <stdlib.h>
-/* %endif */
-
-/* %if-tables-serialization */
-/* %endif */
-/* end standard C headers. */
-
-/* %if-c-or-c++ */
-/* flex integer type definitions */
-
-#ifndef FLEXINT_H
-#define FLEXINT_H
-
-/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
-
-#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L
-
-/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h,
- * if you want the limit (max/min) macros for int types.
- */
-#ifndef __STDC_LIMIT_MACROS
-#define __STDC_LIMIT_MACROS 1
-#endif
-
-#include <inttypes.h>
-typedef int8_t flex_int8_t;
-typedef uint8_t flex_uint8_t;
-typedef int16_t flex_int16_t;
-typedef uint16_t flex_uint16_t;
-typedef int32_t flex_int32_t;
-typedef uint32_t flex_uint32_t;
-#else
-typedef signed char flex_int8_t;
-typedef short int flex_int16_t;
-typedef int flex_int32_t;
-typedef unsigned char flex_uint8_t;
-typedef unsigned short int flex_uint16_t;
-typedef unsigned int flex_uint32_t;
-
-/* Limits of integral types. */
-#ifndef INT8_MIN
-#define INT8_MIN (-128)
-#endif
-#ifndef INT16_MIN
-#define INT16_MIN (-32767-1)
-#endif
-#ifndef INT32_MIN
-#define INT32_MIN (-2147483647-1)
-#endif
-#ifndef INT8_MAX
-#define INT8_MAX (127)
-#endif
-#ifndef INT16_MAX
-#define INT16_MAX (32767)
-#endif
-#ifndef INT32_MAX
-#define INT32_MAX (2147483647)
-#endif
-#ifndef UINT8_MAX
-#define UINT8_MAX (255U)
-#endif
-#ifndef UINT16_MAX
-#define UINT16_MAX (65535U)
-#endif
-#ifndef UINT32_MAX
-#define UINT32_MAX (4294967295U)
-#endif
-
-#endif /* ! C99 */
-
-#endif /* ! FLEXINT_H */
-
-/* %endif */
-
-/* %if-c++-only */
-/* %endif */
-
-#ifdef __cplusplus
-
-/* The "const" storage-class-modifier is valid. */
-#define YY_USE_CONST
-
-#else /* ! __cplusplus */
-
-/* C99 requires __STDC__ to be defined as 1. */
-#if defined (__STDC__)
-
-#define YY_USE_CONST
-
-#endif /* defined (__STDC__) */
-#endif /* ! __cplusplus */
-
-#ifdef YY_USE_CONST
-#define yyconst const
-#else
-#define yyconst
-#endif
-
-/* %not-for-header */
-
-/* %not-for-header */
-
-/* %if-reentrant */
-/* %endif */
-
-/* %if-not-reentrant */
-
-/* %endif */
-
-/* Size of default input buffer. */
-#ifndef YY_BUF_SIZE
-#define YY_BUF_SIZE 16384
-#endif
-
-#ifndef YY_TYPEDEF_YY_BUFFER_STATE
-#define YY_TYPEDEF_YY_BUFFER_STATE
-typedef struct yy_buffer_state *YY_BUFFER_STATE;
-#endif
-
-#ifndef YY_TYPEDEF_YY_SIZE_T
-#define YY_TYPEDEF_YY_SIZE_T
-typedef size_t yy_size_t;
-#endif
-
-/* %if-not-reentrant */
-extern yy_size_t yyleng;
-/* %endif */
-
-/* %if-c-only */
-/* %if-not-reentrant */
-extern FILE *yyin, *yyout;
-/* %endif */
-/* %endif */
-
-#ifndef YY_STRUCT_YY_BUFFER_STATE
-#define YY_STRUCT_YY_BUFFER_STATE
-struct yy_buffer_state
- {
-/* %if-c-only */
- FILE *yy_input_file;
-/* %endif */
-
-/* %if-c++-only */
-/* %endif */
-
- char *yy_ch_buf; /* input buffer */
- char *yy_buf_pos; /* current position in input buffer */
-
- /* Size of input buffer in bytes, not including room for EOB
- * characters.
- */
- yy_size_t yy_buf_size;
-
- /* Number of characters read into yy_ch_buf, not including EOB
- * characters.
- */
- yy_size_t yy_n_chars;
-
- /* Whether we "own" the buffer - i.e., we know we created it,
- * and can realloc() it to grow it, and should free() it to
- * delete it.
- */
- int yy_is_our_buffer;
-
- /* Whether this is an "interactive" input source; if so, and
- * if we're using stdio for input, then we want to use getc()
- * instead of fread(), to make sure we stop fetching input after
- * each newline.
- */
- int yy_is_interactive;
-
- /* Whether we're considered to be at the beginning of a line.
- * If so, '^' rules will be active on the next match, otherwise
- * not.
- */
- int yy_at_bol;
-
- int yy_bs_lineno; /**< The line count. */
- int yy_bs_column; /**< The column count. */
-
- /* Whether to try to fill the input buffer when we reach the
- * end of it.
- */
- int yy_fill_buffer;
-
- int yy_buffer_status;
-
- };
-#endif /* !YY_STRUCT_YY_BUFFER_STATE */
-
-/* %if-c-only Standard (non-C++) definition */
-/* %not-for-header */
-
-/* %endif */
-
-/* %if-c-only Standard (non-C++) definition */
-
-/* %if-not-reentrant */
-/* %not-for-header */
-
-/* %endif */
-
-void yyrestart (FILE *input_file );
-void yy_switch_to_buffer (YY_BUFFER_STATE new_buffer );
-YY_BUFFER_STATE yy_create_buffer (FILE *file,int size );
-void yy_delete_buffer (YY_BUFFER_STATE b );
-void yy_flush_buffer (YY_BUFFER_STATE b );
-void yypush_buffer_state (YY_BUFFER_STATE new_buffer );
-void yypop_buffer_state (void );
-
-YY_BUFFER_STATE yy_scan_buffer (char *base,yy_size_t size );
-YY_BUFFER_STATE yy_scan_string (yyconst char *yy_str );
-YY_BUFFER_STATE yy_scan_bytes (yyconst char *bytes,yy_size_t len );
-
-/* %endif */
-
-void *yyalloc (yy_size_t );
-void *yyrealloc (void *,yy_size_t );
-void yyfree (void * );
-
-/* %% [1.0] yytext/yyin/yyout/yy_state_type/yylineno etc. def's & init go here */
-/* Begin user sect3 */
-
-#define yywrap() 1
-#define YY_SKIP_YYWRAP
-
-#define FLEX_DEBUG
-
-extern int yylineno;
-
-extern char *yytext;
-#define yytext_ptr yytext
-
-/* %if-c-only Standard (non-C++) definition */
-
-/* %endif */
-
-#ifdef YY_HEADER_EXPORT_START_CONDITIONS
-#define INITIAL 0
-
-#endif
-
-#ifndef YY_NO_UNISTD_H
-/* Special case for "unistd.h", since it is non-ANSI. We include it way
- * down here because we want the user's section 1 to have been scanned first.
- * The user has a chance to override it with an option.
- */
-/* %if-c-only */
-#include <unistd.h>
-/* %endif */
-/* %if-c++-only */
-/* %endif */
-#endif
-
-#ifndef YY_EXTRA_TYPE
-#define YY_EXTRA_TYPE void *
-#endif
-
-/* %if-c-only Reentrant structure and macros (non-C++). */
-/* %if-reentrant */
-/* %if-c-only */
-
-/* %endif */
-/* %if-reentrant */
-/* %endif */
-/* %endif End reentrant structures and macros. */
-
-/* Accessor methods to globals.
- These are made visible to non-reentrant scanners for convenience. */
-
-int yylex_destroy (void );
-
-int yyget_debug (void );
-
-void yyset_debug (int debug_flag );
-
-YY_EXTRA_TYPE yyget_extra (void );
-
-void yyset_extra (YY_EXTRA_TYPE user_defined );
-
-FILE *yyget_in (void );
-
-void yyset_in (FILE * in_str );
-
-FILE *yyget_out (void );
-
-void yyset_out (FILE * out_str );
-
-yy_size_t yyget_leng (void );
-
-char *yyget_text (void );
-
-int yyget_lineno (void );
-
-void yyset_lineno (int line_number );
-
-/* %if-bison-bridge */
-/* %endif */
-
-/* Macros after this point can all be overridden by user definitions in
- * section 1.
- */
-
-#ifndef YY_SKIP_YYWRAP
-#ifdef __cplusplus
-extern "C" int yywrap (void );
-#else
-extern int yywrap (void );
-#endif
-#endif
-
-/* %not-for-header */
-
-/* %endif */
-
-#ifndef yytext_ptr
-static void yy_flex_strncpy (char *,yyconst char *,int );
-#endif
-
-#ifdef YY_NEED_STRLEN
-static int yy_flex_strlen (yyconst char * );
-#endif
-
-#ifndef YY_NO_INPUT
-/* %if-c-only Standard (non-C++) definition */
-/* %not-for-header */
-
-/* %endif */
-#endif
-
-/* %if-c-only */
-
-/* %endif */
-
-/* Amount of stuff to slurp up with each read. */
-#ifndef YY_READ_BUF_SIZE
-#define YY_READ_BUF_SIZE 8192
-#endif
-
-/* Number of entries by which start-condition stack grows. */
-#ifndef YY_START_STACK_INCR
-#define YY_START_STACK_INCR 25
-#endif
-
-/* %if-tables-serialization structures and prototypes */
-/* %not-for-header */
-
-/* %not-for-header */
-
-/* Default declaration of generated scanner - a define so the user can
- * easily add parameters.
- */
-#ifndef YY_DECL
-#define YY_DECL_IS_OURS 1
-/* %if-c-only Standard (non-C++) definition */
-
-extern int yylex (void);
-
-#define YY_DECL int yylex (void)
-/* %endif */
-/* %if-c++-only C++ definition */
-/* %endif */
-#endif /* !YY_DECL */
-
-/* %not-for-header */
-
-/* %if-c++-only */
-/* %not-for-header */
-
-/* %endif */
-
-/* yy_get_previous_state - get the state just before the EOB char was reached */
-
-/* %if-c-only */
-/* %not-for-header */
-
-#undef YY_NEW_FILE
-#undef YY_FLUSH_BUFFER
-#undef yy_set_bol
-#undef yy_new_buffer
-#undef yy_set_interactive
-#undef YY_DO_BEFORE_ACTION
-
-#ifdef YY_DECL_IS_OURS
-#undef YY_DECL_IS_OURS
-#undef YY_DECL
-#endif
-
-#line 108 "mlf-scanner.ll"
-
-
-#line 431 "lex.yy.h"
-#undef yyIN_HEADER
-#endif /* yyHEADER_H */
diff --git a/src/lib/GMLMIP-0.1/parser/location.h b/src/lib/GMLMIP-0.1/parser/location.h
deleted file mode 100644
index 7c05741cfbd8cd4502f0c50b556d4e76884b0784..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/location.h
+++ /dev/null
@@ -1,187 +0,0 @@
-// A Bison parser, made by GNU Bison 3.0.2.
-
-// Locations for Bison parsers in C++
-
-// Copyright (C) 2002-2013 Free Software Foundation, Inc.
-
-// This program is free software: you can redistribute it and/or modify
-// it under the terms of the GNU General Public License as published by
-// the Free Software Foundation, either version 3 of the License, or
-// (at your option) any later version.
-
-// This program is distributed in the hope that it will be useful,
-// but WITHOUT ANY WARRANTY; without even the implied warranty of
-// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-// GNU General Public License for more details.
-
-// You should have received a copy of the GNU General Public License
-// along with this program. If not, see <http://www.gnu.org/licenses/>.
-
-// As a special exception, you may create a larger work that contains
-// part or all of the Bison parser skeleton and distribute that work
-// under terms of your choice, so long as that work isn't itself a
-// parser generator using the skeleton or a modified version thereof
-// as a parser skeleton. Alternatively, if you modify or redistribute
-// the parser skeleton itself, you may (at your option) remove this
-// special exception, which will cause the skeleton and the resulting
-// Bison output files to be licensed under the GNU General Public
-// License without this special exception.
-
-// This special exception was added by the Free Software Foundation in
-// version 2.2 of Bison.
-
-/**
- ** \file location.hh
- ** Define the yy::location class.
- */
-
-#ifndef YY_YY_LOCATION_HH_INCLUDED
-# define YY_YY_LOCATION_HH_INCLUDED
-
-# include "position.h"
-
-
-namespace yy {
-#line 46 "location.h" // location.cc:291
- /// Abstract a location.
- class location
- {
- public:
-
- /// Construct a location from \a b to \a e.
- location (const position& b, const position& e)
- : begin (b)
- , end (e)
- {
- }
-
- /// Construct a 0-width location in \a p.
- explicit location (const position& p = position ())
- : begin (p)
- , end (p)
- {
- }
-
- /// Construct a 0-width location in \a f, \a l, \a c.
- explicit location (std::string* f,
- unsigned int l = 1u,
- unsigned int c = 1u)
- : begin (f, l, c)
- , end (f, l, c)
- {
- }
-
-
- /// Initialization.
- void initialize (std::string* f = YY_NULLPTR,
- unsigned int l = 1u,
- unsigned int c = 1u)
- {
- begin.initialize (f, l, c);
- end = begin;
- }
-
- /** \name Line and Column related manipulators
- ** \{ */
- public:
- /// Reset initial location to final location.
- void step ()
- {
- begin = end;
- }
-
- /// Extend the current location to the COUNT next columns.
- void columns (int count = 1)
- {
- end += count;
- }
-
- /// Extend the current location to the COUNT next lines.
- void lines (int count = 1)
- {
- end.lines (count);
- }
- /** \} */
-
-
- public:
- /// Beginning of the located region.
- position begin;
- /// End of the located region.
- position end;
- };
-
- /// Join two location objects to create a location.
- inline location operator+ (location res, const location& end)
- {
- res.end = end.end;
- return res;
- }
-
- /// Change end position in place.
- inline location& operator+= (location& res, int width)
- {
- res.columns (width);
- return res;
- }
-
- /// Change end position.
- inline location operator+ (location res, int width)
- {
- return res += width;
- }
-
- /// Change end position in place.
- inline location& operator-= (location& res, int width)
- {
- return res += -width;
- }
-
- /// Change end position.
- inline location operator- (const location& begin, int width)
- {
- return begin + -width;
- }
-
- /// Compare two location objects.
- inline bool
- operator== (const location& loc1, const location& loc2)
- {
- return loc1.begin == loc2.begin && loc1.end == loc2.end;
- }
-
- /// Compare two location objects.
- inline bool
- operator!= (const location& loc1, const location& loc2)
- {
- return !(loc1 == loc2);
- }
-
- /** \brief Intercept output stream redirection.
- ** \param ostr the destination output stream
- ** \param loc a reference to the location to redirect
- **
- ** Avoid duplicate information.
- */
- template <typename YYChar>
- inline std::basic_ostream<YYChar>&
- operator<< (std::basic_ostream<YYChar>& ostr, const location& loc)
- {
- unsigned int end_col = 0 < loc.end.column ? loc.end.column - 1 : 0;
- ostr << loc.begin// << "(" << loc.end << ") "
-;
- if (loc.end.filename
- && (!loc.begin.filename
- || *loc.begin.filename != *loc.end.filename))
- ostr << '-' << loc.end.filename << ':' << loc.end.line << '.' << end_col;
- else if (loc.begin.line < loc.end.line)
- ostr << '-' << loc.end.line << '.' << end_col;
- else if (loc.begin.column < end_col)
- ostr << '-' << end_col;
- return ostr;
- }
-
-
-} // yy
-#line 187 "location.h" // location.cc:291
-#endif // !YY_YY_LOCATION_HH_INCLUDED
diff --git a/src/lib/GMLMIP-0.1/parser/makefile b/src/lib/GMLMIP-0.1/parser/makefile
deleted file mode 100644
index 041bff3f9f9efa7b6dc00ef84f04ff721560f579..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/makefile
+++ /dev/null
@@ -1,36 +0,0 @@
-include ../config.mk
-
-.PHONY: all clean
-
-all: parser lex.yy.o mlf-parser.tab.o mlf-driver.o
-
-
-../formulas/%:
- make -C ../formulas/ $(@:../formulas/%=%)
-
-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 lex.yy.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/src/lib/GMLMIP-0.1/parser/mlf-driver.c b/src/lib/GMLMIP-0.1/parser/mlf-driver.c
deleted file mode 100644
index 09279c6b4c46b667c9ce59576322aa6e5f8986ef..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/mlf-driver.c
+++ /dev/null
@@ -1,60 +0,0 @@
-#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/src/lib/GMLMIP-0.1/parser/mlf-driver.h b/src/lib/GMLMIP-0.1/parser/mlf-driver.h
deleted file mode 100644
index 2c6666c32d4a982eb03e7dcff78c6366fcea3c7d..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/mlf-driver.h
+++ /dev/null
@@ -1,62 +0,0 @@
-#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/src/lib/GMLMIP-0.1/parser/mlf-parser.tab.c b/src/lib/GMLMIP-0.1/parser/mlf-parser.tab.c
deleted file mode 100644
index d3c4317d4b2126b673b89247a90873cdae8c1b1a..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/mlf-parser.tab.c
+++ /dev/null
@@ -1,1148 +0,0 @@
-// A Bison parser, made by GNU Bison 3.0.2.
-
-// Skeleton implementation for Bison LALR(1) parsers in C++
-
-// Copyright (C) 2002-2013 Free Software Foundation, Inc.
-
-// This program is free software: you can redistribute it and/or modify
-// it under the terms of the GNU General Public License as published by
-// the Free Software Foundation, either version 3 of the License, or
-// (at your option) any later version.
-
-// This program is distributed in the hope that it will be useful,
-// but WITHOUT ANY WARRANTY; without even the implied warranty of
-// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-// GNU General Public License for more details.
-
-// You should have received a copy of the GNU General Public License
-// along with this program. If not, see <http://www.gnu.org/licenses/>.
-
-// As a special exception, you may create a larger work that contains
-// part or all of the Bison parser skeleton and distribute that work
-// under terms of your choice, so long as that work isn't itself a
-// parser generator using the skeleton or a modified version thereof
-// as a parser skeleton. Alternatively, if you modify or redistribute
-// the parser skeleton itself, you may (at your option) remove this
-// special exception, which will cause the skeleton and the resulting
-// Bison output files to be licensed under the GNU General Public
-// License without this special exception.
-
-// This special exception was added by the Free Software Foundation in
-// version 2.2 of Bison.
-
-
-// First part of user declarations.
-
-#line 37 "mlf-parser.tab.cc" // lalr1.cc:399
-
-# ifndef YY_NULLPTR
-# if defined __cplusplus && 201103L <= __cplusplus
-# define YY_NULLPTR nullptr
-# else
-# define YY_NULLPTR 0
-# endif
-# endif
-
-#include "mlf-parser.tab.h"
-
-// User implementation prologue.
-
-#line 51 "mlf-parser.tab.cc" // lalr1.cc:407
-// Unqualified %code blocks.
-#line 44 "mlf-parser.yy" // lalr1.cc:408
-
- #include "mlf-driver.h"
-
-#line 57 "mlf-parser.tab.cc" // lalr1.cc:408
-
-
-#ifndef YY_
-# if defined YYENABLE_NLS && YYENABLE_NLS
-# if ENABLE_NLS
-# include <libintl.h> // FIXME: INFRINGES ON USER NAME SPACE.
-# define YY_(msgid) dgettext ("bison-runtime", msgid)
-# endif
-# endif
-# ifndef YY_
-# define YY_(msgid) msgid
-# endif
-#endif
-
-#define YYRHSLOC(Rhs, K) ((Rhs)[K].location)
-/* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N].
- If N is 0, then set CURRENT to the empty location which ends
- the previous symbol: RHS[0] (always defined). */
-
-# ifndef YYLLOC_DEFAULT
-# define YYLLOC_DEFAULT(Current, Rhs, N) \
- do \
- if (N) \
- { \
- (Current).begin = YYRHSLOC (Rhs, 1).begin; \
- (Current).end = YYRHSLOC (Rhs, N).end; \
- } \
- else \
- { \
- (Current).begin = (Current).end = YYRHSLOC (Rhs, 0).end; \
- } \
- while (/*CONSTCOND*/ false)
-# endif
-
-
-// Suppress unused-variable warnings by "using" E.
-#define YYUSE(E) ((void) (E))
-
-// Enable debugging if requested.
-#if YYDEBUG
-
-// A pseudo ostream that takes yydebug_ into account.
-# define YYCDEBUG if (yydebug_) (*yycdebug_)
-
-# define YY_SYMBOL_PRINT(Title, Symbol) \
- do { \
- if (yydebug_) \
- { \
- *yycdebug_ << Title << ' '; \
- yy_print_ (*yycdebug_, Symbol); \
- *yycdebug_ << std::endl; \
- } \
- } while (false)
-
-# define YY_REDUCE_PRINT(Rule) \
- do { \
- if (yydebug_) \
- yy_reduce_print_ (Rule); \
- } while (false)
-
-# define YY_STACK_PRINT() \
- do { \
- if (yydebug_) \
- yystack_print_ (); \
- } while (false)
-
-#else // !YYDEBUG
-
-# define YYCDEBUG if (false) std::cerr
-# define YY_SYMBOL_PRINT(Title, Symbol) YYUSE(Symbol)
-# define YY_REDUCE_PRINT(Rule) static_cast<void>(0)
-# define YY_STACK_PRINT() static_cast<void>(0)
-
-#endif // !YYDEBUG
-
-#define yyerrok (yyerrstatus_ = 0)
-#define yyclearin (yyempty = true)
-
-#define YYACCEPT goto yyacceptlab
-#define YYABORT goto yyabortlab
-#define YYERROR goto yyerrorlab
-#define YYRECOVERING() (!!yyerrstatus_)
-
-
-namespace yy {
-#line 143 "mlf-parser.tab.cc" // lalr1.cc:474
-
- /* Return YYSTR after stripping away unnecessary quotes and
- backslashes, so that it's suitable for yyerror. The heuristic is
- that double-quoting is unnecessary unless the string contains an
- apostrophe, a comma, or backslash (other than backslash-backslash).
- YYSTR is taken from yytname. */
- std::string
- mlf_parser::yytnamerr_ (const char *yystr)
- {
- if (*yystr == '"')
- {
- std::string yyr = "";
- char const *yyp = yystr;
-
- for (;;)
- switch (*++yyp)
- {
- case '\'':
- case ',':
- goto do_not_strip_quotes;
-
- case '\\':
- if (*++yyp != '\\')
- goto do_not_strip_quotes;
- // Fall through.
- default:
- yyr += *yyp;
- break;
-
- case '"':
- return yyr;
- }
- do_not_strip_quotes: ;
- }
-
- return yystr;
- }
-
-
- /// Build a parser object.
- mlf_parser::mlf_parser (mlf_driver& driver_yyarg)
- :
-#if YYDEBUG
- yydebug_ (false),
- yycdebug_ (&std::cerr),
-#endif
- driver (driver_yyarg)
- {}
-
- mlf_parser::~mlf_parser ()
- {}
-
-
- /*---------------.
- | Symbol types. |
- `---------------*/
-
- inline
- mlf_parser::syntax_error::syntax_error (const location_type& l, const std::string& m)
- : std::runtime_error (m)
- , location (l)
- {}
-
- // basic_symbol.
- template <typename Base>
- inline
- mlf_parser::basic_symbol<Base>::basic_symbol ()
- : value ()
- {}
-
- template <typename Base>
- inline
- mlf_parser::basic_symbol<Base>::basic_symbol (const basic_symbol& other)
- : Base (other)
- , value ()
- , location (other.location)
- {
- value = other.value;
- }
-
-
- template <typename Base>
- inline
- mlf_parser::basic_symbol<Base>::basic_symbol (typename Base::kind_type t, const semantic_type& v, const location_type& l)
- : Base (t)
- , value (v)
- , location (l)
- {}
-
-
- /// Constructor for valueless symbols.
- template <typename Base>
- inline
- mlf_parser::basic_symbol<Base>::basic_symbol (typename Base::kind_type t, const location_type& l)
- : Base (t)
- , value ()
- , location (l)
- {}
-
- template <typename Base>
- inline
- mlf_parser::basic_symbol<Base>::~basic_symbol ()
- {
- }
-
- template <typename Base>
- inline
- void
- mlf_parser::basic_symbol<Base>::move (basic_symbol& s)
- {
- super_type::move(s);
- value = s.value;
- location = s.location;
- }
-
- // by_type.
- inline
- mlf_parser::by_type::by_type ()
- : type (empty)
- {}
-
- inline
- mlf_parser::by_type::by_type (const by_type& other)
- : type (other.type)
- {}
-
- inline
- mlf_parser::by_type::by_type (token_type t)
- : type (yytranslate_ (t))
- {}
-
- inline
- void
- mlf_parser::by_type::move (by_type& that)
- {
- type = that.type;
- that.type = empty;
- }
-
- inline
- int
- mlf_parser::by_type::type_get () const
- {
- return type;
- }
-
-
- // by_state.
- inline
- mlf_parser::by_state::by_state ()
- : state (empty)
- {}
-
- inline
- mlf_parser::by_state::by_state (const by_state& other)
- : state (other.state)
- {}
-
- inline
- void
- mlf_parser::by_state::move (by_state& that)
- {
- state = that.state;
- that.state = empty;
- }
-
- inline
- mlf_parser::by_state::by_state (state_type s)
- : state (s)
- {}
-
- inline
- mlf_parser::symbol_number_type
- mlf_parser::by_state::type_get () const
- {
- return state == empty ? 0 : yystos_[state];
- }
-
- inline
- mlf_parser::stack_symbol_type::stack_symbol_type ()
- {}
-
-
- inline
- mlf_parser::stack_symbol_type::stack_symbol_type (state_type s, symbol_type& that)
- : super_type (s, that.location)
- {
- value = that.value;
- // that is emptied.
- that.type = empty;
- }
-
- inline
- mlf_parser::stack_symbol_type&
- mlf_parser::stack_symbol_type::operator= (const stack_symbol_type& that)
- {
- state = that.state;
- value = that.value;
- location = that.location;
- return *this;
- }
-
-
- template <typename Base>
- inline
- void
- mlf_parser::yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const
- {
- if (yymsg)
- YY_SYMBOL_PRINT (yymsg, yysym);
-
- // User destructor.
- switch (yysym.type_get ())
- {
- case 19: // "identifier"
-
-#line 68 "mlf-parser.yy" // lalr1.cc:599
- { delete &(yysym.value); }
-#line 362 "mlf-parser.tab.cc" // lalr1.cc:599
- break;
-
-
- default:
- break;
- }
- }
-
-#if YYDEBUG
- template <typename Base>
- void
- mlf_parser::yy_print_ (std::ostream& yyo,
- const basic_symbol<Base>& yysym) const
- {
- std::ostream& yyoutput = yyo;
- YYUSE (yyoutput);
- symbol_number_type yytype = yysym.type_get ();
- yyo << (yytype < yyntokens_ ? "token" : "nterm")
- << ' ' << yytname_[yytype] << " ("
- << yysym.location << ": ";
- YYUSE (yytype);
- yyo << ')';
- }
-#endif
-
- inline
- void
- mlf_parser::yypush_ (const char* m, state_type s, symbol_type& sym)
- {
- stack_symbol_type t (s, sym);
- yypush_ (m, t);
- }
-
- inline
- void
- mlf_parser::yypush_ (const char* m, stack_symbol_type& s)
- {
- if (m)
- YY_SYMBOL_PRINT (m, s);
- yystack_.push (s);
- }
-
- inline
- void
- mlf_parser::yypop_ (unsigned int n)
- {
- yystack_.pop (n);
- }
-
-#if YYDEBUG
- std::ostream&
- mlf_parser::debug_stream () const
- {
- return *yycdebug_;
- }
-
- void
- mlf_parser::set_debug_stream (std::ostream& o)
- {
- yycdebug_ = &o;
- }
-
-
- mlf_parser::debug_level_type
- mlf_parser::debug_level () const
- {
- return yydebug_;
- }
-
- void
- mlf_parser::set_debug_level (debug_level_type l)
- {
- yydebug_ = l;
- }
-#endif // YYDEBUG
-
- inline mlf_parser::state_type
- mlf_parser::yy_lr_goto_state_ (state_type yystate, int yysym)
- {
- int yyr = yypgoto_[yysym - yyntokens_] + yystate;
- if (0 <= yyr && yyr <= yylast_ && yycheck_[yyr] == yystate)
- return yytable_[yyr];
- else
- return yydefgoto_[yysym - yyntokens_];
- }
-
- inline bool
- mlf_parser::yy_pact_value_is_default_ (int yyvalue)
- {
- return yyvalue == yypact_ninf_;
- }
-
- inline bool
- mlf_parser::yy_table_value_is_error_ (int yyvalue)
- {
- return yyvalue == yytable_ninf_;
- }
-
- int
- mlf_parser::parse ()
- {
- /// Whether yyla contains a lookahead.
- bool yyempty = true;
-
- // State.
- int yyn;
- /// Length of the RHS of the rule being reduced.
- int yylen = 0;
-
- // Error handling.
- int yynerrs_ = 0;
- int yyerrstatus_ = 0;
-
- /// The lookahead symbol.
- symbol_type yyla;
-
- /// The locations where the error started and ended.
- stack_symbol_type yyerror_range[3];
-
- /// The return value of parse ().
- int yyresult;
-
- // FIXME: This shoud be completely indented. It is not yet to
- // avoid gratuitous conflicts when merging into the master branch.
- try
- {
- YYCDEBUG << "Starting parse" << std::endl;
-
-
- // User initialization code.
- #line 36 "mlf-parser.yy" // lalr1.cc:725
-{
- // Initialize the initial location.
- yyla.location.begin.filename = yyla.location.end.filename = &driver.file;
-}
-
-#line 499 "mlf-parser.tab.cc" // lalr1.cc:725
-
- /* Initialize the stack. The initial state will be set in
- yynewstate, since the latter expects the semantical and the
- location values to have been already stored, initialize these
- stacks with a primary value. */
- yystack_.clear ();
- yypush_ (YY_NULLPTR, 0, yyla);
-
- // A new symbol was pushed on the stack.
- yynewstate:
- YYCDEBUG << "Entering state " << yystack_[0].state << std::endl;
-
- // Accept?
- if (yystack_[0].state == yyfinal_)
- goto yyacceptlab;
-
- goto yybackup;
-
- // Backup.
- yybackup:
-
- // Try to take a decision without lookahead.
- yyn = yypact_[yystack_[0].state];
- if (yy_pact_value_is_default_ (yyn))
- goto yydefault;
-
- // Read a lookahead token.
- if (yyempty)
- {
- YYCDEBUG << "Reading a token: ";
- try
- {
- yyla.type = yytranslate_ (yylex (&yyla.value, &yyla.location, driver));
- }
- catch (const syntax_error& yyexc)
- {
- error (yyexc);
- goto yyerrlab1;
- }
- yyempty = false;
- }
- YY_SYMBOL_PRINT ("Next token is", yyla);
-
- /* If the proper action on seeing token YYLA.TYPE is to reduce or
- to detect an error, take that action. */
- yyn += yyla.type_get ();
- if (yyn < 0 || yylast_ < yyn || yycheck_[yyn] != yyla.type_get ())
- goto yydefault;
-
- // Reduce or error.
- yyn = yytable_[yyn];
- if (yyn <= 0)
- {
- if (yy_table_value_is_error_ (yyn))
- goto yyerrlab;
- yyn = -yyn;
- goto yyreduce;
- }
-
- // Discard the token being shifted.
- yyempty = true;
-
- // Count tokens shifted since error; after three, turn off error status.
- if (yyerrstatus_)
- --yyerrstatus_;
-
- // Shift the lookahead token.
- yypush_ ("Shifting", yyn, yyla);
- goto yynewstate;
-
- /*-----------------------------------------------------------.
- | yydefault -- do the default action for the current state. |
- `-----------------------------------------------------------*/
- yydefault:
- yyn = yydefact_[yystack_[0].state];
- if (yyn == 0)
- goto yyerrlab;
- goto yyreduce;
-
- /*-----------------------------.
- | yyreduce -- Do a reduction. |
- `-----------------------------*/
- yyreduce:
- yylen = yyr2_[yyn];
- {
- stack_symbol_type yylhs;
- yylhs.state = yy_lr_goto_state_(yystack_[yylen].state, yyr1_[yyn]);
- /* If YYLEN is nonzero, implement the default value of the
- action: '$$ = $1'. Otherwise, use the top of the stack.
-
- Otherwise, the following line sets YYLHS.VALUE to garbage.
- This behavior is undocumented and Bison users should not rely
- upon it. */
- if (yylen)
- yylhs.value = yystack_[yylen - 1].value;
- else
- yylhs.value = yystack_[0].value;
-
- // Compute the default @$.
- {
- slice<stack_symbol_type, stack_type> slice (yystack_, yylen);
- YYLLOC_DEFAULT (yylhs.location, slice, yylen);
- }
-
- // Perform the reduction.
- YY_REDUCE_PRINT (yyn);
- try
- {
- switch (yyn)
- {
- case 2:
-#line 75 "mlf-parser.yy" // lalr1.cc:847
- {driver.set_formula_bdd((yystack_[0].value.binarydd)); }
-#line 613 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 3:
-#line 79 "mlf-parser.yy" // lalr1.cc:847
- {driver.set_formula_gml();}
-#line 619 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 4:
-#line 80 "mlf-parser.yy" // lalr1.cc:847
- {driver.set_formula_pml();}
-#line 625 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 5:
-#line 85 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = bdd_biimp((yystack_[2].value.binarydd),(yystack_[0].value.binarydd)); }
-#line 631 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 6:
-#line 86 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = bdd_imp((yystack_[2].value.binarydd),(yystack_[0].value.binarydd)); }
-#line 637 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 7:
-#line 87 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = bdd_or((yystack_[2].value.binarydd),(yystack_[0].value.binarydd)); }
-#line 643 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 8:
-#line 88 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = bdd_and((yystack_[2].value.binarydd),(yystack_[0].value.binarydd)); }
-#line 649 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 9:
-#line 90 "mlf-parser.yy" // lalr1.cc:847
- { bdd* b = new bdd((yystack_[0].value.binarydd)); (yylhs.value.binarydd) = driver.modal(b, (yystack_[1].value.number), 0); }
-#line 655 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 10:
-#line 91 "mlf-parser.yy" // lalr1.cc:847
- { bdd* b = new bdd(bdd_not((yystack_[0].value.binarydd))); (yylhs.value.binarydd) = bdd_not(driver.modal(b, (yystack_[1].value.number), 0)); }
-#line 661 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 11:
-#line 93 "mlf-parser.yy" // lalr1.cc:847
- { bdd* b = new bdd((yystack_[0].value.binarydd)); (yylhs.value.binarydd) = driver.modal(b, (yystack_[1].value.fraction).numerator, (yystack_[1].value.fraction).denominator); }
-#line 667 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 12:
-#line 94 "mlf-parser.yy" // lalr1.cc:847
- { bdd* b = new bdd(bdd_not((yystack_[0].value.binarydd))); (yylhs.value.binarydd) = bdd_not(driver.modal(b, (yystack_[1].value.fraction).numerator, (yystack_[1].value.fraction).denominator)); }
-#line 673 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 13:
-#line 96 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = bdd_not((yystack_[0].value.binarydd)); }
-#line 679 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 14:
-#line 97 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = (yylhs.value.binarydd); }
-#line 685 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 15:
-#line 98 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = bdd_true(); }
-#line 691 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 16:
-#line 99 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = bdd_false(); }
-#line 697 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
- case 17:
-#line 100 "mlf-parser.yy" // lalr1.cc:847
- { (yylhs.value.binarydd) = (yystack_[1].value.binarydd); }
-#line 703 "mlf-parser.tab.cc" // lalr1.cc:847
- break;
-
-
-#line 707 "mlf-parser.tab.cc" // lalr1.cc:847
- default:
- break;
- }
- }
- catch (const syntax_error& yyexc)
- {
- error (yyexc);
- YYERROR;
- }
- YY_SYMBOL_PRINT ("-> $$ =", yylhs);
- yypop_ (yylen);
- yylen = 0;
- YY_STACK_PRINT ();
-
- // Shift the result of the reduction.
- yypush_ (YY_NULLPTR, yylhs);
- }
- goto yynewstate;
-
- /*--------------------------------------.
- | yyerrlab -- here on detecting error. |
- `--------------------------------------*/
- yyerrlab:
- // If not already recovering from an error, report this error.
- if (!yyerrstatus_)
- {
- ++yynerrs_;
- error (yyla.location, yysyntax_error_ (yystack_[0].state,
- yyempty ? yyempty_ : yyla.type_get ()));
- }
-
-
- yyerror_range[1].location = yyla.location;
- if (yyerrstatus_ == 3)
- {
- /* If just tried and failed to reuse lookahead token after an
- error, discard it. */
-
- // Return failure if at end of input.
- if (yyla.type_get () == yyeof_)
- YYABORT;
- else if (!yyempty)
- {
- yy_destroy_ ("Error: discarding", yyla);
- yyempty = true;
- }
- }
-
- // Else will try to reuse lookahead token after shifting the error token.
- goto yyerrlab1;
-
-
- /*---------------------------------------------------.
- | yyerrorlab -- error raised explicitly by YYERROR. |
- `---------------------------------------------------*/
- yyerrorlab:
-
- /* Pacify compilers like GCC when the user code never invokes
- YYERROR and the label yyerrorlab therefore never appears in user
- code. */
- if (false)
- goto yyerrorlab;
- yyerror_range[1].location = yystack_[yylen - 1].location;
- /* Do not reclaim the symbols of the rule whose action triggered
- this YYERROR. */
- yypop_ (yylen);
- yylen = 0;
- goto yyerrlab1;
-
- /*-------------------------------------------------------------.
- | yyerrlab1 -- common code for both syntax error and YYERROR. |
- `-------------------------------------------------------------*/
- yyerrlab1:
- yyerrstatus_ = 3; // Each real token shifted decrements this.
- {
- stack_symbol_type error_token;
- for (;;)
- {
- yyn = yypact_[yystack_[0].state];
- if (!yy_pact_value_is_default_ (yyn))
- {
- yyn += yyterror_;
- if (0 <= yyn && yyn <= yylast_ && yycheck_[yyn] == yyterror_)
- {
- yyn = yytable_[yyn];
- if (0 < yyn)
- break;
- }
- }
-
- // Pop the current state because it cannot handle the error token.
- if (yystack_.size () == 1)
- YYABORT;
-
- yyerror_range[1].location = yystack_[0].location;
- yy_destroy_ ("Error: popping", yystack_[0]);
- yypop_ ();
- YY_STACK_PRINT ();
- }
-
- yyerror_range[2].location = yyla.location;
- YYLLOC_DEFAULT (error_token.location, yyerror_range, 2);
-
- // Shift the error token.
- error_token.state = yyn;
- yypush_ ("Shifting", error_token);
- }
- goto yynewstate;
-
- // Accept.
- yyacceptlab:
- yyresult = 0;
- goto yyreturn;
-
- // Abort.
- yyabortlab:
- yyresult = 1;
- goto yyreturn;
-
- yyreturn:
- if (!yyempty)
- yy_destroy_ ("Cleanup: discarding lookahead", yyla);
-
- /* Do not reclaim the symbols of the rule whose action triggered
- this YYABORT or YYACCEPT. */
- yypop_ (yylen);
- while (1 < yystack_.size ())
- {
- yy_destroy_ ("Cleanup: popping", yystack_[0]);
- yypop_ ();
- }
-
- return yyresult;
- }
- catch (...)
- {
- YYCDEBUG << "Exception caught: cleaning lookahead and stack"
- << std::endl;
- // Do not try to display the values of the reclaimed symbols,
- // as their printer might throw an exception.
- if (!yyempty)
- yy_destroy_ (YY_NULLPTR, yyla);
-
- while (1 < yystack_.size ())
- {
- yy_destroy_ (YY_NULLPTR, yystack_[0]);
- yypop_ ();
- }
- throw;
- }
- }
-
- void
- mlf_parser::error (const syntax_error& yyexc)
- {
- error (yyexc.location, yyexc.what());
- }
-
- // Generate an error message.
- std::string
- mlf_parser::yysyntax_error_ (state_type yystate, symbol_number_type yytoken) const
- {
- std::string yyres;
- // Number of reported tokens (one for the "unexpected", one per
- // "expected").
- size_t yycount = 0;
- // Its maximum.
- enum { YYERROR_VERBOSE_ARGS_MAXIMUM = 5 };
- // Arguments of yyformat.
- char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM];
-
- /* There are many possibilities here to consider:
- - If this state is a consistent state with a default action, then
- the only way this function was invoked is if the default action
- is an error action. In that case, don't check for expected
- tokens because there are none.
- - The only way there can be no lookahead present (in yytoken) is
- if this state is a consistent state with a default action.
- Thus, detecting the absence of a lookahead is sufficient to
- determine that there is no unexpected or expected token to
- report. In that case, just report a simple "syntax error".
- - Don't assume there isn't a lookahead just because this state is
- a consistent state with a default action. There might have
- been a previous inconsistent state, consistent state with a
- non-default action, or user semantic action that manipulated
- yyla. (However, yyla is currently not documented for users.)
- - Of course, the expected token list depends on states to have
- correct lookahead information, and it depends on the parser not
- to perform extra reductions after fetching a lookahead from the
- scanner and before detecting a syntax error. Thus, state
- merging (from LALR or IELR) and default reductions corrupt the
- expected token list. However, the list is correct for
- canonical LR with one exception: it will still contain any
- token that will not be accepted due to an error action in a
- later state.
- */
- if (yytoken != yyempty_)
- {
- yyarg[yycount++] = yytname_[yytoken];
- int yyn = yypact_[yystate];
- if (!yy_pact_value_is_default_ (yyn))
- {
- /* Start YYX at -YYN if negative to avoid negative indexes in
- YYCHECK. In other words, skip the first -YYN actions for
- this state because they are default actions. */
- int yyxbegin = yyn < 0 ? -yyn : 0;
- // Stay within bounds of both yycheck and yytname.
- int yychecklim = yylast_ - yyn + 1;
- int yyxend = yychecklim < yyntokens_ ? yychecklim : yyntokens_;
- for (int yyx = yyxbegin; yyx < yyxend; ++yyx)
- if (yycheck_[yyx + yyn] == yyx && yyx != yyterror_
- && !yy_table_value_is_error_ (yytable_[yyx + yyn]))
- {
- if (yycount == YYERROR_VERBOSE_ARGS_MAXIMUM)
- {
- yycount = 1;
- break;
- }
- else
- yyarg[yycount++] = yytname_[yyx];
- }
- }
- }
-
- char const* yyformat = YY_NULLPTR;
- switch (yycount)
- {
-#define YYCASE_(N, S) \
- case N: \
- yyformat = S; \
- break
- YYCASE_(0, YY_("syntax error"));
- YYCASE_(1, YY_("syntax error, unexpected %s"));
- YYCASE_(2, YY_("syntax error, unexpected %s, expecting %s"));
- YYCASE_(3, YY_("syntax error, unexpected %s, expecting %s or %s"));
- YYCASE_(4, YY_("syntax error, unexpected %s, expecting %s or %s or %s"));
- YYCASE_(5, YY_("syntax error, unexpected %s, expecting %s or %s or %s or %s"));
-#undef YYCASE_
- }
-
- // Argument number.
- size_t yyi = 0;
- for (char const* yyp = yyformat; *yyp; ++yyp)
- if (yyp[0] == '%' && yyp[1] == 's' && yyi < yycount)
- {
- yyres += yytnamerr_ (yyarg[yyi++]);
- ++yyp;
- }
- else
- yyres += *yyp;
- return yyres;
- }
-
-
- const signed char mlf_parser::yypact_ninf_ = -12;
-
- const signed char mlf_parser::yytable_ninf_ = -1;
-
- const signed char
- mlf_parser::yypact_[] =
- {
- -11, -12, -12, 4, 16, -12, 16, 16, 16, 16,
- -12, 16, -12, -12, 16, 29, -12, -12, -12, -12,
- -12, 6, 16, 16, 16, 16, -12, 33, 9, 14,
- -12
- };
-
- const unsigned char
- mlf_parser::yydefact_[] =
- {
- 0, 3, 4, 0, 0, 1, 0, 0, 0, 0,
- 14, 0, 15, 16, 0, 2, 9, 10, 11, 12,
- 13, 0, 0, 0, 0, 0, 17, 5, 6, 7,
- 8
- };
-
- const signed char
- mlf_parser::yypgoto_[] =
- {
- -12, -12, -12, -6
- };
-
- const signed char
- mlf_parser::yydefgoto_[] =
- {
- -1, 3, 4, 15
- };
-
- const signed char
- mlf_parser::yytable_[] =
- {
- 16, 17, 18, 19, 5, 20, 1, 2, 21, 22,
- 23, 24, 25, 23, 24, 25, 27, 28, 29, 30,
- 25, 0, 26, 6, 7, 8, 9, 10, 11, 12,
- 13, 14, 22, 23, 24, 25, -1, 23, 24, 25
- };
-
- const signed char
- mlf_parser::yycheck_[] =
- {
- 6, 7, 8, 9, 0, 11, 17, 18, 14, 3,
- 4, 5, 6, 4, 5, 6, 22, 23, 24, 25,
- 6, -1, 16, 7, 8, 9, 10, 11, 12, 13,
- 14, 15, 3, 4, 5, 6, 3, 4, 5, 6
- };
-
- const unsigned char
- mlf_parser::yystos_[] =
- {
- 0, 17, 18, 21, 22, 0, 7, 8, 9, 10,
- 11, 12, 13, 14, 15, 23, 23, 23, 23, 23,
- 23, 23, 3, 4, 5, 6, 16, 23, 23, 23,
- 23
- };
-
- const unsigned char
- mlf_parser::yyr1_[] =
- {
- 0, 20, 21, 22, 22, 23, 23, 23, 23, 23,
- 23, 23, 23, 23, 23, 23, 23, 23
- };
-
- const unsigned char
- mlf_parser::yyr2_[] =
- {
- 0, 2, 2, 1, 1, 3, 3, 3, 3, 2,
- 2, 2, 2, 2, 1, 1, 1, 3
- };
-
-
-
- // YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
- // First, the terminals, then, starting at \a yyntokens_, nonterminals.
- const char*
- const mlf_parser::yytname_[] =
- {
- "\"end of file\"", "error", "$undefined", "IFF", "IMP", "OR", "AND",
- "GMDIA", "GMBOX", "PMDIA", "PMBOX", "PVAR", "NOT", "TRUE", "FALSE",
- "LPAREN", "RPAREN", "GML", "PML", "\"identifier\"", "$accept", "input",
- "spec", "formula", YY_NULLPTR
- };
-
-#if YYDEBUG
- const unsigned char
- mlf_parser::yyrline_[] =
- {
- 0, 74, 74, 79, 80, 85, 86, 87, 88, 90,
- 91, 93, 94, 96, 97, 98, 99, 100
- };
-
- // Print the state stack on the debug stream.
- void
- mlf_parser::yystack_print_ ()
- {
- *yycdebug_ << "Stack now";
- for (stack_type::const_iterator
- i = yystack_.begin (),
- i_end = yystack_.end ();
- i != i_end; ++i)
- *yycdebug_ << ' ' << i->state;
- *yycdebug_ << std::endl;
- }
-
- // Report on the debug stream that the rule \a yyrule is going to be reduced.
- void
- mlf_parser::yy_reduce_print_ (int yyrule)
- {
- unsigned int yylno = yyrline_[yyrule];
- int yynrhs = yyr2_[yyrule];
- // Print the symbols being reduced, and their result.
- *yycdebug_ << "Reducing stack by rule " << yyrule - 1
- << " (line " << yylno << "):" << std::endl;
- // The symbols being reduced.
- for (int yyi = 0; yyi < yynrhs; yyi++)
- YY_SYMBOL_PRINT (" $" << yyi + 1 << " =",
- yystack_[(yynrhs) - (yyi + 1)]);
- }
-#endif // YYDEBUG
-
- // Symbol number corresponding to token number t.
- inline
- mlf_parser::token_number_type
- mlf_parser::yytranslate_ (int t)
- {
- static
- const token_number_type
- translate_table[] =
- {
- 0, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 2, 1, 2, 3, 4,
- 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
- 15, 16, 17, 18, 19
- };
- const unsigned int user_token_number_max_ = 274;
- const token_number_type undef_token_ = 2;
-
- if (static_cast<int>(t) <= yyeof_)
- return yyeof_;
- else if (static_cast<unsigned int> (t) <= user_token_number_max_)
- return translate_table[t];
- else
- return undef_token_;
- }
-
-
-} // yy
-#line 1138 "mlf-parser.tab.cc" // lalr1.cc:1155
-#line 102 "mlf-parser.yy" // lalr1.cc:1156
-
-
-
-void yy::mlf_parser::error (const yy::mlf_parser::location_type& l, const std::string& m){
- driver.error (l, m);
-}
-
-
-
-
diff --git a/src/lib/GMLMIP-0.1/parser/mlf-parser.tab.h b/src/lib/GMLMIP-0.1/parser/mlf-parser.tab.h
deleted file mode 100644
index 41d3982aed80a295f90793365496880014bef101..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/mlf-parser.tab.h
+++ /dev/null
@@ -1,497 +0,0 @@
-// A Bison parser, made by GNU Bison 3.0.2.
-
-// Skeleton interface for Bison LALR(1) parsers in C++
-
-// Copyright (C) 2002-2013 Free Software Foundation, Inc.
-
-// This program is free software: you can redistribute it and/or modify
-// it under the terms of the GNU General Public License as published by
-// the Free Software Foundation, either version 3 of the License, or
-// (at your option) any later version.
-
-// This program is distributed in the hope that it will be useful,
-// but WITHOUT ANY WARRANTY; without even the implied warranty of
-// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-// GNU General Public License for more details.
-
-// You should have received a copy of the GNU General Public License
-// along with this program. If not, see <http://www.gnu.org/licenses/>.
-
-// As a special exception, you may create a larger work that contains
-// part or all of the Bison parser skeleton and distribute that work
-// under terms of your choice, so long as that work isn't itself a
-// parser generator using the skeleton or a modified version thereof
-// as a parser skeleton. Alternatively, if you modify or redistribute
-// the parser skeleton itself, you may (at your option) remove this
-// special exception, which will cause the skeleton and the resulting
-// Bison output files to be licensed under the GNU General Public
-// License without this special exception.
-
-// This special exception was added by the Free Software Foundation in
-// version 2.2 of Bison.
-
-/**
- ** \file mlf-parser.tab.h
- ** Define the yy::parser class.
- */
-
-// C++ LALR(1) parser skeleton written by Akim Demaille.
-
-#ifndef YY_YY_MLF_PARSER_TAB_H_INCLUDED
-# define YY_YY_MLF_PARSER_TAB_H_INCLUDED
-// // "%code requires" blocks.
-#line 6 "mlf-parser.yy" // lalr1.cc:372
-
- #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;
-};
-
-#line 67 "mlf-parser.tab.h" // lalr1.cc:372
-
-
-# include <vector>
-# include <iostream>
-# include <stdexcept>
-# include <string>
-# include "stack.h"
-# include "location.h"
-
-
-#ifndef YY_ATTRIBUTE
-# if (defined __GNUC__ \
- && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \
- || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C
-# define YY_ATTRIBUTE(Spec) __attribute__(Spec)
-# else
-# define YY_ATTRIBUTE(Spec) /* empty */
-# endif
-#endif
-
-#ifndef YY_ATTRIBUTE_PURE
-# define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__))
-#endif
-
-#ifndef YY_ATTRIBUTE_UNUSED
-# define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__))
-#endif
-
-#if !defined _Noreturn \
- && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112)
-# if defined _MSC_VER && 1200 <= _MSC_VER
-# define _Noreturn __declspec (noreturn)
-# else
-# define _Noreturn YY_ATTRIBUTE ((__noreturn__))
-# endif
-#endif
-
-/* Suppress unused-variable warnings by "using" E. */
-#if ! defined lint || defined __GNUC__
-# define YYUSE(E) ((void) (E))
-#else
-# define YYUSE(E) /* empty */
-#endif
-
-#if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
-/* Suppress an incorrect diagnostic about yylval being uninitialized. */
-# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
- _Pragma ("GCC diagnostic push") \
- _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\
- _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
-# define YY_IGNORE_MAYBE_UNINITIALIZED_END \
- _Pragma ("GCC diagnostic pop")
-#else
-# define YY_INITIAL_VALUE(Value) Value
-#endif
-#ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
-# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
-# define YY_IGNORE_MAYBE_UNINITIALIZED_END
-#endif
-#ifndef YY_INITIAL_VALUE
-# define YY_INITIAL_VALUE(Value) /* Nothing. */
-#endif
-
-/* Debug traces. */
-#ifndef YYDEBUG
-# define YYDEBUG 1
-#endif
-
-
-namespace yy {
-#line 138 "mlf-parser.tab.h" // lalr1.cc:372
-
-
-
-
-
- /// A Bison parser.
- class mlf_parser
- {
- public:
-#ifndef YYSTYPE
- /// Symbol semantic values.
-
-#else
- typedef YYSTYPE semantic_type;
-#endif
- /// Symbol locations.
- typedef location location_type;
-
- /// Syntax errors thrown from user actions.
- struct syntax_error : std::runtime_error
- {
- syntax_error (const location_type& l, const std::string& m);
- location_type location;
- };
-
- /// Tokens.
- struct token
- {
- enum yytokentype
- {
- END = 0,
- IFF = 258,
- IMP = 259,
- OR = 260,
- AND = 261,
- GMDIA = 262,
- GMBOX = 263,
- PMDIA = 264,
- PMBOX = 265,
- PVAR = 266,
- NOT = 267,
- TRUE = 268,
- FALSE = 269,
- LPAREN = 270,
- RPAREN = 271,
- GML = 272,
- PML = 273
- };
- };
-
- /// (External) token type, as returned by yylex.
- typedef token::yytokentype token_type;
-
- /// Internal symbol number.
- typedef int symbol_number_type;
-
- /// Internal symbol number for tokens (subsumed by symbol_number_type).
- typedef unsigned char token_number_type;
-
- /// A complete symbol.
- ///
- /// Expects its Base type to provide access to the symbol type
- /// via type_get().
- ///
- /// Provide access to semantic value and location.
- template <typename Base>
- struct basic_symbol : Base
- {
- /// Alias to Base.
- typedef Base super_type;
-
- /// Default constructor.
- basic_symbol ();
-
- /// Copy constructor.
- basic_symbol (const basic_symbol& other);
-
- /// Constructor for valueless symbols.
- basic_symbol (typename Base::kind_type t,
- const location_type& l);
-
- /// Constructor for symbols with semantic value.
- basic_symbol (typename Base::kind_type t,
- const semantic_type& v,
- const location_type& l);
-
- ~basic_symbol ();
-
- /// Destructive move, \a s is emptied into this.
- void move (basic_symbol& s);
-
- /// The semantic value.
- semantic_type value;
-
- /// The location.
- location_type location;
-
- private:
- /// Assignment operator.
- basic_symbol& operator= (const basic_symbol& other);
- };
-
- /// Type access provider for token (enum) based symbols.
- struct by_type
- {
- /// Default constructor.
- by_type ();
-
- /// Copy constructor.
- by_type (const by_type& other);
-
- /// The symbol type as needed by the constructor.
- typedef token_type kind_type;
-
- /// Constructor from (external) token numbers.
- by_type (kind_type t);
-
- /// Steal the symbol type from \a that.
- void move (by_type& that);
-
- /// The (internal) type number (corresponding to \a type).
- /// -1 when this symbol is empty.
- symbol_number_type type_get () const;
-
- /// The token.
- token_type token () const;
-
- enum { empty = 0 };
-
- /// The symbol type.
- /// -1 when this symbol is empty.
- token_number_type type;
- };
-
- /// "External" symbols: returned by the scanner.
- typedef basic_symbol<by_type> symbol_type;
-
-
- /// Build a parser object.
- mlf_parser (mlf_driver& driver_yyarg);
- virtual ~mlf_parser ();
-
- /// Parse.
- /// \returns 0 iff parsing succeeded.
- virtual int parse ();
-
-#if YYDEBUG
- /// The current debugging stream.
- std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
- /// Set the current debugging stream.
- void set_debug_stream (std::ostream &);
-
- /// Type for debugging levels.
- typedef int debug_level_type;
- /// The current debugging level.
- debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
- /// Set the current debugging level.
- void set_debug_level (debug_level_type l);
-#endif
-
- /// Report a syntax error.
- /// \param loc where the syntax error is found.
- /// \param msg a description of the syntax error.
- virtual void error (const location_type& loc, const std::string& msg);
-
- /// Report a syntax error.
- void error (const syntax_error& err);
-
- private:
- /// This class is not copyable.
- mlf_parser (const mlf_parser&);
- mlf_parser& operator= (const mlf_parser&);
-
- /// State numbers.
- typedef int state_type;
-
- /// Generate an error message.
- /// \param yystate the state where the error occurred.
- /// \param yytoken the lookahead token type, or yyempty_.
- virtual std::string yysyntax_error_ (state_type yystate,
- symbol_number_type yytoken) const;
-
- /// Compute post-reduction state.
- /// \param yystate the current state
- /// \param yysym the nonterminal to push on the stack
- state_type yy_lr_goto_state_ (state_type yystate, int yysym);
-
- /// Whether the given \c yypact_ value indicates a defaulted state.
- /// \param yyvalue the value to check
- static bool yy_pact_value_is_default_ (int yyvalue);
-
- /// Whether the given \c yytable_ value indicates a syntax error.
- /// \param yyvalue the value to check
- static bool yy_table_value_is_error_ (int yyvalue);
-
- static const signed char yypact_ninf_;
- static const signed char yytable_ninf_;
-
- /// Convert a scanner token number \a t to a symbol number.
- static token_number_type yytranslate_ (int t);
-
- // Tables.
- // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
- // STATE-NUM.
- static const signed char yypact_[];
-
- // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
- // Performed when YYTABLE does not specify something else to do. Zero
- // means the default is an error.
- static const unsigned char yydefact_[];
-
- // YYPGOTO[NTERM-NUM].
- static const signed char yypgoto_[];
-
- // YYDEFGOTO[NTERM-NUM].
- static const signed char yydefgoto_[];
-
- // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
- // positive, shift that token. If negative, reduce the rule whose
- // number is the opposite. If YYTABLE_NINF, syntax error.
- static const signed char yytable_[];
-
- static const signed char yycheck_[];
-
- // YYSTOS[STATE-NUM] -- The (internal number of the) accessing
- // symbol of state STATE-NUM.
- static const unsigned char yystos_[];
-
- // YYR1[YYN] -- Symbol number of symbol that rule YYN derives.
- static const unsigned char yyr1_[];
-
- // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN.
- static const unsigned char yyr2_[];
-
-
- /// Convert the symbol name \a n to a form suitable for a diagnostic.
- static std::string yytnamerr_ (const char *n);
-
-
- /// For a symbol, its name in clear.
- static const char* const yytname_[];
-#if YYDEBUG
- // YYRLINE[YYN] -- Source line where rule number YYN was defined.
- static const unsigned char yyrline_[];
- /// Report on the debug stream that the rule \a r is going to be reduced.
- virtual void yy_reduce_print_ (int r);
- /// Print the state stack on the debug stream.
- virtual void yystack_print_ ();
-
- // Debugging.
- int yydebug_;
- std::ostream* yycdebug_;
-
- /// \brief Display a symbol type, value and location.
- /// \param yyo The output stream.
- /// \param yysym The symbol.
- template <typename Base>
- void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
-#endif
-
- /// \brief Reclaim the memory associated to a symbol.
- /// \param yymsg Why this token is reclaimed.
- /// If null, print nothing.
- /// \param yysym The symbol.
- template <typename Base>
- void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
-
- private:
- /// Type access provider for state based symbols.
- struct by_state
- {
- /// Default constructor.
- by_state ();
-
- /// The symbol type as needed by the constructor.
- typedef state_type kind_type;
-
- /// Constructor.
- by_state (kind_type s);
-
- /// Copy constructor.
- by_state (const by_state& other);
-
- /// Steal the symbol type from \a that.
- void move (by_state& that);
-
- /// The (internal) type number (corresponding to \a state).
- /// "empty" when empty.
- symbol_number_type type_get () const;
-
- enum { empty = 0 };
-
- /// The state.
- state_type state;
- };
-
- /// "Internal" symbol: element of the stack.
- struct stack_symbol_type : basic_symbol<by_state>
- {
- /// Superclass.
- typedef basic_symbol<by_state> super_type;
- /// Construct an empty symbol.
- stack_symbol_type ();
- /// Steal the contents from \a sym to build this.
- stack_symbol_type (state_type s, symbol_type& sym);
- /// Assignment, needed by push_back.
- stack_symbol_type& operator= (const stack_symbol_type& that);
- };
-
- /// Stack type.
- typedef stack<stack_symbol_type> stack_type;
-
- /// The stack.
- stack_type yystack_;
-
- /// Push a new state on the stack.
- /// \param m a debug message to display
- /// if null, no trace is output.
- /// \param s the symbol
- /// \warning the contents of \a s.value is stolen.
- void yypush_ (const char* m, stack_symbol_type& s);
-
- /// Push a new look ahead token on the state on the stack.
- /// \param m a debug message to display
- /// if null, no trace is output.
- /// \param s the state
- /// \param sym the symbol (for its value and location).
- /// \warning the contents of \a s.value is stolen.
- void yypush_ (const char* m, state_type s, symbol_type& sym);
-
- /// Pop \a n symbols the three stacks.
- void yypop_ (unsigned int n = 1);
-
- // Constants.
- enum
- {
- yyeof_ = 0,
- yylast_ = 39, ///< Last index in yytable_.
- yynnts_ = 4, ///< Number of nonterminal symbols.
- yyempty_ = -2,
- yyfinal_ = 5, ///< Termination state number.
- yyterror_ = 1,
- yyerrcode_ = 256,
- yyntokens_ = 20 ///< Number of tokens.
- };
-
-
- // User arguments.
- mlf_driver& driver;
- };
-
-
-
-} // yy
-#line 493 "mlf-parser.tab.h" // lalr1.cc:372
-
-
-
-
-#endif // !YY_YY_MLF_PARSER_TAB_H_INCLUDED
diff --git a/src/lib/GMLMIP-0.1/parser/mlf-parser.yy b/src/lib/GMLMIP-0.1/parser/mlf-parser.yy
deleted file mode 100644
index 8a2b9e0ac110a7e579510b2c7bf03bf664791968..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/mlf-parser.yy
+++ /dev/null
@@ -1,111 +0,0 @@
-%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/src/lib/GMLMIP-0.1/parser/mlf-scanner.ll b/src/lib/GMLMIP-0.1/parser/mlf-scanner.ll
deleted file mode 100644
index acdf0ada9818dd1a26f72cd2a4640d268cb4c19b..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/mlf-scanner.ll
+++ /dev/null
@@ -1,124 +0,0 @@
-%{
-# 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/src/lib/GMLMIP-0.1/parser/position.h b/src/lib/GMLMIP-0.1/parser/position.h
deleted file mode 100644
index 107d8e11d504fde109cf019002c302e09f51c15a..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/position.h
+++ /dev/null
@@ -1,180 +0,0 @@
-// A Bison parser, made by GNU Bison 3.0.2.
-
-// Positions for Bison parsers in C++
-
-// Copyright (C) 2002-2013 Free Software Foundation, Inc.
-
-// This program is free software: you can redistribute it and/or modify
-// it under the terms of the GNU General Public License as published by
-// the Free Software Foundation, either version 3 of the License, or
-// (at your option) any later version.
-
-// This program is distributed in the hope that it will be useful,
-// but WITHOUT ANY WARRANTY; without even the implied warranty of
-// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-// GNU General Public License for more details.
-
-// You should have received a copy of the GNU General Public License
-// along with this program. If not, see <http://www.gnu.org/licenses/>.
-
-// As a special exception, you may create a larger work that contains
-// part or all of the Bison parser skeleton and distribute that work
-// under terms of your choice, so long as that work isn't itself a
-// parser generator using the skeleton or a modified version thereof
-// as a parser skeleton. Alternatively, if you modify or redistribute
-// the parser skeleton itself, you may (at your option) remove this
-// special exception, which will cause the skeleton and the resulting
-// Bison output files to be licensed under the GNU General Public
-// License without this special exception.
-
-// This special exception was added by the Free Software Foundation in
-// version 2.2 of Bison.
-
-/**
- ** \file position.hh
- ** Define the yy::position class.
- */
-
-#ifndef YY_YY_POSITION_HH_INCLUDED
-# define YY_YY_POSITION_HH_INCLUDED
-
-# include <algorithm> // std::max
-# include <iostream>
-# include <string>
-
-# ifndef YY_NULLPTR
-# if defined __cplusplus && 201103L <= __cplusplus
-# define YY_NULLPTR nullptr
-# else
-# define YY_NULLPTR 0
-# endif
-# endif
-
-
-namespace yy {
-#line 56 "position.hh" // location.cc:291
- /// Abstract a position.
- class position
- {
- public:
- /// Construct a position.
- explicit position (std::string* f = YY_NULLPTR,
- unsigned int l = 1u,
- unsigned int c = 1u)
- : filename (f)
- , line (l)
- , column (c)
- {
- }
-
-
- /// Initialization.
- void initialize (std::string* fn = YY_NULLPTR,
- unsigned int l = 1u,
- unsigned int c = 1u)
- {
- filename = fn;
- line = l;
- column = c;
- }
-
- /** \name Line and Column related manipulators
- ** \{ */
- /// (line related) Advance to the COUNT next lines.
- void lines (int count = 1)
- {
- if (count)
- {
- column = 1u;
- line = add_ (line, count, 1);
- }
- }
-
- /// (column related) Advance to the COUNT next columns.
- void columns (int count = 1)
- {
- column = add_ (column, count, 1);
- }
- /** \} */
-
- /// File name to which this position refers.
- std::string* filename;
- /// Current line number.
- unsigned int line;
- /// Current column number.
- unsigned int column;
-
- private:
- /// Compute max(min, lhs+rhs) (provided min <= lhs).
- static unsigned int add_ (unsigned int lhs, int rhs, unsigned int min)
- {
- return (0 < rhs || -static_cast<unsigned int>(rhs) < lhs
- ? rhs + lhs
- : min);
- }
- };
-
- /// Add and assign a position.
- inline position&
- operator+= (position& res, int width)
- {
- res.columns (width);
- return res;
- }
-
- /// Add two position objects.
- inline position
- operator+ (position res, int width)
- {
- return res += width;
- }
-
- /// Add and assign a position.
- inline position&
- operator-= (position& res, int width)
- {
- return res += -width;
- }
-
- /// Add two position objects.
- inline position
- operator- (position res, int width)
- {
- return res -= width;
- }
-
- /// Compare two position objects.
- inline bool
- operator== (const position& pos1, const position& pos2)
- {
- return (pos1.line == pos2.line
- && pos1.column == pos2.column
- && (pos1.filename == pos2.filename
- || (pos1.filename && pos2.filename
- && *pos1.filename == *pos2.filename)));
- }
-
- /// Compare two position objects.
- inline bool
- operator!= (const position& pos1, const position& pos2)
- {
- return !(pos1 == pos2);
- }
-
- /** \brief Intercept output stream redirection.
- ** \param ostr the destination output stream
- ** \param pos a reference to the position to redirect
- */
- template <typename YYChar>
- inline std::basic_ostream<YYChar>&
- operator<< (std::basic_ostream<YYChar>& ostr, const position& pos)
- {
- if (pos.filename)
- ostr << *pos.filename << ':';
- return ostr << pos.line << '.' << pos.column;
- }
-
-
-} // yy
-#line 180 "position.hh" // location.cc:291
-#endif // !YY_YY_POSITION_HH_INCLUDED
diff --git a/src/lib/GMLMIP-0.1/parser/stack.h b/src/lib/GMLMIP-0.1/parser/stack.h
deleted file mode 100644
index 87d8f3ef36b53013ca6a34f86c8df53dbf57988d..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/stack.h
+++ /dev/null
@@ -1,158 +0,0 @@
-// A Bison parser, made by GNU Bison 3.0.2.
-
-// Stack handling for Bison parsers in C++
-
-// Copyright (C) 2002-2013 Free Software Foundation, Inc.
-
-// This program is free software: you can redistribute it and/or modify
-// it under the terms of the GNU General Public License as published by
-// the Free Software Foundation, either version 3 of the License, or
-// (at your option) any later version.
-
-// This program is distributed in the hope that it will be useful,
-// but WITHOUT ANY WARRANTY; without even the implied warranty of
-// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-// GNU General Public License for more details.
-
-// You should have received a copy of the GNU General Public License
-// along with this program. If not, see <http://www.gnu.org/licenses/>.
-
-// As a special exception, you may create a larger work that contains
-// part or all of the Bison parser skeleton and distribute that work
-// under terms of your choice, so long as that work isn't itself a
-// parser generator using the skeleton or a modified version thereof
-// as a parser skeleton. Alternatively, if you modify or redistribute
-// the parser skeleton itself, you may (at your option) remove this
-// special exception, which will cause the skeleton and the resulting
-// Bison output files to be licensed under the GNU General Public
-// License without this special exception.
-
-// This special exception was added by the Free Software Foundation in
-// version 2.2 of Bison.
-
-/**
- ** \file stack.hh
- ** Define the yy::stack class.
- */
-
-#ifndef YY_YY_STACK_HH_INCLUDED
-# define YY_YY_STACK_HH_INCLUDED
-
-# include <vector>
-
-
-namespace yy {
-#line 46 "stack.hh" // stack.hh:133
- template <class T, class S = std::vector<T> >
- class stack
- {
- public:
- // Hide our reversed order.
- typedef typename S::reverse_iterator iterator;
- typedef typename S::const_reverse_iterator const_iterator;
-
- stack ()
- : seq_ ()
- {
- }
-
- stack (unsigned int n)
- : seq_ (n)
- {
- }
-
- inline
- T&
- operator[] (unsigned int i)
- {
- return seq_[seq_.size () - 1 - i];
- }
-
- inline
- const T&
- operator[] (unsigned int i) const
- {
- return seq_[seq_.size () - 1 - i];
- }
-
- /// Steal the contents of \a t.
- ///
- /// Close to move-semantics.
- inline
- void
- push (T& t)
- {
- seq_.push_back (T());
- operator[](0).move (t);
- }
-
- inline
- void
- pop (unsigned int n = 1)
- {
- for (; n; --n)
- seq_.pop_back ();
- }
-
- void
- clear ()
- {
- seq_.clear ();
- }
-
- inline
- typename S::size_type
- size () const
- {
- return seq_.size ();
- }
-
- inline
- const_iterator
- begin () const
- {
- return seq_.rbegin ();
- }
-
- inline
- const_iterator
- end () const
- {
- return seq_.rend ();
- }
-
- private:
- stack (const stack&);
- stack& operator= (const stack&);
- /// The wrapped container.
- S seq_;
- };
-
- /// Present a slice of the top of a stack.
- template <class T, class S = stack<T> >
- class slice
- {
- public:
- slice (const S& stack, unsigned int range)
- : stack_ (stack)
- , range_ (range)
- {
- }
-
- inline
- const T&
- operator [] (unsigned int i) const
- {
- return stack_[range_ - i];
- }
-
- private:
- const S& stack_;
- unsigned int range_;
- };
-
-
-} // yy
-#line 157 "stack.hh" // stack.hh:133
-
-#endif // !YY_YY_STACK_HH_INCLUDED
diff --git a/src/lib/GMLMIP-0.1/parser/test.c b/src/lib/GMLMIP-0.1/parser/test.c
deleted file mode 100644
index 8679303fec8ae6a8b649ed03497cf3bb9ebdbbb1..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/parser/test.c
+++ /dev/null
@@ -1,16 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rand.pl b/src/lib/GMLMIP-0.1/rand.pl
deleted file mode 100644
index 7c54e91ab6ebc081793177af7c9d0cf85c517533..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rand.pl
+++ /dev/null
@@ -1,98 +0,0 @@
-#!/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/src/lib/GMLMIP-0.1/rules/GML_premise.c b/src/lib/GMLMIP-0.1/rules/GML_premise.c
deleted file mode 100644
index 3c24658f34a728b063637640d0803d839c97d59b..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/GML_premise.c
+++ /dev/null
@@ -1,251 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/GML_premise.h b/src/lib/GMLMIP-0.1/rules/GML_premise.h
deleted file mode 100644
index 513012f130819640d3b44b61669fdc1838940e71..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/GML_premise.h
+++ /dev/null
@@ -1,33 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/PML_premise.c b/src/lib/GMLMIP-0.1/rules/PML_premise.c
deleted file mode 100644
index 307c6fc838faf5f7a141a9abc90c1e8ab195bad0..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/PML_premise.c
+++ /dev/null
@@ -1,17 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/PML_premise.h b/src/lib/GMLMIP-0.1/rules/PML_premise.h
deleted file mode 100644
index acdf0c0b130b894eba9b7eaaa9b51de6786d465f..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/PML_premise.h
+++ /dev/null
@@ -1,26 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/makefile b/src/lib/GMLMIP-0.1/rules/makefile
deleted file mode 100644
index 0a1891feb73bb5e74bafd6ee30a3f57b26730c9a..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/makefile
+++ /dev/null
@@ -1,33 +0,0 @@
-include ../config.mk
-
-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/src/lib/GMLMIP-0.1/rules/node.c b/src/lib/GMLMIP-0.1/rules/node.c
deleted file mode 100644
index aac26a7e80961d7fe51d1ffa633d73140baa9029..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/node.c
+++ /dev/null
@@ -1,46 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/node.h b/src/lib/GMLMIP-0.1/rules/node.h
deleted file mode 100644
index 55d6ec751e26690116682bd7fb2166e95f55738b..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/node.h
+++ /dev/null
@@ -1,34 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/premise.c b/src/lib/GMLMIP-0.1/rules/premise.c
deleted file mode 100644
index 0db48b35c2422ac5f3e8bd4a9f6aa87c95e2cea9..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/premise.c
+++ /dev/null
@@ -1,110 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/premise.h b/src/lib/GMLMIP-0.1/rules/premise.h
deleted file mode 100644
index 5f2882f97c90efb6d3f629cc96b5f77b7db58987..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/premise.h
+++ /dev/null
@@ -1,76 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/radixtree.c b/src/lib/GMLMIP-0.1/rules/radixtree.c
deleted file mode 100644
index d639213da689bf66bab7a2371a6dac6e08a25213..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/radixtree.c
+++ /dev/null
@@ -1,55 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/radixtree.h b/src/lib/GMLMIP-0.1/rules/radixtree.h
deleted file mode 100644
index 08df3d109f32811971b3474746aa428488aa6e63..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/radixtree.h
+++ /dev/null
@@ -1,37 +0,0 @@
-#ifndef RADIXTREE_HH
-#define RADIXTREE_HH
-
-#include <cstdlib>
-#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/src/lib/GMLMIP-0.1/rules/setofconclusions.c b/src/lib/GMLMIP-0.1/rules/setofconclusions.c
deleted file mode 100644
index d85e192ae8a90c5b66360fa12510c1488046bbbd..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/setofconclusions.c
+++ /dev/null
@@ -1,35 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/setofconclusions.h b/src/lib/GMLMIP-0.1/rules/setofconclusions.h
deleted file mode 100644
index 5a7d2af65ab905a103eb9fd73876f37bbc484820..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/setofconclusions.h
+++ /dev/null
@@ -1,38 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/sizefunctions.c b/src/lib/GMLMIP-0.1/rules/sizefunctions.c
deleted file mode 100644
index bf15efc06a19956459ab276fbb54f5116f25e050..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/sizefunctions.c
+++ /dev/null
@@ -1,26 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/sizefunctions.h b/src/lib/GMLMIP-0.1/rules/sizefunctions.h
deleted file mode 100644
index 3210fac31728660460995908e2e4ccfb7f54bd47..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/sizefunctions.h
+++ /dev/null
@@ -1,11 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/test.c b/src/lib/GMLMIP-0.1/rules/test.c
deleted file mode 100644
index 4a48ce38ba2d09bac4da90c892cf99acb8bd0c30..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/test.c
+++ /dev/null
@@ -1,60 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/valuation.c b/src/lib/GMLMIP-0.1/rules/valuation.c
deleted file mode 100644
index 9bf0ed43cf9f5964e74d6126a6864faf801a0eda..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/valuation.c
+++ /dev/null
@@ -1,71 +0,0 @@
-#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/src/lib/GMLMIP-0.1/rules/valuation.h b/src/lib/GMLMIP-0.1/rules/valuation.h
deleted file mode 100644
index 7f303b0c559a6eed0535e797844a097bf2c9f011..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/rules/valuation.h
+++ /dev/null
@@ -1,34 +0,0 @@
-#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/src/lib/GMLMIP-0.1/satisfyingstack.h b/src/lib/GMLMIP-0.1/satisfyingstack.h
deleted file mode 100644
index 97021dd69a4a70723cfffa6da8a0c0f86cc4e761..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/satisfyingstack.h
+++ /dev/null
@@ -1,12 +0,0 @@
-#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/src/lib/GMLMIP-0.1/timeoutwrapper.sh b/src/lib/GMLMIP-0.1/timeoutwrapper.sh
deleted file mode 100755
index 5c19d2ec9fb1070ee9ddaf5a7af19d83acf64297..0000000000000000000000000000000000000000
--- a/src/lib/GMLMIP-0.1/timeoutwrapper.sh
+++ /dev/null
@@ -1,91 +0,0 @@
-#!/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/src/lib/gmlmip.ml b/src/lib/gmlmip.ml
deleted file mode 100644
index 9300917bf00dd2e8673326466d1bd4e2b7701e2a..0000000000000000000000000000000000000000
--- a/src/lib/gmlmip.ml
+++ /dev/null
@@ -1,8 +0,0 @@
-
-
-(* transforms list of gml formulas (diamond?,number,formula)
- to list of consequences (positive?,formula),
- here positive? means that the formula must be true in order to make the
- given conjunct of modalities true *)
-external gml_rules : (bool*int*int) list -> (int*bool) list list list = "gmlRules_stub"
-external pml_rules : (bool*int*int*int) list -> (int*bool) list list list = "pmlRules_stub"
diff --git a/src/lib/gmlmip.mli b/src/lib/gmlmip.mli
deleted file mode 100644
index 0a4c5535ac1ddfd62fd91f0739eba9ec2ba10a5c..0000000000000000000000000000000000000000
--- a/src/lib/gmlmip.mli
+++ /dev/null
@@ -1,10 +0,0 @@
-(* transforms list of gml formulas (diamond?,number,formula)
- to list of consequences (formula,positive?),
- here positive? means that the formula must be true in order to make the
- given conjunct of modalities true *)
-val gml_rules : (bool*int*int) list -> (int*bool) list list list
-(* transforms list of pml formulas (diamond?,nominator,denominator,formula)
- to list of consequences (formula,positive?),
- here positive? means that the formula must be true in order to make the
- given conjunct of modalities true *)
-val pml_rules : (bool*int*int*int) list -> (int*bool) list list list
diff --git a/src/lib/gmlmip_stub.c b/src/lib/gmlmip_stub.c
deleted file mode 100644
index 996f38ed19c2faacd7a68cee3baf908be31aa3c1..0000000000000000000000000000000000000000
--- a/src/lib/gmlmip_stub.c
+++ /dev/null
@@ -1,130 +0,0 @@
-#define __STDC_LIMIT_MACROS
-#define __STDC_FORMAT_MACROS
-
-#include <utility> // for pair
-#include <vector>
-#include <set>
-
-extern "C" {
- #include <caml/mlvalues.h>
- #include <caml/alloc.h>
- #include <caml/memory.h>
- #include <caml/custom.h>
-}
-
-#include "GMLMIP-0.1/onestep.h"
-
-//
-using namespace std;
-
-extern "C" {
- CAMLprim value gmlRules_stub(value modalities);
- CAMLprim value pmlRules_stub(value modalities);
-}
-
-template<class T>
-value set2CamlList(const set<T>& vec, value (*f)(const T&)) {
- CAMLparam0();
- CAMLlocal2( cli, cons );
- cli = Val_emptylist;
-
- for (typename set<T>::const_reverse_iterator it = vec.rbegin();
- it != vec.rend();
- ++it)
- {
- cons = caml_alloc(2, 0);
-
- Store_field( cons, 0, f(*it) ); // head
- Store_field( cons, 1, cli ); // tail
-
- cli = cons;
- }
-
- return cli ;
-}
-
-
-
-static CAMLprim value pair2caml(const int& t) {
- CAMLparam0();
- CAMLlocal1( abc );
- abc = caml_alloc(2, 0);
- bool neg = t < 0;
- Store_field( abc, 0, Val_int((neg ?(-t) : t) - 1));
- Store_field( abc, 1, Val_bool(!neg));
- return abc;
-}
-
-static CAMLprim value set2caml(const set<int>& vt) {
- return set2CamlList(vt, pair2caml);
-}
-
-static CAMLprim value setset2caml(const set<set<int> >& vt) {
- return set2CamlList(vt, set2caml);
-}
-
-static void printModVec(FILE* f, const vector<pair<pair<bool,int>,int> >& modvec) {
- fprintf(f, "GML-Input: /\\ (");
- for (int i = 0; i < modvec.size(); i++) {
- bool isdia = modvec[i].first.first;
- int cnt = modvec[i].first.second;
- int underl = modvec[i].second;
- if (i > 0) fprintf(f, ",");
- if (isdia) {
- fprintf(f, " <%d> p%d", cnt, underl);
- } else {
- fprintf(f, " [%d] p%d", cnt, underl);
- }
- }
- fprintf(f, " )\n");
-}
-
-CAMLprim value gmlRules_stub(value modalities) {
- // parse caml-modalities to a C++ vector
- CAMLparam1( modalities );
- value block = modalities;
- vector<pair<pair<bool,int>,int> > modvec;
- while (Is_block(block)) {
- CAMLlocal3( vpos, vcnt, vformula );
- vpos = Field(Field(block, 0), 0);
- vcnt = Field(Field(block, 0), 1);
- vformula = Field(Field(block, 0), 2);
- modvec.push_back(make_pair(make_pair(
- Bool_val(vpos),
- Int_val(vcnt)),
- 1+Int_val(vformula)));
- block = Field(block, 1);
- }
- // Do one rule step and save result in rulevec
- GMLConclusion rulevec = gmlmip_onestep_gml(modvec);
- // convert rulevec into ocaml list of pairs
- CAMLlocal1( res );
- res = set2CamlList(rulevec, setset2caml);
- CAMLreturn( res );
-}
-
-CAMLprim value pmlRules_stub(value modalities) {
- // parse caml-modalities to a C++ vector
- CAMLparam1( modalities );
- value block = modalities;
- vector<pair<pair<bool,pair<int,int> >,int> > modvec;
- while (Is_block(block)) {
- CAMLlocal4( vpos, vnom, vdenom, vformula );
- vpos = Field(Field(block, 0), 0);
- vnom = Field(Field(block, 0), 1);
- vdenom = Field(Field(block, 0), 2);
- vformula = Field(Field(block, 0), 3);
- modvec.push_back(make_pair(make_pair(
- Bool_val(vpos),
- make_pair(Int_val(vnom),Int_val(vdenom))),
- 1+Int_val(vformula)));
- block = Field(block, 1);
- }
- // Do one rule step and save result in rulevec
- GMLConclusion rulevec = gmlmip_onestep_pml(modvec);
- // convert rulevec into ocaml list of pairs
- CAMLlocal1( res );
- res = set2CamlList(rulevec, setset2caml);
- CAMLreturn( res );
-}
-