using System.Console
using System.Text
using Nemerle.Collections
using Nemerle.Utility
using Nemerle.Logging
using Nemerle.Imperative
using Nemerle.Profiling

using MiniSatCS

set namespace Fx7

public class DPLLSolver : Solver
  [Accessor] protected core : Core
  [Accessor] protected cnf_converter : InternalCNF
  protected driver : Driver

  protected parent_asserted_literals : Hashtable [Literal, Literal] = Hashtable ()
  protected mutable inside_search = false

  protected start_time : long

  conflicts : Hashtable [list[Literal], bool] = Hashtable ()
  mutable strategies : list [int]
  mutable additional_conflicts : list [vec [Lit]] = []
  protected previous_trail : vec [Lit] = vec ()

  protected vars : vec [Var] = vec ()

  protected mutable conflicts_log : System.IO.StreamWriter

  public this (c : Core, d : Driver, par_cnf : ToCNF = null, level = 0)
    start_time = System.Environment.TickCount
    Level = level
    core = c
    driver = d
    prev_stats = Driver.StatsRec (driver)
    cnf_converter = InternalCNF (c, par_cnf, this)
    previous_trail.push (lit_Undef)
    core.PushState ()
    conflicts_log =
      if (par_cnf == null && Driver.LogConflicts != "")
        log (INFO, $ "opening conflict log file: $(Driver.LogConflicts)")
        def sw = System.IO.File.CreateText (Driver.LogConflicts)
        sw.Write ($ "; starting conflict log for $(Driver.file_name)\n")
        sw
      else null

  internal CreateVar (no : int) : void
    vars.push (no)

  protected DumpCNF (c : vec [Lit]) : void
    _ = c
    whenlogging (DPLL)
      def sb = StringBuilder ()
      foreach (l in c)
        when (sign (l))
          _ = sb.Append ("-")
        // _ = sb.Append (var (l) + 1).Append (" ")
        _ = sb.Append ("x").Append (var (l)).Append (" ")
      //log (DPLL, $ "$this CNF::: $sb 0")

  protected mutable base_bump : double = Driver.BaseBump
  protected mutable theory_bump : double = Driver.TheoryBump
  protected mutable instance_bump : double = Driver.InstanceBump

  public Level : int

  mutable current_clause_kind : ToCNF.ClauseKind

  [Profile] \
  public AddClause (kind : ToCNF.ClauseKind, c : array [SatSolver.Lit]) : void
    core.TheDriver.num_clauses++
    def bump_by =
      match (kind)
        | _ when !inside_search \
        | Init => base_bump
        | Formula \
        | Instance => instance_bump
        | TheoryConflict => theory_bump
        | Invalid => assert (false)

    def c2 = vec (c.Length)
    mutable i = 0
    def sl = Solver.Lit ()
    foreach (l in c)
      sl.x = l.val
      c2[i] = sl
      activity [var (sl)] += bump_by
      dpll_order.update (var (sl))
      i++

    when (kind is TheoryConflict as _d)
      AdditionalConflictAnalisis (c2.ToArray (), null)

    current_clause_kind = kind
    base.newClause (c2, learnt = false, copy = false, theoryClause = inside_search)
    current_clause_kind = ToCNF.ClauseKind.TheoryConflict
    foreach (c2 in additional_conflicts)
      base.newClause (c2, learnt = false, copy = false, theoryClause = inside_search)
    additional_conflicts = []
    current_clause_kind = ToCNF.ClauseKind.Invalid
    DumpCNF (c2)

  [Profile] \
  public Search (formula : Term) : bool
    assert (!inside_search)
    cnf_converter.AssertFormula (formula)
    inside_search = true
    if (!SearchNoRestarts())
      ClearState ()
      log (ANSWER, "UNSAT")
      when (Driver.Verbose)
        WriteLine ("unsatisfable")
      when (Driver.DumpImportantQuant)
        foreach (lit in core.ImportantLiterals.Keys)
          match (lit.atom)
            | q is QAtom =>
              log (INFO, $"important (pos=$(lit.IsPos)): $(q.Dump())")
            | _ => {}
      false
    else
      ClearState ()
      true 

  #pragma warning disable 10003
  DumpTrail (t : vec [Lit]) : string
    def sb = StringBuilder ()
    foreach (l in t)
      if (l == lit_Undef)
        _ = sb.Append (" ||| ")
      else
        def ll = cnf_converter.ToLiteral (index (l))
        if (ll == null)
          _ = sb.Append ($" $l ")
        else
          _ = sb.Append ($" $ll ")
    sb.ToString ()
  #pragma warning restore 10003

  CheckConflict (cnfl : list [Literal]) : void
    when (Driver.UseLevels)
      assert (! conflicts.Contains (cnfl), $ "cnfl=$cnfl $this")
      conflicts [cnfl] = true

  protected GetLiteral (l : Lit) : Literal
    def l = index (l)
    if (l >> 1 < 0) null
    else cnf_converter.ToLiteral (l)

  protected Trail (quant_only = false) : list [Literal]
    mutable res = []
    for (mutable i = previous_trail.size () - 1; i >= 0; --i)
      def l = index (previous_trail [i])
      when ((l >> 1) > 0)
        def l = cnf_converter.ToLiteral (l)
        when (l != null && (!quant_only || l.atom.IsQuantified))
          res ::= l
    res
      
  // the function in InternalCNF is public
  internal GetQMonome () : list [Literal]
    Trail (quant_only = true)

  protected ClearState () : void
    foreach (l in previous_trail)
      when (l == lit_Undef)
        core.PopState ()
    previous_trail.shrinkTo (0)

  protected override AdditionalConflictAnalisis (conflict : array [Lit], c : Clause) : void
    foreach (l in conflict)
      when (value (l) != lbool.False)
        return

    def seen = Hashtable ()
    def clauses = Queue ()
    mutable all_clauses = []

    clauses.Push (conflict)

    when (c != null)
      all_clauses ::= c

    def top_conflict = vec ()

    while (! clauses.IsEmpty)
      def clause = clauses.Take ()

      def start =
        if (clause === conflict) 0
        else 1
     
      foreach (i in [start .. clause.Length - 1])
        assert (value (clause [i]) == lbool.False)
        def v = var (clause [i])
        unless (seen.Contains (v))
          seen [v] = true
          def confl = reason [v]
          //log (TEMP, $ "consider: $v -> $confl")
          if (confl == null)
            when (level [v] != 0 && dpll_order.vars [v].round_introduced != 0)
              // log (TEMP, "skip needness")
              return // don't
            top_conflict.push (clause [i])
          else
            all_clauses ::= confl
            assert (confl [0] == ~clause [i])
            clauses.Push (confl.GetData ())

    // log (TEMP, $"do needness, $(all_clauses.Length) clauses")
    foreach (c in all_clauses)
      ClauseUsedInConflict (c)

    //def lst = $[l | l in top_conflict]
    //def cfl = $[l | l in conflict]
    //log (TEMP, $"top confl: $cfl -> $lst")

    additional_conflicts ::= top_conflict

    //current_clause_kind = ToCNF.ClauseKind.TheoryConflict
    //base.newClause (top_conflict, learnt = false, copy = false, theoryClause = inside_search)
    //current_clause_kind = ToCNF.ClauseKind.Invalid

  [Profile] \
  protected override ModelFoundCallback () : bool
    ModelFoundImpl ()

  mutable base_tableau_size = -1

  mutable last_cleanup : int
  mutable qloop : QuantLoop
  // used for 1-level sat 
  GenerateInstances () : bool
    log (TEMP, $ "inst: $(core.TheDriver.num_inst_rounds) trail=$(trail.size()) units=$n_unit_clauses")
    instance_bump *= Driver.InstanceBumpMult

    when (core.TheDriver.num_inst_rounds - last_cleanup > Driver.InstanceLife)
      last_cleanup = core.TheDriver.num_inst_rounds
      CollectGarbageClauses ()

    when (qloop == null)
      qloop = QuantLoop (this, [])
      qloop.Prepare ()
      core.TheDriver.SetQuantLimits (low = false)
      core.CurrentStrategy = 3

    if (qloop.GenerateFacts ())
      // ok, found some instantiations
      true
    else
      when (Driver.Verbose)
        System.Console.WriteLine ($"failing trail: $(Trail())")
      false

  protected ModelFoundImpl () : bool
    unless (this is QuantDPLLSolver)
      driver.MainLoopCallback ()

    theory_bump *= if (this is QuantDPLLSolver) Driver.QuantTheoryBumpMult else Driver.TheoryBumpMult

    log (DPLL, $"prev_trail: $(DumpTrail (previous_trail))")
    log (DPLL, $"trail: $(DumpTrail (trail))")

    def force_clear = 
      core.linear_theory != null && 
        Level == 0 && 
          base_tableau_size > 0 &&
            base_tableau_size * 3 < core.linear_theory.TableauSize

    //when (Level == 0)
    //  log (TEMP, $"force: $force_clear $base_tableau_size $(core.linear_theory.TableauSize)")
    
    mutable head = 0
    mutable head_j = -1
    mutable j = 0
    foreach (i in [0 .. trail.size() - 1])
      while (j < previous_trail.size () && previous_trail [j] == lit_Undef)
        head = i
        head_j = j
        j++

      if (j >= previous_trail.size ())
        break
      else if (!force_clear && previous_trail [j] == trail [i])
        j++
      else
        while (j < previous_trail.size ())
          when (previous_trail [j] == lit_Undef)
            core.PopState ()
          j++
        assert (head_j >= 0)
        if (head_j == 0)
          core.PopState ()
          core.PushState ()
          previous_trail.shrinkTo (1)
        else
          core.PopState ()
          previous_trail.shrinkTo (head_j)
        log (DPLL, $"prev_trail shrink to: $(DumpTrail(previous_trail))")

    when (force_clear)
      core.ClearTheories ()
      base_tableau_size = -1

    unless (this is QuantDPLLSolver)
      driver.total_main_monome_size += trail.size ()

    #if true
    foreach (i in $[0 .. trail.size() - 1])
      def l = cnf_converter.ToLiteral (index(trail[i]))
      when (l != null && !l.bg_asserted && !l.atom.IsQuantified && 
            !parent_asserted_literals.Contains (l))
        core.TheDriver.total_monome_size++
        when (i < head)
          core.TheDriver.DPLL_saved_monome_size++
    #endif

    when (previous_trail.last () != lit_Undef)
      previous_trail.push (lit_Undef)
      core.PushState ()
    
    trail_lim.push (trail.size ())
    
    mutable cur_level = 0
    while (trail_lim [cur_level] < head)
      cur_level++

    while (cur_level < trail_lim.size ())
      def limit = trail_lim [cur_level]
      log (DPLL, $ "lev=$(cur_level) lim=$limit h=$head")
      cur_level++
      assert (limit >= head, $ "lev=$(cur_level-1) lim=$limit h=$head")
      mutable thlits = []
      while (head < limit)
        // log (DPLL, $ "assert $head/$limit/$(trail.size())")
        def lit = cnf_converter.ToLiteral (index (trail [head]))
        when (// !dpll_order.vars [var (trail [head])].IsDontCare && // XXX this is wrong!
              lit != null && !lit.bg_asserted && 
              !parent_asserted_literals.Contains (lit))
          thlits ::= lit
        previous_trail.push (trail [head])
        head++

      //log (DPLL, $"assert: facts=$facts lim=$limit $(lits.Length) $(thlits)")
      //log (TEMP, $"GetConflicts($thlits $cur_level $(trail_lim.size()))")
      core.CurrentCnfConverter = cnf_converter
      match (if (thlits is []) [] else core.GetConflictsDPLL (thlits, cur_level >= trail_lim.size ()))
        | [] =>
          previous_trail.push (lit_Undef)
          core.PushState ()
        | cnfls =>
          def ht = Hashtable ()
          mutable res = []
          foreach (c in cnfls) 
            unless (ht.Contains (c))
              res ::= c
              ht[c] = true
          def cnfls = res
          log (DPLL, $"confls: cur_lev=$cur_level $cnfls")
          trail_lim.pop ()
          //DumpTrail()
          when (conflicts_log != null)
            def d = core.TheDriver
            def cat =
              if (this is QuantDPLLSolver) "SMALL_TH"
              else "BIG_TH  "
            foreach (c in cnfls)
              conflicts_log.Write ($ "$cat  $(d.num_main_iters)\t$(d.num_quant_iters)\t$(core.CurrentStrategy)\t$c\n")
          cnf_converter.AddConflicts (cnfls)
          foreach (c in cnfls)
            CheckConflict (c)
          return true

    trail_lim.pop ()

    when (base_tableau_size == -1 && core.linear_theory != null)
      base_tableau_size = core.linear_theory.TableauSize

    if (this is QuantDPLLSolver)
      false
    else if (!Driver.UseLevels)
      GenerateInstances ()
    else
      when (strategies == null)
        if (Driver.Strategies == null)
          if (core.SeenExplicitTriggers)
            strategies = [2]
          else
            strategies = [1, 2, 3]
          log (INFO, $ "guessing the strategy list to be: $strategies")
        else
          strategies = Driver.Strategies
          log (INFO, $ "using explicit strategy list: $strategies")

      mutable pos = 0
      def back = core.CurrentStrategy
      foreach (s in strategies)
        pos++
        when (pos > 1)
          log (INFO, $"switch to stragtegy $s")
        core.TheDriver.SetQuantLimits (low = s < 2)
        core.CurrentStrategy = s
        log (CORE, "{ start small sat")
        // log (TEMP, $"$(Trail().Map(_.ToSimplString()))")
        def smallsat = QuantDPLLSolver (this)  
        // TODO we should clean the linear solver state at this point, otherwise
        // switching is pointless
        when (!smallsat.Run ())
          // ok, it should add a conflict clause
          core.CurrentStrategy = back
          log (CORE, "stop small sat, got conflict }")
          return (true)
        log (CORE, "stop small sat, no conflict }")
      core.CurrentStrategy = back

      log (ANSWER, "SAT")

      when (Driver.Mechanical)
        // dump error variables
        def sb = System.Text.StringBuilder ("labels:")
        foreach (l in Trail ())
          def name =
            if (l.atom.term1.Arity == 0 && l.atom.term1 !== core.TermPool.True) l.atom.term1.Name
            else if (l.atom.term2 != null && l.atom.term2.Arity == 0) l.atom.term2.Name
            else null
          when (name != null &&
                ((name.StartsWith ("|EvP@") && l.IsPos) ||
                 (name.StartsWith ("|EvN@") && l.IsNeg)))
              _ = sb.Append (" ").Append (name)
        log (INFO, sb.ToString ())

      false

  #region VarOrder
  type Var = int

  mutable unit_clauses : list [NOClause] = []
  mutable n_unit_clauses : int

  protected override NewClauseCallback (c : Clause) : void
    //log (TEMP, $ "new clause: $c $(System.Environment.StackTrace)")
    dpll_order.StoreClause (c :> NOClause)
    when (c.size () == 1)
      n_unit_clauses++
      unit_clauses ::= c :> NOClause

  protected override RemoveClauseCallback (c : Clause) : void
    //log (TEMP, $ "new clause: $c $(System.Environment.StackTrace)")
    (c :> NOClause).kill_mark = true

  protected QueueCaseSplit (l : Literal) : void
    dpll_order.NeedValueFor (cnf_converter.GetLiteral (l).Var.Id)

  mutable dpll_order : NewOrder
  protected override createOrder () : VarOrder
    dpll_order = NewOrder (this)
    dpll_order

 
  // NewOrderClause
  internal class NOClause : Solver.Clause
    public mutable is_true : bool
    public mutable was_needed : bool
    public mutable is_instance : bool
    public mutable kill_mark : bool
    public round_introduced : int

    public this (c : Core, learnt : bool, ps : vec [Lit])
      base (learnt, ps)
      round_introduced = c.TheDriver.num_inst_rounds

    public MarkNeeded () : void
      was_needed = true

    public override ToString () : string
      base.ToString () + 
        $ "/is_true=$is_true,was_needed=$was_needed,is_instance=$is_instance," + \
        $ "kill_mark=$kill_mark,learnt=$(learnt()),rnd=$round_introduced"

  protected override Clause_new (learnt : bool, ps : vec [Lit]) : Clause
    def c = NOClause (core, learnt, ps)

    match (current_clause_kind)
      | _ when !inside_search \
      | Init \
      | Formula => c.MarkNeeded ()
      | Instance => c.is_instance = true
      | TheoryConflict => {}
      | Invalid => assert (learnt)

    c

  protected ClauseUsedInConflict (c : Clause) : void
    def c = c :> NOClause
    when (c.is_instance && !c.was_needed)
      //log (TEMP, $ "marking clause as needed: $c")
      c.MarkNeeded ()


  CollectGarbageClauses () : void
    cancelUntil (0)
    qloop.Restart ()

    def vars = dpll_order.vars

    // def cutoff = core.TheDriver.num_inst_rounds - Driver.InstanceLife
    def clause_alive (c : NOClause)
      !c.kill_mark && (!c.learnt () || locked (c) || c.was_needed)// || c.round_introduced > cutoff
   
    mutable alive_cnt = 0
    mutable lev0_cnt = 0
    mutable pos = 0
    foreach (v in vars)
      when (v != null)
        v.is_alive = 
          v.positive_uses.Exists (clause_alive) || \
          v.negative_uses.Exists (clause_alive)
        when (v.is_alive) alive_cnt++
        when (!v.is_alive && level [pos] == 0)
          //v.is_alive = true
          lev0_cnt++
      pos++

    mutable dst = 0
    foreach (c in learnts)
      def c = c :> NOClause
      //log (TEMP, $"consider: $c")
      assert (!c.kill_mark)
      foreach (l in c.GetData ())
        def desc = vars [var (l)]
        when (!desc.is_alive)
          assert (!c.was_needed)
          assert (!locked (c))
          c.kill_mark = true
          remove (c)
          break
      unless (c.kill_mark)
        learnts [dst] = c
        dst++

    foreach (c in unit_clauses)
      def desc = vars [var (c [0])]
      when (!desc.is_alive)
        c.kill_mark = true

    log (TEMP, $"clean up $(learnts.size()-dst) clauses, $dst left, $alive_cnt vars alive, dead at 0: $lev0_cnt")
    learnts.shrinkTo (dst)

    foreach (i in [0 .. vars.size () - 1])
      def desc = vars [i]
      desc.CollectDeadClauses (i, dpll_order)



  prev_stats : Driver.StatsRec
  public ConflictTime () : string
    def s = prev_stats
    s.MakeDelta ()
    def res = string.Format ("{0:0.00}Mcyc, ", s.tsc / 1_000_000.0) +
      $ "lev $Level, $(s.num_main_iters)/$(s.num_quant_iters) iters, $(s.num_asserts) asserts, " +
        $ "$(s.num_matchings) mtchs => $(s.instance_count) inst. in $(s.num_inst_rounds) rds"
    s.SaveNow ()
    res

  internal class NewOrder : VarOrder
    /* Invariants:
         - heap is always a heap
    */

    internal vars : vec [VarDesc] = vec ()
    mutable junk = 0
    resurrection_queue : vec [Var] = vec ()
    par : DPLLSolver

    
    internal class VarDesc
      internal mutable positive_uses : list [NOClause] = []
      internal mutable negative_uses : list [NOClause] = []
      internal mutable deadly_clauses : list [NOClause] = null
      internal mutable positive_use_count : int
      internal mutable negative_use_count : int
      internal mutable always_valuate : bool
      internal mutable is_alive : bool

      //  0 - no position
      // -n - asserted to be false at trail [n-1]
      //  n - asserted to be true at trail [n-1]
      internal mutable trail_position : int 

      internal round_introduced : int

      internal IsDead : bool
        get
          !always_valuate && negative_use_count == 0 && positive_use_count == 0

      internal this (par : NewOrder)
        round_introduced = par.par.core.TheDriver.num_inst_rounds

      #if false
      internal IsDontCare : bool
        get
          positive_uses is [] && negative_uses is []

      internal Validate (v : Var, par : NewOrder) : void
        def num_uses (clauses)
          mutable cnt = 0
          foreach (c in clauses)
            outer:
              if (c.is_true)
                foreach (l in c.lits)
                  when (par.par.value (l) == Solver.lbool.True)
                    outer ()
                assert (false)
              else cnt++
          cnt
       
        when (trail_position == 0)
          def real_pos = num_uses (positive_uses)
          def real_neg = num_uses (negative_uses)

          log (DPLLO, $ "pos: pos=$(positive_uses) neg=$(negative_uses) $real_pos/$positive_use_count $real_neg/$negative_use_count $(par.par.value(v))")

          assert (real_pos == positive_use_count, $"for $v")
          assert (real_neg == negative_use_count, $"for $v")
      #endif


      internal Set (par : NewOrder, v : Var, pos : int) : void
        assert (trail_position == 0)
        assert (!IsDead)
        trail_position = pos
        par.Kill (v)
        def uses = if (pos > 0) positive_uses else negative_uses
        deadly_clauses = []
        foreach (c when !c.is_true in uses)
          c.is_true = true
          deadly_clauses ::= c
          foreach (l in c.GetData ())
            def desc = par.vars [var (l)]
            if (sign (l)) desc.negative_use_count--
            else desc.positive_use_count--
            when (desc.IsDead && desc.trail_position == 0)
              par.Kill (var (l))

      internal static ClauseFalse (par : NewOrder, c : NOClause) : void
        c.is_true = false
        foreach (l in c.GetData ())
          def desc = par.vars [var (l)]
          when (desc.trail_position == 0 && desc.IsDead)
            par.Resurrect (var (l))
          if (sign (l)) desc.negative_use_count++
          else desc.positive_use_count++

      internal CollectDeadClauses (v : Var, par : NewOrder) : void
        def was_dead = IsDead

        foreach (c in positive_uses)
          when (!c.is_true && c.kill_mark)
            positive_use_count--

        foreach (c in negative_uses)
          when (!c.is_true && c.kill_mark)
            negative_use_count--

        def aint_killed (c)
          !c.kill_mark

        positive_uses = positive_uses.Filter (aint_killed)
        negative_uses = negative_uses.Filter (aint_killed)
        when (deadly_clauses != null)
          deadly_clauses = deadly_clauses.Filter (aint_killed)

        when (! is_alive)
          assert (IsDead)
          assert (positive_uses is [], $ "$v -> $positive_uses")
          assert (negative_uses is [], $ "$v -> $negative_uses")
          assert (deadly_clauses == null || deadly_clauses is [])

        when (trail_position == 0 && !was_dead && IsDead)
          par.Kill (v)

      internal Undo (par : NewOrder, var : Var) : void
        when (trail_position != 0)
          trail_position = 0
          par.Resurrect (var)
          foreach (c in deadly_clauses)
            ClauseFalse (par, c)
          deadly_clauses = null

    internal NeedValueFor (v : Var) : void
      def desc = vars [v]
      //log (TEMP, $ "need value for: $v $(par.cnf_converter.ToLiteral (v * 2)), dead=$(desc.IsDead), pos=$(desc.trail_position)")
      when (desc.IsDead && desc.trail_position == 0)
        Resurrect (v)
      vars [v].always_valuate = true
      activity [v] += par.instance_bump * 5

    internal StoreClause (c : NOClause) : void
      def lits = c.GetData ()
      mutable min_true = int.MaxValue
      mutable min_desc
      c.is_true = true
      foreach (l in lits)
        def desc = vars [var (l)]
        def cand =
          if (sign (l) && desc.trail_position < 0)
            -desc.trail_position
          else if (!sign (l) && desc.trail_position > 0)
            desc.trail_position
          else min_true
        if (sign (l))
          desc.negative_uses ::= c
        else
          desc.positive_uses ::= c
        when (cand < min_true)
          min_true = cand
          min_desc = desc

      if (min_desc != null)
        min_desc.deadly_clauses ::= c
      else
        VarDesc.ClauseFalse (this, c)
    
    InHeap (v : Var) : bool
      v < heap.indices.size () && heap.inHeap (v)

    Kill (v : Var) : void
      when (InHeap (v))
        junk++

    Resurrect (v : Var) : void
      if (InHeap (v))
        junk--
      else
        resurrection_queue.push (v)

    [Profile] \
    Rebuild () : void
      log (DPLLO, $"rebuild the heap (junk=$junk, resq=$(resurrection_queue.size()), heap=$(heap.heap.size())")
      // rebuild the heap
      mutable dst = 1
      foreach (i in [1 .. heap.heap.size () - 1])
        def v = heap.heap [i]
        log (DPLLO, $"from heap $v")
        def desc = vars [v]
        if (desc.trail_position != 0 || desc.IsDead)
          heap.indices [v] = 0
        else
          heap.heap [dst] = v
          heap.indices [v] = dst
          dst++
      heap.heap.growTo (dst + resurrection_queue.size () + 1)
      foreach (v in resurrection_queue)
        log (DPLLO, $"from queue $v $(heap.indices.size())")
        heap.indices [v] = dst
        heap.heap [dst] = v
        dst++
      log (DPLLO, $"shrink to $dst")
      heap.heap.shrinkTo (dst)
      dst /= 2
      while (dst >= 1)
        heap.percolateDown (dst)
        dst--
      junk = 0

    // takes care of the queues, by either executing them, or rebuilding the heap altogether
    [Profile] \
    Prep () : void
      if (resurrection_queue.size () + junk > heap.heap.size () - junk)
        Rebuild ()
      else
        log (DPLLO, "insert stuff")
        foreach (v in resurrection_queue)
          when (!InHeap (v))
            heap.insert (v)

      resurrection_queue.shrinkTo (0)

    [Profile] \
    public override undo (v : Var) : void
      when (vars [v] != null)
        vars [v].Undo (this, v)

    [Profile] \
    public override update (v : Var) : void
      // otherwise it should sit in the resurection queue
      when (InHeap (v))
        heap.increase (v)

    public override newVar () : void
      def v = assigns.size () - 1
      assert (v == vars.size ())
      vars.push (VarDesc (this))
      heap.setBounds (v+1)
      resurrection_queue.push (v)

    [Profile] \
    public override select (rand_freq : double) : Lit
      mutable i 
      log (DPLLO, "select")
      def trail = par.trail
      for (i = trail.size () - 1; i >= 0; i--)
        log (DPLLO, $"at $i check $(trail[i])/$(var(trail[i])) vars.size = $(vars.size())")
        when (vars [var (trail [i])].trail_position != 0) break
      for (i++; i < trail.size (); i++)
        log (DPLLO, $"xat $i check $(trail[i]) vars.size = $(vars.size())")
        def v = var (trail [i])
        def pos = if (sign (trail [i])) -(i+1) else i+1
        vars [v].Set (this, v, pos)

      log (DPLLO, "prep")
      Prep ()

      while (!heap.empty ())
        def v = 
          if (par.core.Rand ((1 / rand_freq) :> int) == 0)
            heap.heap [par.core.Rand (heap.heap.size ())]
          else heap.getmin ()
        log (DPLLO, $"check $v")
        def desc = vars [v]
        // desc.Validate (v, this)
        when (desc.trail_position != 0) assert (!isUndef (assigns [v]))
        when (desc.trail_position == 0 && !desc.IsDead)
          if (desc.negative_use_count > 0)
            return Lit (v, true)
          else if (desc.positive_use_count > 0)
            return Lit (v, false)
          else
            return Lit (v, true)

      lit_Undef

    public this (par : DPLLSolver)
      this.par = par
      base (par.assigns, par.activity)
  #endregion