From b31f0397bc02b8d903dc7c1e82a1f1ae53729fa1 Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Sat, 11 Jul 2020 04:37:20 +0100 Subject: [PATCH] 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 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 --- src/printer/smt2/smt2_printer.cpp | 87 ++++++++++++++++++------------- src/smt/command.cpp | 1 + src/smt/command.h | 2 + 3 files changed, 55 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(out, c) || tryToStream(out, c) || tryToStream(out, c) - || tryToStream(out, c)) + || tryToStream(out, c) + || tryToStream(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& vars = c->getVars(); - Assert(!type.isFunction() || !vars.empty()); - out << '('; - if (type.isFunction()) - { - // print variable list - std::vector::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(sygusType).getDatatype().isSygus()) + if (!t.isNull() && t.isDatatype() + && static_cast(t).getDatatype().isSygus()) { std::stringstream types_predecl, types_list; std::set grammarTypes; std::list 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& vars = c->getVars(); + Assert(!type.isFunction() || !vars.empty()); + out << '('; + if (type.isFunction()) + { + // print variable list + std::vector::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 diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 095c59374..e60f223b4 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2192,6 +2192,7 @@ GetAbductCommand::GetAbductCommand(const std::string& name, Expr GetAbductCommand::getConjecture() const { return d_conj; } Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; } +std::string GetAbductCommand::getAbductName() const { return d_name; } Expr GetAbductCommand::getResult() const { return d_result; } void GetAbductCommand::invoke(SmtEngine* smtEngine) 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; -- 2.30.2