Class: Udb::LogicNode

Inherits:

Object

• Object
• Udb::LogicNode

Extended by:

T::Sig

Defined in:

lib/udb/logic.rb,
lib/udb/eqn.rb

Overview

Abstract syntax tree of the condition logic

Defined Under Namespace

Classes: CanonicalizationType, ConditionalEndterm, EqntottResult, LogicSymbolFormat, MemoizedState, PairMintermsResult, PrimeImplicantsResult, SizeExplosion

Constant Summary

ChildType =

T.type_alias { T.any(LogicNode, TermType) }

True =

LogicNode.new(LogicNodeType::True, [])

False =

LogicNode.new(LogicNodeType::False, [])

Xlen32 =

LogicNode.new(LogicNodeType::Term, [XlenTerm.new(32).freeze]).freeze

Xlen64 =

LogicNode.new(LogicNodeType::Term, [XlenTerm.new(64).freeze]).freeze

EvalCallbackType =

T.type_alias { T.proc.params(arg0: TermType).returns(SatisfiedResult) }

ReplaceCallbackType =

T.type_alias { T.proc.params(arg0: LogicNode).returns(LogicNode) }

LOGIC_SYMBOLS =

{
  LogicSymbolFormat::C => {
    TRUE: "1",
    FALSE: "0",
    NOT: "!",
    AND: "&&",
    OR: "||",
    XOR: "^",
    IMPLIES: "->" # making this up; there is no implication operator in C
  },
  LogicSymbolFormat::Eqn => {
    TRUE: "ONE",
    FALSE: "ZERO",
    NOT: "!",
    AND: "&",
    OR: "|",
    XOR: "DOES NOT EXIST",
    IMPLIES: "DOES NOT EXIST"
  },
  LogicSymbolFormat::English => {
    TRUE: "true",
    FALSE: "false",
    NOT: "NOT ",
    AND: "AND",
    OR: "OR",
    XOR: "XOR",
    IMPLIES: "IMPLIES"
  },
  LogicSymbolFormat::Predicate => {
    TRUE: "true",
    FALSE: "false",
    NOT: "\u00ac",
    AND: "\u2227",
    OR: "\u2228",
    XOR: "\u2295",
    IMPLIES: "\u2192"
  }
}

Instance Attribute Summary

• #children ⇒ Object readonly

  Returns the value of attribute children.

• #memo ⇒ Object

  Returns the value of attribute memo.

• #type ⇒ Object readonly

  Returns the value of attribute type.

Class Method Summary

• .find_prime_implicants(mterms, group_by) ⇒ Object
• .group_mterms(mterms, group_by) ⇒ Object
• .inc_brute_force_sat_solves ⇒ Object
• .inc_z3_cache_hits ⇒ Object
• .inc_z3_sat_solves ⇒ Object
• .make_eval_cb(&blk) ⇒ Object
• .make_replace_cb(&blk) ⇒ Object
• .num_brute_force_sat_solves ⇒ Object
• .num_z3_cache_hits ⇒ Object
• .num_z3_sat_solves ⇒ Object
• .pair_mterms(group1, group2) ⇒ Object
• .prime_implicant_covers_mterm?(implicant, minterm) ⇒ Boolean
• .reset_stats ⇒ Object

  statistics counters.

Instance Method Summary

• #cnf? ⇒ Boolean
• #cnf_conjunction_term? ⇒ Boolean
• #collect_tseytin(subformulae) ⇒ Object
• #distribute_not ⇒ Object
• #dnf? ⇒ Boolean
• #dnf_disjunctive_term? ⇒ Boolean
• #do_to_eqntott(tree, term_map) ⇒ Object
• #eql?(other) ⇒ Boolean
• #equisat_cnf ⇒ Object
• #equisatisfiable?(other, cfg_arch) ⇒ Boolean
• #equiv_cnf(raise_on_explosion: true) ⇒ Object
• #equivalent?(other, cfg_arch) ⇒ Boolean
• #espresso(result_type, exact) ⇒ Object
• #eval_cb(callback) ⇒ Object
• #failing_conjuncts(eval_cb) ⇒ Object
• #from_dimacs(dimacs) ⇒ Object
• #group_by_2 ⇒ Object
• #grouped_by_2?(node) ⇒ Boolean
• #hash ⇒ Object
• #initialize(type, children) ⇒ LogicNode constructor

  A new instance of LogicNode.

• #literals ⇒ Object
• #minimal_unsat_subsets ⇒ Object
• #minimize(result_type) ⇒ Object
• #nested_cnf? ⇒ Boolean
• #nested_cnf_conjunction_term?(ancestor_or) ⇒ Boolean
• #nnf ⇒ Object
• #nnf? ⇒ Boolean

  True iff self is in Negation Normal Form.

• #node_children ⇒ Object
• #partial_evaluate(cb) ⇒ Object
• #reduce ⇒ Object
• #replace_terms(callback) ⇒ Object
• #satisfiability_depends_on_ext_req?(ext_req) ⇒ Boolean
• #satisfiable?(cfg_arch) ⇒ Boolean
• #terms ⇒ Object
• #terms_no_antecendents ⇒ Object
• #to_asciidoc(include_versions:) ⇒ Object
• #to_dimacs ⇒ Object
• #to_eqntott ⇒ Object
• #to_h(term_determined = false) ⇒ Object
• #to_idl(cfg_arch) ⇒ Object
• #to_s(format: LogicSymbolFormat::Predicate) ⇒ Object
• #to_s_pretty ⇒ Object
• #to_s_with_value(callback, format: LogicSymbolFormat::Predicate) ⇒ Object
• #to_z3(cfg_arch, solver = Z3Solver.new) ⇒ Object
• #tseytin ⇒ Object
• #tseytin_prop ⇒ Object
• #unsatisfiable?(cfg_arch) ⇒ Boolean

Constructor Details

#initialize(type, children) ⇒ LogicNode

Returns a new instance of LogicNode.

# File 'lib/udb/logic.rb', line 1244

def initialize(type, children)
  if [LogicNodeType::Term, LogicNodeType::Not].include?(type) && children.size != 1
    raise ArgumentError, "Children must be singular"
  end
  if [LogicNodeType::And, LogicNodeType::Or, LogicNodeType::Xor, LogicNodeType::None, LogicNodeType::If].include?(type) && children.size < 2
    raise ArgumentError, "Children must have at least two elements"
  end

  @children = children
  @children.freeze
  @node_children = (@type == LogicNodeType::Term) ? nil : T.cast(@children, T::Array[LogicNode])


  if [LogicNodeType::True, LogicNodeType::False].include?(type) && !children.empty?
    raise ArgumentError, "Children must be empty"
  elsif type == LogicNodeType::Term
    # ensure the children are TermType
    children.each { |child| T.assert_type!(T.cast(child, TermType), TermType) }
  else
    # raise ArgumentError, "All Children must be LogicNodes" unless children.all? { |child| child.is_a?(LogicNode) }
  end

  @type = type
  @type.freeze

  # used for memoization in transformation routines
  @memo = MemoizedState.new
end

Instance Attribute Details

#children ⇒ Object (readonly)

Returns the value of attribute children.

# File 'lib/udb/logic.rb', line 1232

def children
  @children
end

#memo ⇒ Object

Returns the value of attribute memo.

# File 'lib/udb/logic.rb', line 1241

def memo
  @memo
end

#type ⇒ Object (readonly)

Returns the value of attribute type.

# File 'lib/udb/logic.rb', line 1229

def type
  @type
end

Class Method Details

.find_prime_implicants(mterms, group_by) ⇒ Object

# File 'lib/udb/logic.rb', line 1432

def self.find_prime_implicants(mterms, group_by)
  groups = group_mterms(mterms, group_by)

  # Pair mterms until no further simplification is possible
  prime_implicants = T.let([], T::Array[String])
  matched = T.let(Set.new, T::Set[String])
  while groups.size > 1
    new_groups = Hash.new { |h, k| h[k] = [] }
    matched.clear
    groups.keys.sort.each_cons(2) do |k1, k2|
      res = pair_mterms(T.must(groups[T.must(k1)]), T.must(groups[T.must(k2)]))
      matched.merge(res.matched_mterms)
      new_group = res.new_group
      new_groups[k1] += new_group unless new_group.empty?
    end
    prime_implicants += groups.values.flatten.reject { |mterm| matched.include?(mterm) }
    groups = new_groups
  end
  prime_implicants += groups.values.flatten.reject { |mterm| matched.include?(mterm) }
  prime_implicants.uniq!

  coverage = Hash.new { |h, k| h[k] = [] }

  mterms.each do |minterm|
    prime_implicants.each_with_index do |implicant, idx|
      if prime_implicant_covers_mterm?(implicant, minterm)
        coverage[minterm] << idx
      end
    end
  end

  essential_indices = []
  uncovered = mterms.dup

  # Find essential prime implicants
  coverage.each do |mterm, implicant_indices|
    if implicant_indices.size == 1
      idx = implicant_indices.first
      unless essential_indices.include?(idx)
        essential_indices << idx
        # Remove all minterms covered by this implicant
        uncovered.reject! { |m| prime_implicant_covers_mterm?(prime_implicants.fetch(idx), m) }
      end
    end
  end

  minimal_indices = essential_indices.dup
  # Greedy selection for remaining minterms
  while uncovered.any?
    best_idx = T.cast(prime_implicants.each_with_index.max_by do |implicant, idx|
      uncovered.count { |m| prime_implicant_covers_mterm?(implicant, m) }
    end, T::Array[Integer]).last

    minimal_indices << best_idx
    uncovered.reject! { |m| prime_implicant_covers_mterm?(prime_implicants.fetch(T.must(best_idx)), m) }
  end

  PrimeImplicantsResult.new(
    essential: essential_indices.map { |i| prime_implicants.fetch(i) },
    minimal:  minimal_indices.map { |i| prime_implicants.fetch(i) }
  )
end

.group_mterms(mterms, group_by) ⇒ Object

# File 'lib/udb/logic.rb', line 1374

def self.group_mterms(mterms, group_by)
  groups = T.let({}, T::Hash[Integer, T::Array[String]])
  mterms.each do |mterm|
    n = mterm.count(group_by)
    groups[n] ||= []
    groups.fetch(n) << mterm
  end
  groups
end

.inc_brute_force_sat_solves ⇒ Object

# File 'lib/udb/logic.rb', line 1205

def self.inc_brute_force_sat_solves
  @num_brute_force_sat_solves += 1
end

.inc_z3_cache_hits ⇒ Object

# File 'lib/udb/logic.rb', line 1221

def self.inc_z3_cache_hits
  @num_z3_cache_hits += 1
end

.inc_z3_sat_solves ⇒ Object

# File 'lib/udb/logic.rb', line 1213

def self.inc_z3_sat_solves
  @num_z3_sat_solves += 1
end

.make_eval_cb(&blk) ⇒ Object

# File 'lib/udb/logic.rb', line 1647

def self.make_eval_cb(&blk)
  blk
end

.make_replace_cb(&blk) ⇒ Object

# File 'lib/udb/logic.rb', line 1653

def self.make_replace_cb(&blk)
  blk
end

.num_brute_force_sat_solves ⇒ Object

# File 'lib/udb/logic.rb', line 1201

def self.num_brute_force_sat_solves
  @num_brute_force_sat_solves
end

.num_z3_cache_hits ⇒ Object

# File 'lib/udb/logic.rb', line 1217

def self.num_z3_cache_hits
  @num_z3_cache_hits
end

.num_z3_sat_solves ⇒ Object

# File 'lib/udb/logic.rb', line 1209

def self.num_z3_sat_solves
  @num_z3_sat_solves
end

.pair_mterms(group1, group2) ⇒ Object

# File 'lib/udb/logic.rb', line 1390

def self.pair_mterms(group1, group2)
  new_group = []
  matched = Set.new
  group1.each do |m1|
    group2.each do |m2|
      diff_count = 0
      diff_index = -1
      loop_index = 0
      m1.each_char do |bit|
        if bit != m2[loop_index]
          diff_count += 1
          diff_index = loop_index
        end
        loop_index += 1
      end
      if diff_count == 1
        new_mterm = m1.dup
        new_mterm[diff_index] = "-"
        new_group << new_mterm
        matched.add(m1)
        matched.add(m2)
      end
    end
  end
  PairMintermsResult.new(new_group: new_group.uniq, matched_mterms: matched)
end

.prime_implicant_covers_mterm?(implicant, minterm) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 1418

def self.prime_implicant_covers_mterm?(implicant, minterm)
  implicant.chars.zip(minterm.chars).all? do |i_bit, m_bit|
    i_bit == "-" || i_bit == m_bit
  end
end

.reset_stats ⇒ Object

statistics counters

# File 'lib/udb/logic.rb', line 1191

def self.reset_stats
  @num_brute_force_sat_solves = 0
  @time_brute_force_sat_solves = 0
  @num_z3_sat_solves = 0
  @time_z3_sat_solves = 0
  @num_z3_cache_hits = 0
end

Instance Method Details

#cnf? ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 2814

def cnf?
  unless @memo.is_cnf.nil?
    return @memo.is_cnf
  end

  ret =
    case @type
    when LogicNodeType::Term, LogicNodeType::True, LogicNodeType::False
      true
    when LogicNodeType::Not
      node_children.fetch(0).type == LogicNodeType::Term
    when LogicNodeType::Or
      node_children.all? do |child|
        [
          child.type == LogicNodeType::True,
          child.type == LogicNodeType::False,
          child.type == LogicNodeType::Term,
          child.type == LogicNodeType::Not && \
            child.node_children.fetch(0).type == LogicNodeType::Term
        ].any?
      end
    when LogicNodeType::Xor, LogicNodeType::If, LogicNodeType::None
      false
    when LogicNodeType::And
      node_children.all? { |child| child.cnf_conjunction_term? }
    else
      T.absurd(@type)
    end

  @memo.is_cnf = ret
end

#cnf_conjunction_term? ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 2876

def cnf_conjunction_term?
  case @type
  when LogicNodeType::Term, LogicNodeType::True, LogicNodeType::False
    true
  when LogicNodeType::Not
    node_children.fetch(0).type == LogicNodeType::Term
  when LogicNodeType::Or
    # or is only valid if only contains literals
    node_children.all? do |child|
      [
        child.type == LogicNodeType::True,
        child.type == LogicNodeType::False,
        child.type == LogicNodeType::Term,
        ((child.type == LogicNodeType::Not) && \
          child.node_children.fetch(0).type == LogicNodeType::Term)
      ].any?
    end
  when LogicNodeType::And, LogicNodeType::Xor, LogicNodeType::If, LogicNodeType::None
    false
  else
    T.absurd(@type)
  end
end

#collect_tseytin(subformulae) ⇒ Object

# File 'lib/udb/logic.rb', line 3261

def collect_tseytin(subformulae)
  case @type
  when LogicNodeType::And
    # (¬A ∨ ¬B ∨ p) ∧ (A ∨ ¬p) ∧ (B ∨ ¬p)
    a = node_children.fetch(0).tseytin_prop
    b = node_children.fetch(1).tseytin_prop
    subformulae <<
      LogicNode.new(
        LogicNodeType::And,
        [
          LogicNode.new(LogicNodeType::Or,
            [
              LogicNode.new(LogicNodeType::Not, [a]),
              LogicNode.new(LogicNodeType::Not, [b]),
              tseytin_prop
            ]
          ),
          LogicNode.new(LogicNodeType::Or,
            [
              a,
              LogicNode.new(LogicNodeType::Not, [tseytin_prop])
            ]
          ),
          LogicNode.new(LogicNodeType::Or,
            [
              b,
              LogicNode.new(LogicNodeType::Not, [tseytin_prop])
            ]
          )
        ]
      )
    node_children.fetch(0).collect_tseytin(subformulae)
    node_children.fetch(1).collect_tseytin(subformulae)
  when LogicNodeType::Or
    # (A ∨ B ∨ ¬p) ∧ (¬A ∨ p) ∧ (¬B ∨ p)
    a = node_children.fetch(0).tseytin_prop
    b = node_children.fetch(1).tseytin_prop
    subformulae <<
      LogicNode.new(
        LogicNodeType::And,
        [
          LogicNode.new(LogicNodeType::Or, [a, b, LogicNode.new(LogicNodeType::Not, [tseytin_prop])]),
          LogicNode.new(LogicNodeType::Or, [LogicNode.new(LogicNodeType::Not, [a]), tseytin_prop]),
          LogicNode.new(LogicNodeType::Or, [LogicNode.new(LogicNodeType::Not, [b]), tseytin_prop])
        ]
      )
    node_children.fetch(0).collect_tseytin(subformulae)
    node_children.fetch(1).collect_tseytin(subformulae)
  when LogicNodeType::Not
    # (A ∨ p) ∧ (¬A ∨ ¬p)
    a = node_children.fetch(0).tseytin_prop
    subformulae <<
      LogicNode.new(
        LogicNodeType::And,
        [
          LogicNode.new(LogicNodeType::Or, [a, tseytin_prop]),
          LogicNode.new(LogicNodeType::Or, [
            LogicNode.new(LogicNodeType::Not, [a]),
            LogicNode.new(LogicNodeType::Not, [tseytin_prop]),
          ])
        ]
      )
    node_children.fetch(0).collect_tseytin(subformulae)
  when LogicNodeType::True, LogicNodeType::False
    # pass
  when LogicNodeType::Term
    # pass
  else
    raise "? #{@type}"
  end
end

#distribute_not ⇒ Object

# File 'lib/udb/logic.rb', line 3248

def distribute_not
  # recursively apply demorgan until we get to terms
  raise "Not a negation" unless @type == LogicNodeType::Not

  distribute_not_helper(self)
end

#dnf? ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 2848

def dnf?
  case @type
  when LogicNodeType::Term, LogicNodeType::True, LogicNodeType::False
    true
  when LogicNodeType::Not
    node_children.fetch(0).type == LogicNodeType::Term
  when LogicNodeType::Or
    node_children.all? { |child| child.dnf_disjunctive_term? }
  when LogicNodeType::And
    node_children.all? do |child|
      [
        child.type == LogicNodeType::True,
        child.type == LogicNodeType::False,
        child.type == LogicNodeType::Term,
        child.type == LogicNodeType::Not && \
          child.node_children.fetch(0).type == LogicNodeType::Term
      ].any?
    end
  when LogicNodeType::Xor, LogicNodeType::If, LogicNodeType::None
    false
  else
    T.absurd(@type)
  end
end

#dnf_disjunctive_term? ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 2903

def dnf_disjunctive_term?
  case @type
  when LogicNodeType::Term, LogicNodeType::True, LogicNodeType::False
    true
  when LogicNodeType::Not
    node_children.fetch(0).type == LogicNodeType::Term
  when LogicNodeType::And
    # and is only valid if only contains literals
    node_children.all? do |child|
      [
        child.type == LogicNodeType::True,
        child.type == LogicNodeType::False,
        child.type == LogicNodeType::Term,
        ((child.type == LogicNodeType::Not) && \
          child.node_children.fetch(0).type == LogicNodeType::Term)
      ]
    end
  when LogicNodeType::Or, LogicNodeType::Xor, LogicNodeType::If, LogicNodeType::None
    false
  else
    T.absurd(@type)
  end
end

#do_to_eqntott(tree, term_map) ⇒ Object

# File 'lib/udb/logic.rb', line 3169

def do_to_eqntott(tree, term_map)
  t = tree.type
  case t
  when LogicNodeType::True
    "1"
  when LogicNodeType::False
    "0"
  when LogicNodeType::And
    "(#{tree.node_children.map { |child| do_to_eqntott(child, term_map) }.join(" & ")})"
  when LogicNodeType::Or
    "(#{tree.node_children.map { |child| do_to_eqntott(child, term_map) }.join(" | ")})"
  when LogicNodeType::Xor
    do_to_eqntott(tree.nnf, term_map)
  when LogicNodeType::None
    do_to_eqntott(LogicNode.new(LogicNodeType::Not, [LogicNode.new(LogicNodeType::Or, tree.children)]), term_map)
  when LogicNodeType::Term
    term_map.fetch(T.cast(tree.children.fetch(0), TermType))
  when LogicNodeType::Not
    "!(#{do_to_eqntott(tree.node_children.fetch(0), term_map)})"
  when LogicNodeType::If
    do_to_eqntott(tree.nnf, term_map)
  else
    T.absurd(t)
  end
end

#eql?(other) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 3637

def eql?(other)
  return false unless other.is_a?(LogicNode)

  to_h.eql?(other.to_h)
end

#equisat_cnf ⇒ Object

# File 'lib/udb/logic.rb', line 2787

def equisat_cnf
  return @memo.equisat_cnf unless @memo.equisat_cnf.nil?
  return self if @type == LogicNodeType::True
  return self if @type == LogicNodeType::False

  # strategy: try conversion using Demorgan's laws first. If that appears to be getting too
  # large (exponential in the worst case), fall back on the tseytin transformation
  @memo.equisat_cnf =
    if @memo.equiv_cnf.nil?
      if terms.count > 4 || literals.count > 10
        tseytin
      else
        # try demorgan first, then fall back if it gets too big
        begin
          equiv_cnf
        rescue SizeExplosion
          tseytin
        end
      end
    else
      # we already calculated an equivalent cnf, which is also equisatisfiable
      @mem.equiv_cnf
    end
end

#equisatisfiable?(other, cfg_arch) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 3112

def equisatisfiable?(other, cfg_arch)
  if satisfiable?(cfg_arch)
    other.satisfiable?(cfg_arch)
  else
    !other.satisfiable?(cfg_arch)
  end
end

#equiv_cnf(raise_on_explosion: true) ⇒ Object

# File 'lib/udb/logic.rb', line 2763

def equiv_cnf(raise_on_explosion: true)
  @memo.equiv_cnf ||=
    begin
      r = reduce
      return r if r.type == LogicNodeType::True || r.type == LogicNodeType::False

      n = r.nnf

      candidate = n.reduce
      candidate = n.group_by_2
      unflattened = do_equiv_cnf(candidate, raise_on_explosion:)
      result = flatten_cnf(unflattened).reduce
      if result.frozen?
        raise "?" unless result.memo.is_cnf == true
      else
        result.memo.is_cnf = true
      end
      result
    end
end

#equivalent?(other, cfg_arch) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 3122

def equivalent?(other, cfg_arch)
  # equivalent (A <=> B) if the biconditional is true:
  #   (A -> B) && (B -> A)
  # or, expressed without implication:
  #   (!A || B) && (!B || A)

  # equivalence is a tautology iff ~(A <=> B) is a contradiction,
  # i.e., !(A <=> B) is UNSATISFIABLE
  #       !((!A || B) && (!B || A)) is UNSATISFIABLE

  r = self
  other = other
  contradiction = LogicNode.new(
    LogicNodeType::Not,
    [
      LogicNode.new(
        LogicNodeType::And,
        [
          LogicNode.new(
            LogicNodeType::Or,
            [
              LogicNode.new(LogicNodeType::Not, [r]),
              other
            ]
          ),
          LogicNode.new(
            LogicNodeType::Or,
            [
              LogicNode.new(LogicNodeType::Not, [r]),
              self
            ]
          )
        ]
      )
    ]
  )
  contradiction.unsatisfiable?(cfg_arch)
end

#espresso(result_type, exact) ⇒ Object

# File 'lib/udb/logic.rb', line 3494

def espresso(result_type, exact)
  nterms = terms.size

  pla =
    if nterms > 4 || literals.size >= 32

      eqn_result =
        if result_type == CanonicalizationType::SumOfProducts
          to_eqntott
        elsif result_type == CanonicalizationType::ProductOfSums
          LogicNode.new(LogicNodeType::Not, [self]).to_eqntott
        else
          T.absurd(result_type)
        end
      tt = T.let(nil, T.nilable(String))
      Tempfile.open do |f|
        f.write <<~FILE
          NAME=f;
          #{eqn_result.eqn};
        FILE
        f.flush

        tt, status = Open3.capture2(Udb::EqntottPath.binary, "-l", T.must(f.path))
        raise "eqntott failure" unless status.success?
      end

      if T.must(tt).lines.any? { |l| l =~ /^\.p 0/ }
        if result_type == CanonicalizationType::SumOfProducts
          # short circuit here, it's trivially false
          return LogicNode.new(LogicNodeType::False, [])
        else
          # short circuit here, it's trivially true
          return LogicNode.new(LogicNodeType::True, [])
        end
      end
      tt
    else

      term_idx = T.let({}, T::Hash[TermType, Integer])
      terms.each_with_index do |term, idx|
        term_idx[term] = idx
      end

      # define the callback outside the loop to avoid allocating a new block on every iteration
      val_out_of_loop = 0
      cb = LogicNode.make_eval_cb do |term|
        ((val_out_of_loop >> term_idx.fetch(term)) & 1).zero? ? SatisfiedResult::No : SatisfiedResult::Yes
      end

      tt = T.let([], T::Array[T::Array[String]])
      (1 << nterms).times do |val|
        val_out_of_loop = val
        if result_type == CanonicalizationType::SumOfProducts
          if eval_cb(cb) == SatisfiedResult::Yes
            tt << [val.to_s(2).rjust(nterms, "0").reverse, "1"]
          else
            tt << [val.to_s(2).rjust(nterms, "0").reverse, "0"]
          end
        elsif result_type == CanonicalizationType::ProductOfSums
          if eval_cb(cb) == SatisfiedResult::Yes
            tt << [val.to_s(2).rjust(nterms, "0").reverse, "0"]
          else
            tt << [val.to_s(2).rjust(nterms, "0").reverse, "1"]
          end
        end
      end

      <<~INFILE
        .i #{nterms}
        .o 1
        .na f
        .ob out
        .p #{tt.size}
        #{tt.map { |t| t.join(" ") }.join("\n")}
      INFILE
    end

  Tempfile.open do |f|
    f.write pla
    f.flush

    args =
      if exact
        [Udb::EspressoPath.binary, "-Dsignature", f.path]
      else
        [Udb::EspressoPath.binary, "-efast", f.path]
      end
    result, status = T.unsafe(Open3).capture2e(*args)
    raise "espresso failure\n#{result}" unless status.success?

    sop_terms = []
    always_true = T.let(false, T::Boolean)
    result.lines.each_with_index do |line, idx|
      next if line[0] == "."
      next if line[0] == "#"

      if line =~ /^([01\-]{#{terms.size}}) 1/
        term = $1
        conjunction_kids = []
        terms.size.times do |i|
          if term[i] == "1"
            conjunction_kids << LogicNode.new(LogicNodeType::Term, [terms.fetch(i)])
          elsif term[i] == "0"
            conjunction_kids << LogicNode.new(LogicNodeType::Not, [LogicNode.new(LogicNodeType::Term, [terms.fetch(i)])])
          else
            raise "unexpected" unless term[i] == "-"
          end
        end
        if conjunction_kids.size == 1
          sop_terms << conjunction_kids.fetch(0)
        elsif conjunction_kids.size > 0
          sop_terms << LogicNode.new(LogicNodeType::And, conjunction_kids)
        else
          # always true
          always_true = true
        end
      end
    end

    sop =
      if sop_terms.size == 1
        sop_terms.fetch(0)
      elsif sop_terms.size > 0
        LogicNode.new(LogicNodeType::Or, sop_terms)
      else
        always_true ? LogicNode.new(LogicNodeType::True, []) : LogicNode.new(LogicNodeType::False, [])
      end

    if result_type == CanonicalizationType::SumOfProducts
      sop
    else
      # result is actually !result, so negate it and then distribute
      LogicNode.new(LogicNodeType::Not, [sop]).distribute_not
    end
  end

end

#eval_cb(callback) ⇒ Object

# File 'lib/udb/logic.rb', line 1697

def eval_cb(callback)
  case @type
  when LogicNodeType::True
    SatisfiedResult::Yes
  when LogicNodeType::False
    SatisfiedResult::No
  when LogicNodeType::Term
    child = T.cast(@children.fetch(0), TermType)
    callback.call(child)
  when LogicNodeType::If
    cond_ext_ret = node_children.fetch(0)
    res = cond_ext_ret.eval_cb(callback)
    if res == SatisfiedResult::Yes
      node_children.fetch(1).eval_cb(callback)
    elsif res == SatisfiedResult::Maybe
      ## if "then" is true, then res doesn't matter....
      node_children.fetch(1).eval_cb(callback) == SatisfiedResult::Yes \
        ? SatisfiedResult::Yes
        : SatisfiedResult::Maybe
    else
      # if antecedent is false, implication is true
      SatisfiedResult::Yes
    end
  when LogicNodeType::Not
    res = node_children.fetch(0).eval_cb(callback)
    case res
    when SatisfiedResult::Yes
      SatisfiedResult::No
    when SatisfiedResult::No
      SatisfiedResult::Yes
    when SatisfiedResult::Maybe
      SatisfiedResult::Maybe
    else
      T.absurd(res)
    end
  when LogicNodeType::And
    yes_cnt = T.let(0, Integer)
    node_children.each do |child|
      res1 = child.eval_cb(callback)
      if res1 == SatisfiedResult::No
        return SatisfiedResult::No
      end

      if res1 == SatisfiedResult::Yes
        yes_cnt += 1
      end
    end
    if yes_cnt == node_children.size
      SatisfiedResult::Yes
    else
      SatisfiedResult::Maybe
    end
  when LogicNodeType::Or
    no_cnt = 0
    node_children.each do |child|
      res1 = child.eval_cb(callback)
      return SatisfiedResult::Yes if res1 == SatisfiedResult::Yes

      no_cnt += 1 if res1 == SatisfiedResult::No
    end
    if no_cnt == node_children.size
      SatisfiedResult::No
    else
      SatisfiedResult::Maybe
    end
  when LogicNodeType::None
    no_cnt = 0
    node_children.each do |child|
      res1 = child.eval_cb(callback)
      return SatisfiedResult::No if res1 == SatisfiedResult::Yes

      no_cnt += 1 if res1 == SatisfiedResult::No
    end
    if no_cnt == node_children.size
      SatisfiedResult::Yes
    else
      SatisfiedResult::Maybe
    end
  when LogicNodeType::Xor
    yes_cnt = T.let(0, Integer)
    has_maybe = T.let(false, T::Boolean)
    node_children.each do |child|
      res1 = child.eval_cb(callback)

      has_maybe ||= (res1 == SatisfiedResult::Maybe)
      yes_cnt += 1 if res1 == SatisfiedResult::Yes
      if yes_cnt > 1
        return SatisfiedResult::No
      end
    end
    if yes_cnt == 1 && !has_maybe
      SatisfiedResult::Yes
    elsif has_maybe
      SatisfiedResult::Maybe
    else
      SatisfiedResult::No
    end
  else
    T.absurd(@type)
  end
end

#failing_conjuncts(eval_cb) ⇒ Object

# File 'lib/udb/logic.rb', line 1676

def failing_conjuncts(eval_cb)
  if @type == LogicNodeType::And
    # Evaluate each original child independently to find failing conjuncts
    child_replace_cb = LogicNode.make_replace_cb do |tn|
      r = eval_cb.call(T.cast(tn.children.fetch(0), TermType))
      case r
      when SatisfiedResult::Yes   then LogicNode::True
      when SatisfiedResult::No    then LogicNode::False
      when SatisfiedResult::Maybe then tn
      else T.absurd(r)
      end
    end
    node_children.select do |child|
      child.replace_terms(child_replace_cb).reduce.type == LogicNodeType::False
    end
  else
    [self]
  end
end

#from_dimacs(dimacs) ⇒ Object

# File 'lib/udb/logic.rb', line 3407

def from_dimacs(dimacs)
  nodes = dimacs.each_line.map do |line|
    if line =~ /^(((-?\d+) )+)0/
      ts = T.let($1.strip.split(" "), T::Array[String])
      if ts.size == 1
        t = ts.fetch(0)
        if t[0] == "-"
          index = t[1..].to_i - 1
          LogicNode.new(
            LogicNodeType::Not,
            [LogicNode.new(LogicNodeType::Term, [terms.fetch(index)])]
          )
        else
          index = t.to_i - 1
          LogicNode.new(LogicNodeType::Term, [terms.fetch(index)])
        end
      else
        LogicNode.new(LogicNodeType::Or,
          ts.map do |t|
            if t[0] == "-"
              i = t[1..].to_i - 1
              LogicNode.new(
                LogicNodeType::Not,
                [LogicNode.new(LogicNodeType::Term, [terms.fetch(i)])]
              )
            else
              i = t.to_i - 1
              LogicNode.new(LogicNodeType::Term, [terms.fetch(i)])
            end
          end
        )
      end
    else
      nil
    end
  end.compact

  if nodes.size == 1
    nodes.fetch(0)
  else
    LogicNode.new(LogicNodeType::And, nodes)
  end
end

#group_by_2 ⇒ Object

# File 'lib/udb/logic.rb', line 2381

def group_by_2
  do_group_by_2(self)
end

#grouped_by_2?(node) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 2356

def grouped_by_2?(node)
  t = node.type
  case t
  when LogicNodeType::And, LogicNodeType::Or
    node.children.size == 2 && \
      grouped_by_2?(node.node_children.fetch(0)) && \
      grouped_by_2?(node.node_children.fetch(1))
  when LogicNodeType::Not
    grouped_by_2?(node.node_children.fetch(0))
  when LogicNodeType::Term
    true
  when LogicNodeType::None, LogicNodeType::If, LogicNodeType::Xor
    raise "?"
  when LogicNodeType::True, LogicNodeType::False
    true
  else
    T.absurd(t)
  end
end

#hash ⇒ Object

# File 'lib/udb/logic.rb', line 1892

def hash
  if @type == LogicNodeType::True
    true.hash
  elsif @type == LogicNodeType::False
    false.hash
  elsif @type == LogicNodeType::Term
    @children[0].to_s.hash
  elsif @type == LogicNodeType::Not
    [:not, node_children.fetch(0).hash].hash
  elsif @type == LogicNodeType::And
    [:and, node_children.map(&:hash)].hash
  elsif @type == LogicNodeType::Or
    [:or, node_children.map(&:hash)].hash
  elsif @type == LogicNodeType::Xor
    [:xor, node_children.map(&:hash)].hash
  elsif @type == LogicNodeType::None
    [:none, node_children.map(&:hash)].hash
  elsif @type == LogicNodeType::If
    [:if, node_children.map(&:hash)].hash
  else
    T.absurd(@type)
  end
end

#literals ⇒ Object

# File 'lib/udb/logic.rb', line 1355

def literals
  @memo.literals ||=
  if @type == LogicNodeType::Term
    [@children.fetch(0)]
  else
    seen = {}
    node_children.each_with_object([]) do |child, result|
      child.literals.each do |t|
        unless seen.key?(t)
          seen[t] = true
          result << t
        end
      end
    end
  end
end

#minimal_unsat_subsets ⇒ Object

# File 'lib/udb/logic.rb', line 3453

def minimal_unsat_subsets
  r = reduce
  c = r.equiv_cnf(raise_on_explosion: false)
  Tempfile.create(%w/formula .cnf/) do |f|
    f.write c.to_dimacs
    f.flush

    Tempfile.create do |rf|
      # run must, re-use the tempfile for the result
      _stdout, status = Open3.capture2(Udb::MustPath.binary, "-o", rf.path, f.path)
      raise "could not find minimal subsets" unless status.success?

      rf.rewind
      result = rf.read

      mus_dimacs = T.let([], T::Array[String])
      cur_dimacs = T.let(nil, T.nilable(String))
      result.each_line do |line|
        if line =~ /MUS #\d+/
          mus_dimacs << cur_dimacs unless cur_dimacs.nil?
          cur_dimacs = ""
        else
          cur_dimacs = T.must(cur_dimacs) + line
        end
      end
      mus_dimacs << T.must(cur_dimacs)

      return mus_dimacs.map { |d| c.from_dimacs(d) }
    end
  end
end

#minimize(result_type) ⇒ Object

# File 'lib/udb/logic.rb', line 1626

def minimize(result_type)
  if terms.size <= 4
    quine_mccluskey(result_type)
  else
    # special-case check for when the formula is large but obviously already minimized
    # added this because espresso runtime for Shcounterenw requirements was painfully long
    if result_type == CanonicalizationType::ProductOfSums && terms.size > 32 && nnf.nested_cnf? && terms.size == literals.size
      equiv_cnf
    else
      espresso(result_type, true)
    end
  end
end

#nested_cnf? ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 2974

def nested_cnf?
  unless @memo.is_nested_cnf.nil?
    return @memo.is_nested_cnf
  end

  ret =
    case @type
    when LogicNodeType::Term, LogicNodeType::True, LogicNodeType::False
      true
    when LogicNodeType::Not
      node_children.fetch(0).type == LogicNodeType::Term
    when LogicNodeType::And
      node_children.all? do |child|
        child.nested_cnf_conjunction_term?(false)
      end
    when LogicNodeType::Or
      # or is only valid if only it recursively contains only literals or disjunctions
      node_children.all? do |child|
        [
          child.type == LogicNodeType::True,
          child.type == LogicNodeType::False,
          child.type == LogicNodeType::Term,
          ((child.type == LogicNodeType::Not) && \
            child.node_children.fetch(0).type == LogicNodeType::Term),
          child.type == LogicNodeType::Or && \
            child.node_children.all? { |grandchild| grandchild.nested_cnf_conjunction_term?(true) }
        ].any?
      end
    when LogicNodeType::Xor, LogicNodeType::If, LogicNodeType::None
      false
    else
      T.absurd(@type)
    end
  @memo.is_nested_cnf = ret
end

#nested_cnf_conjunction_term?(ancestor_or) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 2930

def nested_cnf_conjunction_term?(ancestor_or)
  case @type
  when LogicNodeType::Term, LogicNodeType::True, LogicNodeType::False
    true
  when LogicNodeType::Not
    node_children.fetch(0).type == LogicNodeType::Term
  when LogicNodeType::Or
    node_children.all? do |child|
      [
        child.type == LogicNodeType::True,
        child.type == LogicNodeType::False,
        child.type == LogicNodeType::Term,
        ((child.type == LogicNodeType::Not) && \
          child.node_children.fetch(0).type == LogicNodeType::Term),
        child.type == LogicNodeType::Or && child.nested_cnf_conjunction_term?(true)
      ].any?
    end
  when LogicNodeType::And
    return false if ancestor_or

    node_children.all? do |child|
      [
        child.type == LogicNodeType::True,
        child.type == LogicNodeType::False,
        child.type == LogicNodeType::Term,
        ((child.type == LogicNodeType::Not) && \
          child.node_children.fetch(0).type == LogicNodeType::Term),
        (child.type == LogicNodeType::Or && \
          child.nested_cnf_conjunction_term?(true)),
        (child.type == LogicNodeType::And && \
          child.nested_cnf_conjunction_term?(ancestor_or))
      ].any?
    end
  when LogicNodeType::Xor, LogicNodeType::If, LogicNodeType::None
    false
  else
    T.absurd(@type)
  end
end

#nnf ⇒ Object

# File 'lib/udb/logic.rb', line 2227

def nnf
  do_nnf(self)
end

#nnf? ⇒ Boolean

Returns true iff self is in Negation Normal Form.

Returns:

• (Boolean) —

  true iff self is in Negation Normal Form

# File 'lib/udb/logic.rb', line 2232

def nnf?
  if @type == LogicNodeType::Not
    node_children.fetch(0).type == LogicNodeType::Term
  elsif @type == LogicNodeType::Term
    true
  else
    node_children.all? { |child| child.nnf? }
  end
end

#node_children ⇒ Object

# File 'lib/udb/logic.rb', line 1275

def node_children
  @node_children
end

#partial_evaluate(cb) ⇒ Object

# File 'lib/udb/logic.rb', line 1801

def partial_evaluate(cb)
  case @type
  when LogicNodeType::Term
    res = cb.call(T.cast(@children.fetch(0), TermType))
    if res == SatisfiedResult::Yes
      True
    elsif res == SatisfiedResult::No
      False
    else
      self
    end
  else
    LogicNode.new(@type, node_children.map { |child| child.partial_evaluate(cb) })
  end
end

#reduce ⇒ Object

# File 'lib/udb/logic.rb', line 2612

def reduce
  unless @memo.is_reduced.nil?
    raise "?" unless @memo.is_reduced == true
    return self
  end

  reduced =
    case @type
    when LogicNodeType::And
      reduced = LogicNode.new(LogicNodeType::And, node_children.map { |child| child.reduce })
      # see if there is a false term or a contradiction (a && !a)
      # if so, reduce to false
      must_be_false = reduced.node_children.any? do |child|

        # a false anywhere will make the conjunction false
        child.type == LogicNodeType::False ||

          # a contradiction (a && !a) will make the conjunction false
          (child.type == LogicNodeType::Term &&
            reduced.node_children.any? do |other_child|

              other_child.type == LogicNodeType::Not && \
              other_child.node_children.fetch(0).type == LogicNodeType::Term && \
              child.children.fetch(0) == other_child.node_children.fetch(0).children.fetch(0)
            end)
      end
      if must_be_false
        False
      else

        # eliminate True
        true_reduced_children = reduced.node_children.reject { |c| c.type == LogicNodeType::True }
        if true_reduced_children.size != reduced.children.size
          reduced =
            if true_reduced_children.size == 0
              True
            elsif true_reduced_children.size == 1
              true_reduced_children.fetch(0)
            else
              LogicNode.new(LogicNodeType::And, true_reduced_children)
            end
        end

        reduced
      end
    when LogicNodeType::Or
      reduced = LogicNode.new(LogicNodeType::Or, node_children.map { |child| child.reduce })
      # see if there is a true term or a tautology (a || !a)
      # if so, reduce to true
      must_be_true = reduced.node_children.any? do |child|

        # a true anywhere will make the disjunction true
        child.type == LogicNodeType::True ||

          # a tautology (a || !a) will make the disjunction true
          (child.type == LogicNodeType::Term &&
            reduced.node_children.any? do |other_child|

              other_child.type == LogicNodeType::Not && \
              other_child.node_children.fetch(0).type == LogicNodeType::Term && \
              child.children.fetch(0) == other_child.node_children.fetch(0).children.fetch(0)
            end)
      end
      if must_be_true
        True
      else

        # eliminate False
        false_reduced_children = reduced.node_children.reject { |c| c.type == LogicNodeType::False }
        if false_reduced_children.size != reduced.children.size
          reduced =
            if false_reduced_children.size == 0
              False
            elsif false_reduced_children.size == 1
              false_reduced_children.fetch(0)
            else
              LogicNode.new(LogicNodeType::Or, false_reduced_children)
            end
        end

        reduced
      end
    when LogicNodeType::Xor
      reduced = LogicNode.new(LogicNodeType::Xor, node_children.map { |child| child.reduce })
      xor_with_self = reduced.children.size == 2 &&
        reduced.node_children.fetch(0).type == LogicNodeType::Term &&
        reduced.node_children.fetch(1).type == LogicNodeType::Term &&
        reduced.node_children.fetch(0).children.fetch(0) == reduced.node_children.fetch(1).children.fetch(0)
      if xor_with_self
        # xor with self if always false
        False
      elsif reduced.node_children.all? { |c| c.type == LogicNodeType::True || c.type == LogicNodeType::False }
        # all children are literals: xor is true iff exactly one child is true
        reduced.node_children.count { |c| c.type == LogicNodeType::True } == 1 ? True : False
      else
        reduced
      end
    when LogicNodeType::If
      reduced = LogicNode.new(LogicNodeType::If, node_children.map { |child| child.reduce })
      antecedent = reduced.node_children.fetch(0)
      consequent = reduced.node_children.fetch(1)
      if antecedent.type == LogicNodeType::True
        consequent
      elsif antecedent.type == LogicNodeType::False
        return True
      elsif consequent.type == LogicNodeType::True
        return True
      elsif consequent.type == LogicNodeType::False
        return LogicNode.new(LogicNodeType::Not, [antecedent])
      else
        reduced
      end
    when LogicNodeType::Not
      reduced = LogicNode.new(LogicNodeType::Not, node_children.map { |child| child.reduce })
      child = reduced.node_children.fetch(0)
      if child.type == LogicNodeType::Not
        # !!a = a
        reduced.node_children.fetch(0).node_children.fetch(0)
      elsif child.type == LogicNodeType::False
        # !false = true
        return True
      elsif child.type == LogicNodeType::True
        # !true = false
        return False
      else
        reduced
      end
    when LogicNodeType::None
      if node_children.any? { |c| c.type == LogicNodeType::True }
        True
      else
        self.dup
      end
    when LogicNodeType::True, LogicNodeType::False, LogicNodeType::Term
      self
    else
      T.absurd(@type)
    end

  if reduced.memo.is_reduced.nil?
    reduced.memo.is_reduced = true
  end
  reduced
end

#replace_terms(callback) ⇒ Object

# File 'lib/udb/logic.rb', line 1658

def replace_terms(callback)
  case @type
  when LogicNodeType::True, LogicNodeType::False
    self
  when LogicNodeType::Term
    callback.call(self)
  when LogicNodeType::If, LogicNodeType::Not, LogicNodeType::And,
       LogicNodeType::Or, LogicNodeType::None, LogicNodeType::Xor
    LogicNode.new(
      @type,
      node_children.map { |c| c.replace_terms(callback) }
    )
  else
    T.absurd(@type)
  end
end

#satisfiability_depends_on_ext_req?(ext_req) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 1302

def satisfiability_depends_on_ext_req?(ext_req)
  # the tree needs something in ext_vers if it is always
  # unsatisfiable when the corresponding ExtensionTerms are false
  cb = LogicNode.make_eval_cb do |term|
    case term
    when ExtensionTerm
      ext_req.satisfied_by?(term.to_ext_req(ext_req.cfg_arch)) \
        ? SatisfiedResult::No
        : SatisfiedResult::Maybe
    when ParameterTerm
      SatisfiedResult::Maybe
    when FreeTerm
      SatisfiedResult::No
    when XlenTerm
      SatisfiedResult::Maybe
    else
      T.absurd(term)
    end
  end
  eval_cb(cb) == SatisfiedResult::No
end

#satisfiable?(cfg_arch) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 3059

def satisfiable?(cfg_arch)
  @memo.is_satisfiable ||=
    begin
      nterms = terms.size

      if nterms < 8 && literals.size <= 128
        # just brute force it
        LogicNode.inc_brute_force_sat_solves
        term_idx = T.let({}, T::Hash[TermType, Integer])
        terms.each_with_index do |term, idx|
          term_idx[term] = idx
        end
        # define the callback outside the loop to avoid allocating a new block on every iteration
        val_out_of_loop = 0
        cb = LogicNode.make_eval_cb do |term|
          ((val_out_of_loop >> term_idx.fetch(term)) & 1).zero? ? SatisfiedResult::No : SatisfiedResult::Yes
        end

        if nterms.zero?
          return eval_cb(cb) == SatisfiedResult::Yes
        else
          (2**nterms).to_i.times do |i|
            val_out_of_loop = i
            if eval_cb(cb) == SatisfiedResult::Yes
              return true
            end
          end
        end
        return false

      else
        # use SAT solver
        LogicNode.inc_z3_sat_solves

        @@cache ||= {}
        cache_key = [hash, cfg_arch.hash].hash
        if @@cache.key?(cache_key)
          LogicNode.inc_z3_cache_hits
          return @@cache[cache_key]
        end

        solver = Z3Solver.new
        solver.assert to_z3(cfg_arch, solver)
        @@cache[cache_key] = solver.satisfiable?
      end
    end
end

#terms ⇒ Object

# File 'lib/udb/logic.rb', line 1326

def terms
  @memo.terms ||= literals
end

#terms_no_antecendents ⇒ Object

# File 'lib/udb/logic.rb', line 1332

def terms_no_antecendents
  return @memo.terms_no_antecendents unless @memo.terms_no_antecendents.nil?

  @memo.terms_no_antecendents =
    if @type == LogicNodeType::If
      node_children.fetch(1).terms_no_antecendents
    elsif @type == LogicNodeType::Term
      [T.cast(@children.fetch(0), TermType)]
    else
      seen = {}
      node_children.each_with_object([]) do |child, result|
        child.terms_no_antecendents.each do |t|
          unless seen.key?(t)
            seen[t] = true
            result << t
          end
        end
      end
    end
end

#to_asciidoc(include_versions:) ⇒ Object

# File 'lib/udb/logic.rb', line 1979

def to_asciidoc(include_versions:)
  case @type
  when LogicNodeType::Term
    term = T.cast(children.fetch(0), TermType)
    if term.is_a?(ExtensionTerm)
      if include_versions
        "`#{term.name}`#{term.comparison}#{term.version.canonical}"
      else
        "`#{term.name}`"
      end
    elsif term.is_a?(ParameterTerm)
      term.to_asciidoc
    elsif term.is_a?(FreeTerm)
      raise "Should not occur"
    elsif term.is_a?(XlenTerm)
      term.to_asciidoc
    else
      T.absurd(term)
    end
  when LogicNodeType::False
    "false"
  when LogicNodeType::True
    "true"
  when LogicNodeType::Not
    if node_children.fetch(0).type == LogicNodeType::Term
      term = node_children.fetch(0).children.fetch(0)
      if term.is_a?(ParameterTerm)
        negation = term.negate
        unless negation.nil?
          return negation.to_asciidoc
        end
      end
    end
    "!#{node_children.fetch(0).to_asciidoc(include_versions:)}"
  when LogicNodeType::And
    "++(++#{node_children.map { |c| c.to_asciidoc(include_versions:) }.join(" && ")})"
  when LogicNodeType::Or
    "++(++#{node_children.map { |c| c.to_asciidoc(include_versions:) }.join(" pass:[||] ")})"
  when LogicNodeType::If
    "++(++#{node_children.fetch(0).to_asciidoc(include_versions:)} -> #{node_children.fetch(1).to_asciidoc(include_versions:)})"
  when LogicNodeType::Xor
    "++(++#{node_children.map { |c| c.to_asciidoc(include_versions:) }.join(" ࣷ ")})"
  when LogicNodeType::None
    "!++(++#{node_children.map { |c| c.to_asciidoc(include_versions:) }.join(" pass:[||] ")})"
  else
    T.absurd(@type)
  end
end

#to_dimacs ⇒ Object

# File 'lib/udb/logic.rb', line 3366

def to_dimacs
  if @type == LogicNodeType::Term
    <<~DIMACS
      p cnf 1 1
      1 0
    DIMACS
  elsif @type == LogicNodeType::Not && node_children.fetch(0).type == LogicNodeType::Term
    <<~DIMACS
      p cnf 1 1
      -1 0
    DIMACS
  elsif @type == LogicNodeType::True || @type == LogicNodeType::False
    raise "Cannot represent true/false in DIMACS"
  elsif @type == LogicNodeType::And
    lines = ["p cnf #{terms.size} #{@children.size}"]
    lines += node_children.map do |child|
      if child.type == LogicNodeType::Or
        term_line = child.node_children.map do |grandchild|
          if grandchild.type == LogicNodeType::Not
            (-(T.must(terms.index(grandchild.node_children.fetch(0).node_children.fetch(0))) + 1)).to_s
          elsif grandchild.type == LogicNodeType::Term
            (T.must(terms.index(grandchild.node_children.fetch(0))) + 1).to_s
          end
        end.join(" ")
        "#{term_line} 0"
      elsif child.type == LogicNodeType::Term
        "#{T.must(terms.index(child.children.fetch(0))) + 1} 0"
      elsif child.type == LogicNodeType::Not
        "-#{T.must(terms.index(child.node_children.fetch(0).children.fetch(0))) + 1} 0"
      else
        raise "Not CNF"
      end
    end

    lines.join("\n")
  else
    raise "Not CNF"
  end
end

#to_eqntott ⇒ Object

# File 'lib/udb/logic.rb', line 3202

def to_eqntott
  next_term_name = "a"
  term_map = T.let({}, T::Hash[TermType, String])
  t = terms
  t.each do |term|
    unless term_map.key?(term)
      term_map[term] = next_term_name
      next_term_name = next_term_name.next
    end
  end

  EqntottResult.new(eqn: "out = #{do_to_eqntott(self, term_map)}", term_map: term_map.invert)
end

#to_h(term_determined = false) ⇒ Object

# File 'lib/udb/logic.rb', line 2054

def to_h(term_determined = false)
  if @type == LogicNodeType::True
    true
  elsif @type == LogicNodeType::False
    false
  elsif @type == LogicNodeType::Term
    if term_determined
      @children.fetch(0).to_h
    else
      child = T.cast(@children.fetch(0), TermType)
      case child
      when ExtensionTerm
        { "extension" => @children.fetch(0).to_h }
      when ParameterTerm
        { "param" => @children.fetch(0).to_h }
      when FreeTerm
        { "free" => child.id } # only needed for #hash
      when XlenTerm
        @children.fetch(0).to_h
      else
        T.absurd(child)
      end
    end
  elsif @type == LogicNodeType::Not
    child = node_children.fetch(0)
    if !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ExtensionTerm) }
      { "extension" => { "not" => child.to_h(true) } }
    elsif !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ParameterTerm) }
      { "param" => { "not" => child.to_h(true) } }
    else
      { "not" => child.to_h(term_determined) }
    end
  elsif @type == LogicNodeType::And
    if !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ExtensionTerm) }
      { "extension" => { "allOf" => node_children.map { |child| child.to_h(true) } } }
    elsif !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ParameterTerm) }
      { "param" => { "allOf" => node_children.map { |child| child.to_h(true) } } }
    else
      { "allOf" => node_children.map { |child| child.to_h(term_determined) } }
    end
  elsif @type == LogicNodeType::Or
    if !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ExtensionTerm) }
      { "extension" => { "anyOf" => node_children.map { |child| child.to_h(true) } } }
    elsif !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ParameterTerm) }
      { "param" => { "anyOf" => node_children.map { |child| child.to_h(true) } } }
    else
      { "anyOf" => node_children.map { |child| child.to_h(term_determined) } }
    end
  elsif @type == LogicNodeType::Xor
    if !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ExtensionTerm) }
      { "extension" => { "oneOf" => node_children.map { |child| child.to_h(true) } } }
    elsif !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ParameterTerm) }
      { "param" => { "oneOf" => node_children.map { |child| child.to_h(true) } } }
    else
      { "oneOf" => node_children.map { |child| child.to_h(term_determined) } }
    end
  elsif @type == LogicNodeType::None
    if !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ExtensionTerm) }
      { "extension" => { "noneOf" => node_children.map { |child| child.to_h(true) } } }
    elsif !term_determined && terms_no_antecendents.all? { |term| term.is_a?(ParameterTerm) }
      { "param" => { "noneOf" => node_children.map { |child| child.to_h(true) } } }
    else
      { "noneOf" => node_children.map { |child| child.to_h(term_determined) } }
    end
  elsif @type == LogicNodeType::If
    {
      "if" => node_children.fetch(0).to_h(false),
      "then" => node_children.fetch(1).to_h(term_determined)
    }
  else
    T.absurd(@type)
  end
end

#to_idl(cfg_arch) ⇒ Object

# File 'lib/udb/logic.rb', line 2029

def to_idl(cfg_arch)
  case @type
  when LogicNodeType::True
    "true"
  when LogicNodeType::False
    "false"
  when LogicNodeType::Term
    T.cast(@children.fetch(0), TermType).to_idl(cfg_arch)
  when LogicNodeType::Not
    "!#{node_children.fetch(0).to_idl(cfg_arch)}"
  when LogicNodeType::And
    "(#{node_children.map { |c| c.to_idl(cfg_arch) }.join(" && ") })"
  when LogicNodeType::Or
    "(#{node_children.map { |c| c.to_idl(cfg_arch) }.join(" || ")})"
  when LogicNodeType::Xor, LogicNodeType::None
    nnf.to_idl(cfg_arch)
  when LogicNodeType::If
    "(!(#{node_children.fetch(0).to_idl(cfg_arch)}) || (#{node_children.fetch(1).to_idl(cfg_arch)}))"
  else
    T.absurd(@type)
  end
end

#to_s(format: LogicSymbolFormat::Predicate) ⇒ Object

# File 'lib/udb/logic.rb', line 1917

def to_s(format: LogicSymbolFormat::Predicate)
  if @type == LogicNodeType::True
    LOGIC_SYMBOLS[format][:TRUE]
  elsif @type == LogicNodeType::False
    LOGIC_SYMBOLS[format][:FALSE]
  elsif @type == LogicNodeType::Term
    @children[0].to_s
  elsif @type == LogicNodeType::Not
    "#{LOGIC_SYMBOLS[format][:NOT]}#{node_children.fetch(0).to_s(format:)}"
  elsif @type == LogicNodeType::And
    "(#{node_children.map { |c| c.to_s(format:) }.join(" #{LOGIC_SYMBOLS[format][:AND]} ")})"
  elsif @type == LogicNodeType::Or
    "(#{node_children.map { |c| c.to_s(format:) }.join(" #{LOGIC_SYMBOLS[format][:OR]} ")})"
  elsif @type == LogicNodeType::Xor
    "(#{node_children.map { |c| c.to_s(format:) }.join(" #{LOGIC_SYMBOLS[format][:XOR]} ")})"
  elsif @type == LogicNodeType::None
    "#{LOGIC_SYMBOLS[format][:NOT]}(#{node_children.map { |c| c.to_s(format:) }.join(" #{LOGIC_SYMBOLS[format][:OR]} ")})"
  elsif @type == LogicNodeType::If
    "(#{node_children.fetch(0).to_s(format:)} #{LOGIC_SYMBOLS[format][:IMPLIES]} #{node_children.fetch(1).to_s(format:)})"
  else
    T.absurd(@type)
  end
end

#to_s_pretty ⇒ Object

# File 'lib/udb/logic.rb', line 1867

def to_s_pretty
  if @type == LogicNodeType::True
    "true"
  elsif @type == LogicNodeType::False
    "false"
  elsif @type == LogicNodeType::Term
    @children.fetch(0).to_s_pretty
  elsif @type == LogicNodeType::Not
    "not #{@children.fetch(0).to_s_pretty}"
  elsif @type == LogicNodeType::And
    "(#{node_children.map { |c| c.to_s_pretty }.join(" and ")})"
  elsif @type == LogicNodeType::Or
    "(#{node_children.map { |c| c.to_s_pretty }.join(" or ")})"
  elsif @type == LogicNodeType::Xor
    "(#{node_children.map { |c| c.to_s_pretty }.join(" xor ")})"
  elsif @type == LogicNodeType::None
    "none of (#{node_children.map { |c| c.to_s_pretty }.join(", ")})"
  elsif @type == LogicNodeType::If
    "if #{node_children.fetch(0).to_s_pretty} then #{node_children.fetch(1).to_s_pretty})"
  else
    T.absurd(@type)
  end
end

#to_s_with_value(callback, format: LogicSymbolFormat::Predicate) ⇒ Object

# File 'lib/udb/logic.rb', line 1942

def to_s_with_value(callback, format: LogicSymbolFormat::Predicate)
  if @type == LogicNodeType::True
    LOGIC_SYMBOLS[format][:TRUE]
  elsif @type == LogicNodeType::False
    LOGIC_SYMBOLS[format][:FALSE]
  elsif @type == LogicNodeType::Term
    v = callback.call(T.cast(@children.fetch(0), TermType))
    str =
      case v
      when SatisfiedResult::Yes
        "{true}"
      when SatisfiedResult::No
        "{false}"
      when SatisfiedResult::Maybe
        "{unknown}"
      else
        T.absurd(v)
      end
    "`#{@children.fetch(0)}`#{str}"
  elsif @type == LogicNodeType::Not
    "#{LOGIC_SYMBOLS[format][:NOT]}#{node_children.fetch(0).to_s_with_value(callback, format:)}"
  elsif @type == LogicNodeType::And
    "(#{node_children.map { |c| c.to_s_with_value(callback, format:) }.join(" #{LOGIC_SYMBOLS[format][:AND]} ")})"
  elsif @type == LogicNodeType::Or
    "(#{node_children.map { |c| c.to_s_with_value(callback, format:) }.join(" #{LOGIC_SYMBOLS[format][:OR]} ")})"
  elsif @type == LogicNodeType::Xor
    "(#{node_children.map { |c| c.to_s_with_value(callback, format:) }.join(" #{LOGIC_SYMBOLS[format][:XOR]} ")})"
  elsif @type == LogicNodeType::None
    "#{LOGIC_SYMBOLS[format][:NOT]}(#{node_children.map { |c| c.to_s_with_value(callback, format:) }.join(" #{LOGIC_SYMBOLS[format][:OR]} ")})"
  elsif @type == LogicNodeType::If
    "(#{node_children.fetch(0).to_s_with_value(callback, format:)} #{LOGIC_SYMBOLS[format][:IMPLIES]} #{node_children.fetch(1).to_s_with_value(callback, format:)})"
  else
    T.absurd(@type)
  end
end

#to_z3(cfg_arch, solver = Z3Solver.new) ⇒ Object

# File 'lib/udb/logic.rb', line 3011

def to_z3(cfg_arch, solver = Z3Solver.new)
  case @type
  when LogicNodeType::Term
    t = @children.fetch(0)
    if t.is_a?(ParameterTerm) || t.is_a?(ExtensionTerm)
      t.to_z3(solver, cfg_arch)
    elsif t.is_a?(FreeTerm)
      t.to_z3
    else
      raise "unexpected #{self}" if t.is_a?(LogicNode)

      t.to_z3(solver)
    end
  when LogicNodeType::Or
    T.unsafe(Z3).Or(*node_children.map { |c| c.to_z3(cfg_arch, solver) })
  when LogicNodeType::And
    T.unsafe(Z3).And(*node_children.map { |c| c.to_z3(cfg_arch, solver) })
  when LogicNodeType::Xor
    if node_children.size == 2
      T.unsafe(Z3).Xor(*node_children.map { |c| c.to_z3(cfg_arch, solver) })
    else
      # see https://stackoverflow.com/questions/14888174/how-do-i-determine-if-exactly-one-boolean-is-true-without-type-conversion#33268481
      uneven_number_is_true = T.unsafe(Z3).Xor(*node_children.map { |c| c.to_z3(cfg_arch, solver) })
      max_one_is_true =
        T.unsafe(Z3).And(
          *node_children.combination(2).map do |pair|
            !(pair.fetch(0).to_z3(cfg_arch, solver) & pair.fetch(1).to_z3(cfg_arch, solver))
          end
        )
      uneven_number_is_true & max_one_is_true
    end
  when LogicNodeType::True
    Z3.True
  when LogicNodeType::False
    Z3.False
  when LogicNodeType::Not
    !node_children.fetch(0).to_z3(cfg_arch, solver)
  when LogicNodeType::None
    !node_children.map { |c| c.to_z3(cfg_arch, solver) }.reduce(:|)
  when LogicNodeType::If
    node_children.fetch(0).to_z3(cfg_arch, solver).implies(node_children.fetch(1).to_z3(cfg_arch, solver))
  else
    T.absurd(@type)
  end
end

#tseytin ⇒ Object

# File 'lib/udb/logic.rb', line 3347

def tseytin
  subformulae = []
  r = reduce
  return r if [LogicNodeType::Term, LogicNodeType::True, LogicNodeType::False].any?(r.type)

  grouped = r.group_by_2
  grouped.collect_tseytin(subformulae)

  if subformulae.size == 0
    raise "? #{r}"
  elsif subformulae.size == 1
    subformulae.fetch(0)
  else
    equisatisfiable_formula = LogicNode.new(LogicNodeType::And, subformulae + [grouped.tseytin_prop])
    flatten_cnf(equisatisfiable_formula).reduce
  end
end

#tseytin_prop ⇒ Object

# File 'lib/udb/logic.rb', line 3335

def tseytin_prop
  case @type
  when LogicNodeType::Term, LogicNodeType::True, LogicNodeType::False
    self
  else
    @tseytin_prop ||=
      LogicNode.new(LogicNodeType::Term, [FreeTerm.new])
  end
end

#unsatisfiable?(cfg_arch) ⇒ Boolean

Returns:

• (Boolean)

# File 'lib/udb/logic.rb', line 3109

def unsatisfiable?(cfg_arch) = !satisfiable?(cfg_arch)