z3:归纳数据类型上的Horn子句/固定点
z3是一种高性能的定理证明器，它被广泛应用于形式化验证、软硬件验证、程序分析等领域。z3的核心功能是求解逻辑公式的可满足性和不可满足性，它支持多种逻辑理论，包括一阶逻辑、线性整数和实数算术、位向量、数组理论等。
在归纳数据类型上的Horn子句/固定点问题中，z3可以用于判断一个给定的Horn子句集合是否存在固定点。Horn子句是一种逻辑表达式，它由一个头部和一个可选的正体组成，头部是一个原子命题，正体是一个由原子命题和逻辑连接词构成的逻辑公式。固定点是指一个解，使得在该解下，Horn子句集合中的每个子句都成立。
z3可以通过将Horn子句集合转化为逻辑公式，并利用其内置的求解算法进行求解。如果存在固定点，z3将给出一个满足条件的解；如果不存在固定点，z3将给出不可满足的证明。
在实际应用中，归纳数据类型上的Horn子句/固定点问题可以用于形式化验证、程序分析等领域。例如，在软件验证中，可以将程序的规范表示为Horn子句集合，然后使用z3来验证程序是否满足规范。
腾讯云提供了一系列与云计算相关的产品和服务，其中包括计算、存储、数据库、人工智能等多个领域。具体推荐的腾讯云产品和产品介绍链接地址可以根据具体需求和场景进行选择。
相关·内容
1回答
如果要分析的程序的语义以Horn子句的形式给出，则Z3现在支持求解归纳不变量(暗示所需的属性)。
但是，上Z3源代码的master分支中的版本不支持此功能。由于Z3通过使用插值的PDR算法解决了这些Horn子句问题，因此我转而编译了支持(set-logic HORN)的interp分支(d8b31773b809)。
据我所知，Horn子句问题是用表示不变量的未知谓词来指定的，而X×Y上的谓词只是从X×Y到Bool的函数。到目前一切尚好。
我尝试的第一个例子只是推断for(int i=0; i<=10; i++)循环的归纳不变量的问题。
(set-logic HORN)
(declare-
浏览 2提问于2013-07-06得票数 3
我正在使用Z3来解决我的horn子句。在Horn子句的主体中，未解释的谓语应该是肯定的。但是，我需要否定一些未解释的谓词。 我见过一些例子，在这些例子中否定效果很好。例如，对于以下示例，Z3将返回sat： (set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((k Int)) (or (> k 10) (not (inv k)) (inv (+ k 1)))))
(check-sat) 但我的示例如下所示，其中Z3返回unknown。 (set-logic HORN)
(decl
浏览 18提问于2019-10-11得票数 1
回答已采纳
1回答
我正在尝试使用中的z3实现一些GDL c#，而且我几乎被困在了起始块中。
基本上，我想从下面的gdl开始非常简单
(role you)
(init (state 0))
(<= (legal you proceed)
(true (state 0)))
(<= (next (state 1))
(does you proceed))
(<= terminal
(true (state 1)))
(<= (goal you 100))
然后询问哪一个“法律”是可满足的(在这个设计的例子中，只有一个合法的，在信息状态下是可满足的)。
看一下z3示例，看起来我需要创
浏览 2提问于2013-08-01得票数 1
回答已采纳
就像我们一样，Z3有递归的局限性。有没有办法得到以下程序的结果？什么额外的方程式将帮助z3得到结果？
from z3 import *
ackermann=Function('ackermann',IntSort(),IntSort(),IntSort())
m=Int('m')
n=Int('n')
s=Solver()
s.add(ForAll([n,m],Implies(And(n>=0,m>=0),ackermann(m,n) == If(m!=0,If(n!=0,ackerma
浏览 0提问于2017-07-10得票数 3
回答已采纳
2回答
达夫尼可以选择设置{:induction false}。而且，据我所知，每当我们在Dafny中使用断言时，在它下面发生了什么，它构造了证明义务，然后使用Z3对它们进行计算。
然而，我读到Z3不支持归纳:例如.然而，任何非平凡的属性都需要通过归纳法来证明.Z3目前不支持归纳证明.()
因此，我的问题是:每当我们设置{:induction true}时，如果不使用Z3，在Dafny中如何执行这种归纳？有不同的潜在求解者吗？有什么启发法吗？最后一个建议是在这里()。
然而，我们讨论的是哪种启发式方法呢？
浏览 39提问于2022-09-26得票数 1
回答已采纳
2回答
我对量词有问题。
设a(0) = 0，根据x(n)的值，a(n)+1或a(n)+2。我们可以预期，对于任何类型的x(.)对于所有n，a(n) <= n*2。
下面是Z3的代码：
(declare-fun a (Int) Int)
(declare-fun x (Int) Int)
(declare-fun N () Int)
(assert (forall
((n Int))
(=> (>= n 0)
(= (a (+ n 1))
(ite (> (x n) 0)
(+ (a n) 1)
浏览 1提问于2017-10-27得票数 3
回答已采纳
当我们谈到的时候，我一直在试图弄清楚xor Z的功能和局限性。我教过Z3关于用户定义排序的xor理论，但它无法有效地应用规则，导致对任何有趣的查询都使用unknown。配对后，我得到了这个令人惊讶的返回unknown的示例
(set-logic HORN)
(declare-fun p (Bool Bool Bool) Bool)
; Test if Z3 can discover two a1+b1+c1 by canceling ra, rb, and rc
(assert (exists ((a1 Bool) (b1 Bool) (c1 Bool) (ra Bool) (rb Bool
浏览 4提问于2013-07-06得票数 3
回答已采纳
我正在使用Z3中的Horn Logic来对进程代数进行建模检查，因为Horn Logic擅长处理递归定义。但是，我陷入了一些棘手的问题中。例如，我有以下代码：
(declare-rel A (Int))
(declare-rel B (Int))
(rule (A 1))
(rule (A 2))
(rule (B 1))
(rule (B 2))
那么，我如何证明A和B相等呢？这类似于使用角点逻辑证明Z3中两个集合的等价性。
有没有人能给我点提示？非常感谢。
浏览 1提问于2016-02-13得票数 1
使用Yices使用归纳数据类型进行计算的一个简单示例是：
(define-type T (datatype c1
c2
(c3 val::bool)))
(define x1::T)
(define x2::T)
(assert (/= x1 x2))
(check)
相应的输出是：
sat
(= x1 c1)
(= (c3 false) x2)
此示例使用以下代码使用Z3-SMT-LIB进行求解
(declare-datatypes () ((T c1 ( c3 (T Bool)))))
(declar
浏览 1提问于2013-12-01得票数 1
回答已采纳
我的第一个问题是，我是否可以用Z3Py表示以下公式：
Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t<arr[i])
这意味着:数组中是否存在一个位置i::0<i<|arr|，其值a[i]大于数组avg(arr)的平均值加上给定的阈值t。
我知道这种表达式可以在Dafny中查询，而且(因为Dafny在下面使用Z3 )，我想这可以在Z3Py中完成。
我的第二个问题是: Z3中涉及数组的可判定片段的表达能力如何？我阅读了关于数组的全部理论是如何不可判定的()，而只是一个具体的片段，数组属性片段。
是否有任何有
浏览 8提问于2022-09-19得票数 0
回答已采纳
我使用不稳定分支中的Z3来试验Horn子句(提交61385c8489b7fda11b518a67fe308ea3cfe28c3d)。我可以让Z3推断出一些循环不变量，这很好。然而，通过以下简单的示例，我对Z3的行为感到困惑。这里我漏掉了什么？
示例1：
(set-logic HORN)
(declare-const C Int)
(assert (> C 2))
(check-sat)
(get-model)
我希望得到一个模型，但收到的却是“未知”。
示例2：
(set-logic HORN)
(define-fun step ((I Int) (I1 Int)) Bool (= I1
浏览 3提问于2013-11-29得票数 1
1回答
通过下面的示例，我试图以量化的方式对所有可能的列表的长度设置一个限制。这将导致一个“非卫星”的结果，我相信这是正确的。
有人能详细说明为什么这是不能满足的，如果有办法绕过这个限制而不将长度限制放在特定的变量/常量上呢？
我发现很有趣，但我的问题并没有得到真正的回答。此外，答案是旧的，并参考SMT-LIB版本2.0 (以及一个对一个未量化的版本)。也许Z3现在能够以一种我不知道的方式做到这一点。
(set-logic ALL)
(set-option :produce-unsat-cores true)
(declare-datatypes ((List 1)) ((par (T) ((con
浏览 1提问于2021-01-21得票数 0
回答已采纳
我的目标是将队列定义为z3数据类型(在z3py中)，这样我就可以将队列上的操作作为约束来执行。有没有办法这样做，如果有，那又是什么呢？
我的第一本能是使用代数数据类型(ADT)，比如在OCaml或Haskell中经常使用的递归函数定义。我发现了一些不久前在z3中讨论ADT的文章，比如。其他帖子上的一些答案声称z3不支持递归，但是对这个问题的公认答案定义了一个非常类似于我想要的函数，所以我不知道正确的/最新的答案是什么。
def queuegen(sort):
Queue = Datatype('Queue_of_%s' % sort.name())
Queue.
浏览 0提问于2019-08-01得票数 0
回答已采纳
我正在研究使用Z3作为SMT求解器的自动程序验证。更具体地说，我正在尝试解析带注释的程序，其中包含对其预期行为的规范，以便可以使用Z3自动生成和验证证明义务。我知道Dafny确实做到了这一点，而且做得非常好。然而，完全不清楚Dafny是如何在内部做到这一点的，我正在尝试确定Z3可以直接用于此目的的扩展。但是，当我开始使用从数组常量中选择的值作为递归函数的参数时，就开始出现意外的问题。
在SMT中，该问题可以简化为以下最小示例：
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun d () (Array Int Int))
(de
浏览 19提问于2021-09-14得票数 0
我只是对horn子句的定义感到困惑。"~A=>B“是一个从句吗？如果我们将它转换成析取形式，它将是"AvB“，而不是horn子句。
所以我想知道这是不是一个号角条款。谢谢。
浏览 5提问于2013-12-11得票数 2
我试图养成使用达芙妮作为一些简单公式的友好的SAT-QBF解算器的习惯，例如，在Z3中这样做太不舒服了。
这里的上下文是，我已经实现了Cooper的量化消去算法，当所有变量都有界时，它可以用作一个决策过程:因此，我想知道在执行它之前应该得到哪个结果。
然而，我在达夫尼遇到了一个问题。
例如，让我们提出这个公式(用达夫尼写的)：
assert forall x_1: int :: exists y_1: int :: forall x_2: int :: exists y_2 : int
:: (y_2<y_1) && (x_2<y_2) &&am
浏览 6提问于2021-05-24得票数 1
回答已采纳
1回答
我想通过muZ为BMC使用z3。也许我遗漏了一些关于查询可满足性的定义。然而，在下面的例子中，我有一个无法满足的查询示例(即，返回"false")，但是当添加额外的约束(有效地给出令人满意的赋值)时，将返回一个有效的赋值。
是否有任何文档可以帮助理解z3的muZ语言扩展的确切语义？
谢谢并致以最好的问候！
使用Z3版本4.3.2执行以下.smt2-file将导致以下结果：
formula undetermined in model: (= (head query!0_0_n) (state c1 1))
sat
false
sat
(let ((a!1 (insert (sta
浏览 1提问于2013-09-16得票数 0
1回答
我希望得到定点φ中元素的约束，在下面的例子中，约束应该是c2<=c1+5.0，c1>=5.0它应该是如何在Z3中实现它？或者，有没有什么方法可以不使用Z3中的固定点
(set-option :produce-models true)
(set-option :dl_engine 1)
(set-option :dl_pdr_use_farkas true)
(declare-var c1 Real)
(declare-var c2 Real)
(declare-var lambda Real)
(declare-rel phi(Real Real))
(rule
(=>
浏览 1提问于2012-09-03得票数 1
回答已采纳
1回答
关于Z3如何增量地解决问题，我有一个问题。在阅读了这里的一些答案后，我发现如下：
使用Z3进行增量求解的方法有两种:一种是push/pop(堆栈)模式，另一种是使用假设。。
在堆栈模式下，z3将忘记全局中的所有学习引理(对吗？)范围，即使在一个本地"pop“之后
在假设模式(我不知道名称，也就是我想到的名称)中，z3不会简化某些公式，例如值传播。
我做了一些比较(欢迎您询问公式，它们太大，不能放在rise4fun上)，但下面是我的观察:对于一些公式，包括量词，假设模式更快。在一些具有大量布尔变量(假设变量)的公式中，堆栈模式比假设模式更快。
这些措施是否为特定目的而
浏览 2提问于2013-05-07得票数 54
回答已采纳
我正在Z3中试用PDR引擎，我不确定要使用哪个版本的Z3。
git公司的“官方”支部似乎运转良好，但日期是2012年11月。我敢肯定，从那时起，情况有所改善。另一方面，不稳定分支“可能包含不稳定和/或未经测试的代码”，这似乎是正确的。
什么是最新的“稳定”版本的引擎？
例如
(declare-rel R (Real Real))
(declare-var x Real)
(declare-var y Real)
(rule
(=> (and (= x 0) (= y 0)) (R x y))
)
(rule
(=> (R x y) (R (+ x 1) (+ y
浏览 2提问于2014-08-30得票数 1
回答已采纳
我有一个LLVM字节码的描述，我需要作为Z3输入传递。如果可以做到，那该怎么做呢？如果没有，有什么工具可以做到吗？？
浏览 0提问于2014-02-12得票数 1
2回答
z3是否为两个列表提供了叉积函数？如果没有，是否可以在不使用高阶函数或使用提供的列表函数的情况下定义一个函数？我一直在尝试给它下定义。我知道如何使用map定义一个，但我不认为z3支持这一点。
浏览 0提问于2012-05-18得票数 1
回答已采纳
我已经在Z3/Horn (unstable分支)中使用了以下示例
(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (=> (and (<= I 1000) (inv I)) (inv (+ I 1)))))
(assert (forall ((I Int)) (=> (inv I) (<= I 10000))))
(check-sat)
(get-model)
推导出不变x≤1001需要8.5秒。这是出乎意料的长...
如果我用1500代替1
浏览 2提问于2013-07-09得票数 0
我试图在匹配全名的文档上获得更高的分数，而不是使用相同值的边缘NGram子集。
结果是：
Pos Name _score _id
1 Baritone horn 7.56878 1786
2 Baritone ukulele 7.56878 2313
3 Bari 7.56878 2360
4 Baritone voice 7.56878 1787
我想第三个(“巴里”)将有一个更高的分数，因为它是全名，但是，因为边缘ngram分解将使所有其他的准确“巴里”字索引。
浏览 2提问于2015-09-15得票数 1
回答已采纳
由于Z3发布了新的.NET接口，在我看来，定点接口发生了变化。
但是，我找不到有关如何使用新API的详细信息。
有谁能给我点吃的吗？
浏览 0提问于2012-05-18得票数 1
回答已采纳
我试图从证明一个示例，这个示例位于Sect.6.2.4，但我修改了一些代码。
#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#define size 150
/*@
axiomatic Counter{
logic integer counter{L}(bool arr[size], integer begin, integer end) reads arr[0 .. (size-1)];
axiom count_emp
浏览 10提问于2022-09-20得票数 2
回答已采纳
我正在尝试一些涉及递归函数的示例。我已经尝试了下面的例子。
(第8.3条)
(第8.3条)
(第10.5条)
在上述所有示例中，都会超时。但是，本教程似乎暗示只有是不终止的。
Z3可以检查包含递归函数的公式的可满足性，还是不能处理任何归纳事实？
浏览 0提问于2011-08-02得票数 4
回答已采纳
2回答
当我在定点Z3Py中启用解释生成选项时，我将得到一个包含以下消息的核心转储。
设置‘DL_GENERATE_ Error’错误，原因:未知选项。
在抛出“z3_error”中止的实例后调用的终止(内核转储)
我在Ubuntu12.04上使用了Z3 4.2，并在“解释”一节中得到了Z3Py文档中给出的示例的错误。
我想知道是什么导致了这个问题。
浏览 4提问于2012-11-01得票数 1
回答已采纳
1回答
我试图将整数a的整数和表示为窗体的整数b
\sum_{i=a}^b i
对于这个版本，有一个封闭的表单解决方案，但总的来说，我想对i参数化的表达式进行求和。目前，我尝试定义一个函数symSum，并使用通用量词描述了它的行为：
from z3 import *
s = Solver()
symSum = Function('symSum', IntSort(), IntSort(), IntSort())
a = Int('a')
b = Int('b')
s.add(ForAll([a,b],If(a > b,symSum(a,b) ==
浏览 2提问于2021-03-18得票数 2
回答已采纳
在Isabelle中，我试图对相互递归的归纳定义进行规则归纳。下面是我能够创建的最简单的示例：
theory complex_exprs
imports Main
begin
datatype A = NumA int
| AB B
and B = NumB int
| BA A
inductive eval_a :: "A ⇒ int ⇒ bool" and eval_b :: "B ⇒ int ⇒ bool" where
eval_num_a: "eval_a (NumA i) i" |
eval_a_b
浏览 4提问于2015-10-08得票数 3
回答已采纳
1回答
此文件是否符合SMT2.0标准？至少，z3可以接受它。顺便问一下，‘declare const’和'declare-fun‘有什么区别？例如，为了声明一个Bool变量，我可以编写declare-const a Bool或declare-fun a() Bool。
浏览 0提问于2013-01-06得票数 1
回答已采纳
2回答
证明定理时的循环
、、、
在使用Debruijn指数和Coq中的替换将lambda演算形式化后，我试图证明以下定理。 Theorem atom_equality : forall e : expression , forall x : nat,
(beta_reduction (Var x) e) -> (e = Var x). 这些是表达式和beta约化的定义 Inductive expression : Type :=
| Var (n : nat)
| Abstraction (e : expression)
| Application (e1 : expression) (e2 : ex
浏览 37提问于2021-04-02得票数 0
我正在使用Z3中的定点引擎来编码几个通用的horn公式。查询结果是unsat.在Z3Py中，使用get_answer()将计算结果返回给未解释的关系。但是，在SMTLIB2格式中，get-answer返回unsupported。下面是我的程序：
(declare-var x Int)
(declare-var y Int)
(declare-rel I (Int) interval_relation)
(declare-rel I1 (Int) interval_relation)
(declare-rel err (Int) interval_relation)
(rule (=>
浏览 6提问于2013-11-06得票数 1
编辑
Require Import Bool List ZArith.
Variable A: Type.
Inductive error :=
| Todo.
Inductive result (A : Type) : Type :=
Ok : A -> result A | Ko : error -> result A.
Variable bool_of_result : result A -> bool.
Variable rules : Type.
Variable boolean : Type.
浏览 2提问于2012-11-08得票数 4
回答已采纳
我想得到的是“获取前5个不同客户的订单id值”。当我将下面的查询限制为5时，它只会按预期返回前4个客户的订单id值。(在角周围有两个不同的订单id)，有方法获得前5个不同客户的订单id值吗？
SELECT Customers.CustomerName, Orders.OrderID
FROM Customers
LEFT JOIN Orders
ON Customers.CustomerID=Orders.CustomerID
ORDER BY Customers.CustomerName;
CustomerName OrderID
Alfre
浏览 9提问于2016-11-29得票数 1
回答已采纳
在Z3求解器中，我希望使用定点表示法来表示数字，并使用四舍五入来执行算术运算。 例如:假设X、Y和Z表示定点数字类型， X[4,3] Total 4 digits number with 3 digits after the decimal.
Y[4,2]
Z[4,1]
Assign fixed point numbers to X, Y
X = 1.234 ( here there are total 4 digits & decimal digits are 3 )
Y = 45.67
Perform the Fixed point numbers Arithmetic
浏览 15提问于2020-06-24得票数 1
回答已采纳
1回答
如何使用Prolog将CNF子句转换为Horn形式？我正在尝试创建一个SAT求解器，有CNF作为输入，这将需要转换为号角形式。
浏览 12提问于2017-08-26得票数 1
回答已采纳
在z3中有没有连接两个列表的方法？类似于ML中的@运算符？我正在考虑自己定义它，但我不认为z3支持递归函数定义，即，
define-fun concat ( (List l1) (List l2) List
(ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) )
)
浏览 4提问于2012-05-07得票数 3
回答已采纳
用的机型是VIVO Z3，经测试 其他机子也是如此情况，先黑屏，后白屏，延迟10后几秒进入app，没出现崩溃现象
image.png
image.png
浏览 496提问于2019-10-15
我想知道z3是否支持关联数组(也就是地图)？如果不是，有没有一种简单的方法可以使用当前版本的z3对这种数据结构进行建模？
浏览 0提问于2014-11-16得票数 2
1回答
我计划使用Microsoft的Z3 SMT解决程序做一些工作，它将在有执行时间限制的计算服务器上运行。我预计这项工作将超过这一限度。这个计算中心的推荐策略是使用“检查点”并调用一系列作业，每个作业从前一个作业中拾取检查点并继续工作。这样，任何进程的运行时间都不会超过执行时间限制，因此其他用户也有机会运行他们的作业，但是使用的总计算时间可以超过单个作业的超时时间。
Z3是否支持读写检查点？
所谓“检查点”，我指的是序列化( Z3解决程序的某些部分)内部状态的文件，例如如果Z3进程写入检查点并退出，然后启动第二个Z3进程来读取检查点文件，在读取它之后，新Z3进程的状态与前一个进程的状态相同(因此解
浏览 5提问于2015-02-25得票数 0
回答已采纳
1回答
我正在尝试编写一个在Seq Int上运行的max函数。它应该返回最大值的索引。以下是我所拥有的：
(declare-fun max ((Seq Int)) Int)
(assert (forall ((A (Seq Int)))
(=>
(> (seq.len A) 0)
(and
(<= 0 (max A))
(< (max A) (seq.len A))
(forall ((i Int))
(=>
浏览 0提问于2019-07-28得票数 0
回答已采纳
2回答
我知道我可以在Z3中通过单独声明元素来声明一个z3.Real矩阵(可能是通过列表理解)。有没有办法表示一个大小未知的矩阵？
例如，考虑以下示例:在图像滤波中，给定size [X,Y]的图像i和size [M,N]的滤波核K，图像I和滤波核K之间的卷积为I*K。我希望Z3能证明(或反驳)存在任何大小的过滤器F1和F2，比如I*K == I*F1*F2。
问题本身完全是虚构的，可能没有任何意义。我的想法是，我是否可以要求Z3找到一个大小未知的矩阵，使该矩阵满足某些可以用线性函数表示的性质。谢谢!
浏览 2提问于2017-04-14得票数 0
我试图用Z3对扩展的欧几里得算法进行建模，但遇到了无限循环。
欢迎提出建议和意见。
第一个函数是用Python编写的，仅供参考。
第二个函数是在z3分析它时陷入无限循环的函数。
您是否发现我将常规Python函数映射到相应的Z3语法中有什么错误？
'''
Returns d, x, y such that a*x + b*y = d
d = gcd(a, b)
'''
def extended_euclid_rec(a, b):
if b == 0:
d = a; x = 1; y = 0 # y can be any in
浏览 12提问于2021-05-04得票数 0
不幸的是，我没有足够的声誉来评论其他问题的答案。所以我必须开始一个新的问题。
从本质上讲，我遇到了与所描述的相同的问题。我想使用Z3进行增量求解。为了将约束放入Z3，我使用了smtlib2字符串。对于第一组约束，一切都很正常，我可以将变量的声明等直接放入smtlib2字符串中。当以增量方式添加附加约束时，Z3_parse_smtlib2_string需要接收先前声明的数量(无符号num_decls)、声明(Z3_func_decl const decls[] )及其名称(Z3_symbol const decl_names[])。对于smtlib字符串，解析器接口提供了检索此信息的函数，例如&
浏览 2提问于2013-05-20得票数 1
回答已采纳
我知道z3在一般情况下不能验证归纳证明。但我很好奇是否有办法让它检查一些简单的东西，比如：
; returns the same input list after iterating through each element
(declare-fun iterate ((List Int)) (List Int))
(declare-const l (List Int))
(assert (forall ((l (List Int)))
(ite (= l nil)
(= (iterate l) nil)
(= (iterate l) (insert (head l)
浏览 4提问于2017-08-29得票数 3
回答已采纳
1回答
Z3条件语句
、、
如何在Z3中编写条件语句。
eg:
if (a%2==0){
value=1
}
我正试图在微软研究院的Z3解算器中实现这一点，但到目前为止还没有成功
浏览 1提问于2017-06-02得票数 0
2回答
我有一个关于在MATLAB中为德州仪器TMS320C64xx数字信号处理器编写算法的问题：
我有一个工作草率的实现，我的过滤器在MATLAB。我的目标是使用MATLAB嵌入式编码器将该算法转换为C，然后将其导入并加载到DSP上。
为了做到这一点，我知道我需要对我的MATLAB代码做一些事情。例如，我需要为矩阵预先分配空间，这样它就知道要使它们的大小(除非我想要为可变大小的数据而烦恼)。所有这些把MATLAB代码转换成C‘’ish代码，使MATLAB编码器能够或多或少地将它转换成代码。但是，我不知道如何确保我的数据类型(例如，我的过滤器的系数)是不动点，而不是浮点，这样MATLAB嵌入式编码器将
浏览 1提问于2011-06-13得票数 4
回答已采纳
我在SMT-LIB中使用Int定义时间步长，这迫使我断言事情，以确保在负片中没有发生任何事情：
(declare-sort Pkg) ; A package
(define-sort Time () Int) ; The installation step
; ...
(assert (forall ((t Time) (p Pkg)) (=> (< t 0) (not (installed p t)))))
我看到在Z3中，我们可以用通常的风格来定义归纳Nat。使用Nat的归纳定义是不是很好，或者有没有更好的方法来做我上面试图做的事情？
浏览 26提问于2018-03-03得票数 1
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
