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])
`Const`(name, sort)	Create a constant of a given sort.
`Consts`(names, sort)
`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.
`Exists`(vs, concs, *kwargs)	Quantified Exists
`ForAll`(vs, hyp_conc, *kwargs)	Quantified ForAll
`Function`(args, *kwargs)
`IntSort`([ctx])
`RealSort`([ctx])
`arg`(self, i)
`codomain`(f)
`decl`(self)
`domains`(f)	Get the domain sorts of a lambda or an array.
`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_func`(f)	Check if a term is a function or an array.
`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.Const(name: str, sort: SortRef | FuncRef) → ExprRef

Create a constant of a given sort. If a set value is given as the sort, this is treated as a constraint held in the assumes field of the constant. This field may be used by quantifiers.

>>> n = Int("n")
>>> x = Const("x", Lambda([n], n >= 0))
>>> x.assumes
x >= 0

Parameters:

name (str)
sort (SortRef | FuncRef)

Return type:

ExprRef

kdrag.smt.Consts(names: str, sort: SortRef | FuncRef) → list[ExprRef]

>>> n = Int("n")
>>> xs = Consts("x y z", Lambda([n], n >= 0))
>>> [x.assumes for x in xs]
[x >= 0, y >= 0, z >= 0]

Parameters:

names (str)
sort (SortRef | FuncRef)

Return type:

list[ExprRef]

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.Exists(vs: list[ExprRef], *concs, **kwargs) → QuantifierRef

Quantified Exists

Shorthand for Exists(vars, And(conc[0], conc[1], …))

>>> x,y = Ints("x y")
>>> Exists([x,y], x > 0, y > 0)
Exists([x, y], And(x > 0, y > 0))
>>> x = Const("x", Lambda([x], x >= 0))
>>> Exists([x], x > 3)
Exists(x, And(x >= 0, x > 3))

Parameters:: vs (list[ExprRef])
Return type:: QuantifierRef

kdrag.smt.ForAll(vs: list[ExprRef], *hyp_conc, **kwargs) → QuantifierRef

Quantified ForAll

Shorthand for ForAll(vars, Implies(And(hyp[0], hyp[1], …), conc))

>>> x,y = Ints("x y")
>>> ForAll([x,y], x > 0, y > 0, x + y > 0)
ForAll([x, y], Implies(And(x > 0, y > 0), x + y > 0))
>>> x = Const("x", Lambda([x], x >= 0))
>>> ForAll([x], x > 3)
ForAll(x, Implies(x >= 0, x > 3))

Parameters:: vs (list[ExprRef])
Return type:: QuantifierRef

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.codomain(f: FuncRef | ArraySortRef) → SortRef

>>> x = Int("x")
>>> y = Int("y")
>>> f = Array("f", IntSort(), RealSort())
>>> codomain(f)
Real
>>> lam = Lambda([x, y], x + y)
>>> codomain(lam)
Int

Parameters:: f (FuncRef | ArraySortRef)
Return type:: SortRef

kdrag.smt.decl(self)

kdrag.smt.domains(f: FuncRef | ArraySortRef) → list[SortRef]

Get the domain sorts of a lambda or an array.

>>> x = Int("x")
>>> y = Real("y")
>>> f = Array("f", IntSort(), RealSort(), IntSort())
>>> domains(f)
[Int, Real]
>>> lam = Lambda([x, y], x + y)
>>> domains(lam)
[Int, Real]

Parameters:: f (FuncRef | ArraySortRef)
Return type:: list[SortRef]

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_func(f: ExprRef) → bool

Check if a term is a function or an array.

>>> x = Int("x")
>>> assert is_func(Lambda([x], x))

Parameters:: f (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)