我想从 CVC4 生成的 sygus 文件中改变约束的内部表示。
例如 (constraint (and (<= x (fxy)) (<= y (fxy)))) 是来自 small.sl 的约束，我将其提供给 cvc4 qas 输入以合成程序。
我知道 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;
有谁知道如何获取表达式树的对象？
提前致谢