I've just started digging into Z3's fixed point solver and I've cooked up an example that hangs when using multiplication but completes when defining multiplication as a series of additions. As I'm new to working with Horn clauses, there could be something I don't get here. Is there a reason "native" multiplication is so slow whereas multiplication defined as a series of additions produces a satisfying result in a reasonable timeframe? Thanks!
def test_mseq_hangs():
mul = Function('mul', IntSort(), IntSort(), IntSort(), BoolSort())
mc = Function('mc', IntSort(), IntSort(), BoolSort())
n, m, p = Ints('m n p')
fp = Fixedpoint()
fp.declare_var(n,m,p)
fp.register_relation(mc, mul)
fp.fact(mul(m, n, m * n))
fp.rule(mc(m, 1), m <= 1)
fp.rule(mc(m, n), [m > 1 , mc(m-1, p), mul(m, p, n)])
assert fp.query(And(mc(m,n),n < 1)) == unsat
assert fp.query(And(mc(m,n),n < 2)) == sat
assert fp.query(And(mc(m,n),n > 100 )) == sat
assert fp.query(mc(5,120)) == sat
assert fp.query(mc(5,24)) == unsat
def test_mseq():
mul = Function('mul', IntSort(), IntSort(), IntSort(), BoolSort())
add = Function('add', IntSort(), IntSort(), IntSort(), BoolSort())
neg = Function('neg', IntSort(), IntSort(), BoolSort())
mc = Function('mc', IntSort(), IntSort(), BoolSort())
n, m, p, o = Ints('m n p o')
fp = Fixedpoint()
fp.declare_var(n,m,p,o)
fp.register_relation(mc, add, mul, neg)
fp.fact(add(m, n, m + n))
fp.fact(neg(m, -m))
fp.rule(mul(m, n, 0), n == 0)
fp.rule(mul(m, n, m), n == 1)
fp.rule(mul(m, n, o), [n < 0, mul(m,n,p), neg(p,o)])
fp.rule(mul(m, n, o), [n > 1, mul(m,n-1,p), add(m,p,o)])
fp.rule(mc(m, 1), m <= 1)
fp.rule(mc(m, n), [m > 1 , mc(m-1, p), mul(m, p, n)])
assert fp.query(And(mc(m,n),n < 1)) == unsat
assert fp.query(And(mc(m,n),n < 2)) == sat
assert fp.query(And(mc(m,n),n > 100 )) == sat
assert fp.query(mc(5,120)) == sat
assert fp.query(mc(5,24)) == unsat
This isn't very surprising since multiplying variables leads to non-linear arithmetic, while repeated addition leaves it in the linear fragment. Non-linear arithmetic is not decidable, while there are efficient decision procedures (such as Presburger) for the linear fragment.
I'm not entirely sure how the Fixed-Point engine comes into play here, but the above holds true of the general queries; I'm guessing the same reasoning applies.
Having said that, Z3 does have a non-linear arithmetic solver, called nlsat. You might want to give that a try, though I wouldn't hold my breath. See this question on how to trigger it: (check-sat) then (check-sat-using qfnra-nlsat)
NB. I'm not sure if it's possible to use the nlsat engine from the FixedPoint engine via Python though, so you might have to do some digging to find out what the proper incantation would be, if it is possible to start with.