From: ajreynol Date: Tue, 7 Apr 2015 09:37:24 +0000 (+0200) Subject: Minor fixes for cegqi. X-Git-Tag: cvc5-1.0.0~6365 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e7207dc661a1aa7d6509cc21d86fb757938efb1;p=cvc5.git Minor fixes for cegqi. --- 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::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; rgetTheoryEngine()->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::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