diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-06 09:35:49 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-06 09:35:59 +0100 |
commit | 363e4c378f0bc9598a93c80bce9ecaebca2efdd1 (patch) | |
tree | e40a637326719738866bfbb790aa704a3522a2c1 /src/theory/quantifiers/ce_guided_instantiation.cpp | |
parent | fca6fd532abda44c4da48d5c167b77600690e221 (diff) |
Handle missing cases for single inv solution reconstruction. Minor fixes. Refactor.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 3475e9e97..e291dce9d 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -60,7 +60,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } d_syntax_guided = true; if( options::cegqiSingleInv() ){ - d_ceg_si = new CegConjectureSingleInv( q, this ); + d_ceg_si = new CegConjectureSingleInv( qe, q, this ); d_ceg_si->initialize(); } }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){ @@ -255,7 +255,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( getTermDatabase()->isQAttrSygus( q ) ){ if( conj->d_ceg_si ){ std::vector< Node > lems; - conj->d_ceg_si->check( d_quantEngine, lems ); + conj->d_ceg_si->check( lems ); if( !lems.empty() ){ d_last_inst_si = true; for( unsigned j=0; j<lems.size(); j++ ){ @@ -494,7 +494,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { int status; if( d_last_inst_si ){ Assert( d_conj->d_ceg_si ); - sol = d_conj->d_ceg_si->getSolution( d_quantEngine, i, tn, status ); + sol = d_conj->d_ceg_si->getSolution( i, tn, status ); }else{ if( !d_conj->d_candidate_inst[i].empty() ){ sol = d_conj->d_candidate_inst[i].back(); |