From 35ce540684b88682580414196920145dd49d9c87 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 12 Nov 2014 16:24:08 +0100 Subject: [PATCH] Progressing on new theory interface --- sat/sat.ml | 4 +- sat/solver.ml | 121 ++++++++++++++++++++++----------------------- sat/theory_intf.ml | 4 +- sat/tseitin.ml | 5 -- 4 files changed, 64 insertions(+), 70 deletions(-) diff --git a/sat/sat.ml b/sat/sat.ml index d4627a93..32ad035f 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -69,12 +69,12 @@ module Tsat = struct start : int; length : int; get : int -> formula; - push : formula -> unit; + push : formula -> formula list -> proof -> unit; } type res = | Sat of level - | Unsat of formula list + | Unsat of formula list * proof let dummy = () let current_level () = () diff --git a/sat/solver.ml b/sat/solver.ml index 1ca19bd1..f472508f 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -352,29 +352,47 @@ module Make (F : Formula_intf.S) Vec.shrink watched dead_part (* Propagation (boolean and theory *) + let slice_get i = (Vec.get env.trail i).lit + let slice_push lit l lemma = + let atoms = List.rev_map add_atom (lit :: (List.rev_map F.neg l)) in + let c = St.make_clause (St.fresh_name ()) atoms (List.length atoms) true [] in + enqueue (St.add_atom lit) (decision_level ()) (Some c) + let current_slice () = Th.({ start = env.tatoms_qhead; length = (Vec.size env.trail) - env.tatoms_qhead; - get = (function i -> (Vec.get env.trail i).lit); - push = (function lit -> enqueue (St.add_atom lit) (decision_level ()) None); - (* TODO: modify reasons to allow for theory reason *) + get = slice_get; + push = slice_push; }) - let rec theory_propagate () = None + let rec theory_propagate () = + match Th.assume (current_slice ()) with + | Th.Sat _ -> + env.tatoms_qhead <- Vec.size env.trail; + propagate () + | Th.Unsat (l, p) -> + let l = List.rev_map St.add_atom l in + let c = St.make_clause (St.fresh_name ()) l (List.length l) true [] in + Some c and propagate () = - let num_props = ref 0 in - let res = ref None in - (*assert (Queue.is_empty env.tqueue);*) - while env.qhead < Vec.size env.trail do - let a = Vec.get env.trail env.qhead in - env.qhead <- env.qhead + 1; - incr num_props; - propagate_atom a res; - done; - env.propagations <- env.propagations + !num_props; - env.simpDB_props <- env.simpDB_props - !num_props; - !res + if env.qhead = Vec.size env.trail then + None + else begin + let num_props = ref 0 in + let res = ref None in + while env.qhead < Vec.size env.trail do + let a = Vec.get env.trail env.qhead in + env.qhead <- env.qhead + 1; + incr num_props; + propagate_atom a res; + done; + env.propagations <- env.propagations + !num_props; + env.simpDB_props <- env.simpDB_props - !num_props; + match !res with + | None -> theory_propagate () + | _ -> !res + end (* conflict analysis *) let analyze c_clause = @@ -481,25 +499,18 @@ module Make (F : Formula_intf.S) (struct type t = clause let equal = (==) let hash = Hashtbl.hash end) - let report_b_unsat ({atoms=atoms} as confl) = + let report_unsat ({atoms=atoms} as confl) = env.unsat_conflict <- Some confl; env.is_unsat <- true; raise Unsat - let report_t_unsat dep = - env.is_unsat <- true; - raise Unsat - let simplify () = assert (decision_level () = 0); if env.is_unsat then raise Unsat; begin match propagate () with - | Some confl -> report_b_unsat confl - | None -> - match theory_propagate () with - Some dep -> report_t_unsat dep - | None -> () + | Some confl -> report_unsat confl + | None -> () end; if nb_assigns() <> env.simpDB_assigns && env.simpDB_props <= 0 then begin if Vec.size env.learnts > 0 then remove_satisfied env.learnts; @@ -533,8 +544,8 @@ module Make (F : Formula_intf.S) clause_decay_activity () - let theory_analyze dep = 0, [], [], 1 (* + let theory_analyze dep = 0, [], [], 1 let atoms, sz, max_lvl, c_hist = Ex.fold_atoms (fun a (acc, sz, max_lvl, c_hist) -> @@ -603,7 +614,7 @@ module Make (F : Formula_intf.S) let add_boolean_conflict confl = env.conflicts <- env.conflicts + 1; - if decision_level() = 0 then report_b_unsat confl; (* Top-level conflict *) + if decision_level() = 0 then report_unsat confl; (* Top-level conflict *) let blevel, learnt, history, size = analyze confl in cancel_until blevel; record_learnt_clause blevel learnt history size @@ -618,37 +629,27 @@ module Make (F : Formula_intf.S) add_boolean_conflict confl | None -> (* No Conflict *) - match theory_propagate () with - | Some dep -> - incr conflictC; - env.conflicts <- env.conflicts + 1; - if decision_level() = 0 then report_t_unsat dep; (* T-L conflict *) - let blevel, learnt, history, size = theory_analyze dep in - cancel_until blevel; - record_learnt_clause blevel learnt history size + if nb_assigns() = env.nb_init_vars then raise Sat; + if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then + begin + env.progress_estimate <- progress_estimate(); + cancel_until 0; + raise Restart + end; + if decision_level() = 0 then simplify (); - | None -> - if nb_assigns() = env.nb_init_vars then raise Sat; - if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then - begin - env.progress_estimate <- progress_estimate(); - cancel_until 0; - raise Restart - end; - if decision_level() = 0 then simplify (); + if n_of_learnts >= 0 && + Vec.size env.learnts - nb_assigns() >= n_of_learnts then + reduce_db(); - if n_of_learnts >= 0 && - Vec.size env.learnts - nb_assigns() >= n_of_learnts then - reduce_db(); + env.decisions <- env.decisions + 1; - env.decisions <- env.decisions + 1; - - new_decision_level(); - let next = pick_branch_lit () in - let current_level = decision_level () in - assert (next.level < 0); - Log.debug 5 "Deciding on %a" St.pp_atom next.pa; - enqueue next.pa current_level None + new_decision_level(); + let next = pick_branch_lit () in + let current_level = decision_level () in + assert (next.level < 0); + Log.debug 5 "Deciding on %a" St.pp_atom next.pa; + enqueue next.pa current_level None done let check_clause c = @@ -727,7 +728,7 @@ module Make (F : Formula_intf.S) let size = List.length atoms in match atoms with | [] -> - report_b_unsat init0; + report_unsat init0; | a::_::_ -> let name = fresh_name () in @@ -745,13 +746,11 @@ module Make (F : Formula_intf.S) a.var.vpremise <- init; enqueue a 0 None; match propagate () with - None -> () | Some confl -> report_b_unsat confl + None -> () | Some confl -> report_unsat confl with Trivial -> () let add_clauses cnf ~cnumber = - List.iter (add_clause ~cnumber) cnf; - match theory_propagate () with - None -> () | Some dep -> report_t_unsat dep + List.iter (add_clause ~cnumber) cnf let init_solver cnf ~cnumber = let nbv = made_vars_info env.vars in diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml index 84d748f7..829fae4e 100644 --- a/sat/theory_intf.ml +++ b/sat/theory_intf.ml @@ -25,7 +25,7 @@ module type S = sig start : int; length : int; get : int -> formula; - push : formula -> unit; + push : formula -> formula list -> proof -> unit; } type level @@ -33,7 +33,7 @@ module type S = sig type res = | Sat of level - | Unsat of formula list + | Unsat of formula list * proof (** Type returned by the theory, either the current set of assumptions is satisfiable, or it is not, in which case an unsatisfiable clause (hopefully minimal) is returned. Formulas in the unsat clause must come from the current set of assumptions. *) diff --git a/sat/tseitin.ml b/sat/tseitin.ml index e7aacfd2..0362c429 100644 --- a/sat/tseitin.ml +++ b/sat/tseitin.ml @@ -39,11 +39,6 @@ module Make (F : Formula_intf.S) = struct let make comb l = Comb (comb, l) - let value env c = - if List.mem c env then Some true - else if List.mem (make Not [c]) env then Some false - else None - let make_atom p = Lit p let atomic_true = F.fresh ()