From ca70f879735fcf9bc6f7c80ecbdc27a0e0fb940c Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 16 Dec 2014 17:30:14 +0100 Subject: [PATCH] Mcsat now works --- Makefile | 2 +- msat.mlpack | 9 +- smt/.merlin | 2 + smt/cc.ml | 8 ++ smt/cc.mli | 3 + smt/cnf.ml | 7 ++ smt/cnf.mli | 7 ++ smt/expr.ml | 73 +++++++++++++ smt/mcsat.ml | 145 +++++++++++++++++++++++++ smt/smt.ml | 56 +--------- smt/smt.mli | 11 +- solver/mcsolver.ml | 97 +++++++++++------ solver/mcsolver.mli | 2 - solver/mcsolver_types.ml | 36 ++++--- solver/mcsolver_types.mli | 3 +- solver/plugin_intf.ml | 2 +- tests/sat/test-010.smt2 | 2 + tests/unsat/test-011.smt2 | 2 + util/mcsat_solve.ml | 222 ++++++++++++++++++++++++++++++++++++++ util/sat_solve.ml | 4 +- util/smtlib/smtlib.ml | 4 +- util/smtlib/smtlib.mli | 2 +- 22 files changed, 570 insertions(+), 129 deletions(-) create mode 100644 smt/cnf.ml create mode 100644 smt/cnf.mli create mode 100644 smt/expr.ml create mode 100644 smt/mcsat.ml create mode 100644 tests/sat/test-010.smt2 create mode 100644 tests/unsat/test-011.smt2 create mode 100644 util/mcsat_solve.ml diff --git a/Makefile b/Makefile index 5edfdad9..d3e24e49 100644 --- a/Makefile +++ b/Makefile @@ -5,7 +5,7 @@ COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display FLAGS= DIRS=-Is solver,sat,smt,util,util/smtlib DOC=msat.docdir/index.html -TEST=sat_solve.native bench_stats.native +TEST=sat_solve.native mcsat_solve.native NAME=msat diff --git a/msat.mlpack b/msat.mlpack index b62d96df..ea9ab8da 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -3,8 +3,6 @@ Formula_intf Solver Solver_types Theory_intf - -# Mcsat Solver modules Expr_intf Mcsolver Mcsolver_types @@ -16,10 +14,11 @@ Mcproof Tseitin Tseitin_intf -# Sat modules +# Sat/Smt modules +Expr +Cnf Sat - -# Smt Modules +Mcsat Cc Sig Smt diff --git a/smt/.merlin b/smt/.merlin index 95182585..022353bf 100644 --- a/smt/.merlin +++ b/smt/.merlin @@ -1,8 +1,10 @@ S ./ S ../sat/ S ../util/ +S ../solver/ B ../_build/ B ../_build/sat/ B ../_build/smt/ B ../_build/util/ +B ../_build/solver/ diff --git a/smt/cc.ml b/smt/cc.ml index 3bc8569b..d71621c1 100644 --- a/smt/cc.ml +++ b/smt/cc.ml @@ -23,6 +23,8 @@ module Make(T : Sig.OrderedType) = struct size = M.empty; } + let repr t a = U.find t.repr a + let map_find m v default = try M.find v m with Not_found -> default let find_parent v m = map_find m v v @@ -87,5 +89,11 @@ module Make(T : Sig.OrderedType) = struct with U.Unsat (a, b) -> raise (Unsat (a, b, expl t a b)) + let are_neq t a b = + try + ignore (U.union t.repr a b); + false + with U.Unsat _ -> + true end diff --git a/smt/cc.mli b/smt/cc.mli index ef14aebc..2f92550d 100644 --- a/smt/cc.mli +++ b/smt/cc.mli @@ -12,4 +12,7 @@ module Make(T : Sig.OrderedType) : sig val empty : t val add_eq : t -> T.t -> T.t -> t val add_neq : t -> T.t -> T.t -> t + + val repr : t -> T.t -> T.t + val are_neq : t -> T.t -> T.t -> bool end diff --git a/smt/cnf.ml b/smt/cnf.ml new file mode 100644 index 00000000..f778231a --- /dev/null +++ b/smt/cnf.ml @@ -0,0 +1,7 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module S = Tseitin.Make(Expr) diff --git a/smt/cnf.mli b/smt/cnf.mli new file mode 100644 index 00000000..b0eae539 --- /dev/null +++ b/smt/cnf.mli @@ -0,0 +1,7 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module S : Tseitin.S with type atom = Expr.Formula.t diff --git a/smt/expr.ml b/smt/expr.ml new file mode 100644 index 00000000..b61c62bd --- /dev/null +++ b/smt/expr.ml @@ -0,0 +1,73 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +exception Invalid_var + +type var = string +type formula = + | Prop of int + | Equal of var * var + | Distinct of var * var +type t = formula + +let dummy = Prop 0 + +let max_fresh = ref 0 +let fresh () = + incr 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 + +let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j)) +let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j)) + +let neg = function + | Prop i -> Prop (-i) + | Equal (a, b) -> Distinct (a, b) + | Distinct (a, b) -> Equal (a, b) + +let norm = function + | Prop i -> Prop (abs i), i < 0 + | Equal (a, b) -> Equal (a, b), false + | Distinct (a, b) -> Equal (a, b), true + + (* Only used after normalisation, so usual functions should work *) +let hash = Hashtbl.hash +let equal = (=) +let compare = Pervasives.compare + +let s = Hstring.make "" +let label _ = s +let add_label _ _ = () + +let print fmt = function + | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2) + | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b + | Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b + +module Term = struct + type t = var + let hash = Hashtbl.hash + let equal = (=) + let compare = Pervasives.compare + let print fmt t = Format.fprintf fmt "%s" t +end + +module Formula = struct + type t = formula + let hash = Hashtbl.hash + let equal = (=) + let compare = Pervasives.compare + let print = print +end + diff --git a/smt/mcsat.ml b/smt/mcsat.ml new file mode 100644 index 00000000..f8f4c921 --- /dev/null +++ b/smt/mcsat.ml @@ -0,0 +1,145 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Fsmt = Expr + +module Tsmt = struct + + module M = Map.Make(Fsmt.Term) + module CC = Cc.Make(String) + + (* Type definitions *) + type term = Fsmt.var + type formula = Fsmt.t + + type proof = unit + + type assumption = + | Lit of formula + | Assign of term * term + + type slice = { + start : int; + length : int; + get : int -> assumption * int; + push : formula list -> proof -> unit; + } + + type level = { + cc : CC.t; + assign : (term * int) M.t; + } + + type res = + | Sat of level + | Unsat of formula list * proof + + type eval_res = + | Valued of bool * int + | Unknown + + (* Functions *) + let dummy = { cc = CC.empty; assign = M.empty; } + + let env = ref dummy + + let current_level () = !env + + let to_clause (a, b, l) = + Log.debug 10 "Expl : %s; %s" a b; + List.iter (fun s -> Log.debug 10 " |- %s" s) l; + let rec aux acc = function + | [] | [_] -> acc + | x :: ((y :: _) as r) -> + aux (Fsmt.mk_eq x y :: acc) r + in + (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) + + let assume s = + try + for i = s.start to s.start + s.length - 1 do + match s.get i with + | (Assign (x, v)), lvl -> + env := { !env with assign = M.add x (v, lvl) !env.assign } + | Lit f, _ -> + Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print f); + match f with + | Fsmt.Prop _ -> () + | Fsmt.Equal (i, j) -> + env := { !env with cc = CC.add_eq !env.cc i j } + | Fsmt.Distinct (i, j) -> + env := { !env with cc = CC.add_neq !env.cc i j } + | _ -> assert false + done; + Sat (current_level ()) + with CC.Unsat x -> + Log.debug 8 "Making explanation clause..."; + Unsat (to_clause x, ()) + + let backtrack l = env := l + + let assign t = CC.repr !env.cc t + + let iter_assignable f = function + | Fsmt.Prop _ -> () + | Fsmt.Equal(a, b) + | Fsmt.Distinct (a, b) -> f a; f b + + let eval = function + | Fsmt.Prop _ -> Unknown + | Fsmt.Equal (a, b) -> + begin try + let a', lvl_a = M.find a !env.assign in + let b', lvl_b = M.find b !env.assign in + Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b) + with Not_found -> Unknown end + | Fsmt.Distinct (a, b) -> + begin try + let a', lvl_a = M.find a !env.assign in + let b', lvl_b = M.find b !env.assign in + Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b) + with Not_found -> Unknown end + +end + +module Make(Dummy:sig end) = struct + module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt) + + type atom = Fsmt.t + type clause = SmtSolver.St.clause + type proof = SmtSolver.Proof.proof + + type res = + | Sat + | Unsat + + let _i = ref 0 + let solve () = + try + SmtSolver.solve (); + Sat + with SmtSolver.Unsat -> Unsat + + let assume l = + incr _i; + try + SmtSolver.assume l !_i + with SmtSolver.Unsat -> () + + let get_proof () = + SmtSolver.Proof.learn (SmtSolver.history ()); + match SmtSolver.unsat_conflict () with + | None -> assert false + | Some c -> SmtSolver.Proof.prove_unsat c + + let eval = SmtSolver.eval + + let unsat_core = SmtSolver.Proof.unsat_core + + let print_atom = Fsmt.print + let print_clause = SmtSolver.St.print_clause + let print_proof = SmtSolver.Proof.print_dot +end diff --git a/smt/smt.ml b/smt/smt.ml index 526a1dd1..bfa8c00d 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -4,61 +4,7 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Fsmt = struct - - exception Invalid_var - - type var = string - type t = - | Prop of int - | Equal of var * var - | Distinct of var * var - - let dummy = Prop 0 - - let max_fresh = ref 0 - let fresh () = - incr 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 - - let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j)) - let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j)) - - let neg = function - | Prop i -> Prop (-i) - | Equal (a, b) -> Distinct (a, b) - | Distinct (a, b) -> Equal (a, b) - - let norm = function - | Prop i -> Prop (abs i), i < 0 - | Equal (a, b) -> Equal (a, b), false - | Distinct (a, b) -> Equal (a, b), true - - (* Only used after normalisation, so usual functions should work *) - let hash = Hashtbl.hash - let equal = (=) - let compare = Pervasives.compare - - let s = Hstring.make "" - let label _ = s - let add_label _ _ = () - - let print fmt = function - | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2) - | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b - | Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b - -end - -module Tseitin = Tseitin.Make(Fsmt) +module Fsmt = Expr module Tsmt = struct diff --git a/smt/smt.mli b/smt/smt.mli index c2df81c3..a089b513 100644 --- a/smt/smt.mli +++ b/smt/smt.mli @@ -4,19 +4,10 @@ Copyright 2014 Guillaume Bury 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 - -module Tseitin : Tseitin.S with type atom = Fsmt.t - module Make(Dummy: sig end) : sig (** Fonctor to make a pure SAT Solver module with built-in literals. *) - type atom = Fsmt.t + type atom = Expr.Formula.t (** Type for atoms, i.e boolean literals. *) type clause diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index d40acb11..8707c4d8 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -178,12 +178,12 @@ module Make (E : Expr_intf.S) get_elt_level (St.get_var i) < 0 (* Var/clause activity *) - let rec insert_var_order e = Either.destruct e + let insert_var_order e = Either.destruct e (fun v -> Iheap.insert f_weight env.order v.vid) (fun v -> Iheap.insert f_weight env.order v.vid; - Th.iter_assignable (fun t -> - insert_var_order (Either.mk_left (St.add_term t))) v.tag.pa.lit) + Th.iter_assignable (fun t -> Iheap.insert f_weight env.order (St.add_term t).vid) v.tag.pa.lit + ) let var_decay_activity () = env.var_inc <- env.var_inc *. env.var_decay @@ -191,7 +191,7 @@ module Make (E : Expr_intf.S) let clause_decay_activity () = env.clause_inc <- env.clause_inc *. env.clause_decay - let var_bump_activity v = + let var_bump_activity_aux v = v.weight <- v.weight +. env.var_inc; if v.weight > 1e100 then begin for i = 0 to (St.nb_vars ()) - 1 do @@ -202,6 +202,10 @@ module Make (E : Expr_intf.S) if Iheap.in_heap env.order v.vid then Iheap.decrease f_weight env.order v.vid + let var_bump_activity v = + var_bump_activity_aux v; + Th.iter_assignable (fun t -> var_bump_activity_aux (St.add_term t)) v.tag.pa.lit + let clause_bump_activity c = c.activity <- c.activity +. env.clause_inc; if c.activity > 1e20 then begin @@ -259,16 +263,21 @@ module Make (E : Expr_intf.S) if decision_level () > lvl then begin env.qhead <- Vec.get env.trail_lim lvl; env.tatoms_qhead <- env.qhead; - for c = Vec.size env.trail - 1 downto env.qhead do + for c = env.qhead to Vec.size env.trail - 1 do Either.destruct (Vec.get env.trail c) (fun a -> ()) (fun a -> - a.is_true <- false; - a.neg.is_true <- false; - a.var.level <- -1; - a.var.tag.reason <- Bcp None; - a.var.tag.vpremise <- History []; - insert_var_order (Either.mk_right a.var)) + if a.var.level <= lvl then begin + Vec.set env.trail env.qhead (Either.mk_right a); + env.qhead <- env.qhead + 1 + end else begin + a.is_true <- false; + a.neg.is_true <- false; + a.var.level <- -1; + a.var.tag.reason <- Bcp None; + a.var.tag.vpremise <- History []; + insert_var_order (Either.mk_right a.var) + end) done; Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); @@ -286,9 +295,6 @@ module Make (E : Expr_intf.S) let enqueue_bool a lvl reason = assert (not a.is_true && not a.neg.is_true && a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0); - assert (lvl = decision_level ()); - (* keep the reason for proof/unsat-core *) - (*let reason = if lvl = 0 then None else reason in*) a.is_true <- true; a.var.level <- lvl; a.var.tag.reason <- reason; @@ -299,7 +305,8 @@ module Make (E : Expr_intf.S) v.tag.assigned <- Some value; v.level <- lvl; Log.debug 5 "Enqueue: %a" St.pp_semantic_var v; - Vec.push env.trail (Either.mk_left v) + Vec.push env.trail (Either.mk_left v); + Log.debug 15 "Done." (* conflict analysis *) let max_lvl_atoms l = @@ -308,42 +315,65 @@ module Make (E : Expr_intf.S) else if a.var.level > max_lvl then (a.var.level, [a]) else (max_lvl, acc)) (0, []) l + let backtrack_lvl is_uip = function + | [] -> 0 + | a :: r when not is_uip -> a.var.level - 1 + | a :: r -> + let rec aux = function + | [] -> 0 + | b :: r when b.var.level <> a.var.level -> b.var.level + | _ :: r -> aux r + in + aux r + let analyze c_clause = let tr_ind = ref (Vec.size env.trail) in - let blevel = ref 0 in let is_uip = ref false in let c = ref (Proof.to_list c_clause) in - let history = ref [] in - + let history = ref [c_clause] in + clause_bump_activity c_clause; let is_semantic a = match a.var.tag.reason with | Semantic _ -> true | _ -> false in - try while true do let l, atoms = max_lvl_atoms !c in + Log.debug 15 "Current conflict clause :"; + List.iter (fun a -> Log.debug 15 " |- %a" St.pp_atom a) !c; match atoms with | [] | _ :: [] -> - blevel := -1; + Log.debug 15 "Found UIP clause"; + is_uip := true; raise Exit | _ when List.for_all is_semantic atoms -> - blevel := l - 1; + Log.debug 15 "Found Semantic backtrack clause"; raise Exit | _ -> decr tr_ind; + Log.debug 20 "Looking at trail element %d" !tr_ind; Either.destruct (Vec.get env.trail !tr_ind) - (fun v -> ()) + (fun v -> Log.debug 15 "%a" St.pp_semantic_var v) (fun a -> match a.var.tag.reason with | Bcp (Some d) -> + Log.debug 15 "Propagation : %a" St.pp_atom a; + Log.debug 15 " |- %a" St.pp_clause d; let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in begin match tmp with - | [b] when b == a.neg -> c := !c - | _ -> () + | [] -> Log.debug 15 "No lit to resolve over." + | [b] when b == a.var.tag.pa -> + clause_bump_activity d; + var_bump_activity a.var; + history := d :: !history; + c := res + | _ -> assert false end - | _ -> ()) + | _ -> Log.debug 15 "Decision : %a" St.pp_atom a) done; assert false with Exit -> - !blevel, !c, !history, !is_uip + let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in + let blevel = backtrack_lvl !is_uip learnt in + blevel, learnt, !history, !is_uip + (* while !cond do if !c.learnt then clause_bump_activity !c; @@ -439,7 +469,7 @@ module Make (E : Expr_intf.S) let partition atoms init0 = let rec partition_aux trues unassigned falses init = function | [] -> trues @ unassigned @ falses, init - | a::r -> + | a :: r -> if a.is_true then if a.var.level = 0 then raise Trivial else (a::trues) @ unassigned @ falses @ r, init @@ -574,8 +604,8 @@ module Make (E : Expr_intf.S) (* Propagation (boolean and theory *) let _th_cnumber = ref 0 let slice_get i = Either.destruct (Vec.get env.trail i) - (function {tag={term; assigned = Some v}} -> Th.Assign (term, v) | _ -> assert false) - (fun a -> Th.Lit a.lit) + (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false) + (fun a -> Th.Lit a.lit, a.var.level) let slice_push l lemma = decr _th_cnumber; @@ -612,9 +642,9 @@ module Make (E : Expr_intf.S) Either.destruct (Vec.get env.trail env.qhead) (fun a -> ()) (fun a -> - env.qhead <- env.qhead + 1; incr num_props; - propagate_atom a res) + propagate_atom a res); + env.qhead <- env.qhead + 1 done; env.propagations <- env.propagations + !num_props; env.simpDB_props <- env.simpDB_props - !num_props; @@ -797,9 +827,12 @@ module Make (E : Expr_intf.S) Vec.grow_to_by_double env.clauses nbc; Vec.grow_to_by_double env.learnts nbc; env.nb_init_clauses <- nbc; + St.iter_vars (fun e -> Either.destruct e + (fun v -> Log.debug 50 " -- %a" St.pp_semantic_var v) + (fun a -> Log.debug 50 " -- %a" St.pp_atom a.tag.pa) + ); add_clauses cnf ~cnumber - let assume cnf ~cnumber = let cnf = List.rev_map (List.rev_map St.add_atom) cnf in init_solver cnf ~cnumber diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index e13584d7..ab7d43f9 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -20,12 +20,10 @@ module Make (E : Expr_intf.S) module St : Mcsolver_types.S with type formula = E.Formula.t - (* module Proof : Res.S with type atom = St.atom and type clause = St.clause and type lemma = Th.proof - *) val solve : unit -> unit (** Try and solves the current set of assumptions. diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml index f6013de4..092ed047 100644 --- a/solver/mcsolver_types.ml +++ b/solver/mcsolver_types.ml @@ -15,7 +15,8 @@ open Printf module type S = Mcsolver_types_intf.S -module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct +module Make (E : Expr_intf.S)(Th : Plugin_intf.S with + type formula = E.Formula.t and type term = E.Term.t) = struct (* Types declarations *) @@ -115,6 +116,22 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct let cpt_mk_var = ref 0 + let make_semantic_var t = + try MT.find t !t_map + with Not_found -> + let res = { + vid = !cpt_mk_var; + weight = 1.; + level = -1; + tag = { + term = t; + assigned = None; }; + } in + incr cpt_mk_var; + t_map := MT.add t res !t_map; + Vec.push vars (Either.mk_left res); + res + let make_boolean_var = fun lit -> let lit, negated = E.norm lit in @@ -149,24 +166,9 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct f_map := MF.add lit var !f_map; incr cpt_mk_var; Vec.push vars (Either.mk_right var); + Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit; var, negated - let make_semantic_var t = - try MT.find t !t_map - with Not_found -> - let res = { - vid = !cpt_mk_var; - weight = 0.; - level = -1; - tag = { - term = t; - assigned = None; }; - } in - incr cpt_mk_var; - t_map := MT.add t res !t_map; - Vec.push vars (Either.mk_left res); - res - let add_term t = make_semantic_var t let add_atom lit = diff --git a/solver/mcsolver_types.mli b/solver/mcsolver_types.mli index 981053df..cca0ebe5 100644 --- a/solver/mcsolver_types.mli +++ b/solver/mcsolver_types.mli @@ -13,6 +13,7 @@ module type S = Mcsolver_types_intf.S -module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S) +module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S with + type term = E.Term.t and type formula = E.Formula.t) -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof (** Functor to instantiate the types of clauses for the Solver. *) diff --git a/solver/plugin_intf.ml b/solver/plugin_intf.ml index 65683755..8a4a9c36 100644 --- a/solver/plugin_intf.ml +++ b/solver/plugin_intf.ml @@ -31,7 +31,7 @@ module type S = sig type slice = { start : int; length : int; - get : int -> assumption; + get : int -> assumption * int; push : formula list -> proof -> unit; } (** The type for a slice of litterals to assume/propagate in the theory. diff --git a/tests/sat/test-010.smt2 b/tests/sat/test-010.smt2 new file mode 100644 index 00000000..dbec8ea3 --- /dev/null +++ b/tests/sat/test-010.smt2 @@ -0,0 +1,2 @@ +(assert (and (= a b) (= b c) (or (not (= a c)) (= a d)))) +(check-sat) diff --git a/tests/unsat/test-011.smt2 b/tests/unsat/test-011.smt2 new file mode 100644 index 00000000..9087bf10 --- /dev/null +++ b/tests/unsat/test-011.smt2 @@ -0,0 +1,2 @@ +(assert (and (= a b) (= b c) (= c d) (or (not (= a c)) (not (= a a))))) +(check-sat) diff --git a/util/mcsat_solve.ml b/util/mcsat_solve.ml new file mode 100644 index 00000000..1ccce7b7 --- /dev/null +++ b/util/mcsat_solve.ml @@ -0,0 +1,222 @@ + +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] " +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), + "[kMGT] Sets the size limit for the sat solver"; + "-time", Arg.String (int_arg time_limit), + "[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), + " 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 diff --git a/util/sat_solve.ml b/util/sat_solve.ml index 3b9dee35..73e7b541 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -1,6 +1,6 @@ -module F = Smt.Fsmt -module T = Smt.Tseitin +module F = Expr +module T = Cnf.S module S = Smt.Make(struct end) exception Incorrect_model diff --git a/util/smtlib/smtlib.ml b/util/smtlib/smtlib.ml index 2777fb40..b27ce41f 100644 --- a/util/smtlib/smtlib.ml +++ b/util/smtlib/smtlib.ml @@ -2,8 +2,8 @@ open Smtlib_syntax -module F = Smt.Fsmt -module T = Smt.Tseitin +module F = Expr +module T = Cnf.S exception Bad_arity of string exception Unknown_command diff --git a/util/smtlib/smtlib.mli b/util/smtlib/smtlib.mli index 14d06003..1120b12c 100644 --- a/util/smtlib/smtlib.mli +++ b/util/smtlib/smtlib.mli @@ -1,3 +1,3 @@ (* Copyright 2014 INRIA *) -val parse : string -> Smt.Tseitin.t list +val parse : string -> Cnf.S.t list