feat(core): provide mk_eqn in CC

This commit is contained in:
Simon Cruanes 2021-09-19 13:03:44 -04:00
parent 1188c54d3c
commit 0902777527
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 3 additions and 0 deletions

View file

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

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
(** 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
(** Main congruence closure signature.