kdrag.smt

Reexported z3 functionality <https://z3prover.github.io/api/html/namespacez3py.html> This is a shim file to enable the use of cvc5 and vampire as default solvers. This is controlled by setting the environment variable KNUCKLE_SOLVER to “cvc5” or “vampire” before importing knuckledragger.

Functions

`BoolSort`([ctx])
`DeclareSort`(name)	Declare a sort with the given name.
`Eq`(x, y)	Python __eq__ resolution rules flips the order if y is a subclass of x.
`Function`(args, *kwargs)
`IntSort`([ctx])
`RealSort`([ctx])
`arg`(self, i)
`decl`(self)
`eq`(x, y)
`expr_kind`(self)
`func_kind`(self)
`get_id`(self)
`is_accessor`(x)	Check if an expression is an accessor.
`is_app`(self)
`is_constructor`(x)	Check if an expression is a constructor.
`is_if`(x)	Check if an expression is an if-then-else.
`is_neg`(x)	Check if an expression is a negation.
`is_power`(x)	Check if an expression is a power.
`is_recognizer`(x)	Check if recognizer.
`is_uninterp`(x)	Check if uninterpreted function.
`num_args`(self)
`sort`(self)
`sort_kind`(self)

kdrag.smt.BoolSort(ctx=None) → SortRef

Return type:: SortRef

kdrag.smt.DeclareSort(name): Declare a sort with the given name. >>> DeclareSort(“MySort”) MySort

kdrag.smt.Eq(x, y)

Python __eq__ resolution rules flips the order if y is a subclass of x. This function corrects that.

>>> IntVal(1) + IntVal(2) == IntVal(3)
3 == 1 + 2
>>> Eq(IntVal(1) + IntVal(2), IntVal(3))
1 + 2 == 3

kdrag.smt.Function(*args, **kwargs)

kdrag.smt.IntSort(ctx=None) → SortRef

Return type:: SortRef

kdrag.smt.RealSort(ctx=None) → SortRef

Return type:: SortRef

kdrag.smt.arg(self, i)

kdrag.smt.decl(self)

kdrag.smt.eq(x, y)

kdrag.smt.expr_kind(self)

kdrag.smt.func_kind(self)

kdrag.smt.get_id(self)

kdrag.smt.is_accessor(x: ExprRef) → bool

Check if an expression is an accessor. >>> Color = z3.Datatype(“Color”) >>> Color.declare(“red”, (“r”, z3.IntSort())) >>> Color = Color.create() >>> is_accessor(Color.r(Color.red(3))) True

Parameters:: x (ExprRef)
Return type:: bool

kdrag.smt.is_app(self)

kdrag.smt.is_constructor(x: ExprRef) → bool

Check if an expression is a constructor. >>> Color = z3.Datatype(“Color”) >>> Color.declare(“red”) >>> Color = Color.create() >>> is_constructor(Color.red) True

Parameters:: x (ExprRef)
Return type:: bool

kdrag.smt.is_if(x: ExprRef) → bool

Check if an expression is an if-then-else. >>> is_if(z3.If(True, 1, 2)) True

Parameters:: x (ExprRef)
Return type:: bool

kdrag.smt.is_neg(x: ExprRef) → bool

Check if an expression is a negation. >>> x = z3.Int(“x”) >>> is_neg(-x) True

Parameters:: x (ExprRef)
Return type:: bool

kdrag.smt.is_power(x: ExprRef) → bool

Check if an expression is a power. >>> x = z3.Real(“x”) >>> is_power(x**3) True

Parameters:: x (ExprRef)
Return type:: bool

kdrag.smt.is_recognizer(x: ExprRef) → bool

Check if recognizer. >>> Color = z3.Datatype(“Color”) >>> Color.declare(“red”) >>> Color = Color.create() >>> is_recognizer(Color.is_red(Color.red)) True

Parameters:: x (ExprRef)
Return type:: bool

kdrag.smt.is_uninterp(x: ExprRef) → bool

Check if uninterpreted function. >>> x = z3.Real(“x”) >>> f = z3.Function(“f”, RealSort(), RealSort()) >>> is_uninterp(x) True >>> is_uninterp(f(x)) True >>> is_uninterp(x + 1) False >>> is_uninterp(z3.RealVal(42.1)) False

Parameters:: x (ExprRef)
Return type:: bool

kdrag.smt.num_args(self)

kdrag.smt.sort(self)

kdrag.smt.sort_kind(self)