diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 1596c30f0..e69d746fe 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1178,8 +1178,10 @@ bool SynthConjecture::getSynthSolutions( NodeManager* nm = NodeManager::currentNM(); std::vector<Node> sols; std::vector<int> statuses; + Trace("cegqi-debug") << "getSynthSolutions..." << std::endl; if (!getSynthSolutionsInternal(sols, statuses)) { + Trace("cegqi-debug") << "...failed internal" << std::endl; return false; } // we add it to the solution map, indexed by this conjecture @@ -1188,12 +1190,16 @@ bool SynthConjecture::getSynthSolutions( { Node sol = sols[i]; int status = statuses[i]; + Trace("cegqi-debug") << "...got " << i << ": " << sol + << ", status=" << status << std::endl; // get the builtin solution Node bsol = sol; if (status != 0) { - // convert sygus to builtin here - bsol = d_tds->sygusToBuiltin(sol, sol.getType()); + // Convert sygus to builtin here. + // We must use the external representation to ensure bsol matches the + // grammar. + bsol = datatypes::utils::sygusToBuiltin(sol, true); } // convert to lambda TypeNode tn = d_embed_quant[0][i].getType(); @@ -1214,6 +1220,7 @@ bool SynthConjecture::getSynthSolutions( } // store in map smc[fvar] = bsol; + Trace("cegqi-debug") << "...return " << bsol << std::endl; } return true; } |