小编Yu *_*eng的帖子

假设我有两个约束(c1,c2),我想检查它们是否语法相同:

c1: f(x)>1 && g(y)=2
c2: f(x)>1 && g(y)=2

选项1:我们可以把这变成一个可满足性问题,就像这篇文章: 两个boolexpr是否相等

选项2:我们也可以将它们变成字符串并比较相等:

if(c1.toString().equals(c2.toString()))
    ///do somthing

但随着约束的大小增加,这两个选项都有很大的开销.例如,在Expr中调用toString()方法对于大型约束非常昂贵.

两个问题:

1. 如何在Z3(Java版本)中检查两个约束在语法上是否完全相同？

2. 如果我们没有1的好解决方案,我正在考虑为Expr对象编写一个包装器并使用工厂方法来避免从Z3生成重复(语法)对象.然后我必须设计自己的equal()和hashCode()函数.但到目前为止,我仍然无法找到一种有效的方法.

假设我有一个BoolExpr的形式

a & (a | b) or a | (a & b) 

我想简化它

a 

通过调用simplify().它不起作用.

另外,对于像这样的约束

(a | b) & (b | a) 

simplify()无法将其转换为最简单的形式

(a|b) or (b|a).

有解决方法吗？

@Nikolaj Bjorner:感谢您的帮助,我还有一个问题:

这是我原来的约束:

Goal: (goal
  (or (> (type o) 2) (= (type o) 1))
  (or (= (type o) 1) (> (type o) 2)))

这是简化版本(通过ctx-solver-simplified):

(or (= (type o) 1) (not (<= (type o) 2)))

我期待的实际约束是:

(or (= (type o) 1) (> (type o) 2))

而且我不想引入任何否定.我该怎么办？