summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/theory/quantifiers/alpha_equivalence.cpp15
-rw-r--r--src/theory/quantifiers/alpha_equivalence.h8
-rw-r--r--src/theory/quantifiers/ambqi_builder.cpp2
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp2
-rw-r--r--src/theory/quantifiers/full_model_check.cpp4
-rw-r--r--src/theory/quantifiers/inst_match.cpp16
-rw-r--r--src/theory/quantifiers/inst_match.h32
-rw-r--r--src/theory/quantifiers/inst_match_generator.cpp12
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp4
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp14
-rw-r--r--src/theory/quantifiers/model_builder.cpp4
-rw-r--r--src/theory/quantifiers/model_engine.cpp2
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp2
-rw-r--r--src/theory/quantifiers/rewrite_engine.cpp2
-rw-r--r--src/theory/quantifiers_engine.cpp72
-rw-r--r--src/theory/quantifiers_engine.h11
17 files changed, 105 insertions, 99 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bd67af466..771195a38 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5152,7 +5152,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
//ensure all instantiations were accounted for
for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){
- if( visited.find( it->first )==visited.end() ){
+ if( !it->second.empty() && visited.find( it->first )==visited.end() ){
stringstream ss;
ss << "While performing quantifier elimination, processed a quantified formula : " << it->first;
ss << " that was not related to the query. Try option --simplification=none.";
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 8abc3f65a..80066d690 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -29,7 +29,7 @@ struct sortTypeOrder {
}
};
-bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
+Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
while( !tt.empty() ){
if( tt.size()==arg_index.size()+1 ){
Node t = tt.back();
@@ -49,26 +49,25 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE
}
}
}
+ Node lem;
Trace("aeq-debug") << std::endl;
if( aen->d_quant.isNull() ){
aen->d_quant = q;
- return true;
}else{
if( q.getNumChildren()==2 ){
//lemma ( q <=> d_quant )
Trace("quant-ae") << "Alpha equivalent : " << std::endl;
Trace("quant-ae") << " " << q << std::endl;
Trace("quant-ae") << " " << aen->d_quant << std::endl;
- qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
- return false;
+ lem = q.iffNode( aen->d_quant );
}else{
//do not reduce annotated quantified formulas based on alpha equivalence
- return true;
}
}
+ return lem;
}
-bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
+Node AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){
while( index<(int)typs.size() ){
TypeNode curr = typs[index];
@@ -84,7 +83,7 @@ bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index );
}
-bool AlphaEquivalence::reduceQuantifier( Node q ) {
+Node AlphaEquivalence::reduceQuantifier( Node q ) {
Assert( q.getKind()==FORALL );
Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
//construct canonical quantified formula
@@ -104,7 +103,7 @@ bool AlphaEquivalence::reduceQuantifier( Node q ) {
sto.d_tdb = d_qe->getTermDatabase();
std::sort( typs.begin(), typs.end(), sto );
Trace("aeq-debug") << " ";
- bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
+ Node ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
Trace("aeq") << " ...result : " << ret << std::endl;
return ret;
}
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 40f533da7..8e7556eb6 100644
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -28,14 +28,14 @@ class AlphaEquivalenceNode {
public:
std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children;
Node d_quant;
- static bool registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
+ static Node registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
};
class AlphaEquivalenceTypeNode {
public:
std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children;
AlphaEquivalenceNode d_data;
- static bool registerNode( AlphaEquivalenceTypeNode* aetn,
+ static Node registerNode( AlphaEquivalenceTypeNode* aetn,
QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 );
};
@@ -47,8 +47,8 @@ private:
public:
AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){}
~AlphaEquivalence(){}
-
- bool reduceQuantifier( Node q );
+ /** reduce quantifier, return value (if non-null) is lemma justifying why q ia reducible. */
+ Node reduceQuantifier( Node q );
};
}
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index dd6db951d..5192da7de 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -159,7 +159,7 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe,
return true;
}else{
if( depth==q[0].getNumChildren() ){
- if( qe->addInstantiation( q, terms ) ){
+ if( qe->addInstantiation( q, terms, true ) ){
Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;
inst++;
return true;
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index b00ddf036..d9059a3e6 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -432,7 +432,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
Assert( aq==q );
std::vector< Node > model_terms;
if( getModelValues( conj, conj->d_candidates, model_terms ) ){
- d_quantEngine->addInstantiation( q, model_terms, false );
+ d_quantEngine->addInstantiation( q, model_terms );
}
}
}else{
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 6b06b9e5c..33c853328 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -682,7 +682,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
}else{
//just add the instance
d_triedLemmas++;
- if( d_qe->addInstantiation( f, inst ) ){
+ if( d_qe->addInstantiation( f, inst, true ) ){
Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
d_addedLemmas++;
if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
@@ -810,7 +810,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
if (ev!=d_true) {
Trace("fmc-exh-debug") << ", add!";
//add as instantiation
- if( d_qe->addInstantiation( f, inst ) ){
+ if( d_qe->addInstantiation( f, inst, true ) ){
Trace("fmc-exh-debug") << " ...success.";
addedLemmas++;
if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 55a4e8f8c..8818175db 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -142,7 +142,7 @@ bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
}
bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq,
- bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ) {
+ ImtIndexOrder* imtio, bool onlyExist, int index ) {
if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
return false;
}else{
@@ -150,7 +150,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
Node n = m[i_index];
std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
if( it!=d_data.end() ){
- bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
+ bool ret = it->second.addInstMatch( qe, f, m, modEq, imtio, onlyExist, index+1 );
if( !onlyExist || !ret ){
return ret;
}
@@ -165,7 +165,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
if( en!=n ){
std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
if( itc!=d_data.end() ){
- if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+ if( itc->second.addInstMatch( qe, f, m, modEq, imtio, true, index+1 ) ){
return false;
}
}
@@ -175,7 +175,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
}
}
if( !onlyExist ){
- d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
+ d_data[n].addInstMatch( qe, f, m, modEq, imtio, false, index+1 );
}
return true;
}
@@ -240,7 +240,7 @@ CDInstMatchTrie::~CDInstMatchTrie() {
bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
- context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
+ context::Context* c, bool modEq, int index, bool onlyExist ){
bool reset = false;
if( !d_valid.get() ){
if( onlyExist ){
@@ -256,7 +256,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
Node n = m[ index ];
std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
if( it!=d_data.end() ){
- bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist );
+ bool ret = it->second->addInstMatch( qe, f, m, c, modEq, index+1, onlyExist );
if( !onlyExist || !ret ){
return reset || ret;
}
@@ -271,7 +271,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
if( en!=n ){
std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
if( itc!=d_data.end() ){
- if( itc->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
+ if( itc->second->addInstMatch( qe, f, m, c, modEq, index+1, true ) ){
return false;
}
}
@@ -286,7 +286,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
CDInstMatchTrie* imt = new CDInstMatchTrie( c );
Assert(d_data.find(n) == d_data.end());
d_data[n] = imt;
- imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
+ imt->addInstMatch( qe, f, m, c, modEq, index+1, false );
}
return true;
}
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index a87d2704e..ad287c1a3 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -111,23 +111,23 @@ public:
modInst is if we return true if m is an instance of a match that exists
*/
bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
- bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
- return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+ ImtIndexOrder* imtio = NULL, int index = 0 ) {
+ return !addInstMatch( qe, f, m, modEq, imtio, true, index );
}
bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
- bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
- return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+ ImtIndexOrder* imtio = NULL, int index = 0 ) {
+ return !addInstMatch( qe, f, m, modEq, imtio, true, index );
}
/** add match m for quantifier f, take into account equalities if modEq = true,
if imtio is non-null, this is the order to add to trie
return true if successful
*/
bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
- bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
- return addInstMatch( qe, f, m.d_vals, modEq, modInst, imtio, onlyExist, index );
+ ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
+ return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index );
}
bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
- bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
+ ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
void print( std::ostream& out, Node q ) const{
std::vector< TNode > terms;
@@ -159,23 +159,23 @@ public:
modInst is if we return true if m is an instance of a match that exists
*/
bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
- bool modInst = false, int index = 0 ) {
- return !addInstMatch( qe, q, m, c, modEq, modInst, index, true );
+ int index = 0 ) {
+ return !addInstMatch( qe, q, m, c, modEq, index, true );
}
bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
- bool modInst = false, int index = 0 ) {
- return !addInstMatch( qe, q, m, c, modEq, modInst, index, true );
+ int index = 0 ) {
+ return !addInstMatch( qe, q, m, c, modEq, index, true );
}
/** add match m for quantifier f, take into account equalities if modEq = true,
if imtio is non-null, this is the order to add to trie
return true if successful
*/
bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
- bool modInst = false, int index = 0, bool onlyExist = false ) {
- return addInstMatch( qe, q, m.d_vals, c, modEq, modInst, index, onlyExist );
+ int index = 0, bool onlyExist = false ) {
+ return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist );
}
bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
- bool modInst = false, int index = 0, bool onlyExist = false );
+ int index = 0, bool onlyExist = false );
bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
void print( std::ostream& out, Node q ) const{
std::vector< TNode > terms;
@@ -202,10 +202,10 @@ public:
public:
/** add match m, return true if successful */
bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
- return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio );
+ return d_imt.addInstMatch( qe, f, m, modEq, d_imtio );
}
bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
- return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio );
+ return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio );
}
};/* class InstMatchTrieOrdered */
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 791e36ce4..bf05de3bb 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -270,7 +270,7 @@ bool InstMatchGenerator::continueNextMatch( Node f, InstMatch& m, QuantifiersEng
return d_next->getNextMatch( f, m, qe );
}else{
if( d_active_add ){
- return qe->addInstantiation( f, m, false );
+ return qe->addInstantiation( f, m );
}else{
return true;
}
@@ -343,7 +343,7 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
while( getNextMatch( f, m, qe ) ){
if( !d_active_add ){
m.add( baseMatch );
- if( qe->addInstantiation( f, m, false ) ){
+ if( qe->addInstantiation( f, m ) ){
addedLemmas++;
if( qe->inConflict() ){
break;
@@ -366,7 +366,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
if( !d_match_pattern.isNull() ){
InstMatch m( f );
if( getMatch( f, t, m, qe ) ){
- if( qe->addInstantiation( f, m, false ) ){
+ if( qe->addInstantiation( f, m ) ){
return 1;
}
}
@@ -674,7 +674,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
}
}else{
//m is an instantiation
- if( qe->addInstantiation( d_f, m, false ) ){
+ if( qe->addInstantiation( d_f, m ) ){
addedLemmas++;
Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
}
@@ -770,7 +770,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl;
m.setValue( it->second, t[it->first] );
}
- if( qe->addInstantiation( d_f, m, false ) ){
+ if( qe->addInstantiation( d_f, m ) ){
addedLemmas++;
Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
}
@@ -815,7 +815,7 @@ int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){
return 0;
}
}
- return qe->addInstantiation( q, m, false ) ? 1 : 0;
+ return qe->addInstantiation( q, m ) ? 1 : 0;
}
}/* CVC4::theory::inst namespace */
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index fe4867b4e..149330c61 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -648,12 +648,12 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
d_cbqi_set_quant_inactive = true;
d_incomplete_check = true;
- d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false, true );
+ d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
return true;
}else{
//check if we need virtual term substitution (if used delta or infinity)
bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
- if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
+ if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
//d_added_inst.insert( d_curr_quant );
return true;
}else{
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 8c67eb95e..630880690 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -599,18 +599,6 @@ bool FullSaturation::process( Node f, bool fullEffort ){
unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
unsigned rend = fullEffort ? 1 : rstart;
for( unsigned r=rstart; r<=rend; r++ ){
- /*
- //complete guess
- if( d_guessed.find( f )==d_guessed.end() ){
- Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
- d_guessed[f] = true;
- InstMatch m( f );
- if( d_quantEngine->addInstantiation( f, m ) ){
- ++(d_quantEngine->d_statistics.d_instantiations_guess);
- return true;
- }
- }
- */
if( rd || r>0 ){
if( r==0 ){
Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
@@ -700,7 +688,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
Trace("inst-alg-rd") << " " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl;
}
}
- if( d_quantEngine->addInstantiation( f, terms, false ) ){
+ if( d_quantEngine->addInstantiation( f, terms ) ){
Trace("inst-alg-rd") << "Success!" << std::endl;
++(d_quantEngine->d_statistics.d_instantiations_guess);
return true;
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index b0ca43cfe..3ae36b1d4 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -280,7 +280,7 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
//try to add it
Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
//add model basis instantiation
- if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false ) ){
+ if( d_qe->addInstantiation( fp, d_quant_basis_match[f] ) ){
d_quant_basis_match_added[f] = true;
return 1;
}else{
@@ -430,7 +430,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
//add as instantiation
- if( d_qe->addInstantiation( f, m ) ){
+ if( d_qe->addInstantiation( f, m, true ) ){
d_addedLemmas++;
if( d_qe->inConflict() ){
break;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f94e947e5..0bbca88eb 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -294,7 +294,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
triedLemmas++;
//add as instantiation
- if( d_quantEngine->addInstantiation( f, m ) ){
+ if( d_quantEngine->addInstantiation( f, m, true ) ){
addedLemmas++;
if( d_quantEngine->inConflict() ){
break;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c796333b3..ca87a607d 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2004,7 +2004,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
Assert( !getTermDatabase()->isEntailed( inst, true ) );
Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
}
- if( d_quantEngine->addInstantiation( q, terms, false ) ){
+ if( d_quantEngine->addInstantiation( q, terms ) ){
Trace("qcf-check") << " ... Added instantiation" << std::endl;
Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
qi->debugPrintMatch("qcf-inst");
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 07b1462c6..5365dbcfa 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -154,7 +154,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
if( inst.size()>f[0].getNumChildren() ){
inst.resize( f[0].getNumChildren() );
}
- if( d_quantEngine->addInstantiation( f, inst, false ) ){
+ if( d_quantEngine->addInstantiation( f, inst ) ){
addedLemmas++;
tempAddedLemmas++;
/*
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1008d7d49..6d3b17254 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -58,7 +58,7 @@ using namespace CVC4::theory::inst;
QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
d_te( te ),
//d_quants(u),
- //d_quants_red(u),
+ d_quants_red(u),
d_lemmas_produced_c(u),
d_skolemized(u),
d_ierCounter_c(c),
@@ -385,6 +385,14 @@ void QuantifiersEngine::check( Theory::Effort e ){
if( d_hasAddedLemma ){
return;
}
+ if( !d_recorded_inst.empty() ){
+ Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() << " instantiations..." << std::endl;
+ //remove explicitly recorded instantiations
+ for( unsigned i=0; i<d_recorded_inst.size(); i++ ){
+ removeInstantiationInternal( d_recorded_inst[i].first, d_recorded_inst[i].second );
+ }
+ d_recorded_inst.clear();
+ }
if( Trace.isOn("quant-engine-debug") ){
Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
@@ -503,6 +511,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
}else if( quant_e==QEFFORT_MODEL ){
if( e==Theory::EFFORT_LAST_CALL ){
+ if( !d_recorded_inst.empty() ){
+ setIncomplete = true;
+ }
//if we have a chance not to set incomplete
if( !setIncomplete ){
setIncomplete = false;
@@ -572,20 +583,29 @@ void QuantifiersEngine::notifyCombineTheories() {
}
bool QuantifiersEngine::reduceQuantifier( Node q ) {
- std::map< Node, bool >::iterator it = d_quants_red.find( q );
+ BoolMap::const_iterator it = d_quants_red.find( q );
if( it==d_quants_red.end() ){
- if( d_alpha_equiv ){
- Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
- //add equivalence with another quantified formula
- if( d_alpha_equiv->reduceQuantifier( q ) ){
- Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
- ++(d_statistics.d_red_alpha_equiv);
- d_quants_red[q] = true;
- return true;
+ Node lem;
+ std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
+ if( itr==d_quants_red_lem.end() ){
+ if( d_alpha_equiv ){
+ Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
+ //add equivalence with another quantified formula
+ lem = d_alpha_equiv->reduceQuantifier( q );
+ if( !lem.isNull() ){
+ Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
+ ++(d_statistics.d_red_alpha_equiv);
+ }
}
+ d_quants_red_lem[q] = lem;
+ }else{
+ lem = itr->second;
}
- d_quants_red[q] = false;
- return false;
+ if( !lem.isNull() ){
+ getOutputChannel().lemma( lem );
+ }
+ d_quants_red[q] = !lem.isNull();
+ return !lem.isNull();
}else{
return (*it).second;
}
@@ -759,13 +779,13 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No
}
-bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst, bool addedLem ) {
+bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool addedLem ) {
if( !addedLem ){
//record the instantiation for deletion later
- //TODO
+ d_recorded_inst.push_back( std::pair< Node, std::vector< Node > >( q, terms ) );
}
if( options::incrementalSolving() ){
- Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
+ Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << std::endl;
inst::CDInstMatchTrie* imt;
std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
if( it!=d_c_inst_match_trie.end() ){
@@ -774,10 +794,10 @@ bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >
imt = new CDInstMatchTrie( getUserContext() );
d_c_inst_match_trie[q] = imt;
}
- return imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst );
+ return imt->addInstMatch( this, q, terms, getUserContext(), modEq );
}else{
Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
- return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst );
+ return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq );
}
}
@@ -906,24 +926,20 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bo
}
/*
-bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
+bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){
if( options::incrementalSolving() ){
if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
- if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
+ if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){
return true;
}
}
}else{
if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
- if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
+ if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){
return true;
}
}
}
- //also check model builder (it may contain instantiations internally)
- if( d_builder && d_builder->existsInstantiation( f, m, modEq, modInst ) ){
- return true;
- }
return false;
}
*/
@@ -969,13 +985,13 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
d_phase_req_waiting[lit] = req;
}
-bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){
+bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts ){
std::vector< Node > terms;
m.getTerms( q, terms );
- return addInstantiation( q, terms, mkRep, modEq, modInst, doVts );
+ return addInstantiation( q, terms, mkRep, modEq, doVts );
}
-bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) {
+bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool doVts ) {
// For resource-limiting (also does a time check).
getOutputChannel().safePoint(options::quantifierStep());
Assert( !d_conflict );
@@ -1052,7 +1068,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
}
//check for term vector duplication
- bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst );
+ bool alreadyExists = !recordInstantiationInternal( q, terms, modEq );
if( alreadyExists ){
Trace("inst-add-debug") << " --> Already exists." << std::endl;
++(d_statistics.d_inst_duplicate_eq);
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index a088dfec6..4ee66f9e7 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -164,7 +164,8 @@ private:
/** list of all quantifiers seen */
std::map< Node, bool > d_quants;
/** quantifiers reduced */
- std::map< Node, bool > d_quants_red;
+ BoolMap d_quants_red;
+ std::map< Node, Node > d_quants_red_lem;
/** list of all lemmas produced */
//std::map< Node, bool > d_lemmas_produced;
BoolMap d_lemmas_produced_c;
@@ -175,6 +176,8 @@ private:
/** list of all instantiations produced for each quantifier */
std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
+ /** recorded instantiations */
+ std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
/** quantifiers that have been skolemized */
BoolMap d_skolemized;
/** term database */
@@ -287,7 +290,7 @@ private:
/** compute term vector */
void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
/** record instantiation, return true if it was non-duplicate */
- bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false, bool addedLem = true );
+ bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true );
/** remove instantiation */
bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
/** set instantiation level attr */
@@ -310,9 +313,9 @@ public:
/** add require phase */
void addRequirePhase( Node lit, bool req );
/** do instantiation specified by m */
- bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+ bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false );
/** add instantiation */
- bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+ bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false );
/** remove pending instantiation */
bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms );
/** split on node n */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback