From 5ded4ab6a5c4bb19ac8b58227e9e3b476518d4c8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 May 2018 16:03:39 -0500 Subject: [PATCH] Fix debugPrint and add regress. (#1934) --- .../quantifiers/sygus/sygus_unif_strat.cpp | 43 +++++++++++-------- .../quantifiers/sygus/sygus_unif_strat.h | 6 +-- test/regress/Makefile.tests | 1 + .../regress1/sygus/icfp_14_12_diff_types.sy | 34 +++++++++++++++ 4 files changed, 62 insertions(+), 22 deletions(-) create mode 100644 test/regress/regress1/sygus/icfp_14_12_diff_types.sy diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 0ecf01b74..2f3d5b874 100644 --- 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 >::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(tn.toType()).getDatatype().getName() + << static_cast(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 43919d68e..0c7f207be 100644 --- 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 f8fdd4a18..687ed3c86 100644 --- 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 index 000000000..f83277757 --- /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) -- 2.30.2