Skip to content

Commit

Permalink
Simplify numerical expressions in SMT-LIB printers
Browse files Browse the repository at this point in the history 
The modifications done in PR #970 are to risky for what we need. This
commit simplifies some numerical expressions printed in the SMT-LIB format.
The simplifcations are as follows:

`0 + x -> x`
`x + 0 -> x`
`1 * x -> x`
`x * 1 -> x`
`(0 - 1) * x -> 0 - x`
`x * (0 - 1) -> 0 - x`
`x / 1 -> x`
`x / (-1) -> 0 - x`
  • Loading branch information
@Halbaroth
Halbaroth committed Nov 27, 2023
1 parent a8e0298 commit 29720fd
Showing 1 changed file with 194 additions and 145 deletions.
339 changes: 194 additions & 145 deletions src/lib/structures/expr.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -308,10 +308,177 @@ module F_Htbl : Hashtbl.S with type key = t =
let equal = equal
end)

let neg t =
match t with
| { ty = Ty.Tbool; neg = Some n; _ } -> n
| { f = _; _ } -> assert false

let is_int t = t.ty == Ty.Tint
let is_real t = t.ty == Ty.Treal

let merge_vars acc b =
SMap.merge (fun sy a b ->
match a, b with
| None, None -> assert false
| Some _, None -> a
| None, Some _ -> b
| Some (ty, x), Some (ty', y) ->
assert (Ty.equal ty ty' || Sy.equal sy Sy.underscore);
Some (ty, x + y)
) acc b

let free_vars t acc = merge_vars acc t.vars

let free_type_vars t = t.vty

let is_ground t =
SMap.is_empty (free_vars t SMap.empty) &&
Ty.Svty.is_empty (free_type_vars t)

let size t = t.nb_nodes

let depth t = t.depth

(** smart constructors for terms *)

let free_vars_non_form s l ty =
match s, l with
| Sy.Var _, [] -> SMap.singleton s (ty, 1)
| Sy.Var _, _ -> assert false
| Sy.Form _, _ -> assert false (* not correct for quantified and Lets *)
| _, [] -> SMap.empty
| _, e::r -> List.fold_left (fun s t -> merge_vars s t.vars) e.vars r

let free_type_vars_non_form l ty =
List.fold_left (fun acc t -> Ty.Svty.union acc t.vty) (Ty.vty_of ty) l

let is_ite s = match s with
| Sy.Op Sy.Tite -> true
| _ -> false

let mk_term s l ty =
assert (match s with Sy.Lit _ | Sy.Form _ -> false | _ -> true);
let d = match l with
| [] ->
1 (*no args ? depth = 1 (ie. current app s, ie constant)*)
| _ ->
(* if args, d is 1 + max_depth of args (equals at least to 1 *)
1 + List.fold_left (fun z t -> max z t.depth) 1 l
in
let nb_nodes = List.fold_left (fun z t -> z + t.nb_nodes) 1 l in
let vars = free_vars_non_form s l ty in
let vty = free_type_vars_non_form l ty in
let pure = List.for_all (fun e -> e.pure) l && not (is_ite s) in
let pos =
HC.make {f=s; xs=l; ty=ty; depth=d; tag= -42; vars; vty;
nb_nodes; neg = None; bind = B_none; pure}
in
if ty != Ty.Tbool then pos
else if pos.neg != None then pos
else
let neg_s = Sy.Lit Sy.L_neg_pred in
let neg =
HC.make {f=neg_s; xs=[pos]; ty=ty; depth=d; tag= -42;
vars; vty; nb_nodes; neg = None; bind = B_none; pure = false}
in
assert (neg.neg == None);
pos.neg <- Some neg;
neg.neg <- Some pos;
pos

let vrai =
let res =
let nb_nodes = 0 in
let vars = SMap.empty in
let vty = Ty.Svty.empty in
let faux =
HC.make
{f = Sy.False; xs = []; ty = Ty.Tbool; depth = -2; (*smallest depth*)
tag = -42; vars; vty; nb_nodes; neg = None; bind = B_none;
pure = true}
in
let vrai =
HC.make
{f = Sy.True; xs = []; ty = Ty.Tbool; depth = -1; (*2nd smallest d*)
tag= -42; vars; vty; nb_nodes; neg = None; bind = B_none;
pure = true}
in
assert (vrai.neg == None);
assert (faux.neg == None);
vrai.neg <- Some faux;
faux.neg <- Some vrai;
vrai
in
res

let faux = neg (vrai)
let void = mk_term (Sy.Void) [] Ty.Tunit

let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty

let is_internal_name t =
match t with
| { f; xs = []; _ } -> Sy.is_fresh_internal_name f
| _ -> false

let is_internal_skolem t = Sy.is_fresh_skolem t.f

let positive_int i = mk_term (Sy.int i) [] Ty.Tint

let int i =
let len = String.length i in
assert (len >= 1);
match i.[0] with
| '-' ->
assert (len >= 2);
let pi = String.sub i 1 (len - 1) in
mk_term (Sy.Op Sy.Minus) [ positive_int "0"; positive_int pi ] Ty.Tint
| _ -> positive_int i

let positive_real i = mk_term (Sy.real i) [] Ty.Treal

let real r =
let len = String.length r in
assert (len >= 1);
match r.[0] with
| '-' ->
assert (len >= 2);
let pi = String.sub r 1 (len - 1) in
mk_term (Sy.Op Sy.Minus) [ positive_real "0"; positive_real pi ] Ty.Treal
| _ -> positive_real r

let bitv bt ty = mk_term (Sy.bitv bt) [] ty

let pred t = mk_term (Sy.Op Sy.Minus) [t;int "1"] Ty.Tint

(** pretty printing *)

module SmtPrinter = struct
(** Helper functions used by the postprocessing phase in the printers. *)
let zero ty =
match ty with
| Ty.Tint -> Sy.Int Z.zero
| Ty.Treal -> Sy.Real Q.zero
| _ -> assert false

let is_zero sy =
match sy with
| Sy.Int i when Z.(equal i zero) -> true
| Sy.Real q when Q.(equal q zero) -> true
| _ -> false

let is_one sy =
match sy with
| Sy.Int i when Z.(equal i one) -> true
| Sy.Real q when Q.(equal q one) -> true
| _ -> false

let is_mone sy =
match sy with
| Sy.Int i when Z.(equal i (neg one)) -> true
| Sy.Real q when Q.(equal q (neg one)) -> true
| _ -> false

let pp_binder ppf (var, (ty, _)) =
let var =
match var with
Expand Down Expand Up @@ -419,6 +586,33 @@ module SmtPrinter = struct

| Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op

| Sy.Op Plus, [e1; e2] when is_zero e1.f -> pp ppf e2

| Sy.Op Plus, [e1; e2] when is_zero e2.f -> pp ppf e1

| Sy.Op Minus, [e1; e2] when is_zero e1.f ->
Fmt.pf ppf "@[<hv 2>(-@ %a@])" pp e2

| Sy.Op Minus, [e1; e2] when is_zero e2.f -> pp ppf e1

| Sy.Op Mult, [e1; e2] when is_one e1.f -> pp ppf e2

| Sy.Op Mult, [e1; e2] when is_one e2.f -> pp ppf e1

| Sy.Op Mult, [e1; e2] when is_mone e2.f ->
let ty = e1.ty in
pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e2] ty)

| Sy.Op Mult, [e1; e2] when is_mone e1.f ->
let ty = e2.ty in
pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e1] ty)

| Sy.Op Div, [e1; e2] when is_one e2.f -> pp ppf e1

| Sy.Op Div, [e1; e2] when is_mone e2.f ->
let ty = e1.ty in
pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e1] ty)

| Sy.Op op, _ :: _ ->
Fmt.pf ppf "@[<hv 2>(%a@ %a@])"
Symbols.pp_smtlib_operator op
Expand Down Expand Up @@ -753,29 +947,6 @@ let mk_binders, reset_binders_cpt =
mk_binders, reset_binders_cpt


let merge_vars acc b =
SMap.merge (fun sy a b ->
match a, b with
| None, None -> assert false
| Some _, None -> a
| None, Some _ -> b
| Some (ty, x), Some (ty', y) ->
assert (Ty.equal ty ty' || Sy.equal sy Sy.underscore);
Some (ty, x + y)
) acc b

let free_vars t acc = merge_vars acc t.vars

let free_type_vars t = t.vty

let is_ground t =
SMap.is_empty (free_vars t SMap.empty) &&
Ty.Svty.is_empty (free_type_vars t)

let size t = t.nb_nodes

let depth t = t.depth

let rec is_positive e =
let { f; bind; _ } = e in
match f, bind with
Expand All @@ -784,14 +955,6 @@ let rec is_positive e =
| Sy.Let, B_let { in_e; is_bool = true; _ } -> is_positive in_e
| _ -> true

let neg t =
match t with
| { ty = Ty.Tbool; neg = Some n; _ } -> n
| { f = _; _ } -> assert false

let is_int t = t.ty == Ty.Tint
let is_real t = t.ty == Ty.Treal

let name_of_lemma f =
match form_view f with
| Lemma { name; _ } -> name
Expand All @@ -802,7 +965,6 @@ let name_of_lemma_opt opt =
| None -> "(Lemma=None)"
| Some f -> name_of_lemma f


(** Labeling and models *)

let labels = Labels.create 107
Expand Down Expand Up @@ -833,119 +995,6 @@ let print_tagged_classes =
Format.fprintf fmt "\n{ %a }" (print_list_sep " , ") cl) l


(** smart constructors for terms *)

let free_vars_non_form s l ty =
match s, l with
| Sy.Var _, [] -> SMap.singleton s (ty, 1)
| Sy.Var _, _ -> assert false
| Sy.Form _, _ -> assert false (* not correct for quantified and Lets *)
| _, [] -> SMap.empty
| _, e::r -> List.fold_left (fun s t -> merge_vars s t.vars) e.vars r

let free_type_vars_non_form l ty =
List.fold_left (fun acc t -> Ty.Svty.union acc t.vty) (Ty.vty_of ty) l

let is_ite s = match s with
| Sy.Op Sy.Tite -> true
| _ -> false

let mk_term s l ty =
assert (match s with Sy.Lit _ | Sy.Form _ -> false | _ -> true);
let d = match l with
| [] ->
1 (*no args ? depth = 1 (ie. current app s, ie constant)*)
| _ ->
(* if args, d is 1 + max_depth of args (equals at least to 1 *)
1 + List.fold_left (fun z t -> max z t.depth) 1 l
in
let nb_nodes = List.fold_left (fun z t -> z + t.nb_nodes) 1 l in
let vars = free_vars_non_form s l ty in
let vty = free_type_vars_non_form l ty in
let pure = List.for_all (fun e -> e.pure) l && not (is_ite s) in
let pos =
HC.make {f=s; xs=l; ty=ty; depth=d; tag= -42; vars; vty;
nb_nodes; neg = None; bind = B_none; pure}
in
if ty != Ty.Tbool then pos
else if pos.neg != None then pos
else
let neg_s = Sy.Lit Sy.L_neg_pred in
let neg =
HC.make {f=neg_s; xs=[pos]; ty=ty; depth=d; tag= -42;
vars; vty; nb_nodes; neg = None; bind = B_none; pure = false}
in
assert (neg.neg == None);
pos.neg <- Some neg;
neg.neg <- Some pos;
pos

let vrai =
let res =
let nb_nodes = 0 in
let vars = SMap.empty in
let vty = Ty.Svty.empty in
let faux =
HC.make
{f = Sy.False; xs = []; ty = Ty.Tbool; depth = -2; (*smallest depth*)
tag = -42; vars; vty; nb_nodes; neg = None; bind = B_none;
pure = true}
in
let vrai =
HC.make
{f = Sy.True; xs = []; ty = Ty.Tbool; depth = -1; (*2nd smallest d*)
tag= -42; vars; vty; nb_nodes; neg = None; bind = B_none;
pure = true}
in
assert (vrai.neg == None);
assert (faux.neg == None);
vrai.neg <- Some faux;
faux.neg <- Some vrai;
vrai
in
res

let faux = neg (vrai)
let void = mk_term (Sy.Void) [] Ty.Tunit

let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty

let is_internal_name t =
match t with
| { f; xs = []; _ } -> Sy.is_fresh_internal_name f
| _ -> false

let is_internal_skolem t = Sy.is_fresh_skolem t.f

let positive_int i = mk_term (Sy.int i) [] Ty.Tint

let int i =
let len = String.length i in
assert (len >= 1);
match i.[0] with
| '-' ->
assert (len >= 2);
let pi = String.sub i 1 (len - 1) in
mk_term (Sy.Op Sy.Minus) [ positive_int "0"; positive_int pi ] Ty.Tint
| _ -> positive_int i

let positive_real i = mk_term (Sy.real i) [] Ty.Treal

let real r =
let len = String.length r in
assert (len >= 1);
match r.[0] with
| '-' ->
assert (len >= 2);
let pi = String.sub r 1 (len - 1) in
mk_term (Sy.Op Sy.Minus) [ positive_real "0"; positive_real pi ] Ty.Treal
| _ -> positive_real r

let bitv bt ty = mk_term (Sy.bitv bt) [] ty

let pred t = mk_term (Sy.Op Sy.Minus) [t;int "1"] Ty.Tint


(** simple smart constructors for formulas *)

let mk_or f1 f2 is_impl =
Expand Down

0 comments on commit 29720fd

Please sign in to comment.