小编ali*_*ias的帖子

我正在使用包中的race函数async,导出Control.Concurrent.Async.

我使用race自己runInteractiveProcess启动的子任务调用运行(非Haskell)可执行文件.我们的想法是运行不同的外部程序,并完成第一个程序的结果.从某种意义上说,Haskell"编排"了一堆外部程序.

我所观察到的是,race通过杀死Haskell级别"慢"线程正常工作; 从慢线程本身产生的子进程继续运行.

我怀疑期望race杀死以这种方式产生的进程有点不切实际,因为它们可能变成了僵尸并被init继承.然而,出于我的目的,保持外部进程运行首先失败了使用的全部目的race.

是否有另一种使用方式,race因此以这种方式创建的子进程也会被杀死？虽然我还没有用例,但最好是从raced任务创建的整个流程链被杀死; 可以想象,那些外部程序本身也会创建一堆进程.

浏览Z3源代码,我遇到了一堆引用QF_FPA的文件,它似乎代表无量词,浮点运算.但是,我似乎无法找到有关其状态的任何文档,或者如何通过各种前端(特别是SMT-Lib2)使用它.这是IEEE-754 FP的编码吗？如果是,支持哪些精度/操作？任何文档都是最有帮助的..

有没有办法写下面的内容:

 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveAnyClass     #-}

 data X = A | B | C
     deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind, SMTValue)

因此deriving可以以某种方式缩短该子句,如下所示:

 data X = A | B | C deriving MyOwnClass

我想尽可能避免TH,并且我很乐意创建一个新类,它将所有派生类作为必要的超类(MyOwnClass如上所述),但这并不适用于deriving机制.通过约束种类扩展,我发现你可以这样写:

type MyOwnClass a = (Eq a, Ord a, Show a, Read a, Data a, SymWord a, HasKind a, SMTValue a)

不幸的是,我不能把它放在deriving条款中.是否有一些魔力可以实现这一目标？

编辑从评论中看来,TH可能是唯一可行的选择.(CPP宏真的不行!)如果是这样的话,TH解决方案的草图将会很好看.

这实际上是程序员类别理论 -第 2 章中的挑战#6 ，这个问题是我前段时间问过的另一个问题的后续问题：

绘制一个类别的图片，其唯一对象是类型Void、()（单位）和Bool；箭头对应于这些类型之间所有可能的功能。用函数名称标记箭头。

这是连接这三个对象/类型的箭头/函数列表，我对此更加确定：

• 4个功能Bool -> Bool
• true = const True :: () -> Bool
• false = const False :: () -> Bool
• ignore = const () :: Bool -> ()
• absurd :: Void -> ()
• absurd :: Void -> Bool
• id :: () -> ()
• id :: Void -> Void必须存在，因为我们正在谈论一个类别，对吧？
• Void其他两个不会发生任何事情，因为它是一个初始对象，对吧？

这是正确答案吗？

我有两个使用实数的SMT2-Lib脚本,这在道德上是等价的.唯一的区别是,一个也使用位向量而另一个不使用位向量.

这是使用实数和位向量的版本:

; uses both reals and bit-vectors
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 1))
(assert
   (let ((s4 (- s3 s2)))
   (let ((s5 (ite (= #b1 s1) s2 s4)))
   (let ((s7 (+ s5 s6)))
   (let ((s8 (- s5 s6)))
   (let ((s9 (ite (= #b1 s0) s7 s8)))
   (let …

我是 Z3 的新手，正在尝试制作一个求解器，将每个可满足的解决方案返回到布尔公式。从其他 SO 帖子中记下笔记，我已经编写了我希望能起作用的代码，但事实并非如此。问题似乎是，通过添加以前的解决方案，我删除了一些变量，但它们又在后面的解决方案中返回了？

目前我只是想解决a或b或c。

如果我解释得不好，请告诉我，我会尽力进一步解释。

预先感谢您的回复:)

我的代码：

from z3 import *

a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))

while (s.check() == sat):
        print(s.check())
        print(s)
        print(s.model())
        print(s.model().decls())
        print("\n")
        s.add(Or([ f() != s.model()[f] for f in s.model().decls() if f.arity() == 0])) 

我的输出：

sat
[Or(a, b, c)]
[c = False, b = False, a = True]
[c, b, a]


sat
[Or(a, b, c), Or(c != False, b != False, a != True)]
[b = True, …

Z3会支持AUFBV吗？

对于以下脚本:

(set-logic AUFBV)
(declare-fun x () (_ BitVec 16))
(declare-const t (Array (_ BitVec 16) (_ BitVec 16)))
(assert (= (select t #x0000) #x0000))

在线Z3演示似乎是高兴的set-logic呼叫,但随后抱怨的种类BitVec和Array.(顺便提一下,set-logic无论逻辑名称如何,在线演示似乎都对通话感到满意,即使是伪造的名字,例如(set-logic blarg).)

SMT-Lib网站既没有提及UFBV也没有提到AUFBV,但鉴于他们的无量词对应物(QF_UFBV和QF_AUFBV),我希望Z3也能支持AUFBV.

不用说,阵列在实践中起着非常重要的作用.我认为,鉴于有限性论证,AUFBV逻辑应保持可判定性.看到Z3支持它真的很高兴.

谢谢!

我正在使用 TPTP 语法测试一些定理证明器（例如 Z3、Alt-Ergo、Vampire 等）的归纳能力。令我惊讶的是，他们都没有能够证明以下简单的猜想：

tff(t1, type, (fun: $int > $int )).

tff(ax1, axiom, ( 
    ! [A: $int] : (
        $less(A, 1) => (fun(A) = 123)
    )
)).

tff(ax2, axiom, ( 
    ! [A: $int] : (
        $greatereq(A, 1) => (fun(A) = fun($difference(A, 1))) 
    )
)).

tff(conj1, conjecture, ! [A: $int] : ($greatereq(A, 1) => (fun(A) = 123))).

% END OF SYSTEM OUTPUT
% RESULT: SOT_EWCr1V - Z3---4.8.9.0 says Timeout - CPU = 60.09 WC = 35.47 
% OUTPUT: SOT_EWCr1V - …

考虑证明以下 while 循环的正确性，即我想表明，给定循环条件开始时，它最终将终止并导致最终断言为真。

int x = 0;
while(x>=0 && x<10){
   x = x + 1;
}
assert x==10;

在不使用循环展开的情况下，用于检查正确性的 SMT-LIB 的正确翻译是什么？

我有以下类型系列：

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import GHC.TypeLits
import Data.Type.Bool

type family Valid (n :: Nat) :: Constraint where
  Valid (n :: Nat) = ( KnownNat n
                     , If (2 <=? n && n <=? 16)
                          (() :: Constraint)
                          (TypeError ('Text "No Good"))
                     )

这按预期工作。但是，GHC有一个音符是<=?可能有利于消失CmpNat。到目前为止，我尝试替换<=?with 的尝试CmpNat失败了。这个版本，例如：

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE KindSignatures …

由于精度，0.1 + 0.2不等于0.3大多数编程语言。然而，

var float a, float b
assert(a != 0 && b != 0)
if a / b == -1.0 {
    // a, b are opposite numbers:
    //  abs(a) == abs(b) && (a > 0 && b < 0 || a < 0 && b > 0)
    ...
}

如果非零并且是相反的数（它们的绝对值相同，但一个是正数，另一个是负数），它总是正确的吗？ab

或者我必须引入一个非常小的数字epsilon（例如1e-7）来消除错误：

if a / b >= -1.0 - epsilon && a / b <= -1.0 + epsilon