mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
remove most sigs
This commit is contained in:
Simon Cruanes
parent
65e876bebc
commit
06107c212f
14 changed files with 0 additions and 905 deletions
|
|
@ -1,9 +0,0 @@
|
|||
|
||||
(library
|
||||
(name sidekick_sigs_cc)
|
||||
(public_name sidekick.sigs.cc)
|
||||
(synopsis "Signatures for the congruence closure")
|
||||
(flags :standard -open Sidekick_util)
|
||||
(libraries containers iter sidekick.sigs sidekick.sigs.term
|
||||
sidekick.sigs.lit sidekick.sigs.proof-trace sidekick.sigs.proof.core
|
||||
sidekick.util))
|
||||
|
|
@ -1,515 +0,0 @@
|
|||
(** Main types for congruence closure *)
|
||||
|
||||
module View = View
|
||||
|
||||
module type TERM = Sidekick_sigs_term.S
|
||||
module type LIT = Sidekick_sigs_lit.S
|
||||
module type PROOF_TRACE = Sidekick_sigs_proof_trace.S
|
||||
|
||||
(** Arguments to a congruence closure's implementation *)
|
||||
module type ARG = sig
|
||||
module T : TERM
|
||||
module Lit : LIT with module T = T
|
||||
module Proof_trace : PROOF_TRACE
|
||||
|
||||
(** Arguments for the congruence closure *)
|
||||
val view_as_cc : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) View.t
|
||||
(** View the term through the lens of the congruence closure *)
|
||||
|
||||
val mk_lit_eq : ?sign:bool -> T.Term.store -> T.Term.t -> T.Term.t -> Lit.t
|
||||
(** [mk_lit_eq store t u] makes the literal [t=u] *)
|
||||
|
||||
module Rule_core :
|
||||
Sidekick_sigs_proof_core.S
|
||||
with type term = T.Term.t
|
||||
and type lit = Lit.t
|
||||
and type step_id = Proof_trace.A.step_id
|
||||
and type rule = Proof_trace.A.rule
|
||||
end
|
||||
|
||||
(** Collection of input types, and types defined by the congruence closure *)
|
||||
module type ARGS_CLASSES_EXPL_EVENT = sig
|
||||
module T : TERM
|
||||
module Lit : LIT with module T = T
|
||||
module Proof_trace : PROOF_TRACE
|
||||
|
||||
type term_store = T.Term.store
|
||||
type term = T.Term.t
|
||||
type value = term
|
||||
type fun_ = T.Fun.t
|
||||
type lit = Lit.t
|
||||
type proof_trace = Proof_trace.t
|
||||
type step_id = Proof_trace.A.step_id
|
||||
|
||||
(** E-node.
|
||||
|
||||
An e-node is a node in the congruence closure that is contained
|
||||
in some equivalence classe).
|
||||
An equivalence class is a set of terms that are currently equal
|
||||
in the partial model built by the solver.
|
||||
The class is represented by a collection of nodes, one of which is
|
||||
distinguished and is called the "representative".
|
||||
|
||||
All information pertaining to the whole equivalence class is stored
|
||||
in its representative's {!E_node.t}.
|
||||
|
||||
When two classes become equal (are "merged"), one of the two
|
||||
representatives is picked as the representative of the new class.
|
||||
The new class contains the union of the two old classes' nodes.
|
||||
|
||||
We also allow theories to store additional information in the
|
||||
representative. This information can be used when two classes are
|
||||
merged, to detect conflicts and solve equations à la Shostak.
|
||||
*)
|
||||
module E_node : sig
|
||||
type t
|
||||
(** An E-node.
|
||||
|
||||
A value of type [t] points to a particular term, but see
|
||||
{!find} to get the representative of the class. *)
|
||||
|
||||
include Sidekick_sigs.PRINT with type t := t
|
||||
|
||||
val term : t -> term
|
||||
(** Term contained in this equivalence class.
|
||||
If [is_root n], then [term n] is the class' representative term. *)
|
||||
|
||||
val equal : t -> t -> bool
|
||||
(** Are two classes {b physically} equal? To check for
|
||||
logical equality, use [CC.E_node.equal (CC.find cc n1) (CC.find cc n2)]
|
||||
which checks for equality of representatives. *)
|
||||
|
||||
val hash : t -> int
|
||||
(** An opaque hash of this E_node.t. *)
|
||||
|
||||
val is_root : t -> bool
|
||||
(** Is the E_node.t a root (ie the representative of its class)?
|
||||
See {!find} to get the root. *)
|
||||
|
||||
val iter_class : t -> t Iter.t
|
||||
(** Traverse the congruence class.
|
||||
Precondition: [is_root n] (see {!find} below) *)
|
||||
|
||||
val iter_parents : t -> t Iter.t
|
||||
(** Traverse the parents of the class.
|
||||
Precondition: [is_root n] (see {!find} below) *)
|
||||
|
||||
(* FIXME:
|
||||
[@@alert refactor "this should be replaced with a Per_class concept"]
|
||||
*)
|
||||
|
||||
type bitfield
|
||||
(** A field in the bitfield of this node. This should only be
|
||||
allocated when a theory is initialized.
|
||||
|
||||
Bitfields are accessed using preallocated keys.
|
||||
See {!CC_S.allocate_bitfield}.
|
||||
|
||||
All fields are initially 0, are backtracked automatically,
|
||||
and are merged automatically when classes are merged. *)
|
||||
end
|
||||
|
||||
(** Explanations
|
||||
|
||||
Explanations are specialized proofs, created by the congruence closure
|
||||
when asked to justify why two terms are equal. *)
|
||||
module Expl : sig
|
||||
type t
|
||||
|
||||
include Sidekick_sigs.PRINT with type t := t
|
||||
|
||||
val mk_merge : E_node.t -> E_node.t -> t
|
||||
(** Explanation: the nodes were explicitly merged *)
|
||||
|
||||
val mk_merge_t : term -> term -> t
|
||||
(** Explanation: the terms were explicitly merged *)
|
||||
|
||||
val mk_lit : lit -> t
|
||||
(** Explanation: we merged [t] and [u] because of literal [t=u],
|
||||
or we merged [t] and [true] because of literal [t],
|
||||
or [t] and [false] because of literal [¬t] *)
|
||||
|
||||
val mk_list : t list -> t
|
||||
(** Conjunction of explanations *)
|
||||
|
||||
val mk_theory : term -> term -> (term * term * t list) list -> step_id -> t
|
||||
(** [mk_theory t u expl_sets pr] builds a theory explanation for
|
||||
why [|- t=u]. It depends on sub-explanations [expl_sets] which
|
||||
are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are
|
||||
explanations that justify [t_i = u_i] in the current congruence closure.
|
||||
|
||||
The proof [pr] is the theory lemma, of the form
|
||||
[ (t_i = u_i)_i |- t=u ].
|
||||
It is resolved against each [expls_i |- t_i=u_i] obtained from
|
||||
[expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u]
|
||||
where [Gamma] is a subset of the literals asserted into the congruence
|
||||
closure.
|
||||
|
||||
For example for the lemma [a=b] deduced by injectivity
|
||||
from [Some a=Some b] in the theory of datatypes,
|
||||
the arguments would be
|
||||
[a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr]
|
||||
where [pr] is the injectivity lemma [Some a=Some b |- a=b].
|
||||
*)
|
||||
end
|
||||
|
||||
(** Resolved explanations.
|
||||
|
||||
The congruence closure keeps explanations for why terms are in the same
|
||||
class. However these are represented in a compact, cheap form.
|
||||
To use these explanations we need to {b resolve} them into a
|
||||
resolved explanation, typically a list of
|
||||
literals that are true in the current trail and are responsible for
|
||||
merges.
|
||||
|
||||
However, we can also have merged classes because they have the same value
|
||||
in the current model. *)
|
||||
module Resolved_expl : sig
|
||||
type t = { lits: lit list; pr: proof_trace -> step_id }
|
||||
|
||||
include Sidekick_sigs.PRINT with type t := t
|
||||
end
|
||||
|
||||
(** Per-node data *)
|
||||
|
||||
type e_node = E_node.t
|
||||
(** A node of the congruence closure *)
|
||||
|
||||
type repr = E_node.t
|
||||
(** Node that is currently a representative. *)
|
||||
|
||||
type explanation = Expl.t
|
||||
end
|
||||
|
||||
(** Main congruence closure signature.
|
||||
|
||||
The congruence closure handles the theory QF_UF (uninterpreted
|
||||
function symbols).
|
||||
It is also responsible for {i theory combination}, and provides
|
||||
a general framework for equality reasoning that other
|
||||
theories piggyback on.
|
||||
|
||||
For example, the theory of datatypes relies on the congruence closure
|
||||
to do most of the work, and "only" adds injectivity/disjointness/acyclicity
|
||||
lemmas when needed.
|
||||
|
||||
Similarly, a theory of arrays would hook into the congruence closure and
|
||||
assert (dis)equalities as needed.
|
||||
*)
|
||||
module type S = sig
|
||||
include ARGS_CLASSES_EXPL_EVENT
|
||||
|
||||
type t
|
||||
(** The congruence closure object.
|
||||
It contains a fair amount of state and is mutable
|
||||
and backtrackable. *)
|
||||
|
||||
(** {3 Accessors} *)
|
||||
|
||||
val term_store : t -> term_store
|
||||
val proof : t -> proof_trace
|
||||
|
||||
val find : t -> e_node -> repr
|
||||
(** Current representative *)
|
||||
|
||||
val add_term : t -> term -> e_node
|
||||
(** Add the term to the congruence closure, if not present already.
|
||||
Will be backtracked. *)
|
||||
|
||||
val mem_term : t -> term -> bool
|
||||
(** Returns [true] if the term is explicitly present in the congruence closure *)
|
||||
|
||||
val allocate_bitfield : t -> descr:string -> E_node.bitfield
|
||||
(** Allocate a new e_node field (see {!E_node.bitfield}).
|
||||
|
||||
This field descriptor is henceforth reserved for all nodes
|
||||
in this congruence closure, and can be set using {!set_bitfield}
|
||||
for each class_ individually.
|
||||
This can be used to efficiently store some metadata on nodes
|
||||
(e.g. "is there a numeric value in the class"
|
||||
or "is there a constructor term in the class").
|
||||
|
||||
There may be restrictions on how many distinct fields are allocated
|
||||
for a given congruence closure (e.g. at most {!Sys.int_size} fields).
|
||||
*)
|
||||
|
||||
val get_bitfield : t -> E_node.bitfield -> E_node.t -> bool
|
||||
(** Access the bit field of the given e_node *)
|
||||
|
||||
val set_bitfield : t -> E_node.bitfield -> bool -> E_node.t -> unit
|
||||
(** Set the bitfield for the e_node. This will be backtracked.
|
||||
See {!E_node.bitfield}. *)
|
||||
|
||||
type propagation_reason = unit -> lit list * step_id
|
||||
|
||||
(** Handler Actions
|
||||
|
||||
Actions that can be scheduled by event handlers. *)
|
||||
module Handler_action : sig
|
||||
type t =
|
||||
| Act_merge of E_node.t * E_node.t * Expl.t
|
||||
| Act_propagate of lit * propagation_reason
|
||||
|
||||
(* TODO:
|
||||
- an action to modify data associated with a class
|
||||
*)
|
||||
|
||||
type conflict = Conflict of Expl.t [@@unboxed]
|
||||
|
||||
type or_conflict = (t list, conflict) result
|
||||
(** Actions or conflict scheduled by an event handler.
|
||||
|
||||
- [Ok acts] is a list of merges and propagations
|
||||
- [Error confl] is a conflict to resolve.
|
||||
*)
|
||||
end
|
||||
|
||||
(** Result Actions.
|
||||
|
||||
|
||||
Actions returned by the congruence closure after calling {!check}. *)
|
||||
module Result_action : sig
|
||||
type t =
|
||||
| Act_propagate of { lit: lit; reason: propagation_reason }
|
||||
(** [propagate (lit, reason)] declares that [reason() => lit]
|
||||
is a tautology.
|
||||
|
||||
- [reason()] should return a list of literals that are currently true,
|
||||
as well as a proof.
|
||||
- [lit] should be a literal of interest (see {!S.set_as_lit}).
|
||||
|
||||
This function might never be called, a congruence closure has the right
|
||||
to not propagate and only trigger conflicts. *)
|
||||
|
||||
type conflict =
|
||||
| Conflict of lit list * step_id
|
||||
(** [raise_conflict (c,pr)] declares that [c] is a tautology of
|
||||
the theory of congruence.
|
||||
@param pr the proof of [c] being a tautology *)
|
||||
|
||||
type or_conflict = (t list, conflict) result
|
||||
end
|
||||
|
||||
(** {3 Events}
|
||||
|
||||
Events triggered by the congruence closure, to which
|
||||
other plugins can subscribe. *)
|
||||
|
||||
(** Events emitted by the congruence closure when something changes. *)
|
||||
val on_pre_merge :
|
||||
t -> (t * E_node.t * E_node.t * Expl.t, Handler_action.or_conflict) Event.t
|
||||
(** [Ev_on_pre_merge acts n1 n2 expl] is emitted right before [n1]
|
||||
and [n2] are merged with explanation [expl]. *)
|
||||
|
||||
val on_pre_merge2 :
|
||||
t -> (t * E_node.t * E_node.t * Expl.t, Handler_action.or_conflict) Event.t
|
||||
(** Second phase of "on pre merge". This runs after {!on_pre_merge}
|
||||
and is used by Plugins. {b NOTE}: Plugin state might be observed as already
|
||||
changed in these handlers. *)
|
||||
|
||||
val on_post_merge :
|
||||
t -> (t * E_node.t * E_node.t, Handler_action.t list) Event.t
|
||||
(** [ev_on_post_merge acts n1 n2] is emitted right after [n1]
|
||||
and [n2] were merged. [find cc n1] and [find cc n2] will return
|
||||
the same E_node.t. *)
|
||||
|
||||
val on_new_term : t -> (t * E_node.t * term, Handler_action.t list) Event.t
|
||||
(** [ev_on_new_term n t] is emitted whenever a new term [t]
|
||||
is added to the congruence closure. Its E_node.t is [n]. *)
|
||||
|
||||
type ev_on_conflict = { cc: t; th: bool; c: lit list }
|
||||
(** Event emitted when a conflict occurs in the CC.
|
||||
|
||||
[th] is true if the explanation for this conflict involves
|
||||
at least one "theory" explanation; i.e. some of the equations
|
||||
participating in the conflict are purely syntactic theories
|
||||
like injectivity of constructors. *)
|
||||
|
||||
val on_conflict : t -> (ev_on_conflict, unit) Event.t
|
||||
(** [ev_on_conflict {th; c}] is emitted when the congruence
|
||||
closure triggers a conflict by asserting the tautology [c]. *)
|
||||
|
||||
val on_propagate :
|
||||
t -> (t * lit * (unit -> lit list * step_id), Handler_action.t list) Event.t
|
||||
(** [ev_on_propagate lit reason] is emitted whenever [reason() => lit]
|
||||
is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
|
||||
|
||||
val on_is_subterm : t -> (t * E_node.t * term, Handler_action.t list) Event.t
|
||||
(** [ev_on_is_subterm n t] is emitted when [n] is a subterm of
|
||||
another E_node.t for the first time. [t] is the term corresponding to
|
||||
the E_node.t [n]. This can be useful for theory combination. *)
|
||||
|
||||
(** {3 Misc} *)
|
||||
|
||||
val n_true : t -> E_node.t
|
||||
(** Node for [true] *)
|
||||
|
||||
val n_false : t -> E_node.t
|
||||
(** Node for [false] *)
|
||||
|
||||
val n_bool : t -> bool -> E_node.t
|
||||
(** Node for either true or false *)
|
||||
|
||||
val set_as_lit : t -> E_node.t -> lit -> unit
|
||||
(** map the given e_node to a literal. *)
|
||||
|
||||
val find_t : t -> term -> repr
|
||||
(** Current representative of the term.
|
||||
@raise E_node.t_found if the term is not already {!add}-ed. *)
|
||||
|
||||
val add_iter : t -> term Iter.t -> unit
|
||||
(** Add a sequence of terms to the congruence closure *)
|
||||
|
||||
val all_classes : t -> repr Iter.t
|
||||
(** All current classes. This is costly, only use if there is no other solution *)
|
||||
|
||||
val explain_eq : t -> E_node.t -> E_node.t -> Resolved_expl.t
|
||||
(** Explain why the two nodes are equal.
|
||||
Fails if they are not, in an unspecified way. *)
|
||||
|
||||
val explain_expl : t -> Expl.t -> Resolved_expl.t
|
||||
(** Transform explanation into an actionable conflict clause *)
|
||||
|
||||
(* FIXME: remove
|
||||
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
|
||||
(** Raise a conflict with the given explanation.
|
||||
It must be a theory tautology that [expl ==> absurd].
|
||||
To be used in theories.
|
||||
|
||||
This fails in an unspecified way if the explanation, once resolved,
|
||||
satisfies {!Resolved_expl.is_semantic}. *)
|
||||
*)
|
||||
|
||||
val merge : t -> E_node.t -> E_node.t -> Expl.t -> unit
|
||||
(** Merge these two nodes given this explanation.
|
||||
It must be a theory tautology that [expl ==> n1 = n2].
|
||||
To be used in theories. *)
|
||||
|
||||
val merge_t : t -> term -> term -> Expl.t -> unit
|
||||
(** Shortcut for adding + merging *)
|
||||
|
||||
(** {3 Main API *)
|
||||
|
||||
val assert_eq : t -> term -> term -> Expl.t -> unit
|
||||
(** Assert that two terms are equal, using the given explanation. *)
|
||||
|
||||
val assert_lit : t -> lit -> unit
|
||||
(** Given a literal, assume it in the congruence closure and propagate
|
||||
its consequences. Will be backtracked.
|
||||
|
||||
Useful for the theory combination or the SAT solver's functor *)
|
||||
|
||||
val assert_lits : t -> lit Iter.t -> unit
|
||||
(** Addition of many literals *)
|
||||
|
||||
val check : t -> Result_action.or_conflict
|
||||
(** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
|
||||
Will use the {!actions} to propagate literals, declare conflicts, etc. *)
|
||||
|
||||
val push_level : t -> unit
|
||||
(** Push backtracking level *)
|
||||
|
||||
val pop_levels : t -> int -> unit
|
||||
(** Restore to state [n] calls to [push_level] earlier. Used during backtracking. *)
|
||||
|
||||
val get_model : t -> E_node.t Iter.t Iter.t
|
||||
(** get all the equivalence classes so they can be merged in the model *)
|
||||
end
|
||||
|
||||
(* TODO
|
||||
module type DYN_BUILDER = sig
|
||||
include ARGS_CLASSES_EXPL_EVENT
|
||||
end
|
||||
*)
|
||||
|
||||
(* TODO: full EGG, also have a function to update the value when
|
||||
the subterms (produced in [of_term]) are updated *)
|
||||
|
||||
(** Data attached to the congruence closure classes.
|
||||
|
||||
This helps theories keeping track of some state for each class.
|
||||
The state of a class is the monoidal combination of the state for each
|
||||
term in the class (for example, the set of terms in the
|
||||
class whose head symbol is a datatype constructor). *)
|
||||
module type MONOID_PLUGIN_ARG = sig
|
||||
module CC : S
|
||||
|
||||
type t
|
||||
(** Some type with a monoid structure *)
|
||||
|
||||
include Sidekick_sigs.PRINT with type t := t
|
||||
|
||||
val name : string
|
||||
(** name of the monoid structure (short) *)
|
||||
|
||||
(* FIXME: for subs, return list of e_nodes, and assume of_term already
|
||||
returned data for them. *)
|
||||
val of_term :
|
||||
CC.t -> CC.E_node.t -> CC.term -> t option * (CC.E_node.t * t) list
|
||||
(** [of_term n t], where [t] is the term annotating node [n],
|
||||
must return [maybe_m, l], where:
|
||||
|
||||
- [maybe_m = Some m] if [t] has monoid value [m];
|
||||
otherwise [maybe_m=None]
|
||||
- [l] is a list of [(u, m_u)] where each [u]'s term
|
||||
is a direct subterm of [t]
|
||||
and [m_u] is the monoid value attached to [u].
|
||||
|
||||
*)
|
||||
|
||||
val merge :
|
||||
CC.t ->
|
||||
CC.E_node.t ->
|
||||
t ->
|
||||
CC.E_node.t ->
|
||||
t ->
|
||||
CC.Expl.t ->
|
||||
(t * CC.Handler_action.t list, CC.Handler_action.conflict) result
|
||||
(** Monoidal combination of two values.
|
||||
|
||||
[merge cc n1 mon1 n2 mon2 expl] returns the result of merging
|
||||
monoid values [mon1] (for class [n1]) and [mon2] (for class [n2])
|
||||
when [n1] and [n2] are merged with explanation [expl].
|
||||
|
||||
@return [Ok mon] if the merge is acceptable, annotating the class of [n1 ∪ n2];
|
||||
or [Error expl'] if the merge is unsatisfiable. [expl'] can then be
|
||||
used to trigger a conflict and undo the merge.
|
||||
*)
|
||||
end
|
||||
|
||||
(** Stateful plugin holding a per-equivalence-class monoid.
|
||||
|
||||
Helps keep track of monoid state per equivalence class.
|
||||
A theory might use one or more instance(s) of this to
|
||||
aggregate some theory-specific state over all terms, with
|
||||
the information of what terms are already known to be equal
|
||||
potentially saving work for the theory. *)
|
||||
module type DYN_MONOID_PLUGIN = sig
|
||||
module M : MONOID_PLUGIN_ARG
|
||||
include Sidekick_sigs.DYN_BACKTRACKABLE
|
||||
|
||||
val pp : unit Fmt.printer
|
||||
|
||||
val mem : M.CC.E_node.t -> bool
|
||||
(** Does the CC E_node.t have a monoid value? *)
|
||||
|
||||
val get : M.CC.E_node.t -> M.t option
|
||||
(** Get monoid value for this CC E_node.t, if any *)
|
||||
|
||||
val iter_all : (M.CC.repr * M.t) Iter.t
|
||||
end
|
||||
|
||||
(** Builder for a plugin.
|
||||
|
||||
The builder takes a congruence closure, and instantiate the
|
||||
plugin on it. *)
|
||||
module type MONOID_PLUGIN_BUILDER = sig
|
||||
module M : MONOID_PLUGIN_ARG
|
||||
|
||||
module type DYN_PL_FOR_M = DYN_MONOID_PLUGIN with module M = M
|
||||
|
||||
type t = (module DYN_PL_FOR_M)
|
||||
|
||||
val create_and_setup : ?size:int -> M.CC.t -> t
|
||||
(** Create a new monoid state *)
|
||||
end
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
type ('f, 't, 'ts) t =
|
||||
| Bool of bool
|
||||
| App_fun of 'f * 'ts
|
||||
| App_ho of 't * 't
|
||||
| If of 't * 't * 't
|
||||
| Eq of 't * 't
|
||||
| Not of 't
|
||||
| Opaque of 't
|
||||
(* do not enter *)
|
||||
|
||||
let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
|
||||
match v with
|
||||
| Bool b -> Bool b
|
||||
| App_fun (f, args) -> App_fun (f_f f, f_ts args)
|
||||
| App_ho (f, a) -> App_ho (f_t f, f_t a)
|
||||
| Not t -> Not (f_t t)
|
||||
| If (a, b, c) -> If (f_t a, f_t b, f_t c)
|
||||
| Eq (a, b) -> Eq (f_t a, f_t b)
|
||||
| Opaque t -> Opaque (f_t t)
|
||||
|
||||
let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
|
||||
match v with
|
||||
| Bool _ -> ()
|
||||
| App_fun (f, args) ->
|
||||
f_f f;
|
||||
f_ts args
|
||||
| App_ho (f, a) ->
|
||||
f_t f;
|
||||
f_t a
|
||||
| Not t -> f_t t
|
||||
| If (a, b, c) ->
|
||||
f_t a;
|
||||
f_t b;
|
||||
f_t c
|
||||
| Eq (a, b) ->
|
||||
f_t a;
|
||||
f_t b
|
||||
| Opaque t -> f_t t
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
(** View terms through the lens of the Congruence Closure *)
|
||||
|
||||
(** A view of a term fron the point of view of the congruence closure.
|
||||
|
||||
- ['f] is the type of function symbols
|
||||
- ['t] is the type of terms
|
||||
- ['ts] is the type of sequences of terms (arguments of function application)
|
||||
*)
|
||||
type ('f, 't, 'ts) t =
|
||||
| Bool of bool
|
||||
| App_fun of 'f * 'ts
|
||||
| App_ho of 't * 't
|
||||
| If of 't * 't * 't
|
||||
| Eq of 't * 't
|
||||
| Not of 't
|
||||
| Opaque of 't (** do not enter *)
|
||||
|
||||
val map_view :
|
||||
f_f:('a -> 'b) ->
|
||||
f_t:('c -> 'd) ->
|
||||
f_ts:('e -> 'f) ->
|
||||
('a, 'c, 'e) t ->
|
||||
('b, 'd, 'f) t
|
||||
(** Map function over a view, one level deep.
|
||||
Each function maps over a different type, e.g. [f_t] maps over terms *)
|
||||
|
||||
val iter_view :
|
||||
f_f:('a -> unit) ->
|
||||
f_t:('b -> unit) ->
|
||||
f_ts:('c -> unit) ->
|
||||
('a, 'b, 'c) t ->
|
||||
unit
|
||||
(** Iterate over a view, one level deep. *)
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
(library
|
||||
(name sidekick_sigs_lit)
|
||||
(public_name sidekick.sigs.lit)
|
||||
(synopsis "Common definition for literals")
|
||||
(libraries containers iter sidekick.sigs sidekick.sigs.term))
|
||||
|
|
@ -1,45 +0,0 @@
|
|||
(** Literals
|
||||
|
||||
Literals are a pair of a boolean-sorted term, and a sign.
|
||||
Positive literals are the same as their term, and negative literals
|
||||
are the negation of their term.
|
||||
|
||||
The SAT solver deals only in literals and clauses (sets of literals).
|
||||
Everything else belongs in the SMT solver. *)
|
||||
|
||||
module type TERM = Sidekick_sigs_term.S
|
||||
|
||||
module type S = sig
|
||||
module T : TERM
|
||||
(** Literals depend on terms *)
|
||||
|
||||
type t
|
||||
(** A literal *)
|
||||
|
||||
include Sidekick_sigs.EQ_HASH_PRINT with type t := t
|
||||
|
||||
val term : t -> T.Term.t
|
||||
(** Get the (positive) term *)
|
||||
|
||||
val sign : t -> bool
|
||||
(** Get the sign. A negated literal has sign [false]. *)
|
||||
|
||||
val neg : t -> t
|
||||
(** Take negation of literal. [sign (neg lit) = not (sign lit)]. *)
|
||||
|
||||
val abs : t -> t
|
||||
(** [abs lit] is like [lit] but always positive, i.e. [sign (abs lit) = true] *)
|
||||
|
||||
val signed_term : t -> T.Term.t * bool
|
||||
(** Return the atom and the sign *)
|
||||
|
||||
val atom : ?sign:bool -> T.Term.store -> T.Term.t -> t
|
||||
(** [atom store t] makes a literal out of a term, possibly normalizing
|
||||
its sign in the process.
|
||||
@param sign if provided, and [sign=false], negate the resulting lit. *)
|
||||
|
||||
val norm_sign : t -> t * bool
|
||||
(** [norm_sign (+t)] is [+t, true],
|
||||
and [norm_sign (-t)] is [+t, false].
|
||||
In both cases the term is positive, and the boolean reflects the initial sign. *)
|
||||
end
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
(library
|
||||
(name sidekick_sigs_proof_core)
|
||||
(public_name sidekick.sigs.proof.core)
|
||||
(synopsis "Common rules for proof traces")
|
||||
(flags :standard -open Sidekick_util)
|
||||
(libraries containers iter sidekick.util sidekick.sigs))
|
||||
|
|
@ -1,94 +0,0 @@
|
|||
(** Proof rules for common operations and congruence closure *)
|
||||
|
||||
module type S = sig
|
||||
type rule
|
||||
type term
|
||||
type lit
|
||||
|
||||
type step_id
|
||||
(** Identifier for a proof proof_rule (like a unique ID for a clause previously
|
||||
added/proved) *)
|
||||
|
||||
val lemma_cc : lit Iter.t -> rule
|
||||
(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
|
||||
of uninterpreted functions. *)
|
||||
|
||||
val define_term : term -> term -> rule
|
||||
(** [define_term cst u proof] defines the new constant [cst] as being equal
|
||||
to [u].
|
||||
The result is a proof of the clause [cst = u] *)
|
||||
|
||||
val proof_p1 : step_id -> step_id -> rule
|
||||
(** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
|
||||
and [p2] proves [C \/ t], is the rule that produces [C \/ u],
|
||||
i.e unit paramodulation. *)
|
||||
|
||||
val proof_r1 : step_id -> step_id -> rule
|
||||
(** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
|
||||
and [p2] proves [C \/ ¬t], is the rule that produces [C \/ u],
|
||||
i.e unit resolution. *)
|
||||
|
||||
val proof_res : pivot:term -> step_id -> step_id -> rule
|
||||
(** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l]
|
||||
and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot],
|
||||
is the rule that produces [C \/ D], i.e boolean resolution. *)
|
||||
|
||||
val with_defs : step_id -> step_id Iter.t -> rule
|
||||
(** [with_defs pr defs] specifies that [pr] is valid only in
|
||||
a context where the definitions [defs] are present. *)
|
||||
|
||||
val lemma_true : term -> rule
|
||||
(** [lemma_true (true) p] asserts the clause [(true)] *)
|
||||
|
||||
val lemma_preprocess : term -> term -> using:step_id Iter.t -> rule
|
||||
(** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
|
||||
and that [t] has been preprocessed into [u].
|
||||
|
||||
The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence
|
||||
closure, and then resolved against the clauses [using] to obtain
|
||||
a unit equality.
|
||||
|
||||
From now on, [t] and [u] will be used interchangeably.
|
||||
@return a rule ID for the clause [(t=u)]. *)
|
||||
|
||||
val lemma_rw_clause :
|
||||
step_id -> res:lit Iter.t -> using:step_id Iter.t -> rule
|
||||
(** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c],
|
||||
uses the equations [|- p_i = q_i] from [using]
|
||||
to rewrite some literals of [c] into [res]. This is used to preprocess
|
||||
literals of a clause (using {!lemma_preprocess} individually). *)
|
||||
end
|
||||
|
||||
type ('rule, 'step_id, 'term, 'lit) t =
|
||||
(module S
|
||||
with type rule = 'rule
|
||||
and type step_id = 'step_id
|
||||
and type term = 'term
|
||||
and type lit = 'lit)
|
||||
|
||||
(** Make a dummy proof with given types *)
|
||||
module Dummy (A : sig
|
||||
type rule
|
||||
type step_id
|
||||
type term
|
||||
type lit
|
||||
|
||||
val dummy_rule : rule
|
||||
end) :
|
||||
S
|
||||
with type rule = A.rule
|
||||
and type step_id = A.step_id
|
||||
and type term = A.term
|
||||
and type lit = A.lit = struct
|
||||
include A
|
||||
|
||||
let lemma_cc _ = dummy_rule
|
||||
let define_term _ _ = dummy_rule
|
||||
let proof_p1 _ _ = dummy_rule
|
||||
let proof_r1 _ _ = dummy_rule
|
||||
let proof_res ~pivot:_ _ _ = dummy_rule
|
||||
let with_defs _ _ = dummy_rule
|
||||
let lemma_true _ = dummy_rule
|
||||
let lemma_preprocess _ _ ~using:_ = dummy_rule
|
||||
let lemma_rw_clause _ ~res:_ ~using:_ = dummy_rule
|
||||
end
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
(library
|
||||
(name sidekick_sigs_proof_sat)
|
||||
(public_name sidekick.sigs.proof.sat)
|
||||
(synopsis "SAT-solving rules for proof traces")
|
||||
(flags :standard -open Sidekick_util)
|
||||
(libraries containers iter sidekick.util sidekick.sigs))
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
(** Proof rules for SAT Solver reasoning *)
|
||||
|
||||
module type S = sig
|
||||
type rule
|
||||
(** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
|
||||
|
||||
type step_id
|
||||
(** identifier for a proof *)
|
||||
|
||||
type lit
|
||||
(** A boolean literal for the proof trace *)
|
||||
|
||||
val sat_input_clause : lit Iter.t -> rule
|
||||
(** Emit an input clause. *)
|
||||
|
||||
val sat_redundant_clause : lit Iter.t -> hyps:step_id Iter.t -> rule
|
||||
(** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
|
||||
The clause must be RUP wrt [hyps]. *)
|
||||
|
||||
val sat_unsat_core : lit Iter.t -> rule
|
||||
(** TODO: is this relevant here? *)
|
||||
end
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
(library
|
||||
(name sidekick_sigs_proof_trace)
|
||||
(public_name sidekick.sigs.proof-trace)
|
||||
(synopsis "Common definition for proof traces")
|
||||
(libraries containers iter sidekick.sigs sidekick.util))
|
||||
|
|
@ -1,42 +0,0 @@
|
|||
(** Proof traces.
|
||||
*)
|
||||
|
||||
open Sidekick_util
|
||||
|
||||
module type ARG = sig
|
||||
type rule
|
||||
|
||||
type step_id
|
||||
(** Identifier for a tracing step (like a unique ID for a clause previously
|
||||
added/proved) *)
|
||||
|
||||
module Step_vec : Vec_sig.BASE with type elt = step_id
|
||||
(** A vector indexed by steps. *)
|
||||
end
|
||||
|
||||
module type S = sig
|
||||
module A : ARG
|
||||
|
||||
type t
|
||||
(** The proof trace itself.
|
||||
|
||||
A proof trace is a log of all deductive steps taken by the solver,
|
||||
so we can later reconstruct a certificate for proof-checking.
|
||||
|
||||
Each step in the proof trace should be a {b valid
|
||||
lemma} (of its theory) or a {b valid consequence} of previous steps.
|
||||
*)
|
||||
|
||||
val enabled : t -> bool
|
||||
(** Is proof tracing enabled? *)
|
||||
|
||||
val add_step : t -> A.rule -> A.step_id
|
||||
(** Create a new step in the trace. *)
|
||||
|
||||
val add_unsat : t -> A.step_id -> unit
|
||||
(** Signal "unsat" result at the given proof *)
|
||||
|
||||
val delete : t -> A.step_id -> unit
|
||||
(** Forget a step that won't be used in the rest of the trace.
|
||||
Only useful for performance/memory considerations. *)
|
||||
end
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
(library
|
||||
(name sidekick_sigs_term)
|
||||
(public_name sidekick.sigs.term)
|
||||
(synopsis "Common definition for terms and types")
|
||||
(libraries containers iter sidekick.sigs))
|
||||
|
|
@ -1,80 +0,0 @@
|
|||
(** Main representation of Terms and Types *)
|
||||
module type S = sig
|
||||
module Fun : Sidekick_sigs.EQ_HASH_PRINT
|
||||
(** A function symbol, like "f" or "plus" or "is_human" or "socrates" *)
|
||||
|
||||
(** Types
|
||||
|
||||
Types should be comparable (ideally, in O(1)), and have
|
||||
at least a boolean type available. *)
|
||||
module Ty : sig
|
||||
include Sidekick_sigs.EQ_HASH_PRINT
|
||||
|
||||
type store
|
||||
|
||||
val bool : store -> t
|
||||
val is_bool : t -> bool
|
||||
end
|
||||
|
||||
(** Term structure.
|
||||
|
||||
Terms should be {b hashconsed}, with perfect sharing.
|
||||
This allows, for example, {!Term.Tbl} and {!Term.iter_dag} to be efficient.
|
||||
*)
|
||||
module Term : sig
|
||||
include Sidekick_sigs.EQ_ORD_HASH_PRINT
|
||||
|
||||
type store
|
||||
(** A store used to create new terms. It is where the hashconsing
|
||||
table should live, along with other all-terms related store. *)
|
||||
|
||||
val ty : t -> Ty.t
|
||||
|
||||
val bool : store -> bool -> t
|
||||
(** build true/false *)
|
||||
|
||||
val as_bool : t -> bool option
|
||||
(** [as_bool t] is [Some true] if [t] is the term [true], and similarly
|
||||
for [false]. For other terms it is [None]. *)
|
||||
|
||||
val abs : store -> t -> t * bool
|
||||
(** [abs t] returns an "absolute value" for the term, along with the
|
||||
sign of [t].
|
||||
|
||||
The idea is that we want to turn [not a] into [(a, false)],
|
||||
or [(a != b)] into [(a=b, false)]. For terms without a negation this
|
||||
should return [(t, true)].
|
||||
|
||||
The store is passed in case a new term needs to be created. *)
|
||||
|
||||
val map_shallow : store -> (t -> t) -> t -> t
|
||||
(** Map function on immediate subterms. This should not be recursive. *)
|
||||
|
||||
val iter_shallow : store -> (t -> unit) -> t -> unit
|
||||
(** Iterate function on immediate subterms. This should not be recursive. *)
|
||||
|
||||
val iter_dag : t -> (t -> unit) -> unit
|
||||
(** [iter_dag t f] calls [f] once on each subterm of [t], [t] included.
|
||||
It must {b not} traverse [t] as a tree, but rather as a
|
||||
perfectly shared DAG.
|
||||
|
||||
For example, in:
|
||||
{[
|
||||
let x = 2 in
|
||||
let y = f x x in
|
||||
let z = g y x in
|
||||
z = z
|
||||
]}
|
||||
|
||||
the DAG has the following nodes:
|
||||
|
||||
{[ n1: 2
|
||||
n2: f n1 n1
|
||||
n3: g n2 n1
|
||||
n4: = n3 n3
|
||||
]}
|
||||
*)
|
||||
|
||||
module Tbl : CCHashtbl.S with type key = t
|
||||
end
|
||||
end
|
||||
Loading…
Add table
Reference in a new issue