diff options
author | Andrew V. Jones <andrew.jones@vector.com> | 2020-07-11 04:37:20 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-10 22:37:20 -0500 |
commit | b31f0397bc02b8d903dc7c1e82a1f1ae53729fa1 (patch) | |
tree | 64429f1924ee461eb72921e9ee97323992eac0db /src/smt/command.h | |
parent | 60fae1dc65b47723c83469d1fb20a9666ddc84a2 (diff) |
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
Diffstat (limited to 'src/smt/command.h')
-rw-r--r-- | src/smt/command.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index a6a0faaae..552847fee 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1114,6 +1114,8 @@ class CVC4_PUBLIC GetAbductCommand : public Command Expr getConjecture() const; /** Get the grammar type given for the abduction query */ Type getGrammarType() const; + /** Get the name of the abduction predicate for the abduction query */ + std::string getAbductName() const; /** Get the result of the query, which is the solution to the abduction query. */ Expr getResult() const; |