From: Tim King <taking@google.com>
Date: Thu, 5 Nov 2015 22:56:49 +0000 (-0800)
Subject: Merging the google branch back into master.
X-Git-Tag: cvc5-1.0.0~6175
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0348ee46cb5cfda75fc877e73f176838140fbe61;p=cvc5.git

Merging the google branch back into master.
---

0348ee46cb5cfda75fc877e73f176838140fbe61
diff --cc src/theory/quantifiers_engine.cpp
index ba3dc9fb0,cfe53dd0f..aab04c32c
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@@ -113,76 -115,6 +113,77 @@@ d_presolve_cache_wic(u)
      d_quant_rel = NULL;
    }
  
 +  d_qcf = NULL;
 +  d_sg_gen = NULL;
 +  d_inst_engine = NULL;
 +  d_i_cbqi = NULL;
 +  d_model_engine = NULL;
 +  d_bint = NULL;
 +  d_rr_engine = NULL;
 +  d_ceg_inst = NULL;
 +  d_lte_part_inst = NULL;
 +  d_alpha_equiv = NULL;
 +  d_fun_def_engine = NULL;
 +  d_uee = NULL;
 +  d_fs = NULL;
 +  d_rel_dom = NULL;
 +  d_builder = NULL;
 +
 +  d_total_inst_count_debug = 0;
 +  d_ierCounter = 0;
 +  d_ierCounter_lc = 0;
 +  //if any strategy called only on last call, use phase 3
 +  d_inst_when_phase = options::cbqi() ? 3 : 2;
 +}
 +
 +QuantifiersEngine::~QuantifiersEngine(){
++  delete d_alpha_equiv;
 +  delete d_builder;
 +  delete d_rr_engine;
 +  delete d_bint;
 +  delete d_model_engine;
 +  delete d_inst_engine;
 +  delete d_qcf;
 +  delete d_quant_rel;
 +  delete d_rel_dom;
 +  delete d_model;
 +  delete d_tr_trie;
 +  delete d_term_db;
 +  delete d_eq_query;
 +  delete d_sg_gen;
 +  delete d_ceg_inst;
 +  delete d_lte_part_inst;
 +  delete d_fun_def_engine;
 +  delete d_uee;
 +  delete d_fs;
 +  delete d_i_cbqi;
 +}
 +
 +EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
 +  return d_eq_query;
 +}
 +
 +context::Context* QuantifiersEngine::getSatContext(){
 +  return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 +}
 +
 +context::UserContext* QuantifiersEngine::getUserContext(){
 +  return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
 +}
 +
 +OutputChannel& QuantifiersEngine::getOutputChannel(){
 +  return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
 +}
 +/** get default valuation for the quantifiers engine */
 +Valuation& QuantifiersEngine::getValuation(){
 +  return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
 +}
 +
 +void QuantifiersEngine::finishInit(){
 +  context::Context * c = getSatContext();
 +  Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
 +  bool needsBuilder = false;
 +  bool needsRelDom = false;
    //add quantifiers modules
    if( options::quantConflictFind() || options::quantRewriteRules() ){
      d_qcf = new quantifiers::QuantConflictFind( this, c);
@@@ -1447,4 -1462,4 +1448,3 @@@ int EqualityQueryQuantifiersEngine::get
    }
    //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
  }
--