From b55cdcaee28aebed9f4ea7e4790e0c97249933ae Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 29 Sep 2016 17:48:33 -0500 Subject: [PATCH] Address some coverity warnings, add another stat. --- src/theory/quantifiers/candidate_generator.cpp | 1 + .../quantifiers/ce_guided_instantiation.cpp | 2 +- src/theory/quantifiers/ceg_instantiator.cpp | 4 +--- .../quantifiers/conjecture_generator.cpp | 3 +++ .../quantifiers/inst_match_generator.cpp | 18 ++++++++++-------- src/theory/quantifiers/inst_propagator.cpp | 2 ++ src/theory/quantifiers/inst_strategy_cbqi.cpp | 1 + src/theory/quantifiers/inst_strategy_cbqi.h | 2 +- .../quantifiers/inst_strategy_e_matching.cpp | 1 + src/theory/quantifiers/macros.cpp | 4 ++++ src/theory/quantifiers/macros.h | 2 +- src/theory/quantifiers/quant_conflict_find.cpp | 10 +++++++++- src/theory/quantifiers/relevant_domain.h | 5 ++++- src/theory/quantifiers/term_database.cpp | 1 + src/theory/quantifiers_engine.cpp | 4 ++++ src/theory/quantifiers_engine.h | 1 + src/theory/strings/theory_strings_rewriter.cpp | 1 + 17 files changed, 46 insertions(+), 16 deletions(-) diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index a0d9bda0f..8e8f34cac 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -264,6 +264,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp Assert( mpat.getKind()==INST_CONSTANT ); d_f = quantifiers::TermDb::getInstConstAttr( mpat ); d_index = mpat.getAttribute(InstVarNumAttribute()); + d_firstTime = false; } void CandidateGeneratorQEAll::resetInstantiationRound() { diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 718d06c32..54415d974 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -767,7 +767,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { Assert( dt.isSygus() ); //get the solution Node sol; - int status; + int status = -1; if( d_last_inst_si ){ Assert( d_conj->getCegConjectureSingleInv() != NULL ); sol = d_conj->getSingleInvocationSolution( i, tn, status ); diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 1f817da88..61a20ad42 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -329,9 +329,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( is_cv ){ d_stack_vars.push_back( pv ); } - if( vinst!=NULL ){ - d_active_instantiators.erase( pv ); - } + d_active_instantiators.erase( pv ); unregisterInstantiationVariable( pv ); return false; } diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f4eb67d74..11adc61fd 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -84,6 +84,9 @@ d_notify( *this ), d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), d_ee_conjectures( c ){ d_fullEffortCount = 0; + d_conj_count = 0; + d_subs_confirmCount = 0; + d_subs_unkCount = 0; d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR ); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index ceae3e4c8..2a940f1fd 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -741,17 +741,19 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q Node r = qe->getEqualityQuery()->getRepresentative( d_eqc ); //iterate over all classes except r tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op ); - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - if( it->first!=r ){ - InstMatch m( q ); - m.add( baseMatch ); - addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); - if( qe->inConflict() ){ - break; + if( tat ){ + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ + if( it->first!=r ){ + InstMatch m( q ); + m.add( baseMatch ); + addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); + if( qe->inConflict() ){ + break; + } } } + tat = NULL; } - tat = NULL; } } Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 41c9c40c8..1f68fb787 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -597,6 +597,8 @@ void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& term InstPropagator::InstPropagator( QuantifiersEngine* qe ) : d_qe( qe ), d_notify(*this), d_qy( qe ){ + d_icount = 1; + d_conflict = false; } bool InstPropagator::reset( Theory::Effort e ) { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index f432817fd..ac6e1edbe 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -625,6 +625,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategyCbqi( qe ) { d_out = new CegqiOutputInstStrategy( this ); d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); + d_check_vts_lemma_lc = false; } InstStrategyCegqi::~InstStrategyCegqi() throw () { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index eab267747..c9f62243f 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -79,7 +79,7 @@ protected: //elimination information (for delayed elimination) class NestedQEInfo { public: - NestedQEInfo(){} + NestedQEInfo() : d_doVts(false){} ~NestedQEInfo(){} Node d_q; std::vector< Node > d_inst_terms; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 49e0a698f..c4bf61b28 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -155,6 +155,7 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe d_regenerate_frequency = 3; d_regenerate = true; }else{ + d_regenerate_frequency = 1; d_regenerate = false; } } diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 582599680..976b81e60 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -33,6 +33,10 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; +QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){ + d_ground_macros = false; +} + bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; for( unsigned r=0; r& opc ); void debugMacroDefinition( Node oo, Node n ); public: - QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){} + QuantifierMacros( QuantifiersEngine * qe ); ~QuantifierMacros(){} bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 9b25e27d4..1e484311c 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -967,7 +967,11 @@ MatchGen::MatchGen() d_n(), d_type( typ_invalid ), d_type_not() -{} +{ + d_qni_size = 0; + d_child_counter = -1; + d_use_children = true; +} MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) @@ -980,6 +984,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) d_type(), d_type_not() { + //initialize temporary + d_child_counter = -1; + d_use_children = true; + Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl; std::vector< Node > qni_apps; d_qni_size = 0; diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 8bc8e1f04..aae8f6c5b 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -51,7 +51,10 @@ private: //what each literal does class RDomainLit { public: - RDomainLit() : d_merge(false){} + RDomainLit() : d_merge(false){ + d_rd[0] = NULL; + d_rd[1] = NULL; + } ~RDomainLit(){} bool d_merge; RDomain * d_rd[2]; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 740e76d63..2c6bfb7d3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -91,6 +91,7 @@ TermDb::TermDb(context::Context* c, context::UserContext* u, d_op_id_count(0), d_typ_id_count(0), d_sygus_tdb(NULL) { + d_consistent_ee = true; d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); d_zero = NodeManager::currentNM()->mkConst(Rational(0)); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 08faa8dc7..67990ef69 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1133,6 +1133,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } if( d_term_db->isEntailed( q[1], subs, false, true ) ){ Trace("inst-add-debug") << " --> Currently entailed." << std::endl; + ++(d_statistics.d_inst_duplicate_ent); return false; } //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true ); @@ -1520,6 +1521,7 @@ QuantifiersEngine::Statistics::Statistics() d_instantiations("QuantifiersEngine::Instantiations_Total", 0), d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), + d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0), d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), @@ -1544,6 +1546,7 @@ QuantifiersEngine::Statistics::Statistics() smtStatisticsRegistry()->registerStat(&d_instantiations); smtStatisticsRegistry()->registerStat(&d_inst_duplicate); smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent); smtStatisticsRegistry()->registerStat(&d_triggers); smtStatisticsRegistry()->registerStat(&d_simple_triggers); smtStatisticsRegistry()->registerStat(&d_multi_triggers); @@ -1570,6 +1573,7 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_instantiations); smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent); smtStatisticsRegistry()->unregisterStat(&d_triggers); smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d501cfc76..232d1d889 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -396,6 +396,7 @@ public: IntStat d_instantiations; IntStat d_inst_duplicate; IntStat d_inst_duplicate_eq; + IntStat d_inst_duplicate_ent; IntStat d_triggers; IntStat d_simple_triggers; IntStat d_multi_triggers; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 92b18eed0..2ee367cfc 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -741,6 +741,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i return ( s2 == r[0].getConst() ); } else { Assert( false, "RegExp contains variables" ); + return false; } } case kind::REGEXP_CONCAT: { -- 2.30.2