Я хочу изменить внутреннее представление ограничений из файла sygus, сгенерированного CVC4.
Например, (ограничение (и (‹= x (f x y)) (‹= y (f x y)))) — это ограничение из small.sl, которое я передаю в cvc4 в качестве входных данных для синтеза программы.
Я знаю, что 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;
кто-нибудь знает, как получить объект для дерева выражений?
заранее спасибо
