From 3203dadb8d4e2c9352c03e8c3796f2c55e48d1b9 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 6 Feb 2015 15:46:56 +0100 Subject: [PATCH] Replaced clause number by tag in solver.assume --- sat/sat.ml | 9 ++++----- sat/sat.mli | 7 +++++-- smt/smt.ml | 4 +--- solver/solver.ml | 21 ++++++++++----------- solver/solver.mli | 2 +- solver/solver_types.ml | 5 ++++- solver/solver_types_intf.ml | 3 ++- 7 files changed, 27 insertions(+), 24 deletions(-) diff --git a/sat/sat.ml b/sat/sat.ml index 1b4b10da..0f5fbc2a 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -94,12 +94,12 @@ module Make(Dummy : sig end) = struct type clause = SatSolver.St.clause type proof = SatSolver.Proof.proof + let tag_clause cl = SatSolver.St.(cl.tag) + type res = | Sat | Unsat - let _i = ref 0 - let new_atom () = try Fsat.fresh () @@ -126,10 +126,9 @@ module Make(Dummy : sig end) = struct Sat with SatSolver.Unsat -> Unsat - let assume l = - incr _i; + let assume ?tag l = try - SatSolver.assume l !_i + SatSolver.assume ?tag l with SatSolver.Unsat -> () let eval = SatSolver.eval diff --git a/sat/sat.mli b/sat/sat.mli index 15c3acce..0c082326 100644 --- a/sat/sat.mli +++ b/sat/sat.mli @@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Fsat : Formula_intf.S +module Fsat : Formula_intf.S with type t = int module Tseitin : Tseitin.S with type atom = Fsat.t @@ -52,9 +52,12 @@ module Make(Dummy: sig end) : sig val eval : atom -> bool (** Return the current assignement of the literals. *) - val assume : atom list list -> unit + val assume : ?tag:int -> atom list list -> unit (** Add a list of clauses to the set of assumptions. *) + val tag_clause : clause -> int option + (** Returns the tag associated with the clause. *) + val get_proof : unit -> proof (** Returns the resolution proof found, if [solve] returned [Unsat]. *) diff --git a/smt/smt.ml b/smt/smt.ml index 06910031..70a9da5b 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -72,7 +72,6 @@ module Make(Dummy:sig end) = struct | Sat | Unsat - let _i = ref 0 let solve () = try SmtSolver.solve (); @@ -80,9 +79,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/solver.ml b/solver/solver.ml index 4e40a652..296355cd 100644 --- a/solver/solver.ml +++ b/solver/solver.ml @@ -394,10 +394,10 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) else partition_aux [] [] [] [] atoms - let add_clause ~cnumber atoms history = + let add_clause ?tag name atoms history = if env.is_unsat then raise Unsat; - let init_name = string_of_int cnumber in - let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in + let init_name = name in + let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history in Log.debug 10 "Adding clause : %a" St.pp_clause init0; try let atoms, init = partition atoms init0 in @@ -526,7 +526,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) let atoms = List.rev_map (fun x -> add_atom x) l in Iheap.grow_to_by_double env.order (St.nb_vars ()); List.iter (fun a -> insert_var_order a.var) atoms; - add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma) + add_clause "lemma" atoms (Lemma lemma) let current_slice () = Th.({ start = env.tatoms_qhead; @@ -706,15 +706,15 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) with | Sat -> () - let add_clauses cnf ~cnumber = + let add_clauses ?tag cnf = let aux cl = - add_clause ~cnumber cl (History []); + add_clause ?tag "hyp" cl (History []); match propagate () with | None -> () | Some confl -> report_unsat confl in List.iter aux cnf - let init_solver cnf ~cnumber = + let init_solver ?tag 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; @@ -724,12 +724,11 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) Vec.grow_to_by_double env.clauses nbc; Vec.grow_to_by_double env.learnts nbc; env.nb_init_clauses <- nbc; - add_clauses cnf ~cnumber + add_clauses ?tag cnf - - let assume cnf ~cnumber = + let assume ?tag cnf = let cnf = List.rev_map (List.rev_map St.add_atom) cnf in - init_solver cnf ~cnumber + init_solver ?tag cnf let eval lit = let var, negated = make_var lit in diff --git a/solver/solver.mli b/solver/solver.mli index c8f4c287..492d6139 100644 --- a/solver/solver.mli +++ b/solver/solver.mli @@ -31,7 +31,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) @return () if the current set of clauses is satisfiable @raise Unsat if a toplevel conflict is found *) - val assume : F.t list list -> cnumber:int -> unit + val assume : ?tag:int -> F.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/solver_types.ml b/solver/solver_types.ml index 362dc1c2..974ced65 100644 --- a/solver/solver_types.ml +++ b/solver/solver_types.ml @@ -40,6 +40,7 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct and clause = { name : string; + tag : int option; atoms : atom Vec.t ; mutable activity : float; mutable removed : bool; @@ -75,6 +76,7 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct let dummy_clause = { name = ""; + tag = None; atoms = Vec.make_empty dummy_atom; activity = -1.; removed = false; @@ -136,9 +138,10 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct let var, negated = make_var lit in if negated then var.na else var.pa - let make_clause name ali sz_ali is_learnt premise = + let make_clause ?tag name ali sz_ali is_learnt premise = let atoms = Vec.from_list ali sz_ali dummy_atom in { name = name; + tag = tag; atoms = atoms; removed = false; learnt = is_learnt; diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml index 724bc3f3..995df934 100644 --- a/solver/solver_types_intf.ml +++ b/solver/solver_types_intf.ml @@ -39,6 +39,7 @@ module type S = sig and clause = { name : string; + tag : int option; atoms : atom Vec.t; mutable activity : float; mutable removed : bool; @@ -67,7 +68,7 @@ module type S = sig (** Returns the variable linked with the given formula, and wether the atom associated with the formula is [var.pa] or [var.na] *) - val make_clause : string -> atom list -> int -> bool -> premise -> clause + val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *) val nb_vars : unit -> int