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/printer | |
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/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 87 |
1 files changed, 52 insertions, 35 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 773c733d6..bb3870ee5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1297,7 +1297,8 @@ void Smt2Printer::toStream(std::ostream& out, || tryToStream<DeclareSygusVarCommand>(out, c) || tryToStream<SygusConstraintCommand>(out, c) || tryToStream<SygusInvConstraintCommand>(out, c) - || tryToStream<CheckSynthCommand>(out, c)) + || tryToStream<CheckSynthCommand>(out, c) + || tryToStream<GetAbductCommand>(out, c)) { return; } @@ -2049,45 +2050,16 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v) -------------------------------------------------------------------------- */ -static void toStream(std::ostream& out, const SynthFunCommand* c) +static void toStreamSygusGrammar(std::ostream& out, const Type& t) { - out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()) - << ' '; - Type type = c->getFunction().getType(); - const std::vector<Expr>& vars = c->getVars(); - Assert(!type.isFunction() || !vars.empty()); - out << '('; - if (type.isFunction()) - { - // print variable list - std::vector<Expr>::const_iterator i = vars.begin(), i_end = vars.end(); - Assert(i != i_end); - out << '(' << *i << ' ' << i->getType() << ')'; - ++i; - while (i != i_end) - { - out << " (" << *i << ' ' << i->getType() << ')'; - ++i; - } - FunctionType ft = type; - type = ft.getRangeType(); - } - out << ')'; - // if not invariant-to-synthesize, print return type - if (!c->isInv()) - { - out << ' ' << type; - } - // print grammar, if any - Type sygusType = c->getSygusType(); - if (sygusType.isDatatype() - && static_cast<DatatypeType>(sygusType).getDatatype().isSygus()) + if (!t.isNull() && t.isDatatype() + && static_cast<DatatypeType>(t).getDatatype().isSygus()) { std::stringstream types_predecl, types_list; std::set<Type> grammarTypes; std::list<Type> typesToPrint; - grammarTypes.insert(sygusType); - typesToPrint.push_back(sygusType); + grammarTypes.insert(t); + typesToPrint.push_back(t); NodeManager* nm = NodeManager::currentNM(); // for each datatype in grammar // name @@ -2136,6 +2108,39 @@ static void toStream(std::ostream& out, const SynthFunCommand* c) out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ')'; } +} + +static void toStream(std::ostream& out, const SynthFunCommand* c) +{ + out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()) + << ' '; + Type type = c->getFunction().getType(); + const std::vector<Expr>& vars = c->getVars(); + Assert(!type.isFunction() || !vars.empty()); + out << '('; + if (type.isFunction()) + { + // print variable list + std::vector<Expr>::const_iterator i = vars.begin(), i_end = vars.end(); + Assert(i != i_end); + out << '(' << *i << ' ' << i->getType() << ')'; + ++i; + while (i != i_end) + { + out << " (" << *i << ' ' << i->getType() << ')'; + ++i; + } + FunctionType ft = type; + type = ft.getRangeType(); + } + out << ')'; + // if not invariant-to-synthesize, print return type + if (!c->isInv()) + { + out << ' ' << type; + } + // print grammar, if any + toStreamSygusGrammar(out, c->getSygusType()); out << ')'; } @@ -2182,6 +2187,18 @@ static void toStream(std::ostream& out, const CheckSynthCommand* c) out << '(' << c->getCommandName() << ')'; } +static void toStream(std::ostream& out, const GetAbductCommand* c) +{ + out << '('; + out << c->getCommandName() << ' '; + out << c->getAbductName() << ' '; + out << c->getConjecture(); + + // print grammar, if any + toStreamSygusGrammar(out, c->getGrammarType()); + out << ')'; +} + /* -------------------------------------------------------------------------- End of Handling SyGuS commands |