1

我正在尝试使用 Z3 来求解涉及未知投影函数的方程，以找到满足方程的函数的有效解释。例如，对于等式：snd . f = g . fst一个有效的解释是f = \(x,y) -> (y,x)和g = id。我知道 Z3 不是更高阶的，所以我一直在尝试以一阶形式对问题进行编码。因此，例如对于f = g.fst我使用：

(declare-datatypes (T) ((Tree (leaf (value T)) (node (children TreeList)))
                        (TreeList nil (cons (head Tree) (tail TreeList)))))
(define-fun fst ((x (Tree Int))) (Tree Int) (head (children x)))
(define-fun snd ((x (Tree Int))) (Tree Int) (head (tail (children x))))
(declare-fun f ((Tree Int)) (Tree Int))
(declare-fun g ((Tree Int)) (Tree Int))
(assert (forall ((x (Tree Int))) (= (f x) (g (fst x)))))
(check-sat)
(get-model)

返回的作品类型：

(define-fun g ((x!1 (Tree Int))) (Tree Int)
  (leaf 0))
(define-fun f ((x!1 (Tree Int))) (Tree Int)
  (g (head (children x!1))))

但是对于snd . f = g . fst（我已经将树简化为对尝试和帮助）：

(declare-datatypes (T) ((Pair (leaf (value T)) (pair (fst Pair) (snd Pair)))))
(declare-fun f ((Pair Int)) (Pair Int))
(declare-fun g ((Pair Int)) (Pair Int))
(assert (forall ((x (Pair Int))) (= (snd (f x)) (g (fst x)))))

我明白了unknown。

我还尝试在不使用 ADT 的情况下仅使用布尔值或整数作为参数来编码类似的问题，但是模型只是将常量值分配给函数。我还尝试为函数常量、恒等函数以及成对和顺序组合定义一个简单的 ADT，然后定义一个可以简化表达式的“等于”函数，例如f.id = f，但这要么涉及递归函数，例如：

(declare-datatypes () (
  (Fun id 
       (fun (funnum Int))
       (seq (after Fun) (before Fun))
       (pair (fst Fun) (snd Fun)) )))
(define-fun eq ((x Fun) (y Fun)) Bool (or
    (= x y)
      (eq x (seq y id)) ; id neutral for seq
      (eq x (seq id y))
      (eq y (seq x id))
      (eq y (seq id x))))
(declare-const f Fun)
(declare-const g Fun)
(assert (eq f (seq id g)))
(check-sat)
(get-model)

这显然是无效的。或者，如果我使用未解释的函数，它会使“eq”成为常量函数，即

(declare-fun eq (Fun Fun) Bool)
(assert (forall ((x Fun) (y Fun))  ; semantic equality
    (= (eq x y) (or
      (= x y) ; syntactic eq
      (eq x (seq y id)) ; id neutral for seq
      (eq x (seq id y))
      (eq y (seq x id))
      (eq y (seq id x))
    ))
))
=>
(define-fun eq ((x!1 Fun) (x!2 Fun)) Bool
    true)

与涉及 Int -> Int 类型函数的方程类似，这将返回 f 和 g 的常数函数：

(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (forall ((x Int)) (= (+ (f x) 1) (+ (g x) 2)) ))

并添加这些时间：

(assert (forall ((x Int) (y Int)) (=> 
  (not (= x y)) 
  (not (= (g x) (g y))))))
(assert (forall ((x Int) (y Int)) (=> 
  (not (= x y)) 
  (not (= (f x) (f y))))))

有什么想法可以让这种事情发挥作用吗？

非常感谢！

4

1 回答 1

1

Z3 搜索本质上有限的模型，因此不太适合直接求解函数方程。寻找这类模型的主要技巧是通过提供一组有限的可组合函数的替代解释来加强公式。例如，您可以允许 f(x) 为恒等式、置换或重复 x 或 y，或在其中一个字段中返回一个常量值，这可以由执行简单算术运算的函数组成。你必须限制你愿意承认的作品的数量。您为 g 断言一组类似的模板。到目前为止，这对位向量最有效。这种解释的搜索空间很容易变得不堪重负。我用代数数据类型和模板尝试了你的例子。Z3 在这种情况下无法找到解释，

于 2014-10-03T16:47:07.400 回答