diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-10 08:45:39 -0600 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-11-10 11:45:39 -0300 |
commit | 7f7c4e5f7bfb5c38611afa3a016f4f767d5b86fd (patch) | |
tree | b3d4c7afeb18305d662fe07907f88126b3890e4d /src | |
parent | 1bceb5036a208746bfba1ec42d65862d0d231a83 (diff) |
Fix bugs related to sygus higher-order + recursive functions (#3448)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/fun_def_evaluator.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 33 |
2 files changed, 31 insertions, 12 deletions
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 83debe0d9..376d0eb47 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -150,17 +150,10 @@ Node FunDefEvaluator::evaluate(Node n) const ret = nm->mkNode(cur.getKind(), children); ret = Rewriter::rewrite(ret); } - if (!ret.isConst()) - { - Trace("fd-eval") << "FunDefEvaluator: non-constant subterm " << ret - << ", FAIL" << std::endl; - // failed, possibly due to free variable - return Node::null(); - } visited[cur] = ret; } } - else if (!curEval.isConst()) + else if (cur != curEval && !curEval.isConst()) { Trace("fd-eval-debug") << "from body " << cur << std::endl; // we had to evaluate our body, which should have a definition now @@ -168,7 +161,6 @@ Node FunDefEvaluator::evaluate(Node n) const Assert(it != visited.end()); // our definition is the result of the body visited[cur] = it->second; - Assert(it->second.isConst()); } } } while (!visit.empty()); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 8f935de27..b8bf6c865 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -287,6 +287,7 @@ Node CegGrammarConstructor::convertToEmbedding(Node n) std::stack<TNode> visit; TNode cur; visit.push(n); + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); do { cur = visit.top(); visit.pop(); @@ -337,12 +338,38 @@ Node CegGrammarConstructor::convertToEmbedding(Node n) } if (makeEvalFun) { - // will make into an application of an evaluation function - ret = nm->mkNode(DT_SYGUS_EVAL, children); + if (!cur.getType().isFunction()) + { + // will make into an application of an evaluation function + ret = nm->mkNode(DT_SYGUS_EVAL, children); + } + else + { + Assert(children.size() == 1); + Node ef = children[0]; + // Otherwise, we are using the function-to-synthesize itself in a + // higher-order setting. We must return the lambda term: + // lambda x1...xn. (DT_SYGUS_EVAL ef x1 ... xn) + // where ef is the first order variable for the + // function-to-synthesize. + SygusTypeInfo& ti = tds->getTypeInfo(ef.getType()); + const std::vector<Node>& vars = ti.getVarList(); + Assert(!vars.empty()); + std::vector<Node> vs; + for (const Node& v : vars) + { + vs.push_back(nm->mkBoundVar(v.getType())); + } + Node lvl = nm->mkNode(BOUND_VAR_LIST, vs); + std::vector<Node> eargs; + eargs.push_back(ef); + eargs.insert(eargs.end(), vs.begin(), vs.end()); + ret = nm->mkNode(LAMBDA, lvl, nm->mkNode(DT_SYGUS_EVAL, eargs)); + } } else if (childChanged) { - ret = NodeManager::currentNM()->mkNode(ret_k, children); + ret = nm->mkNode(ret_k, children); } visited[cur] = ret; } |