simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-29 21:04:53 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge branch 'master' into push_pop

Browse source
This commit is contained in:
Guillaume Bury 2015-11-27 14:53:41 +01:00
commit 3f6de07440
23 changed files with 666 additions and 658 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
README.md
View file

@ -1,7 +1,7 @@
# MSAT # MSAT
MSAT is an OCaml library that features a modular SAT-solver and some MSAT is an OCaml library that features a modular SAT-solver and some
extensions (including SMT). This is *work in progress*. extensions (including SMT). This is **work in progress**.
It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero). It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
@ -65,7 +65,9 @@ For the development version, use:
opam pin add msat https://github.com/Gbury/mSAT.git opam pin add msat https://github.com/Gbury/mSAT.git
### Manual installation You will need ocamlfind. The command is: ### Manual installation
You will need ocamlfind. The command is:
make install make install

7
solver/internal.ml
View file

@ -4,8 +4,11 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module Make (L : Log_intf.S)(St : Solver_types.S) module Make
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) = struct (L : Log_intf.S)
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
= struct
module Proof = Res.Make(L)(St) module Proof = Res.Make(L)(St)

7
solver/internal.mli
View file

@ -4,8 +4,11 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module Make (L : Log_intf.S)(St : Solver_types.S) module Make
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) : sig (L : Log_intf.S)
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
: sig
(** Functor to create a solver parametrised by the atomic formulas and a theory. *) (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
(** {2 Solving facilities} *) (** {2 Solving facilities} *)