driver and printer for Simplify

parent 54499c65
......@@ -107,7 +107,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
eliminate_inductive eliminate_let eliminate_if \
explicit_polymorphism
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify
LIBMODULES = src/config \
$(addprefix src/util/, $(LIB_UTIL)) \
......
......@@ -120,6 +120,6 @@ end
(*
Local Variables:
mode: why
compile-command: "make -C ../.. bench"
compile-command: "make -C .. bench"
End:
*)
(* Why driver for Simplify *)
prelude ";;; this is a prelude for Simplify"
printer "simplify"
filename "%f-%t-%g.sx"
valid "\\bValid\\b"
unknown "\\bInvalid\\b" "Unknown"
transformation "simplify_recursive_definition"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "encoding_decorate"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (_=_) "(EQ %1 %2)"
syntax logic (_<>_) "(NEQ %1 %2)"
end
theory int.Int
prelude ";;; this is a prelude for Simplify, Arithmetic"
syntax logic zero "0"
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
remove prop CommutativeGroup.Inv_def
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
end
theory transform.encoding_decorate.Kept
tag cloned type t "encoding_decorate : kept"
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Register
open Format
open Pp
open Ident
open Ty
open Term
open Decl
open Task
let ident_printer =
let bls = [] in
let san = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer bls ~sanitizer:san
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let forget_var v = forget_id ident_printer v.vs_name
let print_var fmt {vs_name = id} = print_ident fmt id
let simplify_max_int = Int64.of_string "2147483646"
let pp_exp fmt e =
if e="" then () else
if e.[0] = '-' then
fprintf fmt "minus%s" (String.sub e 1 (String.length e - 1))
else
fprintf fmt "%s" e
let print_real fmt = function
| RConstDecimal (i, f, e) ->
fprintf fmt "%s_%se%a" i f (Pp.print_option pp_exp) e
| RConstHexa (i, f, e) ->
fprintf fmt "0x%s_%sp%a" i f pp_exp e
let rec print_term drv fmt t = match t.t_node with
| Tbvar _ ->
assert false
| Tconst (ConstInt n) ->
begin try
let n64 = Int64.of_string n in
if n64 < 0L || n64 > simplify_max_int then raise Exit;
fprintf fmt "%s" n
with _ -> (* the constant is too large for Simplify *)
fprintf fmt "constant_too_large_%s" n
end
| Tconst (ConstReal c) ->
fprintf fmt "real_constant_%a" print_real c
| Tvar v ->
print_var fmt v
| Tapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
| Some s ->
Driver.syntax_arguments s (print_term drv) fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
| _ -> fprintf fmt "@[(%a@ %a)@]"
print_ident ls.ls_name (print_list space (print_term drv)) tl
end end
| Tlet _ ->
unsupportedTerm t "simplify: you must eliminate let"
| Tif _ ->
unsupportedTerm t "simplify: you must eliminate if"
| Tcase _ ->
unsupportedTerm t "simplify: you must eliminate match"
| Teps _ ->
unsupportedTerm t "simplify: you must eliminate epsilon"
and print_fmla drv fmt f = match f.f_node with
| Fapp ({ ls_name = id }, []) ->
print_ident fmt id
| Fapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
| Some s ->
Driver.syntax_arguments s (print_term drv) fmt tl
| None ->
fprintf fmt "(EQ (%a@ %a) |@@true|)"
print_ident ls.ls_name (print_list space (print_term drv)) tl
end
| Fquant (q, fq) ->
let q = match q with Fforall -> "FORALL" | Fexists -> "EXISTS" in
let vl, tl, f = f_open_quant fq in
fprintf fmt "@[(%s (%a)%a@ %a)@]" q (print_list space print_var) vl
(print_triggers drv) tl (print_fmla drv) f;
List.iter forget_var vl
| Fbinop (Fand, f1, f2) ->
fprintf fmt "@[(AND@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (For, f1, f2) ->
fprintf fmt "@[(OR@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (Fimplies, f1, f2) ->
fprintf fmt "@[(IMPLIES@ %a@ %a)@]"
(print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (Fiff, f1, f2) ->
fprintf fmt "@[(IFF@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
| Fnot f ->
fprintf fmt "@[(NOT@ %a)@]" (print_fmla drv) f
| Ftrue ->
fprintf fmt "TRUE"
| Ffalse ->
fprintf fmt "FALSE"
| Fif _ ->
unsupportedFmla f "simplify : you must eliminate if"
| Flet _ ->
unsupportedFmla f "simplify : you must eliminate let"
| Fcase _ ->
unsupportedFmla f "simplify : you must eliminate match"
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
and print_trigger drv fmt = function
| [] -> ()
| [Term ({t_node=Tvar _} as t)] -> fprintf fmt "(MPAT %a)" (print_term drv) t
| [t] -> print_expr drv fmt t
| tl -> fprintf fmt "(MPAT %a)" (print_list space (print_expr drv)) tl
and print_triggers drv fmt = function
| [] -> ()
| tl -> fprintf fmt "@ (PATS %a)" (print_list space (print_trigger drv)) tl
let print_logic_decl _drv _fmt (_ls,ld) = match ld with
| None ->
()
| Some _ ->
(* TODO: predicate definitions could actually be passed to Simplify *)
unsupported "Predicate and function definition aren't supported"
let print_logic_decl drv fmt d =
if Driver.query_remove drv (fst d).ls_name then false
else begin print_logic_decl drv fmt d; true end
let print_decl drv fmt d = match d.d_node with
| Dtype _ ->
false
| Dlogic dl ->
print_list_opt newline (print_logic_decl drv) fmt dl
| Dind _ ->
unsupportedDecl d "simplify : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name ->
false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[(BG_PUSH@\n ;; axiom %s@\n @[<hov 2>%a@])@]@\n"
pr.pr_name.id_string (print_fmla drv) f;
true
| Dprop (Pgoal, pr, f) ->
fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
begin match id_from_user pr.pr_name with
| None -> ()
| Some loc -> fprintf fmt " @[;; %a@]@\n"
Loc.gen_report_position loc
end;
fprintf fmt "@[<hov 2>%a@]@\n" (print_fmla drv) f;
true
| Dprop (Plemma, _, _) ->
assert false
let print_decl drv fmt = catch_unsupportedDecl (print_decl drv fmt)
let print_task drv fmt task =
Driver.print_full_prelude drv task fmt;
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls);
fprintf fmt "@."
let () = register_printer "simplify"
(fun drv fmt task ->
forget_all ident_printer;
print_task drv fmt task)
(* test file *)
theory TestMutual
type tree =
| Leaf
| Node (int, forest)
type forest =
| Nil
| Cons (tree, forest)
goal G : forall x:tree. x=x
end
theory Test
use import int.Int
logic id(x: int) : int = x
logic id2(x: int) : int = id(x)
logic succ(x:int) : int = id(x+1)
goal G : (forall x:int.x=x) or
(forall x:int. x=x+1)
goal G2 : forall x:int. let x = 0 + 1 in x = 1
type t = int * real
logic c : t = (1, 3.14)
use import list.List
axiom A :
let x = 1 in
let (y,z) = c in
x = y
end
theory Test2
use import Test
logic d : t = (2, 6.3)
end
theory Test_simplify_array
use import array.Array
goal G : forall x,y:int. forall m: (int,int) t.
select(store(m,y,x),y) = x
end
theory Test_conjunction
use import int.Int
goal G :
forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
goal G2 :
forall x:int.
(x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
use export int.Int
logic f(int) : int
logic q(int, int)
axiom A : forall x:int. q(-x,f(x))
goal G : 3.14 = 3.15
end
theory Split_conj
logic p(x:int)
(*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
(*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
(*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*)
goal G : forall x,y,z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z))
(*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x)) or ((p(z)) and (p(x))))) *)
(*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*)
end
theory TestEnco
use import int.Int
type 'a mytype
logic id(x: int) : int = x
logic id2(x: int) : int = id(x)
logic succ(x:int) : int = id(x+1)
goal G : (forall x:int. x=x) or
(forall x:int. x=x+1)
logic p('a ) : 'a mytype
logic p2('a mytype) : 'a
axiom A1 : forall x : 'a mytype. p(p2(x)) = x
goal G2 : forall x:int. p2(p(x)) = x
end
(*
Local Variables:
compile-command: "make -C .. test"
compile-command: "cd ..; bin/why.opt -D drivers/simplify.drv tests/test-jcf.why && bin/why.opt -P simplify tests/test-jcf.why"
End:
*)
......@@ -31,3 +31,8 @@ driver = "drivers/tptp.drv"
name = "eprover"
command = "why-cpulimit 0 %m eprover -s --print-statistics -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
driver = "drivers/tptp.drv"
[prover simplify]
name = "simplify"
command = "why-cpulimit %t %m Simplify %f 2>&1"
driver = "drivers/simplify.drv"
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment