diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-07 11:37:24 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-07 11:37:32 +0200 |
commit | 1e7207dc661a1aa7d6509cc21d86fb757938efb1 (patch) | |
tree | a1656d3a0c884bb03bc29ad4aff98a8dad1a9608 /src | |
parent | 26b9453941c0c90b887839246882be3629439ccf (diff) |
Minor fixes for cegqi.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 2 |
2 files changed, 18 insertions, 13 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 7d1c06b8e..b3c1e1eaa 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -218,16 +218,21 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } //[3] directly look at assertions - TheoryId tid = Theory::theoryOf( pv ); - Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); - if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { - context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned j = 0; it != it_end; ++ it, ++j) { - Node lit = (*it).assertion; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - bool pol = lit.getKind()!=NOT; - if( tid==THEORY_ARITH ){ - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ + unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; + for( unsigned r=0; r<rmax; r++ ){ + TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() ); + Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); + Trace("cegqi-si-inst-debug2") << "Theory of " << pv << " (r=" << r << ") is " << tid << std::endl; + if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { + Trace("cegqi-si-inst-debug2") << "Look at assertions of " << tid << std::endl; + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned j = 0; it != it_end; ++ it, ++j) { + Node lit = (*it).assertion; + Trace("cegqi-si-inst-debug2") << " look at " << lit << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + //arithmetic inequalities and disequalities + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && ( atom[0].getType().isInteger() || atom[0].getType().isReal() ) ) ){ Assert( atom.getKind()!=GEQ || atom[1].isConst() ); Node atom_lhs; Node atom_rhs; @@ -1165,9 +1170,9 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) { Assert( d_cinst!=NULL ); d_curr_lemmas.clear(); //check if there are delta lemmas - d_cinst->getDeltaLemmas( d_curr_lemmas ); + d_cinst->getDeltaLemmas( lems ); //if not, do ce-guided instantiation - if( d_curr_lemmas.empty() ){ + if( lems.empty() ){ //call check for instantiator d_cinst->check(); //add lemmas diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index cb01fd373..ea3e18be1 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -328,7 +328,7 @@ bool InstantiationEngine::hasNonArithmeticVariable( Node f ){ } bool InstantiationEngine::doCbqi( Node f ){ - if( options::cbqi.wasSetByUser() ){ + if( options::cbqi.wasSetByUser() || options::cbqi2.wasSetByUser() ){ return options::cbqi(); }else if( options::cbqi() ){ //if quantifier has a non-arithmetic variable, then do not use cbqi |