Class: Udb::Z3Solver

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

Instance Method Summary collapse

Constructor Details

#initialize ⇒ Z3Solver

Returns a new instance of Z3Solver.



566
567
568
569
570
571
572
573
574
575
576
 
# File 'lib/udb/z3.rb', line 566

def initialize
  @solver = Z3::Solver.new
  @ext_vers = T.let({}, T::Hash[String, Z3ExtensionVersion])
  @ext_reqs = T.let({}, T::Hash[String, Z3ExtensionRequirement])
  @param_terms = T.let({}, T::Hash[String, Z3ParameterTerm])

  @ext_majors = T.let({}, T::Hash[String, Z3::IntExpr])
  @ext_minors = T.let({}, T::Hash[String, Z3::IntExpr])
  @ext_patches = T.let({}, T::Hash[String, Z3::IntExpr])
  @ext_pres = T.let({}, T::Hash[String, Z3::IntExpr])
end

Instance Method Details

#ext_major(name) ⇒ Z3::IntExpr

Parameters:

  • name (String)

Returns:

  • (Z3::IntExpr) 


615
616
617
 
# File 'lib/udb/z3.rb', line 615

def ext_major(name)
  @ext_majors[name] ||= Z3.Int("#{name}_major")
end

#ext_minor(name) ⇒ Z3::IntExpr

Parameters:

  • name (String)

Returns:

  • (Z3::IntExpr) 


620
621
622
 
# File 'lib/udb/z3.rb', line 620

def ext_minor(name)
  @ext_minors[name] ||= Z3.Int("#{name}_minor")
end

#ext_patch(name) ⇒ Z3::IntExpr

Parameters:

  • name (String)

Returns:

  • (Z3::IntExpr) 


625
626
627
 
# File 'lib/udb/z3.rb', line 625

def ext_patch(name)
  @ext_patches[name] ||= Z3.Int("#{name}_patch")
end

#ext_pre(name) ⇒ Z3::BoolExpr

Parameters:

  • name (String)

Returns:

  • (Z3::BoolExpr) 


630
631
632
 
# File 'lib/udb/z3.rb', line 630

def ext_pre(name)
  @ext_pres[name] ||= Z3.Bool("#{name}_pre")
end

#ext_req(name, req, cfg_arch) ⇒ Z3ExtensionRequirement

Parameters:

Returns:



609
610
611
612
 
# File 'lib/udb/z3.rb', line 609

def ext_req(name, req, cfg_arch)
  key = [name, req].hash
  @ext_reqs[key] ||= Z3ExtensionRequirement.new(name, req, self, cfg_arch)
end

#ext_ver(name, version, cfg_arch) ⇒ Z3ExtensionVersion

Parameters:

Returns:



598
599
600
601
602
603
604
605
606
 
# File 'lib/udb/z3.rb', line 598

def ext_ver(name, version, cfg_arch)
  version_spec = version.is_a?(VersionSpec) ? version : VersionSpec.new(version)
  key = [name, version_spec].hash
  if @ext_vers.key?(key)
    @ext_vers.fetch(key)
  else
    @ext_vers[key] = Z3ExtensionVersion.new(name, version_spec, self, cfg_arch)
  end
end

#param(name, schema_hsh) ⇒ Z3ParameterTerm

Parameters:

  • name (String)
  • schema_hsh (Hash{String => T.untyped})

Returns:



636
637
638
639
640
641
642
 
# File 'lib/udb/z3.rb', line 636

def param(name, schema_hsh)
  if @param_terms.key?(name)
    @param_terms.fetch(name)
  else
    @param_terms[name] = Z3ParameterTerm.new(name, self, schema_hsh)
  end
end

#pop ⇒ Object 



578
579
580
581
582
583
584
585
586
 
# File 'lib/udb/z3.rb', line 578

def pop
  @ext_vers.clear
  @ext_reqs.clear
  @ext_majors.clear
  @ext_minors.clear
  @ext_patches.clear
  @ext_pres.clear
  @solver.pop
end

#xlen ⇒ Z3::IntExpr

Returns:

  • (Z3::IntExpr) 


589
590
591
592
593
594
595
 
# File 'lib/udb/z3.rb', line 589

def xlen
  unless @xlen
    @xlen = Z3.Int("xlen")
    @solver.assert((@xlen == 32) | (@xlen == 64))
  end
  @xlen
end