Stop using the solver for printing sygus synthesis solutions. (#6530)

This PR uses custom methods for printing the synthesis solutions instead of Solver::printSynthSolution, which is going to be removed by #6521.

diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt
index 7b713e6e771063cc059c3cd54f3c4c865ba4227d..bff7caa4d9c10e9427d21dab3109869354f825bc 100644 (file)
--- a/examples/api/CMakeLists.txt
+++ b/examples/api/CMakeLists.txt
@@ -24,11 +24,18 @@ set(CVC5_EXAMPLES_API
   sets
   sequences
   strings
+)
+
+foreach(example ${CVC5_EXAMPLES_API})
+  cvc5_add_example(${example} "" "api")
+endforeach()
+
+set(SYGUS_EXAMPLES_API
   sygus-fun
   sygus-grammar
   sygus-inv
 )
 
-foreach(example ${CVC5_EXAMPLES_API})
-  cvc5_add_example(${example} "" "api")
+foreach(example ${SYGUS_EXAMPLES_API})
+  cvc5_add_example(${example} "${example}.cpp utils.h utils.cpp" "api")
 endforeach()

diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp
index 6eeffff1cdbb4d7ed8aac0a6e232144a72f95738..0f96e72a7d6f38c6747da42ce3dcea9e7638ba1c 100644 (file)
--- a/examples/api/sygus-fun.cpp
+++ b/examples/api/sygus-fun.cpp
@@ -41,15 +41,19 @@
  *
  * (check-synth)
  *
- * The printed output to this example should be equivalent to:
- * (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
- * (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
+ * The printed output for this example should be equivalent to:
+ * (
+ *   (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
+ *   (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
+ * )
  */
 
 #include <cvc5/cvc5.h>
 
 #include <iostream>
 
+#include "utils.h"
+
 using namespace cvc5::api;
 
 int main()
@@ -126,9 +130,12 @@ int main()
   if (slv.checkSynth().isUnsat())
   {
     // Output should be equivalent to:
-    // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
-    // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
-    slv.printSynthSolution(std::cout);
+    // (
+    //   (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
+    //   (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
+    // )
+    std::vector<Term> terms = {max, min};
+    printSynthSolutions(terms, slv.getSynthSolutions(terms));
   }
 
   return 0;

diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp
index 095f15889dfc1fe6b4c023a032a996f9270907cc..ce5a1bc8b715ce6a50223dd2e6041d16dde615a2 100644 (file)
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/sygus-grammar.cpp
@@ -36,17 +36,21 @@
  *
  * (check-synth)
  *
- * The printed output to this example should look like:
- * (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
- * (define-fun id2 ((x Int)) Int x)
- * (define-fun id3 ((x Int)) Int (+ x 0))
- * (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
+ * The printed output for this example should look like:
+ * (
+ *   (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
+ *   (define-fun id2 ((x Int)) Int x)
+ *   (define-fun id3 ((x Int)) Int (+ x 0))
+ *   (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
+ * )
  */
 
 #include <cvc5/cvc5.h>
 
 #include <iostream>
 
+#include "utils.h"
+
 using namespace cvc5::api;
 
 int main()
@@ -114,11 +118,14 @@ int main()
   if (slv.checkSynth().isUnsat())
   {
     // Output should be equivalent to:
-    // (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
-    // (define-fun id2 ((x Int)) Int x)
-    // (define-fun id3 ((x Int)) Int (+ x 0))
-    // (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
-    slv.printSynthSolution(std::cout);
+    // (
+    //   (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
+    //   (define-fun id2 ((x Int)) Int x)
+    //   (define-fun id3 ((x Int)) Int (+ x 0))
+    //   (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
+    // )
+    std::vector<Term> terms = {id1, id2, id3, id4};
+    printSynthSolutions(terms, slv.getSynthSolutions(terms));
   }
 
   return 0;

diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp
index 820fe86307d29915d6140477f0202ac86aaddf17..f658fa33af3acbaf25c99ee7fef13a74aa41561d 100644 (file)
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/sygus-inv.cpp
@@ -30,14 +30,18 @@
  *
  * (check-synth)
  *
- * The printed output to this example should be equivalent to:
- * (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
+ * The printed output for this example should be equivalent to:
+ * (
+ *   (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
+ * )
  */
 
 #include <cvc5/cvc5.h>
 
 #include <iostream>
 
+#include "utils.h"
+
 using namespace cvc5::api;
 
 int main()
@@ -82,8 +86,11 @@ int main()
   if (slv.checkSynth().isUnsat())
   {
     // Output should be equivalent to:
-    // (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
-    slv.printSynthSolution(std::cout);
+    // (
+    //   (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
+    // )
+    std::vector<Term> terms = {inv_f};
+    printSynthSolutions(terms, slv.getSynthSolutions(terms));
   }
 
   return 0;

diff --git a/examples/api/utils.cpp b/examples/api/utils.cpp
new file mode 100644 (file)
index 0000000..b7385d6
--- /dev/null
+++ b/examples/api/utils.cpp
@@ -0,0 +1,69 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementations of utility methods.
+ */
+
+#include "utils.h"
+
+#include <iostream>
+
+/**
+ * Get the string version of define-fun command.
+ * @param f the function to print
+ * @param params the function parameters
+ * @param body the function body
+ * @return a string version of define-fun
+ */
+std::string defineFunToString(const cvc5::api::Term& f,
+                              const std::vector<cvc5::api::Term> params,
+                              const cvc5::api::Sort& sort,
+                              const cvc5::api::Term body)
+{
+  std::stringstream ss;
+  ss << "(define-fun " << f << " (";
+  for (size_t i = 0, n = params.size(); i < n; ++i)
+  {
+    if (i > 0)
+    {
+      ss << ' ';
+    }
+    ss << '(' << params[i] << ' ' << params[i].getSort() << ')';
+  }
+  ss << ") " << sort << ' ' << body << ')';
+  return ss.str();
+}
+
+void printSynthSolutions(const std::vector<cvc5::api::Term>& terms,
+                         const std::vector<cvc5::api::Term>& sols)
+{
+  std::cout << '(' << std::endl;
+
+  for (size_t i = 0, n = terms.size(); i < n; ++i)
+  {
+    std::vector<cvc5::api::Term> params;
+    cvc5::api::Term body;
+    if (sols[i].getKind() == cvc5::api::LAMBDA)
+    {
+      params.insert(params.end(), sols[i][0].begin(), sols[i][0].end());
+      body = sols[i][1];
+    }
+    cvc5::api::Sort rangeSort = terms[i].getSort();
+    if (rangeSort.isFunction())
+    {
+      rangeSort = rangeSort.getFunctionCodomainSort();
+    }
+    std::cout << "  " << defineFunToString(terms[i], params, rangeSort, body)
+              << std::endl;
+  }
+  std::cout << ')' << std::endl;
+}

diff --git a/examples/api/utils.h b/examples/api/utils.h
new file mode 100644 (file)
index 0000000..69cddee
--- /dev/null
+++ b/examples/api/utils.h
@@ -0,0 +1,29 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Utility methods.
+ */
+
+#ifndef CVC5__UTILS_H
+#define CVC5__UTILS_H
+
+#include <cvc5/cvc5.h>
+
+/**
+ * Print solutions for synthesis conjecture to the standard output stream.
+ * @param terms the terms for which the synthesis solutions were retrieved
+ * @param sols the synthesis solutions of the given terms
+ */
+void printSynthSolutions(const std::vector<cvc5::api::Term>& terms,
+                         const std::vector<cvc5::api::Term>& sols);
+
+#endif  // CVC5__UTILS_H