open Format
open Options
open Ast
open Util
open Types
type t = node_cube
let variables {cube = {Cube.vars = vars }} = vars
let array n = n.cube.Cube.array
let litterals n = n.cube.Cube.litterals
let dim n = Cube.dim n.cube
let size n = Cube.size n.cube
let compare_kind s1 s2 =
match s1.kind, s2.kind with
| Approx, Approx -> 0
| Approx, _ -> -1
| _, Approx -> 1
| k1, k2 -> Pervasives.compare k1 k2
let compare_by_breadth s1 s2 =
let v1 = dim s1 in
let v2 = dim s2 in
let c = Pervasives.compare v1 v2 in
if c <> 0 then c else
let c1 = size s1 in
let c2 = size s2 in
let c = Pervasives.compare c1 c2 in
if c <> 0 then c else
let c = compare_kind s1 s2 in
if c <> 0 then c else
let c = Pervasives.compare s1.depth s2.depth in
if c <> 0 then c else
Pervasives.compare (abs s1.tag) (abs s2.tag)
let compare_by_depth s1 s2 =
let v1 = dim s1 in
let v2 = dim s2 in
let c = Pervasives.compare v1 v2 in
if c <> 0 then c else
let c1 = size s1 in
let c2 = size s2 in
let c = Pervasives.compare c1 c2 in
if c <> 0 then c else
let c = compare_kind s1 s2 in
if c <> 0 then c else
let c = Pervasives.compare s2.depth s1.depth in
if c <> 0 then c else
Pervasives.compare (abs s1.tag) (abs s2.tag)
let rec origin n = match n.from with
| [] -> n
| (_,_, p)::_ ->
if p.kind = Approx then p
else origin p
let new_tag =
let cpt_pos = ref 0 in
let cpt_neg = ref 0 in
fun ?(kind=Node) () ->
match kind with
| Approx -> decr cpt_neg; !cpt_neg
| _ -> incr cpt_pos; !cpt_pos
let create ?(kind=Node) ?(from=None) cube =
let hist = match from with
| None -> []
| Some ((_, _, n) as f) -> f :: n.from in
{
cube = cube;
tag = new_tag ~kind ();
kind = kind;
depth = List.length hist;
deleted = false;
from = hist;
}
let has_deleted_ancestor n =
let rec has acc = function
| [] -> false, acc
| (_, _, a) :: r ->
if a.deleted then true, acc
else has (a :: acc) r
in
let del, children = has [] n.from in
if del then List.iter (fun a -> a.deleted <- true) children;
del
let has_deleted_ancestor n =
List.exists (fun (_, _, a) -> a.deleted) n.from
let ancestor_of n s =
List.exists (fun (_, _, ps) -> n.tag = ps.tag) s.from
let subset n1 n2 = ArrayAtom.subset (array n1) (array n2)
let print fmt n = Cube.print fmt n.cube
module Latex = struct
let print_const fmt = function
| ConstInt n | ConstReal n -> fprintf fmt "%s" (Num.string_of_num n)
| ConstName n -> fprintf fmt "%a" Hstring.print n
let print_cs fmt cs =
MConst.iter
(fun c i ->
fprintf fmt " %s %a"
(if i = 1 then "+" else if i = -1 then "-"
else if i < 0 then "- "^(string_of_int (abs i))
else "+ "^(string_of_int (abs i)))
print_const c) cs
let rec print_term fmt = function
| Const cs -> print_cs fmt cs
| Elem (s, Var) -> fprintf fmt "%a" Hstring.print s
| Elem (s, Glob) -> fprintf fmt "\\texttt{%a}" Hstring.print s
| Elem (s, Constr) -> fprintf fmt "\\textsf{%a}" Hstring.print s
| Access (a, li) ->
fprintf fmt "\\texttt{%a}[%a]" Hstring.print a (Hstring.print_list ", ") li
| Arith (x, cs) ->
fprintf fmt "@[%a%a@]" print_term x print_cs cs
let str_op_comp =
function Eq -> "=" | Lt -> "<" | Le -> "\\le" | Neq -> "\\neq"
let rec print_atom fmt = function
| Atom.True -> fprintf fmt "true"
| Atom.False -> fprintf fmt "false"
| Atom.Comp (x, op, y) ->
fprintf fmt "%a %s %a" print_term x (str_op_comp op) print_term y
| Atom.Ite (la, a1, a2) ->
fprintf fmt "@[ite(%a,@ %a,@ %a)@]"
(print_atoms false "\\land") (SAtom.elements la)
print_atom a1 print_atom a2
and print_atoms inline sep fmt = function
| [] -> ()
| [a] -> print_atom fmt a
| a::l ->
if inline then
fprintf fmt "%a %s@ %a" print_atom a sep (print_atoms inline sep) l
else
fprintf fmt "%a %s@\n%a" print_atom a sep (print_atoms inline sep) l
let print fmt n =
fprintf fmt "\\item $";
let l = variables n in
(match l with
| [] -> ()
| [_] -> fprintf fmt "\\forall %a.~ " Variable.print_vars l
| x::y::[] -> fprintf fmt "\\forall %a.~ %a \\neq %a \\implies "
Variable.print_vars l Variable.print x Variable.print y
| _ -> fprintf fmt "\\forall %a.~ " Variable.print_vars l
);
let natoms = List.rev (SAtom.elements (litterals n)) in
(match natoms with
| [] -> ()
| [a] -> print_atom fmt (Atom.neg a)
| last :: r ->
let lr = List.rev r in
fprintf fmt "(%a) \\implies %a" (print_atoms true " \\land ") lr
print_atom (Atom.neg last)
);
fprintf fmt "$"
end
let print_history fmt n =
let last = List.fold_left
(fun last (tr, args, a) ->
if dmcmt then
fprintf fmt "[%a%a]" Hstring.print tr.tr_name Variable.print_vars args
else
fprintf fmt "%a(%a) ->@ " Hstring.print tr.tr_name
Variable.print_vars args;
a
) n n.from in
if dmcmt then fprintf fmt "[0] "
else
if last.kind = Approx then
fprintf fmt "@{<fg_blue>approx[%d]@}" last.tag
else
fprintf fmt "@{<fg_magenta>unsafe[%d]@}" last.tag