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

Question

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

Answer 1

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

Answer 2

This sounds like a dangerous and unnecessary thing to do: Why would you want to directly mess with a generated constraint? This should really be addressed in the tool that generates those constraints.

Even if you got access to the internals, messing up internal CVC4 representation might mean you violate a bunch of internal invariants and the solver state would most likely become invalid.

If you have no access to the generating system, I'd recommend dumping the SMTLib to a file, read it as text, change it as you see fit, and then call cvc4 on it. This would be the only way to ensure you keep CVC4 internal invariants intact.