小编Ant*_*ton的帖子

(declare-datatypes () ((SE BROKEN ON OFF)))
(declare-const s SE)
(declare-const a Int)
(simplify (or (= s ON) (= s OFF) (= s BROKEN)))
(simplify (and (> a 0) (> a 1)))

结果是:

(or (= s ON) (= s OFF) (= s BROKEN))
(and (not (<= a 0)) (not (<= a 1)))

但预期的结果是:

1
> a 1

是否有可能在Z3中简化这些表达式(这些表达式的组合)？谢谢!

我的课很简单：

MyObject:
 - String index;
 - MyObject parent;
 - List<MyObject> childs;

我想将存储的信息打印到json中。我使用Gson库的toJson函数。但是由于每个孩子都有到父对象的链接，因此我遇到了无限循环递归。有没有一种方法可以定义gson应该为每个孩子仅打印父索引而不是转储完整信息？