simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-11 05:28:34 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: properly typecheck and build LRA terms

Browse source
This commit is contained in:
Simon Cruanes 2020-10-04 00:32:52 -04:00
parent 943efad206
commit ac6ca7d584
5 changed files with 86 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/base-term/Base_types.ml
View file

@ -10,6 +10,7 @@ type lra_op = Sidekick_lra.op = Plus | Minus
type 'a lra_view = 'a Sidekick_lra.lra_view =
| LRA_pred of lra_pred * 'a * 'a
| LRA_op of lra_op * 'a * 'a
| LRA_mult of Q.t * 'a
| LRA_const of Q.t
| LRA_other of 'a
@ -234,6 +235,8 @@ let pp_term_view_gen ~pp_id ~pp_t out = function
Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_pred p) pp_t a pp_t b
| LRA_op (p, a, b) ->
Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_op p) pp_t a pp_t b
| LRA_mult (n, x) ->
Fmt.fprintf out "(@[*@ %a@ %a@])" Q.pp_print n pp_t x
| LRA_const q -> Q.pp_print out q
| LRA_other x -> pp_t out x
end
@ -603,7 +606,9 @@ end = struct
Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
| LRA_op (p, a, b) ->
Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
| LRA_const q -> Hash.combine2 83 (Hash.string @@ Q.to_string q)
| LRA_mult (n, x) ->
Hash.combine3 83 (Hash.string @@ Q.to_string n) (sub_hash x)
| LRA_const q -> Hash.combine2 84 (Hash.string @@ Q.to_string q)
| LRA_other x -> sub_hash x
end
@ -623,8 +628,10 @@ end = struct
| LRA_op(p1,a1,b1), LRA_op (p2,a2,b2) ->
p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
| LRA_const a1, LRA_const a2 -> Q.equal a1 a2
| LRA_mult (n1,x1), LRA_mult (n2,x2) -> Q.equal n1 n2 && sub_eq x1 x2
| LRA_other x1, LRA_other x2 -> sub_eq x1 x2
| (LRA_pred _ | LRA_op _ | LRA_const _ | LRA_other _), _ -> false
| (LRA_pred _ | LRA_op _ | LRA_const _
| LRA_mult _ | LRA_other _), _ -> false
end
| (Bool _ | App_fun _ | Eq _ | Not _ | Ite _ | LRA _), _
-> false
@ -659,8 +666,8 @@ end = struct
| Not u -> u.term_view
| _ -> Not t
let ite a b c = Ite (a,b,c)
let lra l : t = LRA l
let[@inline] ite a b c = Ite (a,b,c)
let[@inline] lra l : t = LRA l
let ty (t:t): Ty.t = match t with
| Bool _ | Eq _ | Not _ -> Ty.bool
@ -694,7 +701,7 @@ end = struct
| LRA l ->
begin match l with
| LRA_pred _ -> Ty.bool
| LRA_op _ | LRA_const _ -> Ty.real
| LRA_op _ | LRA_const _ | LRA_mult _ -> Ty.real
| LRA_other x -> x.term_ty
end
@ -708,8 +715,8 @@ end = struct
| LRA l ->
begin match l with
| LRA_pred (_, a, b)|LRA_op (_, a, b) -> f a; f b
| LRA_mult (_,x) | LRA_other x -> f x
| LRA_const _ -> ()
| LRA_other x -> f x
end
let map f view =
@ -877,7 +884,9 @@ end = struct
let app_cstor st c args : t = app_fun st (Fun.cstor c) args
let[@inline] lra (st:state) (l:t lra_view) : t =
make st (Term_cell.lra l)
match l with
| LRA_other x -> x (* normalize *)
| _ -> make st (Term_cell.lra l)
(* might need to tranfer the negation from [t] to [sign] *)
let abs tst t : t * bool = match view t with

6
src/smtlib/Process.ml
View file

@ -304,9 +304,13 @@ end)
module Th_lra = Sidekick_lra.Make(struct
module S = Solver
module T = BT.Term
type term = S.T.Term.t
include Lra
let mk_lra = T.lra
let view_as_lra t = match T.view t with
| T.LRA l -> l
| _ -> LRA_other t
module Gensym = struct
type t = {

51
src/smtlib/Typecheck.ml
View file

@ -105,6 +105,21 @@ let is_num s =
then CCString.for_all is_digit_or_dot (String.sub s 1 (String.length s-1))
else CCString.for_all is_digit_or_dot s
let string_as_q (s:string) : Q.t option =
try
let x =
try Q.of_string s
with _ ->
let f = float_of_string s in
Q.of_float f
in
Some x
with _ -> None
let t_as_q t = match Term.view t with
| T.LRA (LRA_const n) -> Some n
| _ -> None
(* conversion of terms *)
let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
let tst = ctx.Ctx.tst in
@ -112,8 +127,11 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
| PA.True -> T.true_ tst
| PA.False -> T.false_ tst
| PA.Const s when is_num s ->
errorf_ctx ctx "cannot handle numbers for now"
(* FIXME A.num_str Ty.rat s (* numeral *) *)
let open Base_types in
begin match string_as_q s with
| Some n -> T.lra tst (LRA_const n)
| None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t
end
| PA.Const f
| PA.App (f, []) ->
(* lookup in `let` table, then in type defs *)
@ -251,8 +269,33 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
in
A.match_ lhs cases
*)
| PA.Arith (_op, _l) ->
errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t
| PA.Arith (op, l) ->
let l = List.map (conv_term ctx) l in
let open Base_types in
begin match op, l with
| PA.Leq, [a;b] -> T.lra ctx.tst (LRA_pred (Leq, a, b))
| PA.Lt, [a;b] -> T.lra ctx.tst (LRA_pred (Lt, a, b))
| PA.Geq, [a;b] -> T.lra ctx.tst (LRA_pred (Geq, a, b))
| PA.Gt, [a;b] -> T.lra ctx.tst (LRA_pred (Gt, a, b))
| PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b))
| PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b))
| PA.Mult, [a;b] ->
begin match t_as_q a, t_as_q b with
| Some a, _ -> T.lra ctx.tst (LRA_mult (a, b))
| _, Some b -> T.lra ctx.tst (LRA_mult (b, a))
| None, None ->
errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t
end
| PA.Div, [a;b] ->
begin match t_as_q a, t_as_q b with
| Some a, _ -> T.lra ctx.tst (LRA_mult (Q.inv a, b))
| _, Some b -> T.lra ctx.tst (LRA_mult (Q.inv b, a))
| None, None ->
errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t
end
| _ ->
errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t
end;
(* FIXME: arith
let l = List.map (conv_term ctx) l in
List.iter

23
src/smtlib/lra.ml
View file

@ -1,23 +0,0 @@
open Sidekick_base_term
module T = Sidekick_base_term.Term
let id_leq = ID.make "<="
let id_lt = ID.make "<"
let id_plus = ID.make "+"
let id_uminus = ID.make "-"
let id_mult = ID.make "*"
let fun_leq = Fun.mk_undef id_leq Ty.(Fun.mk [real; real] bool)
let fun_lt = Fun.mk_undef id_lt Ty.(Fun.mk [real; real] bool)
let fun_plus = Fun.mk_undef id_plus Ty.(Fun.mk [real; real] real)
let fun_uminus = Fun.mk_undef id_plus Ty.(Fun.mk [real] real)
let fun_times = Fun.mk_undef id_plus Ty.(Fun.mk [real; real] real)
let leq st a b = T.app_fun st fun_leq (IArray.of_array_unsafe [|a; b|])
let lt st a b = T.app_fun st fun_lt (IArray.of_array_unsafe [|a; b|])
let lt st a b = T.app_fun st fun_lt (IArray.of_array_unsafe [|a; b|])
let view_as_lra _ = assert false (* TODO *)
let mk_lra _ = assert false

22
src/th-lra/Sidekick_lra.ml
View file

@ -12,6 +12,7 @@ type op = Plus | Minus
type 'a lra_view =
| LRA_pred of pred * 'a * 'a
| LRA_op of op * 'a * 'a
| LRA_mult of Q.t * 'a
| LRA_const of Q.t
| LRA_other of 'a
@ -19,6 +20,7 @@ let map_view f (l:_ lra_view) : _ lra_view =
begin match l with
| LRA_pred (p, a, b) -> LRA_pred (p, f a, f b)
| LRA_op (p, a, b) -> LRA_op (p, f a, f b)
| LRA_mult (n,a) -> LRA_mult (n, f a)
| LRA_const q -> LRA_const q
| LRA_other x -> LRA_other (f x)
end
@ -163,18 +165,30 @@ module Make(A : ARG) : S with module A = A = struct
| Plus -> t1 + t2
| Minus -> t1 - t2
end
| LRA_mult (n, x) ->
let t = as_linexp x in
LE.( n * t )
| LRA_const q -> LE.of_const q
(* TODO: keep the linexps until they're asserted;
TODO: but use simplification in preprocess
*)
(* preprocess linear expressions away *)
let preproc_lra self si ~mk_lit ~add_clause (t:T.t) : T.t option =
let _tst = SI.tst si in
match A.view_as_lra t with
| LRA_pred (_pre, _t1, _t2) ->
assert false (* TODO: define a bool variable *)
| LRA_op _ | LRA_const _ ->
None (* TODO: define a bool variable *)
| LRA_op _ | LRA_const _ -> None
(* TODO: remove?
let le = as_linexp t in
let proxy = fresh_term self ~pre:"lra" (T.ty t) in
Simplex.add_eq self.simplex (V_t proxy, []); (* TODO add LE *)
Some proxy
*)
(* TODO: useless?
add_clause [
mk_lit
@ -182,7 +196,6 @@ module Make(A : ARG) : S with module A = A = struct
(LRA_pred (Eq, le, Simplex.L.Comb.monomial1 (V_t proxy))))
];
*)
Some proxy
(*
| B_ite (a,b,c) ->
let t_a = fresh_term self ~pre:"ite" (T.ty b) in
@ -191,8 +204,9 @@ module Make(A : ARG) : S with module A = A = struct
add_clause [lit_a; mk_lit (eq self.tst t_a c)];
Some t_a
*)
| LRA_mult _ -> None (* TODO *)
| LRA_const _ ->
assert false (* TODO: turn into linexp *)
None (* TODO: turn into linexp *)
| LRA_other _ -> None
(* TODO: remove