Class: Udb::Z3ExtensionVersion

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(name, version, solver, cfg_arch)

Parameters:



473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
 
# File 'lib/udb/z3.rb', line 473

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

  @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 ⇒ Z3::BoolExpr (readonly)

Returns:

  • (Z3::BoolExpr) 


470
471
472
 
# File 'lib/udb/z3.rb', line 470

def term
  @term
end

Instance Method Details

#!=(ver) ⇒ Z3::BoolExpr

Parameters:

Returns:

  • (Z3::BoolExpr) 


500
501
502
503
504
 
# File 'lib/udb/z3.rb', line 500

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) ⇒ Z3::BoolExpr

Parameters:

Returns:

  • (Z3::BoolExpr) 


538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
 
# File 'lib/udb/z3.rb', line 538

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))
    )
  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) ⇒ Z3::BoolExpr

Parameters:

Returns:

  • (Z3::BoolExpr) 


531
532
533
534
535
 
# File 'lib/udb/z3.rb', line 531

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

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

#==(ver) ⇒ Z3::BoolExpr

Parameters:

Returns:

  • (Z3::BoolExpr) 


493
494
495
496
497
 
# File 'lib/udb/z3.rb', line 493

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) ⇒ Z3::BoolExpr

Parameters:

Returns:

  • (Z3::BoolExpr) 


514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
 
# File 'lib/udb/z3.rb', line 514

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))
    )
  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) ⇒ Z3::BoolExpr

Parameters:

Returns:

  • (Z3::BoolExpr) 


507
508
509
510
511
 
# File 'lib/udb/z3.rb', line 507

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

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