diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-11-20 16:42:58 -0300 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-20 13:42:58 -0600 |
commit | 596fe8c79106dd9b7764df2ddce6b2d3344fea34 (patch) | |
tree | 194dedc76376b7023cbd431289e4724bbbb98e3d /src | |
parent | 45bcf28ab55c0fe471b445820fc21627495beee8 (diff) |
Lazy evaluation via rec-funs of ITE expressions (#3482)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/fun_def_evaluator.cpp | 57 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 3 |
2 files changed, 56 insertions, 4 deletions
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 376d0eb47..1528d5338 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -75,6 +75,13 @@ Node FunDefEvaluator::evaluate(Node n) const Trace("fd-eval-debug") << "constant " << cur << std::endl; visited[cur] = cur; } + else if (cur.getKind() == ITE) + { + Trace("fd-eval-debug") << "ITE " << cur << std::endl; + visited[cur] = Node::null(); + visit.push_back(cur); + visit.push_back(cur[0]); + } else { Trace("fd-eval-debug") << "recurse " << cur << std::endl; @@ -102,6 +109,28 @@ Node FunDefEvaluator::evaluate(Node n) const { children.push_back(cur.getOperator()); } + else if (ck == ITE) + { + // get evaluation of condition + it = visited.find(cur[0]); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + Assert(it->second.isConst()); + // pick child to evaluate depending on condition eval + unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2; + Trace("fd-eval-debug2") + << "FunDefEvaluator: result of ITE condition : " + << it->second.getConst<bool>() << "\n"; + // the result will be the result of evaluation the child + visited[cur] = cur[childIdxToEval]; + // push back self and child. The child will be evaluated first and + // result will be the result of evaluation child + visit.push_back(cur); + visit.push_back(cur[childIdxToEval]); + Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : " + << cur[childIdxToEval] << "\n"; + continue; + } for (const Node& cn : cur) { it = visited.find(cn); @@ -114,6 +143,8 @@ Node FunDefEvaluator::evaluate(Node n) const { // need to evaluate it f = cur.getOperator(); + Trace("fd-eval-debug2") + << "FunDefEvaluator: need to eval " << f << "\n"; itf = d_funDefMap.find(f); if (itf == d_funDefMap.end()) { @@ -123,6 +154,8 @@ Node FunDefEvaluator::evaluate(Node n) const } // get the function definition Node sbody = itf->second.d_body; + Trace("fd-eval-debug2") + << "FunDefEvaluator: definition: " << sbody << "\n"; const std::vector<Node>& args = itf->second.d_args; if (!args.empty()) { @@ -131,6 +164,17 @@ Node FunDefEvaluator::evaluate(Node n) const args.begin(), args.end(), children.begin(), children.end()); // rewrite it sbody = Rewriter::rewrite(sbody); + if (Trace.isOn("fd-eval-debug2")) + { + Trace("fd-eval-debug2") + << "FunDefEvaluator: evaluation with args:\n"; + for (const Node& child : children) + { + Trace("fd-eval-debug2") << "..." << child << "\n"; + } + Trace("fd-eval-debug2") + << "FunDefEvaluator: results in " << sbody << "\n"; + } } // our result is the result of the body visited[cur] = sbody; @@ -164,11 +208,18 @@ Node FunDefEvaluator::evaluate(Node n) const } } } while (!visit.empty()); + Trace("fd-eval") << "FunDefEvaluator: return " << visited[n]; Assert(visited.find(n) != visited.end()); Assert(!visited.find(n)->second.isNull()); - Assert(visited.find(n)->second.isConst()); - Trace("fd-eval") << "FunDefEvaluator: return SUCCESS " << visited[n] - << std::endl; + if (!visited.find(n)->second.isConst()) + { + visited[n] = Node::null(); + Trace("fd-eval") << "\n with NONCONST\n"; + } + else + { + Trace("fd-eval") << "\n with SUCCESS\n"; + } return visited[n]; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6e69715ef..6591e6828 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -591,7 +591,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Trace("cegqi-debug") << "...squery : " << squery << std::endl; squery = Rewriter::rewrite(squery); Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; - Assert(squery.isConst() && squery.getConst<bool>()); + Assert(options::sygusRecFun() + || (squery.isConst() && squery.getConst<bool>())); #endif return false; } |