simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 03:35:38 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Typos in doc

Browse source
This commit is contained in:
Guillaume Bury 2016-11-21 14:40:51 +01:00
parent 0ec4288d7c
commit 38972d7fc6
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/core/solver_types_intf.ml
View file

@ -28,9 +28,9 @@ module type S = sig
term : term; (** Wrapped term *) term : term; (** Wrapped term *)
mutable l_level : int; (** Decision level of the assignment *) mutable l_level : int; (** Decision level of the assignment *)
mutable l_weight : float; (** Weight (for the heap) *) mutable l_weight : float; (** Weight (for the heap) *)
mutable assigned : term option; (** Assignement *) mutable assigned : term option; (** Assignment *)
} }
(** Wrapper type for litterals, i.e theory terms (for mcsat only). *) (** Wrapper type for literals, i.e. theory terms (for mcsat only). *)
type var = { type var = {
vid : int; (** Unique identifier *) vid : int; (** Unique identifier *)
@ -42,7 +42,7 @@ module type S = sig
mutable v_assignable: lit list option; mutable v_assignable: lit list option;
(** In mcsat, the list of lits that wraps subterms of the formula wrapped. *) (** In mcsat, the list of lits that wraps subterms of the formula wrapped. *)
mutable reason : reason option; mutable reason : reason option;
(** The reason for propagation/decision of the litteral *) (** The reason for propagation/decision of the literal *)
} }
and atom = { and atom = {
@ -66,10 +66,10 @@ module type S = sig
mutable cpremise : premise; (** The premise of the clause, i.e. the justification mutable cpremise : premise; (** The premise of the clause, i.e. the justification
of why the clause must be satisfied. *) of why the clause must be satisfied. *)
mutable activity : float; (** Clause activity, used for the heap heuristics. *) mutable activity : float; (** Clause activity, used for the heap heuristics. *)
mutable attached : bool; (** Is the clause attached, i.e. does it watsh literals. *) mutable attached : bool; (** Is the clause attached, i.e. does it watch literals. *)
mutable visited : bool; (** Boolean used during propagation and proof generation. *) mutable visited : bool; (** Boolean used during propagation and proof generation. *)
} }
(** The type of clauses. Each clause generated should be true, i.e enforced (** The type of clauses. Each clause generated should be true, i.e. enforced
by the current problem (for more information, see the cpremise field). *) by the current problem (for more information, see the cpremise field). *)
and reason = and reason =
@ -87,8 +87,8 @@ module type S = sig
the given proof. *) the given proof. *)
| History of clause list (** The clause can be obtained by resolution of the clauses | History of clause list (** The clause can be obtained by resolution of the clauses
in the list. For a premise [History [a_1 :: ... :: a_n]] in the list. For a premise [History [a_1 :: ... :: a_n]]
the claus eis obtained by performing resolution of the clause is obtained by performing resolution of
[a_1] with [a_2], and then performin a resolution step between [a_1] with [a_2], and then performing a resolution step between
the result and [a_3], etc... the result and [a_3], etc...
Of course, each of the clause [a_i] also has its own premise. *) Of course, each of the clause [a_i] also has its own premise. *)
(** Premises for clauses. Indeed each clause generated during a run of the solver (** Premises for clauses. Indeed each clause generated during a run of the solver