小编Joh*_*ith的帖子

如何将F#中的Discriminated Union转换为Scala:

type Expr =
    | Val     of String
    | Integer of Int32
    | Lower   of Expr * Expr
    | Greater of Expr * Expr
    | And     of Expr * Expr
    | Or      of Expr * Expr

有一篇类似的文章谈论F#和Scala中的ADT,但这似乎不是我追求的.

我在Windows 7以及64位Java 7上使用的是Z3版本4.3.2的Java-API,但我不认为Java是回答这个问题的必要条件.

现在我使用以下Java代码来简化Z3中断言的一个子集:

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify");
Goal goal = ctx.mkGoal(true, false, false);
goal.add(bel.toArray(new BoolExpr[0])); // bel is List<BoolExpr>
ApplyResult applyResult = simplifyTactic.apply(goal);

到目前为止,我已经过滤了要简化的断言,然后使用上面的代码进行简化,它按预期工作.

经过一些测试后,我得出结论,我还需要插入模型的过滤断言(其中包含一些元信息,如基数).

是否有可能简化一些断言集A,而另一个断言集B仍被视为但未被改变？

以下示例可能会稍微澄清这个问题:

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)

(assert (=> a c)); member of set A
(assert (=> b d)); member of set A
(assert a); member of set A

; member of set B
(assert 
    (<= 
        (+ (ite (= c true) 1 0) (ite (= d true) …

如何使用smt-lib2获得最大公式？

我想要这样的东西:

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= x 2))
(assert (= y 4))
(assert (= z (max x y))
(check-sat)
(get-model)
(exit)

当然,smtlibv2不知道'max'.那么,怎么做呢？

如何将带有when条件的F#模式匹配转换为Scala？

我在F#中有以下代码:

match t0, t1 with
| "a", _ -> true
| b, "a" when not (b = "c") -> false

关于这个主题的另一篇文章Scala:当两个项目中的一个满足某些条件时模式匹配,但我无法获得基线.