Project

General

Profile

Revision bc0691dc src/lib/Nom2fix.ml

View differences:

src/lib/Nom2fix.ml
122 122
  done;
123 123
  (*end calc flc*)
124 124

  
125
  let ret = ref (calcforsub (List.hd !formulaList) noms funct) in
126
  for i = 1 to (List.length !formulaList) - 1 do
127
    let akt = List.nth !formulaList i in
125
  let formulaListSmall = ref [] in
126

  
127
  let rem = ref false in
128

  
129
  for i = 0 to (List.length !formulaList) - 1 do
130
    for j = i + 1 to (List.length !formulaList) - 1 do
131
      rem := if CoAlgFormula.equals (List.nth !formulaList i) (CoAlgFormula.nnfNeg (List.nth !formulaList j)) then true else !rem;
132
      print_endline (if !rem == true then "true" else "false");
133
      print_endline (CoAlgFormula.exportFormula (CoAlgFormula.nnf (List.nth !formulaList i)));
134
      print_endline (CoAlgFormula.exportFormula (CoAlgFormula.nnfNeg (List.nth !formulaList j)));
135
    done;
136
    if !rem == false then formulaListSmall := (List.nth !formulaList i) :: !formulaListSmall;
137
    rem := false;
138
  done; 
139

  
140
  let ret = ref CoAlgFormula.TRUE in
141
  for i = 0 to (List.length !formulaListSmall) - 1 do
142
    let akt = List.nth !formulaListSmall i in
128 143
    match akt with
129
    | CoAlgFormula.NOT f1 -> ret := !ret;
130 144
    | CoAlgFormula.AND (f1,f2)
131 145
    | CoAlgFormula.OR (f1,f2) -> ret := !ret;
132
    | _ -> let sub = calcforsub (List.nth !formulaList i) noms funct in
146
    | CoAlgFormula.NOT f1 -> let sub = calcforsub f1 noms funct in
147
          ret := CoAlgFormula.AND(!ret, sub);
148
    | _ -> let sub = calcforsub (List.nth !formulaListSmall i) noms funct in
133 149
           ret := CoAlgFormula.AND(!ret, sub);
134 150
  done;
135 151

  

Also available in: Unified diff