问题标签 [cvc4]

使用此代码：

我得到以下回复：

但我希望是这样的：

我假设，参数inUnsatCore会SmtEngine.assertFormula以某种方式指导断言。但事实并非如此。

如果不是如上所示，断言公式和要求未饱和核心的正确方法是什么？

使用来自 github 的带有标签 1.5 的 cvc4 版本。

我一直在研究各种 SMT 求解器，主要是 Z3、CVC4 和 VeriT。他们对使用量词解决 SMT 问题的能力都有模糊的描述。他们的文档主要基于示例 (Z3)，或由学术论文组成，描述了可能实际实施或未实施的可能变化。

我知道一阶逻辑有可判定的片段，例如：

• 有界量词
• 一阶一阶逻辑

我想知道的是，哪些（如果有的话）FOL 类是保证完成的各种 SMT 求解器？我如何知道我正在查看的问题是否存在于它们完成的片段中？

I am looking for a solver that can provide models of formulas on real numbers involving logarithms or exponentials.

Can cvc4 handle functions which contain logarithms or exponentials of real numbers? Similarly, can cvc4 express the constant e?

According to this question, z3 can only handle constant exponents, which does not help me.

This question only asks about logarithms for integers.

我目前正在使用 CVC4 来解决以下形式的公式：

在这里，f1...fn是从某个数量Bool到的函数Bool，以及 b1...bk是布尔值。

我的问题完全属于UFSMT 的片段：它有量词，但除了函数和布尔值之外没有其他种类。

当我尝试使用 CVC4 上的默认设置解决问题时，它立即返回未知，尽管事实上我所有的量化都是在有限域上的。

问题是，CVC4 有非常多的处理量词的选项：有一堆cegqi，一堆fmf，还有mbqi等等。我的印象是这些大部分是从特定的研究项目中添加的，我宁愿不必阅读 20 篇不同的论文就可以让我的解决方案继续下去。

我的问题：是否有一组推荐的选项来解决此类问题？

我知道 CVC4 是可能的，因为他们在 SMT 比赛的UF Track上竞争并表现相当出色，但我找不到用于该比赛的具体论据。

I need to change "123" into a const in c++ what I coded as

or

but I got some error

Undefined symbols for architecture x86_64: "___gmpq_canonicalize", referenced from: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>::canonicalize() in ex1-4f9d4d.o "___gmpq_clear", referenced from: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>::~__gmp_expr() in ex1-4f9d4d.o "___gmpz_clear", referenced from: __gmp_expr<__mpz_struct [1], __mpz_struct [1]>::~__gmp_expr() in ex1-4f9d4d.o "___gmpz_init_set", referenced from: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>::__gmp_expr(__gmp_expr<__mpz_struct [1], __mpz_struct [1]> const&, __gmp_expr<__mpz_struct [1], __mpz_struct [1]> const&) in ex1-4f9d4d.o "___gmpz_init_set_si", referenced from: __gmp_expr<__mpz_struct [1], __mpz_struct [1]>::init_si(long) in ex1-4f9d4d.o ld: symbol(s) not found for architecture x86_64

我在 SMT-LIB 中使用 Int 定义时间步长，这迫使我断言事情以确保在否定中没有任何事情发生：

我看到在 Z3 中我们可以Nat用通常的样式定义 inductive s。使用归纳定义会更好，Nat还是有更好的方法来做我上面想做的事情？

我已经根据他们的手册从源代码构建了cvc4。我跑make check的很完美，然后sudo make install。然后，我尝试运行一个适用于 z3 的简单示例：

但我得到这个错误：

我究竟做错了什么？谢谢！

我正在尝试使用 Z3 和 CVC4 运行以下 unsat 示例。如果我用(seq.unit #x00)替换“\x00” ，那么这对 Z3 来说不是问题，但 CVC4 抱怨它不知道 seq.unit。

这是命令行调用：

以下是我使用 seq.unit 行时 cvc4 抱怨的内容：

使用截至 2018-07-10 的最新 cvc4，此代码：

从 cvc4 产生这个输出：

Z3 接受相同的数据类型声明。这不应该工作吗？那是一个错误吗？任何解决方法？

我刚刚在弦理论中遇到了一个 SMTLIB 问题，Z3 的回答可能不一致。调用Z3 解决问题时：带参数smt.string_solver=z3str3返回unsat；没有任何参数它返回sat。

我也使用 CVC4 来解决这个问题。它返回了一个解决方案，这似乎是一个有效的模型，因为我通过手动将变量分配替换为问题来检查它。

由于我正在尝试使用 Z3 进行研究，因此我想知道这是否是 Z3 的已知行为。感谢任何可以提供帮助的人！:)

编辑：我在 WSL Ubuntu 16.04 上使用 Z3 4.7.1。