From be46f40312b81dae93eccbd882bbb84c84546f10 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 3 Jul 2021 21:46:39 -0400 Subject: [PATCH] more docs --- src/base/Base_types.ml | 34 ++++++++++++++++++++++++++++++++-- src/base/ID.ml | 5 ----- src/base/ID.mli | 34 +++++++++++++++++++++++++--------- src/base/Model.ml | 2 -- src/base/Model.mli | 22 +++++++++++++++++++++- src/base/Proof.ml | 1 + src/base/Proof.mli | 11 +++++++++++ src/base/Sidekick_base.ml | 3 ++- src/core/Sidekick_core.ml | 8 +++++++- 9 files changed, 99 insertions(+), 21 deletions(-) diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index 3b80d725..0ce03541 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -1,3 +1,5 @@ +(** Basic type definitions for Sidekick_base *) + module Vec = Msat.Vec module Log = Msat.Log module Fmt = CCFormat @@ -16,14 +18,20 @@ type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view = | LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num | LRA_other of 'a -(* main term cell. *) +(** Term. + + A term, with its own view, type, and a unique identifier. + Do not create directly, see {!Term}. *) type term = { mutable term_id: int; (* unique ID *) mutable term_ty: ty; term_view : term term_view; } -(* term shallow structure *) +(** Shallow structure of a term. + + A term is a DAG (direct acyclic graph) of nodes, each of which has a + term view. *) and 'a term_view = | Bool of bool | App_fun of fun_ * 'a IArray.t (* full, first-order application *) @@ -36,6 +44,7 @@ and fun_ = { fun_id: ID.t; fun_view: fun_view; } +(** type of function symbols *) and fun_view = | Fun_undef of fun_ty (* simple undefined constant *) @@ -258,6 +267,7 @@ let pp_term_top ~ids out t = let pp_term = pp_term_top ~ids:false let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term +(** Types *) module Ty : sig type t = ty type state = unit @@ -436,6 +446,7 @@ end = struct end end +(** Function symbols *) module Fun : sig type view = fun_view = | Fun_undef of fun_ty (* simple undefined constant *) @@ -758,6 +769,7 @@ end = struct end) end +(** Term creation and manipulation *) module Term : sig type t = term = { mutable term_id : int; @@ -999,6 +1011,7 @@ end = struct | LRA l -> lra tst (Sidekick_arith_lra.map_view f l) end +(** Values (used in models) *) module Value : sig type t = value = | V_bool of bool @@ -1070,6 +1083,7 @@ end = struct mk_elt (ID.makef "v_%d" t.term_id) t.term_ty end +(** Datatypes *) module Data = struct type t = data = { data_id: ID.t; @@ -1080,6 +1094,10 @@ module Data = struct let pp out d = ID.pp out d.data_id end +(** Datatype selectors. + + A selector is a kind of function that allows to obtain an argument + of a given constructor. *) module Select = struct type t = select = { select_id: ID.t; @@ -1091,6 +1109,10 @@ module Select = struct let ty sel = Lazy.force sel.select_ty end +(** Datatype constructors. + + A datatype has one or more constructors, each of which is a special + kind of function symbol. Constructors are injective and pairwise distinct. *) module Cstor = struct type t = cstor = { cstor_id: ID.t; @@ -1107,6 +1129,13 @@ module Cstor = struct let pp out c = ID.pp out c.cstor_id end +(* TODO: check-sat-assuming, get-unsat-assumptions, push, pop *) + +(** Statements. + + A statement is an instruction for the SMT solver to do something, + like asserting that a formula is true, declaring a new constant, + or checking satisfiabilty of the current set of assertions. *) module Statement = struct type t = statement = | Stmt_set_logic of string @@ -1121,6 +1150,7 @@ module Statement = struct | Stmt_check_sat of (bool * term) list | Stmt_exit + (** Pretty print a statement *) let pp out = function | Stmt_set_logic s -> Fmt.fprintf out "(set-logic %s)" s | Stmt_set_option l -> Fmt.fprintf out "(@[set-logic@ %a@])" (Util.pp_list Fmt.string) l diff --git a/src/base/ID.ml b/src/base/ID.ml index 3614d9ae..8f928002 100644 --- a/src/base/ID.ml +++ b/src/base/ID.ml @@ -38,8 +38,3 @@ end module Map = CCMap.Make(AsKey) module Set = CCSet.Make(AsKey) module Tbl = CCHashtbl.Make(AsKey) - -module B = struct - let int = make "int" - let rat = make "rat" -end diff --git a/src/base/ID.mli b/src/base/ID.mli index 8f2b1e76..454e04ef 100644 --- a/src/base/ID.mli +++ b/src/base/ID.mli @@ -1,18 +1,42 @@ (* This file is free software. See file "license" for more details. *) -(** {1 Unique Identifiers} *) +(** Unique Identifiers *) + +(** + We use generative identifiers everywhere in [Sidekick_base]. Unlike + strings, there are no risk of collision: during parsing, a new + declaration or definition should create a fresh [ID.t] and associate + it with the string name, and later references should look into some hashtable + or map to get the ID corresponding to a string. + + This allows us to handle definition shadowing or binder shadowing easily. +*) type t +(** The opaque type of unique identifiers *) val make : string -> t +(** [make s] creates a new identifier with name [s] + and some internal information. It is different than any other identifier + created before or after, even with the same name. *) + val makef : ('a, Format.formatter, unit, t) format4 -> 'a +(** [makef "foo %d bar %b" 42 true] is like + [make (Format.asprintf "foo %d bar %b" 42 true)]. *) + val copy : t -> t +(** Fresh copy of the identifier, distinct from it, but with the + same name. *) val id : t -> int +(** Unique integer counter for this identifier. *) val to_string : t -> string +(** Print identifier. *) + val to_string_full : t -> string +(** Printer name and unique counter for this ID. *) include Intf.EQ with type t := t include Intf.ORD with type t := t @@ -25,11 +49,3 @@ module Map : CCMap.S with type key = t module Set : CCSet.S with type elt = t module Tbl : CCHashtbl.S with type key = t - -module B : sig - val rat : t - val int : t - -end - - diff --git a/src/base/Model.ml b/src/base/Model.ml index 220785c6..c4a8f6a4 100644 --- a/src/base/Model.ml +++ b/src/base/Model.ml @@ -1,7 +1,5 @@ (* This file is free software. See file "license" for more details. *) -(** {1 Model} *) - open Base_types module Val_map = struct diff --git a/src/base/Model.mli b/src/base/Model.mli index 1d80a308..44e8a32d 100644 --- a/src/base/Model.mli +++ b/src/base/Model.mli @@ -1,6 +1,14 @@ (* This file is free software. See file "license" for more details. *) -(** {1 Model} *) +(** Models + + A model is a solution to the satisfiability question, created by the + SMT solver when it proves the formula to be {b satisfiable}. + + A model gives a value to each term of the original formula(s), in + such a way that the formula(s) is true when the term is replaced by its + value. +*) open Base_types @@ -14,6 +22,14 @@ module Val_map : sig val add : key -> 'a -> 'a t -> 'a t end +(** Model for function symbols. + + Function models are a finite map from argument tuples to values, + accompanied with a default value that every other argument tuples + map to. In other words, it's of the form: + + [lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault] +*) module Fun_interpretation : sig type t = { cases: Value.t Val_map.t; @@ -29,11 +45,13 @@ module Fun_interpretation : sig t end +(** Model *) type t = { values: Value.t Term.Map.t; funs: Fun_interpretation.t Fun.Map.t; } +(** Empty model *) val empty : t val add : Term.t -> Value.t -> t -> t @@ -46,4 +64,6 @@ val merge : t -> t -> t val pp : t CCFormat.printer +(** [eval m t] tries to evaluate term [t] in the model. + If it succeeds, the value is returned, otherwise [None] is. *) val eval : t -> Term.t -> Value.t option diff --git a/src/base/Proof.ml b/src/base/Proof.ml index 7feb5117..6a094795 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -1,3 +1,4 @@ + open Base_types module T = Term diff --git a/src/base/Proof.mli b/src/base/Proof.mli index 347bc339..2cf5fe41 100644 --- a/src/base/Proof.mli +++ b/src/base/Proof.mli @@ -1,3 +1,14 @@ +(** Proofs of unsatisfiability + + Proofs are used in sidekick when the problem is found {b unsatisfiable}. + A proof collects inferences made by the solver into a list of steps, + each with its own kind of justification (e.g. "by congruence"), + and outputs it in some kind of format. + + Currently we target {{: https://c-cube.github.io/quip-book/ } Quip} + as an experimental proof backend. +*) + open Base_types include Sidekick_core.PROOF diff --git a/src/base/Sidekick_base.ml b/src/base/Sidekick_base.ml index ad423b9b..6d50cdcf 100644 --- a/src/base/Sidekick_base.ml +++ b/src/base/Sidekick_base.ml @@ -6,7 +6,8 @@ It provides a representation of terms, boolean formulas, linear arithmetic expressions, datatypes for the functors in Sidekick. - In addition, it has a notion of {!Statement}. Statements are instructions + In addition, it has a notion of {{!Base_types.Statement} Statement}. + Statements are instructions for the SMT solver to do something, such as: define a new constant, declare a new constant, assert a formula as being true, set an option, check satisfiability of the set of statements added so far, diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index f5136f17..67378baf 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -145,10 +145,15 @@ module type TERM = sig end end +(** Proofs of unsatisfiability *) module type PROOF = sig + type t + (** The abstract representation of a proof. A proof always proves + a clause to be {b valid} (true in every possible interpretation + of the problem's assertions, and the theories) *) + type term type ty - type t type hres_step (** hyper-resolution steps: resolution, unit resolution; @@ -179,6 +184,7 @@ module type PROOF = sig val lit_sign : lit -> bool type composite_step + val stepc : name:string -> lit list -> t -> composite_step val deft : term -> term -> composite_step (** define a (new) atomic term *)