From 6fe7877d82721e453d5d928a8fe9dbad2099dac1 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 18 Nov 2019 13:52:18 -0600
Subject: Use standard sygus interface for abduction and rewrite rule synthesis
 (#3471)

---
 src/theory/quantifiers/sygus/sygus_abduct.cpp | 29 ++++++++++++++++-----------
 1 file changed, 17 insertions(+), 12 deletions(-)

(limited to 'src/theory')

diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 529ef037f..0396aba86 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/datatype.h"
 #include "expr/node_algorithm.h"
+#include "expr/sygus_datatype.h"
 #include "printer/sygus_print_callback.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
@@ -86,7 +87,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   {
     Assert(abdGType.isDatatype() && abdGType.getDatatype().isSygus());
     // must convert all constructors to version with bound variables in "vars"
-    std::vector<Datatype> datatypes;
+    std::vector<SygusDatatype> sdts;
     std::set<Type> unres;
 
     Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl;
@@ -129,9 +130,9 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
         const Datatype& dtc = curr.getDatatype();
         std::stringstream ssdtn;
         ssdtn << dtc.getName() << "_s";
-        datatypes.push_back(Datatype(ssdtn.str()));
+        sdts.push_back(SygusDatatype(ssdtn.str()));
         Trace("sygus-abduct-debug")
-            << "Process datatype " << datatypes.back().getName() << "..."
+            << "Process datatype " << sdts.back().getName() << "..."
             << std::endl;
         for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
         {
@@ -141,7 +142,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
               syms.begin(), syms.end(), varlist.begin(), varlist.end());
           Trace("sygus-abduct-debug") << "  Process constructor " << op << " / "
                                       << ops << "..." << std::endl;
-          std::vector<Type> cargs;
+          std::vector<TypeNode> cargs;
           for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
           {
             TypeNode argt = TypeNode::fromType(dtc[j].getArgType(k));
@@ -167,7 +168,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
             }
             Trace("sygus-abduct-debug")
                 << "    Arg #" << k << ": " << argtNew << std::endl;
-            cargs.push_back(argtNew.toType());
+            cargs.push_back(argtNew);
           }
           // callback prints as the expression
           std::shared_ptr<SygusPrintCallback> spc;
@@ -191,22 +192,26 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
           ss << ops.getKind();
           Trace("sygus-abduct-debug")
               << "Add constructor : " << ops << std::endl;
-          datatypes.back().addSygusConstructor(
-              ops.toExpr(), ss.str(), cargs, spc);
+          sdts.back().addConstructor(ops, ss.str(), cargs, spc);
         }
         Trace("sygus-abduct-debug")
             << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
-        datatypes.back().setSygus(dtc.getSygusType(),
-                                  abvl.toExpr(),
-                                  dtc.getSygusAllowConst(),
-                                  dtc.getSygusAllowAll());
+        TypeNode stn = TypeNode::fromType(dtc.getSygusType());
+        sdts.back().initializeDatatype(
+            stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll());
       }
       dtToProcess.clear();
       dtToProcess.insert(
           dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end());
     }
     Trace("sygus-abduct-debug")
-        << "Make " << datatypes.size() << " datatype types..." << std::endl;
+        << "Make " << sdts.size() << " datatype types..." << std::endl;
+    // extract the datatypes
+    std::vector<Datatype> datatypes;
+    for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
+    {
+      datatypes.push_back(sdts[i].getDatatype());
+    }
     // make the datatype types
     std::vector<DatatypeType> datatypeTypes =
         nm->toExprManager()->mkMutualDatatypeTypes(
-- 
cgit v1.2.3