using Nemerle.Utility
using Nemerle.Collections
using Nemerle.Logging
using Nemerle.Profiling
using Nemerle.Imperative

using System.IO
using System.Text

set namespace Fx7

//#define CLAUSE_DUMP

abstract public class ToCNF
  type Lit = SatSolver.Lit
  public type BitVec = System.Collections.BitArray
  public enum ClauseKind
    | Init
    | Formula // formula clauses added during search are also instances
    | Instance
    | TheoryConflict
    | Invalid

  protected core : Core
  protected parent : ToCNF

  and_cache : Hashtable [list [int], Lit] = Hashtable ()
  or_cache : Hashtable [list [int], Lit] = Hashtable ()
  formula_cache : Hashtable [Term, Lit] = Hashtable ()

  real_atom_term_cache : Hashtable [Term, Atom] = Hashtable ()

  // this is stright level one cache
  atom_term_cache : Hashtable [Term, Lit] = Hashtable ()
  // this contains simplified terms
  atom_cache : Hashtable [Atom, Lit] = Hashtable ()
  
  terms_for_atom : Hashtable [Atom, list [Term]] = Hashtable ()
  // reverse of atom_cache
  mutable atom_rev_cache : array [Atom] = array (200)

  ite_expanded : Hashtable [Term, Term] = Hashtable ()

  mutable add_explanation = false
  mutable true_literal : Lit

  [Accessor] \
  mutable var_count : int

  public this (c : Core, p : ToCNF)
    core = c
    parent = p
    known_predicates = c.PlainPredicates
    when (parent != null)
      real_atom_term_cache = parent.real_atom_term_cache.Clone ()

  protected Init () : void
    true_literal = NewLit ()
    AddClause (ClauseKind.Init, array [true_literal])

  // OPT: check if formula is (AND ...) or even an atom, and skip literal generation
  [Profile] \
  public AssertFormula (f : Term) : void
    log (CNF, $ "assert_formula ($f)")
    AddClause (ClauseKind.Formula, array [ConvertFormula (f)])

  public GetLiteral (l : Literal) : Lit
    assert (atom_cache.Contains (l.atom), $"l=$l")
    if (l.is_neg)
      ~atom_cache [l.atom]
    else
      atom_cache [l.atom]

  #region UnsatCore stuff
  mutable all_clauses : list [array [Lit]] = []
  mutable quantified_clauses : list [list [array [Lit]]] = []
  mutable initial_monome : list [Lit] = []
  mutable quantified_initial_monome : list [Lit] = []
  mutable initial_monome_ht : Hashtable [Literal, Literal] = Hashtable ()
  mutable clause_tracing = false
  mutable instances : list [Fact * list [array [Lit]]] = []

  [Profile] \
  public AssertMonome (lits : list [Literal]) : void
    #if CLAUSE_DUMP
    sw.Write ("c AssertMonome\n")
    #endif
    def ar = array (1)
    initial_monome_ht.Clear ()
    foreach (l in lits)
      initial_monome_ht [l] = l
      def lbool = LitForAtom (l.atom)
      ar [0] = if (l.is_neg) ~lbool else lbool
      DumpClause (ar)
      if (!Driver.QuantInstances || l.is_neg || !l.atom.IsQuantified)
        initial_monome ::= ar [0]
      else
        quantified_initial_monome ::= ar [0]
      AddClauseImpl (ClauseKind.Init, ar)
    clause_tracing = true

  #if CLAUSE_DUMP
  static mutable id = 0
  sw : StreamWriter = { id++; File.CreateText ("log.cnf" + id.ToString()) }

  DumpClause (c : array [Lit]) : void
    def sb = StringBuilder ()
    foreach (l in c)
      when (l.IsNeg) _ = sb.Append ("-")
      _ = sb.Append (l.Var.Id+1).Append (" ")
    _ = sb.Append($"0 c $($[ToLiteral(x.val) | x in c])\n")
    sw.Write(sb.ToString ())
  #else
  DumpClause (_ : array [Lit]) : void
    {}
  #endif

  public AddClause (kind : ClauseKind, c : array [Lit]) : void
    when (clause_tracing)
      all_clauses ::= c
    log (CNF, $"add clause: trace=$(clause_tracing) $(StringizeClause (c))")
    DumpClause (c)
    AddClauseImpl (kind, c)

  protected abstract AddClauseImpl (kind : ClauseKind, c : array [Lit]) : void

  SaveImportant (lit : Literal, a : float) : void
    def v = 
      if (core.ImportantLiterals.Contains (lit))
        core.ImportantLiterals [lit] + a
      else a
    core.ImportantLiterals [lit] = v

  MaybeDeflateImportance () : void
    def keys = $[k | k in core.ImportantLiterals.Keys]
    foreach (k in keys)
      core.ImportantLiterals [k] /= 2

  [Profile] \
  public FindUnsatCore (conflicts_log : System.IO.StreamWriter = null) : void
    Account ()
    core.LastUnsatCore = null
    def nvars = var_count

    MaybeDeflateImportance ()

    when (Driver.QuantInstances)
      // make a new solver
      def solver = SatSolver (core)

      solver.AddClause (array [true_literal])

      // and clauses
      foreach (c in all_clauses)
        log (CNFQ, $ "c=$(List.FromArray(c))")
        solver.AddClause (c)
      def formulas = array (nvars + 2 + instances.Length)

      mutable assertions = []
      // and instances
      mutable varid = nvars
      foreach ((fact, clauses) when !(clauses is []) in instances)
        def v = SatSolver.Var (varid)
        varid++
        assertions ::= v.ToLit ()
        def n = ~v.ToLit ()
        def l0 = clauses.Head [0]
        foreach (c in clauses)
          assert (c [0].val == l0.val)
          c [0] = n
          log (CNFQ, $ "inst clause: $(List.FromArray (c)) (from $fact)")
          solver.AddClause (c)
          c [0] = l0
        //log (CNFQ, $ "$lit [$(LitForAtom (lit.atom))/$v]  ==>  $formula [$(clause [1])]")
        formulas [v.Id] = fact

      
      log (CNFQ, $ "i=$(initial_monome) a=$(assertions) qi=$(quantified_initial_monome)")
      def res = solver.SolveWith ((initial_monome + assertions + quantified_initial_monome).ToArray ())
      // def res = solver.SolveWith ((initial_monome + assertions).ToArray ())

      def xlits = Hashtable ()
      foreach (lbool in res)
        log (CNFQ, $"x$(lbool >> 1) neg=$(lbool & 1)")
        def fact = formulas [lbool >> 1]
        when (fact != null)
          def lit = fact.GetLiteral ()
          when (Driver.ImportantQuantOpt)
            if (xlits.Contains (lit))
              SaveImportant (lit, 1)
            else
              xlits [lit] = lit
              SaveImportant (lit, 1)
          assert (lbool & 1 == 1)
          log (CNFQ, $"important: $fact")
          lit.atom.term1.Stats.usable_instantiations++
          parent.AddInstance (fact, add_explanation = false)

    #if CLAUSE_DUMP
    sw.Write ("c Redo\n")
    #endif

    log (CNFQ, $ "stright conflict")
    // also add the stright conflict
    def solver = SatSolver (core)
    solver.AddClause (array [true_literal])
    foreach (c in all_clauses)
      DumpClause (c)
      solver.AddClause (c)
    foreach (c in quantified_clauses)
      foreach (d in c)
        DumpClause (d)
        solver.AddClause (d)

    #if CLAUSE_DUMP
    sw.Write("c Monome\n")
    foreach (l in quantified_initial_monome + initial_monome)
      DumpClause (array [l])
    sw.Write ("c Check\n")
    sw.Close ()
    #endif

    def res = solver.SolveWith ((quantified_initial_monome + initial_monome).ToArray ())
    def lits = ToLiterals (res, false)
    core.LastUnsatCore = lits
    when (Driver.Verbose)
      System.Console.WriteLine ($"small sat conflict: $lits")
    
    when (!Driver.QuantInstances && Driver.ImportantQuantOpt)
      foreach (lit in lits)
        SaveImportant (lit, 3)

    log (CNFQ, $"small sat conflict: $lits")

    when (conflicts_log != null)
      def d = core.TheDriver
      conflicts_log.Write ($ "SMALL_UC  $(d.num_main_iters)\t$(d.num_quant_iters)\t$(core.CurrentStrategy)\t$lits\n")

    parent.AddConflicts ([lits])

    // clean up
    initial_monome = null
    quantified_initial_monome = null
    quantified_clauses = null
    all_clauses = null

  [Profile] \
  public AddInstance (f : Fact, add_explanation : bool) : void
    //when (parent != null && Driver.DumpQuantStats)
    //  current_idesc = InstanceDesc (formula, lit.atom.term1, lit.is_neg, Lit ())

    //log (TEMP, $"addinst: $(LinSize (formula)) $(CNFSize (formula, false))")

    log (CNF, $"AddInstance: $f")

    def lit = f.GetLiteral ()
    lit.atom.term1.Stats.AddInstantiations (1)
    def l = if (lit.is_neg) ~LitForAtom (lit.atom) else LitForAtom (lit.atom)
    this.add_explanation = add_explanation
    def (kind, clauses) = f.Generate (l, this)
    this.add_explanation = false

    //when (current_idesc != null)
    //  current_idesc.lit =
    //    if (lit.is_neg) ~conv_form else conv_form
    //  current_idesc = null
      
    if (Driver.QuantInstances && initial_monome_ht.Contains (lit))
      instances ::= (f, clauses)
      quantified_clauses ::= clauses
      clauses.Iter (AddClauseImpl (kind, _))
    else
      clauses.Iter (AddClause (kind, _))
  #endregion

  protected virtual NewLitImpl (_idx : int) : void
    {}

  public abstract GetQMonome () : list [Literal]

  NewLit () : Lit
    def res = SatSolver.Var (var_count).ToLit ()
    NewLitImpl (var_count)
    var_count++
    res

  mutable pending_literals : list [Literal] = []

  [Profile] \
  TryAddExplanation (newlit : Literal, store_for_later = false) : void
    when (!Driver.NewLiteralExplanation)
      return
      
    core.PushState ()
    
    def t1 = newlit.atom.term1
    def t2 = newlit.atom.term2
    t1.MakeActive ()
    unless (t2 == null) t2.MakeActive ()

    if (t2 == null) {}
    else
      if (t1 : object == t2)
        // hey! this one was easy, just add X = X tautology
        _ = LitForAtom (newlit.atom)
        //log (TEMP, $"add $t1 = $t2")
        AddConflicts ([[newlit.atom.GetLiteral (is_neg = false)]])
      else if (t1.SameAs (t2))
        _ = LitForAtom (newlit.atom)
        def lits = $[ ~lit | lit in t1.ProofOfEqualityWith (t2).GetLiterals () ]
        AddConflicts ([newlit.atom.GetLiteral (is_neg = false) :: lits])
      else
        def proof = t1.CannotMergeProof (t2)
        if (proof != null)
          _ = LitForAtom (newlit.atom)
          def lits = $[ ~lit | lit in proof.GetLiterals () ]
          AddConflicts ([newlit.atom.GetLiteral (is_neg = true) :: lits])
        else
          when (store_for_later)
            pending_literals ::= newlit

    core.PopState ()

  LitForAtom (a : Atom) : Lit
    match (atom_cache.Get (a))
      | Some (lit) => lit
      | None =>
        def lit = NewLit ()
        when (atom_rev_cache.Length <= lit.val >> 1)
          System.Array.Resize (ref atom_rev_cache, lit.val * 2)
        atom_rev_cache [lit.val >> 1] = a
        atom_cache [a] = lit
        lit
        

  internal ToLiteral (lit : int) : Literal
    def idx = lit >> 1
    //log (DPLL, $"lit=$lit idx=$idx len=$(atom_rev_cache.Length)")
    when (idx < atom_rev_cache.Length)
      def a = atom_rev_cache [idx]
      when (a != null)
        return (a.GetLiteral ((lit & 1) != 0))
    null

  internal ToLiterals (lits : array [int], skip_asserted = false) : list [Literal]
    mutable res = []
    foreach (lit in lits)
      def l = ToLiteral (lit)
      when (l != null && (!skip_asserted || !l.bg_asserted))
        res ::= l
    res
        

  public StringizeClause (lits : array [Lit], bool_only = false) : list [string]
    def f (lit)
     if (!bool_only && (lit >> 1) < atom_rev_cache.Length && atom_rev_cache [lit >> 1] != null)
       atom_rev_cache [lit >> 1].GetLiteral ((lit & 1) != 0).ToString ()
     else
       if ((lit & 1) != 0) 
         $ "~x$(lit >> 1)"
       else
         $ "x$(lit >> 1)"
    $[f (lit) | (Id = lit) in lits]
        

  public AddConflicts (conflicts : list [list [Literal]], dump = false) : void
    when (dump)
      log (TEMP, "(conflicts")
      foreach (c in conflicts)
        log (TEMP, "conflict:\n\t" + c.ToString ("\n\t"))
      log (TEMP, "conflicts)")
    foreach (c in conflicts)
      AddClause (ClauseKind.TheoryConflict, $[GetLiteral (l) | l in c].ToArray ())
      
  mk (name : string, ch1 : Term) : Term
    core.TermPool.Get (name, [ch1])

  mk (name : string, ch1 : Term, ch2 : Term) : Term
    core.TermPool.Get (name, [ch1, ch2])
 
  mk (name : string, ch : list [Term]) : Term
    core.TermPool.Get (name, ch)

  ExpandITE (f : Term) : Term
    if (ite_expanded.Contains (f))
      ite_expanded [f]
    else if (f.Name == "ite")
      match (f.Children)
        | [cond, th, el] =>
          def fv = core.TermPool.FreshVar ()
          ite_expanded [f] = fv
          def assertion = 
            mk ("and", 
              mk ("or", mk ("=", fv, ExpandITE (th)), mk ("not", cond)),
              mk ("or", mk ("=", fv, ExpandITE (el)), cond))
          AssertFormula (assertion)
          fv
        | _ => throw FatalError ("bad ITE")
    else
      def t = mk (f.Name, f.Children.Map (ExpandITE))
      ite_expanded [f] = t
      t

  known_predicates : Hashtable [string, string]

  [Profile] \
  MakeAtom (f : Term) : Atom
    mutable a
    if (real_atom_term_cache.TryGetValue (f, out a)) a
    else
      // log (TEMP, $"make atom $f")
      def res =
        match ((f.Name, f.Children))
          | ("=", [p, q]) => 
            if (p === core.SubtypingTrue && q.Name == core.SubtypingSymbol)
              Atom (ExpandITE (q), null)
            else if (q === core.SubtypingTrue && p.Name == core.SubtypingSymbol)
              Atom (ExpandITE (p), null)
            else
              Atom (ExpandITE (p), ExpandITE (q))
          | ("forall", _) => 
            def q = QAtom (f)
            when (q.HasExplicitTriggers)
              core.SeenExplicitTriggers = true
            q
          | (_, []) => assert (f.IsVar); Atom (f, core.TermPool.True)
          | (name, _) when core.IsSomeTheoryPredicate (name) =>
            Atom (ExpandITE (f), null)
          | (name, _) =>
            unless (known_predicates.Contains (name))
              known_predicates [name] = name
              unless (name.IndexOf ('.') != -1)
                log (INFO, $ "new predicate: $name")
            Atom (ExpandITE (f), core.TermPool.True)
      real_atom_term_cache [f] = res
      when (add_explanation)
        TryAddExplanation (res.GetLiteral (false))
      res

  [Profile] \
  ConvertFormulaAI (f : Term) : Lit
    ConvertFormula (f)

  ConvertFormula (f : Term) : Lit
    def handle_nary (cache, lst)
      def lits = lst.Map (ConvertFormula)
      def key = lits.Map (_.Id).Sort (_ - _)
      match (cache.Get (key))
        | Some (lit) => (false, lit, lits)
        | None =>
          def lit = NewLit ()
          cache [key] = lit
          (true, lit, lits)

    def lst = f.Children
    match (f.Name)
      | _ when formula_cache.Contains (f) =>
        def lit = formula_cache [f]
        when (current_idesc != null)
          when (f.Name == "and" || f.Name == "or")
            foreach (t in lst)
              _ = ConvertFormula (t)
        lit

      | "or" => 
        def (need_clauses, x, lits) = handle_nary (or_cache, lst)
        log (CNF, $"$f --> x=$x lits=$lits")
        when (need_clauses)
          foreach (l in lits)
            AddClause (ClauseKind.Formula, array [~l, x])
          AddClause (ClauseKind.Formula, (~x :: lits).ToArray ())
        formula_cache [f] = x
        x
      
      | "and" => 
        def (need_clauses, x, lits) = handle_nary (and_cache, lst)
        log (CNF, $"$f --> x=$x lits=$lits")
        when (need_clauses)
          foreach (l in lits)
            AddClause (ClauseKind.Formula, array [l, ~x])
          AddClause (ClauseKind.Formula, (x :: lits.Map (~_)).ToArray ())
        formula_cache [f] = x
        x
        
      | "true" =>
        assert (lst is [])
        true_literal

      | "false" => 
        assert (lst is [])
        ~true_literal

      | "not" =>
        ~ConvertFormula (f.OnlyChild)

      | _ => GetLit (f)


  public MakeLiteral (f : Term) : Literal
    def idx = GetLit (f).Var.Id
    atom_rev_cache [idx].GetLiteral (is_neg = false)
 
  [Profile] \
  GetLit (f : Term) : Lit
    match (f.Name)
      | "not" | "and" | "or" => assert (false)
      | _ =>
        mutable lit = Lit ()
        if (atom_term_cache.TryGetValue (f, out lit))
          SaveSource (lit)
          lit
        else
          def atom = MakeAtom (f)
          lit = LitForAtom (atom)
          if (terms_for_atom.Contains (atom))
            terms_for_atom [atom] ::= f
          else
            terms_for_atom [atom] = [f]
          atom_term_cache [f] = lit
          SaveSource (lit)
          lit
  
  
  #region case split stats
  [Record] \
  class InstanceDesc
    internal instance : Term
    internal axiom : Term
    internal is_skolemization : bool
    internal mutable lit : Lit
    
  class VarUsage
    internal idesc : InstanceDesc
    internal mutable seen_true : bool
    internal mutable seen_false : bool
    internal this (id : InstanceDesc)
      idesc = id

  var_stats : Hashtable [int, list [VarUsage]] = Hashtable ()
  mutable current_idesc : InstanceDesc = null
  mutable model_count : int

  SaveSource (lit : Lit) : void
    when (current_idesc != null)
      def id = lit.Var.Id
      unless (var_stats.Contains (id))
        var_stats [id] = []
      match (var_stats [id])
        | x :: _ when x.idesc : object == current_idesc => {}
        | _ => var_stats [id] ::= VarUsage (current_idesc)
  
  Account () : void
    def evil_instances = Hashtable ()
    mutable to_account = []
    foreach (kv in var_stats)
      foreach (vu in kv.Value)
        when (vu.seen_true && vu.seen_false)
          unless (evil_instances.Contains (vu.idesc.instance))
            to_account ::= vu.idesc.axiom
            evil_instances [vu.idesc.instance] = true
    def amount = (model_count : float) / to_account.Length
    foreach (t in to_account)
      //log (TEMP, $ "charge: $amount $t")
      t.Stats.iters_account += amount

  protected CheckForSplits (model : array [int]) : void
    model_count++

    def true_vals = BitVec (VarCount + 1)
    def false_vals = BitVec (VarCount + 1)
    
    foreach (lit in model)
      if (lit & 1 != 0)
        false_vals [lit >> 1] = true
      else
        true_vals [lit >> 1] = true

    foreach (lit in model)
      mutable s = null
      when (var_stats.TryGetValue (lit >> 1, out s))
        foreach (vu in s)
          def formula_ok =
            if (vu.idesc.lit.IsNeg)
              false_vals [vu.idesc.lit.Var.Id]
            else
              true_vals [vu.idesc.lit.Var.Id]
          when (formula_ok)
            if ((lit & 1) == 0)
              vu.seen_false = true
            else
              vu.seen_true = true
  #endregion

  #region instance generators
  public abstract class Fact
    protected inst : Instantiator

    abstract public Terms : array [Term]
      get
    abstract public AddTerm (t : Term) : void
    abstract public Generate (lit : Lit, tocnf : ToCNF) : ClauseKind * list [array [Lit]]
    abstract public IsExistential : bool
      get

    public GetLiteral () : Literal
      inst.qatom.GetLiteral (IsExistential)

    protected this (i : Instantiator)
      inst = i
  
  class SimpleFact : Fact
    mutable formula : Term
    existential : bool

    public override Terms : array [Term]
      get
        inst.SingleFormula

    public override AddTerm (t : Term) : void
      assert (formula == null)
      formula = t

    public override Generate (lit : Lit, tocnf : ToCNF) : ClauseKind * list [array [Lit]]
      def conv_form = tocnf.ConvertFormulaAI (formula)
      (ClauseKind.Formula,
        if (lit.IsNeg)
          [array [~lit, ~conv_form]]
        else
          [array [~lit, conv_form]])

    public override IsExistential : bool
      get
        existential

    public this (ex : bool, i : Instantiator)
      base (i)
      existential = ex

    public override ToString () : string
      def lit = GetLiteral ()
      if (lit.IsNeg)
        $ "$lit ==> (not $formula)"
      else
        $ "$lit ==> $formula"

  class PreConvertedFact : Fact
    mutable i : int
    sterms : array [Term]

    public override Terms : array [Term]
      get
        inst.Terms

    public override IsExistential : bool
      get
        false

    public override AddTerm (t : Term) : void
      sterms [i] = t
      i++

    public override Generate (lit : Lit, tocnf : ToCNF) : ClauseKind * list [array [Lit]]
      assert (sterms.Length == inst.Terms.Length)
      assert (i == sterms.Length, $"i=$i len=$(sterms.Length)")
      assert (! lit.IsNeg)

      def lits = array (sterms.Length)
      foreach (i in [0 .. sterms.Length - 1])
        lits [i] = tocnf.GetLit (sterms [i])

      def get_clause (template)
        def clause = array (template.Length + 1)
        clause [0] = ~lit
        mutable ptr = 0
        foreach (t in template)
          //log (TEMP, $ "ptr=$ptr t=$t ll=$(lits.Length) cl=$(clause.Length)")
          ptr++
          clause [ptr] = if (t < 0) ~lits[-t-1] else lits[t-1]
        clause

      (ClauseKind.Instance, $[get_clause (c) | c in inst.clauses])

    public this (inst : Instantiator)
      base (inst)
      sterms = array (inst.Terms.Length)

    public override ToString () : string
      def str (i)
        if (i < 0) $"- $(sterms [-i - 1])" else $"$(sterms [i - 1])"
      def c = inst.clauses.Map (c => $[str (l) | l in c])
      $"$(GetLiteral()) ==> $c"

  public class Instantiator
    internal clauses : list [array [int]]
    internal Terms : array [Term]
    internal SingleFormula : array [Term]
    internal qatom : QAtom

    public this (qa : QAtom)
      qatom = qa
      def f = qa.Formula
      SingleFormula = array [f]
      if (CNFSize (f, false) < LinSize (f) * 4)
        (clauses, Terms) = ConvertToTrueCNF (f)
      else
        clauses = null
        Terms = SingleFormula
    
    public GetFreshFact (existential = false) : Fact
      if (clauses == null || existential)
        SimpleFact (existential, this)
      else
        PreConvertedFact (this)
    
    static CNFSize (f : Term, neg : bool) : int
      match (f.Name)
        | "and" when !neg \
        | "or" when neg =>
          mutable res = 0
          f.IterChildren (c => res += CNFSize (c, neg))
          res
        | "and" | "or" =>
          mutable res = 1
          f.IterChildren (c => res *= CNFSize (c, neg))
          res
        | "not" => CNFSize (f.OnlyChild, !neg)
        | _ => 1

    static LinSize (f : Term) : int
      match (f.Name)
        | "and" | "or" =>
          mutable res = 0
          f.IterChildren (c => res += LinSize (c))
          res
        | "not" => LinSize (f.OnlyChild)
        | _ => 1

    static ConvertToTrueCNF (f : Term) : list [array [int]] * array [Term]
      def lits = Hashtable ()

      def add (aa)
        mutable len = 0
        foreach (a in aa) len += a.Length
        def res = array (len)
        mutable i = 0
        foreach (a in aa) 
          a.CopyTo (res, i)
          i += a.Length
        res

      def conv (f, neg)
        match (f.Name)
          | "and" when !neg \
          | "or" when neg =>
            $[ clause | ch in f.Children, clause in conv (ch, neg) ]

          | "and" | "or" =>
            def loop (pref, sets)
              match (sets)
                | set :: sets =>
                  $[clause | c in set, clause in loop (c :: pref, sets)]
                | [] => [add (pref)]
            loop ([], $[ conv (ch, neg) | ch in f.Children ])

          | "not" => conv (f.OnlyChild, !neg)

          | "false" when !neg \
          | "true" when neg =>
            [array []]

          | "true" | "false" =>
            []

          | _ =>
            unless (lits.Contains (f))
              lits [f] = lits.Count
            def n = lits [f] + 1
            [array [if (neg) -n else n]]

      def clauses = conv (f, false)
      def terms = array (lits.Count)
      foreach ((Key = term, Value = idx) in lits)
        terms [idx] = term
      
      (clauses, terms)

  #endregion