Class: Z3::Solver

Inherits:

Object

• Object
• Z3::Solver

Extended by:

T::Sig

Defined in:

lib/udb/z3.rb

Overview

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

Instance Method Summary

• #assert_as(ast, name)

  Assert an expression and track it with a name for unsat core analysis.

Instance Method Details

#assert_as(ast, name)

This method returns an undefined value.

Assert an expression and track it with a name for unsat core analysis

This method extends Z3::Solver to support named assertions, which is useful for debugging when a set of constraints is unsatisfiable. The name appears in the unsat core, helping identify which constraints conflict.

Parameters:

• ast (Z3::Expr) —

  The boolean expression to assert

• name (String) —

  A descriptive name for this assertion (used in unsat cores)

# 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