Project

General

Profile

Revision 1d36cd07

View differences:

src/coalg/coalg.ml
170 170
      done
171 171
    with End_of_file -> ()
172 172

  
173
let choiceApprox opts =
174
  let verb = opts.verbose in
175
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
176
    let printRes sat =
177
      if not verb then
178
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
179
      else ()
180
    in
181
    try
182
      while true do
183
        let input = read_line () in
184
        if not (GenAndComp.isEmptyString input) then
185
          let (s, fo) = CoAlgFormula.importSortedFormula input in
186
          let (tbox, fu) = CoAlgFormula.importQuery input in
187
          let g = Nom2fix.translate fo nomTable sorts s true in
188
          let f = Nom2fix.delFix g in
189
          let str = CoAlgFormula.exportFormula f in
190
          incr counter;
191
          print_string("\nFormula " ^ (string_of_int !counter) ^ ": ");
192
          printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
193
          flush stdout;
194
        else ()
195
      done
196
    with End_of_file -> ()
197

  
173 198
let choiceNom2fixNonOpt opts =
174 199
  let verb = opts.verbose in
175 200
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
......
325 350
       | "nom2fixN" -> choiceNom2fixNonOpt opts
326 351
       | "solveNom" -> choiceSolveNom opts
327 352
       | "solveNomN" -> choiceSolveNomNonOpt opts
353
       | "approx" -> choiceApprox opts
328 354
       | _ -> printUsage (Sys.argv.(0))
329 355

  
330 356
(* vim: set et sw=2 sts=2 ts=8 : *)
src/lib/CoAlgFormula.ml
135 135
 *)
136 136
let sizeSortedFormula f = sizeFormula (snd f)
137 137

  
138
let depthFormula form = 
139
  let rec depth f =
140
    match f with
141
      | TRUE
142
      | FALSE
143
      | AP _ -> 0
144
      | NOT f1
145
      | AT (_, f1) -> (depth f1)
146
      | OR (f1, f2)
147
      | AND (f1, f2)
148
      | EQU (f1, f2)
149
      | IMP (f1, f2) -> (max (depth f1)(depth f2))
150
      | EX (_, f1)
151
      | AX (_, f1)
152
      | ENFORCES (_, f1)
153
      | ALLOWS (_, f1) -> succ ((depth f1))
154
      | MIN (_, _, f1)
155
      | MAX (_, _, f1)
156
      | ATLEASTPROB (_, f1)
157
      | LESSPROBFAIL (_, f1)
158
      | MORETHAN (_, _, f1)
159
      | MAXEXCEPT (_, _, f1) -> succ ((depth f1))
160
      | ID (f1) -> succ ((depth f1))
161
      | NORM(f1, f2)
162
      | NORMN(f1, f2) -> succ ((max (depth f1) (depth f2))) 
163
      | CONST _
164
      | CONSTN _ -> 1
165
      | CHC (f1, f2) -> succ ((max (depth f1) (depth f2))) 
166
      | FUS (_, f1) -> succ (depth f1)
167
      | MU (_, f1)
168
      | NU (_, f1) -> depth f1
169
      | VAR _ -> 0
170
  in
171
  depth form
172

  
138 173

  
139 174
(* think of func: (formula -> unit) -> formula -> unit as identity.
140 175
  iterate over all subformulae and collect side effects. *)
src/lib/CoAlgFormula.mli
69 69

  
70 70
val sizeFormula : formula -> int
71 71
val sizeSortedFormula : sortedFormula -> int
72
val depthFormula : formula -> int
72 73

  
73 74
val string_of_formula : formula -> string
74 75
val exportFormula : formula -> string
src/lib/Nom2fix.ml
94 94

  
95 95
  !ret
96 96

  
97
let delFix foo =
98
let rec selFixpoints fo =
99
  let n = CoAlgFormula.depthFormula fo in
100
  match fo with 
101
    | CoAlgFormula.FALSE -> CoAlgFormula.FALSE
102
    | CoAlgFormula.TRUE -> CoAlgFormula.TRUE
103
    | CoAlgFormula.AP s -> CoAlgFormula.AP s
104
    | CoAlgFormula.NOT f -> CoAlgFormula.NOT (selFixpoints f)
105
    | CoAlgFormula.OR (f1, f2) -> CoAlgFormula.OR ((selFixpoints f1), (selFixpoints f2))
106
    | CoAlgFormula.AND (f1, f2) -> CoAlgFormula.AND ((selFixpoints f1), (selFixpoints f2))
107
    | CoAlgFormula.EQU (f1, f2) -> CoAlgFormula.EQU ((selFixpoints f1), (selFixpoints f2))
108
    | CoAlgFormula.IMP (f1, f2) -> CoAlgFormula.IMP ((selFixpoints f1), (selFixpoints f2))
109
    | CoAlgFormula.EX (s, f) -> CoAlgFormula.EX (s, (selFixpoints f))
110
    | CoAlgFormula.AX (s, f) -> CoAlgFormula.AX (s, (selFixpoints f))
111
    | CoAlgFormula.ENFORCES (l, f) -> CoAlgFormula.ENFORCES(l, (selFixpoints f))
112
    | CoAlgFormula.ALLOWS (l, f) -> CoAlgFormula.ALLOWS(l, (selFixpoints f))
113
    | CoAlgFormula.MIN (i, s, f) -> CoAlgFormula.MIN(i, s, (selFixpoints f))
114
    | CoAlgFormula.MAX (i, s, f) -> CoAlgFormula.MAX(i, s, (selFixpoints f))
115
    | CoAlgFormula.MORETHAN (i, s, f) -> CoAlgFormula.MORETHAN(i, s, (selFixpoints f))
116
    | CoAlgFormula.MAXEXCEPT (i, s, f) -> CoAlgFormula.MAXEXCEPT(i, s, (selFixpoints f))
117
    | CoAlgFormula.ATLEASTPROB (r, f) -> CoAlgFormula.ATLEASTPROB(r, (selFixpoints f))
118
    | CoAlgFormula.LESSPROBFAIL (r, f) -> CoAlgFormula.LESSPROBFAIL (r, (selFixpoints f))
119
    | CoAlgFormula.ID f -> CoAlgFormula.ID (selFixpoints f)
120
    | CoAlgFormula.MU (s, f) -> 
121
        let ret = ref CoAlgFormula.FALSE in
122
        for i = 1 to n+1 do
123
          ret := CoAlgFormula.OR(f, EX("",!ret));
124
        done;
125
        !ret
126
    | CoAlgFormula.NU (s, f) -> 
127
        let ret = ref CoAlgFormula.TRUE in
128
        for i = 1 to n+1 do
129
          ret := CoAlgFormula.AND(f, AX("",!ret));
130
        done;
131
        !ret
132
    | CoAlgFormula.AF f -> CoAlgFormula.AF (selFixpoints f)
133
    | CoAlgFormula.EF f -> CoAlgFormula.EF (selFixpoints f)
134
    | CoAlgFormula.AG f -> CoAlgFormula.AG (selFixpoints f)
135
    | CoAlgFormula.EG f -> CoAlgFormula.EG (selFixpoints f)
136
    | CoAlgFormula.VAR s -> CoAlgFormula.VAR s
137
in
138
selFixpoints foo
139

  
97 140

  
98 141
let calcinv f noms nomTbl sorts s =
99 142
  (*calc flc*)
src/lib/Nom2fix.mli
2 2

  
3 3
type nomTbl = string -> CoAlgFormula.sort option
4 4

  
5

  
5 6
val rename : CoAlgFormula.formula -> string Map.Make(String).t ref -> string list ref ->  CoAlgFormula.formula
7
val delFix : CoAlgFormula.formula -> CoAlgFormula.formula
6 8
val calcinv : CoAlgFormula.formula -> string list ref -> (string -> int option) -> CoAlgReasoner.sortTable -> int -> CoAlgFormula.formula
7 9
val translate : CoAlgFormula.formula -> (string -> int option) -> CoAlgReasoner.sortTable -> int -> bool ->  CoAlgFormula.formula
8 10

  

Also available in: Unified diff