Class: Udb::Z3ExtensionVersion

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

Overview

Models a specific RISC-V extension version in Z3

Represents a concrete extension version (e.g., “Zicsr@2.0.0”) as:

  • A boolean term indicating if this version is present

  • Integer terms for major, minor, patch version components

  • A boolean term for pre-release status

The version term implies constraints on the component terms, allowing version comparison operations (==, !=, <, <=, >, >=) to work correctly.

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(name, version, solver, cfg_arch) ⇒ Z3ExtensionVersion

Returns a new instance of Z3ExtensionVersion.



964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
 
# File 'lib/udb/z3.rb', line 964

def initialize(name, version, solver, cfg_arch)
  @name = name
  @solver = T.let(solver, Z3Solver)
  @term = T.let(Z3::Bool("#{name}@#{version}"), Z3::BoolExpr)
  @major_term = T.let(solver.ext_major(name), Z3::IntExpr)
  @minor_term = T.let(solver.ext_minor(name), Z3::IntExpr)
  @patch_term = T.let(solver.ext_patch(name), Z3::IntExpr)
  @pre_term = T.let(solver.ext_pre(name), Z3::BoolExpr)

  # If this version is present, constrain the component terms
  @solver.assert @term.implies(
    Z3.And(
      @major_term == version.major,
      @minor_term == version.minor,
      @patch_term == version.patch,
      @pre_term == version.pre,
    )
  )
end

Instance Attribute Details

#term ⇒ Object (readonly)

Returns the value of attribute term.



961
962
963
 
# File 'lib/udb/z3.rb', line 961

def term
  @term
end

Instance Method Details

#!=(ver) ⇒ Object 



995
996
997
998
999
 
# File 'lib/udb/z3.rb', line 995

def !=(ver)
  ver_spec = ver.is_a?(VersionSpec) ? ver : VersionSpec.new(ver)

  Z3.Or((@major_term != ver_spec.major), (@minor_term != ver_spec.minor), (@patch_term != ver_spec.patch), (@pre_term != ver_spec.pre))
end

#<(ver) ⇒ Object 



1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
 
# File 'lib/udb/z3.rb', line 1042

def <(ver)
  ver_spec = ver.is_a?(VersionSpec) ? ver : VersionSpec.new(ver)

  e =
    Z3.Or(
      (@major_term < ver_spec.major),
      ((@major_term == ver_spec.major) & (@minor_term < ver_spec.minor)),
      Z3.And((@major_term == ver_spec.major), (@minor_term == ver_spec.minor), (@patch_term < ver_spec.patch))
    )
  # Handle pre-release comparison: if comparing to a release, a pre-release version is less
  if ver_spec.pre
    e
  else
    e | Z3.And((@major_term == ver_spec.major), (@minor_term == ver_spec.minor), (@patch_term == ver_spec.patch), (@pre_term))
  end
end

#<=(ver) ⇒ Object 



1032
1033
1034
1035
1036
 
# File 'lib/udb/z3.rb', line 1032

def <=(ver)
  ver_spec = ver.is_a?(VersionSpec) ? ver : VersionSpec.new(ver)

  (self == ver) | (self < ver)
end

#==(ver) ⇒ Object 



988
989
990
991
992
 
# File 'lib/udb/z3.rb', line 988

def ==(ver)
  ver_spec = ver.is_a?(VersionSpec) ? ver : VersionSpec.new(ver)

  Z3.And((@major_term == ver_spec.major), (@minor_term == ver_spec.minor), (@patch_term == ver_spec.patch), (@pre_term == ver_spec.pre))
end

#>(ver) ⇒ Object 



1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
 
# File 'lib/udb/z3.rb', line 1014

def >(ver)
  ver_spec = ver.is_a?(VersionSpec) ? ver : VersionSpec.new(ver)

  e =
    Z3.Or(
      (@major_term > ver_spec.major),
      ((@major_term == ver_spec.major) & (@minor_term > ver_spec.minor)),
      Z3.And((@major_term == ver_spec.major), (@minor_term == ver_spec.minor), (@patch_term > ver_spec.patch))
    )
  # Handle pre-release comparison: if comparing to a pre-release, a release version is greater
  if ver_spec.pre
    e & Z3.And((@major_term == ver_spec.major), (@minor_term == ver_spec.minor), (@patch_term == ver_spec.patch), (!@pre_term))
  else
    e
  end
end

#>=(ver) ⇒ Object 



1002
1003
1004
1005
1006
 
# File 'lib/udb/z3.rb', line 1002

def >=(ver)
  ver_spec = ver.is_a?(VersionSpec) ? ver : VersionSpec.new(ver)

  (self == ver) | (self > ver)
end