如何在CVC4工具中输入sygus文件中的约束访问AST

问题描述

我想从CVC4生成的sygus文件中更改约束的内部表示形式。

例如（constraint（and（

我知道cvc4使用Expr类创建内部表示形式；

cvc4定义了一个命令cmd，该命令似乎指向sygus文件中的每个语句，如下所示：

(set-logic LIA)

(synth-fun f ((x Int) (y Int)) Int)

(declare-var x Int)
(declare-var y Int)
(constraint (= (f x y) (f y x)))
(constraint (and (<= x (f x y)) (<= y (f x y))))

(check-synth)

我担心这两个约束。我想通过在运算符周围交换约束来修改约束，如下所示：

(constraint (and (<= x (f x y)) (<= y (f x y)))) commutated to

(constraint (and (<= y (f x y)) (<= x (f x y))))

为此，我正在搜索的对象指向解析后由约束形成的表达式树。

这就是他们声明其解析器生成器的方式。

ParserBuilder parserBuilder(pExecutor->getSolver(),filename,opts);

此处定义了指向解析器的指针。

std::unique_ptr<Parser> parser(parserBuilder.build());

这是指向输入文件中已解析语句的命令。

std::unique_ptr<Command> cmd;

这是内部表示形式的类声明。

// The internal expression representation
template <bool ref_count>
class NodeTemplate;

class NodeManager;

class Expr;
class ExprManager;
class SmtEngine;
class Type;
class TypeCheckingException;
class TypeCheckingExceptionPrivate;

有人知道如何获取表达式树的对象吗？

预先感谢

解决方法

这听起来像是一件危险且不必要的事情：为什么要直接与生成的约束混淆？确实应该在生成这些约束的工具中解决该问题。

即使可以访问内部，弄乱内部CVC4表示也可能意味着您违反了一堆内部不变式，并且求解器状态很可能变为无效。

如果您无法访问生成系统，建议将SMTLib转储到文件中，将其读取为文本，根据需要进行更改，然后在其上调用cvc4。这是确保CVC4内部不变式保持完整的唯一方法。

,

要获取与（约束e）命令关联的表达式e，请使用Parser::nextCommand()。 https://github.com/CVC4/CVC4/blob/b02977f0076ade00b631e8ee79a31b96bf7a24c4/src/smt/command.h#L842

您可以从src/main/获取命令。

对此有一些警告。示例：解析不是没有副作用的（唯一的副作用文档是阅读源代码），SMT中的命令可以对应于多个CVC4命令，并且您需要能够生成新命令并像CVC4的{{ 1}}二进制文件可以。如果要调试，也要从Exprs打印有效的SMT-LIB，这比听起来要难。我不确定您要完成的工作，但是我认为您应该直接与[活跃的] CVC4人员联系以寻求帮助：https://cvc4.github.io/people.html