Commit f0b2e7c5 authored by Erwan Jahier's avatar Erwan Jahier

Add missing files to the commit 8d69d9ed

which aims at Adding bddrand, simple front-end to the lutin Random
toss machinary (the log msg was wrong).
parent cedfd53a
Pipeline #17408 passed with stages
in 8 minutes and 15 seconds
(* OASIS_START *)
(* DO NOT EDIT (digest: 92cce301c349ffd5db07434c1bfe26ec) *)
(* DO NOT EDIT (digest: b02258ab91ae2df27b3896c979a325ed) *)
Authors of Lutin:
Authors of lutin:
* Erwan Jahier
* Pascal Raymond
* Bertrand Jeannnet (polka)
* Yvan Roux
Current maintainers of Lutin:
Current maintainers of lutin:
* erwan.jahier@univ-grenoble-alpes.fr
......
OASISFormat: 0.4
Name: lutin
Version: 2.64
Version: 2.65
Authors: Erwan Jahier, Pascal Raymond, Bertrand Jeannnet (polka), Yvan Roux
Maintainers: erwan.jahier@univ-grenoble-alpes.fr
License: CeCILL
......
(* Time-stamp: <modified the 15/11/2018 (at 16:10) by Erwan Jahier> *)
(**********************************************************************************
The dimacs parser comes from:
http://www.enseignement.polytechnique.fr/informatique/INF551/TD/TD1/aux/DIMACS.ml *)
open String
let read_from_file filename =
let lines = ref "" in
let chan = open_in filename in
try
while true; do
let line = input_line chan in
if (length line>0)&&(not ((line.[0]) = 'c')) then
lines := (!lines)^"\n"^line
done; ""
with End_of_file ->
close_in chan;
!lines
let latexescaped = function
| '%' | '{' | '}' as c -> "\\"^Char.escaped c
| c -> Char.escaped c
let rec list_from_string s list_so_far n =
if (n>=length s) then List.rev list_so_far
else
match s.[n] with
| ' ' | '\n' | '\t' -> list_from_string s list_so_far (n+1)
| '-' -> list_from_string s ("-"::list_so_far) (n+1)
| _ ->
let rec word_from_string s word_so_far n =
if (n>=length s) then List.rev (word_so_far::list_so_far)
else
begin
match s.[n] with
| ' '| '\n' | '\t' -> list_from_string s (word_so_far::list_so_far) n
| c -> word_from_string s (word_so_far^(latexescaped c)) (n+1)
end
in
word_from_string s "" n
let rec print_list = function
| [] -> ()
| s::l -> print_string (s^" "); print_list l
module PairLit = struct
type t = bool*int
let negation (b,s) = (not b,s)
end
let rec parse_cnf cnf_so_far: string list -> PairLit.t list list = function
| [] -> List.rev cnf_so_far
| "0"::l -> parse_cnf ((* []:: *)cnf_so_far) l
| l -> let rec parse_clause clause_so_far ispos = function
| [] -> parse_cnf ((List.rev clause_so_far)::cnf_so_far) []
| "0"::l -> parse_cnf ((List.rev clause_so_far)::cnf_so_far) l
| "-"::l -> parse_clause clause_so_far false l
| s::l -> parse_clause ((ispos,int_of_string s)::clause_so_far) true l
in parse_clause [] true l
let parse_cnf_file l =
let rec aux nbvar = function
| "p"::"cnf"::nbvar::_nbclauses::l -> parse_cnf [] l, int_of_string nbvar
| _ -> assert false
in
aux 0 l
type t = (bool * int) list list * int
let (parse: string -> t) = fun x -> try
list_from_string (read_from_file x) [] 0
|> parse_cnf_file
with e -> failwith (Printf.sprintf "Is file %s a valid dimacs file?" x)
(**********************************************************************************)
(* a printer *)
let (print: t -> string) = fun (pll,_) ->
let p_to_str (b,n) = if b then string_of_int n else "not("^string_of_int n^")" in
let pl_to_str pl =
List.fold_left
(fun acc p -> Printf.sprintf "%s or %s" acc (p_to_str p))
(p_to_str (List.hd pl))
(List.tl pl)
in
List.fold_left
(fun acc pl -> Printf.sprintf "%s and \n%s" acc (pl_to_str pl))
(pl_to_str (List.hd pll))
(List.tl pll)
(**********************************************************************************)
(* Translate dimacs data type into Exp.formula *)
let make_var i = Var.make "" ((string_of_int i)) Type.BoolT Var.Output
(* Returns the and of all the variables using the dimacs var number *)
let (gen_vars : int -> Exp.var list) = fun size ->
let rec aux acc i =
if i > size then acc else aux ((make_var i)::acc) (i+1)
in
aux [] 1
let (to_formula : t -> Exp.var list * Exp.formula) = fun (pll, size) ->
let p_to_bdd (b,n) =
let v = Exp.Bvar (make_var n) in
if b then v else Exp.Not(v)
in
let pl_to_bdd pl =
List.fold_left
(fun acc p -> Exp.Or (acc, (p_to_bdd p)))
(p_to_bdd (List.hd pl))
(List.tl pl)
in
let f =
List.fold_left
(fun acc pl -> Exp.And (acc, (pl_to_bdd pl)))
(pl_to_bdd (List.hd pll))
(List.tl pll)
in
let vl = gen_vars size in
vl, f
(* Time-stamp: <modified the 15/11/2018 (at 15:59) by Erwan Jahier> *)
type t = (bool * int) list list * int
val parse: string -> t
val print : t -> string
(* returns the formula corresponding to the dimacs sat pb, plus the
list of all the variables of the sat problem *)
val to_formula : t -> Exp.var list * Exp.formula
let str="2.64"
let sha="8d69d9ed"
let str="2.65"
let sha="cedfd53a"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment