Fix debugPrint and add regress. (#1934)

diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 0ecf01b742e5481e48bf2832138ded4ad614b4ef..2f3d5b87445963b09b633d03533753d5cc61ff66 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -88,7 +88,7 @@ void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
   d_qe = qe;
 
   // collect the enumerator types and form the strategy
-  collectEnumeratorTypes(d_root, role_equal);
+  buildStrategyGraph(d_root, role_equal);
   // add the enumerators
   enums.insert(enums.end(), d_esym_list.begin(), d_esym_list.end());
   // finish the initialization of the strategy
@@ -127,7 +127,7 @@ EnumTypeInfo& SygusUnifStrategy::getEnumTypeInfo(TypeNode tn)
 }
 // ----------------------------- establishing enumeration types
 
-void SygusUnifStrategy::registerEnumerator(Node et,
+void SygusUnifStrategy::registerStrategyPoint(Node et,
                                            TypeNode tn,
                                            EnumRole enum_role,
                                            bool inSearch)
@@ -162,7 +162,7 @@ void SygusUnifStrategy::registerEnumerator(Node et,
   }
 }
 
-void SygusUnifStrategy::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
+void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
 {
   NodeManager* nm = NodeManager::currentNM();
   if (d_tinfo.find(tn) == d_tinfo.end())
@@ -203,7 +203,7 @@ void SygusUnifStrategy::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
   if (nrole == role_ite_condition)
   {
     Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
-    registerEnumerator(ee, tn, erole, true);
+    registerStrategyPoint(ee, tn, erole, true);
     return;
   }
 
@@ -467,13 +467,9 @@ void SygusUnifStrategy::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
         }
       }
     }
-    if (cop_to_strat.find(cop) == cop_to_strat.end())
-    {
-      Trace("sygus-unif") << "...constructor " << cop
-                          << " does not correspond to a strategy." << std::endl;
-      search_this = true;
-    }
-    else
+    
+    std::map<Node, std::vector<StrategyType> >::iterator itcs = cop_to_strat.find(cop);
+    if (itcs != cop_to_strat.end())
     {
       Trace("sygus-unif") << "-> constructor " << cop
                           << " matches strategy for " << eut.getKind() << "..."
@@ -481,19 +477,27 @@ void SygusUnifStrategy::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
       // collect children types
       for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++)
       {
-        TypeNode tn = sktns[cop_to_carg_list[cop][k]];
+        TypeNode ctn = sktns[cop_to_carg_list[cop][k]];
         Trace("sygus-unif-debug")
             << "   Child type " << k << " : "
-            << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
+            << static_cast<DatatypeType>(ctn.toType()).getDatatype().getName()
             << std::endl;
-        cop_to_child_types[cop].push_back(tn);
+        cop_to_child_types[cop].push_back(ctn);
       }
+      // if there are checks on the consistency of child types wrt strategies,
+      // these should be enforced here. We currently have none.
+    }
+    if (cop_to_strat.find(cop) == cop_to_strat.end())
+    {
+      Trace("sygus-unif") << "...constructor " << cop
+                          << " does not correspond to a strategy." << std::endl;
+      search_this = true;
     }
   }
 
   // check whether we should also enumerate the current type
-  Trace("sygus-unif-debug2") << "  register this enumerator..." << std::endl;
-  registerEnumerator(ee, tn, erole, search_this);
+  Trace("sygus-unif-debug2") << "  register this strategy ..." << std::endl;
+  registerStrategyPoint(ee, tn, erole, search_this);
 
   if (cop_to_strat.empty())
   {
@@ -575,7 +579,7 @@ void SygusUnifStrategy::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
                                              .getDatatype()
                                              .getName()
                                       << std::endl;
-            registerEnumerator(et, ct, erole_c, true);
+            registerStrategyPoint(et, ct, erole_c, true);
             d_einfo[et].d_template = cop_to_child_templ[cop][j];
             d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j];
             Assert(!d_einfo[et].d_template.isNull());
@@ -587,7 +591,7 @@ void SygusUnifStrategy::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
                 << "...child type enumerate "
                 << ((DatatypeType)ct.toType()).getDatatype().getName()
                 << ", node role = " << nrole_c << std::endl;
-            collectEnumeratorTypes(ct, nrole_c);
+            buildStrategyGraph(ct, nrole_c);
             // otherwise use the previous
             Assert(d_tinfo[ct].d_enum.find(erole_c)
                    != d_tinfo[ct].d_enum.end());
@@ -980,7 +984,8 @@ void SygusUnifStrategy::debugPrint(
   if (ei.isTemplated())
   {
     Trace(c) << ", templated : (lambda " << ei.d_template_arg << " "
-             << ei.d_template << ")";
+             << ei.d_template << ")" << std::endl;
+    return;
   }
   Trace(c) << std::endl;
 

diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 43919d68e7424c81652bc18f452a3555012dadeb..0c7f207be3c2909f29be38cb8db7a7987cfa3d64 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -348,12 +348,12 @@ class SygusUnifStrategy
   //-----------------------end debug printing
 
   //------------------------------ strategy registration
-  /** collect enumerator types
+  /** build strategy graph
    *
    * This builds the strategy for enumerated values of type tn for the given
    * role of nrole, for solutions to function-to-synthesize of this class.
    */
-  void collectEnumeratorTypes(TypeNode tn, NodeRole nrole);
+  void buildStrategyGraph(TypeNode tn, NodeRole nrole);
   /** register enumerator
    *
    * This registers that et is an enumerator of type tn, having enumerator
@@ -364,7 +364,7 @@ class SygusUnifStrategy
    * we may use enumerators for which this flag is false to represent strategy
    * nodes that have child strategies.
    */
-  void registerEnumerator(Node et,
+  void registerStrategyPoint(Node et,
                           TypeNode tn,
                           EnumRole enum_role,
                           bool inSearch);

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index f8fdd4a18846ddef9d5f247a5a9695a2f3acf1ee..687ed3c86ab1bb2e3a33453c27210555577d102f 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1486,6 +1486,7 @@ REG1_TESTS = \
        regress1/sygus/hd-sdiv.sy \
        regress1/sygus/icfp_14.12-flip-args.sy \
        regress1/sygus/icfp_14.12.sy \
+       regress1/sygus/icfp_14_12_diff_types.sy \
        regress1/sygus/icfp_28_10.sy \
        regress1/sygus/icfp_easy-ite.sy \
        regress1/sygus/inv-example.sy \

diff --git a/test/regress/regress1/sygus/icfp_14_12_diff_types.sy b/test/regress/regress1/sygus/icfp_14_12_diff_types.sy
new file mode 100644 (file)
index 0000000..f832777
--- /dev/null
+++ b/test/regress/regress1/sygus/icfp_14_12_diff_types.sy
@@ -0,0 +1,34 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic BV)
+
+(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)
+(
+
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+                   (bvand Start Start)
+                   (bvor Start Start)
+                   (bvxor Start Start)
+                   (bvadd Start Start)
+                   (if0 Start Start2 Start2)
+                   (ite StartBool Start Start2)
+ ))
+(Start2 (BitVec 64) (#x0000000000000000 #x0000000000000002))
+(StartBool Bool ((= Start Start)))
+)
+)
+(constraint (= (f #x0000000000000001) #x0000000000000001))
+(constraint (= (f #x1ED2E25068744C80) #x0000000000000000))
+(constraint (= (f #x2D2144F9D8CDCBD6) #x0000000000000000))
+(constraint (= (f #xE5D371D100002E8A) #x0000000000000000))
+(constraint (= (f #xADFF6BA34EBDAD72) #x0000000000000000))
+(constraint (= (f #xDA9299B546AAB59A) #x0000000000000000))
+(constraint (= (f #x0000000000015C8A) #x0000000000000000))
+(constraint (= (f #x0000000000017066) #x0000000000000000))
+(constraint (= (f #x000000000001D9D8) #x0000000000000000))
+(constraint (= (f #x00000000000151AE) #x0000000000000000))
+(constraint (= (f #x0000000000017A14) #x0000000000000000))
+(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000))
+(check-synth)