Metis/src/Model.sig

16 (* A model of size N has integer elements 0...N-1.                           *)
26 (* The parts of the model that are fixed.                                    *)
55 (* Renaming fixed model parts.                                               *)
67 (* Standard fixed model parts.                                               *)
202 type model
206 val new : parameters -> model
208 val size : model -> int
211 (* Interpreting terms and formulas in the model.                             *)
214 val interpretFunction : model -> Term.functionName * element list -> element
216 val interpretRelation : model -> Atom.relationName * element list -> bool
218 val interpretTerm : model -> valuation -> Term.term -> element
220 val interpretAtom : model -> valuation -> Atom.atom -> bool
222 val interpretFormula : model -> valuation -> Formula.formula -> bool
224 val interpretLiteral : model -> valuation -> Literal.literal -> bool
226 val interpretClause : model -> valuation -> Thm.clause -> bool
229 (* Check whether random groundings of a formula are true in the model.       *)
234     (model -> valuation -> 'a -> bool) -> {maxChecks : int option} -> model ->
238     {maxChecks : int option} -> model -> Atom.atom -> {T : int, F : int}
241     {maxChecks : int option} -> model -> Formula.formula -> {T : int, F : int}
244     {maxChecks : int option} -> model -> Literal.literal -> {T : int, F : int}
247     {maxChecks : int option} -> model -> Thm.clause -> {T : int, F : int}
250 (* Updating the model.                                                       *)
254     model -> (Term.functionName * element list) * element -> unit
257     model -> (Atom.relationName * element list) * bool -> unit
260 (* Choosing a random perturbation to make a formula true in the model.       *)
263 val perturbTerm : model -> valuation -> Term.term * element list -> unit
265 val perturbAtom : model -> valuation -> Atom.atom * bool -> unit
267 val perturbLiteral : model -> valuation -> Literal.literal -> unit
269 val perturbClause : model -> valuation -> Thm.clause -> unit
275 val pp : model Print.pp