Class: Udb::Z3ExtensionRequirement

Inherits:

Object

• Object
• Udb::Z3ExtensionRequirement

Extended by:

T::Sig

Defined in:

lib/udb/z3.rb

Instance Method Summary

• #initialize(name, req, solver, cfg_arch) constructor
• #term ⇒ Z3::BoolExpr

Constructor Details

#initialize(name, req, solver, cfg_arch)

Parameters:

• name (String)
• req (RequirementSpec, Array<RequirementSpec>)
• solver (Z3Solver)
• cfg_arch (ConfiguredArchitecture)

# File 'lib/udb/z3.rb', line 431

def initialize(name, req, solver, cfg_arch)
  @name = name
  @reqs = req
  @solver = solver

  @ext_req = cfg_arch.extension_requirement(name, @reqs)
  vers = @ext_req.satisfying_versions
  @term = Z3.Bool("#{name} #{@reqs.is_a?(Array) ? @reqs.map { |r| r.to_s }.join(", ") : @reqs.to_s}")
  if vers.empty?
    @solver.assert @term.implies(Z3.False)
  else
    if vers.size == 1
      @solver.assert @term.implies(@solver.ext_ver(name, vers.fetch(0).version_spec, cfg_arch).term)
    elsif vers.size == 2
      @solver.assert @term.implies(T.unsafe(Z3).Xor(*vers.map { |v| @solver.ext_ver(name, v.version_spec, cfg_arch).term }))
    else
      uneven_number_is_true = T.unsafe(Z3).Xor(*vers.map { |v| @solver.ext_ver(name, v.version_spec, cfg_arch).term })
      max_one_is_true =
        T.unsafe(Z3).And(
          *vers.combination(2).map do |pair|
            !(@solver.ext_ver(name, pair.fetch(0).version_spec, cfg_arch).term & @solver.ext_ver(name, pair.fetch(1).version_spec, cfg_arch).term)
          end
        )
      @solver.assert @term.implies(uneven_number_is_true & max_one_is_true)
    end
  end
  vers.each do |v|
    @solver.assert @solver.ext_ver(name, v.version_spec, cfg_arch).term.implies(@term)
  end
end

Instance Method Details

#term ⇒ Z3::BoolExpr

Returns:

• (Z3::BoolExpr)

# File 'lib/udb/z3.rb', line 463

def term = @term