From 306d432e2c567ee9af8319ec3277ae9be22ba9c4 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 15 Apr 2019 14:45:36 +0200 Subject: [PATCH] Formula simplification at preprocessing --- non-regression/main_script.sh | 1 + src/bin/gui/annoted_ast.ml | 19 +- src/lib/dune | 1 + src/lib/frontend/cnf.ml | 83 ++- src/lib/frontend/simple_reasoner_expr.ml | 698 ++++++++++++++++++++++ src/lib/frontend/simple_reasoner_expr.mli | 119 ++++ src/lib/reasoners/fun_sat.ml | 3 - src/lib/reasoners/th_util.ml | 2 + src/lib/reasoners/th_util.mli | 2 + src/lib/structures/commands.ml | 2 +- src/lib/structures/commands.mli | 2 +- src/lib/structures/expr.ml | 90 ++- src/lib/structures/expr.mli | 17 + src/lib/structures/symbols.ml | 16 +- src/lib/structures/typed.ml | 472 +++++++++++---- src/lib/structures/typed.mli | 75 ++- src/lib/util/options.ml | 9 + src/lib/util/options.mli | 21 + src/lib/util/util.ml | 5 + src/lib/util/util.mli | 5 + src/parsers/psmt2_to_alt_ergo.ml | 1 + 21 files changed, 1496 insertions(+), 147 deletions(-) create mode 100644 src/lib/frontend/simple_reasoner_expr.ml create mode 100644 src/lib/frontend/simple_reasoner_expr.mli diff --git a/non-regression/main_script.sh b/non-regression/main_script.sh index d27714d2fa..0c1c6d1d9e 100755 --- a/non-regression/main_script.sh +++ b/non-regression/main_script.sh @@ -54,6 +54,7 @@ do tput hpa 25 total=`expr $total + 1` echo -n "$total / $big_total" + echo "$pr $ae $opt 1> $main_script_out 2> $main_script_err" timeout 2 $pr $ae $opt 1> $main_script_out 2> $main_script_err if grep -q -w Valid $main_script_out ; then score=`expr $score + 1` diff --git a/src/bin/gui/annoted_ast.ml b/src/bin/gui/annoted_ast.ml index 08fd7eec8f..577cabaa19 100644 --- a/src/bin/gui/annoted_ast.ml +++ b/src/bin/gui/annoted_ast.ml @@ -739,15 +739,18 @@ and print_tt_desc fmt = function | TTnamed (lbl, t) -> fprintf fmt "%s:%a" (Hstring.view lbl) print_tterm t | TTinInterval(e, lb, ub) -> fprintf fmt "%a in %a, %a" - print_term e + (print_term ~annot:no_print) e Symbols.print_bound lb Symbols.print_bound ub - | TTmapsTo(x,e) -> fprintf fmt "%a |-> %a" Var.print x print_term e + | TTmapsTo(x,e) -> + fprintf fmt "%a |-> %a" Var.print x (print_term ~annot:no_print) e | TTite(f,t1, t2) -> fprintf fmt "(if %a then %a else %a)" - print_tform f print_term t1 print_term t2 + print_tform f + (print_term ~annot:no_print) t1 + (print_term ~annot:no_print) t2 | TTproject (_, _, _) | TTmatch (_, _) -> Gui_config.not_supported "Algebraic datatypes" @@ -759,9 +762,13 @@ and print_term_binders fmt l = match l with | [] -> assert false | (sy, t) :: l -> - fprintf fmt "%a = %a" Symbols.print_clean sy print_term t; + fprintf fmt "%a = %a" Symbols.print_clean sy (print_term ~annot:no_print) t; List.iter (fun (sy, t) -> - fprintf fmt ",\n%a = %a" Symbols.print_clean sy print_term t) l + fprintf + fmt + ",\n%a = %a" + Symbols.print_clean sy + (print_term ~annot:no_print) t) l and print_tatom fmt a = match a.Typed.c with | TAtrue -> fprintf fmt "true" @@ -814,7 +821,7 @@ and print_tform2 fmt f = match f.Typed.c with and print_mixed_binders = let aux fmt e = match e with - | TletTerm t -> fprintf fmt "%a" print_term t + | TletTerm t -> fprintf fmt "%a" (print_term ~annot:no_print) t | TletForm f -> fprintf fmt "%a" print_tform2 f in fun fmt binders -> match binders with diff --git a/src/lib/dune b/src/lib/dune index 1832a2eba6..b75bade905 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -29,6 +29,7 @@ ; modules that make up the lib (modules ; frontend + Simple_reasoner_expr Cnf Input Frontend Parsed_interface Typechecker ; reasoners Ac Arith Arrays Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 163d64658f..a5528122a7 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -34,6 +34,57 @@ open Commands module E = Expr module Sy = Symbols module SE = E.Set +module SRE = Simple_reasoner_expr + +(** Simplifyer not using the theory *) +module DummySimp: + (Simple_reasoner_expr.S with type expr = Expr.t + and type env = Theory.Main_Default.t + and type expl = Explanation.t) = + Expr.SimpExpr + (Explanation) + (struct + type expr = Expr.t + type expl = Explanation.t + type env = Theory.Main_Default.t + let empty = Theory.Main_Default.empty + let bool_query _ _ = None + let q_query _ _ = None + end + ) + +(** Simplifyer using the theory *) +module ThSimp : Simple_reasoner_expr.S with type expr = Expr.t + and type env = Theory.Main_Default.t + and type expl = Explanation.t = + Expr.SimpExpr + (Explanation) + (struct + type expr = Expr.t + type expl = Explanation.t + type env = Theory.Main_Default.t + let empty = Theory.Main_Default.empty + let bool_query ex env = + try + match Theory.Main_Default.query ex env with + | Some (expl,[]) -> Some (true, expl) + | Some _ | None -> None + with _ -> + Format.eprintf "Query failed on %a@." Expr.print ex; None + let q_query _ex _env = None + end + ) + + +let choose_preproc () : + (module Simple_reasoner_expr.S with type expr = Expr.t + and type env = Theory.Main_Default.t + and type expl = Explanation.t) = + if not (Options.get_simplify_th ()) + then (module DummySimp) + else (module ThSimp) + +module SimpExprPreproc () = (val (choose_preproc ())) [@@ocaml.ppwarning "TODO: Change Symbols.Float to store FP numeral \ constants (eg, <24, -149> for single) instead of \ @@ -283,8 +334,15 @@ let rec make_term up_qv quant_basename t = ~decl_kind:E.Daxiom (* not correct, but not a problem *) ~toplevel:false in - mk_term t - + let term = mk_term t in + match Options.get_simplify () with + | Util.SNo -> term + | Util.SPreprocess | Util.SAll -> + let module S = SimpExprPreproc () in + let smp_term = S.simp_expr term in + if SRE.has_changed smp_term + then SRE.get_expr smp_term + else term and make_trigger ~in_theory name up_qv quant_basename hyp (e, from_user) = let content, guard = match e with @@ -485,7 +543,14 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t = (* wrapper of function make_form *) let make_form name f loc ~decl_kind = let ff = - make_form Sy.Map.empty name f loc ~decl_kind ~toplevel:true + let form = make_form Sy.Map.empty name f loc ~decl_kind ~toplevel:true in + match Options.get_simplify () with + Util.SNo -> form + | Util.SPreprocess | Util.SAll -> + let module S = SimpExprPreproc () in + let smp_form = S.simp_expr form in + if SRE.has_changed smp_form then SRE.get_expr smp_form + else form in assert (Sy.Map.is_empty (E.free_vars ff Sy.Map.empty)); let ff = E.purify_form ff in @@ -511,7 +576,7 @@ let mk_assume acc f name loc = *) let defining_term f = if get_verbose () then - Format.eprintf "defining term of %a@." Typed.print_formula f; + Format.eprintf "defining term of %a@." (Typed.print_formula ?annot:None) f; match f.c with | TFforall {qf_form={c=TFop(OPiff,[{c=TFatom {c=TApred(d,_);_};_};_]); _}; _} | TFforall {qf_form={c=TFatom {c=TAeq[d;_];_}; _}; _} @@ -554,12 +619,16 @@ let mk_theory acc l th_name extends _loc = | TAxiom (loc, name, ax_kd, f) -> loc, name, f, ax_kd | _ -> assert false in - let ax_form = make_form ax_name f loc ~decl_kind:E.Dtheory in + let ax_form = + make_form ax_name f loc ~decl_kind:E.Dtheory + in let th_elt = {Expr.th_name; axiom_kind; extends; ax_form; ax_name} in {st_decl=ThAssume th_elt ; st_loc=loc} :: acc - )acc l + ) + acc + l -let make acc d = +let make acc (d : (int Typed.tdecl, 'a) Typed.annoted) = match d.c with | TPush (loc,n) -> {st_decl=Push n; st_loc=loc} :: acc | TPop (loc,n) -> {st_decl=Pop n; st_loc=loc} :: acc diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml new file mode 100644 index 0000000000..2d4dcf85a5 --- /dev/null +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -0,0 +1,698 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2018 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +let verb = Options.get_simplify_verbose + +let silent (msg : ('a, Format.formatter, unit) format) = + Format.ifprintf Format.std_formatter msg + +let talk (msg : ('a, Format.formatter, unit) format) = + Format.printf "[Preprocess] "; + Format.printf msg + +let debug (msg : ('a, Format.formatter, unit) format) = + if verb () + then talk msg + else silent msg + +(** 1. Utils *) + +(** Values are representations of expressions + that have been "solved", in the sense that they can + be reduced to a boolean or a float/int. *) +type value = + | Bool of bool + | Num of Q.t + +let (++) v1 v2 = + match v1, v2 with + Bool b1, Bool b2 -> Bool (b1 || b2) + | Num n1, Num n2 -> Num (Q.add n1 n2) + | _,_ -> assert false + +let (--) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> Num (Q.sub n1 n2) + | _,_ -> assert false + +let ( ** ) v1 v2 = + match v1, v2 with + Bool b1, Bool b2 -> Bool (b1 && b2) + | Num n1, Num n2 -> Num (Q.mul n1 n2) + | _,_ -> assert false + +let (|=) v1 v2 = + match v1, v2 with + Bool b1, Bool b2 -> b1 == b2 + | Num n1, Num n2 -> (Stdlib.(=)) n1 n2 + | _,_ -> false + +let (|<>) v1 v2 = not (v1 |= v2) + +let (|<) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> n1 < n2 + | _,_ -> assert false + +let (|<=) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> n1 <= n2 + | _,_ -> assert false + +let (|>) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> n1 > n2 + | _,_ -> assert false + +let (|>=) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> n1 >= n2 + | _,_ -> assert false + +(** Same as List.fold_left, but f returns + a tuple (acc, stop) where stop is a boolean + stating that the loop has to stop. *) +let fold_left_stop + (f : 'a -> 'b -> ('a * bool)) + (acc : 'a) + (l : 'b list) : 'a + = + let rec __fold acc l = + match l with + [] -> acc + | hd :: tl -> + let acc, stop = f acc hd in + if stop then acc + else __fold acc tl + in __fold acc l + +let pp_val fmt v = + match v with + Bool b -> Format.fprintf fmt "Bool %b" b + | Num n -> Format.fprintf fmt "Num %a" Q.pp_print n + +(** A simplified formula/expr/... type. + The diff field is set to false if the operation did not change the + input. + As queries may provide explanations, the third field correspond to the + explanation behind the simplification. *) +type ('a, 'expl) simp = + { + v : 'a; + diff : bool; + expl : 'expl + } + +let get_expr (e : ('a,_) simp) : 'a = e.v +let has_changed (e : _ simp) : bool = e.diff +let get_expl (e : (_,'expl) simp) : 'a = e.expl + +(** 2. Simplifyer *) + +(** As the simplifyer interacts with different components of alt-ergo, + it is written to be as generic as possible. + The simplifyer is then a functor of different modules which type is + defined below. *) + +(** Expr is the signature of the module dedicated to + the representation of expressions that are to be + simplified. *) +module type Expr = +sig + type t + + val equal : t -> t -> bool + val mk_expr : Symbols.t -> t list -> Ty.t -> t + + (** Expressions are generally defined by 3 elements: + - a type + - a set of sub expressions + - a composition operator *) + val get_comp : t -> Symbols.t + val get_sub_expr : t -> t list + val get_type : t -> Ty.t + + val _true : t + val _false : t + + val real : string -> t + val int : string -> t + + val pretty : Format.formatter -> t -> unit +end + +(** Expl is the signature of the module dedicated to + the explanations of the calculations. *) +module type Expl = +sig + type t + + (** Represents no explanation. *) + val empty : t + + (** Tests if the explanation is empty *) + val is_empty : t -> bool + + (** Merges two explanations. *) + val union : t -> t -> t +end + +(** Th is the signature of the module dedicated to + the interactions with the theory. *) +module type Th = +sig + type expr + type env + type expl + + (** Empty environment. *) + val empty : unit -> env + + (** Tries to decide the expression in argument given the environment. + If it fails, returns None. Otherwise, provides the answer and + an explanation (possibly empty) + *) + val bool_query : expr -> env -> (bool * expl) option + + (** Tries to decide the arithmetic value of an expression given the + environment. + If it fails, returns None. Otherwise, provides the answer and + an explanation (possibly empty) *) + val q_query : expr -> env -> (Q.t * expl) option + +end + +(** This is the signature of the simplifyer. *) +module type S = +sig + (** The type of expressions. *) + type expr + + (** The type of environments the theory works in. *) + type env + + (** The type of explanations *) + type expl + + (** Sets the environment to be used in the simplifyer. + Set to empty by default. *) + val set_env : env -> unit + + (** Simplifies an expression. *) + val simp_expr : expr -> (expr,expl) simp +end + +module SimpleReasoner + (E : Expr) + (Expl : Expl) + (T : Th with type expr = E.t and type expl = Expl.t) + : S with type expr = E.t and type env = T.env and type expl = Expl.t = struct + type expr = E.t + type env = T.env + type expl = Expl.t + + let env = ref (T.empty ()) + + let set_env e = env := e + let no_reason = Expl.empty + + let identity v = {v; diff = false; expl = Expl.empty} + let diff_list (l : ('a, 'expl) simp list) : (('a list), 'expl) simp = + let rev = + List.fold_left + (fun acc s -> + {v = s.v :: acc.v; + diff = acc.diff || s.diff; + expl = Expl.union acc.expl s.expl + } + ) + (identity []) + l + in + {rev with v = List.rev rev.v} + + (* Check is an expression has an arithmetic type (Some true), + a boolean type (Some false) or else (None). *) + let is_arith (e : expr) : bool option = + match E.get_type e with + Ty.Tbool -> Some false + | Ty.Tint | Ty.Treal + | Ty.Tvar {value = Some Ty.Tint;_} + | Ty.Tvar {value = Some Ty.Treal;_} -> Some true + | _ -> None + + let value_from_query (e : expr) : (value * expl) option = + match is_arith e with + Some true -> ( + match T.q_query e !env with + Some (res_query, expl) -> + Some ((Num res_query), expl) + | None -> None + ) + | Some false -> ( + match T.bool_query e !env with + Some (res_query, expl) -> + Some ((Bool res_query), expl) + | None -> None + ) + | None -> None + + let expr_to_value (e : expr) : (value * expl) option = + match E.get_comp e with + True -> Some ((Bool true), no_reason) + | False -> Some ((Bool false), no_reason) + | Int s -> Some ((Num (Q.of_string (Hstring.view s))), no_reason) + | Real s -> Some ((Num (Q.of_string (Hstring.view s))), no_reason) + | _ -> value_from_query e + + let value_to_expr (ty : Ty.t) (v : value) : expr = + debug "Type = %a@." Ty.print ty; + match v with + Bool true -> E._true + | Bool false -> E._false + | Num i -> + let i' = Q.to_string i in + if ty == Ty.Treal + then E.real i' + else E.int i' + + let arith + (ty : Ty.t) + (op : value -> value -> value) + (e_list : expr list): (expr list, expl) simp = + (* Wrapper for op. Checks that it has been called. + If it has never been called, then there have been no + simplification. *) + let op_has_been_called = ref 0 in + let op v1 v2 = + op_has_been_called := !op_has_been_called + 1 ; + debug "Calling operator@."; + op v1 v2 + in + + let vals,expl,exprs = + List.fold_left + (fun (acc_solved,acc_expl,acc_remain) v -> + match expr_to_value v with + None -> (acc_solved, acc_expl, v :: acc_remain) + | Some (v, expl) -> + let new_expl = Expl.union expl acc_expl in + match acc_solved with + None -> + (Some v, new_expl, acc_remain) + | Some old_v -> (Some (op old_v v), new_expl, acc_remain) + ) + (None, Expl.empty, []) + e_list + in + if !op_has_been_called = 0 + then + begin + debug "Operator has not been called.@."; + identity e_list + end + else + match vals with + None -> identity e_list + | Some v -> + let cst_expr = value_to_expr ty v in + debug "Result of simplifyable operations : %a@." E.pretty cst_expr; + {v = List.rev exprs @ [value_to_expr ty v]; diff = true; expl} + + let oper (op : value -> value -> bool) (l : expr list) : bool * bool * expl = + (* all_true is a boolean stating that every call of 'op' returned 'true'. + set to true at the beginning, it is set to false if one of the + list term. + last_val is the last value that has been accepted by the test + acc_expl is the accumulated explanations of each value tested + *) + let rec _oper + (all_true : bool) + (last_val : value option) + (acc_expl : expl) + (l : expr list) : bool * bool * expl = + match l with + [] -> (* No more elements, and none failed the test. *) + false, all_true, acc_expl + | hd :: tl -> + let hd_val = expr_to_value hd in + match hd_val, last_val with + | None, None -> + _oper false None acc_expl tl + + | Some (v, expl), None -> + _oper + all_true + (Some v) + (Expl.union expl acc_expl) + tl + + | None, Some v -> + _oper false (Some v) acc_expl tl + + | Some (v, expl), Some v' -> + let res = op v v' in + debug "Result : %a (op) %a = %b@." + pp_val v' pp_val v res; + if op v' v + then ( + _oper all_true (Some v') (Expl.union expl acc_expl) tl + ) + else (* The operation is not respected *) ( + true, false, (Expl.union expl acc_expl) + ) + in + _oper true None no_reason l + + let apply_op + (op : value -> value -> bool) + (l : expr list) : (expr list, expl) simp = + let falsify,all_true,expl = oper op l in + if falsify + then {v = [E._false]; diff = true; expl} + else if all_true + then {v = [E._true]; diff = true; expl} + else {v = l; diff = false; expl} + + let is_unary (o : Symbols.operator) : bool = + let open Symbols in + match o with + | Plus | Minus | Mult | Div | Modulo + | Concat | Extract | Get | Set | Fixed | Float + | Reach | Record | Min_real | Min_int | Max_real | Max_int + | Integer_log2 | Pow | Tite -> false + + | Access _ + | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil + | Sqrt_real_default | Sqrt_real_excess | Integer_round + | Constr _ + | Destruct (_,_) -> true + + let rec simp_expr (e : expr) : (expr, expl) simp = + if E.equal e E._true || E.equal e E._false + then ( + debug "Expression is trivial@."; + {v = e; diff = false; expl = no_reason} + ) + else + let query_res = value_from_query e in + match query_res with + | Some (q, expl) -> ( + let cst_exp = value_to_expr (E.get_type e) q in + debug "Theory found %a = %a@." + E.pretty e E.pretty cst_exp; + {v = cst_exp; diff = true; expl} + ) + | None -> + debug "Theory did not found an answer@."; + let ty = E.get_type e in + (* simp_expr treats 3 cases : either the expression is an operation, + a formula or a literal. + A function is dedicated to each of these cases, returning a + simplified list of subexpressions. + If this list contains only 1 element, it is either because + it has been simplified to 1 element or because it is an operation + over a single expression. *) + + (* The boolean states that the operation is a unary operation and + must be preserved. + Otherwise, it can be discarded. + For example, (3 + 2) is simplified to 5, the operator '+' can + be discarded. + However, in f(3 + 2), f must not be discarded. *) + let by_operator + (op : Symbols.operator) + (elist : expr list) : + (expr list, expl) simp * bool = + match op with + | Symbols.Plus -> arith ty (++) elist, false + | Symbols.Minus -> ( + match elist with + hd :: _ :: [] -> ( + (* in the case 0 - sthg, we don't want to do anything. *) + match E.get_comp hd with + | Int s + | Real s when Q.equal (Q.of_string (Hstring.view s)) Q.zero -> + identity elist, false + | _ -> arith ty ( -- ) elist, false + ) + | _ -> arith ty ( -- ) elist, false + ) + | Symbols.Mult -> arith ty ( ** ) elist, false + | Symbols.Tite -> ( + match elist with + cond :: th :: el :: [] -> + if E.(equal cond _true) + then {v = [th]; diff = true; expl = no_reason} + else if E.(equal cond _false) + then {v = [el]; diff = true; expl = no_reason} + else if E.equal th el + then {v = [th]; diff = true; expl = no_reason} + else identity elist + | _ -> assert false + ), false + | o -> identity elist, is_unary o in + + let by_form + (f : Symbols.form) + (elist : expr list) + : (expr list, expl) simp = + match f with + | Symbols.F_Unit _ -> (* <=> AND *) ( + let () = debug "F_Unit@." in + let res = + fold_left_stop + (fun acc e -> + if E.(equal e _true) + then ( + debug "%a = true@." E.pretty e; + {acc with diff = true}, false + ) + else if E.(equal e _false) + then ( + debug "%a = false@." E.pretty e; + {v = [E._false]; diff = true; expl = no_reason}, true + ) + else + ( + debug "Keeping %a@." E.pretty e; + {acc with v = (e :: acc.v)}, false + ) + ) + {v = []; diff= false; expl = no_reason} + elist + in + match res.v with + [] -> {v = [E._true]; diff = true; expl = no_reason} + | _ -> {res with v = List.rev res.v} + ) + | F_Clause _ -> (* <=> OR *) ( + let () = debug "F_Clause@." in + let res = + fold_left_stop + (fun acc e -> + if E.(equal e _false) + then ( + debug "%a = false@." E.pretty e; + {acc with diff = true}, false + ) + else if E.(equal e _true) + then ( + debug "%a = true@." E.pretty e; + {v = [E._true]; diff = true; expl = no_reason}, true + ) + else ( + debug "Keeping %a@." E.pretty e; + {acc with v = (e :: acc.v)}, false + ) + ) + {v = []; diff= false; expl = no_reason} + elist + in + match res.v with + [] -> {v = [E._false]; diff = true; expl = no_reason} + | _ -> {res with v = List.rev res.v} + ) + | _ -> + let () = debug "No additional simplification@." in identity elist + + and by_lit + (l : Symbols.lit) + (elist : expr list) : (expr list, expl) simp = + let is_constr (constr : Hstring.t) (e : expr) : bool option = + match E.get_comp e with + Op (Constr s') -> Some (Hstring.equal constr s') + | _ -> None + in + match l with + L_eq -> ( + let res = apply_op (|=) elist in + match res.v with + [] | _ :: [] -> res + | _ -> (* structural equality check *) + if + List.for_all + (fun elt -> E.equal elt @@ List.hd res.v) (List.tl res.v) + then + {v = [E._true]; diff = true; expl = no_reason} + else res + ) + | L_built LE -> apply_op (|<=) elist + | L_built LT -> apply_op (|<) elist + | L_neg_built LE -> apply_op (|>) elist + | L_neg_built LT -> apply_op (|>=) elist + | L_neg_built (IsConstr s) -> ( + match elist with + e :: [] -> ( + match is_constr s e with + None -> + debug + "%a is not explicitely the constructor %a,\ + leaving as is@." + E.pretty e + Hstring.print s + ; + identity elist + | Some true -> + debug + "%a is explicitely the constructor %a,\ + this is FALSE@." + E.pretty e + Hstring.print s; + {v = [E._false]; diff = true; expl = no_reason} + | Some false -> + debug + "%a is explicitely NOT the constructor %a,\ + this is TRUE@." + E.pretty e + Hstring.print s; + {v = [E._true]; diff = true; expl = no_reason} + ) + | _ -> assert false + ) + | L_neg_pred -> identity elist + | L_neg_eq -> apply_op (|<>) elist + + | L_built (IsConstr s) -> ( + match elist with + e :: [] -> ( + match is_constr s e with + None -> + debug + "%a is not explicitely the constructor %a,\ + leaving as is@." + E.pretty e + Hstring.print s + ; + identity elist + | Some true -> + debug + "%a is explicitely the constructor %a,\ + this is TRUE@." + E.pretty e + Hstring.print s; + {v = [E._true]; diff = true; expl = no_reason} + | Some false -> + debug + "%a is explicitely NOT the constructor %a,\ + this is FALSE@." + E.pretty e + Hstring.print s; + {v = [E._false]; diff = true; expl = no_reason} + ) + | _ -> assert false + ) + in + let elist = + (List.map (fun e -> simp_expr e)) (E.get_sub_expr e) in + let elist = diff_list elist in + let xs, may_be_unary_op = + let symb = E.get_comp e in + match symb with + Op o -> + debug + "Operator: %a@." + Symbols.print symb; + by_operator o elist.v + | Form f -> + debug + "Formula: %a@." + Symbols.print symb; + by_form f elist.v, false + | Lit l -> + debug + "Literal: %a@." + Symbols.print symb; + by_lit l elist.v, false + | Name _ -> + debug + "Name: %a@." + Symbols.print symb; + elist, true + | _ -> + debug + "Other: %a@." + Symbols.print symb; + elist, true + in + let diff = elist.diff || xs.diff in + let expl = Expl.union elist.expl xs.expl in + let v = + if not diff then e + else + match xs.v with + [] -> (* The simplification did something strange and discarded + everything. This should not happen. *) + debug + "Expression %a was discarded by simplifyer. Keeping it." + E.pretty e; + e + | elt :: [] when not (may_be_unary_op) -> + debug + "Expression %a is now %a.@." + E.pretty e E.pretty elt; + (* It usually means that the expression is trivial. *) + elt + | l -> E.mk_expr (E.get_comp e) l (E.get_type e) + in + {v; diff; expl} + + (** Wrapper of simp_expr for verbose *) + let simp_expr e = + try + debug "Simplifying %a@." E.pretty e; + let res = simp_expr e in + if res.diff + then + let () = + debug + "Old expression = %a@." + E.pretty e; + debug + "New expression = %a@." + E.pretty res.v in + res + else + let () = + debug + "No change on %a@." + E.pretty e + in + identity e + with + Failure s -> + talk + "Error while simplifying %a\n%s\n\ + I will continue with the initial expression@." + E.pretty e + s; + {v=e;diff=false;expl=no_reason} +end diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli new file mode 100644 index 0000000000..52ea849d35 --- /dev/null +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -0,0 +1,119 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2018 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +(** A simplified formula/expr/... type. + the diff field is set to false if the operation did not change the + input. +*) +type ('a,'expl) simp + +val get_expr : ('a, _) simp -> 'a +val has_changed : _ simp -> bool +val get_expl : (_, 'expl) simp -> 'expl + +(** As the simplifyer interacts with different components of alt-ergo, + it is written to be as generic as possible. + The simplifyer is then a functor of different modules which type is + defined below. +*) + +(** Expr is the signature of the module dedicated to + the representation of expressions that are to be + simplified. *) +module type Expr = +sig + type t + + val equal : t -> t -> bool + val mk_expr : Symbols.t -> t list -> Ty.t -> t + + (** Expressions are generally defined by 3 elements: + - a type + - a set of sub expressions + - a composition operator *) + val get_comp : t -> Symbols.t + val get_sub_expr : t -> t list + val get_type : t -> Ty.t + + val _true : t + val _false : t + + val real : string -> t + val int : string -> t + + val pretty : Format.formatter -> t -> unit +end + +(** Expl is the signature of the module dedicated to + the explanations of the calculations. *) +module type Expl = +sig + type t + + (** Represents no explanation. *) + val empty : t + + (** Tests if the explanation is empty *) + val is_empty : t -> bool + + (** Merges two explanations. *) + val union : t -> t -> t +end + +(** Th is the signature of the module dedicated to + the interactions with the theory. *) +module type Th = +sig + type expr + type env + type expl + + (** Empty environment. *) + val empty : unit -> env + + (** Tries to decide the expression in argument given the environment. + If it fails, returns None. Otherwise, provides the answer and + an explanation (possibly empty) + *) + val bool_query : expr -> env -> (bool * expl) option + + (** Tries to decide the arithmetic value of an expression given the + environment. + If it fails, returns None. Otherwise, provides the answer and + an explanation (possibly empty) *) + val q_query : expr -> env -> (Q.t * expl) option +end + +(** This is the signature of the simplifyer. *) +module type S = +sig + (** The type of expressions. *) + type expr + + (** The type of environments the theory works in. *) + type env + + (** The type of explanations *) + type expl + + (** Sets the environment to be used in the simplifyer. + Set to empty by default. *) + val set_env : env -> unit + + (** Simplifies an expression. *) + val simp_expr : expr -> (expr,expl) simp +end + +module SimpleReasoner + (E : Expr) + (Expl : Expl) + (T : Th with type expr = E.t and type expl = Expl.t) + : S with type expr = E.t and type env = T.env and type expl = Expl.t diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 4b04cddb22..792767e7f0 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -34,7 +34,6 @@ module SE = E.Set module ME = E.Map module Ex = Explanation - module Make (Th : Theory.S) : Sat_solver_sig.S = struct module Inst = Instances.Make(Th) module CDCL = Satml_frontend_hybrid.Make(Th) @@ -974,7 +973,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct nb_related_to_goal = t.nb_related_to_goal + 1; nb_related_to_hypo = t.nb_related_to_hypo + 1} - let rec asm_aux acc list = List.fold_left (fun @@ -1122,7 +1120,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct env.heuristics := Heuristics.bump_activity !(env.heuristics) expl; raise (IUnsat (expl, classes)) - let new_inst_level env = let new_ilevel = env.ilevel + 1 in let env = {env with ilevel = new_ilevel} in diff --git a/src/lib/reasoners/th_util.ml b/src/lib/reasoners/th_util.ml index e0bc7301c9..f1a13b5f2e 100644 --- a/src/lib/reasoners/th_util.ml +++ b/src/lib/reasoners/th_util.ml @@ -26,6 +26,8 @@ (* *) (******************************************************************************) +(** An answer type. If it is Some (thing), then the answer is yes, + otherwise it is unknown. *) type answer = (Explanation.t * Expr.Set.t list) option diff --git a/src/lib/reasoners/th_util.mli b/src/lib/reasoners/th_util.mli index e0bc7301c9..f1a13b5f2e 100644 --- a/src/lib/reasoners/th_util.mli +++ b/src/lib/reasoners/th_util.mli @@ -26,6 +26,8 @@ (* *) (******************************************************************************) +(** An answer type. If it is Some (thing), then the answer is yes, + otherwise it is unknown. *) type answer = (Explanation.t * Expr.Set.t list) option diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index 9cf6287a69..b1d58be6d4 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -31,7 +31,7 @@ open Typed (* Sat entry *) type sat_decl_aux = - | Assume of string * Expr.t * bool + | Assume of string * Expr.t * bool (* axioms / asserts *) | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t rwt_rule) list | Query of string * Expr.t * goal_sort diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index e77228dbe4..8c4d038e25 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -32,7 +32,7 @@ open Typed (* Sat entry *) type sat_decl_aux = - | Assume of string * Expr.t * bool + | Assume of string * Expr.t * bool (* axioms / asserts *) | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t rwt_rule) list | Query of string * Expr.t * goal_sort diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 6402eccfb8..7defd372e0 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -43,9 +43,9 @@ type t = view and view = { f: Sy.t; xs: t list; - ty: Ty.t; + ty: Ty.t; (* expression type *) bind : bind_kind; - tag: int; + tag: int; (* always = -42 *) vars : (Ty.t * int) SMap.t; (* vars to types and nb of occurences *) vty : Ty.Svty.t; depth: int; @@ -124,14 +124,14 @@ type lit_view = | Not_a_lit of { is_form : bool } type form_view = - | Unit of t*t (* unit clauses *) - | Clause of t*t*bool (* a clause (t1 or t2) bool <-> is implication *) + | Unit of t * t (* unit clauses *) + | Clause of t * t * bool (* a clause (t1 or t2) bool <-> is implication *) | Iff of t * t | Xor of t * t - | Literal of t (* an atom *) - | Lemma of quantified (* a lemma *) - | Skolem of quantified (* lazy skolemization *) - | Let of letin (* a binding of an expr *) + | Literal of t (* an atom *) + | Lemma of quantified (* a lemma *) + | Skolem of quantified (* lazy skolemization *) + | Let of letin (* a binding of an expr *) | Not_a_form @@ -2542,3 +2542,77 @@ type th_elt = let print_th_elt fmt t = Format.fprintf fmt "%s/%s: @[%a@]" t.th_name t.ax_name print t.ax_form + +module SimpExpr = + Simple_reasoner_expr.SimpleReasoner ( + struct + type t' = t + type t = t' + let equal = equal + + let mk_expr sy l typ = + match sy,l with + Sy.Form (Sy.F_Unit is_impl), f1 :: f2 :: [] -> + mk_and f1 f2 is_impl 0 + | Sy.Form (Sy.F_Unit _), _ -> + failwith "F_Unit not supported by simplifyer"; + + | Sy.Form (Sy.F_Clause is_impl), f1 :: f2 :: [] -> + mk_or f1 f2 is_impl 0 + | Sy.Form (Sy.F_Clause _), _ -> + failwith "F_Clause not supported by simplifyer"; + + | Sy.Form (Sy.F_Iff), [f1;f2] -> mk_iff f1 f2 0 + | Sy.Form (Sy.F_Iff), _ -> mk_nary_eq l + + | Sy.Form (Sy.F_Xor), f1 :: f2 :: [] -> mk_xor f1 f2 0 + | Sy.Form (Sy.F_Xor), _ -> + Format.eprintf "F_Xor not supported by simplifyer"; + assert false + + | Sy.Form (Sy.F_Lemma),_ + | Sy.Form (Sy.F_Skolem),_ -> failwith "Formula undefined." + + | Sy.Lit (Sy.L_eq),_ -> + mk_positive_lit sy (Sy.Lit (Sy.L_neg_eq)) l + | Sy.Lit (Sy.L_built b),_ -> + mk_positive_lit sy (Sy.Lit (Sy.L_neg_built b)) l + | Sy.Lit (Sy.L_neg_eq), _ -> + mk_positive_lit (Sy.Lit Sy.L_eq) (Sy.Lit Sy.L_neg_eq) l |> neg + | Sy.Lit (Sy.L_neg_built n), _ -> + mk_builtin ~is_pos:false n l + | Sy.Lit (Sy.L_neg_pred), _ -> + failwith "Lit (L_neg_pred) not supported by simplifyer" + | _ -> mk_term sy l typ + + let get_comp e = e.f + let get_sub_expr e = e.xs + let get_type e = e.ty + + let _true = vrai + let _false = faux + + let real = real + let int = int + + let pretty = print + end + ) + +module SimpExprDummy = + SimpExpr + (struct + type t = unit + let empty = () + let is_empty _ = true + let union _ _ = () + end) + (struct + type expr = t + type env = unit + type expl = unit + let empty _ = () + let bool_query _ _ = None + let q_query _ _ = None + end + ) diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index db7607e0d6..edbfa1ab6a 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -319,3 +319,20 @@ val is_pure : t -> bool val const_term : t -> bool (** return true iff the given argument is a term without arguments *) + +(** SimpExpr defines a simplifyer functor for expressions of type t + (defined in this file). *) +module SimpExpr : + functor + (Expl : Simple_reasoner_expr.Expl) + (T : Simple_reasoner_expr.Th with type expr = t and type expl = Expl.t) + -> Simple_reasoner_expr.S with type expr = t + and type env = T.env + and type expl = Expl.t + +(** Implementation of the simplifyer with no theory and no explanations. + This module can be used for agnostic simplification / preprocessing. *) +module SimpExprDummy : + Simple_reasoner_expr.S with type expr = t + and type env = unit + and type expl = unit diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 579148f18b..47032c4276 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -30,9 +30,10 @@ open Format open Options type builtin = - LE | LT (* arithmetic *) - | IsConstr of Hstring.t (* ADT tester *) + LE | LT (** Arithmetic *) + | IsConstr of Hstring.t (** ADT tester *) +(** Operators on integer and reals, plus constructors/destructors & ITEs *) type operator = Plus | Minus | Mult | Div | Modulo | Concat | Extract | Get | Set | Fixed | Float @@ -45,18 +46,20 @@ type operator = | Destruct of Hstring.t * bool | Tite +(** Literals : relations between values *) type lit = - (* literals *) | L_eq | L_built of builtin | L_neg_eq | L_neg_built of builtin | L_neg_pred +(** Formulas : composition of expressions *) type form = - (* formulas *) - | F_Unit of bool - | F_Clause of bool + | F_Unit of bool (** F_Unit b <=> (AND), + b = true => the formula was an implication *) + | F_Clause of bool (** F_Clause b <=> (OR), + b = true => the formula was an implication *) | F_Iff | F_Xor | F_Lemma @@ -69,7 +72,6 @@ type bound_kind = VarBnd of Var.t | ValBnd of Numbers.Q.t type bound = (* private *) { kind : bound_kind; sort : Ty.t; is_open : bool; is_lower : bool } - type t = | True | False diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 13b48e5487..3bf2726b5e 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -136,6 +136,22 @@ and 'a tlet_kind = | TletTerm of 'a atterm | TletForm of 'a atform +(** Toplevel common components *) + +let true_atatom = {c=TAtrue; annot = new_id ()} +let false_atatom = {c=TAfalse; annot = new_id ()} + +let true_tform = TFatom true_atatom +let false_tform = TFatom false_atatom + +let true_atform = {c = true_tform; annot = new_id()} +let false_atform = {c = false_tform; annot = new_id()} + +let true_term = {tt_desc = TTconst Ttrue; tt_ty=Ty.Tbool} +let false_term = {tt_desc = TTconst Tfalse; tt_ty=Ty.Tbool} + +let true_atterm = {c = true_term; annot = new_id ()} +let false_atterm = {c = false_term; annot = new_id ()} (** Rewrite rules *) @@ -189,6 +205,200 @@ and 'a tdecl = | TPush of Loc.t * int | TPop of Loc.t * int +let eq_list eq l1 l2 = + let rec loop l1 l2 = + match l1, l2 with + [],[] -> true + | hd1 :: tl1, hd2 :: tl2 -> + if eq hd1 hd2 + then loop tl1 tl2 + else false + | _,_ -> false + in loop l1 l2 + +let eq_tconstant (c1 : tconstant) (c2 : tconstant) : bool = + match c1, c2 with + Tint s1, Tint s2 + | Tbitv s1, Tbitv s2 -> String.equal s1 s2 + | Treal n1, Treal n2 -> Num.eq_num n1 n2 + | Ttrue, Ttrue | Tfalse, Tfalse | Tvoid, Tvoid -> true + | _ -> false + +let eq_pattern (p1 : pattern) (p2 : pattern) : bool = + match p1, p2 with + Constr {name = name1; args = args1}, + Constr {name = name2; args = args2} -> + Hstring.equal name1 name2 + && + eq_list + (fun (x1,s1,t1) (x2,s2,t2) -> + Var.equal x1 x2 && + Hstring.equal s1 s2 && + Ty.equal t1 t2) + args1 + args2 + + | Var x1, Var x2 -> Var.equal x1 x2 + | _,_ -> false + +let rec eq_tterm (t1 : 'a tterm) (t2 : 'a tterm) : bool = + Ty.equal t1.tt_ty t2.tt_ty && eq_tt_desc t1.tt_desc t2.tt_desc + +and eq_tt_desc (e1 : 'a tt_desc) (e2 : 'a tt_desc) : bool = + match e1, e2 with + TTconst c1, TTconst c2 -> eq_tconstant c1 c2 + | TTvar v1, TTvar v2 -> Symbols.equal v1 v2 + | TTinfix (t11, symb1, t12), TTinfix (t21, symb2, t22) -> + Symbols.equal symb1 symb2 && + eq_tterm t11.c t21.c && + eq_tterm t12.c t22.c + + | TTprefix (s1,t1), TTprefix (s2, t2) -> + Symbols.equal s1 s2 && + eq_tterm t1.c t2.c + + | TTapp (s1, l1), TTapp (s2, l2) -> + Symbols.equal s1 s2 && + eq_list + (fun t1 t2 -> eq_tterm t1.c t2.c) + l1 l2 + + | TTmapsTo (x1, t1), TTmapsTo (x2, t2) -> + Var.equal x1 x2 && + eq_tterm t1.c t2.c + + | TTget (t11, t12), TTget (t21, t22) + | TTconcat (t11, t12), TTconcat (t21, t22) -> + eq_tterm t11.c t21.c && + eq_tterm t12.c t22.c + + | TTset (t11, t12, t13), TTset (t21, t22, t23) + | TTextract (t11, t12, t13), TTextract (t21, t22, t23) -> + eq_tterm t11.c t21.c && + eq_tterm t12.c t22.c && + eq_tterm t13.c t23.c + + | TTdot (t1, s1), TTdot (t2, s2) + | TTnamed (s1, t1), TTnamed (s2, t2) -> + Hstring.equal s1 s2 && + eq_tterm t1.c t2.c + + | TTrecord l1, TTrecord l2 -> + eq_list + (fun (s1,t1) (s2,t2) -> Hstring.equal s1 s2 && eq_tterm t1.c t2.c) + l1 l2 + + | TTlet (l1, t1), TTlet (l2, t2) -> + eq_tterm t1.c t2.c && + eq_list + (fun (s1, t1) (s2, t2) -> + Symbols.equal s1 s2 && eq_tterm t1.c t2.c) + l1 + l2 + + | TTite (c1,th1,el1), TTite (c2,th2,el2) -> + eq_tform c1.c c2.c && eq_tterm th1.c th2.c && eq_tterm el1.c el2.c + + | TTproject (b1,t1,s1), TTproject (b2,t2,s2) -> + (b1 && (not b2) || (not b1) && b2) + && eq_tterm t1.c t2.c && Hstring.equal s1 s2 + + | TTmatch (t1, l1), TTmatch (t2, l2) -> + eq_tterm t1.c t2.c && + eq_list + (fun (p1,t1) (p2,t2) -> + eq_pattern p1 p2 && eq_tterm t1.c t2.c + ) + l1 + l2 + + | TTform f1, TTform f2 -> eq_tform f1.c f2.c + | _,_ -> false + +and eq_tatom (a1 : 'a tatom) (a2 : 'a tatom) : bool = + match a1, a2 with + TAtrue, TAtrue + | TAfalse, TAfalse -> true + | TAeq l1, TAeq l2 + | TAdistinct l1, TAdistinct l2 + | TAneq l1, TAneq l2 + | TAle l1, TAle l2 + | TAlt l1, TAlt l2 -> + eq_list + (fun t1 t2 -> eq_tterm t1.c t2.c) + l1 + l2 + | TApred (t1, b1), TApred (t2, b2) -> + (b1 && (not b2) || (not b1) && b2) && + eq_tterm t1.c t2.c + | TTisConstr (t1, s1), TTisConstr (t2, s2) -> + Hstring.equal s1 s2 && eq_tterm t1.c t2.c + | _,_ -> false + +and eq_quant_form (q1 : 'a quant_form) (q2 : 'a quant_form) : bool = + let stylist = + eq_list + (fun (s1,t1) (s2, t2) -> Symbols.equal s1 s2 && Ty.equal t1 t2) + in + stylist q1.qf_bvars q2.qf_bvars && + stylist q1.qf_upvars q2.qf_upvars && + eq_list (fun f1 f2 -> eq_tform f1.c f2.c) q1.qf_hyp q2.qf_hyp && + eq_tform q1.qf_form.c q2.qf_form.c && + eq_list + (fun (tlist1,b1) (tlist2,b2) -> + (b1 && (not b2) || (not b1) && b2) && + eq_list + (fun t1 t2 -> eq_tterm t1.c t2.c) + tlist1 + tlist2) + q1.qf_triggers + q2.qf_triggers + +and eq_tform (f1 : 'a tform) (f2 : 'a tform) : bool = + match f1, f2 with + | TFatom a1, TFatom a2 -> eq_tatom a1.c a2.c + + | TFop (op1, l1), TFop (op2, l2) -> + (Stdlib.(=)) op1 op2 && + eq_list + (fun f1 f2 -> eq_tform f1.c f2.c) + l1 + l2 + + | TFforall q1, TFforall q2 + | TFexists q1, TFexists q2 -> + eq_quant_form q1 q2 + + | TFlet (stlist1, slklist1,f1), TFlet (stlist2, slklist2,f2) -> + let stylist = + eq_list + (fun (s1,t1) (s2, t2) -> Symbols.equal s1 s2 && Ty.equal t1 t2) + in + stylist stlist1 stlist2 && + eq_list + (fun (s1,lf1) (s2, lf2) -> Symbols.equal s1 s2 && eq_tlet_kind lf1 lf2) + slklist1 slklist2 + && + eq_tform f1.c f2.c + + | TFnamed (s1, f1), TFnamed (s2, f2) -> + Hstring.equal s1 s2 && eq_tform f1.c f2.c + + | TFmatch (t1, pfl1), TFmatch (t2, pfl2) -> + eq_tterm t1.c t2.c && + eq_list + (fun (p1, f1) (p2, f2) -> eq_pattern p1 p2 && eq_tform f1.c f2.c) + pfl1 + pfl2 + + | _,_ -> false + +and eq_tlet_kind (k1 : 'a tlet_kind) (k2 : 'a tlet_kind) : bool = + match k1, k2 with + TletTerm t1, TletTerm t2 -> eq_tterm t1.c t2.c + | TletForm f1, TletForm f2 -> eq_tform f1.c f2.c + | _,_ -> false + (*****) let string_of_op = function @@ -196,164 +406,211 @@ let string_of_op = function | OPor -> "or" | OPimp -> "->" | OPiff -> "<->" + | OPxor -> "xor" + | OPif -> "ite" | _ -> assert false +type 'annot annot_printer = Format.formatter -> 'annot -> unit +type ('a,'annot) annoted_printer = + Format.formatter -> ('a,'annot) annoted -> unit + +let (no_print : _ annot_printer) = fun fmt _ -> fprintf fmt "" +let (int_print : int annot_printer) = fun fmt -> fprintf fmt ".%i" + +let print_annot + (pp_annot : 'annot annot_printer) + (print : ('a,'annot) annoted_printer) + (fmt : Format.formatter) (t : ('a, 'annot) annoted) = + fprintf fmt "%a%a" print t pp_annot t.annot + let print_binder fmt (s, t) = fprintf fmt "%a :%a" Symbols.print s Ty.print t let print_binders fmt l = List.iter (fun c -> fprintf fmt "%a, " print_binder c) l -let rec print_term fmt t = match t.c.tt_desc with - | TTconst Ttrue -> - fprintf fmt "true" - | TTconst Tfalse -> - fprintf fmt "false" - | TTconst Tvoid -> - fprintf fmt "void" - | TTconst (Tint n) -> - fprintf fmt "%s" n - | TTconst (Treal n) -> - fprintf fmt "%s" (Num.string_of_num n) - | TTconst Tbitv s -> - fprintf fmt "%s" s - | TTvar s -> - fprintf fmt "%a" Symbols.print s - | TTapp(s,l) -> - fprintf fmt "%a(%a)" Symbols.print s print_term_list l - | TTinfix(t1,s,t2) -> - fprintf fmt "%a %a %a" print_term t1 Symbols.print s print_term t2 - | TTprefix (s, t') -> - fprintf fmt "%a %a" Symbols.print s print_term t' - | TTget (t1, t2) -> - fprintf fmt "%a[%a]" print_term t1 print_term t2 - | TTset (t1, t2, t3) -> - fprintf fmt "%a[%a<-%a]" print_term t1 print_term t2 print_term t3 - | TTextract (t1, t2, t3) -> - fprintf fmt "%a^{%a,%a}" print_term t1 print_term t2 print_term t3 - | TTconcat (t1, t2) -> - fprintf fmt "%a @ %a" print_term t1 print_term t2 - | TTdot (t1, s) -> - fprintf fmt "%a.%s" print_term t1 (Hstring.view s) - | TTrecord l -> - fprintf fmt "{ "; - List.iter - (fun (s, t) -> fprintf fmt "%s = %a" (Hstring.view s) print_term t) l; - fprintf fmt " }" - | TTlet (binders, t2) -> - fprintf fmt "let %a in %a" print_term_binders binders print_term t2 - | TTnamed (_, t) -> - fprintf fmt "%a" print_term t - - | TTinInterval(e, i, j) -> - fprintf fmt "%a in %a, %a" - print_term e - Symbols.print_bound i - Symbols.print_bound j - - | TTmapsTo(x,e) -> - fprintf fmt "%a |-> %a" Var.print x print_term e - - | TTite(cond, t1, t2) -> - fprintf fmt "(if %a then %a else %a)" - print_formula cond print_term t1 print_term t2 - | TTproject (grded, t1, s) -> - fprintf fmt "%a#%s%s" - print_term t1 (if grded then "" else "!") (Hstring.view s) - - | TTform f -> - fprintf fmt "%a" print_formula f - - | TTmatch (e, cases) -> - let pp_vars fmt l = - match l with - [] -> () - | [e,_,_] -> Var.print fmt e - | (e,_,_) :: l -> - fprintf fmt "(%a" Var.print e; - List.iter (fun (e,_,_) -> fprintf fmt ", %a" Var.print e) l; - fprintf fmt ")" - in - fprintf fmt "match %a with\n" print_term e; - List.iter - (fun (p, v) -> - match p with - | Constr {name = n; args = l} -> - fprintf fmt "| %a %a -> %a\n" Hstring.print n pp_vars l print_term v - | Var x -> - fprintf fmt "| %a -> %a\n" Var.print x print_term v; - )cases; - fprintf fmt "end@." - -and print_term_binders fmt l = +let rec print_term ?(annot=no_print) fmt t = + let printer fmt t = + match t.c.tt_desc with + | TTconst Ttrue -> + fprintf fmt "true" + | TTconst Tfalse -> + fprintf fmt "false" + | TTconst Tvoid -> + fprintf fmt "void" + | TTconst (Tint n) -> + fprintf fmt "%s" n + | TTconst (Treal n) -> + fprintf fmt "%s" (Num.string_of_num n) + | TTconst Tbitv s -> + fprintf fmt "%s" s + | TTvar s -> + fprintf fmt "%a" Symbols.print s + | TTapp(s,l) -> + fprintf fmt "%a(%a)" Symbols.print s (print_term_list ~annot) l + | TTinfix(t1,s,t2) -> + fprintf + fmt + "%a %a %a" + (print_term ~annot) t1 + Symbols.print s + (print_term ~annot) t2 + | TTprefix (s, t') -> + fprintf fmt "%a %a" Symbols.print s (print_term ~annot) t' + | TTget (t1, t2) -> + fprintf fmt "%a[%a]" (print_term ~annot) t1 (print_term ~annot) t2 + | TTset (t1, t2, t3) -> + fprintf + fmt + "%a[%a<-%a]" + (print_term ~annot) t1 + (print_term ~annot) t2 + (print_term ~annot) t3 + | TTextract (t1, t2, t3) -> + fprintf + fmt + "%a^{%a,%a}" + (print_term ~annot) t1 + (print_term ~annot) t2 + (print_term ~annot) t3 + | TTconcat (t1, t2) -> + fprintf fmt "%a @ %a" (print_term ~annot) t1 (print_term ~annot) t2 + | TTdot (t1, s) -> + fprintf fmt "%a.%s" (print_term ~annot) t1 (Hstring.view s) + | TTrecord l -> + fprintf fmt "{ "; + List.iter + (fun (s, t) -> + fprintf fmt "%s = %a" (Hstring.view s) (print_term ~annot) t) l; + fprintf fmt " }" + | TTlet (binders, t2) -> + fprintf + fmt + "let %a in %a" + (print_term_binders ~annot) binders + (print_term ~annot) t2 + | TTnamed (_, t) -> + fprintf fmt "%a" (print_term ~annot) t + + | TTinInterval(e, i, j) -> + fprintf fmt "%a in %a, %a" + (print_term ~annot) e + Symbols.print_bound i + Symbols.print_bound j + + | TTmapsTo(x,e) -> + fprintf fmt "%a |-> %a" Var.print x (print_term ~annot) e + + | TTite(cond, t1, t2) -> + fprintf fmt "(if %a then %a else %a)" + (print_formula ~annot) cond + (print_term ~annot) t1 + (print_term ~annot) t2 + | TTproject (grded, t1, s) -> + fprintf fmt "%a#%s%s" + (print_term ~annot) t1 (if grded then "" else "!") (Hstring.view s) + + | TTform f -> + fprintf fmt "%a" (print_formula ~annot) f + + | TTmatch (e, cases) -> + let pp_vars fmt l = + match l with + [] -> () + | [e,_,_] -> Var.print fmt e + | (e,_,_) :: l -> + fprintf fmt "(%a" Var.print e; + List.iter (fun (e,_,_) -> fprintf fmt ", %a" Var.print e) l; + fprintf fmt ")" + in + fprintf fmt "match %a with\n" (print_term ~annot) e; + List.iter + (fun (p, v) -> + match p with + | Constr {name = n; args = l} -> + fprintf + fmt + "| %a %a -> %a\n" + Hstring.print n + pp_vars l + (print_term ~annot) v + | Var x -> + fprintf fmt "| %a -> %a\n" Var.print x (print_term ~annot) v; + )cases; + fprintf fmt "end@." + in + print_annot annot printer fmt t + +and print_term_binders ?(annot=no_print) fmt l = match l with | [] -> assert false | (sy, t) :: l -> - fprintf fmt "%a = %a" Symbols.print sy print_term t; + fprintf fmt "%a = %a" Symbols.print sy (print_term ~annot) t; List.iter (fun (sy, t) -> - fprintf fmt ", %a = %a" Symbols.print sy print_term t) l + fprintf fmt ", %a = %a" Symbols.print sy (print_term ~annot) t) l -and print_term_list fmt = List.iter (fprintf fmt "%a," print_term) +and print_term_list ?(annot=no_print) fmt = List.iter (fprintf fmt "%a," (print_term ~annot)) -and print_atom fmt a = +and print_atom ?(annot=no_print) fmt a = match a.c with | TAtrue -> fprintf fmt "True" | TAfalse -> fprintf fmt "True" | TAeq [t1; t2] -> - fprintf fmt "%a = %a" print_term t1 print_term t2 + fprintf fmt "%a = %a" (print_term ~annot) t1 (print_term ~annot) t2 | TAneq [t1; t2] -> - fprintf fmt "%a <> %a" print_term t1 print_term t2 + fprintf fmt "%a <> %a" (print_term ~annot) t1 (print_term ~annot) t2 | TAle [t1; t2] -> - fprintf fmt "%a <= %a" print_term t1 print_term t2 + fprintf fmt "%a <= %a" (print_term ~annot) t1 (print_term ~annot) t2 | TAlt [t1; t2] -> - fprintf fmt "%a < %a" print_term t1 print_term t2 + fprintf fmt "%a < %a" (print_term ~annot) t1 (print_term ~annot) t2 | TApred (t, negated) -> - if negated then fprintf fmt "(not (%a))" print_term t - else print_term fmt t + if negated then fprintf fmt "(not (%a))" (print_term ~annot) t + else (print_term ~annot) fmt t | TTisConstr (t1, s) -> - fprintf fmt "%a ? %s" print_term t1 (Hstring.view s) + fprintf fmt "%a ? %s" (print_term ~annot) t1 (Hstring.view s) | TAdistinct l -> - fprintf fmt "distinct(%a)" print_term_list l + fprintf fmt "distinct(%a)" (print_term_list ~annot) l | _ -> assert false -and print_triggers fmt l = - List.iter (fun (tr, _) -> fprintf fmt "%a | " print_term_list tr) l +and print_triggers ?(annot=no_print) fmt l = + List.iter (fun (tr, _) -> fprintf fmt "%a | " (print_term_list ~annot) tr) l -and print_formula fmt f = +and print_formula ?(annot=no_print) fmt f = match f.c with | TFatom a -> print_atom fmt a | TFop(OPnot, [f]) -> - fprintf fmt "not %a" print_formula f + fprintf fmt "not %a" (print_formula ~annot) f | TFop(OPif, [cond; f1;f2]) -> fprintf fmt "if %a then %a else %a" - print_formula cond print_formula f1 print_formula f2 + (print_formula ~annot) cond (print_formula ~annot) f1 (print_formula ~annot) f2 | TFop(op, [f1; f2]) -> - fprintf fmt "%a %s %a" print_formula f1 (string_of_op op) print_formula f2 + fprintf fmt "%a %s %a" (print_formula ~annot) f1 (string_of_op op) (print_formula ~annot) f2 | TFforall { qf_bvars = l; qf_triggers = t; qf_form = f; _ } -> fprintf fmt "forall %a [%a]. %a" - print_binders l print_triggers t print_formula f + print_binders l (print_triggers ~annot) t (print_formula ~annot) f | TFlet (_, binders, f) -> List.iter (fun (sy, let_e) -> fprintf fmt " let %a = " Symbols.print sy; match let_e with - | TletTerm t -> fprintf fmt "%a in@." print_term t - | TletForm f -> fprintf fmt "%a in@." print_formula f + | TletTerm t -> fprintf fmt "%a in@." (print_term ~annot) t + | TletForm f -> fprintf fmt "%a in@." (print_formula ~annot) f )binders; - fprintf fmt "%a" print_formula f + fprintf fmt "%a" (print_formula ~annot) f | _ -> fprintf fmt "(formula pprint not implemented)" (* let rec print_tdecl fmt = function + | TTheory (_, name, _, l) -> Format.fprintf fmt "th %s: @[%a@]" name (Util.print_list_pp ~sep:Format.pp_print_space ~pp:print_atdecl) l - | TAxiom (_, name, kind, f) -> - Format.fprintf fmt "ax %s: @[%a@]" name print_formula f + | TAxiom (_, name, _kind, f) -> + Format.fprintf fmt "ax %s: @[%a@]" name (print_formula ~annot) f | TRewriting (_, name, l) -> Format.fprintf fmt "rwt %s: @[%a@]" name (Util.print_list_pp ~sep:Format.pp_print_space @@ -365,7 +622,8 @@ let rec print_tdecl fmt = function | TPop (_loc,n) -> Format.fprintf fmt "pop %d" n -and print_atdecl fmt a = print_tdecl fmt a.c +and print_atdecl ?(annot=no_print) fmt a = + print_annot annot (fun fmt a -> print_tdecl ~annot fmt a.c) fmt a *) let fresh_hypothesis_name = diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli index ea03e419ef..e21aaa0bd4 100644 --- a/src/lib/structures/typed.mli +++ b/src/lib/structures/typed.mli @@ -306,24 +306,85 @@ and 'a tdecl = (* TODO: wrap this in a record to factorize away the location and name of the declaration ? *) +(** {5. Toplevel constants} *) +val true_atatom : int atatom +val false_atatom : int atatom -(** {5 Printing} *) +val true_tform : int tform +val false_tform : int tform -val print_term : Format.formatter -> _ atterm -> unit -(** Print annoted typed terms. Ignore the annotations. *) +val true_atform : int atform +val false_atform : int atform -val print_formula : Format.formatter -> _ atform -> unit -(**Print annoted typed formulas; Ignores the annotations. *) +val true_term : int tterm +val false_term : int tterm + +val true_atterm : int atterm +val false_atterm : int atterm + +(** {6. Structural equality} *) + +val eq_tterm : 'a tterm -> 'a tterm -> bool + +val eq_tt_desc : 'a tt_desc -> 'a tt_desc -> bool + +val eq_tatom : 'a tatom -> 'a tatom -> bool + +val eq_quant_form : 'a quant_form -> 'a quant_form -> bool + +val eq_tform : 'a tform -> 'a tform -> bool + +val eq_tlet_kind : 'a tlet_kind -> 'a tlet_kind -> bool + +(** {7 Printing} *) + +val string_of_op : oplogic -> string + +type 'annot annot_printer = Format.formatter -> 'annot -> unit +type ('a,'annot) annoted_printer = + Format.formatter -> ('a,'annot) annoted -> unit + +val no_print : _ annot_printer +val int_print : int annot_printer + +val print_atom : + ?annot: 'annot annot_printer -> Format.formatter -> 'annot atatom -> unit + +(** Print annoted typed terms. If no annot function is given, ignores + the annotations. *) +val print_term : + ?annot: 'annot annot_printer -> Format.formatter -> 'annot atterm -> unit + +(** Print annoted typed formulas. If no annot function is given, ignores + the annotations. *) +val print_formula : + ?annot: 'annot annot_printer -> Format.formatter -> 'annot atform -> unit -val print_binders : Format.formatter -> (Symbols.t * Ty.t) list -> unit (** Print a list of bound typed variables. *) +val print_binders : Format.formatter -> (Symbols.t * Ty.t) list -> unit -val print_triggers : Format.formatter -> ('a atterm list * bool) list -> unit +val print_triggers : + ?annot: 'annot annot_printer -> + Format.formatter -> ('annot atterm list * bool) list -> unit (** Print a list of triggers. *) val print_goal_sort : Format.formatter -> goal_sort -> unit (** Print a goal sort *) +(* +val print_tdecl : + ?annot: 'annot annot_printer -> + Format.formatter -> 'annot tdecl -> unit + +val print_atdecl : + ?annot: 'annot annot_printer -> Format.formatter -> 'annot atdecl -> unit +*) + +val print_annot : + 'annot annot_printer -> + ('a,'annot) annoted_printer -> + Format.formatter -> ('a,'annot) annoted -> unit + val print_rwt : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a rwt_rule -> unit diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index d1d237a1e7..5493b476da 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -485,6 +485,9 @@ let status = ref Status_Unknown let session_file = ref "" let used_context_file = ref "" let js_mode = ref false +let simplify = ref Util.SNo +let simplify_th = ref true +let simplify_verbose = ref true let set_timers b = timers := b let set_status s = status := match_known_status s @@ -492,6 +495,9 @@ let set_file f = file := f let set_session_file f = session_file := f let set_used_context_file f = used_context_file := f let set_js_mode b = js_mode := b +let set_simplify s = simplify := s +let set_simplify_th b = simplify_th := b +let set_simplify_verbose b = simplify_verbose := b let get_timers () = !timers || !profiling let get_file () = !file @@ -499,6 +505,9 @@ let get_status () = !status let get_session_file () = !session_file let get_used_context_file () = !used_context_file let get_js_mode () = !js_mode +let get_simplify () = !simplify +let get_simplify_th () = !simplify_th +let get_simplify_verbose () = !simplify_verbose (** particular getters : functions that are immediately executed **************) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 308dbaae60..b166ca53f9 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -274,6 +274,15 @@ val set_file : string -> unit (** Updates the filename to be parsed and sets a js_mode flag *) val set_file_for_js : string -> unit +(** Set [simplify] accessible with {!val:get_simplify} *) +val set_simplify : Util.simplify -> unit + +(** Set [simplify_th] accessible with {!val:get_simplify_th} *) +val set_simplify_th : bool -> unit + +(** Set [simplify_verbose] accessible with {!val:get_simplify_verbose} *) +val set_simplify_verbose : bool -> unit + (** Setters used by parse_command *) (** Set [case_split_policy] accessible with {!val:get_case_split_policy} *) @@ -962,6 +971,18 @@ val get_status : unit -> known_status val get_js_mode : unit -> bool (** Default to [false] *) +(** [true] if simplification is activated *) +val get_simplify : unit -> Util.simplify +(** Default to [true] *) + +(** Gets the simplify mode: [false] => no theory used *) +val get_simplify_th : unit -> bool +(** Default to [true] *) + +(** Gets the simplify verbose mode: [false] => no verbose *) +val get_simplify_verbose : unit -> bool +(** Default to [false] *) + (** Value specifying the file given to Alt-Ergo *) val get_file : unit -> string (** Default to [""] *) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index 672173403d..1815cda8a2 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -54,6 +54,11 @@ type theories_extensions = | NIA | FPA +type simplify = + | SNo + | SPreprocess + | SAll + type axiom_kind = Default | Propagator let th_ext_of_string ext = diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 65699b9b38..3c95df223a 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -49,6 +49,11 @@ type theories_extensions = | NIA | FPA +type simplify = + | SNo + | SPreprocess + | SAll + type axiom_kind = Default | Propagator val th_ext_of_string : string -> theories_extensions option diff --git a/src/parsers/psmt2_to_alt_ergo.ml b/src/parsers/psmt2_to_alt_ergo.ml index a612908d98..93edd24d21 100644 --- a/src/parsers/psmt2_to_alt_ergo.ml +++ b/src/parsers/psmt2_to_alt_ergo.ml @@ -512,6 +512,7 @@ let file_parser token lexbuf = let lexpr_parser token lexbuf = Translate.lexpr (Smtlib_parser.term token lexbuf) +(*|> Simple_reasoner.simplify_boolean_expr *) let trigger_parser token lexbuf = Translate.trigger (Smtlib_parser.term_list token lexbuf)