diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e9e21fb48..6960c4684 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -89,6 +89,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/term_database.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" #include "theory/substitutions.h" @@ -4605,11 +4606,17 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx if( conj.getKind()==kind::FORALL ){ //possibly run quantifier elimination to make formula into single invocation if( conj[1].getKind()==kind::EXISTS ){ - Node conj_se = conj[1][1]; + Node conj_se = Node::fromExpr( expandDefinitions( conj[1][1].toExpr() ) ); Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl; - quantifiers::SingleInvocationPartition sip( kind::APPLY ); - sip.init( conj_se ); + quantifiers::SingleInvocationPartition sip; + std::vector< Node > funcs; + for( unsigned i=0; i<conj[0].getNumChildren(); i++ ){ + Node sf = conj[0][i].getAttribute(theory::SygusSynthFunAttribute()); + Assert( !sf.isNull() ); + funcs.push_back( sf ); + } + sip.init( funcs, conj_se ); Trace("smt-synth") << "...finished, got:" << std::endl; sip.debugPrint("smt-synth"); |