Add support for printing 'get-abduct' in verbose mode (#4710)

Issue
For any of the following files:

test/regress/regress1/abduct-dt.smt2
test/regress/regress1/sygus-abduct-test-ccore.smt2
test/regress/regress1/sygus-abduct-test.smt2
test/regress/regress1/sygus-abduct-ex1-grammar.smt2
test/regress/regress1/sygus-abduct-test-user.smt2
test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
test/regress/regress1/sygus/abduction_streq.readable.smt2
test/regress/regress1/sygus/abd-simple-conj-4.smt2
test/regress/regress1/sygus/uf-abduct.smt2
test/regress/regress1/sygus/yoni-true-sol.smt2
running the following:

./bin/cvc4 -vvv <file>
would print:

Invoking: ERROR: don't know how to print a Command of class: N4CVC416GetAbductCommandE
Resolution
This PR adds support in src/printer/smt2/smt2_printer.cpp to be able to print a Command of type GetAbductCommand.

Given the similarities between get-abduct and synth-fun, I have refactored the printing logic in toStream(std::ostream& out, const SynthFunCommand* c) for a printing a SyGuS grammar to be shared between both SynthFunCommand and GetAbductCommand.

As a result, you now see something like this:

[avj@tempvm build]$ ./bin/cvc4 -vvv ../test/regress/regress1/abduct-dt.smt2
Invoking: (set-option :incremental false)
Invoking: (set-logic ALL)
Invoking: (declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))

Invoking: (declare-fun x () List)
Invoking: (assert (distinct x nil))
minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy.
Invoking: (get-abduct A (= x (cons (head x) (tail x))))
(error "Cannot get abduct when produce-abducts options is off.")
Signed-off-by: Andrew V. Jones andrew.jones@vector.com

0 files changed, 0 insertions, 0 deletions