首页 文章
  • 0 votes
     answers
     views

    将循环语义转换为SMT-LIB

    是否有标准方法将命令式语言(比如C或Java)中的 for 循环的语义转换为SMT-LIB?我正在考虑将它们定义为SMT-LIB公理,但它似乎是临时的,我理解翻译并不总是由解算器说明z3 .
  • 1 votes
     answers
     views

    SMT-LIB基准

    我想对一些SMT求解器进行基准测试,而SMT-LIB基准测试库[1,2]似乎是一个很好的起点 . 但是,该链接已经停止了至少几天 . 有谁知道我能找到这些基准的任何其他地方? [1] http://www.smtlib.org/ [2] http://smtexec.org/exec/smtlib-portal-benchmarks.php
  • 1 votes
     answers
     views

    如何在SMT-LIB中为Z3定义枚举类型

    我以前使用Z3的API来定义枚举类型 let T = ctx.MkEnumSort("T", [| "a"; "b"; "c"|]) 它将类型T的元素枚举为“a”“b”和“c”(并且没有别的) . 但是我现在尝试做类似的事情,但是通过SMT-LIB而不是API,我遇到了Z3抱怨量词的问题 . 我正在使用的程序(Boo...
  • 4 votes
     answers
     views

    在SMT-LIB中表示时间约束

    我试图在SMT-LIB中表示时间约束,以检查它们的可满足性 . 我正在寻找有关我正在采取的方向的反馈 . 我对SMT-LIB比较陌生,我非常欣赏输入 . 我所拥有的约束是关于事件的时间和持续时间 . 例如,考虑以自然语言给出的以下约束: 约翰在13:03:41开始写一篇文章,花了20分钟完成它 . 写完之后,他检查了他的电子邮件,这花了他超过40分钟 . 检查完他的电子邮件后,他打电话...
  • 1 votes
     answers
     views

    QF_NRA中是否包含零除?

    QF_NRA中是否包含零除? SMT-LIB标准在这个问题上令人困惑 . paper where the standard is defined根本没有讨论这一点,实际上NRA和QF_NRA没有出现在该文件的任何地方 . 有关信息,请参见standard website . 实际定义包括: - all terms of the form (/ m n) or (/ (- m) n) where ...
  • 0 votes
     answers
     views

    是否有选项可以在cvc4中为SMT输入启用用户定义符号的重载?

    在SMT-LIB语言的1.2版本中,允许重载用户定义的符号 . 从标准2.0版开始,重载仅限于理论符号 . 尽管如此,一些SMT解算器仍允许重载用户定义的符号,这对我的用例来说很方便:证明义务很容易通过重载自动生成,而不是没有...我想将cvc4添加到我的投资组合中SMT求解器,但我发现它在重载的用户符号上产生解析错误 . 我知道这是符合SMT-LIB标准的正确方法,但我想知道以下内容:CVC4是...
  • 0 votes
     answers
     views

    处理SMT-LIB / Z3中的溢出

    我正在尝试使用SMT a + b - c - d 建模以下表达式,所有常量 a,b,c,d 都是相同大小的bitvecs,约束与以下断言 a + b >= c + d . 我想以不会发生溢出/下溢的方式对其进行建模 . 这是我到目前为止所尝试的: (declare-const a (_ BitVec 4)) (declare-const b (_ BitVec 4)) (declare-...
  • 7 votes
     answers
     views

    在位向量算法的决策过程中使用术语重写

    我正在研究一个项目,其重点是使用术语重写来解决/简化固定大小的位向量算术问题,这对于某些决策程序(例如基于钻头爆破的程序)的先前步骤是有用的 . 术语重写可以完全解决问题,或者产生更简单的等效问题,因此两者的组合可以导致相当大的加速 . 我知道许多SMT求解器实现了这种策略(例如Boolector,Beaver,Alt-Ergo或Z3),但是很难找到详细描述这些重写步骤的论文/技术报告/等 . 一...
  • 0 votes
     answers
     views

    使用C,使用Z3_parse_smtlib2_string在Z3中获取Unsat Core

    我需要使用 Z3_parse_smtlib2_string 使用C API将一些SMTLIB字符串解析为Z3,并使用Z3 C API来查找不满核心 . 我知道还有其他方法可以找到更容易且不那么繁琐的here和here描述的不饱和核心,但我真的希望能够仅使用从字符串解析到Z3的数据结构来做到这一点 . 原因是我试图使用Z3自动化某些东西 . 很明显,如果我将这个SMTLIB程序传递给Z3,那就是UN...
  • 3 votes
     answers
     views

    SMT求解器中约束强化的效率

    解决优化问题的一种方法是使用SMT求解器来询问是否存在(坏)解决方案,然后逐步添加更严格的成本约束,直到命题不再可满足为止 . 例如,http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf讨论了这种方法 . 这种方法有效吗...
  • 0 votes
     answers
     views

    Z3 Java API - 获得不满的核心

    我试图弄清楚如何使用Java API for Z3获得不饱和核心 . 我们的场景如下(代码在下面,在rise4fun中工作): 我们以编程方式创建SMT2输入 输入包含函数定义,数据类型声明和断言 我们使用parseSMTLIB2String API解析它 我们确保上下文和解算器具有unsat_core - > true Z3为提供的输入返回UNSAT,这是正确的 ...
  • 1 votes
     answers
     views

    没有元组(declare-datatypes)?

    我用SMT-LIB的Z3方言写了一个大型的库 . 不幸的是,我使用 (declare-datatypes) 来创建元组意味着我无法按照我的意愿将逻辑设置为 QF_AUFBV . 这有使我的脚本更慢(有时超时)的副作用比我以编程方式手动创建公式并使用 QF_ABV 解决 . 因此,我想从我的脚本中删除 (declare-datatypes) . 大多数数据类型可以编码为位向量 . 但是,库中最重...
  • 6 votes
     answers
     views

    用于位向量算术的SMT求解器

    我正在计划一些C代码的符号执行实验,使用现成的SMT求解器,并想知道使用哪个求解器;看着例如SMT比赛的参赛者,只采用开源系统,将其缩小为Beaver,Boolector,CVC3,OpenSMT,Sateen,Sonolar,STP,Verit;这仍然是一个很长的名单 . 为了进一步缩小范围,我注意到一些系统宣传处理位向量算术的能力,而其他系统只宣传处理一般整数算术的能力 . 原则上,前者对于C...
  • 3 votes
     answers
     views

    Z3 / SMT:我什么时候应该选择push / pop来重置?

    我使用Z3来解决符号 Actuator 产生的路径条件,它以深度优先顺序探索状态空间,与CUTE,DART或(可能)SAGE非常相似 . 我们正在尝试使用Z3的不同方法 . 在一个极端,我们将每个查询发送到Z3并立即(重置)它 . 另一方面,我们(推)每个额外的分支约束,并且(弹出)(pop)在回溯时正确削弱路径条件所需的最小值 . 问题是,在所有情况下,没有任何策略似乎比任何其他策略更好 . 推...
  • 2 votes
     answers
     views

    将z3 C API ast(或解算器)对象转换为SMTLIB字符串

    我正在玩z3和其他SMT求解器,并且想要检查其他求解器如boolector胜过z3的情况,反之亦然 . 为此,我需要一种方法将声明和断言转换为SMT-LIB2格式,而其他SMT求解器可以识别这种格式 . 例如,对于此示例 void print_as_smtlib2_string() { context c; expr x = c.int_const("x"); ...
  • 2 votes
     answers
     views

    Z3位向量操作

    如何使用'repeat'和'rotate_left'位向量操作? 更一般地说,在哪里可以找到Z3使用的SMT2脚本格式的bitvector操作的详细文档? 我发现的一切似乎只是去教程或破坏的链接:https://github.com/Z3Prover/z3/wiki/Documentationhttp://research.microsoft.com/en-us/um/redmond/projec...
  • 0 votes
     answers
     views

    dReal SMT求解器反例

    dReal SMT求解器是否会返回反例?我已经看到了以下示例: 生产环境 模型是真的,但我不知道如何生成反例 . 此外,dReach工具有一个--visualize选项,因此看起来dReal需要生成一些模型信息 . 但是,当我在.smt2文件上运行它时,我似乎找不到查看反例的方法 .
  • 1 votes
     answers
     views

    在SMT中表达不关心的位向量

    我想定义一个接受位向量的函数,如果某个位置的位满足某些值,则返回true . 例如:如果bitvector是1x00x01x,我需要返回true,其中x表示不关心 . 我目前的实施是: (define-fun function_i ((i (_ BitVec 8))) Bool (and true (= #b1 ((_ extract 1 1) i)) (=...
  • 12 votes
     answers
     views

    用Z3 / SMT-LIB2定义集合论

    我正在尝试使用SMTLIB接口为Z3定义集合理论(并集,交集等) . 不幸的是,我的当前定义为一个简单的查询挂起z3,所以我想我错过了一些简单的选项/标志 . 这是永久链接:http://rise4fun.com/Z3/JomY (declare-sort Set) (declare-fun emp () Set) (declare-fun add (Set Int) Set) (declare-...
  • 1 votes
     answers
     views

    使用Z3和SMT-LIB定义具有实数的sqrt函数

    我如何以smt-libv2格式编写sqrt函数 . 注意:要获得最多两个值,我在这里找到了一个有用的链接:Use Z3 and SMT-LIB to get a maximum of two values .
  • 2 votes
     answers
     views

    Z3无法找到具有量词和模式的简单公式的令人满意的赋值

    我目前正在为Z3之上的编程语言编写一个自动Verifier作为一个有趣的项目,我试图用它来证明使用循环的fibonacci实现等同于递归 . 如果输入程序是正确的,它似乎有效,即它为Z3生成合理的输入,Z3表示它是不可满足的,这意味着在我的上下文中,程序是正确的 . 但是当我改变一个变量初始化并因此使程序不正确时,我的验证者提出了以下Z3公式,这对我来说似乎并不太复杂,但Z3说“未知” . (se...
  • 3 votes
     answers
     views

    z3是否支持将运算符标记为关联运算符,可交换运算符或两者兼有?

    我想用SMT格式编写证明义务,其中一些函数具有一些共同的通用属性(即关联性和可交换性) . 一个简单的解决方案是在证明义务中包含相应的公理 . 我想这意味着这些属性的推理将在很大程度上取决于量词实例化算法 . 其他技术,如重写,可能更有效,我想知道Z3是否实现了这种技术 . API中存在诸如Z3_OP_PR_REFLEXIVITY和Z3_OP_PR_COMMUTATIVITY之类的值表明这可能是...
  • 1 votes
     answers
     views

    Z3 / SMT-LIB评估功能和收集结果

    我试图以一种自动查询所有可用值的方式从Z3中获取一些值: (define-fun-rec out ((p Pkg) (t Time)) (List Bool) (ite (< t 0) (as nil (List Bool)) (insert (eval (installed p t)) (out p (- t 1))))) (eval (out a t-final)) 不幸的是,这...
  • 1 votes
     answers
     views

    SMT-LIB中的QF_NRA逻辑是否可判定?

    SMT-LIB中的QF_NRA逻辑是否可判定? 我知道Tarski证明非线性算法是可判定的,因为实数中的多项式系统是可判定的 . 然而,由于QF_NRA包含分区,因此QF_NRA属于这一范围并不明显 . 所以第一个问题是QF_NRA中的除法是否包括除以分母可能为零的变量 . I posted that as a separate question,因为回答这一点本身就足够困难了 . 如果除以零不...
  • 3 votes
     answers
     views

    支持QF_AUFBV中的多维数组?

    我目前正致力于将通过C程序的“路径”转换为相应的SMT查询以测试此路径的可行性的代码 . 我有工作代码创建SMT-LIB v1.2查询,并使用Z3 2.11和QF_AUFBV逻辑来解决查询 . 我目前正在将此代码移植到Z3 4.3,以利用自那时以来可能发生的任何速度提升,特别是因为我的前代码似乎需要花费很长时间(大约22分钟)来查询仅分配24个值一个三维数组并检查数组中某个位置的值 . 但是,似乎...
  • 0 votes
     answers
     views

    如何统一SMT-LIB中的变量

    我试图在SMT-LIB中执行此操作,在包含这些表达式的脚本上运行 z3 -smt2 script.smt2 : (set-logic AUFLIA) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) (declare-fun d () Int) (declare-fun e () Int) (declare-...
  • 4 votes
     answers
     views

    如何在SMT-LIB标准中表示浮点常数(例如1e307)?

    目前我正在对Z3进行一些实验,我不知道在SMT中表示浮点常量字面值(例如1e307): (declare-const a Real) (assert (= a 1e+307)) (check-sat) FPA理论也出现了同样的问题: (declare-const a (_ FloatingPoint 11 53)) (assert (= a 1e+307)) (check-sat) 所有这些S...
  • 0 votes
     answers
     views

    z3(v4.4.0)统计信息中报告的时间是否包括读取SMT约束文件所需的时间?

    或者纯粹是解决时间?这个问题适用于将z3作为外部二进制文件调用的情况 . 我问这个,在我的一些例子中,约束求解时间很短,我怀疑它将与文件读取时间相当 . 另外,小值(例如<1s)的总时间有多准确?
  • 0 votes
     answers
     views

    z3,z3py:我可以定义一个包含一组整数的排序吗?

    这是我之前的问题"Is it possible to intrinsically reduce the search space of Function"的后续问题 . 我在想是否有可能我可以定义一个包含一组整数的排序,例如整数1-10 . 我的直觉是,为了减少Function的搜索空间,而不是定义一个域的排序和范围排序是IntSort的Function,我想定义一个Funct...
  • 1 votes
     answers
     views

    如何在Z3中零/符号扩展位向量?

    我无法使用Z3 SMT接口在位向量上执行零扩展 . 从我通过阅读源学到的东西,有这方面的函数,它们可用于各种绑定(C,C,Python等),但SMT接口教程不知道如何调用它们 . 使用SMT QF_BV逻辑标准中的 zero_extend 也无济于事 - Z3说 unsupported .

热门问题