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

Better integration of smt into sat-solve (sic)

Browse source
This commit is contained in:
Guillaume Bury 2014-11-15 00:59:09 +01:00
parent 37d8ddbd7b
commit e92740e75e
10 changed files with 32 additions and 357 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
sat/res.ml
View file

@ -49,13 +49,10 @@ module Make(St : Solver_types.S) = struct
let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c)
(* Printing functions *)
let print_atom fmt a =
Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "¬ ") St.(a.var.vid + 1)
let rec print_cl fmt = function
| [] -> Format.fprintf fmt "[]"
| [a] -> print_atom fmt a
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" print_atom a print_cl r
| [a] -> St.print_atom fmt a
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.print_atom a print_cl r
(* Compute resolution of 2 clauses *)
let resolve l =
@ -322,7 +319,7 @@ module Make(St : Solver_types.S) = struct
Format.fprintf fmt "%s -> %s;@\n" id_c id_d
let print_res_atom id fmt a =
Format.fprintf fmt "%s [label=\"%a\"]" id print_atom a
Format.fprintf fmt "%s [label=\"%a\"]" id St.print_atom a
let print_res_node concl p1 p2 fmt atom =
let id = new_id () in

36
smt/smt.ml
View file

@ -10,33 +10,35 @@ module Fsmt = struct
type var = string
type t =
| Fresh of int
| Prop of int
| Equal of var * var
| Distinct of var * var
let dummy = Fresh 0
let dummy = Prop 0
let max_fresh = ref 0
let fresh () =
incr max_fresh;
Fresh !max_fresh
Prop (2 * !max_fresh + 1)
let mk_prop i =
if i <> 0 && i < max_int / 2 then Prop (2 * i)
else raise Invalid_var
let mk_var i =
if i <> "" then
i
else
raise Invalid_var
if i <> "" then i
else raise Invalid_var
let mk_eq i j = Equal (mk_var i, mk_var j)
let mk_neq i j = Distinct (mk_var i, mk_var j)
let neg = function
| Fresh i -> Fresh (-i)
| Prop i -> Prop (-i)
| Equal (a, b) -> Distinct (a, b)
| Distinct (a, b) -> Equal (a, b)
let norm = function
| Fresh i -> Fresh (abs i), i < 0
| Prop i -> Prop (abs i), i < 0
| Equal (a, b) -> Equal (min a b, max a b), false
| Distinct (a, b) -> Equal (min a b, max a b), true
@ -50,9 +52,9 @@ module Fsmt = struct
let add_label _ _ = ()
let print fmt = function
| Fresh i -> Format.fprintf fmt "%sv%d" (if i < 0 then "¬ " else "") (abs i)
| Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") (abs i)
| Equal (a, b) -> Format.fprintf fmt "%s = %s" a b
| Distinct (a, b) -> Format.fprintf fmt "%s <> %s" a b
| Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b
end
@ -89,7 +91,7 @@ module Tsmt = struct
try
for i = s.start to s.start + s.length - 1 do
match s.get i with
| Fsmt.Fresh _ -> ()
| Fsmt.Prop _ -> ()
| Fsmt.Equal (i, j) as f ->
env := { !env with seen = f :: !env.seen };
env := { !env with uf = U.union !env.uf i j }
@ -118,16 +120,6 @@ module Make(Dummy:sig end) = struct
| Unsat
let _i = ref 0
let make_eq = Fsmt.mk_eq
let make_neq = Fsmt.mk_neq
let neg = Fsmt.neg
let hash = Fsmt.hash
let equal = Fsmt.equal
let compare = Fsmt.compare
let solve () =
try
SmtSolver.solve ();

18
smt/smt.mli
View file

@ -6,6 +6,7 @@ Copyright 2014 Simon Cruanes
module Fsmt : sig
include Formula_intf.S
val mk_prop : int -> t
val mk_eq : string -> string -> t
val mk_neq : string -> string -> t
end
@ -27,23 +28,6 @@ module Make(Dummy: sig end) : sig
type res = Sat | Unsat
(** Type of results returned by the solve function. *)
val make_eq : string -> string -> atom
(** Returns the literal corresponding to equality of the given variables
@raise Invalid_var if given [0] as argument.*)
val make_neq : string -> string -> atom
(** Returns the literal corresponding to disequality of the given variables
@raise Invalid_var if given [0] as argument.*)
val neg : atom -> atom
(** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *)
val hash : atom -> int
val equal : atom -> atom -> bool
val compare : atom -> atom -> int
(** Usual hash and comparison functions. For now, directly uses
[Pervasives] and [Hashtbl] builtins. *)
val solve : unit -> res
(** Returns the satisfiability status of the current set of assumptions. *)

0
tests/smt/test-007.smt2 → tests/sat/test-007.smt2
View file

0
tests/smt/test-008.smt2 → tests/unsat/test-008.smt2
View file

18
util/sat_solve.ml
View file

@ -1,5 +1,7 @@
module S = Sat.Make(struct end)
module F = Smt.Fsmt
module T = Smt.Tseitin
module S = Smt.Make(struct end)
exception Out_of_time
exception Out_of_space
@ -60,8 +62,8 @@ let format_of_filename s =
let parse_with_input file = function
| Auto -> assert false
| Dimacs -> List.rev_map (List.rev_map S.make) (Parsedimacs.parse file)
| Smtlib -> rev_flat_map Sat.Tseitin.make_cnf [] (Satlib.parse file)
| 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
@ -79,15 +81,17 @@ let print_proof proof = match !output with
| Standard -> ()
| Dot -> S.print_proof std proof
(*
let print_assign () = match !output with
| Standard -> S.iter_atoms (fun a ->
Format.fprintf std "%a -> %s,@ " S.print_atom a (if S.eval a then "T" else "F"))
| Dot -> ()
*)
let rec print_cl fmt = function
| [] -> Format.fprintf fmt "[]"
| [a] -> Sat.Fsat.print fmt a
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" Sat.Fsat.print a print_cl r
| [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
@ -189,9 +193,11 @@ let main () =
S.assume cnf;
match S.solve () with
| S.Sat ->
print "Sat";
print "Sat"
(*
if !p_assign then
print_assign ()
*)
| S.Unsat ->
print "Unsat";
if !p_proof_check then begin

198
util/smt_solve.ml
View file

@ -1,198 +0,0 @@
module S = Smt.Make(struct end)
exception Out_of_time
exception Out_of_space
(* IO wrappers *)
(* Types for input/output languages *)
type sat_input =
| Auto
| Smtlib
type sat_output =
| Standard (* Only output problem status *)
| Dot
let input = ref Auto
let output = ref Standard
let input_list = [
"auto", Auto;
"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 5 = ".smt2" then
Smtlib
else (* Default choice *)
Smtlib
let parse_with_input file = function
| Auto -> assert false
| Smtlib -> rev_flat_map Smt.Tseitin.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] -> Smt.Fsmt.print fmt a
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" Smt.Fsmt.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
(* Arguments parsing *)
let file = ref ""
let p_cnf = ref false
let p_proof_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_proof_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;
ignore(Gc.create_alarm check);
(* Interesting stuff happening *)
let cnf = get_cnf () in
if !p_cnf then
print_lcl cnf;
S.assume cnf;
match S.solve () with
| S.Sat ->
print "Sat";
| S.Unsat ->
print "Unsat";
if !p_proof_check then begin
let p = S.get_proof () in
print_proof p;
if !p_unsat_core then
print_lclause (S.unsat_core p)
end
let () =
try
main ()
with
| Out_of_time ->
print "Time limit exceeded";
exit 2
| Out_of_space ->
print "Size limit exceeded";
exit 3

103
util/smtlib/satlib.ml
View file

@ -1,103 +0,0 @@
(* Copyright 2014 INRIA **)
open Smtlib_syntax
module F = Sat.Fsat
module T = Sat.Tseitin
exception Bad_arity of string
exception Unknown_command
exception Incomplete_translation
(* Environment *)
let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;;
Hashtbl.add env "true" T.f_true;;
Hashtbl.add env "false" T.f_false;;
let get_var =
fun s ->
try
Hashtbl.find env s
with Not_found ->
let f = T.make_atom (F.fresh ()) in
Hashtbl.add env s f;
f
(* Term translation *)
let translate_const = function
| SpecConstsDec(_, s)
| SpecConstNum(_, s)
| SpecConstString(_, s)
| SpecConstsHex(_, s)
| SpecConstsBinary(_, s) -> get_var s
let translate_symbol = function
| Symbol(_, s)
| SymbolWithOr(_, s) -> s
let translate_id = function
| IdSymbol(_, s) -> translate_symbol s
| IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation
let translate_sort = function
| SortIdentifier(_, id) ->
let s = translate_id id in
if s <> "Bool" then raise Incomplete_translation
| _ -> raise Incomplete_translation
let translate_qualid = function
| QualIdentifierId(_, id) -> translate_id id
| QualIdentifierAs(_, id, s) -> raise Incomplete_translation
let left_assoc s f = function
| x :: r -> List.fold_left f x r
| _ -> raise (Bad_arity s)
let right_assoc s f = function
| x :: r -> List.fold_right f r x
| _ -> raise (Bad_arity s)
let rec translate_term = function
| TermSpecConst(_, const) -> translate_const const
| TermQualIdentifier(_, id) -> get_var (translate_qualid id)
| TermQualIdTerm(_, f, (_, l)) ->
begin match (translate_qualid f), (List.map translate_term l) with
(* CORE theory translation - '=', 'distinct','ite' not yet implemented *)
| "not", [e] -> T.make_not e
| "not", _ -> raise (Bad_arity "not")
| "and", l -> T.make_and l
| "or", l -> T.make_or l
| "xor" as s, l -> left_assoc s T.make_xor l
| "=>" as s, l -> right_assoc s T.make_imply l
| _ -> raise Unknown_command
end
| _ -> raise Incomplete_translation
(* Command Translation *)
let translate_command = function
| CommandDeclareFun(_, s, (_, []), ret) ->
ignore (translate_sort ret);
ignore (get_var (translate_symbol s));
None
| CommandAssert(_, t) ->
Some (translate_term t)
| _ -> None
let rec translate_command_list acc = function
| [] -> acc
| c :: r ->
begin match translate_command c with
| None -> translate_command_list acc r
| Some t -> translate_command_list (t :: acc) r
end
let translate = function
| Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l)
| None -> []
let parse file =
let f = open_in file in
let lexbuf = Lexing.from_channel f in
let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in
close_in f;
translate commands

3
util/smtlib/satlib.mli
View file

@ -1,3 +0,0 @@
(* Copyright 2014 INRIA *)
val parse : string -> Sat.Tseitin.t list

4
util/smtlib/smtlib.ml
View file

@ -14,7 +14,7 @@ let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;;
Hashtbl.add env "true" T.f_true;;
Hashtbl.add env "false" T.f_false;;
let get_var s =
let get_atom s =
try
Hashtbl.find env s
with Not_found ->
@ -75,7 +75,7 @@ let rec translate_term = function
| _ -> raise Unknown_command
end
end
| _ -> raise Incomplete_translation
| e -> (get_atom (translate_atom e))
(* Command Translation *)
let translate_command = function