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

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 773c733d65e7a84ac1e45dc30df9edfc6b0161d8..bb3870ee5adee12c0fded95ba17188e85343f30b 100644 (file)
--- 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

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 095c593742adb63dab1bd2a1a8d014a4b115b1de..e60f223b462e9e5b0a2a020f486c1e9770169d31 100644 (file)
--- 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 a6a0faaaee29e73cef564b6431a8e0a589482564..552847feed009cc0596c2991ebc95c79946d37be 100644 (file)
--- 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;