0

我刚刚开始深入研究 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
4

1 回答 1

1

这并不奇怪，因为变量相乘会导致非线性算术，而重复加法会将其留在线性片段中。非线性算法是不可判定的，而线性片段有有效的判定程序（如 Presburger）。

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

话虽如此，Z3确实有一个非线性算术求解器，称为nlsat. 您可能想尝试一下，尽管我不会屏住呼吸。请参阅有关如何触发它的问题：(check-sat) then (check-sat-using qfnra-nlsat)

注意。我不确定是否可以nlsat通过 Python 使用 FixedPoint 引擎中的引擎，因此如果可以开始，您可能需要进行一些挖掘以找出正确的咒语是什么。

于 2019-08-01T17:51:51.920 回答