summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options8
-rw-r--r--src/smt/smt_engine.cpp10
-rw-r--r--src/theory/quantifiers/ceg_instantiator.cpp200
-rw-r--r--src/theory/quantifiers/ceg_instantiator.h64
-rw-r--r--src/theory/quantifiers/inst_match_generator.cpp47
-rw-r--r--src/theory/quantifiers/inst_match_generator.h8
-rw-r--r--src/theory/quantifiers/term_database.cpp11
-rw-r--r--src/theory/quantifiers/trigger.cpp10
-rw-r--r--src/theory/quantifiers/trigger.h2
-rw-r--r--src/theory/quantifiers_engine.cpp5
10 files changed, 123 insertions, 242 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 04b918afc..9e704691a 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -47,7 +47,7 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal
option preSkolemQuant --pre-skolem-quant bool :read-write :default false
apply skolemization eagerly to bodies of quantified formulas
option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true
- apply skolemization to nested quantified formulass
+ apply skolemization to nested quantified formulas
option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
apply skolemization to quantified formulas aggressively
option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
@@ -118,10 +118,6 @@ option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMo
option instRelevantCond --inst-rlv-cond bool :default false
add relevancy conditions for instantiations
-
-option eagerInstQuant --eager-inst-quant bool :default false
- apply quantifier instantiation eagerly
-
option fullSaturateQuant --full-saturate-quant bool :default false :read-write
when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
@@ -293,8 +289,6 @@ option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false
preregister ground instantiations in counterexample-based quantifier instantiation
option cbqiMinBounds --cbqi-min-bounds bool :default false
use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
-option cbqiSymLia --cbqi-sym-lia bool :default false
- use symbolic integer division in substitutions for counterexample-based quantifier instantiation
option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false
round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
option cbqiMidpoint --cbqi-midpoint bool :default false
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b7997a204..19bc85e3e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1748,6 +1748,12 @@ void SmtEngine::setDefaults() {
options::finiteModelFind.set( true );
}
}
+ //EPR
+ if( options::quantEpr() ){
+ if( !options::preSkolemQuant.wasSetByUser() ){
+ options::preSkolemQuant.set( true );
+ }
+ }
//now, have determined whether finite model find is on/off
//apply finite model finding options
@@ -1840,9 +1846,7 @@ void SmtEngine::setDefaults() {
}
if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){
//only instantiation should happen at last call when model is avaiable
- if( !options::instWhenMode.wasSetByUser() ){
- options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
- }
+ options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
}
}
}
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index d31851ec4..6eb91cbdf 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -69,22 +69,20 @@ void CegInstantiator::computeProgVars( Node n ){
}
}
-bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
- std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+bool CegInstantiator::isEligible( Node n ) {
+ //compute d_subs_fv, which program variables are contained in n, and determines if eligible
+ computeProgVars( n );
+ return d_inelig.find( n )==d_inelig.end();
+}
+
+bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i, unsigned effort,
std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
if( i==d_vars.size() ){
//solved for all variables, now construct instantiation
if( !sf.d_has_coeff.empty() ){
- if( options::cbqiSymLia() ){
- //use symbolic solved forms
- SolvedForm csf;
- csf.copy( ssf );
- return doAddInstantiationCoeff( csf, vars, btyp, 0, cons );
- }else{
- return doAddInstantiationCoeff( sf, vars, btyp, 0, cons );
- }
+ return doAddInstantiationCoeff( sf, 0, cons );
}else{
- return doAddInstantiation( sf.d_subs, vars, cons );
+ return doAddInstantiation( sf.d_subs, sf.d_vars, cons );
}
}else{
std::map< Node, std::map< Node, bool > > subs_proc;
@@ -122,19 +120,17 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
Node n = it_eqc->second[k];
if( n!=pv ){
Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl;
- //compute d_subs_fv, which program variables are contained in n
- computeProgVars( n );
//must be an eligible term
- if( d_inelig.find( n )==d_inelig.end() ){
+ if( isEligible( n ) ){
Node ns;
Node pv_coeff; //coefficient of pv in the equality we solve (null is 1)
bool proc = false;
if( !d_prog_var[n].empty() ){
- ns = applySubstitution( pvtn, n, sf, vars, pv_coeff, false );
+ ns = applySubstitution( pvtn, n, sf, pv_coeff, false );
if( !ns.isNull() ){
computeProgVars( ns );
//substituted version must be new and cannot contain pv
- proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end();
+ proc = d_prog_var[ns].find( pv )==d_prog_var[ns].end();
}
}else{
ns = n;
@@ -142,8 +138,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
}
if( proc ){
//try the substitution
- subs_proc[ns][pv_coeff] = true;
- if( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( tryDoAddInstantiationInc( ns, pv, pv_coeff, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
return true;
}
}
@@ -167,7 +162,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
}
- if( doAddInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiation( sf, theta, i, effort, cons, curr_var ) ){
return true;
}else{
//cleanup
@@ -201,14 +196,12 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
Node n = it_reqc->second[kk];
Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
- //compute the variables in n
- computeProgVars( n );
//must be an eligible term
- if( d_inelig.find( n )==d_inelig.end() ){
+ if( isEligible( n ) ){
Node ns;
Node pv_coeff;
if( !d_prog_var[n].empty() ){
- ns = applySubstitution( pvtn, n, sf, vars, pv_coeff );
+ ns = applySubstitution( pvtn, n, sf, pv_coeff );
if( !ns.isNull() ){
computeProgVars( ns );
}
@@ -274,7 +267,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
Node val = veq[1];
if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
subs_proc[val][veq_c] = true;
- if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( val, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var ) ){
return true;
}
}
@@ -288,11 +281,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
}
}
if( success ){
- if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
- subs_proc[val][veq_c] = true;
- if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
- return true;
- }
+ if( tryDoAddInstantiationInc( val, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+ return true;
}
}
}
@@ -343,14 +333,12 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
atom_lhs = Rewriter::rewrite( atom_lhs );
atom_rhs = d_zero;
}
-
- computeProgVars( atom_lhs );
//must be an eligible term
- if( d_inelig.find( atom_lhs )==d_inelig.end() ){
+ if( isEligible( atom_lhs ) ){
//apply substitution to LHS of atom
if( !d_prog_var[atom_lhs].empty() ){
Node atom_lhs_coeff;
- atom_lhs = applySubstitution( pvtn, atom_lhs, sf, vars, atom_lhs_coeff );
+ atom_lhs = applySubstitution( pvtn, atom_lhs, sf, atom_lhs_coeff );
if( !atom_lhs.isNull() ){
computeProgVars( atom_lhs );
if( !atom_lhs_coeff.isNull() ){
@@ -460,11 +448,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
mbp_lit[index].push_back( lit );
}else{
//try this bound
- if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
- subs_proc[uval][veq_c] = true;
- if( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
- return true;
- }
+ if( tryDoAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+ return true;
}
}
}
@@ -492,7 +477,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
}
if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
subs_proc[uval][veq_c] = true;
- if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var ) ){
return true;
}
}
@@ -529,7 +514,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
val = NodeManager::currentNM()->mkNode( UMINUS, val );
val = Rewriter::rewrite( val );
}
- if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( tryDoAddInstantiationInc( val, pv, Node::null(), 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
return true;
}
}
@@ -623,11 +608,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] );
if( !val.isNull() ){
- if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
- subs_proc[val][mbp_coeff[rr][best]] = true;
- if( doAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
- return true;
- }
+ if( tryDoAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+ return true;
}
}
}
@@ -640,11 +622,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
Node c; //null (one) coefficient
val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() );
if( !val.isNull() ){
- if( subs_proc[val].find( c )==subs_proc[val].end() ){
- subs_proc[val][c] = true;
- if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
- return true;
- }
+ if( tryDoAddInstantiationInc( val, pv, c, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+ return true;
}
}
}
@@ -684,11 +663,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
}
Trace("cbqi-bound") << "Midpoint value : " << val << std::endl;
if( !val.isNull() ){
- if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){
- subs_proc[val][Node::null()] = true;
- if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
- return true;
- }
+ if( tryDoAddInstantiationInc( val, pv, Node::null(), 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+ return true;
}
}
}
@@ -705,11 +681,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
mbp_vts_coeff[rr][0][j], mbp_vts_coeff[rr][1][j] );
if( !val.isNull() ){
- if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
- subs_proc[val][mbp_coeff[rr][j]] = true;
- if( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
- return true;
- }
+ if( tryDoAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+ return true;
}
}
}
@@ -738,7 +711,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
//we only resort to values in the case of booleans
Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
#endif
- if( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
+ if( tryDoAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, theta, i, new_effort, cons, curr_var, subs_proc ) ){
return true;
}
}
@@ -747,9 +720,19 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
}
}
+//cached version
+bool CegInstantiator::tryDoAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort,
+ std::map< Node, Node >& cons, std::vector< Node >& curr_var,
+ std::map< Node, std::map< Node, bool > >& subs_proc ) {
+ if( subs_proc[n].find( pv_coeff )==subs_proc[n].end() ){
+ subs_proc[n][pv_coeff] = true;
+ return doAddInstantiationInc( n, pv, pv_coeff, bt, sf, theta, i, effort, cons, curr_var );
+ }else{
+ return false;
+ }
+}
-bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
- std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort,
std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
if( Trace.isOn("cbqi-inst") ){
for( unsigned j=0; j<sf.d_subs.size(); j++ ){
@@ -791,16 +774,16 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
TNode tv = pv;
TNode ts = n;
Node a_pv_coeff;
- Node new_subs = applySubstitution( vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
+ Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
if( !new_subs.isNull() ){
sf.d_subs[j] = new_subs;
if( !a_pv_coeff.isNull() ){
prev_coeff[j] = sf.d_coeff[j];
if( sf.d_coeff[j].isNull() ){
- Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), vars[j] )==sf.d_has_coeff.end() );
+ Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), sf.d_vars[j] )==sf.d_has_coeff.end() );
//now has coefficient
- new_has_coeff.push_back( vars[j] );
- sf.d_has_coeff.push_back( vars[j] );
+ new_has_coeff.push_back( sf.d_vars[j] );
+ sf.d_has_coeff.push_back( sf.d_vars[j] );
sf.d_coeff[j] = a_pv_coeff;
}else{
sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) );
@@ -819,19 +802,10 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
}else{
Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
}
- if( options::cbqiSymLia() && pv_coeff.isNull() ){
- //apply simple substitutions also to sym_subs
- prev_sym_subs[j] = ssf.d_subs[j];
- ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() );
- ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] );
- }
}
if( success ){
Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
- vars.push_back( pv );
- btyp.push_back( bt );
- sf.push_back( pv, n, pv_coeff );
- ssf.push_back( pv, n, pv_coeff );
+ sf.push_back( pv, n, pv_coeff, bt );
Node new_theta = theta;
if( !pv_coeff.isNull() ){
if( new_theta.isNull() ){
@@ -848,16 +822,13 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
is_cv = true;
}
Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
- success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
+ success = doAddInstantiation( sf, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
if( !success ){
Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
if( is_cv ){
curr_var.push_back( pv );
}
- sf.pop_back( pv, n, pv_coeff );
- ssf.pop_back( pv, n, pv_coeff );
- vars.pop_back();
- btyp.pop_back();
+ sf.pop_back( pv, n, pv_coeff, bt );
}
}
if( success ){
@@ -874,29 +845,23 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
for( unsigned i=0; i<new_has_coeff.size(); i++ ){
sf.d_has_coeff.pop_back();
}
- for( std::map< int, Node >::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){
- ssf.d_subs[it->first] = it->second;
- }
return false;
}
}
-bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
- unsigned j, std::map< Node, Node >& cons ) {
-
-
+bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, unsigned j, std::map< Node, Node >& cons ) {
if( j==sf.d_has_coeff.size() ){
- return doAddInstantiation( sf.d_subs, vars, cons );
+ return doAddInstantiation( sf.d_subs, sf.d_vars, cons );
}else{
- Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() );
- unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin();
+ Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), sf.d_has_coeff[j] )!=sf.d_vars.end() );
+ unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), sf.d_has_coeff[j] )-sf.d_vars.begin();
Node prev = sf.d_subs[index];
Assert( !sf.d_coeff[index].isNull() );
- Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl;
- Assert( vars[index].getType().isInteger() );
+ Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl;
+ Assert( sf.d_vars[index].getType().isInteger() );
//must ensure that divisibility constraints are met
//solve updated rewritten equality for vars[index], if coefficient is one, then we are successful
- Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] );
+ Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], sf.d_vars[index] );
Node eq_rhs = sf.d_subs[index];
Node eq = eq_lhs.eqNode( eq_rhs );
eq = Rewriter::rewrite( eq );
@@ -904,20 +869,20 @@ bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node
std::map< Node, Node > msum;
if( QuantArith::getMonomialSumLit( eq, msum ) ){
Node veq;
- if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){
+ if( QuantArith::isolate( sf.d_vars[index], msum, veq, EQUAL, true )!=0 ){
Node veq_c;
- if( veq[0]!=vars[index] ){
+ if( veq[0]!=sf.d_vars[index] ){
Node veq_v;
if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
- Assert( veq_v==vars[index] );
+ Assert( veq_v==sf.d_vars[index] );
}
}
sf.d_subs[index] = veq[1];
if( !veq_c.isNull() ){
sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
- Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
+ Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl;
//intger division rounding up if from a lower bound
- if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
+ if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
NodeManager::currentNM()->mkNode( ITE,
NodeManager::currentNM()->mkNode( EQUAL,
@@ -927,24 +892,8 @@ bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node
);
}
}
- Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl;
- if( options::cbqiSymLia() ){
- //must apply substitution to previous subs
- std::vector< Node > curr_var;
- std::vector< Node > curr_subs;
- curr_var.push_back( vars[index] );
- curr_subs.push_back( sf.d_subs[index] );
- for( unsigned k=0; k<index; k++ ){
- Node prevs = sf.d_subs[k];
- sf.d_subs[k] = sf.d_subs[k].substitute( curr_var.begin(), curr_var.end(), curr_subs.begin(), curr_subs.end() );
- if( prevs!=sf.d_subs[k] ){
- Trace("cbqi-inst-debug2") << " rewrite " << vars[k] << " -> " << prevs << " to ";
- sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] );
- Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl;
- }
- }
- }
- if( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
+ Trace("cbqi-inst-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl;
+ if( doAddInstantiationCoeff( sf, j+1, cons ) ){
return true;
}
}
@@ -1176,14 +1125,11 @@ bool CegInstantiator::check() {
processAssertions();
for( unsigned r=0; r<2; r++ ){
SolvedForm sf;
- SolvedForm ssf;
- std::vector< Node > vars;
- std::vector< int > btyp;
Node theta;
std::map< Node, Node > cons;
std::vector< Node > curr_var;
//try to add an instantiation
- if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
+ if( doAddInstantiation( sf, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
return true;
}
}
@@ -1236,16 +1182,16 @@ void CegInstantiator::presolve( Node q ) {
//at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
//only if no nested quantifiers
if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){
- std::vector< Node > vars;
+ std::vector< Node > ps_vars;
std::map< Node, std::vector< Node > > teq;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- vars.push_back( q[0][i] );
+ ps_vars.push_back( q[0][i] );
teq[q[0][i]].clear();
}
collectPresolveEqTerms( q[1], teq );
std::vector< Node > terms;
std::vector< Node > conj;
- getPresolveEqConjuncts( vars, terms, teq, q, conj );
+ getPresolveEqConjuncts( ps_vars, terms, teq, q, conj );
if( !conj.empty() ){
Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
@@ -1410,10 +1356,8 @@ void CegInstantiator::processAssertions() {
std::vector< Node > akeep;
for( unsigned i=0; i<it->second.size(); i++ ){
Node n = it->second[i];
- //compute the variables in assertion
- computeProgVars( n );
//must be an eligible term
- if( d_inelig.find( n )==d_inelig.end() ){
+ if( isEligible( n ) ){
//must contain at least one variable
if( !d_prog_var[n].empty() ){
Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 3d7bbcb55..5b8942027 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -38,6 +38,8 @@ public:
virtual bool addLemma( Node lem ) = 0;
};
+class Instantiator;
+
class CegInstantiator {
private:
QuantifiersEngine * d_qe;
@@ -72,55 +74,53 @@ private:
void collectCeAtoms( Node n, std::map< Node, bool >& visited );
//for adding instantiations during check
void computeProgVars( Node n );
+ // is eligible
+ bool isEligible( Node n );
//solved form, involves substitution with coefficients
class SolvedForm {
public:
+ std::vector< Node > d_vars;
std::vector< Node > d_subs;
std::vector< Node > d_coeff;
+ std::vector< int > d_btyp;
std::vector< Node > d_has_coeff;
void copy( SolvedForm& sf ){
d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() );
d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() );
d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() );
}
- void push_back( Node pv, Node n, Node pv_coeff ){
+ void push_back( Node pv, Node n, Node pv_coeff, int bt ){
+ d_vars.push_back( pv );
d_subs.push_back( n );
d_coeff.push_back( pv_coeff );
+ d_btyp.push_back( bt );
if( !pv_coeff.isNull() ){
d_has_coeff.push_back( pv );
}
}
- void pop_back( Node pv, Node n, Node pv_coeff ){
+ void pop_back( Node pv, Node n, Node pv_coeff, int bt ){
+ d_vars.pop_back();
d_subs.pop_back();
d_coeff.pop_back();
+ d_btyp.pop_back();
if( !pv_coeff.isNull() ){
d_has_coeff.pop_back();
}
}
};
- /*
- class MbpBound {
- public:
- Node d_bound;
- Node d_coeff;
- Node d_vts_coeff[2];
- Node d_lit;
- };
- */
// effort=0 : do not use model value, 1: use model value, 2: one must use model value
- bool doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
- std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
- std::map< Node, Node >& cons, std::vector< Node >& curr_var );
- bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
- std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
- std::map< Node, Node >& cons, std::vector< Node >& curr_var );
- bool doAddInstantiationCoeff( SolvedForm& sf,
- std::vector< Node >& vars, std::vector< int >& btyp,
- unsigned j, std::map< Node, Node >& cons );
+ bool doAddInstantiation( SolvedForm& sf, Node theta, unsigned i, unsigned effort,
+ std::map< Node, Node >& cons, std::vector< Node >& curr_var );
+ bool tryDoAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort,
+ std::map< Node, Node >& cons, std::vector< Node >& curr_var,
+ std::map< Node, std::map< Node, bool > >& subs_proc );
+ bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort,
+ std::map< Node, Node >& cons, std::vector< Node >& curr_var );
+ bool doAddInstantiationCoeff( SolvedForm& sf, unsigned j, std::map< Node, Node >& cons );
bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons );
- Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
- return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
+ Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) {
+ return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff );
}
Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true );
@@ -142,6 +142,26 @@ public:
void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars );
};
+
+/*
+// an instantiator for individual variables
+class InstantiatorVar {
+public:
+
+ void postProcessInstantiation( SolvedForm& sf );
+};
+*/
+
+/*
+class MbpBound {
+public:
+ Node d_bound;
+ Node d_coeff;
+ Node d_vts_coeff[2];
+ Node d_lit;
+};
+*/
+
}
}
}
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index b3df9ca5d..ceae3e4c8 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -388,23 +388,6 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
return addedLemmas;
}
-int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
- Assert( options::eagerInstQuant() );
- if( !d_match_pattern.isNull() ){
- InstMatch m( f );
- if( getMatch( f, t, m, qe ) ){
- if( qe->addInstantiation( f, m ) ){
- return 1;
- }
- }
- }else{
- for( unsigned i=0; i<d_children.size(); i++ ){
- d_children[i]->addTerm( f, t, qe );
- }
- }
- return 0;
-}
-
InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) {
std::vector< Node > pats;
@@ -716,22 +699,6 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
}
}
-int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){
- Assert( options::eagerInstQuant() );
- int addedLemmas = 0;
- for( int i=0; i<(int)d_children.size(); i++ ){
- Node t_op = qe->getTermDatabase()->getMatchOperator( t );
- if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){
- InstMatch m( q );
- //if it produces a match, then process it with the rest
- if( ((InstMatchGenerator*)d_children[i])->getMatch( q, t, m, qe ) ){
- processNewMatch( qe, m, i, addedLemmas );
- }
- }
- }
- return addedLemmas;
-}
-
InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) {
if( d_match_pattern.getKind()==NOT ){
d_match_pattern = d_match_pattern[0];
@@ -841,20 +808,6 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
}
}
-int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){
- //for eager instantiation only
- Assert( options::eagerInstQuant() );
- InstMatch m( q );
- for( unsigned i=0; i<t.getNumChildren(); i++ ){
- if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- m.setValue(d_var_num[i], t[i]);
- }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
- return 0;
- }
- }
- return qe->addInstantiation( q, m ) ? 1 : 0;
-}
-
int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 65c5a1427..c238e3c4e 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -42,8 +42,6 @@ public:
virtual bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0;
/** add instantiations directly */
virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
- /** add ground term t, called when t is added to term db */
- virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; }
/** set active add */
virtual void setActiveAdd( bool val ) {}
/** get active score */
@@ -113,8 +111,6 @@ public:
bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
/** add instantiations */
int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t */
- int addTerm( Node q, Node t, QuantifiersEngine* qe );
bool d_active_add;
void setActiveAdd( bool val );
@@ -205,8 +201,6 @@ public:
bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
/** add instantiations */
int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t */
- int addTerm( Node q, Node t, QuantifiersEngine* qe );
};/* class InstMatchGeneratorMulti */
/** smart (single)-trigger implementation */
@@ -240,8 +234,6 @@ public:
bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
/** add instantiations */
int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t, possibly add instantiations */
- int addTerm( Node q, Node t, QuantifiersEngine* qe );
/** get active score */
int getActiveScore( QuantifiersEngine * qe );
};/* class InstMatchGeneratorSimple */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a34ad116a..dee4952bd 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -175,17 +175,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
if( d_sygus_tdb ){
d_sygus_tdb->registerEvalTerm( n );
}
-
- if( options::eagerInstQuant() ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
- int addedLemmas = 0;
- for( unsigned i=0; i<d_op_triggers[op].size(); i++ ){
- addedLemmas += d_op_triggers[op][i]->addTerm( n );
- }
- }
- }
- }
}
}else{
setTermInactive( n );
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index d0bcd3a69..3017238ca 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -76,12 +76,6 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
++(qe->d_statistics.d_multi_triggers);
}
//Notice() << "Trigger : " << (*this) << " for " << f << std::endl;
- if( options::eagerInstQuant() ){
- for( int i=0; i<(int)d_nodes.size(); i++ ){
- Node op = qe->getTermDatabase()->getMatchOperator( d_nodes[i] );
- qe->getTermDatabase()->registerTrigger( this, op );
- }
- }
Trace("trigger-debug") << "Finished making trigger." << std::endl;
}
@@ -107,10 +101,6 @@ bool Trigger::getMatch( Node f, Node t, InstMatch& m ){
return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine );
}
-int Trigger::addTerm( Node t ){
- return d_mg->addTerm( d_f, t, d_quantEngine );
-}
-
Node Trigger::getInstPattern(){
return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
}
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 6d7bf1f4d..631627331 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -72,8 +72,6 @@ class Trigger {
Currently the trigger should not be a multi-trigger.
*/
bool getMatch( Node f, Node t, InstMatch& m);
- /** add ground term t, called when t is added to the TermDb */
- int addTerm( Node t );
/** return whether this is a multi-trigger */
bool isMultiTrigger() { return d_nodes.size()>1; }
/** get inst pattern list */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index fbfdb856e..ec20d1ede 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -794,10 +794,7 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
if( !d_presolve || !options::incrementalSolving() ){
std::set< Node > added;
getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
- //maybe have triggered instantiations if we are doing eager instantiation
- if( options::eagerInstQuant() ){
- flushLemmas();
- }
+
//added contains also the Node that just have been asserted in this branch
if( d_quant_rel ){
for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback