Class: Z3::Solver

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

Overview

Extension to the Z3::Solver class to add tracked assertions

Instance Method Summary collapse

Instance Method Details

#assert_as(ast, name) ⇒ Object 



63
64
65
66
67
68
 
# File 'lib/udb/z3.rb', line 63

def assert_as(ast, name)
  reset_model!
  Z3::LowLevel.solver_assert_and_track(
    self,
    ast, Z3::Bool(name))
end