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

Added dummy arguments to some functors

Browse source 
Some functors lacked a dummy argument, and thus
could introduce some problems if duplicated (because
they would share the same internal state).
This commit is contained in:
Guillaume Bury 2016-02-29 10:54:17 +01:00
parent a6a44445c7
commit b6effe691c
11 changed files with 20 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
README.md
View file

@ -23,7 +23,7 @@ as shown in the following code :
```ocaml
(* Module initialization *)
module F = Msat.Sat.Tseitin
module Sat = Msat.Sat.Make(Msat.Log)
module Sat = Msat.Sat.Make()
(* We create here two distinct atoms *)
let a = Sat.new_atom () (* A 'new_atom' is always distinct from any other atom *)

8
_tags
View file

@ -6,10 +6,10 @@
<backend/*.cmx>: for-pack(Msat)
# enable stronger inlining everywhere
#<util/{vec,hashcons,hstring,iheap}.cmx>: inline(100)
#<solver/*.cmx>: inline(50)
#<sat/**/*.cmx>: inline(100)
#<smt/**/*.cmx>: inline(100)
<util/{vec,hashcons,hstring,iheap}.cmx>: inline(100)
<solver/*.cmx>: inline(50)
<sat/**/*.cmx>: inline(100)
<smt/**/*.cmx>: inline(100)
<util/log.cmx>: inline(30)
# more warnings

2
sat/sat.ml
View file

@ -66,7 +66,7 @@ module Tseitin = Tseitin.Make(Fsat)
module Make(Dummy : sig end) = struct
module Tsat = Solver.DummyTheory(Fsat)
include Solver.Make(Fsat)(Tsat)
include Solver.Make(Fsat)(Tsat)()
let print_atom = Fsat.print
let print_clause = St.print_clause

2
smt/mcsat.ml
View file

@ -111,7 +111,7 @@ end
module Make(Dummy:sig end) = struct
module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)
module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)()
module Proof = SmtSolver.Proof

2
smt/smt.ml
View file

@ -61,7 +61,7 @@ end
module Make(Dummy:sig end) = struct
include Solver.Make(Fsmt)(Tsmt)
include Solver.Make(Fsmt)(Tsmt)()
module Dot = Dot.Make(Proof)(struct
let clause_name c = St.(c.name)
let print_atom = St.print_atom

1
solver/internal.ml
View file

@ -7,6 +7,7 @@ Copyright 2014 Simon Cruanes
module Make
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
(Dummy: sig end)
= struct
module Proof = Res.Make(St)

1
solver/internal.mli
View file

@ -7,6 +7,7 @@ Copyright 2014 Simon Cruanes
module Make
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
(Dummy: sig end)
: sig
(** Functor to create a solver parametrised by the atomic formulas and a theory. *)

5
solver/mcsolver.ml
View file

@ -5,11 +5,12 @@ Copyright 2014 Simon Cruanes
*)
module Make (E : Expr_intf.S)
(Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) = struct
(Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof)
(Dummy: sig end) = struct
module St = Solver_types.McMake(E)
module M = Internal.Make(St)(Th)
module M = Internal.Make(St)(Th)()
include St

3
solver/mcsolver.mli
View file

@ -5,7 +5,8 @@ Copyright 2014 Simon Cruanes
*)
module Make (E : Expr_intf.S)
(Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) : sig
(Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof)
(Dummy: sig end) : sig
(** Functor to create a solver parametrised by the atomic formulas and a theory. *)
exception Unsat

5
solver/solver.ml
View file

@ -99,13 +99,14 @@ end
module Make (E : Formula_intf.S)
(Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct
(Th : Theory_intf.S with type formula = E.t and type proof = E.proof)
(Dummy: sig end) = struct
module P = Plugin(E)(Th)
module St = Solver_types.SatMake(E)
module S = Internal.Make(St)(P)
module S = Internal.Make(St)(P)()
module Proof = S.Proof

3
solver/solver.mli
View file

@ -18,7 +18,8 @@ module DummyTheory(F : Formula_intf.S with type proof = unit) :
Theory_intf.S with type formula = F.t and type proof = unit
module Make (F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t and type proof = F.proof) :
(Th : Theory_intf.S with type formula = F.t and type proof = F.proof)
(Dummy: sig end) :
S with type St.formula = F.t
and type St.proof = F.proof
(** Functor to create a SMT Solver parametrised by the atomic