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

Bundled both smt and mcsat in sat_solve; updated the tests in Makefile

Browse source
This commit is contained in:
Guillaume Bury 2014-12-16 21:32:18 +01:00
parent ca70f87973
commit aacae0883b
4 changed files with 77 additions and 252 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
Makefile
View file

@ -5,7 +5,7 @@ COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display
FLAGS= FLAGS=
DIRS=-Is solver,sat,smt,util,util/smtlib DIRS=-Is solver,sat,smt,util,util/smtlib
DOC=msat.docdir/index.html DOC=msat.docdir/index.html
TEST=sat_solve.native mcsat_solve.native TEST=sat_solve.native
NAME=msat NAME=msat
@ -23,7 +23,8 @@ build-test:
$(COMP) $(FLAGS) $(DIRS) $(TEST) $(COMP) $(FLAGS) $(DIRS) $(TEST)
test: build-test test: build-test
./tests/run @./tests/run smt
@./tests/run mcsat
bench: build-test bench: build-test
cd bench && $(MAKE) cd bench && $(MAKE)

10
tests/run
View file

@ -7,16 +7,16 @@ solvertest () {
for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'` for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'`
do do
echo -ne "\r\033[KTesting $f..." echo -ne "\r\033[KTesting $f..."
"$SOLVER" -check -time 30s -size 1G $f | grep $2 > /dev/null 2> /dev/null "$SOLVER" -s $3 -check -time 30s -size 1G $f | grep $2 > /dev/null 2> /dev/null
RET=$? RET=$?
if [ $RET -ne 0 ]; if [ $RET -ne 0 ];
then then
echo -e "\r\033[K\e[31m[KO]\e[0m $f" echo -e "\r\033[K\e[31m[KO]\e[0m $3 - $f"
exit 2 exit 2
fi fi
done done
echo -e "\r\033[K\e[32m[OK]\e[0m $2" echo -e "\r\033[K\e[32m[OK]\e[0m $2-$3"
} }
solvertest "$CURDIR/sat/" "Sat" solvertest "$CURDIR/sat/" "Sat" $1
solvertest "$CURDIR/unsat/" "Unsat" solvertest "$CURDIR/unsat/" "Unsat" $1

222
util/mcsat_solve.ml
View file

@ -1,222 +0,0 @@
module F = Expr
module T = Cnf.S
module S = Mcsat.Make(struct end)
exception Incorrect_model
exception Out_of_time
exception Out_of_space
(* IO wrappers *)
(* Types for input/output languages *)
type sat_input =
| Auto
| Dimacs
| Smtlib
type sat_output =
| Standard (* Only output problem status *)
| Dot
let input = ref Auto
let output = ref Standard
let input_list = [
"auto", Auto;
"dimacs", Dimacs;
"smtlib", Smtlib;
]
let output_list = [
"dot", Dot;
]
let error_msg opt arg l =
Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
Format.flush_str_formatter ()
let set_io opt arg flag l =
try
flag := List.assoc arg l
with Not_found ->
invalid_arg (error_msg opt arg l)
let set_input s = set_io "Input" s input input_list
let set_output s = set_io "Output" s output output_list
(* Input Parsing *)
let rec rev_flat_map f acc = function
| [] -> acc
| a :: r -> rev_flat_map f (List.rev_append (f a) acc) r
let format_of_filename s =
let last n =
try String.sub s (String.length s - n) n
with Invalid_argument _ -> ""
in
if last 4 = ".cnf" then
Dimacs
else if last 5 = ".smt2" then
Smtlib
else (* Default choice *)
Dimacs
let parse_with_input file = function
| Auto -> assert false
| Dimacs -> List.rev_map (List.rev_map F.mk_prop) (Parsedimacs.parse file)
| Smtlib -> rev_flat_map T.make_cnf [] (Smtlib.parse file)
let parse_input file =
parse_with_input file (match !input with
| Auto -> format_of_filename file
| f -> f)
(* Printing wrappers *)
let std = Format.std_formatter
let print format = match !output with
| Standard -> Format.fprintf std "%( fmt %)@." format
| Dot -> Format.fprintf std "/* %( fmt %) */@." format
let print_proof proof = match !output with
| Standard -> ()
| Dot -> S.print_proof std proof
let rec print_cl fmt = function
| [] -> Format.fprintf fmt "[]"
| [a] -> F.print fmt a
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" F.print a print_cl r
let print_lcl l =
List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l
let print_lclause l =
List.iter (fun c -> Format.fprintf std "%a@\n" S.print_clause c) l
let print_cnf cnf = match !output with
| Standard -> print_lcl cnf
| Dot -> ()
let print_unsat_core u = match !output with
| Standard -> print_lclause u
| Dot -> ()
(* Arguments parsing *)
let file = ref ""
let p_cnf = ref false
let p_check = ref false
let p_proof_print = ref false
let p_unsat_core = ref false
let time_limit = ref 300.
let size_limit = ref 1000_000_000.
let int_arg r arg =
let l = String.length arg in
let multiplier m =
let arg1 = String.sub arg 0 (l-1) in
r := m *. (float_of_string arg1)
in
if l = 0 then raise (Arg.Bad "bad numeric argument")
else
try
match arg.[l-1] with
| 'k' -> multiplier 1e3
| 'M' -> multiplier 1e6
| 'G' -> multiplier 1e9
| 'T' -> multiplier 1e12
| 's' -> multiplier 1.
| 'm' -> multiplier 60.
| 'h' -> multiplier 3600.
| 'd' -> multiplier 86400.
| '0'..'9' -> r := float_of_string arg
| _ -> raise (Arg.Bad "bad numeric argument")
with Failure "float_of_string" -> raise (Arg.Bad "bad numeric argument")
let setup_gc_stat () =
at_exit (fun () ->
Gc.print_stat stdout;
)
let input_file = fun s -> file := s
let usage = "Usage : main [options] <file>"
let argspec = Arg.align [
"-bt", Arg.Unit (fun () -> Printexc.record_backtrace true),
" Enable stack traces";
"-cnf", Arg.Set p_cnf,
" Prints the cnf used.";
"-check", Arg.Set p_check,
" Build, check and print the proof (if output is set), if unsat";
"-gc", Arg.Unit setup_gc_stat,
" Outputs statistics about the GC";
"-i", Arg.String set_input,
" Sets the input format (default auto)";
"-o", Arg.String set_output,
" Sets the output format (default none)";
"-size", Arg.String (int_arg size_limit),
"<s>[kMGT] Sets the size limit for the sat solver";
"-time", Arg.String (int_arg time_limit),
"<t>[smhd] Sets the time limit for the sat solver";
"-u", Arg.Set p_unsat_core,
" Prints the unsat-core explanation of the unsat proof (if used with -check)";
"-v", Arg.Int (fun i -> Log.set_debug i),
"<lvl> Sets the debug verbose level";
]
(* Limits alarm *)
let check () =
let t = Sys.time () in
let heap_size = (Gc.quick_stat ()).Gc.heap_words in
let s = float heap_size *. float Sys.word_size /. 8. in
if t > !time_limit then
raise Out_of_time
else if s > !size_limit then
raise Out_of_space
(* Entry file parsing *)
let get_cnf () = parse_input !file
let main () =
(* Administrative duties *)
Arg.parse argspec input_file usage;
if !file = "" then begin
Arg.usage argspec usage;
exit 2
end;
let al = Gc.create_alarm check in
(* Interesting stuff happening *)
let cnf = get_cnf () in
if !p_cnf then
print_cnf cnf;
S.assume cnf;
let res = S.solve () in
Gc.delete_alarm al;
match res with
| S.Sat ->
print "Sat";
if !p_check then
if not (List.for_all (List.exists S.eval) cnf) then
raise Incorrect_model
| S.Unsat ->
print "Unsat";
if !p_check then begin
let p = S.get_proof () in
print_proof p;
if !p_unsat_core then
print_unsat_core (S.unsat_core p)
end
let () =
try
main ()
with
| Incorrect_model ->
print "Internal error : incorrect *sat* model";
exit 4
| Out_of_time ->
print "Time limit exceeded";
exit 2
| Out_of_space ->
print "Size limit exceeded";
exit 3

92
util/sat_solve.ml
View file

@ -1,7 +1,8 @@
module F = Expr module F = Expr
module T = Cnf.S module T = Cnf.S
module S = Smt.Make(struct end) module Smt = Smt.Make(struct end)
module Mcsat = Mcsat.Make(struct end)
exception Incorrect_model exception Incorrect_model
exception Out_of_time exception Out_of_time
@ -18,8 +19,13 @@ type sat_output =
| Standard (* Only output problem status *) | Standard (* Only output problem status *)
| Dot | Dot
type solver =
| Smt
| Mcsat
let input = ref Auto let input = ref Auto
let output = ref Standard let output = ref Standard
let solver = ref Smt
let input_list = [ let input_list = [
"auto", Auto; "auto", Auto;
@ -29,20 +35,25 @@ let input_list = [
let output_list = [ let output_list = [
"dot", Dot; "dot", Dot;
] ]
let solver_list = [
"smt", Smt;
"mcsat", Mcsat;
]
let error_msg opt arg l = let error_msg opt arg l =
Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a" Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l; arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
Format.flush_str_formatter () Format.flush_str_formatter ()
let set_io opt arg flag l = let set_flag opt arg flag l =
try try
flag := List.assoc arg l flag := List.assoc arg l
with Not_found -> with Not_found ->
invalid_arg (error_msg opt arg l) invalid_arg (error_msg opt arg l)
let set_input s = set_io "Input" s input input_list let set_input s = set_flag "Input" s input input_list
let set_output s = set_io "Output" s output output_list let set_output s = set_flag "Output" s output output_list
let set_solver s = set_flag "Solver" s solver solver_list
(* Input Parsing *) (* Input Parsing *)
let rec rev_flat_map f acc = function let rec rev_flat_map f acc = function
@ -80,7 +91,11 @@ let print format = match !output with
let print_proof proof = match !output with let print_proof proof = match !output with
| Standard -> () | Standard -> ()
| Dot -> S.print_proof std proof | Dot -> Smt.print_proof std proof
let print_mcproof proof = match !output with
| Standard -> ()
| Dot -> Mcsat.print_proof std proof
let rec print_cl fmt = function let rec print_cl fmt = function
| [] -> Format.fprintf fmt "[]" | [] -> Format.fprintf fmt "[]"
@ -91,7 +106,10 @@ let print_lcl l =
List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l
let print_lclause l = let print_lclause l =
List.iter (fun c -> Format.fprintf std "%a@\n" S.print_clause c) l List.iter (fun c -> Format.fprintf std "%a@\n" Smt.print_clause c) l
let print_mclause l =
List.iter (fun c -> Format.fprintf std "%a@\n" Mcsat.print_clause c) l
let print_cnf cnf = match !output with let print_cnf cnf = match !output with
| Standard -> print_lcl cnf | Standard -> print_lcl cnf
@ -101,6 +119,10 @@ let print_unsat_core u = match !output with
| Standard -> print_lclause u | Standard -> print_lclause u
| Dot -> () | Dot -> ()
let print_mc_unsat_core u = match !output with
| Standard -> print_mclause u
| Dot -> ()
(* Arguments parsing *) (* Arguments parsing *)
let file = ref "" let file = ref ""
let p_cnf = ref false let p_cnf = ref false
@ -153,6 +175,8 @@ let argspec = Arg.align [
" Sets the input format (default auto)"; " Sets the input format (default auto)";
"-o", Arg.String set_output, "-o", Arg.String set_output,
" Sets the output format (default none)"; " Sets the output format (default none)";
"-s", Arg.String set_solver,
" Sets the solver to use (default smt)";
"-size", Arg.String (int_arg size_limit), "-size", Arg.String (int_arg size_limit),
"<s>[kMGT] Sets the size limit for the sat solver"; "<s>[kMGT] Sets the size limit for the sat solver";
"-time", Arg.String (int_arg time_limit), "-time", Arg.String (int_arg time_limit),
@ -189,23 +213,45 @@ let main () =
let cnf = get_cnf () in let cnf = get_cnf () in
if !p_cnf then if !p_cnf then
print_cnf cnf; print_cnf cnf;
S.assume cnf; match !solver with
let res = S.solve () in | Smt ->
Gc.delete_alarm al; Smt.assume cnf;
match res with let res = Smt.solve () in
| S.Sat -> Gc.delete_alarm al;
print "Sat"; begin match res with
if !p_check then | Smt.Sat ->
if not (List.for_all (List.exists S.eval) cnf) then print "Sat";
raise Incorrect_model if !p_check then
| S.Unsat -> if not (List.for_all (List.exists Smt.eval) cnf) then
print "Unsat"; raise Incorrect_model
if !p_check then begin | Smt.Unsat ->
let p = S.get_proof () in print "Unsat";
print_proof p; if !p_check then begin
if !p_unsat_core then let p = Smt.get_proof () in
print_unsat_core (S.unsat_core p) print_proof p;
end if !p_unsat_core then
print_unsat_core (Smt.unsat_core p)
end
end
| Mcsat ->
Mcsat.assume cnf;
let res = Mcsat.solve () in
Gc.delete_alarm al;
begin match res with
| Mcsat.Sat ->
print "Sat";
if !p_check then
if not (List.for_all (List.exists Mcsat.eval) cnf) then
raise Incorrect_model
| Mcsat.Unsat ->
print "Unsat";
if !p_check then begin
let p = Mcsat.get_proof () in
print_mcproof p;
if !p_unsat_core then
print_mc_unsat_core (Mcsat.unsat_core p)
end
end
let () = let () =
try try