diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-06 12:20:57 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-06 12:20:57 +0200 |
commit | 289f4081c7497efbf33ffbcef5c5e35b89a9bbed (patch) | |
tree | 0f69c01a57aa349d1e932bdbd58ecbe0c1dab958 /src/theory/quantifiers/ce_guided_instantiation.cpp | |
parent | 1a5ac01182d327bf99c7da2dde7bcc09ac0dab15 (diff) |
Improve quantifiers rewriter, minor refactoring.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 17 |
1 files changed, 4 insertions, 13 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 0bc5bb008..44b353ae5 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -598,19 +598,10 @@ void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) { void CegInstantiation::preregisterAssertion( Node n ) { //check if it sygus conjecture - if( n.getKind()==FORALL ){ - if( n.getNumChildren()==3 ){ - for( unsigned i=0; i<n[2].getNumChildren(); i++ ){ - if( n[2][i].getKind()==INST_ATTRIBUTE ){ - Node avar = n[2][i][0]; - if( avar.getAttribute(SygusAttribute()) ){ - //this is a sygus conjecture - Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl; - d_conj->preregisterConjecture( n ); - } - } - } - } + if( TermDb::isSygusConjecture( n ) ){ + //this is a sygus conjecture + Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl; + d_conj->preregisterConjecture( n ); } } |