Project

General

Profile

Revision 946e8213

View differences:

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

  
173 173
let choiceNom2fix opts =
174
  let verb = opts.verbose in
174 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
175 181
  (*CoAlgMisc.sortTable = ref sorts;*)
176 182
  try
177 183
    while true do
178 184
      let input = read_line () in
179 185
      if not (GenAndComp.isEmptyString input) then
180
        let f = CoAlgFormula.importFormula input in
181
        (*let g = EAFormula.nom2EA f nomTable sorts in*)
182
        (*let str = EAFormula.exportFormula g in*)
183
        let g = Nom2fix.translate f nomTable sorts in
186
        let (s, f) = CoAlgFormula.importSortedFormula input in
187
        let (tbox, fu) = CoAlgFormula.importQuery input in
188
        let g = Nom2fix.translate f nomTable sorts s in
184 189
        let str = CoAlgFormula.exportFormula g in
185 190
        incr counter;
186 191
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
192
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
187 193
        flush stdout;
188 194
      else ()
189 195
    done
src/lib/CoAlgFormula.mli
63 63
val convert_post : (formula -> formula) -> formula -> formula (* run over all subformulas in post order *)
64 64
val convertToK : formula -> formula (* tries to convert a formula to a pure K formula *)
65 65
val convertToGML : formula -> formula (* tries to convert a formula to a pure GML formula *)
66
val convertToMu : formula -> formula (* tries to convert a formula to a pure Mu formula *)
66 67

  
67 68
val isNominal : string -> bool
68 69

  
src/lib/Nom2fix.ml
44 44

  
45 45
  !ret
46 46

  
47
let calcinv f noms nomTbl sorts =
47
let calcinv f noms nomTbl sorts s =
48 48
  (*calc flc*)
49 49
  let card = Array.length sorts in
50 50
  let hcF = CoAlgFormula.HcFormula.create true in
......
52 52
  let vset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
53 53
  let atset = CoAlgFormula.HcFHt.create 64 in
54 54
  let nomset = Hashtbl.create 16 in
55
  let (s, fo) = CoAlgFormula.importSortedFormula (CoAlgFormula.exportFormula f) in
56 55

  
57 56
  let hcform = CoAlgFormula.hc_formula hcF f in
58 57

  
......
78 77

  
79 78
  !ret
80 79

  
81
let translate f nomTbl sorts =
80
let translate fu nomTbl sorts s =
81
  let f = (CA.nnf fu) in
82

  
82 83
  (*list of nominals*)
83 84
  let noms = ref [] in
84 85
  (*mapping from nominals to new syms*)
85 86
  let nomsub = ref StringMap.empty in
86 87

  
87
  print_endline (CA.exportFormula f);
88

  
89 88
  (*first rename nominals then change type to eaformula*)
90 89
  let ren = rename f nomsub noms in
91
  print_string "rename: ";
90
  print_string "using Formula: ";
92 91
  print_endline (CA.exportFormula ren);
93 92

  
94 93
  (*first calculate flc then rename nominals*)
95
  let invhelp = calcinv f noms nomTbl sorts in
96
  print_string "invhelp: ";
97
  print_endline (CoAlgFormula.exportFormula invhelp);
94
  let invhelp = calcinv f noms nomTbl sorts s in
95
  (*print_string "invhelp: ";
96
  print_endline (CoAlgFormula.exportFormula invhelp);*)
98 97

  
99 98
  let inv = rename invhelp nomsub noms in
100
  print_string "inv: ";
101
  print_endline (CoAlgFormula.exportFormula inv);
99
  (*print_string "inv: ";
100
  print_endline (CoAlgFormula.exportFormula inv);*)
102 101

  
103 102
  let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in
103
  let ret = CA.convertToMu formula in
104 104
 
105
  formula
105
  ret
106 106

  
107 107
(* vim: set et sw=2 sts=2 ts=8 : *)
src/lib/Nom2fix.mli
2 2

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

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

  
10 10
(* vim: set et sw=2 sts=2 ts=8 : *)

Also available in: Unified diff