- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我想在另一个模型中使用一个模型的输出(在我的例子中只有 sat 和 unsat)。在这里,模型是对一组逻辑公式(在本例中为 Z3 表达式)中涉及的常量的令人满意的赋值。我的目标可以简要解释如下。
我的问题可以详细描述如下:我有一个形式化的问题P,一组逻辑公式(表达式)对应多个约束(C)。在这些表达式中,一个(例如,Ai > 0)是我的目标。如果所有约束都可满足,则执行模型/形式化 P 返回 sat。请注意,Ai = 0 总是可能的。现在,我想找到一组特定变量的赋值对应于约束 (C),以确保 Ai > 0(对于任何 i)是不可能的。目前,我正在通过编写一个程序(在 C# 中)来解决问题,该程序开发基于 DFS 的约束搜索算法(即约束值)并执行 P 以在“push/pop”的帮助下查看结果是否为假”。虽然我试图让搜索变得更好,但它对我没有太大帮助。对于大问题规模,这是非常低效的。如果我可以使用 P 创建另一个 SMT 程序(模型)来搜索这样一个可满足的集合,那就太好了。
问题 P(原始问题的简短 SMT LIB 2 版本)的当前形式化如下:
(declare-fun th1 () Real)
(declare-fun th2 () Real)
(declare-fun th3 () Real)
(declare-fun th4 () Real)
(declare-fun th5 () Real)
(declare-fun l1 () Real)
(declare-fun l2 () Real)
(declare-fun l3 () Real)
(declare-fun l4 () Real)
(declare-fun l5 () Real)
(declare-fun l6 () Real)
(declare-fun l7 () Real)
(declare-fun p1 () Real)
(declare-fun p2 () Real)
(declare-fun p3 () Real)
(declare-fun p4 () Real)
(declare-fun p5 () Real)
(declare-fun sl1 () Int)
(declare-fun sl2 () Int)
(declare-fun sl3 () Int)
(declare-fun sl4 () Int)
(declare-fun sl5 () Int)
(declare-fun sl6 () Int)
(declare-fun sl7 () Int)
(declare-fun sp1 () Int)
(declare-fun sp2 () Int)
(declare-fun sp3 () Int)
(declare-fun sp4 () Int)
(declare-fun sp5 () Int)
(declare-fun a1 () Int)
(declare-fun a2 () Int)
(declare-fun a3 () Int)
(declare-fun a4 () Int)
(declare-fun a5 () Int)
(declare-fun na () Int)
(declare-fun ns () Int)
(declare-fun attack () Bool)
;;;; System
(assert (and (= l1 (* (- th2 th1) 17.0))
(= l2 (* (- th5 th1) 4.5))
(= l3 (* (- th3 th2) 5.05))
(= l4 (* (- th4 th2) 5.65))
(= l5 (* (- th5 th2) 5.75))
(= l6 (* (- th4 th3) 5.85))
(= l7 (* (- th5 th4) 23.75))
(= p1 (+ l1 l2))
(= p2 (+ l1 l3 l4 l5))
(= p3 (+ l3 l6))
(= p4 (+ l4 l6 l7))
(= p5 (+ l2 l5 l7))
)
)
;;;; Secured measurements
(assert (and (or (= sl1 0) (= sl1 1))
(or (= sl2 0) (= sl2 1))
(or (= sl3 0) (= sl3 1))
(or (= sl4 0) (= sl4 1))
(or (= sl5 0) (= sl5 1))
(or (= sl6 0) (= sl6 1))
(or (= sl7 0) (= sl7 1))
(or (= sp1 0) (= sp1 1))
(or (= sp2 0) (= sp2 1))
(or (= sp3 0) (= sp3 1))
(or (= sp4 0) (= sp4 1))
(or (= sp5 0) (= sp5 1))
)
)
(assert (and (=> (not (= l1 0.0)) (= sl1 0))
(=> (not (= l2 0.0)) (= sl2 0))
(=> (not (= l3 0.0)) (= sl3 0))
(=> (not (= l4 0.0)) (= sl4 0))
(=> (not (= l5 0.0)) (= sl5 0))
(=> (not (= l6 0.0)) (= sl6 0))
(=> (not (= l7 0.0)) (= sl7 0))
(=> (not (= p1 0.0)) (= sp1 0))
(=> (not (= p2 0.0)) (= sp2 0))
(=> (not (= p3 0.0)) (= sp3 0))
(=> (not (= p4 0.0)) (= sp4 0))
(=> (not (= p5 0.0)) (= sp5 0))
)
)
(assert (and (= sl1 1) (= sl2 1)))
;;;; Attacks
(assert (and (or (= a1 0) (= a1 1))
(or (= a2 0) (= a2 1))
(or (= a3 0) (= a3 1))
(or (= a4 0) (= a4 1))
(or (= a5 0) (= a5 1))
)
)
(assert (and
(= (not (= th1 0.0)) (= a1 1))
(= (not (= th2 0.0)) (= a2 1))
(= (not (= th3 0.0)) (= a3 1))
(= (not (= th4 0.0)) (= a4 1))
(= (not (= th5 0.0)) (= a5 1))
)
)
(assert (= th1 0.0)) // Base condition
(assert (= na (+ a1 a2 a3 a4 a5)))
(assert (=> attack (> na 1)))
;;;; Check for satisfiable model
(assert attack)
(check-sat)
(get-model)
(exit)
我想综合安全测量(即找到“sl”和“sp”项的分配),以便在给定约束的情况下不会发生攻击(即 na 将为 0),例如,如下所示:
(assert (= ns (+ sl1 sl2 sl3 sl4 sl5 sl6 sl7 sp1 sp2 sp3 sp4 sp5)))
(assert (<= ns 4))
在这种情况下,断言(即 '(assert (and (= sl1 1) (= sl2 1)))' )将被注释。目前,我已经开发了一个 C# 程序,它接受 'sl' 和 'sp' 的赋值,像 (assert (and (= sl1 1) (= sl2 1) ...))' 一样断言它们,并执行给定的程序看看是否有任何可能的攻击。当程序返回 unsat 时我就完成了(即 na > 1 是不可能的)。有没有办法只使用SMT(Z3)解决问题?
最佳答案
感谢您解决问题。如果我理解了一些事情,您可以使用 Z3 执行 sli
和 spj
值的搜索,但是您不能仅使用 SMT-LIB 执行此操作,您需要使用应用程序接口(interface)。这个想法是使用来自一次 sat 检查的模型(满足分配)作为 future 检查的约束,如这些答案中详细解释的那样:
Z3: finding all satisfying models
(Z3Py) checking all solutions for equation
这是用 Python API 编码的示例(z3py 链接:http://rise4fun.com/Z3Py/KHzm):
s = Solver()
th1, th2, th3, th4, th5 = Reals('th1 th2 th3 th4 th5')
th = { 'th1' : th1, 'th2' : th2, 'th3' : th3, 'th4' : th4, 'th5' : th5}
l1, l2, l3, l4, l5, l6, l7 = Reals('l1 l2 l3 l4 l5 l6 l7')
l = { 'l1' : l1, 'l2' : l2, 'l3' : l3, 'l4' : l4, 'l5' : l5, 'l6' : l6, 'l7' : l7 }
p1, p2, p3, p4, p5 = Reals('p1 p2 p3 p4 p5')
p = { 'p1' : p1, 'p2' : p2, 'p3' : p3, 'p4' : p4, 'p5' : p5 }
sl1, sl2, sl3, sl4, sl5, sl6, sl7 = Ints('sl1 sl2 sl3 sl4 sl5 sl6 sl7')
sl = { 'sl1' : sl1, 'sl2' : sl2, 'sl3' : sl3, 'sl4' : sl4, 'sl5' : sl5, 'sl6' : sl6, 'sl7' : sl7 }
sp1, sp2, sp3, sp4, sp5 = Ints('sp1 sp2 sp3 sp4 sp5')
sp = { 'sp1' : sp1, 'sp2' : sp2, 'sp3' : sp3, 'sp4' : sp4, 'sp5' : sp5 }
a1, a2, a3, a4, a5 = Ints('a1 a2 a3 a4 a5')
a = { 'a1' : a1, 'a2' : a2, 'a3' : a3, 'a4' : a4, 'a5' : a5 }
na, ns = Ints('na ns')
attack = Bool('attack')
n = { 'na' : na, 'ns' : ns, 'attack' : attack}
dict_decl = dict(th.items() + l.items() + p.items() + sl.items() + sp.items() + a.items() + n.items() )
assertions = []
assertions.append(parse_smt2_string('(assert (and (= l1 (* (- th2 th1) 17.0)) (= l2 (* (- th5 th1) 4.5)) (= l3 (* (- th3 th2) 5.05)) (= l4 (* (- th4 th2) 5.65)) (= l5 (* (- th5 th2) 5.75)) (= l6 (* (- th4 th3) 5.85)) (= l7 (* (- th5 th4) 23.75)) (= p1 (+ l1 l2)) (= p2 (+ l1 l3 l4 l5)) (= p3 (+ l3 l6)) (= p4 (+ l4 l6 l7)) (= p5 (+ l2 l5 l7))))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and (or (= sl1 0) (= sl1 1)) (or (= sl2 0) (= sl2 1)) (or (= sl3 0) (= sl3 1)) (or (= sl4 0) (= sl4 1)) (or (= sl5 0) (= sl5 1)) (or (= sl6 0) (= sl6 1)) (or (= sl7 0) (= sl7 1)) (or (= sp1 0) (= sp1 1)) (or (= sp2 0) (= sp2 1)) (or (= sp3 0) (= sp3 1)) (or (= sp4 0) (= sp4 1)) (or (= sp5 0) (= sp5 1)) ))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and (=> (not (= l1 0.0)) (= sl1 0)) (=> (not (= l2 0.0)) (= sl2 0)) (=> (not (= l3 0.0)) (= sl3 0)) (=> (not (= l4 0.0)) (= sl4 0)) (=> (not (= l5 0.0)) (= sl5 0)) (=> (not (= l6 0.0)) (= sl6 0)) (=> (not (= l7 0.0)) (= sl7 0)) (=> (not (= p1 0.0)) (= sp1 0)) (=> (not (= p2 0.0)) (= sp2 0)) (=> (not (= p3 0.0)) (= sp3 0)) (=> (not (= p4 0.0)) (= sp4 0)) (=> (not (= p5 0.0)) (= sp5 0)) ))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and (= sl1 1) (= sl2 1)))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and (or (= a1 0) (= a1 1))(or (= a2 0) (= a2 1))(or (= a3 0) (= a3 1))(or (= a4 0) (= a4 1))(or (= a5 0) (= a5 1)) ))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and (= (not (= th1 0.0)) (= a1 1))(= (not (= th2 0.0)) (= a2 1))(= (not (= th3 0.0)) (= a3 1))(= (not (= th4 0.0)) (= a4 1))(= (not (= th5 0.0)) (= a5 1)) ))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (= ns (+ sl1 sl2 sl3 sl4 sl5 sl6 sl7 sp1 sp2 sp3 sp4 sp5)))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (<= ns 4))', decls=dict_decl))
#assertions.append(parse_smt2_string('(assert (and (= sl1 1) (= sl2 1)))', decls=dict_decl)) # commented as suggested
assertions.append(parse_smt2_string('(assert (= th1 0.0))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (= na (+ a1 a2 a3 a4 a5)))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (=> attack (> na 1)))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert attack)', decls=dict_decl))
print assertions
s.add(assertions)
synthesized = []
iters = 0
while s.check() == sat:
print "Iteration " + str(iters)
print s.model()
avoid = []
# key step: add constraint to prevent any values assigned (if possible) to constants from being equal to their satisfying assignments (models) in this sat iteration
for sli in sl.values():
avoid.append(sli != s.model()[sli])
for spi in sp.values():
avoid.append(spi != s.model()[spi])
s.add(Or(avoid))
# end key step
synthesized.append(avoid)
print avoid
iters = iters + 1
# unless you know how to guarantee termination (e.g., there is a constraint ensuring the slis and spis take values in finite sets)
if iters >= 1000:
break
print "Done"
print synthesized # all the constraints
对于所有常量和数字表示歉意,我只是使用了您的 SMT-LIB 脚本的最快翻译,但最终变得相当麻烦,我会在任何地方使用迭代器。这对 sli
和 spj
常量产生了以下约束:
[[sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0]]
关于z3 - 我可以在另一个 SMT 表达式中使用 SMT 程序的结果吗?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/16310747/
我想在另一个模型中使用一个模型的输出(在我的例子中只有 sat 和 unsat)。在这里,模型是对一组逻辑公式(在本例中为 Z3 表达式)中涉及的常量的令人满意的赋值。我的目标可以简要解释如下。 我的
我想在另一个模型中使用一个模型的输出(在我的例子中只有 sat 和 unsat)。在这里,模型是对一组逻辑公式(在本例中为 Z3 表达式)中涉及的常量的令人满意的赋值。我的目标可以简要解释如下。 我的
我正在尝试 a Z3 tutorial 的一些示例涉及递归函数。我已经尝试了以下示例。 Fibonacci (第 8.3 节) IsNat (第 8.3 节) Inductive (第 10.5 节)
下面的 smt2 代码给出了与类型相关的错误。 ( declare-datatypes ( ( List 1 ) ) ( ( par ( T ) ( ( cons ( hd T ) ( tl (
我有一个关于 MaxSat 的想法,并且已经使用 MSU3 以及使用 minisat API 的顺序编码实现了一个朴素的 Maxsat 求解器 我想知道是否有办法加速这个求解器。 我带来了这篇论文:
我在以下看似微不足道的基准测试中尝试了几种 SMT 求解器(CVC3、CVC4 和 Z3): (set-logic LIA) (set-info :smt-lib-version 2.0) (asse
最近,我开始研究形式验证技术。在文献中,模型检查器和求解器可以以某种方式互换使用。 但是,模型检查器和求解器如何相互连接? p.s.如果建议提供一些论文或链接,我将不胜感激。 最佳答案 为了执行模型检
我一直在研究各种 SMT 求解器,主要是 Z3、CVC4 和 VeriT。他们都对自己用量词解决 SMT 问题的能力有模糊的描述。他们的文档主要基于示例 (Z3),或由学术论文组成,描述可能会或可能不
我想构造一个 SMT 公式,其中包含对整数线性算术和 bool 变量的多个断言,以及对实数非线性算术和 bool 变量的一些断言。对整数和实数的断言仅共享 bool 变量。例如,请考虑以下公式: (d
解决优化问题的一种方法是使用 SMT 求解器来询问是否存在(坏)解决方案,然后逐步添加更严格的成本约束,直到命题不再可满足。例如,http://www.lsi.upc.edu/~oliveras/es
我有一个 SMT 应用程序(基于 Haskell SBV 库构建),它针对单个 s 求解一些复杂的方程式使用 Z3 的实逻辑变量。就我而言,找到解决方案大约需要 30 秒。 为了加快速度,我添加了额外
在 previous post使用Z3Py在线解决了一些涉及运算放大器的问题。但是现在 Z3Py online 已停止服务,我正在尝试使用 Z3 SMT-LIB online 解决此类问题。 示例 1
我尝试了一段时间来完成一个相当简单的要求: 我声明了一个新的数据类型 (declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))
HT/SMT 背后的主要思想是,当一个线程停顿时,同一内核上的另一个线程可以选择该内核的其余空闲时间并透明地运行它。 In 2013 Intel dropped SMT in favor of out
我正在使用 Microsoft 的 Z3 SMT 求解器,并且我正在尝试定义自定义类型的常量。默认情况下,这些常量似乎并不不平等。假设您有以下程序: (declare-sort S 0) (decla
我正在考虑做一些验证工作,其中我有常规的树语法作为基础理论。 Z3 允许您使用未解释的函数定义自己的东西,但是当您的决策过程是递归的时,这往往不会很好地工作。他们曾经允许使用插件,但我认为这已经被贬低
是否有增量 SMT 求解器或某些增量 SMT 求解器的 API,我可以在其中增量添加约束,我可以通过某个标签/名称唯一标识每个约束? 我想唯一标识约束的原因是我以后可以通过指定该标签/名称来删除它们。
我正在计划使用现成的 SMT 求解器对 C 代码的符号执行进行一些实验,并且想知道使用哪个求解器;看着例如SMT 竞赛参赛者只选择开源系统,将范围缩小到 Beaver、Boolector、CVC3、O
我用 Haskell 编写了一个应用程序,它调用 Z3 求解器来解决一些复杂公式的约束。感谢 Haskell,我可以快速切换正在使用的数据类型。 当使用 SBV 的 AlgReal 类型进行计算时,我
我正在使用Z3的Java API。在检查“满意度”(s.status)时,我遇到了段错误。有人可以帮忙调试这个问题吗?有什么方法可以转储消息以便我可以调试这个问题。我尝试使用 Log.open(),但
我是一名优秀的程序员,十分优秀!