summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_strategy_cbqi.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-08-01 17:22:11 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2015-08-01 17:22:11 +0200
commit86ad2ca93048844eedcafd2a2dadc43ef85dfb32 (patch)
tree69e4b02df3f06e090a668f01fbf8a18438d927c1 /src/theory/quantifiers/inst_strategy_cbqi.cpp
parent8f4e966ae0c0f42e595e1c603cb7c3f779b713ef (diff)
Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datatypes.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp43
1 files changed, 6 insertions, 37 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 0c4648e51..20bd71b45 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -56,16 +56,10 @@ void CegInstantiator::computeProgVars( Node n ){
d_inelig[n] = true;
return;
}
- if( d_has_delta.find( n[i] )!=d_has_delta.end() ){
- d_has_delta[n] = true;
- }
for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
d_prog_var[n][it->first] = true;
}
}
- if( n==d_n_delta ){
- d_has_delta[n] = true;
- }
}
}
@@ -108,12 +102,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
ns = n;
proc = true;
}
- if( d_has_delta.find( ns )!=d_has_delta.end() ){
- //also must set delta to zero
- ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero );
- ns = Rewriter::rewrite( ns );
- computeProgVars( ns );
- }
if( proc ){
//try the substitution
subs_proc[0][ns][pv_coeff] = true;
@@ -180,9 +168,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl;
std::map< Node, Node > msum;
if( QuantArith::getMonomialSumLit( eq, msum ) ){
- if( !d_n_delta.isNull() ){
- msum.erase( d_n_delta );
- }
if( Trace.isOn("cegqi-si-inst-debug") ){
Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
@@ -269,9 +254,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl;
std::map< Node, Node > msum;
if( QuantArith::getMonomialSumLit( satom, msum ) ){
- if( !d_n_delta.isNull() ){
- msum.erase( d_n_delta );
- }
if( Trace.isOn("cegqi-si-inst-debug") ){
Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
@@ -358,6 +340,11 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
unsigned i, unsigned effort ) {
+ if( styp==2 || styp==-2 ){
+ Node delta = d_qe->getTermDatabase()->getVtsDelta();
+ n = NodeManager::currentNM()->mkNode( styp==2 ? PLUS : MINUS, n, delta );
+ n = Rewriter::rewrite( n );
+ }
//must ensure variables have been computed for n
computeProgVars( n );
//substitute into previous substitutions, when applicable
@@ -530,25 +517,7 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec
}
bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ) {
- // do delta rationals
- std::map< int, Node > prev;
- for( unsigned i=0; i<subs.size(); i++ ){
- if( subs_typ[i]==2 || subs_typ[i]==-2 ){
- prev[i] = subs[i];
- Node delta = d_qe->getTermDatabase()->getVtsDelta();
- d_n_delta = delta;
- subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], delta );
- }
- }
- //check if we have already added this instantiation
- bool success = d_out->addInstantiation( subs, subs_typ );
- if( !success ){
- //revert the substitution
- for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){
- subs[it->first] = it->second;
- }
- }
- return success;
+ return d_out->addInstantiation( subs, subs_typ );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback