How to access the AST for constraints in the input sygus file in CVC4 tool

I want to mutate the internal representation of constraints from the sygus file generated by CVC4.

For e.g. (constraint (and (<= x (f x y)) (<= y (f x y)))) is a constraint from small.sl which I give to cvc4 qas input to synthesize a program.

I know that cvc4 creates an internal representation using class Expr;

cvc4 defines a command cmd which seems to point to each statement in the sygus file which is as below:

(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)

I am concerned with the two constraints. I want to modify the constraints by commutating it around the operators as below:

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

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

For this, I am searching the object that points to the expression tree formed from constraint after parsing it.

This is how they declare their parser builder.

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

here pointer to parser is defined.

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

this is the command that points to the parsed statements from the input file.

std::unique_ptr<Command> cmd;

this is the class declarations for the internal representations.

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

class NodeManager;

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

does anyone know how to get the object for the expression tree?

Thanks in advance

Solution

To get the expression e associated with a (constraint e) command use SygusConstraintCommand::getExpr(). https://github.com/CVC4/CVC4/blob/b02977f0076ade00b631e8ee79a31b96bf7a24c4/src/smt/command.h#L842

You can get the commands from Parser::nextCommand().

There are several caveats to making use of this. Examples: parsing is not side effect free (the only documentation of the side effects is to read the source), commands in SMT can correspond to multiple CVC4 Commands, and you need to be able to generate new commands and replay them like CVC4's src/main/ binaries do. Also printing valid SMT-LIB from Exprs if you want to debug this is harder than it sounds. I am not sure what you are trying to accomplish, but I think you should reach out the [active] CVC4 folks directly for help: https://cvc4.github.io/people.html