path: root/abstract/formula.ml

open Ast
open Util
open Ast_util

(* AST for logical formulas *)


(* Numerical part *)

(* bool on numerical operators : is it float ? *)

type num_expr =
  (* constants *)
  | NIntConst of int
  | NRealConst of float
  (* operators *)
  | NBinary of binary_op * num_expr * num_expr * bool
  | NUnary of unary_op * num_expr * bool
  (* identifier *)
  | NIdent of id

type num_cons_op =
  | CONS_EQ | CONS_NE
  | CONS_GT | CONS_GE
type num_cons = num_expr * num_cons_op  (* always imply right member = 0 *)


(* Logical part *)


(* Enumerated types *)
type enum_expr =
  | EIdent of id
  | EItem of string

type enum_op =
  | E_EQ | E_NE

type enum_cons = enum_op * id * enum_expr

type bool_expr =
  (* constants *)
  | BConst of bool
  (* operators from numeric values to boolean values *)
  | BRel of binary_rel_op * num_expr * num_expr * bool
  (* operators on enumerated types *)
  | BEnumCons of enum_cons
  (* boolean operators *)
  | BAnd of bool_expr * bool_expr
  | BOr of bool_expr * bool_expr
  | BNot of bool_expr

let is_false = function
  | BConst false | BNot(BConst true) -> true
  | _ -> false
let is_true = function
  | BConst true | BNot(BConst false) -> true
  | _ -> false

let f_and a b =
  if is_false a || is_false b then BConst false
  else if is_true a then b
  else if is_true b then a
  else BAnd(a, b)

let f_and_list = List.fold_left f_and (BConst true)

let f_or a b =
  if is_true a || is_true b then BConst true
  else if is_false a then b
  else if is_false b then a
  else BOr(a, b)

let f_e_op op a b = match a, b with
  | EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j)
  | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v)
let f_e_eq = f_e_op E_EQ

(* Write all formula without using the NOT operator *)

let rec eliminate_not = function
  | BNot e -> eliminate_not_negate e
  | BAnd(a, b) -> BAnd(eliminate_not a, eliminate_not b)
  | BOr(a, b) -> BOr(eliminate_not a, eliminate_not b)
  | x -> x
and eliminate_not_negate = function
  | BConst x -> BConst(not x)
  | BEnumCons(op, a, b) -> BEnumCons((if op = E_EQ then E_NE else E_EQ), a, b)
  | BNot e -> eliminate_not e
  | BRel(r, a, b, is_real) ->
    if r = AST_EQ then
      BOr(BRel(AST_LT, a, b, is_real), BRel(AST_GT, a, b, is_real))
    else
      let r' = match r with
      | AST_EQ -> AST_NE
      | AST_NE -> AST_EQ
      | AST_LT -> AST_GE
      | AST_LE -> AST_GT
      | AST_GT -> AST_LE
      | AST_GE -> AST_LT
      in
      BRel(r', a, b, is_real)
  | BAnd(a, b) ->
    BOr(eliminate_not_negate a, eliminate_not_negate b)
  | BOr(a, b) ->
    BAnd(eliminate_not_negate a, eliminate_not_negate b)



(*
  In big ANDs, try to separate levels of /\ and levels of \/
  We also use this step to simplify trues and falses that may be present.
*)

type conslist = enum_cons list * num_cons list * conslist_bool_expr
and conslist_bool_expr =
  | CLTrue
  | CLFalse
  | CLAnd of conslist_bool_expr * conslist_bool_expr
  | CLOr of conslist * conslist

let rec conslist_of_f = function
  | BNot e -> conslist_of_f (eliminate_not_negate e)
  | BRel (op, a, b, is_real) ->
    let x, y, op = match op with
      | AST_EQ -> a, b, CONS_EQ
      | AST_NE -> a, b, CONS_NE
      | AST_GT -> a, b, CONS_GT
      | AST_GE -> a, b, CONS_GE
      | AST_LT -> b, a, CONS_GT
      | AST_LE -> b, a, CONS_GE
    in
    let cons = if y = NIntConst 0 || y = NRealConst 0.
      then (x, op)
      else (NBinary(AST_MINUS, x, y, is_real), op)
    in [], [cons], CLTrue
  | BConst x ->
    [], [], if x then CLTrue else CLFalse
  | BEnumCons e ->
    [e], [], CLTrue
  | BOr(a, b) ->
    let eca, ca, ra = conslist_of_f a in
    let ecb, cb, rb = conslist_of_f b in
    begin match eca, ca, ra, ecb, cb, rb with
      | _, _, CLFalse, _, _, _ -> ecb, cb, rb
      | _, _, _, _, _, CLFalse -> eca, ca, ra
      | [], [], CLTrue, _, _, _ -> [], [], CLTrue
      | _, _, _, [], [], CLTrue -> [], [], CLTrue
      | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb))
    end
  | BAnd(a, b) ->
    let eca, ca, ra = conslist_of_f a in
    let ecb, cb, rb = conslist_of_f b in
    let cons = ca @ cb in
    let econs = eca @ ecb in
    begin match ra, rb with
      | CLFalse, _ | _, CLFalse -> [], [], CLFalse
      | CLTrue, _ -> econs, cons, rb
      | _, CLTrue -> econs, cons, ra
      | _, _ -> econs, cons, CLAnd(ra, rb)
    end