From 6eee137dc64e3f2c467d70edf2bb18abd6b3b071 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 7 Aug 2017 05:00:43 -0500 Subject: [PATCH] Change sygus output for failed reconstruction case. --- src/theory/quantifiers/ce_guided_instantiation.cpp | 10 +++------- 1 file 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; } -- 2.30.2