From c4aee9225d36d4c2b7822a92533d35a4b48e80c9 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Thu, 16 Mar 2017 16:51:43 +0100
Subject: [PATCH] Remove GMLMIP
This drops the rule implementation for GML and PML, because they were
relying on GMLMIP which complicated the build process and didn't work
completely. See Issue 19.
GML and PML are still implemented as functors but currently disabled.
To re-instantiate them, an OCaml implementation is needed.
---
_oasis | 43 +-
src/coalg/coalg.ml | 8 +-
src/lib/CoAlgLogics.ml | 98 +-
src/lib/GMLMIP-0.1/.gitignore | 2 -
src/lib/GMLMIP-0.1/README.txt | 79 -
src/lib/GMLMIP-0.1/config.mk | 7 -
src/lib/GMLMIP-0.1/formulas/GML_formula.c | 80 -
src/lib/GMLMIP-0.1/formulas/GML_formula.h | 14 -
src/lib/GMLMIP-0.1/formulas/PML_formula.c | 102 -
src/lib/GMLMIP-0.1/formulas/PML_formula.h | 14 -
src/lib/GMLMIP-0.1/formulas/formula.c | 324 ---
src/lib/GMLMIP-0.1/formulas/formula.h | 168 --
src/lib/GMLMIP-0.1/formulas/makefile | 21 -
src/lib/GMLMIP-0.1/formulas/rational.c | 29 -
src/lib/GMLMIP-0.1/formulas/rational.h | 26 -
.../formulas/satisfyingassignment.c | 64 -
.../formulas/satisfyingassignment.h | 26 -
src/lib/GMLMIP-0.1/input | 2 -
src/lib/GMLMIP-0.1/main.c | 70 -
src/lib/GMLMIP-0.1/makefile | 51 -
src/lib/GMLMIP-0.1/onestep-example.c | 68 -
src/lib/GMLMIP-0.1/onestep.c | 143 --
src/lib/GMLMIP-0.1/onestep.h | 33 -
src/lib/GMLMIP-0.1/parser/lex.yy.c | 2233 -----------------
src/lib/GMLMIP-0.1/parser/lex.yy.h | 432 ----
src/lib/GMLMIP-0.1/parser/location.h | 187 --
src/lib/GMLMIP-0.1/parser/makefile | 36 -
src/lib/GMLMIP-0.1/parser/mlf-driver.c | 60 -
src/lib/GMLMIP-0.1/parser/mlf-driver.h | 62 -
src/lib/GMLMIP-0.1/parser/mlf-parser.tab.c | 1148 ---------
src/lib/GMLMIP-0.1/parser/mlf-parser.tab.h | 497 ----
src/lib/GMLMIP-0.1/parser/mlf-parser.yy | 111 -
src/lib/GMLMIP-0.1/parser/mlf-scanner.ll | 124 -
src/lib/GMLMIP-0.1/parser/position.h | 180 --
src/lib/GMLMIP-0.1/parser/stack.h | 158 --
src/lib/GMLMIP-0.1/parser/test.c | 16 -
src/lib/GMLMIP-0.1/rand.pl | 98 -
src/lib/GMLMIP-0.1/rules/GML_premise.c | 251 --
src/lib/GMLMIP-0.1/rules/GML_premise.h | 33 -
src/lib/GMLMIP-0.1/rules/PML_premise.c | 17 -
src/lib/GMLMIP-0.1/rules/PML_premise.h | 26 -
src/lib/GMLMIP-0.1/rules/makefile | 33 -
src/lib/GMLMIP-0.1/rules/node.c | 46 -
src/lib/GMLMIP-0.1/rules/node.h | 34 -
src/lib/GMLMIP-0.1/rules/premise.c | 110 -
src/lib/GMLMIP-0.1/rules/premise.h | 76 -
src/lib/GMLMIP-0.1/rules/radixtree.c | 55 -
src/lib/GMLMIP-0.1/rules/radixtree.h | 37 -
src/lib/GMLMIP-0.1/rules/setofconclusions.c | 35 -
src/lib/GMLMIP-0.1/rules/setofconclusions.h | 38 -
src/lib/GMLMIP-0.1/rules/sizefunctions.c | 26 -
src/lib/GMLMIP-0.1/rules/sizefunctions.h | 11 -
src/lib/GMLMIP-0.1/rules/test.c | 60 -
src/lib/GMLMIP-0.1/rules/valuation.c | 71 -
src/lib/GMLMIP-0.1/rules/valuation.h | 34 -
src/lib/GMLMIP-0.1/satisfyingstack.h | 12 -
src/lib/GMLMIP-0.1/timeoutwrapper.sh | 91 -
src/lib/gmlmip.ml | 8 -
src/lib/gmlmip.mli | 10 -
src/lib/gmlmip_stub.c | 130 -
60 files changed, 13 insertions(+), 8045 deletions(-)
delete mode 100644 src/lib/GMLMIP-0.1/.gitignore
delete mode 100644 src/lib/GMLMIP-0.1/README.txt
delete mode 100644 src/lib/GMLMIP-0.1/config.mk
delete mode 100644 src/lib/GMLMIP-0.1/formulas/GML_formula.c
delete mode 100644 src/lib/GMLMIP-0.1/formulas/GML_formula.h
delete mode 100644 src/lib/GMLMIP-0.1/formulas/PML_formula.c
delete mode 100644 src/lib/GMLMIP-0.1/formulas/PML_formula.h
delete mode 100644 src/lib/GMLMIP-0.1/formulas/formula.c
delete mode 100644 src/lib/GMLMIP-0.1/formulas/formula.h
delete mode 100644 src/lib/GMLMIP-0.1/formulas/makefile
delete mode 100644 src/lib/GMLMIP-0.1/formulas/rational.c
delete mode 100644 src/lib/GMLMIP-0.1/formulas/rational.h
delete mode 100644 src/lib/GMLMIP-0.1/formulas/satisfyingassignment.c
delete mode 100644 src/lib/GMLMIP-0.1/formulas/satisfyingassignment.h
delete mode 100644 src/lib/GMLMIP-0.1/input
delete mode 100644 src/lib/GMLMIP-0.1/main.c
delete mode 100644 src/lib/GMLMIP-0.1/makefile
delete mode 100644 src/lib/GMLMIP-0.1/onestep-example.c
delete mode 100644 src/lib/GMLMIP-0.1/onestep.c
delete mode 100644 src/lib/GMLMIP-0.1/onestep.h
delete mode 100644 src/lib/GMLMIP-0.1/parser/lex.yy.c
delete mode 100644 src/lib/GMLMIP-0.1/parser/lex.yy.h
delete mode 100644 src/lib/GMLMIP-0.1/parser/location.h
delete mode 100644 src/lib/GMLMIP-0.1/parser/makefile
delete mode 100644 src/lib/GMLMIP-0.1/parser/mlf-driver.c
delete mode 100644 src/lib/GMLMIP-0.1/parser/mlf-driver.h
delete mode 100644 src/lib/GMLMIP-0.1/parser/mlf-parser.tab.c
delete mode 100644 src/lib/GMLMIP-0.1/parser/mlf-parser.tab.h
delete mode 100644 src/lib/GMLMIP-0.1/parser/mlf-parser.yy
delete mode 100644 src/lib/GMLMIP-0.1/parser/mlf-scanner.ll
delete mode 100644 src/lib/GMLMIP-0.1/parser/position.h
delete mode 100644 src/lib/GMLMIP-0.1/parser/stack.h
delete mode 100644 src/lib/GMLMIP-0.1/parser/test.c
delete mode 100644 src/lib/GMLMIP-0.1/rand.pl
delete mode 100644 src/lib/GMLMIP-0.1/rules/GML_premise.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/GML_premise.h
delete mode 100644 src/lib/GMLMIP-0.1/rules/PML_premise.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/PML_premise.h
delete mode 100644 src/lib/GMLMIP-0.1/rules/makefile
delete mode 100644 src/lib/GMLMIP-0.1/rules/node.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/node.h
delete mode 100644 src/lib/GMLMIP-0.1/rules/premise.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/premise.h
delete mode 100644 src/lib/GMLMIP-0.1/rules/radixtree.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/radixtree.h
delete mode 100644 src/lib/GMLMIP-0.1/rules/setofconclusions.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/setofconclusions.h
delete mode 100644 src/lib/GMLMIP-0.1/rules/sizefunctions.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/sizefunctions.h
delete mode 100644 src/lib/GMLMIP-0.1/rules/test.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/valuation.c
delete mode 100644 src/lib/GMLMIP-0.1/rules/valuation.h
delete mode 100644 src/lib/GMLMIP-0.1/satisfyingstack.h
delete mode 100755 src/lib/GMLMIP-0.1/timeoutwrapper.sh
delete mode 100644 src/lib/gmlmip.ml
delete mode 100644 src/lib/gmlmip.mli
delete mode 100644 src/lib/gmlmip_stub.c
diff --git a/_oasis b/_oasis
index 707258a..f68d16d 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 30f4ec3..2bfbf20 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 fd46280..4b89965 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 bc7e2fd..0000000
--- 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 f31b51f..0000000
--- 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 9b5d1ab..0000000
--- 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 1fc45b4..0000000
--- 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 a24a13b..0000000
--- 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 c4c04ab..0000000
--- 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 8e04b3f..0000000
--- 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 06bd40c..0000000
--- 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 e7a50c4..0000000
--- 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 f2465b1..0000000
--- 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 a0b5a10..0000000
--- 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 2e41dd4..0000000
--- 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 3f9b1b0..0000000
--- 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 7ad5565..0000000
--- 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 66bbf4f..0000000
--- 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 219c055..0000000
--- 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 934e0e7..0000000
--- 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 3283733..0000000
--- 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 ddc0e8b..0000000
--- 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 efefbe0..0000000
--- 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 f5d55a4..0000000
--- 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 ed75b0e..0000000
--- 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 7c05741..0000000
--- 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 041bff3..0000000
--- 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 09279c6..0000000
--- 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 2c6666c..0000000
--- 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 d3c4317..0000000
--- 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 41d3982..0000000
--- 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 8a2b9e0..0000000
--- 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 acdf0ad..0000000
--- 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 107d8e1..0000000
--- 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 87d8f3e..0000000
--- 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 8679303..0000000
--- 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 7c54e91..0000000
--- 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 3c24658..0000000
--- 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 513012f..0000000
--- 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 307c6fc..0000000
--- 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 acdf0c0..0000000
--- 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 0a1891f..0000000
--- 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 aac26a7..0000000
--- 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 55d6ec7..0000000
--- 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 0db48b3..0000000
--- 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 5f2882f..0000000
--- 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 d639213..0000000
--- 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 08df3d1..0000000
--- 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 d85e192..0000000
--- 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 5a7d2af..0000000
--- 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 bf15efc..0000000
--- 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 3210fac..0000000
--- 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 4a48ce3..0000000
--- 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 9bf0ed4..0000000
--- 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 7f303b0..0000000
--- 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 97021dd..0000000
--- 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 5c19d2e..0000000
--- 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 9300917..0000000
--- 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 0a4c553..0000000
--- 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 996f38e..0000000
--- 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 );
-}
-
--
GitLab