diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-07 05:00:43 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-07 05:00:43 -0500 |
commit | 6eee137dc64e3f2c467d70edf2bb18abd6b3b071 (patch) | |
tree | 5dc13ffa4de9e58fe2c440b363ca7845c6de0227 | |
parent | 53d881246fba60c630d7b15ad2ea1acf3e0ce335 (diff) |
Change sygus output for failed reconstruction case.
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index cb8e6f200..9ee79af1f 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -1002,7 +1002,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl; } } - if( !(Trace.isOn("cegqi-stats")) ){ + if( !(Trace.isOn("cegqi-stats")) && !sol.isNull() ){ out << "(define-fun " << f << " "; if( dt.getSygusVarList().isNull() ){ out << "() "; @@ -1013,12 +1013,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { if( status==0 ){ out << sol; }else{ - if( sol.isNull() ){ - out << "?"; - }else{ - std::vector< Node > lvs; - TermDbSygus::printSygusTerm( out, sol, lvs ); - } + std::vector< Node > lvs; + TermDbSygus::printSygusTerm( out, sol, lvs ); } out << ")" << std::endl; } |