From a00506b95f1255ffca3a2b08e729102bc741c5fd Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 31 Oct 2014 14:09:59 +0100 Subject: [PATCH] Solver module is now functorised. 'make' now compiles. --- Makefile | 3 + _tags | 1 + msat.mlpack | 17 +- msat.odocl | 9 +- sat/.merlin | 1 + sat/explanation.ml | 2 + sat/formula_intf.ml | 7 +- sat/solver.ml | 1797 ++++++++++++++++++-------------------- sat/solver.mli | 8 +- sat/solver_types.ml | 29 +- sat/solver_types_intf.ml | 4 +- sat/theory_intf.ml | 8 +- smt/cc.ml | 14 +- smt/literal.ml | 18 +- smt/literal.mli | 4 +- smt/smt.ml | 10 +- smt/term.ml | 4 +- smt/term.mli | 4 +- 18 files changed, 931 insertions(+), 1009 deletions(-) diff --git a/Makefile b/Makefile index 7a091109..d7e31f45 100644 --- a/Makefile +++ b/Makefile @@ -18,6 +18,9 @@ $(LIB): doc: $(COMP) $(FLAGS) $(DIRS) $(DOC) +log: + cat _build/$(LOG) || true + clean: $(COMP) -clean diff --git a/_tags b/_tags index c3d8dc13..e3b6de48 100644 --- a/_tags +++ b/_tags @@ -1,2 +1,3 @@ : for-pack(Msat) +: for-pack(Msat) diff --git a/msat.mlpack b/msat.mlpack index e35f665b..b4591901 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -1,18 +1,5 @@ -Arith -Cc -Combine -Exception Explanation -Fm -Intervals -Literal -Polynome -Smt +Formula_intf Solver Solver_types -Sum -Symbols -Term -Ty -Uf -Use +Theory_intf diff --git a/msat.odocl b/msat.odocl index 1f78d9ee..87ca5a83 100644 --- a/msat.odocl +++ b/msat.odocl @@ -1,15 +1,18 @@ +sat/Formula_intf +sat/Explanation +sat/Solver +sat/Solver_types +sat/Theory_intf + smt/Arith smt/Cc smt/Combine smt/Exception -smt/Explanation smt/Fm smt/Intervals smt/Literal smt/Polynome smt/Smt -smt/Solver -smt/Solver_types smt/Sum smt/Symbols smt/Term diff --git a/sat/.merlin b/sat/.merlin index ddac6bf5..91f14621 100644 --- a/sat/.merlin +++ b/sat/.merlin @@ -2,3 +2,4 @@ S ./ S ../common/ B ../_build/ +B ../_build/common/ diff --git a/sat/explanation.ml b/sat/explanation.ml index 380f8ef0..89e13f2c 100644 --- a/sat/explanation.ml +++ b/sat/explanation.ml @@ -14,6 +14,8 @@ open Format +module type S = Explanation_intf.S + module Make(Stypes : Solver_types.S) = struct type atom = Stypes.atom diff --git a/sat/formula_intf.ml b/sat/formula_intf.ml index 60ce4037..03834ae8 100644 --- a/sat/formula_intf.ml +++ b/sat/formula_intf.ml @@ -17,12 +17,14 @@ module type S = sig type t - val vrai : t - val faux : t + val true_ : t + val false_ : t val dummy : t val neg : t -> t + val norm : t -> t * bool + (** Returns a 'normalized' form of the formula, possibly negated *) val hash : t -> int val equal : t -> t -> bool @@ -34,7 +36,6 @@ module type S = sig val print : Format.formatter -> t -> unit module Map : Map.S with type key = t - module Set : Set.S with type elt = t end diff --git a/sat/solver.ml b/sat/solver.ml index 474dfd6b..d5ef01ea 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -12,1019 +12,942 @@ open Format -module Make(F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) = struct +module Make (F : Formula_intf.S) + (St : Solver_types.S with type formula = F.t) + (Ex : Explanation.S with type atom = St.atom) + (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) = struct -module Stypes = Solver_types.Make(F) -module Ex = Explanation.Make(Stypes) + open St -open Stypes - -exception Sat -exception Unsat of clause list -exception Restart - -type env = - { - (* si vrai, les contraintes sont deja fausses *) - mutable is_unsat : bool; - - mutable unsat_core : clause list; + exception Sat + exception Unsat of clause list + exception Restart + exception Conflict of clause + type env = { + (* si true_, les contraintes sont deja fausses *) + mutable is_unsat : bool; + mutable unsat_core : clause list; (* clauses du probleme *) - mutable clauses : clause Vec.t; - + mutable clauses : clause Vec.t; (* clauses apprises *) - mutable learnts : clause Vec.t; - + mutable learnts : clause Vec.t; (* valeur de l'increment pour l'activite des clauses *) - mutable clause_inc : float; - + mutable clause_inc : float; (* valeur de l'increment pour l'activite des variables *) - mutable var_inc : float; - + mutable var_inc : float; (* un vecteur des variables du probleme *) - mutable vars : var Vec.t; - + mutable vars : var Vec.t; (* la pile de decisions avec les faits impliques *) - mutable trail : atom Vec.t; - + mutable trail : atom Vec.t; (* une pile qui pointe vers les niveaux de decision dans trail *) - mutable trail_lim : int Vec.t; - + mutable trail_lim : int Vec.t; (* Tete de la File des faits unitaires a propager. C'est un index vers le trail *) - mutable qhead : int; - + mutable qhead : int; (* Nombre des assignements top-level depuis la derniere execution de 'simplify()' *) - mutable simpDB_assigns : int; - + mutable simpDB_assigns : int; (* Nombre restant de propagations a faire avant la prochaine execution de 'simplify()' *) - mutable simpDB_props : int; - + mutable simpDB_props : int; (* Un tas ordone en fonction de l'activite des variables *) - mutable order : Iheap.t; - + mutable order : Iheap.t; (* estimation de progressions, mis a jour par 'search()' *) - mutable progress_estimate : float; - + mutable progress_estimate : float; (* *) - remove_satisfied : bool; - + remove_satisfied : bool; (* inverse du facteur d'acitivte des variables, vaut 1/0.999 par defaut *) - var_decay : float; - + var_decay : float; (* inverse du facteur d'activite des clauses, vaut 1/0.95 par defaut *) - clause_decay : float; - + clause_decay : float; (* la limite de restart initiale, vaut 100 par defaut *) - mutable restart_first : int; - + mutable restart_first : int; (* facteur de multiplication de restart limite, vaut 1.5 par defaut*) - restart_inc : float; - + restart_inc : float; (* limite initiale du nombre de clause apprises, vaut 1/3 des clauses originales par defaut *) - mutable learntsize_factor : float; - + mutable learntsize_factor : float; (* multiplier learntsize_factor par cette valeur a chaque restart, vaut 1.1 par defaut *) - learntsize_inc : float; - + learntsize_inc : float; (* controler la minimisation des clauses conflit, vaut true par defaut *) - expensive_ccmin : bool; - + expensive_ccmin : bool; (* controle la polarite a choisir lors de la decision *) - polarity_mode : bool; - - mutable starts : int; - - mutable decisions : int; - - mutable propagations : int; - - mutable conflicts : int; - - mutable clauses_literals : int; - - mutable learnts_literals : int; - - mutable max_literals : int; - - mutable tot_literals : int; - - mutable nb_init_vars : int; - - mutable nb_init_clauses : int; - - mutable model : var Vec.t; - - mutable tenv : Th.t; - - mutable tenv_queue : Th.t Vec.t; - - mutable tatoms_queue : atom Queue.t; + polarity_mode : bool; + mutable starts : int; + mutable decisions : int; + mutable propagations : int; + mutable conflicts : int; + mutable clauses_literals : int; + mutable learnts_literals : int; + mutable max_literals : int; + mutable tot_literals : int; + mutable nb_init_vars : int; + mutable nb_init_clauses : int; + mutable model : var Vec.t; + mutable tenv : Th.t; + mutable tenv_queue : Th.t Vec.t; + mutable tatoms_queue : atom Queue.t; } - - -exception Conflict of clause - - type state = - { + type state = { env : env; st_cpt_mk_var: int; - st_ma : var F.Map.t; - } - - - let env = - { - is_unsat = false; - - unsat_core = [] ; - - clauses = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*) - - learnts = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*) - - clause_inc = 1.; - - var_inc = 1.; - - vars = Vec.make 0 dummy_var; (*sera mis a jour lors du parsing*) - - trail = Vec.make 601 dummy_atom; - - trail_lim = Vec.make 601 (-105); - - qhead = 0; - - simpDB_assigns = -1; - - simpDB_props = 0; - - order = Iheap.init 0; (* sera mis a jour dans solve *) - - progress_estimate = 0.; - - remove_satisfied = true; - - var_decay = 1. /. 0.95; - - clause_decay = 1. /. 0.999; - - restart_first = 100; - - restart_inc = 1.5; - - learntsize_factor = 1. /. 3. ; - - learntsize_inc = 1.1; - - expensive_ccmin = true; - - polarity_mode = false; - - starts = 0; - - decisions = 0; - - propagations = 0; - - conflicts = 0; - - clauses_literals = 0; - - learnts_literals = 0; - - max_literals = 0; - - tot_literals = 0; - - nb_init_vars = 0; - - nb_init_clauses = 0; - - model = Vec.make 0 dummy_var; - - tenv = Th.empty(); - - tenv_queue = Vec.make 100 (Th.empty()); - - tatoms_queue = Queue.create (); + st_ma : varmap; + } + let env = { + is_unsat = false; + unsat_core = [] ; + clauses = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*) + learnts = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*) + clause_inc = 1.; + var_inc = 1.; + vars = Vec.make 0 dummy_var; (*sera mis a jour lors du parsing*) + trail = Vec.make 601 dummy_atom; + trail_lim = Vec.make 601 (-105); + qhead = 0; + simpDB_assigns = -1; + simpDB_props = 0; + order = Iheap.init 0; (* sera mis a jour dans solve *) + progress_estimate = 0.; + remove_satisfied = true; + var_decay = 1. /. 0.95; + clause_decay = 1. /. 0.999; + restart_first = 100; + restart_inc = 1.5; + learntsize_factor = 1. /. 3. ; + learntsize_inc = 1.1; + expensive_ccmin = true; + polarity_mode = false; + starts = 0; + decisions = 0; + propagations = 0; + conflicts = 0; + clauses_literals = 0; + learnts_literals = 0; + max_literals = 0; + tot_literals = 0; + nb_init_vars = 0; + nb_init_clauses = 0; + model = Vec.make 0 dummy_var; + tenv = Th.empty(); + tenv_queue = Vec.make 100 (Th.empty()); + tatoms_queue = Queue.create (); } -let f_weight i j = (Vec.get env.vars j).weight < (Vec.get env.vars i).weight + let f_weight i j = + (Vec.get env.vars j).weight < (Vec.get env.vars i).weight -let f_filter i = (Vec.get env.vars i).level < 0 + let f_filter i = + (Vec.get env.vars i).level < 0 -let insert_var_order v = - Iheap.insert f_weight env.order v.vid + let insert_var_order v = + Iheap.insert f_weight env.order v.vid -let var_decay_activity () = env.var_inc <- env.var_inc *. env.var_decay + let var_decay_activity () = + env.var_inc <- env.var_inc *. env.var_decay -let clause_decay_activity () = - env.clause_inc <- env.clause_inc *. env.clause_decay + let clause_decay_activity () = + env.clause_inc <- env.clause_inc *. env.clause_decay -let var_bump_activity v = - v.weight <- v.weight +. env.var_inc; - if v.weight > 1e100 then begin - for i = 0 to env.vars.Vec.sz - 1 do - (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100 - done; - env.var_inc <- env.var_inc *. 1e-100; - end; - if Iheap.in_heap env.order v.vid then - Iheap.decrease f_weight env.order v.vid + let var_bump_activity v = + v.weight <- v.weight +. env.var_inc; + if v.weight > 1e100 then begin + for i = 0 to env.vars.Vec.sz - 1 do + (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100 + done; + env.var_inc <- env.var_inc *. 1e-100; + end; + if Iheap.in_heap env.order v.vid then + Iheap.decrease f_weight env.order v.vid -let clause_bump_activity c = - c.activity <- c.activity +. env.clause_inc; - if c.activity > 1e20 then begin - for i = 0 to env.learnts.Vec.sz - 1 do - (Vec.get env.learnts i).activity <- - (Vec.get env.learnts i).activity *. 1e-20; - done; - env.clause_inc <- env.clause_inc *. 1e-20 - end - -let decision_level () = Vec.size env.trail_lim - -let nb_assigns () = Vec.size env.trail -let nb_clauses () = Vec.size env.clauses -let nb_learnts () = Vec.size env.learnts -let nb_vars () = Vec.size env.vars - -let new_decision_level() = - Vec.push env.trail_lim (Vec.size env.trail); - Vec.push env.tenv_queue env.tenv (* save the current tenv *) - -let attach_clause c = - Vec.push (Vec.get c.atoms 0).neg.watched c; - Vec.push (Vec.get c.atoms 1).neg.watched c; - if c.learnt then - env.learnts_literals <- env.learnts_literals + Vec.size c.atoms - else - env.clauses_literals <- env.clauses_literals + Vec.size c.atoms - -let detach_clause c = - c.removed <- true; - (* - Vec.remove (Vec.get c.atoms 0).neg.watched c; - Vec.remove (Vec.get c.atoms 1).neg.watched c; - *) - if c.learnt then - env.learnts_literals <- env.learnts_literals - Vec.size c.atoms - else - env.clauses_literals <- env.clauses_literals - Vec.size c.atoms - -let remove_clause c = detach_clause c - -let satisfied c = - try - for i = 0 to Vec.size c.atoms - 1 do - if (Vec.get c.atoms i).is_true then raise Exit - done; - false - with Exit -> true - -(* annule tout jusqu'a lvl *exclu* *) -let cancel_until lvl = - if decision_level () > lvl then begin - env.qhead <- Vec.get env.trail_lim lvl; - for c = Vec.size env.trail - 1 downto env.qhead do - let a = Vec.get env.trail c in - a.is_true <- false; - a.neg.is_true <- false; - a.var.level <- -1; - a.var.reason <- None; - a.var.vpremise <- []; - insert_var_order a.var - done; - Queue.clear env.tatoms_queue; - env.tenv <- Vec.get env.tenv_queue lvl; (* recover the right tenv *) - Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); - Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); - Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl) - end; - assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) - -let rec pick_branch_lit () = - let max = Iheap.remove_min f_weight env.order in - let v = Vec.get env.vars max in - if v.level>= 0 then begin - assert (v.pa.is_true || v.na.is_true); - pick_branch_lit () - end - else v - -let enqueue a lvl reason = - assert (not a.is_true && not a.neg.is_true && - a.var.level < 0 && a.var.reason = None && lvl >= 0); - (* Garder la reason car elle est utile pour les unsat-core *) - (*let reason = if lvl = 0 then None else reason in*) - a.is_true <- true; - a.var.level <- lvl; - a.var.reason <- reason; - (*eprintf "enqueue: %a@." Debug.atom a; *) - Vec.push env.trail a - -let progress_estimate () = - let prg = ref 0. in - let nbv = to_float (nb_vars()) in - let lvl = decision_level () in - let _F = 1. /. nbv in - for i = 0 to lvl do - let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in - let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in - prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg)) - done; - !prg /. nbv - -let propagate_in_clause a c i watched new_sz = - let atoms = c.atoms in - let first = Vec.get atoms 0 in - if first == a.neg then begin (* le litiral faux doit etre dans .(1) *) - Vec.set atoms 0 (Vec.get atoms 1); - Vec.set atoms 1 first - end; - let first = Vec.get atoms 0 in - if first.is_true then begin - (* clause vraie, la garder dans les watched *) - Vec.set watched !new_sz c; - incr new_sz; - end - else - try (* chercher un nouveau watcher *) - for k = 2 to Vec.size atoms - 1 do - let ak = Vec.get atoms k in - if not (ak.neg.is_true) then begin - (* Watcher Trouve: mettre a jour et sortir *) - Vec.set atoms 1 ak; - Vec.set atoms k a.neg; - Vec.push ak.neg.watched c; - raise Exit + let clause_bump_activity c = + c.activity <- c.activity +. env.clause_inc; + if c.activity > 1e20 then begin + for i = 0 to env.learnts.Vec.sz - 1 do + (Vec.get env.learnts i).activity <- + (Vec.get env.learnts i).activity *. 1e-20; + done; + env.clause_inc <- env.clause_inc *. 1e-20 end - done; - (* Watcher NON Trouve *) - if first.neg.is_true then begin - (* la clause est fausse *) - env.qhead <- Vec.size env.trail; - for k = i to Vec.size watched - 1 do - Vec.set watched !new_sz (Vec.get watched k); - incr new_sz; + + let decision_level () = Vec.size env.trail_lim + + let nb_assigns () = Vec.size env.trail + let nb_clauses () = Vec.size env.clauses + let nb_learnts () = Vec.size env.learnts + let nb_vars () = Vec.size env.vars + + let new_decision_level() = + Vec.push env.trail_lim (Vec.size env.trail); + Vec.push env.tenv_queue env.tenv (* save the current tenv *) + + let attach_clause c = + Vec.push (Vec.get c.atoms 0).neg.watched c; + Vec.push (Vec.get c.atoms 1).neg.watched c; + if c.learnt then + env.learnts_literals <- env.learnts_literals + Vec.size c.atoms + else + env.clauses_literals <- env.clauses_literals + Vec.size c.atoms + + let detach_clause c = + c.removed <- true; + (* + Vec.remove (Vec.get c.atoms 0).neg.watched c; + Vec.remove (Vec.get c.atoms 1).neg.watched c; + *) + if c.learnt then + env.learnts_literals <- env.learnts_literals - Vec.size c.atoms + else + env.clauses_literals <- env.clauses_literals - Vec.size c.atoms + + let remove_clause c = detach_clause c + + let satisfied c = + try + for i = 0 to Vec.size c.atoms - 1 do + if (Vec.get c.atoms i).is_true then raise Exit done; - raise (Conflict c) + false + with Exit -> true + + (* annule tout jusqu'a lvl *exclu* *) + let cancel_until lvl = + if decision_level () > lvl then begin + env.qhead <- Vec.get env.trail_lim lvl; + for c = Vec.size env.trail - 1 downto env.qhead do + let a = Vec.get env.trail c in + a.is_true <- false; + a.neg.is_true <- false; + a.var.level <- -1; + a.var.reason <- None; + a.var.vpremise <- []; + insert_var_order a.var + done; + Queue.clear env.tatoms_queue; + env.tenv <- Vec.get env.tenv_queue lvl; (* recover the right tenv *) + Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); + Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); + Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl) + end; + assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) + + let rec pick_branch_lit () = + let max = Iheap.remove_min f_weight env.order in + let v = Vec.get env.vars max in + if v.level>= 0 then begin + assert (v.pa.is_true || v.na.is_true); + pick_branch_lit () end - else begin - (* la clause est unitaire *) + else v + + let enqueue a lvl reason = + assert (not a.is_true && not a.neg.is_true && + a.var.level < 0 && a.var.reason = None && lvl >= 0); + (* Garder la reason car elle est utile pour les unsat-core *) + (*let reason = if lvl = 0 then None else reason in*) + a.is_true <- true; + a.var.level <- lvl; + a.var.reason <- reason; + (*eprintf "enqueue: %a@." Debug.atom a; *) + Vec.push env.trail a + + let progress_estimate () = + let prg = ref 0. in + let nbv = to_float (nb_vars()) in + let lvl = decision_level () in + let _F = 1. /. nbv in + for i = 0 to lvl do + let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in + let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in + prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg)) + done; + !prg /. nbv + + let propagate_in_clause a c i watched new_sz = + let atoms = c.atoms in + let first = Vec.get atoms 0 in + if first == a.neg then begin (* le litiral false_ doit etre dans .(1) *) + Vec.set atoms 0 (Vec.get atoms 1); + Vec.set atoms 1 first + end; + let first = Vec.get atoms 0 in + if first.is_true then begin + (* clause vraie, la garder dans les watched *) Vec.set watched !new_sz c; incr new_sz; - enqueue first (decision_level ()) (Some c) end - with Exit -> () + else + try (* chercher un nouveau watcher *) + for k = 2 to Vec.size atoms - 1 do + let ak = Vec.get atoms k in + if not (ak.neg.is_true) then begin + (* Watcher Trouve: mettre a jour et sortir *) + Vec.set atoms 1 ak; + Vec.set atoms k a.neg; + Vec.push ak.neg.watched c; + raise Exit + end + done; + (* Watcher NON Trouve *) + if first.neg.is_true then begin + (* la clause est fausse *) + env.qhead <- Vec.size env.trail; + for k = i to Vec.size watched - 1 do + Vec.set watched !new_sz (Vec.get watched k); + incr new_sz; + done; + raise (Conflict c) + end + else begin + (* la clause est unitaire *) + Vec.set watched !new_sz c; + incr new_sz; + enqueue first (decision_level ()) (Some c) + end + with Exit -> () -let propagate_atom a res = - let watched = a.watched in - let new_sz_w = ref 0 in - begin - try - for i = 0 to Vec.size watched - 1 do - let c = Vec.get watched i in - if not c.removed then propagate_in_clause a c i watched new_sz_w + let propagate_atom a res = + let watched = a.watched in + let new_sz_w = ref 0 in + begin + try + for i = 0 to Vec.size watched - 1 do + let c = Vec.get watched i in + if not c.removed then propagate_in_clause a c i watched new_sz_w + done; + with Conflict c -> assert (!res = None); res := Some c + end; + let dead_part = Vec.size watched - !new_sz_w in + Vec.shrink watched dead_part + + let expensive_theory_propagate () = None + (* try *) + (* if D1.d then eprintf "expensive_theory_propagate@."; *) + (* ignore(Th.expensive_processing env.tenv); *) + (* if D1.d then eprintf "expensive_theory_propagate => None@."; *) + (* None *) + (* with Th.Inconsistent dep -> *) + (* if D1.d then eprintf "expensive_theory_propagate => Inconsistent@."; *) + (* Some dep *) + + let theory_propagate () = + let facts = ref [] in + while not (Queue.is_empty env.tatoms_queue) do + let a = Queue.pop env.tatoms_queue in + if a.is_true then + (*let ex = if a.var.level > 0 then Ex.singleton a else Ex.empty in*) + let ex = Ex.singleton a in (* Usefull for debugging *) + facts := (a.lit, ex) :: !facts + else + if a.neg.is_true then + (*let ex = if a.var.level > 0 then Ex.singleton a.neg else Ex.empty in*) + let ex = Ex.singleton a.neg in (* Usefull for debugging *) + facts := (a.neg.lit, ex) :: !facts + else assert false; done; - with Conflict c -> assert (!res = None); res := Some c - end; - let dead_part = Vec.size watched - !new_sz_w in - Vec.shrink watched dead_part + try + let full_model = nb_assigns() = env.nb_init_vars in + env.tenv <- + List.fold_left + (fun t (a,ex) -> let t = Th.assume ~cs:true a ex t in t) + env.tenv !facts; + if full_model then expensive_theory_propagate () + else None + with Th.Inconsistent dep -> + (* eprintf "th inconsistent : %a @." Ex.print dep; *) + Some dep -let expensive_theory_propagate () = None - (* try *) - (* if D1.d then eprintf "expensive_theory_propagate@."; *) - (* ignore(Th.expensive_processing env.tenv); *) - (* if D1.d then eprintf "expensive_theory_propagate => None@."; *) - (* None *) - (* with Th.Inconsistent dep -> *) - (* if D1.d then eprintf "expensive_theory_propagate => Inconsistent@."; *) - (* Some dep *) - -let theory_propagate () = - let facts = ref [] in - while not (Queue.is_empty env.tatoms_queue) do - let a = Queue.pop env.tatoms_queue in - if a.is_true then - (*let ex = if a.var.level > 0 then Ex.singleton a else Ex.empty in*) - let ex = Ex.singleton a in (* Usefull for debugging *) - facts := (a.lit, ex) :: !facts - else - if a.neg.is_true then - (*let ex = if a.var.level > 0 then Ex.singleton a.neg else Ex.empty in*) - let ex = Ex.singleton a.neg in (* Usefull for debugging *) - facts := (a.neg.lit, ex) :: !facts - else assert false; - done; - try - let full_model = nb_assigns() = env.nb_init_vars in - env.tenv <- - List.fold_left - (fun t (a,ex) -> let t = Th.assume ~cs:true a ex t in t) - env.tenv !facts; - if full_model then expensive_theory_propagate () - else None - with Th.Inconsistent dep -> - (* eprintf "th inconsistent : %a @." Ex.print dep; *) - Some dep - -let 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; - Queue.push a env.tatoms_queue; - done; - env.propagations <- env.propagations + !num_props; - env.simpDB_props <- env.simpDB_props - !num_props; - !res + let 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; + Queue.push a env.tatoms_queue; + done; + env.propagations <- env.propagations + !num_props; + env.simpDB_props <- env.simpDB_props - !num_props; + !res -let analyze c_clause = - let pathC = ref 0 in - let learnt = ref [] in - let cond = ref true in - let blevel = ref 0 in - let seen = ref [] in - let c = ref c_clause in - let tr_ind = ref (Vec.size env.trail - 1) in - let size = ref 1 in - let history = ref [] in - while !cond do - if !c.learnt then clause_bump_activity !c; - history := !c :: !history; - (* visit the current predecessors *) - for j = 0 to Vec.size !c.atoms - 1 do - let q = Vec.get !c.atoms j in - (*printf "I visit %a@." D1.atom q;*) - assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) - if not q.var.seen && q.var.level > 0 then begin - var_bump_activity q.var; - q.var.seen <- true; - seen := q :: !seen; - if q.var.level >= decision_level () then incr pathC + let analyze c_clause = + let pathC = ref 0 in + let learnt = ref [] in + let cond = ref true in + let blevel = ref 0 in + let seen = ref [] in + let c = ref c_clause in + let tr_ind = ref (Vec.size env.trail - 1) in + let size = ref 1 in + let history = ref [] in + while !cond do + if !c.learnt then clause_bump_activity !c; + history := !c :: !history; + (* visit the current predecessors *) + for j = 0 to Vec.size !c.atoms - 1 do + let q = Vec.get !c.atoms j in + (*printf "I visit %a@." D1.atom q;*) + assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) + if not q.var.seen && q.var.level > 0 then begin + var_bump_activity q.var; + q.var.seen <- true; + seen := q :: !seen; + if q.var.level >= decision_level () then incr pathC + else begin + learnt := q :: !learnt; + incr size; + blevel := max !blevel q.var.level + end + end + done; + + (* look for the next node to expand *) + while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; + decr pathC; + let p = Vec.get env.trail !tr_ind in + decr tr_ind; + match !pathC, p.var.reason with + | 0, _ -> + cond := false; + learnt := p.neg :: (List.rev !learnt) + | n, None -> assert false + | n, Some cl -> c := cl + done; + List.iter (fun q -> q.var.seen <- false) !seen; + !blevel, !learnt, !history, !size + + let f_sort_db c1 c2 = + let sz1 = Vec.size c1.atoms in + let sz2 = Vec.size c2.atoms in + let c = compare c1.activity c2.activity in + if sz1 = sz2 && c = 0 then 0 + else + if sz1 > 2 && (sz2 = 2 || c < 0) then -1 + else 1 + + let locked c = false(* + try + for i = 0 to Vec.size env.vars - 1 do + match (Vec.get env.vars i).reason with + | Some c' when c ==c' -> raise Exit + | _ -> () + done; + false + with Exit -> true*) + + let reduce_db () = () + (* + let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in + Vec.sort env.learnts f_sort_db; + let lim2 = Vec.size env.learnts in + let lim1 = lim2 / 2 in + let j = ref 0 in + for i = 0 to lim1 - 1 do + let c = Vec.get env.learnts i in + if Vec.size c.atoms > 2 && not (locked c) then + remove_clause c + else + begin Vec.set env.learnts !j c; incr j end + done; + for i = lim1 to lim2 - 1 do + let c = Vec.get env.learnts i in + if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then + remove_clause c + else + begin Vec.set env.learnts !j c; incr j end + done; + Vec.shrink env.learnts (lim2 - !j) + *) + + let remove_satisfied vec = + let j = ref 0 in + let k = Vec.size vec - 1 in + for i = 0 to k do + let c = Vec.get vec i in + if satisfied c then remove_clause c else begin - learnt := q :: !learnt; - incr size; - blevel := max !blevel q.var.level + Vec.set vec !j (Vec.get vec i); + incr j end - end - done; - - (* look for the next node to expand *) - while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; - decr pathC; - let p = Vec.get env.trail !tr_ind in - decr tr_ind; - match !pathC, p.var.reason with - | 0, _ -> - cond := false; - learnt := p.neg :: (List.rev !learnt) - | n, None -> assert false - | n, Some cl -> c := cl - done; - List.iter (fun q -> q.var.seen <- false) !seen; - !blevel, !learnt, !history, !size - -let f_sort_db c1 c2 = - let sz1 = Vec.size c1.atoms in - let sz2 = Vec.size c2.atoms in - let c = compare c1.activity c2.activity in - if sz1 = sz2 && c = 0 then 0 - else - if sz1 > 2 && (sz2 = 2 || c < 0) then -1 - else 1 - -let locked c = false(* - try - for i = 0 to Vec.size env.vars - 1 do - match (Vec.get env.vars i).reason with - | Some c' when c ==c' -> raise Exit - | _ -> () - done; - false - with Exit -> true*) - -let reduce_db () = () -(* - let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in - Vec.sort env.learnts f_sort_db; - let lim2 = Vec.size env.learnts in - let lim1 = lim2 / 2 in - let j = ref 0 in - for i = 0 to lim1 - 1 do - let c = Vec.get env.learnts i in - if Vec.size c.atoms > 2 && not (locked c) then - remove_clause c - else - begin Vec.set env.learnts !j c; incr j end - done; - for i = lim1 to lim2 - 1 do - let c = Vec.get env.learnts i in - if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then - remove_clause c - else - begin Vec.set env.learnts !j c; incr j end - done; - Vec.shrink env.learnts (lim2 - !j) -*) - -let remove_satisfied vec = - let j = ref 0 in - let k = Vec.size vec - 1 in - for i = 0 to k do - let c = Vec.get vec i in - if satisfied c then remove_clause c - else begin - Vec.set vec !j (Vec.get vec i); - incr j - end - done; - Vec.shrink vec (k + 1 - !j) + done; + Vec.shrink vec (k + 1 - !j) -module HUC = Hashtbl.Make - (struct type t = clause let equal = (==) let hash = Hashtbl.hash end) + module HUC = Hashtbl.Make + (struct type t = clause let equal = (==) let hash = Hashtbl.hash end) -let report_b_unsat ({atoms=atoms} as confl) = - let l = ref [confl] in - for i = 0 to Vec.size atoms - 1 do - let v = (Vec.get atoms i).var in - l := List.rev_append v.vpremise !l; - match v.reason with None -> () | Some c -> l := c :: !l - done; - if false then begin - eprintf "@.>>UNSAT Deduction made from:@."; - List.iter - (fun hc -> - eprintf " %a@." Debug.clause hc - )!l; - end; - let uc = HUC.create 17 in - let rec roots todo = - match todo with - | [] -> () - | c::r -> - for i = 0 to Vec.size c.atoms - 1 do - let v = (Vec.get c.atoms i).var in - if not v.seen then begin - v.seen <- true; - roots v.vpremise; - match v.reason with None -> () | Some r -> roots [r]; - end - done; - match c.cpremise with - | [] -> if not (HUC.mem uc c) then HUC.add uc c (); roots r - | prems -> roots prems; roots r - in roots !l; - let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in - if false then begin - eprintf "@.>>UNSAT_CORE:@."; - List.iter - (fun hc -> - eprintf " %a@." Debug.clause hc - )unsat_core; - end; - env.is_unsat <- true; - env.unsat_core <- unsat_core; - raise (Unsat unsat_core) + let report_b_unsat ({atoms=atoms} as confl) = + let l = ref [confl] in + for i = 0 to Vec.size atoms - 1 do + let v = (Vec.get atoms i).var in + l := List.rev_append v.vpremise !l; + match v.reason with None -> () | Some c -> l := c :: !l + done; + if false then begin + eprintf "@.>>UNSAT Deduction made from:@."; + List.iter + (fun hc -> + eprintf " %a@." pp_clause hc + )!l; + end; + let uc = HUC.create 17 in + let rec roots todo = + match todo with + | [] -> () + | c::r -> + for i = 0 to Vec.size c.atoms - 1 do + let v = (Vec.get c.atoms i).var in + if not v.seen then begin + v.seen <- true; + roots v.vpremise; + match v.reason with None -> () | Some r -> roots [r]; + end + done; + match c.cpremise with + | [] -> if not (HUC.mem uc c) then HUC.add uc c (); roots r + | prems -> roots prems; roots r + in roots !l; + let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in + if false then begin + eprintf "@.>>UNSAT_CORE:@."; + List.iter + (fun hc -> + eprintf " %a@." pp_clause hc + )unsat_core; + end; + env.is_unsat <- true; + env.unsat_core <- unsat_core; + raise (Unsat unsat_core) -let report_t_unsat dep = - let l = - Ex.fold_atoms - (fun {var=v} l -> - let l = List.rev_append v.vpremise l in - match v.reason with None -> l | Some c -> c :: l - ) dep [] - in - if false then begin - eprintf "@.>>T-UNSAT Deduction made from:@."; - List.iter - (fun hc -> - eprintf " %a@." Debug.clause hc - )l; - end; - let uc = HUC.create 17 in - let rec roots todo = - match todo with - | [] -> () - | c::r -> - for i = 0 to Vec.size c.atoms - 1 do - let v = (Vec.get c.atoms i).var in - if not v.seen then begin - v.seen <- true; - roots v.vpremise; - match v.reason with None -> () | Some r -> roots [r]; - end - done; - match c.cpremise with - | [] -> if not (HUC.mem uc c) then HUC.add uc c (); roots r - | prems -> roots prems; roots r - in roots l; - let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in - if false then begin - eprintf "@.>>T-UNSAT_CORE:@."; - List.iter - (fun hc -> - eprintf " %a@." Debug.clause hc - ) unsat_core; - end; - env.is_unsat <- true; - env.unsat_core <- unsat_core; - raise (Unsat unsat_core) - -let simplify () = - assert (decision_level () = 0); - if env.is_unsat then raise (Unsat env.unsat_core); - begin - match propagate () with - | Some confl -> report_b_unsat confl - | None -> - match theory_propagate () with - Some dep -> report_t_unsat dep - | 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; - if env.remove_satisfied then remove_satisfied env.clauses; - (*Iheap.filter env.order f_filter f_weight;*) - env.simpDB_assigns <- nb_assigns (); - env.simpDB_props <- env.clauses_literals + env.learnts_literals; - end - -let record_learnt_clause blevel learnt history size = - begin match learnt with - | [] -> assert false - | [fuip] -> - assert (blevel = 0); - fuip.var.vpremise <- history; - enqueue fuip 0 None - | fuip :: _ -> - let name = fresh_lname () in - let lclause = make_clause name learnt size true history in - Vec.push env.learnts lclause; - attach_clause lclause; - clause_bump_activity lclause; - enqueue fuip blevel (Some lclause) - end; - var_decay_activity (); - clause_decay_activity() - -let check_inconsistence_of dep = - try - let env = ref (Th.empty()) in (); - Ex.iter_atoms - (fun atom -> - let t = Th.assume ~cs:true atom.lit (Ex.singleton atom) !env in - env := t) - dep; - (* ignore (Th.expensive_processing !env); *) - assert false - with Th.Inconsistent _ -> () - -let theory_analyze dep = - let atoms, sz, max_lvl, c_hist = - Ex.fold_atoms - (fun a (acc, sz, max_lvl, c_hist) -> - let c_hist = List.rev_append a.var.vpremise c_hist in - let c_hist = match a.var.reason with - | None -> c_hist | Some r -> r:: c_hist in - if a.var.level = 0 then acc, sz, max_lvl, c_hist - else a.neg :: acc, sz + 1, max max_lvl a.var.level, c_hist - ) dep ([], 0, 0, []) - in - if atoms = [] then begin - (* check_inconsistence_of dep; *) - report_t_unsat dep - (* une conjonction de faits unitaires etaient deja unsat *) - end; - let name = fresh_dname() in - let c_clause = make_clause name atoms sz false c_hist in - (* eprintf "c_clause: %a@." Debug.clause c_clause; *) - c_clause.removed <- true; - - let pathC = ref 0 in - let learnt = ref [] in - let cond = ref true in - let blevel = ref 0 in - let seen = ref [] in - let c = ref c_clause in - let tr_ind = ref (Vec.size env.trail - 1) in - let size = ref 1 in - let history = ref [] in - while !cond do - if !c.learnt then clause_bump_activity !c; - history := !c :: !history; - (* visit the current predecessors *) - for j = 0 to Vec.size !c.atoms - 1 do - let q = Vec.get !c.atoms j in - (*printf "I visit %a@." D1.atom q;*) - assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) - if not q.var.seen && q.var.level > 0 then begin - var_bump_activity q.var; - q.var.seen <- true; - seen := q :: !seen; - if q.var.level >= max_lvl then incr pathC - else begin - learnt := q :: !learnt; - incr size; - blevel := max !blevel q.var.level - end - end - done; - - (* look for the next node to expand *) - while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; - decr pathC; - let p = Vec.get env.trail !tr_ind in - decr tr_ind; - match !pathC, p.var.reason with - | 0, _ -> - cond := false; - learnt := p.neg :: (List.rev !learnt) - | n, None -> assert false - | n, Some cl -> c := cl - done; - List.iter (fun q -> q.var.seen <- false) !seen; - !blevel, !learnt, !history, !size - - - -let add_boolean_conflict confl = - env.conflicts <- env.conflicts + 1; - if decision_level() = 0 then report_b_unsat confl; (* Top-level conflict *) - let blevel, learnt, history, size = analyze confl in - cancel_until blevel; - record_learnt_clause blevel learnt history size - -let search n_of_conflicts n_of_learnts = - let conflictC = ref 0 in - env.starts <- env.starts + 1; - while (true) do - match propagate () with - | Some confl -> (* Conflict *) - incr conflictC; - 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 - - | 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(); - - env.decisions <- env.decisions + 1; - - new_decision_level(); - let next = pick_branch_lit () in - let current_level = decision_level () in - assert (next.level < 0); - (* eprintf "decide: %a@." Debug.atom next.pa; *) - enqueue next.pa current_level None - done - -let check_clause c = - let b = ref false in - let atoms = c.atoms in - for i = 0 to Vec.size atoms - 1 do - let a = Vec.get atoms i in - b := !b || a.is_true - done; - assert (!b) - -let check_vec vec = - for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done - -let check_model () = - check_vec env.clauses; - check_vec env.learnts - - -let solve () = - if env.is_unsat then raise (Unsat env.unsat_core); - let n_of_conflicts = ref (to_float env.restart_first) in - let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in - try - while true do - (try search (to_int !n_of_conflicts) (to_int !n_of_learnts); - with Restart -> ()); - n_of_conflicts := !n_of_conflicts *. env.restart_inc; - n_of_learnts := !n_of_learnts *. env.learntsize_inc; - done; - with - | Sat -> - (*check_model ();*) - raise Sat - | (Unsat cl) as e -> - (* check_unsat_core cl; *) - raise e - -exception Trivial - -let partition atoms init = - let rec partition_aux trues unassigned falses init = function - | [] -> trues @ unassigned @ falses, init - | a::r -> - if a.is_true then - if a.var.level = 0 then raise Trivial - else (a::trues) @ unassigned @ falses @ r, init - else if a.neg.is_true then - if a.var.level = 0 then - partition_aux trues unassigned falses - (List.rev_append (a.var.vpremise) init) r - else partition_aux trues unassigned (a::falses) init r - else partition_aux trues (a::unassigned) falses init r - in - partition_aux [] [] [] init atoms - - -let add_clause ~cnumber atoms = - if env.is_unsat then raise (Unsat env.unsat_core); - let init_name = string_of_int cnumber in - let init0 = make_clause init_name atoms (List.length atoms) false [] in - try - let atoms, init = - if decision_level () = 0 then - let atoms, init = List.fold_left - (fun (atoms, init) a -> - if a.is_true then raise Trivial; - if a.neg.is_true then - atoms, (List.rev_append (a.var.vpremise) init) - else a::atoms, init - ) ([], [init0]) atoms in - List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init - else partition atoms [init0] + let report_t_unsat dep = + let l = + Ex.fold_atoms + (fun {var=v} l -> + let l = List.rev_append v.vpremise l in + match v.reason with None -> l | Some c -> c :: l + ) dep [] in - let size = List.length atoms in - match atoms with - | [] -> - report_b_unsat init0; + if false then begin + eprintf "@.>>T-UNSAT Deduction made from:@."; + List.iter + (fun hc -> + eprintf " %a@." pp_clause hc + )l; + end; + let uc = HUC.create 17 in + let rec roots todo = + match todo with + | [] -> () + | c::r -> + for i = 0 to Vec.size c.atoms - 1 do + let v = (Vec.get c.atoms i).var in + if not v.seen then begin + v.seen <- true; + roots v.vpremise; + match v.reason with None -> () | Some r -> roots [r]; + end + done; + match c.cpremise with + | [] -> if not (HUC.mem uc c) then HUC.add uc c (); roots r + | prems -> roots prems; roots r + in roots l; + let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in + if false then begin + eprintf "@.>>T-UNSAT_CORE:@."; + List.iter + (fun hc -> + eprintf " %a@." pp_clause hc + ) unsat_core; + end; + env.is_unsat <- true; + env.unsat_core <- unsat_core; + raise (Unsat unsat_core) - | a::_::_ -> - let name = fresh_name () in - let clause = make_clause name atoms size false init in - attach_clause clause; - Vec.push env.clauses clause; - - if a.neg.is_true then begin - let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in - cancel_until lvl; - add_boolean_conflict clause - end - - | [a] -> - cancel_until 0; - a.var.vpremise <- init; - enqueue a 0 None; + let simplify () = + assert (decision_level () = 0); + if env.is_unsat then raise (Unsat env.unsat_core); + begin match propagate () with - None -> () | Some confl -> report_b_unsat confl - with Trivial -> () + | Some confl -> report_b_unsat confl + | None -> + match theory_propagate () with + Some dep -> report_t_unsat dep + | 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; + if env.remove_satisfied then remove_satisfied env.clauses; + (*Iheap.filter env.order f_filter f_weight;*) + env.simpDB_assigns <- nb_assigns (); + env.simpDB_props <- env.clauses_literals + env.learnts_literals; + end -let add_clauses cnf ~cnumber = - List.iter (add_clause ~cnumber) cnf; - match theory_propagate () with - None -> () | Some dep -> report_t_unsat dep + let record_learnt_clause blevel learnt history size = + begin match learnt with + | [] -> assert false + | [fuip] -> + assert (blevel = 0); + fuip.var.vpremise <- history; + enqueue fuip 0 None + | fuip :: _ -> + let name = fresh_lname () in + let lclause = make_clause name learnt size true history in + Vec.push env.learnts lclause; + attach_clause lclause; + clause_bump_activity lclause; + enqueue fuip blevel (Some lclause) + end; + var_decay_activity (); + clause_decay_activity() -let init_solver cnf ~cnumber = - let nbv, _ = made_vars_info () in - let nbc = env.nb_init_clauses + List.length cnf in - Vec.grow_to_by_double env.vars nbv; - Iheap.grow_to_by_double env.order nbv; - List.iter - (List.iter - (fun a -> - Vec.set env.vars a.var.vid a.var; - insert_var_order a.var - ) - ) cnf; - env.nb_init_vars <- nbv; - Vec.grow_to_by_double env.model nbv; - 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 + let check_inconsistence_of dep = + try + let env = ref (Th.empty()) in (); + Ex.iter_atoms + (fun atom -> + let t = Th.assume ~cs:true atom.lit (Ex.singleton atom) !env in + env := t) + dep; + (* ignore (Th.expensive_processing !env); *) + assert false + with Th.Inconsistent _ -> () + + let theory_analyze dep = + let atoms, sz, max_lvl, c_hist = + Ex.fold_atoms + (fun a (acc, sz, max_lvl, c_hist) -> + let c_hist = List.rev_append a.var.vpremise c_hist in + let c_hist = match a.var.reason with + | None -> c_hist | Some r -> r:: c_hist in + if a.var.level = 0 then acc, sz, max_lvl, c_hist + else a.neg :: acc, sz + 1, max max_lvl a.var.level, c_hist + ) dep ([], 0, 0, []) + in + if atoms = [] then begin + (* check_inconsistence_of dep; *) + report_t_unsat dep + (* une conjonction de faits unitaires etaient deja unsat *) + end; + let name = fresh_dname() in + let c_clause = make_clause name atoms sz false c_hist in + (* eprintf "c_clause: %a@." Debug.clause c_clause; *) + c_clause.removed <- true; + + let pathC = ref 0 in + let learnt = ref [] in + let cond = ref true in + let blevel = ref 0 in + let seen = ref [] in + let c = ref c_clause in + let tr_ind = ref (Vec.size env.trail - 1) in + let size = ref 1 in + let history = ref [] in + while !cond do + if !c.learnt then clause_bump_activity !c; + history := !c :: !history; + (* visit the current predecessors *) + for j = 0 to Vec.size !c.atoms - 1 do + let q = Vec.get !c.atoms j in + (*printf "I visit %a@." D1.atom q;*) + assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) + if not q.var.seen && q.var.level > 0 then begin + var_bump_activity q.var; + q.var.seen <- true; + seen := q :: !seen; + if q.var.level >= max_lvl then incr pathC + else begin + learnt := q :: !learnt; + incr size; + blevel := max !blevel q.var.level + end + end + done; + + (* look for the next node to expand *) + while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; + decr pathC; + let p = Vec.get env.trail !tr_ind in + decr tr_ind; + match !pathC, p.var.reason with + | 0, _ -> + cond := false; + learnt := p.neg :: (List.rev !learnt) + | n, None -> assert false + | n, Some cl -> c := cl + done; + List.iter (fun q -> q.var.seen <- false) !seen; + !blevel, !learnt, !history, !size -let assume cnf ~cnumber = - let cnf = List.map (List.map Solver_types.add_atom) cnf in - init_solver cnf ~cnumber -let clear () = - let empty_theory = Th.empty () in - env.is_unsat <- false; - env.unsat_core <- []; - env.clauses <- Vec.make 0 dummy_clause; - env.learnts <- Vec.make 0 dummy_clause; - env.clause_inc <- 1.; - env.var_inc <- 1.; - env.vars <- Vec.make 0 dummy_var; - env.qhead <- 0; - env.simpDB_assigns <- -1; - env.simpDB_props <- 0; - env.order <- Iheap.init 0; (* sera mis a jour dans solve *) - env.progress_estimate <- 0.; - env.restart_first <- 100; - env.starts <- 0; - env.decisions <- 0; - env.propagations <- 0; - env.conflicts <- 0; - env.clauses_literals <- 0; - env.learnts_literals <- 0; - env.max_literals <- 0; - env.tot_literals <- 0; - env.nb_init_vars <- 0; - env.nb_init_clauses <- 0; - env.tenv <- empty_theory; - env.model <- Vec.make 0 dummy_var; - env.trail <- Vec.make 601 dummy_atom; - env.trail_lim <- Vec.make 601 (-105); - env.tenv_queue <- Vec.make 100 (empty_theory); - env.tatoms_queue <- Queue.create (); - Solver_types.clear () + let add_boolean_conflict confl = + env.conflicts <- env.conflicts + 1; + if decision_level() = 0 then report_b_unsat confl; (* Top-level conflict *) + let blevel, learnt, history, size = analyze confl in + cancel_until blevel; + record_learnt_clause blevel learnt history size + + let search n_of_conflicts n_of_learnts = + let conflictC = ref 0 in + env.starts <- env.starts + 1; + while (true) do + match propagate () with + | Some confl -> (* Conflict *) + incr conflictC; + 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 + + | 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(); + + env.decisions <- env.decisions + 1; + + new_decision_level(); + let next = pick_branch_lit () in + let current_level = decision_level () in + assert (next.level < 0); + (* eprintf "decide: %a@." Debug.atom next.pa; *) + enqueue next.pa current_level None + done + + let check_clause c = + let b = ref false in + let atoms = c.atoms in + for i = 0 to Vec.size atoms - 1 do + let a = Vec.get atoms i in + b := !b || a.is_true + done; + assert (!b) + + let check_vec vec = + for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done + + let check_model () = + check_vec env.clauses; + check_vec env.learnts -let copy (v : 'a) : 'a = Marshal.from_string (Marshal.to_string v []) 0 + let solve () = + if env.is_unsat then raise (Unsat env.unsat_core); + let n_of_conflicts = ref (to_float env.restart_first) in + let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in + try + while true do + (try search (to_int !n_of_conflicts) (to_int !n_of_learnts); + with Restart -> ()); + n_of_conflicts := !n_of_conflicts *. env.restart_inc; + n_of_learnts := !n_of_learnts *. env.learntsize_inc; + done; + with + | Sat -> + (*check_model ();*) + raise Sat + | (Unsat cl) as e -> + (* check_unsat_core cl; *) + raise e -let save () = - let sv = - { env = env; - st_cpt_mk_var = !Solver_types.cpt_mk_var; - st_ma = !Solver_types.ma } - in - copy sv + exception Trivial -let restore { env = s_env; st_cpt_mk_var = st_cpt_mk_var; st_ma = st_ma } = - env.is_unsat <- s_env.is_unsat; - env.unsat_core <- s_env.unsat_core; - env.clauses <- s_env.clauses; - env.learnts <- s_env.learnts; - env.clause_inc <- s_env.clause_inc; - env.var_inc <- s_env.var_inc; - env.vars <- s_env.vars; - env.qhead <- s_env.qhead; - env.simpDB_assigns <- s_env.simpDB_assigns; - env.simpDB_props <- s_env.simpDB_props; - env.order <- s_env.order; - env.progress_estimate <- s_env.progress_estimate; - env.restart_first <- s_env.restart_first; - env.starts <- s_env.starts; - env.decisions <- s_env.decisions; - env.propagations <- s_env.propagations; - env.conflicts <- s_env.conflicts; - env.clauses_literals <- s_env.clauses_literals; - env.learnts_literals <- s_env.learnts_literals; - env.max_literals <- s_env.max_literals; - env.tot_literals <- s_env.tot_literals; - env.nb_init_vars <- s_env.nb_init_vars; - env.nb_init_clauses <- s_env.nb_init_clauses; - env.tenv <- s_env.tenv; - env.model <- s_env.model; - env.trail <- s_env.trail; - env.trail_lim <- s_env.trail_lim; - env.tenv_queue <- s_env.tenv_queue; - env.tatoms_queue <- s_env.tatoms_queue; - env.learntsize_factor <- s_env.learntsize_factor; - Solver_types.cpt_mk_var := st_cpt_mk_var; - Solver_types.ma := st_ma + let partition atoms init = + let rec partition_aux trues unassigned falses init = function + | [] -> trues @ unassigned @ falses, init + | a::r -> + if a.is_true then + if a.var.level = 0 then raise Trivial + else (a::trues) @ unassigned @ falses @ r, init + else if a.neg.is_true then + if a.var.level = 0 then + partition_aux trues unassigned falses + (List.rev_append (a.var.vpremise) init) r + else partition_aux trues unassigned (a::falses) init r + else partition_aux trues (a::unassigned) falses init r + in + partition_aux [] [] [] init atoms - let eval lit = - let var, negated = make_var lit in - let truth = var.pa.is_true in - if negated then not truth else truth + + let add_clause ~cnumber atoms = + if env.is_unsat then raise (Unsat env.unsat_core); + let init_name = string_of_int cnumber in + let init0 = make_clause init_name atoms (List.length atoms) false [] in + try + let atoms, init = + if decision_level () = 0 then + let atoms, init = List.fold_left + (fun (atoms, init) a -> + if a.is_true then raise Trivial; + if a.neg.is_true then + atoms, (List.rev_append (a.var.vpremise) init) + else a::atoms, init + ) ([], [init0]) atoms in + List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init + else partition atoms [init0] + in + let size = List.length atoms in + match atoms with + | [] -> + report_b_unsat init0; + + | a::_::_ -> + let name = fresh_name () in + let clause = make_clause name atoms size false init in + attach_clause clause; + Vec.push env.clauses clause; + + if a.neg.is_true then begin + let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in + cancel_until lvl; + add_boolean_conflict clause + end + + | [a] -> + cancel_until 0; + a.var.vpremise <- init; + enqueue a 0 None; + match propagate () with + None -> () | Some confl -> report_b_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 + + let init_solver cnf ~cnumber = + let nbv, _ = made_vars_info () in + let nbc = env.nb_init_clauses + List.length cnf in + Vec.grow_to_by_double env.vars nbv; + Iheap.grow_to_by_double env.order nbv; + List.iter + (List.iter + (fun a -> + Vec.set env.vars a.var.vid a.var; + insert_var_order a.var + ) + ) cnf; + env.nb_init_vars <- nbv; + Vec.grow_to_by_double env.model nbv; + 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 + + + let assume cnf ~cnumber = + let cnf = List.map (List.map St.add_atom) cnf in + init_solver cnf ~cnumber + + let clear () = + let empty_theory = Th.empty () in + env.is_unsat <- false; + env.unsat_core <- []; + env.clauses <- Vec.make 0 dummy_clause; + env.learnts <- Vec.make 0 dummy_clause; + env.clause_inc <- 1.; + env.var_inc <- 1.; + env.vars <- Vec.make 0 dummy_var; + env.qhead <- 0; + env.simpDB_assigns <- -1; + env.simpDB_props <- 0; + env.order <- Iheap.init 0; (* sera mis a jour dans solve *) + env.progress_estimate <- 0.; + env.restart_first <- 100; + env.starts <- 0; + env.decisions <- 0; + env.propagations <- 0; + env.conflicts <- 0; + env.clauses_literals <- 0; + env.learnts_literals <- 0; + env.max_literals <- 0; + env.tot_literals <- 0; + env.nb_init_vars <- 0; + env.nb_init_clauses <- 0; + env.tenv <- empty_theory; + env.model <- Vec.make 0 dummy_var; + env.trail <- Vec.make 601 dummy_atom; + env.trail_lim <- Vec.make 601 (-105); + env.tenv_queue <- Vec.make 100 (empty_theory); + env.tatoms_queue <- Queue.create (); + St.clear () + + + let copy (v : 'a) : 'a = Marshal.from_string (Marshal.to_string v []) 0 + + let save () = + let sv = + { env = env; + st_cpt_mk_var = !St.cpt_mk_var; + st_ma = !St.ma } + in + copy sv + + let restore { env = s_env; st_cpt_mk_var = st_cpt_mk_var; st_ma = st_ma } = + env.is_unsat <- s_env.is_unsat; + env.unsat_core <- s_env.unsat_core; + env.clauses <- s_env.clauses; + env.learnts <- s_env.learnts; + env.clause_inc <- s_env.clause_inc; + env.var_inc <- s_env.var_inc; + env.vars <- s_env.vars; + env.qhead <- s_env.qhead; + env.simpDB_assigns <- s_env.simpDB_assigns; + env.simpDB_props <- s_env.simpDB_props; + env.order <- s_env.order; + env.progress_estimate <- s_env.progress_estimate; + env.restart_first <- s_env.restart_first; + env.starts <- s_env.starts; + env.decisions <- s_env.decisions; + env.propagations <- s_env.propagations; + env.conflicts <- s_env.conflicts; + env.clauses_literals <- s_env.clauses_literals; + env.learnts_literals <- s_env.learnts_literals; + env.max_literals <- s_env.max_literals; + env.tot_literals <- s_env.tot_literals; + env.nb_init_vars <- s_env.nb_init_vars; + env.nb_init_clauses <- s_env.nb_init_clauses; + env.tenv <- s_env.tenv; + env.model <- s_env.model; + env.trail <- s_env.trail; + env.trail_lim <- s_env.trail_lim; + env.tenv_queue <- s_env.tenv_queue; + env.tatoms_queue <- s_env.tatoms_queue; + env.learntsize_factor <- s_env.learntsize_factor; + St.cpt_mk_var := st_cpt_mk_var; + St.ma := st_ma + + let eval lit = + let var, negated = make_var lit in + let truth = var.pa.is_true in + if negated then not truth else truth end diff --git a/sat/solver.mli b/sat/solver.mli index 7a12ef90..47641916 100644 --- a/sat/solver.mli +++ b/sat/solver.mli @@ -11,9 +11,10 @@ (* *) (**************************************************************************) -module Make (F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) : sig - - module St : Solver_types.S with type formula = F.t +module Make (F : Formula_intf.S) + (St : Solver_types.S with type formula = F.t) + (Ex : Explanation.S with type atom = St.atom) + (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) : sig exception Sat exception Unsat of St.clause list @@ -29,3 +30,4 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) : s val restore : state -> unit end + diff --git a/sat/solver_types.ml b/sat/solver_types.ml index 8798c752..71102786 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -21,8 +21,12 @@ let is_le n = Hstring.compare n ale = 0 let is_lt n = Hstring.compare n alt = 0 let is_gt n = Hstring.compare n agt = 0 +module type S = Solver_types_intf.S + module Make (F : Formula_intf.S) = struct +type formula = F.t + type var = { vid : int; pa : atom; @@ -35,7 +39,7 @@ type var = and atom = { var : var; - lit : F.t; + lit : formula; neg : atom; mutable watched : clause Vec.t; mutable is_true : bool; @@ -80,6 +84,7 @@ and dummy_clause = cpremise = [] } module MA = F.Map +type varmap = var MA.t let ale = Hstring.make "<=" let alt = Hstring.make "<" @@ -174,8 +179,6 @@ let clear () = cpt_mk_var := 0; ma := MA.empty -module Debug = struct - let sign a = if a==a.var.pa then "" else "-" let level a = @@ -196,25 +199,23 @@ module Debug = struct else if a.neg.is_true then sprintf ":0%s" (level a) else ":X" - let premise fmt v = + let pp_premise fmt v = List.iter (fun {name=name} -> fprintf fmt "%s," name) v - let atom fmt a = + let pp_atom fmt a = fprintf fmt "%s%d%s [lit:%a] vpremise={{%a}}" (sign a) (a.var.vid+1) (value a) F.print a.lit - premise a.var.vpremise + pp_premise a.var.vpremise - let atoms_list fmt l = List.iter (fprintf fmt "%a ; " atom) l - let atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " atom) arr + let pp_atoms_list fmt l = List.iter (fprintf fmt "%a ; " pp_atom) l + let pp_atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " pp_atom) arr - let atoms_vec fmt vec = + let pp_atoms_vec fmt vec = for i = 0 to Vec.size vec - 1 do - fprintf fmt "%a ; " atom (Vec.get vec i) + fprintf fmt "%a ; " pp_atom (Vec.get vec i) done - let clause fmt {name=name; atoms=arr; cpremise=cp} = - fprintf fmt "%s:{ %a} cpremise={{%a}}" name atoms_vec arr premise cp - -end + let pp_clause fmt {name=name; atoms=arr; cpremise=cp} = + fprintf fmt "%s:{ %a} cpremise={{%a}}" name pp_atoms_vec arr pp_premise cp end diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml index a9f25908..d339f1c2 100644 --- a/sat/solver_types_intf.ml +++ b/sat/solver_types_intf.ml @@ -48,8 +48,8 @@ module type S = sig and premise = clause list val cpt_mk_var : int ref - module Map : Map.S with type key = formula - val ma : var Map.t ref + type varmap + val ma : varmap ref val dummy_var : var val dummy_atom : atom diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml index bf851388..da38c7af 100644 --- a/sat/theory_intf.ml +++ b/sat/theory_intf.ml @@ -15,13 +15,11 @@ module type S = sig type t type formula + type explanation - module St : Solver_types.S with type formula = formula - module Ex : Explanation.S with type atom = St.atom - - exception Inconsistent of Ex.t + exception Inconsistent of explanation val empty : unit -> t - val assume : cs:bool -> formula -> Ex.t -> t -> t + val assume : cs:bool -> formula -> explanation -> t -> t end diff --git a/smt/cc.ml b/smt/cc.ml index f9cedc56..21ad9397 100644 --- a/smt/cc.ml +++ b/smt/cc.ml @@ -189,13 +189,13 @@ module Make (X : Sig.X) = struct | _ -> [] let contra_congruence = - let vrai,_ = X.make T.vrai in - let faux, _ = X.make T.faux in + let true_,_ = X.make T.true_ in + let false_, _ = X.make T.false_ in fun env r ex -> - if X.equal (fst (Uf.find_r env.uf r)) vrai then - new_facts_by_contra_congruence env r T.faux ex - else if X.equal (fst (Uf.find_r env.uf r)) faux then - new_facts_by_contra_congruence env r T.vrai ex + if X.equal (fst (Uf.find_r env.uf r)) true_ then + new_facts_by_contra_congruence env r T.false_ ex + else if X.equal (fst (Uf.find_r env.uf r)) false_ then + new_facts_by_contra_congruence env r T.true_ ex else [] let clean_use = @@ -518,7 +518,7 @@ module Make (X : Sig.X) = struct let t = { gamma = env; gamma_finite = env; choices = [] } in let t, _, _ = assume ~cs:false - (A.LT.make (A.Distinct (false, [T.vrai; T.faux]))) Ex.empty t + (A.LT.make (A.Distinct (false, [T.true_; T.false_]))) Ex.empty t in t end diff --git a/smt/literal.ml b/smt/literal.ml index ffd917c9..405cea4a 100644 --- a/smt/literal.ml +++ b/smt/literal.ml @@ -168,8 +168,8 @@ module type S_Term = sig val mk_pred : Term.t -> t - val vrai : t - val faux : t + val true_ : t + val false_ : t (* val terms_of : t -> Term.Set.t val vars_of : t -> Symbols.Set.t @@ -182,16 +182,16 @@ module LT : S_Term = struct module L = Make(Term) include L - let mk_pred t = make (Eq (t, Term.vrai) ) + let mk_pred t = make (Eq (t, Term.true_) ) - let vrai = mk_pred Term.vrai - let faux = mk_pred Term.faux + let true_ = mk_pred Term.true_ + let false_ = mk_pred Term.false_ let neg a = match view a with - | Eq(t1, t2) when Term.equal t2 Term.faux -> - make (Eq (t1, Term.vrai)) - | Eq(t1, t2) when Term.equal t2 Term.vrai -> - make (Eq (t1, Term.faux)) + | Eq(t1, t2) when Term.equal t2 Term.false_ -> + make (Eq (t1, Term.true_)) + | Eq(t1, t2) when Term.equal t2 Term.true_ -> + make (Eq (t1, Term.false_)) | _ -> L.neg a (* let terms_of a = diff --git a/smt/literal.mli b/smt/literal.mli index 773e6871..b4c3d9ef 100644 --- a/smt/literal.mli +++ b/smt/literal.mli @@ -53,8 +53,8 @@ module type S_Term = sig include S with type elt = Term.t val mk_pred : Term.t -> t - val vrai : t - val faux : t + val true_ : t + val false_ : t end diff --git a/smt/smt.ml b/smt/smt.ml index ddfbd5d5..24376c7d 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -274,8 +274,8 @@ end lift_ite sb l ty with Not_found -> raise (Error (UnknownSymb s)) - let t_true = T AETerm.vrai - let t_false = T AETerm.faux + let t_true = T AETerm.true_ + let t_false = T AETerm.false_ let rec is_int = function | T t -> AETerm.is_int t @@ -365,8 +365,8 @@ end | [f] -> print fmt f | f::l -> fprintf fmt "%a %s %a" print f sep (print_list sep) l - let f_true = Lit Literal.LT.vrai - let f_false = Lit Literal.LT.faux + let f_true = Lit Literal.LT.true_ + let f_false = Lit Literal.LT.false_ let make comb l = Comb (comb, l) @@ -565,7 +565,7 @@ end [] Ty.Tbool in incr cpt; - Literal.LT.make (Literal.Eq (t, AETerm.vrai)) + Literal.LT.make (Literal.Eq (t, AETerm.true_)) module Tseitin (Dummy : sig end)= struct let acc_or = ref [] diff --git a/smt/term.ml b/smt/term.ml index c92f597d..5c293739 100644 --- a/smt/term.ml +++ b/smt/term.ml @@ -62,8 +62,8 @@ let compare t1 t2 = let make s l ty = T.hashcons {f=s;xs=l;ty=ty;tag=0 (* dumb_value *) } -let vrai = make (Sy.True) [] Ty.Tbool -let faux = make (Sy.False) [] Ty.Tbool +let true_ = make (Sy.True) [] Ty.Tbool +let false_ = make (Sy.False) [] Ty.Tbool let int i = make (Sy.int i) [] Ty.Tint let real r = make (Sy.real r) [] Ty.Treal diff --git a/smt/term.mli b/smt/term.mli index 0274e347..9d3d39cb 100644 --- a/smt/term.mli +++ b/smt/term.mli @@ -17,8 +17,8 @@ type view = private {f: Symbols.t ; xs: t list; ty: Ty.t; tag : int} val view : t -> view val make : Symbols.t -> t list -> Ty.t -> t -val vrai : t -val faux : t +val true_ : t +val false_ : t val int : string -> t val real : string -> t