how to combine two probes to a new probe or a new predicates in Z3?

Question

I have two probes in z3 for example

p1 = z3.Probe('num-consts')
p2 = z3.Probe('num-exprs')

and I want to combine these two Probe to the form such as p1/p2 or p1-p2 in a branching statement such as If(), but I don't know how to implement this.

import z3
p1 = z3.Probe('num-consts')
p2 = z3.Probe('num-exprs')
t = z3.If(z3.BoolVal(p1/p2 > 2), z3.Tactic('simplify'), z3.Tactic('factor'))

Answer 1

You should pass the goal to the composite tactic. Here's an example:

import z3

p1 = z3.Probe('num-consts')
p2 = z3.Probe('num-exprs')

def t(g):
    return z3.If(p1(g)/p2(g) > 2, z3.Tactic('simplify'), z3.Tactic('factor'))

x = z3.Int('x')
g = z3.Goal()
g.add(x > 0)
g.add(x < 10)
print(t(g)(g))

This prints:

[[x > 0, x < 10]]