Address some coverity warnings, add another stat.

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index a0d9bda0fe07445bedb0f4a501aecc7564284be1..8e8f34cac268a83971a620127073adfb9b8f31d6 100644 (file)
--- 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 718d06c322bfdc91e50fc1845195c4b7443f892d..54415d974ee0290f2b7ae4e05eb8149186f09eff 100644 (file)
--- 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 1f817da88c90db0eb3a76522ce85df6630011344..61a20ad42bb407ea32928525765c9313fc3e2198 100644 (file)
--- 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 f4eb67d7486d9ca7cd681c795b35bbdb58ed3807..11adc61fd3ecf3d8e5e1300511270d2bea53b7a2 100644 (file)
--- 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 ceae3e4c8363d1e7fd15bc350e1071bf16440d46..2a940f1fd15f1e3b7abaf97485b908d012a0c595 100644 (file)
--- 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 41c9c40c8e97c42d4ffc1ec9e7880e9c8991fb01..1f68fb787c236c0b8b2a214220c71fbaaeea53eb 100644 (file)
--- 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 f432817fd06a87f13fa29d7cfcc4f81e974142a0..ac6e1edbe874e11ae551528797bda9029c181b23 100644 (file)
--- 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 eab2677471c3d01254bfead5e3fae910655b47db..c9f62243fb139998b6f979a2a78852ff3117e914 100644 (file)
--- 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 49e0a698f62e54aaccc684fc3691a517c2aad686..c4bf61b280eb83b34a42d06628afb7aec6b5abe8 100644 (file)
--- 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 582599680494c525355cfcb6960c6cc0216b8c69..976b81e608c5795a6e843489d9c4dbf627257960 100644 (file)
--- 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<rmax; r++ ){

diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index 39ec2f0a1d5f85612f6efa62d13dfc27760d8e6f..60af7ad0a6a37ed827708cabb2a2e6c909ca2105 100644 (file)
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -60,7 +60,7 @@ private:
   void addMacro( Node op, Node n, std::vector< Node >& 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 9b25e27d4edff75148833c729fec58bfc21f1856..1e484311c9df7250ebeea149d94e836a19e9c1bb 100644 (file)
--- 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 8bc8e1f04fd362f88200b88066c065f54d26d8cd..aae8f6c5b3dcbeaf969c676aa60c4d9fba9baaef 100644 (file)
--- 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 740e76d63c1cee3548dad84635c207fa8042ee65..2c6bfb7d3a971d86757c9db4190ada2a1f6e5982 100644 (file)
--- 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 08faa8dc7a914e77cd60191c350180a7bac5910f..67990ef69c93cced05e6b618a35230bf9281af3a 100644 (file)
--- 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 d501cfc76d1e0b3092a0ce166d4e4f6c674ec977..232d1d889d6ed1fdafe0a02972e1067eebabf1b8 100644 (file)
--- 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 92b18eed0aa3627e827cac339124f1fcdf778d61..2ee367cfcca8129e0b954fbd6108ce29fd4484af 100644 (file)
--- 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<String>() );
       } else {
         Assert( false, "RegExp contains variables" );
+        return false;
       }
     }
     case kind::REGEXP_CONCAT: {