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

feat(core): provide mk_eqn in CC

Browse source
This commit is contained in:
Simon Cruanes 2021-09-19 13:03:44 -04:00
parent 156af6e803
commit 265442116f
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/base-solver/sidekick_base_solver.ml
View file

@ -13,6 +13,7 @@ module Solver_arg = struct
module Lit = Sidekick_base.Lit module Lit = Sidekick_base.Lit
let cc_view = Term.cc_view let cc_view = Term.cc_view
let mk_eqn = Term.eq
let is_valid_literal _ = true let is_valid_literal _ = true
module P = Proof_stub module P = Proof_stub
type proof = P.t type proof = P.t

2
src/core/Sidekick_core.ml
View file

@ -336,6 +336,8 @@ module type CC_ARG = sig
val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
(** View the term through the lens of the congruence closure *) (** View the term through the lens of the congruence closure *)
val mk_eqn : T.Term.store -> T.Term.t -> T.Term.t -> T.Term.t
end end
(** Main congruence closure signature. (** Main congruence closure signature.