src/Tools/Argo/argo_cdcl.ML
author boehmes
Thu Sep 29 20:54:44 2016 +0200 (2016-09-29)
changeset 63960 3daf02070be5
permissions -rw-r--r--
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
     1 (*  Title:      Tools/Argo/argo_cdcl.ML
     2     Author:     Sascha Boehme
     3 
     4 Propositional satisfiability solver in the style of conflict-driven
     5 clause-learning (CDCL). It features:
     6 
     7  * conflict analysis and clause learning based on the first unique implication point
     8  * nonchronological backtracking
     9  * dynamic variable ordering (VSIDS)
    10  * restarting
    11  * polarity caching
    12  * propagation via two watched literals
    13  * special propagation of binary clauses 
    14  * minimizing learned clauses
    15  * support for external knowledge
    16 
    17 These features might be added:
    18 
    19  * pruning of unnecessary learned clauses
    20  * rebuilding the variable heap
    21  * aligning the restart level with the decision heuristics: keep decisions that would
    22    be recovered instead of backjumping to level 0
    23 
    24 The implementation is inspired by:
    25 
    26   Niklas E'en and Niklas S"orensson. An Extensible SAT-solver. In Enrico
    27   Giunchiglia and Armando Tacchella, editors, Theory and Applications of
    28   Satisfiability Testing. Volume 2919 of Lecture Notes in Computer
    29   Science, pages 502-518. Springer, 2003.
    30 
    31   Niklas S"orensson and Armin Biere. Minimizing Learned Clauses. In
    32   Oliver Kullmann, editor, Theory and Applications of Satisfiability
    33   Testing. Volume 5584 of Lecture Notes in Computer Science,
    34   pages 237-243. Springer, 2009.
    35 *)
    36 
    37 signature ARGO_CDCL =
    38 sig
    39   (* types *)
    40   type 'a explain = Argo_Lit.literal -> 'a -> Argo_Cls.clause * 'a
    41 
    42   (* context *)
    43   type context
    44   val context: context
    45   val assignment_of: context -> Argo_Lit.literal -> bool option
    46 
    47   (* enriching the context *)
    48   val add_atom: Argo_Term.term -> context -> context
    49   val add_axiom: Argo_Cls.clause -> context -> int * context
    50 
    51   (* main operations *)
    52   val assume: 'a explain -> Argo_Lit.literal -> context -> 'a ->
    53     Argo_Cls.clause option * context * 'a
    54   val propagate: context -> Argo_Common.literal Argo_Common.implied * context
    55   val decide: context -> context option
    56   val analyze: 'a explain -> Argo_Cls.clause -> context -> 'a -> int * context * 'a
    57   val restart: context -> int * context
    58 end
    59 
    60 structure Argo_Cdcl: ARGO_CDCL =
    61 struct
    62 
    63 (* basic types and operations *)
    64 
    65 type 'a explain = Argo_Lit.literal -> 'a -> Argo_Cls.clause * 'a
    66 
    67 datatype reason =
    68   Level0 of Argo_Proof.proof |
    69   Decided of int * int * (bool * reason) Argo_Termtab.table |
    70   Implied of int * int * (Argo_Lit.literal * reason) list * Argo_Proof.proof |
    71   External of int
    72 
    73 fun level_of (Level0 _) = 0
    74   | level_of (Decided (l, _, _)) = l
    75   | level_of (Implied (l, _, _, _)) = l
    76   | level_of (External l) = l
    77 
    78 type justified = Argo_Lit.literal * reason
    79 
    80 type watches = Argo_Cls.clause list * Argo_Cls.clause list
    81 
    82 fun get_watches wts t = Argo_Termtab.lookup wts t
    83 fun map_watches f t wts = Argo_Termtab.map_default (t, ([], [])) f wts
    84 
    85 fun map_lit_watches f (Argo_Lit.Pos t) = map_watches (apsnd f) t
    86   | map_lit_watches f (Argo_Lit.Neg t) = map_watches (apfst f) t
    87 
    88 fun watches_of wts (Argo_Lit.Pos t) = (case get_watches wts t of SOME (ws, _) => ws | NONE => [])
    89   | watches_of wts (Argo_Lit.Neg t) = (case get_watches wts t of SOME (_, ws) => ws | NONE => [])
    90 
    91 fun attach cls lit = map_lit_watches (cons cls) lit
    92 fun detach cls lit = map_lit_watches (remove Argo_Cls.eq_clause cls) lit
    93 
    94 
    95 (* literal values *)
    96 
    97 fun raw_val_of vals lit = Argo_Termtab.lookup vals (Argo_Lit.term_of lit)
    98 
    99 fun val_of vals (Argo_Lit.Pos t) = Argo_Termtab.lookup vals t
   100   | val_of vals (Argo_Lit.Neg t) = Option.map (apfst not) (Argo_Termtab.lookup vals t)
   101 
   102 fun value_of vals (Argo_Lit.Pos t) = Option.map fst (Argo_Termtab.lookup vals t)
   103   | value_of vals (Argo_Lit.Neg t) = Option.map (not o fst) (Argo_Termtab.lookup vals t)
   104 
   105 fun justified vals lit = Option.map (pair lit o snd) (raw_val_of vals lit)
   106 fun the_reason_of vals lit = snd (the (raw_val_of vals lit))
   107 
   108 fun assign (Argo_Lit.Pos t) r = Argo_Termtab.update (t, (true, r))
   109   | assign (Argo_Lit.Neg t) r = Argo_Termtab.update (t, (false, r))
   110 
   111 
   112 (* context *)
   113 
   114 type trail = int * justified list (* the trail height and the sequence of assigned literals *)
   115 
   116 type context = {
   117   units: Argo_Common.literal list, (* the literals that await propagation *)
   118   level: int, (* the decision level *)
   119   trail: int * justified list, (* the trail height and the sequence of assigned literals *)
   120   vals: (bool * reason) Argo_Termtab.table, (* mapping of terms to polarity and reason *)
   121   wts: watches Argo_Termtab.table, (* clauses watched by terms *)
   122   heap: Argo_Heap.heap, (* max-priority heap for decision heuristics *)
   123   clss: Argo_Cls.table, (* information about clauses *)
   124   prf: Argo_Proof.context} (* the proof context *)
   125 
   126 fun mk_context units level trail vals wts heap clss prf: context =
   127   {units=units, level=level, trail=trail, vals=vals, wts=wts, heap=heap, clss=clss, prf=prf}
   128 
   129 val context =
   130   mk_context [] 0 (0, []) Argo_Termtab.empty Argo_Termtab.empty Argo_Heap.heap
   131     Argo_Cls.table Argo_Proof.cdcl_context
   132 
   133 fun drop_levels n (Decided (l, h, vals)) trail heap =
   134       if l = n + 1 then ((h, trail), vals, heap) else drop_literal n trail heap
   135   | drop_levels n _ tr heap = drop_literal n tr heap
   136 
   137 and drop_literal n ((lit, r) :: trail) heap = drop_levels n r trail (Argo_Heap.insert lit heap)
   138   | drop_literal _ [] _ = raise Fail "bad trail"
   139 
   140 fun backjump_to new_level (cx as {level, trail=(_, tr), wts, heap, clss, prf, ...}: context) =
   141   if new_level >= level then (0, cx)
   142   else
   143     let val (trail, vals, heap) = drop_literal (Integer.max 0 new_level) tr heap
   144     in (level - new_level, mk_context [] new_level trail vals wts heap clss prf) end
   145 
   146 
   147 (* proofs *)
   148 
   149 fun tag_clause (lits, p) prf = Argo_Proof.mk_clause lits p prf |>> pair lits
   150 
   151 fun level0_unit_proof (lit, Level0 p') (p, prf) = Argo_Proof.mk_unit_res lit p p' prf
   152   | level0_unit_proof _ _ = raise Fail "bad reason"
   153 
   154 fun level0_unit_proofs lrs p prf = fold level0_unit_proof lrs (p, prf)
   155 
   156 fun unsat ({vals, prf, ...}: context) (lits, p) =
   157   let val lrs = map (fn lit => (lit, the_reason_of vals lit)) lits
   158   in Argo_Proof.unsat (fst (level0_unit_proofs lrs p prf)) end
   159 
   160 
   161 (* literal operations *)
   162 
   163 fun push lit p reason prf ({units, level, trail=(h, tr), vals, wts, heap, clss, ...}: context) =
   164   let val vals = assign lit reason vals
   165   in mk_context ((lit, p) :: units) level (h + 1, (lit, reason) :: tr) vals wts heap clss prf end
   166 
   167 fun push_level0 lit p lrs (cx as {prf, ...}: context) =
   168   let val (p, prf) = level0_unit_proofs lrs p prf
   169   in push lit (SOME p) (Level0 p) prf cx end
   170 
   171 fun push_implied lit p lrs (cx as {level, trail=(h, _), prf, ...}: context) =
   172   if level > 0 then push lit NONE (Implied (level, h, lrs, p)) prf cx
   173   else push_level0 lit p lrs cx
   174 
   175 fun push_decided lit (cx as {level, trail=(h, _), vals, prf, ...}: context) =
   176   push lit NONE (Decided (level, h, vals)) prf cx
   177 
   178 fun assignment_of ({vals, ...}: context) = value_of vals
   179 
   180 fun replace_watches old new cls ({units, level, trail, vals, wts, heap, clss, prf}: context) =
   181   mk_context units level trail vals (attach cls new (detach cls old wts)) heap clss prf
   182 
   183 
   184 (* clause operations *)
   185 
   186 fun as_clause cls ({units, level, trail, vals, wts, heap, clss, prf}: context) =
   187   let val (cls, prf) = tag_clause cls prf
   188   in (cls, mk_context units level trail vals wts heap clss prf) end
   189 
   190 fun note_watches ([_, _], _) _ clss = clss
   191   | note_watches cls lp clss = Argo_Cls.put_watches cls lp clss
   192 
   193 fun attach_clause lit1 lit2 (cls as (lits, _)) cx =
   194   let
   195     val {units, level, trail, vals, wts, heap, clss, prf}: context = cx
   196     val wts = attach cls lit1 (attach cls lit2 wts)
   197     val clss = note_watches cls (lit1, lit2) clss
   198   in mk_context units level trail vals wts (fold Argo_Heap.count lits heap) clss prf end
   199 
   200 fun change_watches _ (false, _, _) cx = cx
   201   | change_watches cls (true, l1, l2) ({units, level, trail, vals, wts, heap, clss, prf}: context) =
   202       mk_context units level trail vals wts heap (Argo_Cls.put_watches cls (l1, l2) clss) prf
   203 
   204 fun add_asserting lit lit' (cls as (_, p)) lrs cx =
   205   attach_clause lit lit' cls (push_implied lit p lrs cx)
   206 
   207 (*
   208   When learning a non-unit clause, the context is backtracked to the highest decision level
   209   of the assigned literals.
   210 *)
   211 
   212 fun learn_clause _ ([lit], p) cx = backjump_to 0 cx ||> push_level0 lit p []
   213   | learn_clause lrs (cls as (lits, _)) cx =
   214       let
   215         fun max_level (l, r) (ll as (_, lvl)) = if level_of r > lvl then (l, level_of r) else ll
   216         val (lit, lvl) = fold max_level lrs (hd lits, 0)
   217       in backjump_to lvl cx ||> add_asserting (hd lits) lit cls lrs end
   218 
   219 (*
   220   An axiom with one unassigned literal and all remaining literals being assigned to
   221   false is asserting. An axiom with all literals assigned to false on level 0 makes the
   222   context unsatisfiable. An axiom with all literals assigned to false on higher levels
   223   causes backjumping before the highest level, and then the axiom might be asserting if
   224   only one literal is unassigned on that level.
   225 *)
   226 
   227 fun min lit i NONE = SOME (lit, i)
   228   | min lit i (SOME (lj as (_, j))) = SOME (if i < j then (lit, i) else lj)
   229 
   230 fun level_ord ((_, r1), (_, r2)) = int_ord (level_of r2, level_of r1)
   231 fun add_max lr lrs = Ord_List.insert level_ord lr lrs
   232 
   233 fun part [] [] t us fs = (t, us, fs)
   234   | part (NONE :: vs) (l :: ls) t us fs = part vs ls t (l :: us) fs
   235   | part (SOME (true, r) :: vs) (l :: ls) t us fs = part vs ls (min l (level_of r) t) us fs
   236   | part (SOME (false, r) :: vs) (l :: ls) t us fs = part vs ls t us (add_max (l, r) fs)
   237   | part _ _ _ _ _ = raise Fail "mismatch between values and literals"
   238 
   239 fun backjump_add (lit, r) (lit', r') cls lrs cx =
   240   let
   241     val add =
   242       if level_of r = level_of r' then attach_clause lit lit' cls
   243       else add_asserting lit lit' cls lrs
   244   in backjump_to (level_of r - 1) cx ||> add end
   245 
   246 fun analyze_axiom vs (cls as (lits, p), cx) =
   247   (case part vs lits NONE [] [] of
   248     (SOME (lit, lvl), [], []) =>
   249       if lvl > 0 then backjump_to 0 cx ||> push_implied lit p [] else (0, cx)
   250   | (SOME (lit, lvl), [], (lit', _) :: _) => (0, cx |> (lvl > 0) ? attach_clause lit lit' cls)
   251   | (SOME (lit, lvl), lit' :: _, _) => (0, cx |> (lvl > 0) ? attach_clause lit lit' cls)
   252   | (NONE, [], (_, Level0 _) :: _) => unsat cx cls
   253   | (NONE, [], [(lit, _)]) => backjump_to 0 cx ||> push_implied lit p []
   254   | (NONE, [], lrs as (lr :: lr' :: _)) => backjump_add lr lr' cls lrs cx
   255   | (NONE, [lit], []) => backjump_to 0 cx ||> push_implied lit p []
   256   | (NONE, [lit], lrs as (lit', _) :: _) => (0, add_asserting lit lit' cls lrs cx)
   257   | (NONE, lit1 :: lit2 :: _, _) => (0, attach_clause lit1 lit2 cls cx)
   258   | _ => raise Fail "bad clause")
   259 
   260 
   261 (* enriching the context *)
   262 
   263 fun add_atom t ({units, level, trail, vals, wts, heap, clss, prf}: context) =
   264   let val heap = Argo_Heap.insert (Argo_Lit.Pos t) heap
   265   in mk_context units level trail vals wts heap clss prf end
   266 
   267 fun add_axiom ([], p) _ = Argo_Proof.unsat p
   268   | add_axiom (cls as (lits, _)) (cx as {vals, ...}: context) =
   269       if has_duplicates Argo_Lit.eq_lit lits then raise Fail "clause with duplicate literals"
   270       else if has_duplicates Argo_Lit.dual_lit lits then (0, cx)
   271       else analyze_axiom (map (val_of vals) lits) (as_clause cls cx)
   272 
   273 
   274 (* external knowledge *)
   275 
   276 fun assume explain lit (cx as {level, vals, prf, ...}: context) x =
   277   (case value_of vals lit of
   278     SOME true => (NONE, cx, x)
   279   | SOME false => 
   280       let val (cls, x) = explain lit x
   281       in if level = 0 then unsat cx cls else (SOME cls, cx, x) end
   282   | NONE =>
   283       if level = 0 then
   284         let val ((lits, p), x) = explain lit x
   285         in (NONE, push_level0 lit p (map_filter (justified vals) lits) cx, x) end
   286       else (NONE, push lit NONE (External level) prf cx, x))
   287 
   288 
   289 (* propagation *)
   290 
   291 exception CONFLICT of Argo_Cls.clause * context
   292 
   293 fun order_lits_by lit (l1, l2) =
   294   if Argo_Lit.eq_id (l1, lit) then (true, l2, l1) else (false, l1, l2)
   295 
   296 fun prop_binary (_, implied_lit, other_lit) (cls as (_, p)) (cx as {level, vals, ...}: context) =
   297   (case value_of vals implied_lit of
   298     NONE => push_implied implied_lit p [(other_lit, the_reason_of vals other_lit)] cx
   299   | SOME true => cx
   300   | SOME false => if level = 0 then unsat cx cls else raise CONFLICT (cls, cx))
   301 
   302 datatype next = Lit of Argo_Lit.literal | None of justified list
   303 
   304 fun with_non_false f l (SOME (false, r)) lrs = f ((l, r) :: lrs)
   305   | with_non_false _ l _ _ = Lit l
   306 
   307 fun first_non_false _ _ [] lrs = None lrs
   308   | first_non_false vals lit (l :: ls) lrs =
   309       if Argo_Lit.eq_lit (l, lit) then first_non_false vals lit ls lrs
   310       else with_non_false (first_non_false vals lit ls) l (val_of vals l) lrs
   311 
   312 fun prop_nary (lp as (_, lit1, lit2)) (cls as (lits, p)) (cx as {level, vals, ...}: context) =
   313   let val v = value_of vals lit1
   314   in
   315     if v = SOME true then change_watches cls lp cx
   316     else
   317       (case first_non_false vals lit1 lits [] of
   318         Lit lit2' => change_watches cls (true, lit1, lit2') (replace_watches lit2 lit2' cls cx)
   319       | None lrs =>
   320           if v = NONE then push_implied lit1 p lrs (change_watches cls lp cx)
   321           else if level = 0 then unsat cx cls
   322           else raise CONFLICT (cls, change_watches cls lp cx))
   323   end
   324 
   325 fun prop_cls lit (cls as ([l1, l2], _)) cx = prop_binary (order_lits_by lit (l1, l2)) cls cx
   326   | prop_cls lit cls (cx as {clss, ...}: context) =
   327       prop_nary (order_lits_by lit (Argo_Cls.get_watches clss cls)) cls cx
   328 
   329 fun prop_lit (lp as (lit, _)) (lps, cx as {wts, ...}: context) =
   330   (lp :: lps, fold (prop_cls lit) (watches_of wts lit) cx)
   331 
   332 fun prop lps (cx as {units=[], ...}: context) = (Argo_Common.Implied (rev lps), cx)
   333   | prop lps ({units, level, trail, vals, wts, heap, clss, prf}: context) =
   334       fold_rev prop_lit units (lps, mk_context [] level trail vals wts heap clss prf) |-> prop
   335 
   336 fun propagate cx = prop [] cx
   337   handle CONFLICT (cls, cx) => (Argo_Common.Conflict cls, cx)
   338 
   339 
   340 (* decisions *)
   341 
   342 (*
   343   Decisions are based on an activity heuristics. The most active variable that is
   344   still unassigned is chosen.
   345 *)
   346 
   347 fun decide ({units, level, trail, vals, wts, heap, clss, prf}: context) =
   348   let
   349     fun check NONE = NONE
   350       | check (SOME (lit, heap)) =
   351           if Argo_Termtab.defined vals (Argo_Lit.term_of lit) then check (Argo_Heap.extract heap)
   352           else SOME (push_decided lit (mk_context units (level + 1) trail vals wts heap clss prf))
   353   in check (Argo_Heap.extract heap) end
   354 
   355 
   356 (* conflict analysis and clause learning *)
   357 
   358 (*
   359   Learned clauses often contain literals that are redundant, because they are
   360   subsumed by other literals of the clause. By analyzing the implication graph beyond
   361   the unique implication point, such redundant literals can be identified and hence
   362   removed from the learned clause. Only literals occurring in the learned clause and
   363   their reasons need to be analyzed.
   364 *)
   365 
   366 exception ESSENTIAL of unit
   367 
   368 fun history_ord ((h1, lit1, _), (h2, lit2, _)) =
   369   if h1 < 0 andalso h2 < 0 then int_ord (apply2 Argo_Lit.signed_id_of (lit1, lit2))
   370   else int_ord (h2, h1)
   371 
   372 fun rec_redundant stop (lit, Implied (lvl, h, lrs, p)) lps =
   373       if stop lit lvl then lps
   374       else fold (rec_redundant stop) lrs ((h, lit, p) :: lps)
   375   | rec_redundant stop (lit, Decided (lvl, _, _)) lps =
   376       if stop lit lvl then lps
   377       else raise ESSENTIAL ()
   378   | rec_redundant _ (lit, Level0 p) lps = ((~1, lit, p) :: lps)
   379   | rec_redundant _ _ _ = raise ESSENTIAL ()
   380 
   381 fun redundant stop (lr as (lit, Implied (_, h, lrs, p))) (lps, essential_lrs) = (
   382       (fold (rec_redundant stop) lrs ((h, lit, p) :: lps), essential_lrs)
   383       handle ESSENTIAL () => (lps, lr :: essential_lrs))
   384   | redundant _ lr (lps, essential_lrs) = (lps, lr :: essential_lrs)
   385 
   386 fun resolve_step (_, l, p') (p, prf) = Argo_Proof.mk_unit_res l p p' prf
   387 
   388 fun reduce lrs p prf =
   389   let
   390     val lits = map fst lrs
   391     val levels = fold (insert (op =) o level_of o snd) lrs []
   392     fun stop lit level =
   393       if member Argo_Lit.eq_lit lits lit then true
   394       else if member (op =) levels level then false
   395       else raise ESSENTIAL ()
   396 
   397     val (lps, lrs) = fold (redundant stop) lrs ([], [])
   398   in (lrs, fold resolve_step (sort_distinct history_ord lps) (p, prf)) end
   399 
   400 (*
   401   Literals that are candidates for the learned lemma are marked and unmarked while
   402   traversing backwards through the trail. The last remaining marked literal is the first
   403   unique implication point.
   404 *)
   405 
   406 fun unmark lit ms = remove Argo_Lit.eq_id lit ms
   407 fun marked ms lit = member Argo_Lit.eq_id ms lit
   408 
   409 (*
   410   Whenever an implication is recorded, the reason for the false literals of the
   411   asserting clause are known. It is reasonable to store this justification list as part
   412   of the implication reason. Consequently, the implementation of conflict analysis can
   413   benefit from this information, which does not need to be re-computed here.
   414 *)
   415 
   416 fun justification_for _ _ _ (Implied (_, _, lrs, p)) x = (lrs, p, x)
   417   | justification_for explain vals lit (External _) x =
   418       let val ((lits, p), x) = explain lit x
   419       in (map_filter (justified vals) lits, p, x) end
   420   | justification_for _ _ _ _ _ = raise Fail "bad reason"
   421 
   422 fun first_lit pred ((lr as (lit, _)) :: lrs) = if pred lit then (lr, lrs) else first_lit pred lrs
   423   | first_lit _ _ = raise Empty
   424 
   425 (*
   426   Beginning from the conflicting clause, the implication graph is traversed to the first
   427   unique implication point. This breadth-first search is controlled by the topological order of
   428   the trail, which is traversed backwards. While traversing through the trail, the conflict
   429   literals of lower levels are collected to form the conflict lemma together with the unique
   430   implication point. Conflict literals assigned on level 0 are excluded from the conflict lemma.
   431   Conflict literals assigned on the current level are candidates for the first unique
   432   implication point.
   433 *)
   434 
   435 fun analyze explain cls (cx as {level, trail, vals, wts, heap, clss, prf, ...}: context) x =
   436   let
   437     fun from_clause [] trail ms lrs h p prf x =
   438           from_trail (first_lit (marked ms) trail) ms lrs h p prf x
   439       | from_clause ((lit, r) :: clause_lrs) trail ms lrs h p prf x =
   440           from_reason r lit clause_lrs trail ms lrs h p prf x
   441  
   442     and from_reason (Level0 p') lit clause_lrs trail ms lrs h p prf x =
   443           let val (p, prf) = Argo_Proof.mk_unit_res lit p p' prf
   444           in from_clause clause_lrs trail ms lrs h p prf x end
   445       | from_reason r lit clause_lrs trail ms lrs h p prf x =
   446           if level_of r = level then
   447             if marked ms lit then from_clause clause_lrs trail ms lrs h p prf x
   448             else from_clause clause_lrs trail (lit :: ms) lrs (Argo_Heap.increase lit h) p prf x
   449           else
   450             let
   451               val (lrs, h) =
   452                 if AList.defined Argo_Lit.eq_id lrs lit then (lrs, h)
   453                 else ((lit, r) :: lrs, Argo_Heap.increase lit h)
   454             in from_clause clause_lrs trail ms lrs h p prf x end
   455 
   456     and from_trail ((lit, _), _) [_] lrs h p prf x =
   457           let val (lrs, (p, prf)) = reduce lrs p prf
   458           in (Argo_Lit.negate lit :: map fst lrs, lrs, h, p, prf, x) end
   459       | from_trail ((lit, r), trail) ms lrs h p prf x =
   460           let
   461             val (clause_lrs, p', x) = justification_for explain vals lit r x
   462             val (p, prf) = Argo_Proof.mk_unit_res lit p' p prf
   463           in from_clause clause_lrs trail (unmark lit ms) lrs h p prf x end
   464 
   465     val (ls, p) = cls
   466     val lrs = if level = 0 then unsat cx cls else map (fn l => (l, the_reason_of vals l)) ls
   467     val (lits, lrs, heap, p, prf, x) = from_clause lrs (snd trail) [] [] heap p prf x
   468     val heap = Argo_Heap.decay heap
   469     val (levels, cx) = learn_clause lrs (lits, p) (mk_context [] level trail vals wts heap clss prf)
   470   in (levels, cx, x) end
   471 
   472 
   473 (* restarting *)
   474 
   475 fun restart cx = backjump_to 0 cx
   476 
   477 end