From 0050fdae3c24cf2e5994db63c48d3662ec488cc9 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 13 Mar 2015 14:31:46 +0100 Subject: [PATCH] Better clause names --- smt/mcsat.ml | 4 +--- solver/mcsolver.ml | 16 ++++++++-------- solver/mcsolver.mli | 2 +- solver/mcsolver_types.ml | 8 ++++++-- solver/mcsolver_types_intf.ml | 3 ++- 5 files changed, 18 insertions(+), 15 deletions(-) diff --git a/smt/mcsat.ml b/smt/mcsat.ml index de5dc594..b79680d1 100644 --- a/smt/mcsat.ml +++ b/smt/mcsat.ml @@ -123,7 +123,6 @@ module Make(Dummy:sig end) = struct | Sat | Unsat - let _i = ref 0 let solve () = try SmtSolver.solve (); @@ -131,9 +130,8 @@ module Make(Dummy:sig end) = struct with SmtSolver.Unsat -> Unsat let assume l = - incr _i; try - SmtSolver.assume l !_i + SmtSolver.assume l with SmtSolver.Unsat -> () let get_proof () = diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index da3f94f6..b29be7d6 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -622,7 +622,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) let atoms = List.rev_map (fun x -> new_atom x) l in Iheap.grow_to_by_double env.order (St.nb_vars ()); List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms; - add_clause "lemma" atoms (Lemma lemma) + add_clause (fresh_tname ()) atoms (Lemma lemma) let slice_propagate f lvl = let a = add_atom f in @@ -655,7 +655,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) let l = List.rev_map new_atom l in Iheap.grow_to_by_double env.order (St.nb_vars ()); List.iter (fun a -> insert_var_order (Either.mk_right a.var)) l; - let c = St.make_clause (St.fresh_name ()) l (List.length l) true (Lemma p) in + let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in Some c and propagate () = @@ -819,9 +819,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) let check_vec vec = for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done - let add_clauses cnf ~cnumber = + let add_clauses cnf = let aux cl = - add_clause "hyp" cl (History []); + add_clause (fresh_hname ()) cl (History []); match propagate () with | None -> () | Some confl -> report_unsat confl in @@ -850,7 +850,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) with | Sat -> () - let init_solver cnf ~cnumber = + let init_solver cnf = let nbv = St.nb_vars () in let nbc = env.nb_init_clauses + List.length cnf in Iheap.grow_to_by_double env.order nbv; @@ -863,11 +863,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) (fun v -> L.debug 50 " -- %a" St.pp_semantic_var v) (fun a -> L.debug 50 " -- %a" St.pp_atom a.tag.pa) ); - add_clauses cnf ~cnumber + add_clauses cnf - let assume cnf ~cnumber = + let assume cnf = let cnf = List.rev_map (List.rev_map St.add_atom) cnf in - init_solver cnf ~cnumber + init_solver cnf let eval lit = let var, negated = make_boolean_var lit in diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index bda45808..82040a90 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -24,7 +24,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) @return () if the current set of clauses is satisfiable @raise Unsat if a toplevel conflict is found *) - val assume : E.Formula.t list list -> cnumber:int -> unit + val assume : E.Formula.t list list -> unit (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. @raise Unsat if a conflict is detect when adding the clauses *) diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml index cf169ac5..ec436745 100644 --- a/solver/mcsolver_types.ml +++ b/solver/mcsolver_types.ml @@ -185,9 +185,13 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with let cpt = ref 0 in fun () -> incr cpt; "L" ^ (string_of_int !cpt) - let fresh_dname = + let fresh_hname = let cpt = ref 0 in - fun () -> incr cpt; "D" ^ (string_of_int !cpt) + fun () -> incr cpt; "H" ^ (string_of_int !cpt) + + let fresh_tname = + let cpt = ref 0 in + fun () -> incr cpt; "T" ^ (string_of_int !cpt) let fresh_name = let cpt = ref 0 in diff --git a/solver/mcsolver_types_intf.ml b/solver/mcsolver_types_intf.ml index 969ef2e9..f22b8256 100644 --- a/solver/mcsolver_types_intf.ml +++ b/solver/mcsolver_types_intf.ml @@ -91,7 +91,8 @@ module type S = sig val fresh_name : unit -> string val fresh_lname : unit -> string - val fresh_dname : unit -> string + val fresh_tname : unit -> string + val fresh_hname : unit -> string (** Fresh names for clauses *) val proof_debug : proof -> string * (atom list) * (semantic var list) * (string option)