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

feat(bool): also provide xor/neq

Browse source
This commit is contained in:
Simon Cruanes 2021-03-18 11:52:19 -04:00
parent 0a14d556d9
commit 2312da883c
2 changed files with 29 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smtlib/Form.ml
View file

@ -59,6 +59,7 @@ module Funs = struct
else if Value.is_false a then c else if Value.is_false a then c
else Error.errorf "non boolean value %a in ite" Value.pp a else Error.errorf "non boolean value %a in ite" Value.pp a
| B_equiv (a,b) | B_eq(a,b) -> Value.bool (Value.equal a b) | B_equiv (a,b) | B_eq(a,b) -> Value.bool (Value.equal a b)
| B_xor (a,b) | B_neq(a,b) -> Value.bool (not (Value.equal a b))
| B_atom v -> v | B_atom v -> v
| B_opaque_bool t -> Error.errorf "cannot evaluate opaque bool %a" pp t | B_opaque_bool t -> Error.errorf "cannot evaluate opaque bool %a" pp t
| B_not _ | B_and _ | B_or _ | B_imply _ | B_not _ | B_and _ | B_or _ | B_imply _
@ -154,7 +155,9 @@ let mk_bool st = function
| B_imply (a,b) -> imply_a st a b | B_imply (a,b) -> imply_a st a b
| B_ite (a,b,c) -> ite st a b c | B_ite (a,b,c) -> ite st a b c
| B_equiv (a,b) -> equiv st a b | B_equiv (a,b) -> equiv st a b
| B_xor (a,b) -> not_ st (equiv st a b)
| B_eq (a,b) -> T.eq st a b | B_eq (a,b) -> T.eq st a b
| B_neq (a,b) -> not_ st (T.eq st a b)
| B_not t -> not_ st t | B_not t -> not_ st t
| B_opaque_bool t -> t | B_opaque_bool t -> t

40
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -7,7 +7,9 @@ type ('a, 'args) bool_view =
| B_or of 'args | B_or of 'args
| B_imply of 'args * 'a | B_imply of 'args * 'a
| B_equiv of 'a * 'a | B_equiv of 'a * 'a
| B_xor of 'a * 'a
| B_eq of 'a * 'a | B_eq of 'a * 'a
| B_neq of 'a * 'a
| B_ite of 'a * 'a * 'a | B_ite of 'a * 'a * 'a
| B_opaque_bool of 'a (* do not enter *) | B_opaque_bool of 'a (* do not enter *)
| B_atom of 'a | B_atom of 'a
@ -124,9 +126,14 @@ module Make(A : ARG) : S with module A = A = struct
| B_equiv (a,b) when is_false a -> Some (not_ tst b) | B_equiv (a,b) when is_false a -> Some (not_ tst b)
| B_equiv (a,b) when is_true b -> Some a | B_equiv (a,b) when is_true b -> Some a
| B_equiv (a,b) when is_false b -> Some (not_ tst a) | B_equiv (a,b) when is_false b -> Some (not_ tst a)
| B_equiv _ -> None | B_xor (a,b) when is_false a -> Some b
| B_xor (a,b) when is_true a -> Some (not_ tst b)
| B_xor (a,b) when is_false b -> Some a
| B_xor (a,b) when is_true b -> Some (not_ tst a)
| B_equiv _ | B_xor _ -> None
| B_eq (a,b) when T.equal a b -> Some (T.bool tst true) | B_eq (a,b) when T.equal a b -> Some (T.bool tst true)
| B_eq _ -> None | B_neq (a,b) when T.equal a b -> Some (T.bool tst true)
| B_eq _ | B_neq _ -> None
| B_atom _ -> None | B_atom _ -> None
let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
@ -167,6 +174,20 @@ module Make(A : ARG) : S with module A = A = struct
lit lit
in in
if t_sign then lit else Lit.neg lit if t_sign then lit else Lit.neg lit
and equiv_ ~is_xor a b : Lit.t =
let a = get_lit a in
let b = get_lit b in
let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
let proxy = fresh_lit ~mk_lit ~pre:"equiv_" self in
(* proxy => a<=> b,
¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b];
add_clause [Lit.neg proxy; Lit.neg b; a];
add_clause [proxy; a; b];
add_clause [proxy; Lit.neg a; Lit.neg b];
proxy
and get_lit_uncached t : Lit.t = and get_lit_uncached t : Lit.t =
match A.view_as_bool t with match A.view_as_bool t with
| B_bool b -> mk_lit (T.bool self.tst b) | B_bool b -> mk_lit (T.bool self.tst b)
@ -195,18 +216,9 @@ module Make(A : ARG) : S with module A = A = struct
in in
or_a self.tst @@ IArray.append args (IArray.singleton u) in or_a self.tst @@ IArray.append args (IArray.singleton u) in
get_lit t' get_lit t'
| B_ite _ | B_eq _ -> mk_lit t | B_ite _ | B_eq _ | B_neq _ -> mk_lit t
| B_equiv (a,b) -> | B_equiv (a,b) -> equiv_ ~is_xor:false a b
let a = get_lit a in | B_xor (a,b) -> equiv_ ~is_xor:true a b
let b = get_lit b in
let proxy = fresh_lit ~mk_lit ~pre:"equiv_" self in
(* proxy => a<=> b,
¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b];
add_clause [Lit.neg proxy; Lit.neg b; a];
add_clause [proxy; a; b];
add_clause [proxy; Lit.neg a; Lit.neg b];
proxy
| B_atom u -> mk_lit u | B_atom u -> mk_lit u
in in
let lit = get_lit t in let lit = get_lit t in