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.



986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
 
# File 'lib/udb/z3.rb', line 986

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.



983
984
985
 
# File 'lib/udb/z3.rb', line 983

def term
  @term
end

Instance Method Details

#!=(ver) ⇒ Object 



1017
1018
1019
1020
1021
 
# File 'lib/udb/z3.rb', line 1017

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 



1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
 
# File 'lib/udb/z3.rb', line 1064

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 



1054
1055
1056
1057
1058
 
# File 'lib/udb/z3.rb', line 1054

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

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

#==(ver) ⇒ Object 



1010
1011
1012
1013
1014
 
# File 'lib/udb/z3.rb', line 1010

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 



1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
 
# File 'lib/udb/z3.rb', line 1036

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 



1024
1025
1026
1027
1028
 
# File 'lib/udb/z3.rb', line 1024

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

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