diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-20 10:35:38 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-20 10:35:43 +0200 |
commit | 6d82ee2d1f84065ff4a86f688a3b671b85728f80 (patch) | |
tree | aad38c08dc4cef60132a1734776c5c9d252e7806 /src/theory | |
parent | d70a63324c95210f1d78c2efc46395d2369d2e2b (diff) |
Fix a few bugs related to sygus.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv_sol.cpp | 6 |
3 files changed, 9 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index a635568fe..cb8e6f200 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -924,7 +924,9 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { if( d_last_inst_si ){ Assert( d_conj->getCegConjectureSingleInv() != NULL ); sol = d_conj->getSingleInvocationSolution( i, tn, status ); - sol = sol.getKind()==LAMBDA ? sol[1] : sol; + if( !sol.isNull() ){ + sol = sol.getKind()==LAMBDA ? sol[1] : sol; + } }else{ Node cprog = d_conj->getCandidate( i ); if( !d_conj->d_cinfo[cprog].d_inst.empty() ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index a8dcd5887..f25d42284 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -888,6 +888,8 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec Node sol; if( reconstructed==1 ){ sol = d_sygus_solution; + }else if( reconstructed==-1 ){ + return Node::null(); }else{ sol = d_solution; } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 9e65be202..1eafe1a93 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -714,8 +714,10 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int } }while( !active.empty() ); - //if solution is null, we ran out of elements, return the original solution - return sol; + // we ran out of elements, return null + reconstructed = -1; + Warning() << CommandFailure("Cannot get synth function: reconstruction to syntax failed."); + return Node::null(); // return sol; } } |