diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 1 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 6 |
2 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index e16e696b5..fa39f28b7 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -293,6 +293,7 @@ void CegConjectureSingleInv::initialize( Node q ) { void CegConjectureSingleInv::finishInit( bool syntaxRestricted, bool hasItes ) { d_has_ites = hasItes; + Trace("cegqi-si-debug") << "Single invocation, finish init, has ITEs = " << d_has_ites << std::endl; // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && d_single_invocation && syntaxRestricted ){ d_single_invocation = false; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 79db09175..88a8f258c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -247,10 +247,8 @@ Node CegGrammarConstructor::process(Node q, } d_qe->getTermDatabaseSygus()->registerSygusType( tn ); // check grammar restrictions - if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ - if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ - d_has_ite = false; - } + if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ + d_has_ite = false; } Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); |