小编Mal*_*off的帖子

我有以下列表:

case class myPair(ids:Int,vals:Int)

val someTable = List((20,30), (89,90), (40,65), (45,75), (35,45))

val someList:List[myPair] =
  someTable.map(elem => myPair(elem._1, elem._2)).toList

我想过滤所有"ids"> 45.我试过类似这篇文章的过滤器使用模式匹配):

someList.filter{ case(myPair) => ids >= 45 }

但没有成功.感谢您的帮助

我刚绊倒方法的以下定义to由下式定义TraversableLike（2.10.0）：

override def to[Col[_]](implicit cbf: CanBuildFrom[Nothing, A, Col[A @uV]]): Col[A @uV] = {
  val b = cbf()
  b.sizeHint(this)
  b ++= thisCollection
  b.result
}

根据这个答案，@uV禁用差异检查。这听起来很危险。我为什么要这样做？

在此Z3问题评论中建议选项rlimit优先于timeout:

将超时与搜索算法相结合使得一切都是非确定性的,所以现在您甚至不必更改随机种子以使其失败!使用rlimits((set-option :rlimit <n>)和类似的)来确定资源边界的方式.

我试图rlimit在Z3的帮助(z3 -pd)中找到更多信息,但提供的描述只有很短.

具体来说,我有以下问题:

• Q1:什么样的"求解器资源" rlimit限制了 - 只是时间还是记忆？
• Q2::rlimit 1000相当于:timeout 1000求解器必须在1000几毫秒后终止？
• Q3:可以rlimit重复设置(timeout可以)还是只设置一次？

我创造了一个 MultiMap

val ms =
  new collection.mutable.HashMap[String, collection.mutable.Set[String]]()
  with collection.mutable.MultiMap[String, String]

在填充了条目之后,必须将其传递给期望a的函数Map[String, Set[String]].ms直接传递不起作用,并试图通过它将其转换为不可变的地图toMap

ms.toMap[String, Set[String]]

产量

Cannot prove that (String, scala.collection.mutable.Set[String]) <:< (String, Set[String]).

这可以解决而无需手动迭代ms并将所有条目插入到新的不可变映射中吗？

我正在尝试将 z3py 集成到我的应用程序中。有涉及小实数的断言，例如

solver.add(x <= 1e-6)

然后我收到以下错误：

File "~/src/solver/z3.py", line 2001, in __le__
  a, b = _coerce_exprs(self, other)
File "~/src/solver/z3.py", line 846, in _coerce_exprs
  b = s.cast(b)
File "~/src/solver/z3.py", line 1742, in cast
  return RealVal(val, self.ctx)
File "~/src/solver/z3.py", line 2526, in RealVal
  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
File "~/src/solver/z3core.py", line 1774, in Z3_mk_numeral
  raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
src.solver.z3types.Z3Exception: 'parser error'

虽然断言

solver.add(x <= 1e-4)

似乎没问题。

因此，我猜测 z3 中存在某种精度限制。如果是这样，是否可以选择让第一个断言通过？

谢谢。

是否可以一般性地替换案例类中的参数？更具体地说,我想要一个替代函数,它接收一个"查找"案例类和一个"替换"案例类(如语法规则的左侧和右侧)以及一个目标案例类,该函数将返回一个将case case类的参数替换为replace case类的新case类？该函数还可以简单地将case类(Product？)和一个函数应用于case类的所有参数/产品.

显然,给定一个特定的case类,我可以使用unapply和apply - 但是一般来说(给定任何case类)编写这种函数的最好/最简单/等方法是什么？

我想知道是否有一个很好的解决方案,使用Scala 2.10反射功能或无形的Iso.hlist.

例如,我真正希望能够做的是,给出如下的类......

class Op[T]
case class From(x:Op[Int]) extends Op[Int]
case class To(x:Op[Int]) extends Op[Int]

case class Target(a:Op[Int], b:Op[Int]) extends ...
// and lots of other similar case classes

...有一个函数可以接受任意的case类并返回它的副本,其中任何类型的元素都替换为To类型的实例.

SMTLib2指令(get-info all-statistics)显示多个数字，例如

num. conflicts:     4
num. propagations:  0 (binary: 0)
num. qa. inst:      23

为了测试不同的公理化和编码，我想知道这些数字中的哪一个适合宣布一个Z3运行比另一个运行更好/更有效。

从名字中猜测，我想说的是num. qa. inst-数量化实例化的数量-是一个很好的指标（低=更好），但是其他指标呢？

以下脚本http://rise4fun.com/Z3Py/Cbl有什么问题？添加最后两行给出了以下错误'instancemethod' object is not #subscriptable

x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next')
location,location_next=Bools('location location_next')
x=0
location=BoolVal(False)
k=20
for i in range(k):
 s=Solver()
 s.add(Or(And(x_next-x>=2*t,x_next-x<=3*t,x_next<=12,t>0,Not(location)),
         And(x_next-x>=-2*t,x_next-x<=-t,x_next>=0,t>0,location)),location_next==If(And(Not(location),x_next>=12),True,If(And(location,x_next<=0),False,location)))

print s.check()
print s.model()
m=s.model
#x=m[x_next]
#location=m[location_next]

我正在使用Z3的Python API,试图在我正在编写的研究工具中包含对它的支持.我有一个关于使用Python接口提取不可满足核心的问题.

我有以下简单查询:

(set-option :produce-unsat-cores true)
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(check-sat)
(get-unsat-core)
(exit)

通过z3可执行文件(对于Z3 4.1)运行此查询,我收到了预期的结果:

unsat
(__constraint0)

对于Z3 4.3,我获得了一个分段错误:

unsat
Segmentation fault

这不是主要问题,尽管这是一个有趣的观察.然后我将查询(在文件中)修改为

(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(exit)

使用文件处理程序,我将此文件的内容(在变量`queryStr'中)传递给以下Python代码:

import z3
...
solver = z3.Solver()
solver.reset()
solver.add(z3.parse_smt2_string(queryStr))
querySatResult = solver.check()
if querySatResult == z3.sat:
    ...
elif querySatResult == z3.unsat:
    print solver.unsat_core()

我从`unsat_core'函数接收空列表:[].我是否正确使用此功能？该函数的文档字符串表明我应该做类似的事情

solver.add(z3.Implies(p1, z3.Not(0 == 0)))

但是,我想知道是否仍然可以按原样使用查询,因为它符合SMT-LIB v2.0标准(我相信),以及我是否遗漏了一些明显的东西.

给定一个使用 Z3 实数编码的问题，Z3 /smt2 /st产生的哪些统计数据可能有助于判断实数引擎是否“有问题/做了很多工作”？

就我而言，我有两个几乎等效的问题编码，都使用实数。然而，编码中的“小”差异在运行时产生了很大差异，即编码 A 需要 2:30 分钟，编码 B 需要 13 分钟。Z3的统计数据显示，conflicts和quant-instantiations大多是等价的，但其他人都没有，例如grobner，pivots和nonlinear-horner。

两种不同的统计数据可作为gist 使用。

编辑（以解决 Leo 的评论）：

两个版本生成的 SMT2 编码约为 30k 行，并且使用实数的断言散布在整个代码中。的主要区别在于编码乙使用大量尚未得以实时类型的常量从范围0.0到1.0由不等式，例如有界0.0 < r1 < 1.0或0.0 < r3 < 0.75 - r1 - r2，而在编码许多这些尚未得以常数已经从相同的范围置换为固定真实值，例如，0.1或0.75 - 0.01。两种编码都使用非线性实数算术，例如r1 * (1.0 - r2).

来自两种编码的一些随机示例可作为要点。如上所述，所有出现的变量都是未指定的实数。

PS：是否为固定实数值引入别名，例如，

(define-sort $Perms () Real)
(declare-const …