[sledge] Port Ses equality solver to Fol term and formula representation

Summary:
Adapt the solver implementation from Ses.Equality to Context, and use
the interface of Fol.Context.

Reviewed By: jvillard

Differential Revision: D24532348

fbshipit-source-id: 2c6d41669

sledge/src/context.mli

@@ -0,0 +1,117 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Sets of assumptions, interpreted as conjunction, plus reasoning about
+    their logical consequences.
+
+    Functions that return contexts that might be stronger than their
+    argument contexts accept and return a set of variables. The input set is
+    the variables with which any generated variables must be chosen fresh,
+    and the output set is the variables that have been generated. *)
+
+open Fol
+
+type t [@@deriving sexp]
+
+val pp : t pp
+
+val ppx_diff :
+  Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool
+
+include Invariant.S with type t := t
+
+val empty : t
+(** The empty context of assumptions. *)
+
+val add : Var.Set.t -> Formula.t -> t -> Var.Set.t * t
+(** Add (that is, conjoin) an assumption to a context. *)
+
+val union : Var.Set.t -> t -> t -> Var.Set.t * t
+(** Union (that is, conjoin) two contexts of assumptions. *)
+
+val inter : Var.Set.t -> t -> t -> Var.Set.t * t
+(** Intersect (that is, disjoin) contexts of assumptions. *)
+
+val interN : Var.Set.t -> t list -> Var.Set.t * t
+(** Intersect contexts of assumptions. Possibly weaker than logical
+    disjunction. *)
+
+val dnf : Formula.t -> (Var.Set.t * Formula.t * t) iter
+(** Disjunctive-normal form expansion. *)
+
+val rename : t -> Var.Subst.t -> t
+(** Apply a renaming substitution to the context. *)
+
+val is_empty : t -> bool
+(** Test if the context of assumptions is empty. *)
+
+val is_unsat : t -> bool
+(** Test if the context of assumptions is inconsistent. *)
+
+val implies : t -> Formula.t -> bool
+(** Holds only if a formula is a logical consequence of a context of
+    assumptions. This only checks if the formula is valid in the current
+    state of the context, without doing any further logical reasoning or
+    propagation. *)
+
+val refutes : t -> Formula.t -> bool
+(** Holds only if a formula is inconsistent with a context of assumptions,
+    that is, conjoining the formula to the assumptions is unsatisfiable. *)
+
+val normalize : t -> Term.t -> Term.t
+(** Normalize a term [e] to [e'] such that [e = e'] is implied by the
+    assumptions, where [e'] and its subterms are expressed in terms of the
+    canonical representatives of each equivalence class. *)
+
+val class_of : t -> Term.t -> Trm.t list
+(** Equivalence class of [e]: all the terms [f] in the context such that
+    [e = f] is implied by the assumptions. *)
+
+val vars : t -> Var.t iter
+(** Enumerate the variables occurring in the terms of the context. *)
+
+val fv : t -> Var.Set.t
+(** The variables occurring in the terms of the context. *)
+
+(** Solution Substitutions *)
+module Subst : sig
+  type t
+
+  val pp : t pp
+  val is_empty : t -> bool
+  val fold_eqs : t -> 's -> f:(Formula.t -> 's -> 's) -> 's
+
+  val subst : t -> Term.t -> Term.t
+  (** Apply a substitution recursively to subterms. *)
+
+  val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
+  (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks
+      and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and
+      ks ∩ fv(τ) = ∅. *)
+end
+
+val apply_subst : Var.Set.t -> Subst.t -> t -> Var.Set.t * t
+(** Context induced by applying a solution substitution to a set of
+    equations generating the argument context. *)
+
+val solve_for_vars : Var.Set.t list -> t -> Subst.t
+(** [solve_for_vars vss x] is a solution substitution that is implied by [x]
+    and consists of oriented equalities [v ↦ e] that map terms [v] with
+    free variables contained in (the union of) a prefix [uss] of [vss] to
+    terms [e] with free variables contained in as short a prefix of [uss] as
+    possible. *)
+
+val elim : Var.Set.t -> t -> t
+(** [elim ks x] is [x] weakened by removing oriented equations [k ↦ _] for
+    [k] in [ks]. *)
+
+(**/**)
+
+val pp_raw : t pp
+
+val replay : string -> unit
+(** Replay debugging *)