path: root/abstract/formula.ml

open Ast

(* AST for logical formulas *)

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


type bool_expr =
  (* constants *)
  | BConst of bool
  (* operators from numeric values to boolean values *)
  | BRel of binary_rel_op * num_expr * num_expr
  | BBoolEq of id * bool
  (* boolean operators *)
  | BAnd of bool_expr * bool_expr
  | BOr of bool_expr * bool_expr
  | BNot of bool_expr


let f_and a b = match a, b with
  | BConst false, _ | _, BConst false -> BConst false
  | BConst true, b -> b
  | a, BConst true -> a
  | a, b -> BAnd(a, b)

let f_or a b = match a, b with
  | BConst true, _ | _, BConst true -> BConst true
  | BConst false, b -> b
  | a, BConst false -> a
  | a, b -> BOr(a, b)


(* 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)
  | BBoolEq(id, v) -> BBoolEq(id, not v)
  | BNot e -> eliminate_not e
  | BRel(r, a, b) ->
    if r = AST_EQ then
      BOr(BRel(AST_LT, a, b), BRel(AST_GT, a, b))
    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)
  | 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 cons_op =
  | CONS_EQ | CONS_NE
  | CONS_GT | CONS_GE
type cons = num_expr * cons_op  (* always imply right member = 0 *)

type conslist = 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) ->
    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
      then (x, op)
      else (NBinary(AST_MINUS, x, y), op)
    in [cons], CLTrue
  | BConst x ->
    [], if x then CLTrue else CLFalse
  | BBoolEq(id, v) ->
    if v then
      [NBinary(AST_MINUS, NIdent id, NIntConst 1), CONS_EQ], CLTrue
    else
      [NIdent id, CONS_EQ], CLTrue
  | BOr(a, b) ->
    let ca, ra = conslist_of_f a in
    let cb, rb = conslist_of_f b in
    begin match ca, ra, cb, rb with
      | _, CLFalse, _, _ -> cb, rb
      | _, _, _, CLFalse -> ca, ra
      | [], CLTrue, _, _ -> [], CLTrue
      | _, _, [], CLTrue -> [], CLTrue
      | _ -> [], CLOr((ca, ra), (cb, rb))
    end
  | BAnd(a, b) ->
    let ca, ra = conslist_of_f a in
    let cb, rb = conslist_of_f b in
    let cons = ca @ cb in
    begin match ra, rb with
      | CLFalse, _ | _, CLFalse -> [], CLFalse
      | CLTrue, _ -> cons, rb
      | ra, CLTrue -> cons, ra
      | _, _ -> cons, CLAnd(ra, rb)
    end