diff --git a/src/core/internal.ml b/src/core/internal.ml index 44ad3744..fdd9756d 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -464,8 +464,6 @@ module Make (* Boolean propagation. Wrapper function for adding a new propagated formula. *) let enqueue_bool a ~level:lvl reason : unit = - Log.debugf 99 "Trying to enqueue: @[%a@\n%a@]" - (fun k -> k St.pp_atom a St.pp_reason (lvl, Some reason)); if a.neg.is_true then begin Log.debugf 0 "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a); assert false @@ -523,22 +521,19 @@ module Make and a boolean stating whether it is a UIP ("Unique Implication Point") precond: the atom list is sorted by decreasing decision level *) - let backtrack_lvl ~is_uip : atom list -> int = function - | [] -> 0 - | [a] -> - assert is_uip; - 0 + let backtrack_lvl : atom list -> int * bool = function + | [] | [_] -> + 0, true | a :: b :: r -> assert(a.var.v_level > base_level ()); - if is_uip then ( + if a.var.v_level > b.var.v_level then begin (* backtrack below [a], so we can propagate [not a] *) - assert(a.var.v_level > b.var.v_level); - b.var.v_level - ) else ( + b.var.v_level, true + end else begin assert (a.var.v_level = b.var.v_level); assert (a.var.v_level >= base_level ()); - max (a.var.v_level - 1) (base_level ()) - ) + max (a.var.v_level - 1) (base_level ()), false + end (* result of conflict analysis, containing the learnt clause and some additional info. @@ -558,7 +553,7 @@ module Make atom, and perform resolution steps with each propagation reason, until the First UIP clause is found, or we get semantic propagations at the highest level (see mcsat paper for more explications). - *) + *) (* let analyze_mcsat c_clause : conflict_res = let tr_ind = ref (Vec.size env.elt_queue) in let is_uip = ref false in @@ -612,6 +607,7 @@ module Make cr_history = List.rev !history; cr_is_uip = !is_uip; } + *) let get_atom i = match Vec.get env.elt_queue i with @@ -629,7 +625,6 @@ module Make let seen = ref [] in let c = ref c_clause in let tr_ind = ref (Vec.size env.elt_queue - 1) in - let size = ref 1 in let history = ref [] in assert (decision_level () > 0); let conflict_level = @@ -660,7 +655,6 @@ module Make incr pathC; end else begin learnt := q :: !learnt; - incr size; blevel := max !blevel q.var.v_level end end @@ -682,6 +676,9 @@ module Make | 0, _ -> cond := false; learnt := p.neg :: (List.rev !learnt) + | n, Some Semantic _ -> + assert (n > 0); + learnt := p.neg :: !learnt | n, Some Bcp cl -> assert (n > 0); assert (p.var.v_level >= conflict_level); @@ -689,16 +686,21 @@ module Make | n, _ -> assert false done; List.iter (fun q -> q.var.seen <- false) !seen; - { cr_backtrack_lvl= !blevel; - cr_learnt= !learnt; - cr_history= List.rev !history; - cr_is_uip = true; + let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in + let level, is_uip = backtrack_lvl l in + { cr_backtrack_lvl = level; + cr_learnt = l; + cr_history = List.rev !history; + cr_is_uip = is_uip; } let analyze c_clause : conflict_res = + analyze_sat c_clause + (* if St.mcsat then analyze_mcsat c_clause else analyze_sat c_clause + *) (* add the learnt clause to the clause database, propagate, etc. *) let record_learnt_clause (confl:clause) (cr:conflict_res): unit = @@ -749,7 +751,7 @@ module Make (* Add a new clause, simplifying, propagating, and backtracking if the clause is false in the current trail *) let add_clause ?(force=false) (init:clause) : unit = - Log.debugf 90 "Adding clause:@[%a@]" (fun k -> k St.pp_clause init); + Log.debugf 90 "Adding clause: @[%a@]" (fun k -> k St.pp_clause init); let vec = match init.cpremise with | Hyp -> env.clauses_hyps | Local -> env.clauses_temp @@ -766,7 +768,7 @@ module Make ) else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history)) in - Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause); + Log.debugf 4 "New clause: @[%a@]" (fun k->k St.pp_clause clause); Array.iter (fun x -> insert_var_order (elt_of_var x.var)) clause.atoms; Vec.push vec clause; match atoms with diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index 4ec1f9a8..aa32b2ea 100644 --- a/src/core/solver_types.ml +++ b/src/core/solver_types.ml @@ -280,11 +280,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let pp_value fmt a = if a.is_true then - Format.fprintf fmt "[T%a]" pp_level a + Format.fprintf fmt "T%a" pp_level a else if a.neg.is_true then - Format.fprintf fmt "[F%a]" pp_level a + Format.fprintf fmt "F%a" pp_level a else - Format.fprintf fmt "[]" + Format.fprintf fmt "" let pp_premise out = function | Hyp -> Format.fprintf out "hyp" @@ -292,16 +292,19 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct | Lemma _ -> Format.fprintf out "th_lemma" | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v - let pp_assign out = function - | None -> () - | Some t -> Format.fprintf out " ->@ @[%a@]" E.Term.print t + let pp_assign fmt v = + match v.assigned with + | None -> + Format.fprintf fmt "" + | Some t -> + Format.fprintf fmt "@[@@%d->@ %a@]" v.l_level E.Term.print t let pp_lit out v = - Format.fprintf out "%d [lit:@[%a%a@]]" - (v.lid+1) E.Term.print v.term pp_assign v.assigned + Format.fprintf out "%d[%a][lit:@[%a@]]" + (v.lid+1) pp_assign v E.Term.print v.term let pp_atom out a = - Format.fprintf out "%s%d%a[atom:@[%a@]]@ " + Format.fprintf out "%s%d[%a][atom:@[%a@]]@ " (sign a) (a.var.vid+1) pp_value a E.Formula.print a.lit let pp_atoms_vec out vec = diff --git a/src/mcsat/plugin_mcsat.ml b/src/mcsat/plugin_mcsat.ml index eee5e1f0..2f17975b 100644 --- a/src/mcsat/plugin_mcsat.ml +++ b/src/mcsat/plugin_mcsat.ml @@ -150,7 +150,7 @@ let eval = function | { Expr_smt.atom = Expr_smt.Equal (a, b); sign } -> begin try let v_a, a_lvl = H.find map a in - let v_b, b_lvl = H.find map a in + let v_b, b_lvl = H.find map b in if Expr_smt.Term.equal v_a v_b then Plugin_intf.Valued(sign, max a_lvl b_lvl) else