From b272d60452028025d56dbf6ffe10276d6f9281cb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Aug 2021 15:45:38 -0500 Subject: [PATCH] Fix single invocation partition for higher-order (#7046) It was not robust to cases where a function-to-synthesize occurred in a higher-order context. Also does general clean up of the single invocation utility. --- src/expr/subs.cpp | 6 ++ src/expr/subs.h | 2 + .../quantifiers/single_inv_partition.cpp | 62 ++++++++++--------- src/theory/quantifiers/single_inv_partition.h | 4 +- test/regress/CMakeLists.txt | 1 + .../regress0/sygus/ho-occ-synth-fun.sy | 9 +++ 6 files changed, 52 insertions(+), 32 deletions(-) create mode 100644 test/regress/regress0/sygus/ho-occ-synth-fun.sy diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index 7e9c83d06..b140a4190 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -173,6 +173,12 @@ std::string Subs::toString() const return ss.str(); } +void Subs::clear() +{ + d_vars.clear(); + d_subs.clear(); +} + std::ostream& operator<<(std::ostream& out, const Subs& s) { out << s.toString(); diff --git a/src/expr/subs.h b/src/expr/subs.h index 56158d36c..afde63b6e 100644 --- a/src/expr/subs.h +++ b/src/expr/subs.h @@ -67,6 +67,8 @@ class Subs std::map toMap() const; /** Get string for this substitution */ std::string toString() const; + /** clear the substitution */ + void clear(); /** The data */ std::vector d_vars; std::vector d_subs; diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 05492b5b7..73bcad535 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -233,42 +233,37 @@ bool SingleInvocationPartition::init(std::vector& funcs, std::map visited; // functions to arguments std::vector args; - std::vector terms; - std::vector subs; + Subs sb; bool singleInvocation = true; bool ngroundSingleInvocation = false; - if (processConjunct(cr, visited, args, terms, subs)) + if (processConjunct(cr, visited, args, sb)) { - for (unsigned j = 0; j < terms.size(); j++) + for (size_t j = 0, vsize = sb.d_vars.size(); j < vsize; j++) { - si_terms.push_back(subs[j]); - Node op = subs[j].hasOperator() ? subs[j].getOperator() : subs[j]; + Node s = sb.d_subs[j]; + si_terms.push_back(s); + Node op = s.hasOperator() ? s.getOperator() : s; Assert(d_func_fo_var.find(op) != d_func_fo_var.end()); si_subs.push_back(d_func_fo_var[op]); } std::map subs_map; std::map subs_map_rev; // normalize the invocations - if (!terms.empty()) + if (!sb.empty()) { - Assert(terms.size() == subs.size()); - cr = cr.substitute( - terms.begin(), terms.end(), subs.begin(), subs.end()); + cr = sb.apply(cr); } std::vector children; children.push_back(cr); - terms.clear(); - subs.clear(); + sb.clear(); Trace("si-prt") << "...single invocation, with arguments: " << std::endl; for (unsigned j = 0; j < args.size(); j++) { Trace("si-prt") << args[j] << " "; - if (args[j].getKind() == BOUND_VARIABLE - && std::find(terms.begin(), terms.end(), args[j]) == terms.end()) + if (args[j].getKind() == BOUND_VARIABLE && !sb.contains(args[j])) { - terms.push_back(args[j]); - subs.push_back(d_si_vars[j]); + sb.add(args[j], d_si_vars[j]); } else { @@ -276,12 +271,8 @@ bool SingleInvocationPartition::init(std::vector& funcs, } } Trace("si-prt") << std::endl; - cr = children.size() == 1 - ? children[0] - : NodeManager::currentNM()->mkNode(OR, children); - Assert(terms.size() == subs.size()); - cr = - cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end()); + cr = nm->mkOr(children); + cr = sb.apply(cr); Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl; // now must check if it has other bound variables @@ -417,8 +408,7 @@ bool SingleInvocationPartition::collectConjuncts(Node n, bool SingleInvocationPartition::processConjunct(Node n, std::map& visited, std::vector& args, - std::vector& terms, - std::vector& subs) + Subs& sb) { std::map::iterator it = visited.find(n); if (it != visited.end()) @@ -430,7 +420,7 @@ bool SingleInvocationPartition::processConjunct(Node n, bool ret = true; for (unsigned i = 0; i < n.getNumChildren(); i++) { - if (!processConjunct(n[i], visited, args, terms, subs)) + if (!processConjunct(n[i], visited, args, sb)) { ret = false; } @@ -445,7 +435,20 @@ bool SingleInvocationPartition::processConjunct(Node n, if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f) != d_input_funcs.end()) { - success = true; + // If n is an application of a function-to-synthesize f, or is + // itself a function-to-synthesize, then n must be fully applied. + // This catches cases where n is a function-to-synthesize that occurs + // in a higher-order context. + // If the type of n is functional, then it is not fully applied. + if (n.getType().isFunction()) + { + ret = false; + success = false; + } + else + { + success = true; + } } } else @@ -458,7 +461,8 @@ bool SingleInvocationPartition::processConjunct(Node n, } if (success) { - if (std::find(terms.begin(), terms.end(), n) == terms.end()) + Trace("si-prt-debug") << "Process " << n << std::endl; + if (!sb.contains(n)) { // check if it matches the type requirement if (isAntiSkolemizableType(f)) @@ -487,8 +491,7 @@ bool SingleInvocationPartition::processConjunct(Node n, } if (ret) { - terms.push_back(n); - subs.push_back(d_func_inv[f]); + sb.add(n, d_func_inv[f]); } } else @@ -500,7 +503,6 @@ bool SingleInvocationPartition::processConjunct(Node n, } } } - //} visited[n] = ret; return ret; } diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 7f8cfc326..1b4ea62b0 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -22,6 +22,7 @@ #include #include "expr/node.h" +#include "expr/subs.h" #include "expr/type_node.h" namespace cvc5 { @@ -284,8 +285,7 @@ class SingleInvocationPartition bool processConjunct(Node n, std::map& visited, std::vector& args, - std::vector& terms, - std::vector& subs); + Subs& sb); /** get the and node corresponding to d_conjuncts[index] */ Node getConjunct(int index); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 483e3a01e..d68400b66 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1243,6 +1243,7 @@ set(regress_0_tests regress0/sygus/dt-sel-parse1.sy regress0/sygus/General_plus10.sy regress0/sygus/hd-05-d1-prog-nogrammar.sy + regress0/sygus/ho-occ-synth-fun.sy regress0/sygus/inv-different-var-order.sy regress0/sygus/issue3356-syg-inf-usort.smt2 regress0/sygus/issue3624.sy diff --git a/test/regress/regress0/sygus/ho-occ-synth-fun.sy b/test/regress/regress0/sygus/ho-occ-synth-fun.sy new file mode 100644 index 000000000..4bef02b69 --- /dev/null +++ b/test/regress/regress0/sygus/ho-occ-synth-fun.sy @@ -0,0 +1,9 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic HO_ALL) +(synth-fun f ((x Int)) Int) +(synth-fun g ((x Int)) Int) +(declare-var P (-> (-> Int Int) Bool)) +(constraint (=> (P f) (P g))) +; a trivial class of solutions is where f = g. +(check-synth) -- 2.30.2