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

Made sat atom type private

Browse source
This commit is contained in:
Guillaume Bury 2015-02-18 16:32:18 +01:00
parent e584e0979d
commit d58c5c0756
5 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
_tags
View file

@ -1,4 +1,4 @@
<util/*.cmx>: package(unix) <util/*.cmx>: for-pack(Msat), package(unix)
<util/*.native>: package(unix) <util/*.native>: package(unix)
<smt/*.cmx>: for-pack(Msat), package(zarith) <smt/*.cmx>: for-pack(Msat), package(zarith)
<sat/*.cmx>: for-pack(Msat) <sat/*.cmx>: for-pack(Msat)

3
msat.mlpack
View file

@ -1,3 +1,6 @@
# Debug
Log
# Solver Modules # Solver Modules
Log_intf Log_intf
Formula_intf Formula_intf

2
msat.odocl
View file

@ -1,3 +1,5 @@
util/Log
solver/Log_intf solver/Log_intf
solver/Formula_intf solver/Formula_intf
solver/Expr_intf solver/Expr_intf

2
sat/sat.ml
View file

@ -7,8 +7,6 @@ Copyright 2014 Simon Cruanes
module Fsat = struct module Fsat = struct
exception Dummy of int exception Dummy of int
(* Until the constant true_ and false_ are not needed anymore,
* wa can't simply use sigend integers to represent literals *)
type t = int type t = int
let max_lit = max_int let max_lit = max_int

2
sat/sat.mli
View file

@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module Fsat : Formula_intf.S with type t = int module Fsat : Formula_intf.S with type t = private int
module Tseitin : Tseitin.S with type atom = Fsat.t module Tseitin : Tseitin.S with type atom = Fsat.t