From 8ea095d515fbadc297f763a2ecf457500171029d Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 22 May 2019 11:22:54 +0200 Subject: [PATCH] Arithmetic queries on simplifyer --- sources/lib/frontend/cnf.ml | 6 +- sources/lib/frontend/simple_reasoner_expr.ml | 64 ++++++++++++------- sources/lib/frontend/simple_reasoner_expr.mli | 15 ++++- sources/lib/structures/expr.ml | 3 +- 4 files changed, 62 insertions(+), 26 deletions(-) diff --git a/sources/lib/frontend/cnf.ml b/sources/lib/frontend/cnf.ml index ba7963cc3..bdae28d2c 100644 --- a/sources/lib/frontend/cnf.ml +++ b/sources/lib/frontend/cnf.ml @@ -48,7 +48,8 @@ module DummySimp: type expl = Explanation.t type env = Theory.Main_Default.t let empty = Theory.Main_Default.empty - let query _ _ = None + let bool_query _ _ = None + let q_query _ _ = None end ) @@ -63,13 +64,14 @@ module ThSimp : Simple_reasoner_expr.S with type expr = Expr.t type expl = Explanation.t type env = Theory.Main_Default.t let empty = Theory.Main_Default.empty - let query ex env = + let bool_query ex env = try match Theory.Main_Default.query ex env with Some (expl,_) -> Some (true, expl) | None -> None with _ -> Format.eprintf "Query failed on %a@." Expr.print ex; None + let q_query _ _ = None (* Todo : add arithmetic solving *) end ) diff --git a/sources/lib/frontend/simple_reasoner_expr.ml b/sources/lib/frontend/simple_reasoner_expr.ml index 98eacc578..e9ea63ba0 100644 --- a/sources/lib/frontend/simple_reasoner_expr.ml +++ b/sources/lib/frontend/simple_reasoner_expr.ml @@ -77,8 +77,6 @@ let (|>=) v1 v2 = | 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. *) @@ -174,14 +172,21 @@ sig type env type expl - (** An empty environment. Know nothing. *) + (** 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 query : expr -> env -> (bool * expl) option + 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. *) @@ -235,19 +240,39 @@ struct 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) - | _ -> - if E.get_type e = Ty.Tbool then - match T.query e !env with - Some (res_query, expl) -> - Some ((Bool res_query), expl) - | None -> None - else None + | _ -> value_from_query e let value_to_expr (ty : Ty.t) (v : value) : expr = debug "Type = %a@." Ty.print ty; @@ -379,18 +404,13 @@ struct {v = e; diff = false; expl = no_reason} ) else - let query_res = - if E.get_type e = Ty.Tbool - then T.query e !env - else None in + let query_res = value_from_query e in match query_res with - Some (true, expl) -> ( - debug "Theory found it is true@."; - {v = E.vrai; diff = true; expl} - ) - | Some (false, expl) -> ( - debug "Theory found it is false@."; - {v = E.faux; diff = true; expl} + | 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@."; diff --git a/sources/lib/frontend/simple_reasoner_expr.mli b/sources/lib/frontend/simple_reasoner_expr.mli index d551fc30a..2114a8e10 100644 --- a/sources/lib/frontend/simple_reasoner_expr.mli +++ b/sources/lib/frontend/simple_reasoner_expr.mli @@ -68,8 +68,21 @@ sig type expr type env type expl + + (** Empty environment. *) val empty : unit -> env - val query : expr -> env -> (bool * expl) option + + (** 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. *) diff --git a/sources/lib/structures/expr.ml b/sources/lib/structures/expr.ml index 7eb343350..e265ab828 100644 --- a/sources/lib/structures/expr.ml +++ b/sources/lib/structures/expr.ml @@ -2563,6 +2563,7 @@ module SimpExprDummy = type env = unit type expl = unit let empty _ = () - let query _ _ = None + let bool_query _ _ = None + let q_query _ _ = None end )