diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2018-06-05 13:45:41 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2018-06-05 13:45:41 -0500 |
commit | 3fbbf1498bc6ce2867c543c41c90b60df6c7c1ed (patch) | |
tree | 04a04992a18f1fdad57986569efb7a1a50cf8a07 | |
parent | 2f808f53237540b7459036aa6e2e30970cd63bdf (diff) |
Disable special case for all-abort Booleans.
-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(); |