Z3中带有乘法的角子句

Question

我刚刚开始挖掘Z3的固定点求解器，并且我煮了一个示例，该示例在使用乘法时挂起，但在将乘法定义为一系列添加时完成。我是与Horn条款合作的新手，可能会有一些我不到这里的东西。是否有一个原因"本地"乘法如此慢，而定义为一系列添加的乘法会在合理的时间范围内产生令人满意的结果？谢谢！

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

Answer 1

这并不令人惊讶，因为乘变量会导致非线性算术，而重复的添加使其在线性片段中。非线性算术不是可决定的，而线性片段有有效的决策程序(例如Presburger(。

我不完全确定定点引擎是如何在这里发挥作用的，但是上面是一般查询。我猜相同的推理也适用。

话虽如此，z3 do 具有一个非线性算术求解器，称为 nlsat。您可能想尝试一下，尽管我不会屏住呼吸。请参阅有关如何触发它的问题：( check-sat(然后(检查 - 使用qfnra-nlsat(

nb。我不确定是否可以通过Python从固定点引擎中使用nlsat引擎，因此您可能必须进行一些挖掘才能找出适当的咒语是什么，如果可以从。