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.



901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
 
# File 'lib/udb/z3.rb', line 901

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 



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

def term = @term