Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
verimag
synchrone
lutin
Commits
8d69d9ed
Commit
8d69d9ed
authored
Dec 20, 2018
by
Erwan Jahier
Browse files
Some opam fix
parent
104415c4
Changes
11
Hide whitespace changes
Inline
Side-by-side
_oasis
View file @
8d69d9ed
OASISFormat: 0.4
Name: Lutin
Version: 2.6
1
Version: 2.6
3
Authors: Erwan Jahier, Pascal Raymond, Bertrand Jeannnet (polka), Yvan Roux
Maintainers: erwan.jahier@univ-grenoble-alpes.fr
License: CeCILL
...
...
@@ -45,6 +45,17 @@ Library lutin
InternalModules: Auto2Lucky,AutoGen,Bddd,CheckEnv,CheckType,CkIdentInfo,CkTypeEff,CoAlgExp,CoIdent,CoTraceExp,Constraint,Draw,Exp,ExpEval,Expand,ExprUtil,FGen,Fair_bddd,Formula_to_bdd,GenOcamlGlue,Glue,Gne,Guard,Lexeme,LoopWeights,Luc2alice,Luc2c,LucFGen,Lucky,LutErrors,LutExe,LutLexer,LutParser,LutPredef,LutProg,LutVersion,MainArg,Ne,Parsers,Poly_draw,Polyhedron,Prevar,Prog,Reactive,Rif,Sol_nb,Solver,Store,Syntaxe,SyntaxeDump,Thickness,Type,Util,Utils,Value,Var,Verbose,Version
DllLib: libgmp.so dllcamlidl.so
Library bddrand
XMETADescription: A simple front-end to the lutin Random toss machinary
Path: lutin/src
Modules: BddRandom,Dimacs
BuildDepends: camlp4,lutin-utils,ezdl,gbddml,bigarray,polka,camlidl,lutils
FindlibParent: lutin
Install:true
CompiledObject: native
XMETAEnable: true
DllLib: libgmp.so dllcamlidl.so
#Library lut4c
# XMETADescription: Calling Lutin from C XXX NOT WORKING
...
...
_tags
View file @
8d69d9ed
# OASIS_START
# DO NOT EDIT (digest:
b8b37f2e72fed2e3e0f22b0faad0c518
)
# DO NOT EDIT (digest:
71d84d7cf0a80c1b7d8a7d1353354192
)
# Ignore VCS directories, you can use the same kind of rule outside
# OASIS_START/STOP if you want to exclude directories that contains
# useless stuff for the build process
...
...
@@ -81,6 +81,9 @@ true: annot, bin_annot
"polka/poly_caml.c": package(num)
"polka/polka_caml.c": package(gmp)
"polka/polka_caml.c": package(num)
# Library bddrand
"lutin/src/bddrand.cmxs": use_bddrand
"lutin/src/bddrand.cmxa": oasis_library_bddrand_dlllib
# Library lutin
"lutin/src/lutin.cmxs": use_lutin
"lutin/src/lutin.cmxa": oasis_library_lutin_dlllib
...
...
lutin/src/bddRandom.ml
0 → 100644
View file @
8d69d9ed
(* Time-stamp: <modified the 20/11/2018 (at 10:05) by Erwan Jahier> *)
(** todo : Parse constraints given in Lustre/Lutin like syntax *)
let
(
contraints
:
string
->
(
string
*
bool
)
list
)
=
fun
f
->
assert
false
let
(
contraints_file
:
string
->
(
string
*
bool
)
list
)
=
fun
f
->
assert
false
let
verbose
=
ref
0
let
empty
=
Value
.
OfIdent
.
empty
(* make a comb from a list of var *)
let
(
get_vars_f
:
Exp
.
var
list
->
Exp
.
formula
)
=
fun
vl
->
match
vl
with
|
[]
->
assert
false
|
v1
::
t
->
List
.
fold_left
(
fun
acc
v
->
Exp
.
And
(
Exp
.
Bvar
v
,
acc
))
(
Exp
.
Bvar
v1
)
t
let
(
draw
:
?
number
:
int
->
Exp
.
var
list
->
Exp
.
var
list
->
Exp
.
formula
->
(
string
*
bool
)
list
list
)
=
fun
?
(
number
=
1
)
bvl
nvl
f
->
let
bool_vars_to_gen
:
Exp
.
formula
=
get_vars_f
bvl
in
let
output_var_names
:
Var
.
name
list
list
=
[
List
.
map
Var
.
name
bvl
]
in
let
outs_l
=
Solver
.
solve_formula
empty
empty
!
verbose
"[BddRandom.draw]"
output_var_names
number
(
1
,
0
,
AtMost
0
)
bool_vars_to_gen
nvl
f
in
let
outs_l
=
fst
(
List
.
split
outs_l
)
in
(* throw numerics away for the time being *)
let
outs_l
=
List
.
map
(
fun
outs
->
Value
.
OfIdent
.
fold
(
fun
n
v
acc
->
(
n
,
v
)
::
acc
)
outs
[]
)
outs_l
in
let
outs_l
=
List
.
map
(
fun
outs
->
List
.
map
(
fun
(
n
,
v
)
->
match
v
with
Value
.
B
b
->
n
,
b
|
Value
.
N
n
->
assert
false
)
outs
)
outs_l
in
outs_l
(*********************************************************************************)
let
draw_in_dimacs_file
?
(
number
=
1
)
f
=
let
ll
,
size
=
Dimacs
.
parse
f
in
let
vl
,
f
=
Dimacs
.
to_formula
(
ll
,
size
)
in
let
res
=
draw
~
number
:
number
vl
[]
f
in
res
lutin/src/bddRandom.mli
0 → 100644
View file @
8d69d9ed
(* Time-stamp: <modified the 20/11/2018 (at 09:41) by Erwan Jahier> *)
(** A simple front-end to the lutin Random toss machinary *)
val
verbose
:
int
ref
(** [draw bvl nvl f] draw values according to constraints contained in [f]
- [bvl] contains Bool vars to gen
- [nvl] contains numeric vars to gen
- [bvl] and [nvl] should contains at least all the variables appearing in [f].
- The optional argument [number] controls the number of draw to be done
(1 by default)
*)
val
draw
:
?
number
:
int
->
Exp
.
var
list
->
Exp
.
var
list
->
Exp
.
formula
->
(
string
*
bool
)
list
list
(** [draw_in_dimacs_file dimacs_file]
Do the same job a [draw], by looking for constraints in a dimacs file
*)
val
draw_in_dimacs_file
:
?
number
:
int
->
string
->
(
string
*
bool
)
list
list
(* type num = I of Num.num | F of float *)
(* type value = B of bool | N of num *)
(* val num_draw : t -> (string * value) list *)
(*
#require "rdbg-plugin";;
#require "lutin";;
#require "lutin.bddrand";;
open BddRandom;;
open Dimacs;;
let res_67 = draw_in_dimacs_file "tutorial1.sk_1_1.cnf";;
let res_313 = draw_in_dimacs_file "polynomial.sk_7_25.cnf";;
let res_795 = draw_in_dimacs_file "scenarios_tree_delete3.sb.pl.sk_2_32.cnf";;
let res_1026 = draw_in_dimacs_file "tableBasedAddition.sk_240_1024.cnf"
let res = draw_in_dimacs_file "10.sk_1_46.cnf";;
*)
lutin/src/bddd.ml
View file @
8d69d9ed
...
...
@@ -235,7 +235,7 @@ let (toss_up_one_var_index: Var.env_in -> Var.env -> int -> string -> var_idx ->
match
(
Var
.
default
v
)
with
|
Some
(
Formu
f
)
->
let
bdd
=
Formula_to_bdd
.
f
input
memory
ctx_msg
vl
f
in
(*
print_string ("\n give a default to " ^ (Var.name v) ^ "\n"); flush stdout; *)
(* print_string ("\n give a default to " ^ (Var.name v) ^ "\n"); flush stdout; *)
if
Bdd
.
is_false
bdd
then
Some
((
Var
.
name
v
)
,
B
false
)
else
if
Bdd
.
is_true
bdd
then
Some
((
Var
.
name
v
)
,
B
true
)
else
...
...
lutin/src/bddd.mli
View file @
8d69d9ed
...
...
@@ -10,9 +10,12 @@
(** Bdd Drawer. *)
(** Machinery to perform a draw in a bdd.
*)
(** Machinery to perform a draw in a bdd.
ZZZ : To be used by Solver only !!
*)
val
draw_in_bdd
:
Var
.
env_in
->
Var
.
env
->
int
->
string
->
Exp
.
var
list
->
Bdd
.
t
->
Bdd
.
t
->
Var
.
env
*
Store
.
t'
*
Store
.
p
...
...
@@ -20,6 +23,8 @@ val draw_in_bdd : Var.env_in -> Var.env -> int -> string -> Exp.var list ->
returns a draw of the Boolean variables as well as a range based
and a polyhedron based representation of numeric constraints
(cf. the [Store] module).
Side effect: this is where the solution number tables is filled in.
Raises [No_numeric_solution].
*)
...
...
lutin/src/formula_to_bdd.ml
View file @
8d69d9ed
...
...
@@ -198,7 +198,8 @@ let (index_to_linear_constraint : int -> Constraint.t) =
fun
i
->
try
Util
.
hfind
global_i2lc_tbl
i
with
Not_found
->
Util
.
hfind
i2lc_tbl
i
try
Util
.
hfind
i2lc_tbl
i
with
_
->
failwith
(
Printf
.
sprintf
"Error: can not find index %i in Formula_to_bdd tables
\n
"
i
)
(****************************************************************************)
...
...
lutin/src/formula_to_bdd.mli
View file @
8d69d9ed
...
...
@@ -9,20 +9,21 @@
*)
(**)
(* Encoding formula and expressions into bdds. *)
(*
*
Encoding formula and expressions into bdds. *)
val
f
:
Var
.
env_in
->
Var
.
env
->
string
->
int
->
Exp
.
formula
->
Bdd
.
t
(** [Formula_to_bdd.f input memory ctx_msg verbosity_level
state
f]
(** [Formula_to_bdd.f input memory ctx_msg verbosity_level f]
returns the bdd of [f] where [input] and pre variables have
been repaced by their values. [ctx_msg] is used for printing
source information in case of errors.
ZZZ this function fills in local tables that are used later on during
the random toss (e.g., via index_to_linear_constraint).
Hence bdd should be build by this module.
*)
(**/**)
val
num_to_gne
:
Var
.
env_in
->
Var
.
env
->
string
->
int
->
Exp
.
num
->
Gne
.
t
(** The same as f but for numeric expressions *)
...
...
lutin/src/solver.ml
View file @
8d69d9ed
...
...
@@ -48,18 +48,13 @@ let (set_fair_mode : unit -> unit) =
clear_snt
:=
Fair_bddd
.
clear_snt
;
!
clear_snt
()
(****************************************************************************)
(****************************************************************************)
(* Exported *)
let
(
is_satisfiable_bdd
:
Var
.
env_in
->
Var
.
env
->
int
->
string
->
formula
->
string
->
bool
*
Bdd
.
t
)
=
fun
input
memory
vl
ctx_msg
f
msg
->
let
(
is_satisfiable_bdd
:
Var
.
env_in
->
Var
.
env
->
int
->
string
->
formula
->
string
->
bool
*
Bdd
.
t
)
=
fun
input
memory
vl
ctx_msg
f
msg
->
let
bdd
=
Formula_to_bdd
.
f
input
memory
ctx_msg
vl
f
in
let
is_sat1
=
not
(
Bdd
.
is_false
bdd
)
and
is_sat2
=
...
...
@@ -102,7 +97,6 @@ let (is_satisfiable: Var.env_in -> Var.env -> int -> string -> formula -> string
(****************************************************************************)
(* printing bbd's with dot *)
open
Sol_nb
let
cpt
=
ref
0
...
...
@@ -160,12 +154,17 @@ let (bdd_to_graph: Bdd.t -> (int -> string) -> bool ->
fst
(
bdd_to_graph_acc
[]
[]
only_true
bdd
)
let
(
print_bdd_with_dot
:
Bdd
.
t
->
(
int
->
string
)
->
string
->
bool
->
unit
)
=
fun
bdd
index_to_vn
label
only_true
->
let
index_to_vn
i
=
(
try
Constraint
.
to_string
(
Formula_to_bdd
.
index_to_linear_constraint
i
)
^
"
\"
"
with
_
->
"
\"
"
)
let
(
print_bdd_with_dot
:
Bdd
.
t
->
string
->
bool
->
unit
)
=
fun
bdd
label
only_true
->
let
arcs
=
bdd_to_graph
bdd
(
index_to_vn
)
only_true
in
let
dot_file
=
label
^
".dot"
in
let
p
s_file
=
label
^
".p
s
"
in
let
p
df
=
label
^
".p
df
"
in
let
dot_oc
=
open_out
dot_file
in
let
put
=
output_string
dot_oc
in
let
_
=
...
...
@@ -177,11 +176,12 @@ let (print_bdd_with_dot: Bdd.t -> (int -> string) -> string -> bool -> unit) =
flush
dot_oc
;
close_out
dot_oc
in
(* Calling dot to create the postscript file *)
let
exit_code_dot
=
Sys
.
command
(
"dot -Tps "
^
dot_file
^
" -o "
^
ps_file
)
in
if
(
exit_code_dot
<>
0
)
then
print_string
" Can't call dot; is dot in your path?
\n\n
"
else
()
(* Calling dot to create the postscript file *)
let
cmd
=
(
"dot -Tpdf "
^
dot_file
^
" -o "
^
pdf
)
in
let
exit_code_dot
=
Sys
.
command
cmd
in
if
(
exit_code_dot
<>
0
)
then
Printf
.
printf
"The sys call '%s' failed (exit code %i)
\n\n
"
cmd
exit_code_dot
else
(
Printf
.
printf
"%s generated (with '%s')"
pdf
cmd
)
(****************************************************************************)
...
...
@@ -345,16 +345,14 @@ let (draw : Var.env_in -> Var.env -> int -> string -> Var.name list list ->
)
subst_ll
(****************************************************************************)
(* Exported *)
let
(
solve_formula
:
Var
.
env_in
->
Var
.
env
->
int
->
string
->
Var
.
name
list
list
->
Thickness
.
formula_draw_nb
->
Thickness
.
numeric
->
formula
->
var
list
->
formula
->
(
Var
.
env
*
Var
.
env
)
list
)
=
fun
input
memory
vl
ctx_msg
output_var_names
p
num_thickness
bool_vars_to_gen_f
num_vars_to_gen
f
->
Thickness
.
formula_draw_nb
->
Thickness
.
numeric
->
formula
->
var
list
->
formula
->
(
Var
.
env
*
Var
.
env
)
list
)
=
fun
input
memory
vl
ctx_msg
output_var_names
p
num_thickness
bool_vars_to_gen_f
num_vars_to_gen
f
->
let
bdd
=
(
Formula_to_bdd
.
f
input
memory
ctx_msg
vl
f
)
in
let
_
=
...
...
@@ -399,22 +397,8 @@ let (solve_formula: Var.env_in -> Var.env -> int -> string -> Var.name list list
with
No_numeric_solution
->
if
vl
>=
3
then
(
(
print_bdd_with_dot
bdd
(
fun
i
->
Constraint
.
to_string
(
Formula_to_bdd
.
index_to_linear_constraint
i
)
^
"
\"
"
)
"debug_bdd"
true
);
(
print_bdd_with_dot
bdd
(
fun
i
->
Constraint
.
to_string
(
Formula_to_bdd
.
index_to_linear_constraint
i
)
^
"
\"
"
)
"debug_bdd_all"
false
);
(
print_bdd_with_dot
bdd
"debug_bdd"
true
);
(
print_bdd_with_dot
bdd
"debug_bdd_all"
false
);
);
!
add_snt_entry
bdd
(
Sol_nb
.
zero_sol
,
Sol_nb
.
zero_sol
);
if
vl
>=
2
then
...
...
lutin/src/solver.mli
View file @
8d69d9ed
...
...
@@ -8,10 +8,28 @@
** Main author: jahier@imag.fr
*)
(** Formula solver.
*)
(** Formula solver.
It is a wrapper around Bddd (and Fair_Bddd), which are not supposed
to be used elsewhere.
val
is_satisfiable
:
ZZZ:
- init_snt should be called once before using all the other functions !
- clear_snt can be called or not (it simply clears cache tables)
- is_satisfiable/is_satisfiable_bdd is a lightweight version of
[solve_formula], that do not build solution number table; it is used
to avoid calling [solve_formula] when we do not really need to draw
some solutions
- solve_formula is the main function, that
- solve the formula
- fills in sol nb table
- performs a (Boolean) draw (numerics are drawn latter)
*)
val
is_satisfiable
:
Var
.
env_in
->
Var
.
env
->
int
->
string
->
Exp
.
formula
->
string
->
bool
(** [is_satisfiable input memory verbose_level msg f] suceeds iff the
formula [f], once evaluated w.r.t. [input] and memories, is
...
...
@@ -24,7 +42,7 @@ val is_satisfiable :
val
is_satisfiable_bdd
:
Var
.
env_in
->
Var
.
env
->
int
->
string
->
Exp
.
formula
->
string
->
bool
*
Bdd
.
t
(* idem, but return
ing
the corresponding bdd *)
(* idem, but return
s
the corresponding bdd *)
val
solve_formula
:
Var
.
env_in
->
Var
.
env
->
int
->
string
->
Var
.
name
list
list
->
Thickness
.
formula_draw_nb
->
Thickness
.
numeric
->
...
...
@@ -41,14 +59,19 @@ val solve_formula : Var.env_in -> Var.env -> int -> string ->
performance reasons: [solve_formula] is likely to be called
significantly often with the same arguments so that it is worth
precomputing this encoding before.
*)
val
draw
:
Var
.
env_in
->
Var
.
env
->
int
->
string
->
Var
.
name
list
list
->
Thickness
.
numeric
->
Var
.
name
list
->
Exp
.
var
list
->
Bdd
.
t
->
Bdd
.
t
->
(
Var
.
env
*
Var
.
env
)
list
Side effect: fills in the solution number table
*)
(**/**)
(** The bool flag can be set to true to remove path to the false node.
ZZZ : solve_formula should have been called once to be able to use
this function with this flag set to [true], as it uses the solution
number table. *)
val
print_bdd_with_dot
:
Bdd
.
t
->
string
->
bool
->
unit
val
init_snt
:
(
unit
->
unit
)
ref
val
clear_snt
:
(
unit
->
unit
)
ref
...
...
lutin/src/version.ml
View file @
8d69d9ed
let
str
=
"2.6
1
"
let
sha
=
"
ad57bc8e
"
let
str
=
"2.6
3
"
let
sha
=
"
104415c4
"
erwan
@jahier
mentioned in commit
f0b2e7c5
·
Dec 21, 2018
mentioned in commit
f0b2e7c5
mentioned in commit f0b2e7c5adac4ada61723f33f0f4fd4b9546708d
Toggle commit list
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment