mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
cleanup
This commit is contained in:
Simon Cruanes
parent
40734d5074
commit
e3aa43f817
8 changed files with 187 additions and 1576 deletions
|
|
@ -1,151 +0,0 @@
|
|||
open struct
|
||||
let hash_z = Z.hash
|
||||
let[@inline] hash_q q = CCHash.combine2 (hash_z (Q.num q)) (hash_z (Q.den q))
|
||||
end
|
||||
|
||||
module LRA_pred = struct
|
||||
type t = Sidekick_th_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
|
||||
|
||||
let to_string = function
|
||||
| Lt -> "<"
|
||||
| Leq -> "<="
|
||||
| Neq -> "!="
|
||||
| Eq -> "="
|
||||
| Gt -> ">"
|
||||
| Geq -> ">="
|
||||
|
||||
let equal : t -> t -> bool = ( = )
|
||||
let hash : t -> int = Hashtbl.hash
|
||||
let pp out p = Fmt.string out (to_string p)
|
||||
end
|
||||
|
||||
module LRA_op = struct
|
||||
type t = Sidekick_th_lra.op = Plus | Minus
|
||||
|
||||
let to_string = function
|
||||
| Plus -> "+"
|
||||
| Minus -> "-"
|
||||
|
||||
let equal : t -> t -> bool = ( = )
|
||||
let hash : t -> int = Hashtbl.hash
|
||||
let pp out p = Fmt.string out (to_string p)
|
||||
end
|
||||
|
||||
module LRA_view = struct
|
||||
include Sidekick_th_lra
|
||||
|
||||
type 'a t = (Q.t, 'a) lra_view
|
||||
|
||||
let map ~f_c f (l : _ t) : _ t =
|
||||
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 (f_c n, f a)
|
||||
| LRA_const c -> LRA_const (f_c c)
|
||||
| LRA_other x -> LRA_other (f x)
|
||||
|
||||
let iter f l : unit =
|
||||
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 _ -> ()
|
||||
|
||||
let pp ~pp_t out = function
|
||||
| LRA_pred (p, a, b) ->
|
||||
Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_pred.to_string p) pp_t a pp_t b
|
||||
| LRA_op (p, a, b) ->
|
||||
Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_op.to_string 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
|
||||
|
||||
let hash ~sub_hash = function
|
||||
| LRA_pred (p, a, b) ->
|
||||
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_mult (n, x) -> Hash.combine3 83 (hash_q n) (sub_hash x)
|
||||
| LRA_const q -> Hash.combine2 84 (hash_q q)
|
||||
| LRA_other x -> sub_hash x
|
||||
|
||||
let equal ~sub_eq l1 l2 =
|
||||
match l1, l2 with
|
||||
| LRA_pred (p1, a1, b1), LRA_pred (p2, a2, b2) ->
|
||||
p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
|
||||
| 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_mult _ | LRA_other _), _ ->
|
||||
false
|
||||
end
|
||||
|
||||
module LIA_pred = LRA_pred
|
||||
module LIA_op = LRA_op
|
||||
|
||||
module LIA_view = struct
|
||||
type 'a t =
|
||||
| LRA_pred of LIA_pred.t * 'a * 'a
|
||||
| LRA_op of LIA_op.t * 'a * 'a
|
||||
| LRA_mult of Z.t * 'a
|
||||
| LRA_const of Z.t
|
||||
| LRA_other of 'a
|
||||
|
||||
let map ~f_c f (l : _ t) : _ t =
|
||||
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 (f_c n, f a)
|
||||
| LRA_const c -> LRA_const (f_c c)
|
||||
| LRA_other x -> LRA_other (f x)
|
||||
|
||||
let iter f l : unit =
|
||||
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 _ -> ()
|
||||
|
||||
let pp ~pp_t out = function
|
||||
| LRA_pred (p, a, b) ->
|
||||
Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_pred.to_string p) pp_t a pp_t b
|
||||
| LRA_op (p, a, b) ->
|
||||
Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_op.to_string p) pp_t a pp_t b
|
||||
| LRA_mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Z.pp_print n pp_t x
|
||||
| LRA_const n -> Z.pp_print out n
|
||||
| LRA_other x -> pp_t out x
|
||||
|
||||
let hash ~sub_hash = function
|
||||
| LRA_pred (p, a, b) ->
|
||||
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_mult (n, x) -> Hash.combine3 83 (hash_z n) (sub_hash x)
|
||||
| LRA_const n -> Hash.combine2 84 (hash_z n)
|
||||
| LRA_other x -> sub_hash x
|
||||
|
||||
let equal ~sub_eq l1 l2 =
|
||||
match l1, l2 with
|
||||
| LRA_pred (p1, a1, b1), LRA_pred (p2, a2, b2) ->
|
||||
p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
|
||||
| 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 -> Z.equal a1 a2
|
||||
| LRA_mult (n1, x1), LRA_mult (n2, x2) -> Z.equal n1 n2 && sub_eq x1 x2
|
||||
| LRA_other x1, LRA_other x2 -> sub_eq x1 x2
|
||||
| (LRA_pred _ | LRA_op _ | LRA_const _ | LRA_mult _ | LRA_other _), _ ->
|
||||
false
|
||||
|
||||
(* convert the whole structure to reals *)
|
||||
let to_lra f l : _ LRA_view.t =
|
||||
match l with
|
||||
| LRA_pred (p, a, b) -> LRA_view.LRA_pred (p, f a, f b)
|
||||
| LRA_op (op, a, b) -> LRA_view.LRA_op (op, f a, f b)
|
||||
| LRA_mult (c, x) -> LRA_view.LRA_mult (Q.of_bigint c, f x)
|
||||
| LRA_const x -> LRA_view.LRA_const (Q.of_bigint x)
|
||||
| LRA_other v -> LRA_view.LRA_other (f v)
|
||||
end
|
||||
File diff suppressed because it is too large
Load diff
71
src/base/LIA_term.ml
Normal file
71
src/base/LIA_term.ml
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
open struct
|
||||
let hash_z = Z.hash
|
||||
let[@inline] hash_q q = CCHash.combine2 (hash_z (Q.num q)) (hash_z (Q.den q))
|
||||
end
|
||||
|
||||
module LIA_pred = LRA_term.Pred
|
||||
module LIA_op = LRA_term.Op
|
||||
|
||||
module LIA_view = struct
|
||||
type 'a t =
|
||||
| LRA_pred of LIA_pred.t * 'a * 'a
|
||||
| LRA_op of LIA_op.t * 'a * 'a
|
||||
| LRA_mult of Z.t * 'a
|
||||
| LRA_const of Z.t
|
||||
| LRA_other of 'a
|
||||
|
||||
let map ~f_c f (l : _ t) : _ t =
|
||||
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 (f_c n, f a)
|
||||
| LRA_const c -> LRA_const (f_c c)
|
||||
| LRA_other x -> LRA_other (f x)
|
||||
|
||||
let iter f l : unit =
|
||||
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 _ -> ()
|
||||
|
||||
let pp ~pp_t out = function
|
||||
| LRA_pred (p, a, b) ->
|
||||
Fmt.fprintf out "(@[%a@ %a@ %a@])" LRA_term.Pred.pp p pp_t a pp_t b
|
||||
| LRA_op (p, a, b) ->
|
||||
Fmt.fprintf out "(@[%a@ %a@ %a@])" LRA_term.Op.pp p pp_t a pp_t b
|
||||
| LRA_mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Z.pp_print n pp_t x
|
||||
| LRA_const n -> Z.pp_print out n
|
||||
| LRA_other x -> pp_t out x
|
||||
|
||||
let hash ~sub_hash = function
|
||||
| LRA_pred (p, a, b) ->
|
||||
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_mult (n, x) -> Hash.combine3 83 (hash_z n) (sub_hash x)
|
||||
| LRA_const n -> Hash.combine2 84 (hash_z n)
|
||||
| LRA_other x -> sub_hash x
|
||||
|
||||
let equal ~sub_eq l1 l2 =
|
||||
match l1, l2 with
|
||||
| LRA_pred (p1, a1, b1), LRA_pred (p2, a2, b2) ->
|
||||
p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
|
||||
| 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 -> Z.equal a1 a2
|
||||
| LRA_mult (n1, x1), LRA_mult (n2, x2) -> Z.equal n1 n2 && sub_eq x1 x2
|
||||
| LRA_other x1, LRA_other x2 -> sub_eq x1 x2
|
||||
| (LRA_pred _ | LRA_op _ | LRA_const _ | LRA_mult _ | LRA_other _), _ ->
|
||||
false
|
||||
|
||||
(* convert the whole structure to reals *)
|
||||
let to_lra f l : _ LRA_term.View.t =
|
||||
match l with
|
||||
| LRA_pred (p, a, b) -> LRA_term.View.LRA_pred (p, f a, f b)
|
||||
| LRA_op (op, a, b) -> LRA_term.View.LRA_op (op, f a, f b)
|
||||
| LRA_mult (c, x) -> LRA_term.View.LRA_mult (Q.of_bigint c, f x)
|
||||
| LRA_const x -> LRA_term.View.LRA_const (Q.of_bigint x)
|
||||
| LRA_other v -> LRA_term.View.LRA_other (f v)
|
||||
end
|
||||
|
|
@ -1,9 +1,91 @@
|
|||
open Sidekick_core
|
||||
module Pred = Arith_types_.LRA_pred
|
||||
module Op = Arith_types_.LRA_op
|
||||
module View = Arith_types_.LRA_view
|
||||
module T = Term
|
||||
|
||||
open struct
|
||||
let hash_z = Z.hash
|
||||
let[@inline] hash_q q = CCHash.combine2 (hash_z (Q.num q)) (hash_z (Q.den q))
|
||||
end
|
||||
|
||||
module Pred = struct
|
||||
type t = Sidekick_th_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
|
||||
|
||||
let to_string = function
|
||||
| Lt -> "<"
|
||||
| Leq -> "<="
|
||||
| Neq -> "!="
|
||||
| Eq -> "="
|
||||
| Gt -> ">"
|
||||
| Geq -> ">="
|
||||
|
||||
let equal : t -> t -> bool = ( = )
|
||||
let hash : t -> int = Hashtbl.hash
|
||||
let pp out p = Fmt.string out (to_string p)
|
||||
end
|
||||
|
||||
module Op = struct
|
||||
type t = Sidekick_th_lra.op = Plus | Minus
|
||||
|
||||
let to_string = function
|
||||
| Plus -> "+"
|
||||
| Minus -> "-"
|
||||
|
||||
let equal : t -> t -> bool = ( = )
|
||||
let hash : t -> int = Hashtbl.hash
|
||||
let pp out p = Fmt.string out (to_string p)
|
||||
end
|
||||
|
||||
module View = struct
|
||||
include Sidekick_th_lra
|
||||
|
||||
type 'a t = (Q.t, 'a) lra_view
|
||||
|
||||
let map ~f_c f (l : _ t) : _ t =
|
||||
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 (f_c n, f a)
|
||||
| LRA_const c -> LRA_const (f_c c)
|
||||
| LRA_other x -> LRA_other (f x)
|
||||
|
||||
let iter f l : unit =
|
||||
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 _ -> ()
|
||||
|
||||
let pp ~pp_t out = function
|
||||
| LRA_pred (p, a, b) ->
|
||||
Fmt.fprintf out "(@[%s@ %a@ %a@])" (Pred.to_string p) pp_t a pp_t b
|
||||
| LRA_op (p, a, b) ->
|
||||
Fmt.fprintf out "(@[%s@ %a@ %a@])" (Op.to_string 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
|
||||
|
||||
let hash ~sub_hash = function
|
||||
| LRA_pred (p, a, b) ->
|
||||
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_mult (n, x) -> Hash.combine3 83 (hash_q n) (sub_hash x)
|
||||
| LRA_const q -> Hash.combine2 84 (hash_q q)
|
||||
| LRA_other x -> sub_hash x
|
||||
|
||||
let equal ~sub_eq l1 l2 =
|
||||
match l1, l2 with
|
||||
| LRA_pred (p1, a1, b1), LRA_pred (p2, a2, b2) ->
|
||||
p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
|
||||
| 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_mult _ | LRA_other _), _ ->
|
||||
false
|
||||
end
|
||||
|
||||
type term = Term.t
|
||||
type ty = Term.t
|
||||
type Const.view += Const of Q.t | Pred of Pred.t | Op of Op.t | Mult_by of Q.t
|
||||
|
|
|
|||
|
|
@ -1,7 +1,33 @@
|
|||
open Sidekick_core
|
||||
module Pred = Arith_types_.LRA_pred
|
||||
module Op = Arith_types_.LRA_op
|
||||
module View = Arith_types_.LRA_view
|
||||
|
||||
module Pred : sig
|
||||
type t = Sidekick_th_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
|
||||
|
||||
include Sidekick_sigs.EQ_HASH_PRINT with type t := t
|
||||
end
|
||||
|
||||
module Op : sig
|
||||
type t = Sidekick_th_lra.op = Plus | Minus
|
||||
|
||||
include Sidekick_sigs.EQ_HASH_PRINT with type t := t
|
||||
end
|
||||
|
||||
module View : sig
|
||||
type ('num, 'a) lra_view = ('num, 'a) Sidekick_th_lra.lra_view =
|
||||
| LRA_pred of Pred.t * 'a * 'a
|
||||
| LRA_op of Op.t * 'a * 'a
|
||||
| LRA_mult of 'num * 'a
|
||||
| LRA_const of 'num
|
||||
| LRA_other of 'a
|
||||
|
||||
type 'a t = (Q.t, 'a) Sidekick_th_lra.lra_view
|
||||
|
||||
val map : f_c:(Q.t -> Q.t) -> ('a -> 'b) -> 'a t -> 'b t
|
||||
val iter : ('a -> unit) -> 'a t -> unit
|
||||
val pp : pp_t:'a Fmt.printer -> 'a t Fmt.printer
|
||||
val hash : sub_hash:('a -> int) -> 'a t -> int
|
||||
val equal : sub_eq:('a -> 'b -> bool) -> 'a t -> 'b t -> bool
|
||||
end
|
||||
|
||||
type term = Term.t
|
||||
type ty = Term.t
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
It provides a representation of terms, boolean formulas,
|
||||
linear arithmetic expressions, datatypes for the functors in Sidekick.
|
||||
|
||||
In addition, it has a notion of {{!Base_types.Statement} Statement}.
|
||||
In addition, it has a notion of {{!Statement.t} Statement}.
|
||||
Statements are instructions
|
||||
for the SMT solver to do something, such as: define a new constant,
|
||||
declare a new constant, assert a formula as being true,
|
||||
|
|
@ -22,7 +22,6 @@ module Const = Sidekick_core.Const
|
|||
module Ty = Ty
|
||||
module ID = ID
|
||||
module Form = Form
|
||||
include Arith_types_
|
||||
module Data_ty = Data_ty
|
||||
module Cstor = Data_ty.Cstor
|
||||
module Select = Data_ty.Select
|
||||
|
|
|
|||
|
|
@ -177,7 +177,7 @@ let main_smt ~config () : _ result =
|
|||
Log.debugf 1 (fun k ->
|
||||
k "(@[main.th-bool.pick@ %S@])"
|
||||
(Sidekick_smt_solver.Theory.name th_bool));
|
||||
Sidekick_smt_solver.Theory.[ th_bool; Process.th_data; Process.th_lra ]
|
||||
[ th_bool; Process.th_data; Process.th_lra ]
|
||||
in
|
||||
Process.Solver.create_default ~proof ~theories tst
|
||||
in
|
||||
|
|
|
|||
|
|
@ -6,31 +6,6 @@ open struct
|
|||
module Rule_ = Proof_core
|
||||
end
|
||||
|
||||
(* TODO
|
||||
let mk_cc_acts_ (pr : P.t) (a : sat_acts) : CC.actions =
|
||||
let (module A) = a in
|
||||
|
||||
(module struct
|
||||
module T = T
|
||||
module Lit = Lit
|
||||
|
||||
type nonrec lit = lit
|
||||
type nonrec term = term
|
||||
type nonrec proof_trace = Proof_trace.t
|
||||
type nonrec step_id = step_id
|
||||
|
||||
let proof_trace () = pr
|
||||
let[@inline] raise_conflict lits (pr : step_id) = A.raise_conflict lits pr
|
||||
|
||||
let[@inline] raise_semantic_conflict lits semantic =
|
||||
raise (Semantic_conflict { lits; semantic })
|
||||
|
||||
let[@inline] propagate lit ~reason =
|
||||
let reason = Sidekick_sat.Consequence reason in
|
||||
A.propagate lit reason
|
||||
end)
|
||||
*)
|
||||
|
||||
module Sat_solver = Sidekick_sat
|
||||
(** the parametrized SAT Solver *)
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue