Class: Udb::Z3ExtensionRequirement

Inherits:
Object
  • Object
show all
Extended by:
T::Sig
Defined in:
lib/udb/z3.rb

Overview

Models a RISC-V extension requirement in Z3

An extension requirement specifies that an extension must satisfy certain version constraints (e.g., ">=1.0.0", "~>2.0"). This class:

  1. Finds all extension versions that satisfy the requirement
  2. Creates a Z3 boolean term representing the requirement
  3. Asserts that the requirement implies exactly one satisfying version is present

The constraint logic ensures:

  • If no versions satisfy the requirement, the requirement term implies false
  • If versions exist, exactly one must be true (using XOR for mutual exclusivity)
  • If a version is true, the requirement must be true (bidirectional implication)

Instance Method Summary collapse

Constructor Details

#initialize(name, req, solver, cfg_arch) ⇒ Z3ExtensionRequirement

Returns a new instance of Z3ExtensionRequirement.



923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
 
# File 'lib/udb/z3.rb', line 923

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

  @ext_req = T.let(cfg_arch.extension_requirement(name, @reqs), ExtensionRequirement)
  vers = @ext_req.satisfying_versions
  @term = T.let(
    Z3.Bool("#{name} #{@reqs.is_a?(Array) ? @reqs.map { |r| r.to_s }.join(", ") : @reqs.to_s}"),
    Z3::BoolExpr
  )
  if vers.empty?
    # No versions satisfy this requirement, so it can never be true
    @solver.assert @term.implies(Z3.False)
  else
    if vers.size == 1
      # Exactly one version satisfies: requirement iff that version
      @solver.assert @term.implies(@solver.ext_ver(name, vers.fetch(0).version_spec, cfg_arch).term)
    elsif vers.size == 2
      # Two versions: use XOR for mutual exclusivity
      @solver.assert @term.implies(T.unsafe(Z3).Xor(*vers.map { |v| @solver.ext_ver(name, v.version_spec, cfg_arch).term }))
    else
      # Multiple versions: ensure exactly one is true
      # XOR of all versions ensures an odd number are true
      uneven_number_is_true = T.unsafe(Z3).Xor(*vers.map { |v| @solver.ext_ver(name, v.version_spec, cfg_arch).term })
      # Pairwise exclusion ensures at most one is true
      max_one_is_true =
        T.unsafe(Z3).And(
          *vers.combination(2).map do |pair|
            # No two versions can both be true
            !(@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
        )
      # Together: exactly one version is true
      @solver.assert @term.implies(uneven_number_is_true & max_one_is_true)
    end
  end
  # Bidirectional: if a version is present, the requirement is satisfied
  vers.each do |v|
    @solver.assert @solver.ext_ver(name, v.version_spec, cfg_arch).term.implies(@term)
  end
end

Instance Method Details

#term ⇒ Object 



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

def term = @term