如何解决如何在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
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。