diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 98 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 9 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 1 |
9 files changed, 90 insertions, 63 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 84743fc1d..33dfa19bc 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -817,6 +817,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) { d_solution = s; const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); + Trace("csi-sol") << "Reconstruct to syntax " << s << ", allow all = " << dt.getSygusAllowAll() << " " << stn << ", reconstruct = " << rconsSygus << std::endl; //reconstruct the solution into sygus if necessary reconstructed = 0; diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 7ce299864..1543b2ebd 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -717,14 +717,10 @@ void CegInstantiator::processAssertions() { std::map< Node, Node > aux_subs; //for each variable - std::vector< TheoryId > tids; - tids.push_back(THEORY_UF); for( unsigned i=0; i<d_vars.size(); i++ ){ Node pv = d_vars[i]; TypeNode pvtn = pv.getType(); - //collect relevant theories - std::map< TypeNode, bool > visited; - collectTheoryIds( pvtn, visited, tids ); + Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl; //collect information about eqc if( ee->hasTerm( pv ) ){ Node pvr = ee->getRepresentative( pv ); @@ -739,8 +735,8 @@ void CegInstantiator::processAssertions() { } } //collect assertions for relevant theories - for( unsigned i=0; i<tids.size(); i++ ){ - TheoryId tid = tids[i]; + for( unsigned i=0; i<d_tids.size(); i++ ){ + TheoryId tid = d_tids[i]; Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){ Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl; @@ -781,7 +777,7 @@ void CegInstantiator::processAssertions() { TypeNode rtn = r.getType(); TheoryId tid = Theory::theoryOf( rtn ); //if we care about the theory of this eqc - if( std::find( tids.begin(), tids.end(), tid )!=tids.end() ){ + if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){ if( rtn.isInteger() || rtn.isReal() ){ rtn = rtn.getBaseType(); } @@ -810,7 +806,7 @@ void CegInstantiator::processAssertions() { if( it!=aux_subs.end() ){ addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); }else{ - Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl; + Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl; Assert( false ); } } @@ -997,6 +993,21 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st for( unsigned i=0; i<lems.size(); i++ ){ collectCeAtoms( lems[i], visited ); } + + //compute the theory ids + d_tids.clear(); + d_tids.push_back(THEORY_UF); + for( unsigned r=0; r<2; r++ ){ + unsigned sz = r==0 ? d_vars.size() : d_aux_vars.size(); + for( unsigned i=0; i<sz; i++ ){ + Node pv = r==0 ? d_vars[i] : d_aux_vars[i]; + TypeNode pvtn = pv.getType(); + Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl; + //collect relevant theories + std::map< TypeNode, bool > visited; + collectTheoryIds( pvtn, visited, d_tids ); + } + } } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 94d02de9b..f9a711704 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -93,6 +93,8 @@ private: std::map< TypeNode, std::vector< Node > > d_curr_type_eqc; //auxiliary variables std::vector< Node > d_aux_vars; + // relevant theory ids + std::vector< TheoryId > d_tids; //literals to equalities for aux vars std::map< Node, std::map< Node, Node > > d_aux_eq; //the CE variables diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 420a3d2f7..008514dcc 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2079,70 +2079,76 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { //try to make a matches making the body false Trace("qcf-check-debug") << "Get next match..." << std::endl; while( qi->getNextMatch( this ) ){ - Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - if( !qi->isMatchSpurious( this ) ){ - std::vector< int > assigned; - if( qi->completeMatch( this, assigned ) ){ - std::vector< Node > terms; - qi->getMatch( terms ); - bool tcs = qi->isTConstraintSpurious( this, terms ); - if( !tcs ){ - //for debugging - if( Debug.isOn("qcf-check-inst") ){ - Node inst = d_quantEngine->getInstantiation( q, terms ); - Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( !getTermDatabase()->isEntailed( inst, true ) ); - Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); - } - 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"); - Trace("qcf-inst") << std::endl; - ++addedLemmas; - if( e==effort_conflict ){ - d_quantEngine->markRelevant( q ); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); - if( options::qcfAllConflict() ){ - isConflict = true; - }else{ - d_conflict.set( true ); + if( d_quantEngine->inConflict() ){ + Trace("qcf-check") << " ... Quantifiers engine discovered conflict, "; + Trace("qcf-check") << "probably related to disequal congruent terms in master equality engine" << std::endl; + break; + }else{ + Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + if( !qi->isMatchSpurious( this ) ){ + std::vector< int > assigned; + if( qi->completeMatch( this, assigned ) ){ + std::vector< Node > terms; + qi->getMatch( terms ); + bool tcs = qi->isTConstraintSpurious( this, terms ); + if( !tcs ){ + //for debugging + if( Debug.isOn("qcf-check-inst") ){ + Node inst = d_quantEngine->getInstantiation( q, terms ); + Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; + Assert( !getTermDatabase()->isEntailed( inst, true ) ); + Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); + } + 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"); + Trace("qcf-inst") << std::endl; + ++addedLemmas; + if( e==effort_conflict ){ + d_quantEngine->markRelevant( q ); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); + if( options::qcfAllConflict() ){ + isConflict = true; + }else{ + d_conflict.set( true ); + } + break; + }else if( e==effort_prop_eq ){ + d_quantEngine->markRelevant( q ); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); } + }else{ + Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; + //this should only happen if the algorithm generates the same propagating instance twice this round + //in this case, break to avoid exponential behavior break; - }else if( e==effort_prop_eq ){ - d_quantEngine->markRelevant( q ); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); } }else{ - Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; - //this should only happen if the algorithm generates the same propagating instance twice this round - //in this case, break to avoid exponential behavior - break; + Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; } + //clean up assigned + qi->revertMatch( this, assigned ); + d_tempCache.clear(); }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; + Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; } - //clean up assigned - qi->revertMatch( this, assigned ); - d_tempCache.clear(); }else{ - Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; + Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; } - }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; } } Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; - if( d_conflict ){ + if( d_conflict || d_quantEngine->inConflict() ){ break; } } } } } - if( addedLemmas>0 ){ + if( addedLemmas>0 || d_quantEngine->inConflict() ){ break; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5ac5ae0cc..30b17d42c 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -278,10 +278,12 @@ void TermDb::computeUfTerms( TNode f ) { Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; if( !d_quantEngine->getTheoryEngine()->needCheck() ){ Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; + // we should be a full effort check, prior to theory combination } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } d_quantEngine->addLemma( lem ); + d_quantEngine->setConflict(); d_consistent_ee = false; return; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index db0efd988..55b1af83c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -80,6 +80,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_util.push_back( d_term_db ); if( options::instPropagate() ){ + // notice that this option is incompatible with options::qcfAllConflict() d_inst_prop = new quantifiers::InstPropagator( this ); d_util.push_back( d_inst_prop ); d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() ); @@ -1250,8 +1251,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo for( unsigned j=0; j<d_inst_notify.size(); j++ ){ if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){ Trace("inst-add-debug") << "...we are in conflict." << std::endl; - d_conflict = true; - d_conflict_c = true; + setConflict(); Assert( !d_lemmas_waiting.empty() ); break; } @@ -1319,6 +1319,11 @@ void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); } +void QuantifiersEngine::setConflict() { + d_conflict = true; + d_conflict_c = true; +} + bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; //determine if we should perform check, based on instWhenMode diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bb38e5e4a..7405241b7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -39,11 +39,6 @@ namespace theory { class QuantifiersEngine; -namespace quantifiers { - class TermDb; - class TermDbSygus; -} - class InstantiationNotify { public: InstantiationNotify(){} @@ -53,6 +48,8 @@ public: }; namespace quantifiers { + class TermDb; + class TermDbSygus; class FirstOrderModel; //modules class InstantiationEngine; @@ -343,6 +340,8 @@ public: bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** is in conflict */ bool inConflict() { return d_conflict; } + /** set conflict */ + void setConflict(); /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } /** get needs check */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 0338eb1b3..a0748f2b9 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -856,7 +856,7 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) { valid = true; }else{ // if not, check whether it is definitely not a member, if unknown, split - bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2->second.end(); + bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2n->second.end(); if( !not_in_r2 ){ exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ) ); valid = true; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 3590fc62d..e42a3347d 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -328,6 +328,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager::currentNM()->mkNode( kind::CARD, NodeManager::currentNM()->mkNode( kind::INTERSECTION, node[0][0], node[0][1] ) ) ); return RewriteResponse(REWRITE_DONE, ret ); } + break; } case kind::TRANSPOSE: { if(node[0].getKind() == kind::TRANSPOSE) { |