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

Version 1.1 release

Browse source
This commit is contained in:
Guillaume Bury 2015-06-26 14:51:23 +02:00
parent e7140d6897
commit 393d521478
3 changed files with 16 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
_tags
View file

@ -5,9 +5,10 @@
<solver/*.cmx>: for-pack(Msat)
# enable stronger inlining everywhere
<util/{vec,hashcons,hstring,iheap}.cmx>: inline(15)
<sat/**/*.cmx>: inline(10)
<smt/**/*.cmx>: inline(10)
<util/{vec,hashcons,hstring,iheap}.cmx>: inline(100)
<solver/*.cmx>: inline(1000)
<sat/**/*.cmx>: inline(100)
<smt/**/*.cmx>: inline(100)
# more warnings
<**/*.ml>: warn_K, warn_Y, warn_X

2
opam
View file

@ -1,6 +1,6 @@
opam-version: "1.2"
license: "Apache"
version: "1.0"
version: "1.1"
author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"]
maintainer: ["guillaume.bury@gmail.com" "simon.cruanes@inria.fr"]
build: [

11
solver/solver_types.ml
View file

@ -15,6 +15,10 @@ open Printf
module type S = Solver_types_intf.S
(* Solver types for McSat Solving *)
(* ************************************************************************ *)
module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
type formula = E.Formula.t and type term = E.Term.t) = struct
@ -308,6 +312,13 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
end
(* Solver types for pure SAT Solving *)
(* ************************************************************************ *)
module SatMake (L : Log_intf.S)(E : Formula_intf.S)
(Th : Theory_intf.S with type formula = E.t ) = struct