diff --git a/src/arith.ml b/src/arith.ml
index 74cdfc66ee872504aa3edf31a4ee1c2315d43ac2..93bc177c9dbebb8ea716e2e1efe99dbd1b1b8943 100644
--- a/src/arith.ml
+++ b/src/arith.ml
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
open Stdlib
+open Types
open Solver
let debug = Debug.register_info_flag
diff --git a/src/arith.mli b/src/arith.mli
index 21e765358503e5ea65b6257a8a0e5d9fd9ae6505..1a37a073cfe40b9a48409db4485122be2bdca345 100644
--- a/src/arith.mli
+++ b/src/arith.mli
@@ -19,6 +19,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
+open Types
open Solver
type env = Solver.t
diff --git a/src/bool.ml b/src/bool.ml
index 878866da273ac370c84bd6ed3181332f70a83fe1..f69b2fcdad83633555c3622565623f9b3fed10cf 100644
--- a/src/bool.ml
+++ b/src/bool.ml
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
open Stdlib
+open Types
open Solver
let lazy_propagation = false
diff --git a/src/bool.mli b/src/bool.mli
index edcbcab5309981eabdba1521b1b5375809274159..37922ef6cd9f8ae0975f781af20c26b2f14f6209 100644
--- a/src/bool.mli
+++ b/src/bool.mli
@@ -19,11 +19,12 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
+open Types
open Solver
type t
-val sem: t Solver.sem
-val dom: bool Solver.dom
+val sem: t sem
+val dom: bool dom
val _true : Solver.t -> Cl.t
diff --git a/src/equality.ml b/src/equality.ml
index c0ab5fcdca850c69adba3c85de826ec1c1b02c17..57c7b73b3bb2b418a72004b9f8635935d5fc8dd2 100644
--- a/src/equality.ml
+++ b/src/equality.ml
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
open Stdlib
+open Types
open Solver
let debug = Debug.register_info_flag
diff --git a/src/equality.mli b/src/equality.mli
index 41d0167af714b3f230d56b1ce04893dca40bd481..2c9cb379ada77f58f27f71b1d404e9bb21baac9a 100644
--- a/src/equality.mli
+++ b/src/equality.mli
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
open Stdlib
+open Types
open Solver
module Dis : sig type t end (* TODO complete *)
diff --git a/src/inputlang/dimacs_cnf/dimacs.mll b/src/inputlang/dimacs_cnf/dimacs.mll
index 716753cc39d2ad22a762b4fe62b5b4015cf20c5c..f97df55f0a3f441bc7c39e863f9b28389082ec0e 100644
--- a/src/inputlang/dimacs_cnf/dimacs.mll
+++ b/src/inputlang/dimacs_cnf/dimacs.mll
@@ -23,7 +23,7 @@
{
open Lexing
-type vars = Solver.Cl.t array
+type vars = Types.Cl.t array
let get_indice i =
if i > 0 then (i-1)*2
else if i < 0 then (-i-1)*2+1
diff --git a/src/scheduler_queue.ml b/src/scheduler_queue.ml
index 21023ac79bf0b9c9c3ac4555e3c332dc6be04a8f..2c090b547633c43045d2fd56bce25d641455044f 100644
--- a/src/scheduler_queue.ml
+++ b/src/scheduler_queue.ml
@@ -108,7 +108,7 @@ module Make(X:module type of Solver) = struct
begin
try
X.flush d'; X.delayed_stop d'
- with X.Contradiction ->
+ with Types.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction@.";
(** The other branch is directly unsat: remove prev from the list *)
t.prev_solver_state <- prev.prev_solver_state
@@ -128,7 +128,7 @@ module Make(X:module type of Solver) = struct
let d =
try
X.flush d; d
- with X.Contradiction ->
+ with Types.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction@.";
match t.prev_solver_state with
| None ->
@@ -154,7 +154,7 @@ module Make(X:module type of Solver) = struct
let d =
try
X.flush d; d
- with X.Contradiction ->
+ with Types.Contradiction ->
match t.prev_solver_state with
| None ->
Debug.dprintf0 debug "[Sched] Contradiction@.";
@@ -169,7 +169,7 @@ module Make(X:module type of Solver) = struct
let d =
try
run_one_step t d att
- with X.Contradiction ->
+ with Types.Contradiction ->
match t.prev_solver_state with
| None ->
Debug.dprintf0 debug "[Sched] Contradiction@.";
@@ -191,7 +191,7 @@ module Make(X:module type of Solver) = struct
d, (fun () ->
try
X.flush d; X.delayed_stop d
- with X.Contradiction ->
+ with Types.Contradiction ->
match t.prev_solver_state with
| None ->
Debug.dprintf0 debug "[Sched] Contradiction@.";
diff --git a/src/solver.ml b/src/solver.ml
index 6fef520147b13e9bdaee0ed25d1954f07aea5474..555c87131cc88d6171fdbe26adba80ce1fd4b60b 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -21,35 +21,12 @@
(**************************************************************************)
open Stdlib
-
+open Types
let debug = Debug.register_info_flag
~desc:"for the core solver in the simple version"
"simple_core"
-exception BrokenInvariant of string
-exception Impossible (* Absurd *)
-exception Contradiction
-exception SolveSameRepr
-exception UnregisteredKey
-exception AlreadyRegisteredKey
-exception UnwaitedEvent
-exception AlreadyDead
-
-module Cl = Strings.Fresh(struct end)
-
-module KDom = Strings.Fresh(struct end)
-module KSem = Strings.Fresh(struct end)
-module KDem = Strings.Fresh(struct end)
-
-type 'a dom = KDom.t (* >= 0 *)
-type 'a sem = KSem.t (* >= 0 *)
-type ('k,'d) dem = KDem.t (* >= 0 *)
-
-module EqDom = Eqtype.Make1(struct type 'a t = 'a dom end)
-module EqSem = Eqtype.Make1(struct type 'a t = 'a sem end)
-module EqDem = Eqtype.Make2(struct type ('a,'b) t = ('a,'b) dem end)
-
module Print = struct (** Cutting the knot for printer *)
type psem = { mutable psem : 'a. ('a sem -> Format.formatter -> 'a -> unit)}
@@ -129,9 +106,9 @@ module Events = struct
| EventUser (ue, _) ->
KUE.print fmt ue
| EventDom (cl, dom, _) ->
- Format.fprintf fmt "dom:%a of %a" KDom.print dom Cl.print cl
+ Format.fprintf fmt "dom:%a of %a" KDom.print (dom :> KDom.t) Cl.print cl
| EventSem (cl, sem, _) ->
- Format.fprintf fmt "sem:%a of %a" KSem.print sem Cl.print cl
+ Format.fprintf fmt "sem:%a of %a" KSem.print (sem :> KSem.t) Cl.print cl
| EventPropaCl (cl, _) ->
Format.fprintf fmt "propagation of %a" Cl.print cl
| EventPropa _ ->
@@ -139,7 +116,7 @@ module Events = struct
| EventChange (cl, _) ->
Format.fprintf fmt "changecl of %a" Cl.print cl
| EventPropaSem (sem, _) ->
- Format.fprintf fmt "propasem for %a" KSem.print sem
+ Format.fprintf fmt "propasem for %a" KSem.print (sem :> KSem.t)
type 'b t = 'b event list
@@ -153,7 +130,7 @@ module Events = struct
| Event (dem, key, data) ->
let f (type k) (type d) (dem:(k,d) dem) (key : k) (data : d) =
Format.fprintf fmt "Daemon %a event (%a,%a)"
- KDem.print dem
+ KDem.print (dem :> KDem.t)
(Print.dem_key dem) key
(Print.dem_data dem) data in
f dem key data
@@ -197,10 +174,10 @@ module Events = struct
| EventUser (ue, v, _) ->
Format.fprintf fmt "%a with %a" KUE.print ue (print_ue ue) v
| EventDom (cl, dom, _) ->
- Format.fprintf fmt "dom:%a of %a" KDom.print dom Cl.print cl
+ Format.fprintf fmt "dom:%a of %a" KDom.print (dom :> KDom.t) Cl.print cl
| EventSem (cl, sem, v, _) ->
Format.fprintf fmt "sem:%a of %a with %a"
- KSem.print sem Cl.print cl (Print.sem sem) v
+ KSem.print (sem :> KSem.t) Cl.print cl (Print.sem sem) v
| EventPropa (cl, _) ->
Format.fprintf fmt "any propagation of %a" Cl.print cl
| EventPropaCl (cl, _) ->
@@ -209,7 +186,7 @@ module Events = struct
Format.fprintf fmt "changecl of %a" Cl.print cl
| EventPropaSem (cl, sem, v, _) ->
Format.fprintf fmt "propasem:%a of %a with %a"
- KSem.print sem Cl.print cl (Print.sem sem) v
+ KSem.print (sem :> KSem.t) Cl.print cl (Print.sem sem) v
type 'b t = 'b event list
end
@@ -299,11 +276,11 @@ module type SemTable' = sig
end
-module VDomTable = Vector_hetero.Make1(struct type 'a t = 'a dom end)
+module VDomTable = Vector_Dom
(struct type ('a,'delayed) t =
(module DomTable' with type dt = 'a and type delayed = 'delayed)
end)
-module VSemTable = Vector_hetero.Make1(struct type 'a t = 'a sem end)
+module VSemTable = Vector_Sem
(struct type ('a,'delayed) t =
(module SemTable' with type dt = 'a and type delayed = 'delayed)
end)
@@ -323,8 +300,7 @@ module type DemTable' = sig
end
-module VDemTable = Vector_hetero.Make2
- (struct type ('k,'d) t = ('k,'d) dem end)
+module VDemTable = Vector_Dem
(struct type ('k,'d,'delayed) t =
(module DemTable' with type delayed = 'delayed
and type dk = 'k
@@ -450,16 +426,15 @@ module type Dom = Dom' with type delayed := delayed_t
module type Sem = Sem' with type delayed := delayed_t
module type Dem = Dem' with type delayed := delayed_t
-module VDom = Vector_hetero.Make1(struct type 'a t = 'a dom end)
+module VDom = Vector_Dom
(struct type ('a,'unedeed) t =
(module Dom with type t = 'a)
end)
-module VSem = Vector_hetero.Make1(struct type 'a t = 'a sem end)
+module VSem = Vector_Sem
(struct type ('a,'unedeed) t =
(module Sem with type t = 'a)
end)
-module VDem = Vector_hetero.Make2
- (struct type ('k,'d) t = ('k,'d) dem end)
+module VDem = Vector_Dem
(struct type ('k,'d,'unedeed) t =
(module Dem with type k = 'k
and type d = 'd)
@@ -469,11 +444,6 @@ let defined_dom : unit VDom.t = VDom.create 8
let defined_sem : unit VSem.t = VSem.create 8
let defined_dem : unit VDem.t = VDem.create 8
-
-let create_sem_key s = KSem.create s
-let create_dom_key s = KDom.create s
-let create_dem_key s = KDem.create s
-
module RegisterDom (D:Dom) = struct
let () =
@@ -678,7 +648,7 @@ let output_graph filename t =
and type dt = VSemTable.exi) in
let iter s cl =
let mssg = Pp.sprintf_wnl "| {%a | %a} "
- KSem.print Sem.S.key Sem.S.print s in
+ KSem.print (Sem.S.key :> KSem.t) Sem.S.print s in
let mssg' = (Cl.H.find_def table "" cl) in
let mssg = mssg' ^ mssg in
Cl.H.replace table cl mssg
@@ -695,7 +665,7 @@ let output_graph filename t =
try
let s = Cl.M.find cl Dom.table in
Format.fprintf fmt "{%a | %a}"
- KDom.print Dom.D.key Dom.D.print s;
+ KDom.print (Dom.D.key :> KDom.t) Dom.D.print s;
with Not_found -> ()
in
Format.fprintf fmt "{%a %s| %a}" (* "{%a | %a | %a}" *)
@@ -831,7 +801,7 @@ module Delayed = struct
Some (Alive (event::d)))
k DemTable.state in
Debug.dprintf6 debug "[Solver] @[schedule %a for %a with %a@]@."
- KDem.print dem (print_dem_key dem) k
+ KDem.print (dem :> KDem.t) (print_dem_key dem) k
Events.Fired.print event;
let module DemTable' = struct
include DemTable
@@ -1037,7 +1007,7 @@ module Delayed = struct
let module DemTable =
(val demtable : DemTable with type dk = k and type dd = d) in
Debug.dprintf4 debug "[Solver] @[Kill dem %a %a@]@."
- KDem.print dem DemTable.D.Key.print k;
+ KDem.print (dem :> KDem.t) DemTable.D.Key.print k;
let module DemTable' = struct
include DemTable
let state = DemTable.D.Key.M.change (function
@@ -1052,11 +1022,12 @@ module Delayed = struct
(type k) (type d) d cl (dem:(k,d) dem) : (k * d) list =
List.fold_left (fun acc event ->
match event with
- | Events.Wait.Event(dem',k,d) when KDem.equal dem dem' ->
+ | Events.Wait.Event(dem',k,d)
+ when KDem.equal (dem :> KDem.t) (dem' :> KDem.t) ->
let f (type k) (type d) (type k') (type d')
(dem:(k,d) dem) (dem':(k',d') dem) (k:k') (d:d') : (k * d) =
match EqDem.coerce_type dem dem' with
- | (Eqtype.Eq : (k',k) Eqtype.eq) , (Eqtype.Eq : (d',d) Eqtype.eq) ->
+ | (Eqtype.Eq : (k,k') Eqtype.eq) , (Eqtype.Eq : (d,d') Eqtype.eq) ->
(k:k),(d:d) in
(f dem dem' k d)::acc
| _ -> acc
@@ -1388,8 +1359,7 @@ module Delayed = struct
| Some repr_events ->
Some (List.rev_append other_events repr_events))
repr_cl DomTable.events in
- let module DomTable' :
- DomTable' with type delayed = delayed_t = struct
+ let module DomTable' = struct
include DomTable
let table =
let table1 =
@@ -1498,11 +1468,11 @@ module Delayed = struct
match DemTable.D.Key.M.find k (DemTable.state) with
| Dead ->
Debug.dprintf4 debug "[Solver] @[Daemon %a for %a is dead@]@."
- KDem.print dem DemTable.D.Key.print k;
+ KDem.print (dem :> KDem.t) DemTable.D.Key.print k;
assert false
| Alive events ->
Debug.dprintf6 debug "[Solver] @[Run daemon %a for %a:@\n@[%a@]@]@."
- KDem.print dem DemTable.D.Key.print k
+ KDem.print (dem :> KDem.t) DemTable.D.Key.print k
(Pp.print_list Pp.newline Events.Fired.print) events;
(** event can be added during wakeup *)
let module DemTable' = struct
@@ -1577,7 +1547,7 @@ module Delayed = struct
match Queue.pop t.todo_merge_dom with
| SetMergeDomCl(dom,cl1,cl2) ->
Debug.dprintf6 debug "[Solver] @[do_pending SetDomCl %a %a %a@]@."
- KDom.print dom Cl.print cl1 Cl.print cl2;
+ KDom.print (dom :> KDom.t) Cl.print cl1 Cl.print cl2;
merge_dom_pending t dom cl1 cl2;
do_pending t
| SetMergeDomVal(dom,cl,v) ->
diff --git a/src/solver.mli b/src/solver.mli
index 5f734286fd062aa9eff878f4d4be638b3b6d1961..1ac148ff6dd953c3cf95317051b7adbd8d8ecec2 100644
--- a/src/solver.mli
+++ b/src/solver.mli
@@ -21,34 +21,7 @@
(**************************************************************************)
open Stdlib
-
-(** {2 Types } *)
-
-exception SolveSameRepr
-exception Contradiction
-exception UnwaitedEvent
-exception Impossible (* Absurd *)
-exception AlreadyDead
-
-(** Classes *)
-module Cl : sig
- include Datatype
- val create: string -> t
- (** the string is used as the prefix for the debug output *)
-end
-
-type 'a sem
-(** key of a kind of semantic values of type 'a *)
-
-module EqSem: Eqtype.S1 with type 'a t = 'a sem
-
-type 'a dom
-(** key of a domain of type 'a *)
-
-module EqDom: Eqtype.S1 with type 'a t = 'a dom
-
-type ('k,'d) dem
-(** kind of daemon for semantic value of type 'a *)
+open Types
module Events : sig
type 'u user_event (** User event *)
@@ -166,14 +139,6 @@ end
(** {2 Domains and Semantic Values key creation} *)
-(** the key shouldn't be used before its registration and shouldn't be
- registered again *)
-exception UnregisteredKey
-exception AlreadyRegisteredKey
-val create_dom_key: string -> 'a dom
-val create_sem_key: string -> 'a sem
-val create_dem_key: string -> ('k,'d) dem
-
module type Dom = sig
type t
diff --git a/src/types.ml b/src/types.ml
new file mode 100644
index 0000000000000000000000000000000000000000..6b9e9314b6bb2ceaef7e03d5873f88b3c6c9308a
--- /dev/null
+++ b/src/types.ml
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+
+exception BrokenInvariant of string
+exception Impossible (* Absurd *)
+exception Contradiction
+exception SolveSameRepr
+exception UnregisteredKey
+exception AlreadyRegisteredKey
+exception UnwaitedEvent
+exception AlreadyDead
+
+module Cl = Strings.Fresh(struct end)
+
+module KDom = Strings.Fresh(struct end)
+module KSem = Strings.Fresh(struct end)
+module KDem = Strings.Fresh(struct end)
+
+type 'a dom = KDom.t (* >= 0 *)
+type 'a sem = KSem.t (* >= 0 *)
+type ('k,'d) dem = KDem.t (* >= 0 *)
+
+module EqDom = Eqtype.Make1(struct type 'a t = 'a dom end)
+module EqSem = Eqtype.Make1(struct type 'a t = 'a sem end)
+module EqDem = Eqtype.Make2(struct type ('a,'b) t = ('a,'b) dem end)
+
+let create_sem_key s = KSem.create s
+let create_dom_key s = KDom.create s
+let create_dem_key s = KDem.create s
+
+
+module Vector_Dom(D:sig type ('a,'b) t end) =
+ Vector_hetero.Make1(struct type 'a t = 'a dom end)(D)
+
+module Vector_Sem(D:sig type ('a,'b) t end) =
+ Vector_hetero.Make1(struct type 'a t = 'a sem end)(D)
+
+module Vector_Dem(D:sig type ('k,'d,'b) t end) =
+ Vector_hetero.Make2(struct type ('k,'d) t = ('k,'d) dem end)(D)
diff --git a/src/types.mli b/src/types.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d4f5c45543533d04c666c21ff68a5e425a33f745
--- /dev/null
+++ b/src/types.mli
@@ -0,0 +1,73 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Stdlib
+
+(** {2 Types } *)
+
+exception SolveSameRepr
+exception Contradiction
+exception UnwaitedEvent
+exception Impossible (* Absurd *)
+exception AlreadyDead
+
+(** Classes *)
+module Cl : sig
+ include Datatype
+ val create: string -> t
+ (** the string is used as the prefix for the debug output *)
+end
+
+module KSem: Datatype
+type 'a sem = private KSem.t
+(** key of a kind of semantic values of type 'a *)
+module EqSem: Eqtype.S1 with type 'a t = 'a sem
+
+module KDom: Datatype
+type 'a dom = private KDom.t
+(** key of a domain of type 'a *)
+module EqDom: Eqtype.S1 with type 'a t = 'a dom
+
+module KDem: Datatype
+type ('k,'d) dem = private KDem.t
+(** kind of daemon for semantic value of type 'a *)
+module EqDem: Eqtype.S2 with type ('k,'d) t = ('k,'d) dem
+
+(** the key shouldn't be used before its registration and shouldn't be
+ registered again *)
+exception UnregisteredKey
+exception AlreadyRegisteredKey
+val create_dom_key: string -> 'a dom
+val create_sem_key: string -> 'a sem
+val create_dem_key: string -> ('k,'d) dem
+
+open Vector_hetero
+
+module Vector_Dom(D:sig type ('a,'b) t end)
+ : S1 with type 'a key = 'a dom and type ('a,'b) data = ('a,'b) D.t
+
+module Vector_Sem(D:sig type ('a,'b) t end)
+ : S1 with type 'a key = 'a sem and type ('a,'b) data = ('a,'b) D.t
+
+module Vector_Dem(D:sig type ('k,'d,'b) t end)
+ : S2 with type ('k,'d) key = ('k,'d) dem
+ and type ('k,'d,'b) data = ('k,'d,'b) D.t
diff --git a/src/uninterp.ml b/src/uninterp.ml
index 17a7fc7701d1dcabf4022f55e9cbc0159564038c..d805b2faafb485bb9c313e5709d0aec781042a82 100644
--- a/src/uninterp.ml
+++ b/src/uninterp.ml
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
open Stdlib
+open Types
open Solver
let debug = Debug.register_info_flag
diff --git a/src/uninterp.mli b/src/uninterp.mli
index b0b7b0b23898087b5e8d66f97af993c181fce182..7bd6cbd7bcde58e3c4af557adb2cf852ceaea0dd 100644
--- a/src/uninterp.mli
+++ b/src/uninterp.mli
@@ -20,11 +20,12 @@
(* *)
(**************************************************************************)
+open Types
open Solver
type t = App of Cl.t * Cl.t
-val sem: t Solver.sem
+val sem: t sem
val app: Solver.t -> Cl.t -> Cl.t -> Cl.t
val appl: Solver.t -> Cl.t -> Cl.t list -> Cl.t
diff --git a/src/variable.ml b/src/variable.ml
index a09d8df31a25d98481459aa2ce3e09ee26f84fc7..6ad6b788ac16f2c79358803c6896dc86c091219b 100644
--- a/src/variable.ml
+++ b/src/variable.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Stdlib
+open Types
open Solver
let cst =
diff --git a/src/variable.mli b/src/variable.mli
index facb1ce919a4507b8f9f7e323109cb69ee33d294..3eacfedbfe35d821d2c28b17b864c81ccc146b45 100644
--- a/src/variable.mli
+++ b/src/variable.mli
@@ -19,6 +19,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
+open Types
open Solver
val cst: Solver.t -> string -> Cl.t