diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/options/options_template.cpp | 6 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 11 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 10 | ||||
-rw-r--r-- | src/prop/registrar.h | 10 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 11 | ||||
-rw-r--r-- | src/theory/bv/bitblaster.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.h | 22 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 8 | ||||
-rw-r--r-- | src/theory/theory_model.h | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 1 |
19 files changed, 107 insertions, 41 deletions
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index de44d717e..a16e7f899 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -557,6 +557,8 @@ ${all_modules_option_handlers} Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl; + free(extra_argv); + return nonOptions; } @@ -573,7 +575,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 577 "${template}" +#line 579 "${template}" NULL };/* smtOptions[] */ @@ -595,7 +597,7 @@ SExpr Options::getOptions() const throw() { ${all_modules_get_options} -#line 599 "${template}" +#line 601 "${template}" return SExpr(opts); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2a2a60391..cb4a32ee7 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -69,7 +69,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_theoryEngine(te), d_decisionEngine(de), d_context(satContext), + d_theoryProxy(NULL), d_satSolver(NULL), + d_registrar(NULL), d_cnfStream(NULL), d_satTimer(*this), d_interrupted(false) { @@ -78,16 +80,17 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_satSolver = SatSolverFactory::createDPLLMinisat(); - theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine); + d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream - (d_satSolver, registrar, + (d_satSolver, d_registrar, userContext, // fullLitToNode Map = options::threads() > 1 || options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY ); - d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream)); + d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream); + d_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); @@ -97,7 +100,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext PropEngine::~PropEngine() { Debug("prop") << "Destructing the PropEngine" << endl; delete d_cnfStream; + delete d_registrar; delete d_satSolver; + delete d_theoryProxy; } void PropEngine::assertFormula(TNode node) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 39182204c..753890087 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -32,6 +32,10 @@ namespace CVC4 { class DecisionEngine; class TheoryEngine; +namespace theory { + class TheoryRegistrar; +}/* CVC4::theory namespace */ + namespace prop { class CnfStream; @@ -132,12 +136,18 @@ class PropEngine { /** The context */ context::Context* d_context; + /** SAT solver's proxy back to theories; kept around for dtor cleanup */ + TheoryProxy* d_theoryProxy; + /** The SAT solver proxy */ DPLLSatSolverInterface* d_satSolver; /** List of all of the assertions that need to be made */ std::vector<Node> d_assertionList; + /** Theory registrar; kept around for destructor cleanup */ + theory::TheoryRegistrar* d_registrar; + /** The CNF converter in use */ CnfStream* d_cnfStream; diff --git a/src/prop/registrar.h b/src/prop/registrar.h index 0cb3accf1..4fe04f062 100644 --- a/src/prop/registrar.h +++ b/src/prop/registrar.h @@ -5,7 +5,7 @@ ** Major contributors: Tim King, Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -32,13 +32,11 @@ public: };/* class Registrar */ -class NullRegistrar: public Registrar { +class NullRegistrar : public Registrar { public: - void preRegister(Node n) {}; - -};/* class Registrar */ - + void preRegister(Node n) {} +};/* class NullRegistrar */ }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index f84aecbac..92c81616b 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -139,6 +139,10 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine, d_queue(context) {} +inline TheoryProxy::~TheoryProxy() { + /* nothing to do for now */ +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index cbe550f96..552f3b448 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -61,10 +61,12 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : d_statistics() { d_satSolver = prop::SatSolverFactory::createMinisat(c); - d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context()); + d_nullRegistrar = new NullRegistrar(); + d_nullContext = new Context(); + d_cnfStream = new TseitinCnfStream(d_satSolver, d_nullRegistrar, d_nullContext); - MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); - d_satSolver->setNotify(notify); + d_notify = new MinisatNotify(d_cnfStream, bv); + d_satSolver->setNotify(d_notify); // initializing the bit-blasting strategies initAtomBBStrategies(); initTermBBStrategies(); @@ -72,7 +74,10 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : Bitblaster::~Bitblaster() { delete d_cnfStream; + delete d_nullContext; + delete d_nullRegistrar; delete d_satSolver; + delete d_notify; } diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 2dc82bddc..34345086b 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -37,6 +37,7 @@ #include "bitblast_strategies.h" #include "prop/sat_solver.h" +#include "prop/registrar.h" namespace CVC4 { @@ -92,8 +93,11 @@ class Bitblaster { // sat solver used for bitblasting and associated CnfStream theory::OutputChannel* d_bvOutput; + MinisatNotify* d_notify; prop::BVSatSolverInterface* d_satSolver; prop::CnfStream* d_cnfStream; + prop::NullRegistrar* d_nullRegistrar; + context::Context* d_nullContext; // caches and mappings TermDefMap d_termCache; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 098a7819a..509c00bb6 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -545,6 +545,12 @@ FirstOrderModel(qe, c, name){ } +FirstOrderModelFmc::~FirstOrderModelFmc() { + for(std::map<Node, Def*>::iterator i = d_models.begin(); i != d_models.end(); ++i) { + delete (*i).second; + } +} + Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { //Assert( fm->hasTerm(n) ); TypeNode tn = n.getType(); diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 2ac9dadcf..63d8ffcce 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -26,14 +26,16 @@ namespace theory { class QuantifiersEngine; -namespace quantifiers{ +namespace quantifiers { class TermDb; class FirstOrderModelIG; + namespace fmcheck { class FirstOrderModelFmc; -} +}/* CVC4::theory::quantifiers::fmcheck namespace */ + class FirstOrderModelQInt; struct IsStarAttributeId {}; @@ -69,7 +71,7 @@ public: //for Theory Quantifiers: virtual void processInitializeQuantifier( Node q ) {} public: FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ); - virtual ~FirstOrderModel(){} + virtual ~FirstOrderModel() {} virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; } virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; } virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; } @@ -134,7 +136,7 @@ private: void clearEvalFailed( int index ); std::map< Node, bool > d_eval_failed; std::map< int, std::vector< Node > > d_eval_failed_lits; -}; +};/* class FirstOrderModelIG */ namespace fmcheck { @@ -156,6 +158,7 @@ private: void processInitializeModelForTerm(Node n); public: FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); + virtual ~FirstOrderModelFmc(); FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } // initialize the model void processInitialize( bool ispre ); @@ -169,9 +172,9 @@ public: bool isInterval(Node n); Node getInterval( Node lb, Node ub ); bool isInRange( Node v, Node i ); -}; +};/* class FirstOrderModelFmc */ -} +}/* CVC4::theory::quantifiers::fmcheck namespace */ class QIntDef; @@ -215,7 +218,7 @@ public: unsigned getOrderedNumVars( Node q ); TypeNode getOrderedVarType( Node q, int i ); int getOrderedVarNumToVarNum( Node q, int i ); -}; +};/* class FirstOrderModelQInt */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index db5abb01e..372868ad7 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef FULL_MODEL_CHECK -#define FULL_MODEL_CHECK +#ifndef __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H +#define __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H #include "theory/quantifiers/model_builder.h" #include "theory/quantifiers/first_order_model.h" @@ -45,7 +45,7 @@ public: void collectIndices(Node c, int index, std::vector< int >& indices ); bool isComplete(FirstOrderModelFmc * m, Node c, int index); -}; +};/* class EntryTrie */ class Def @@ -79,7 +79,7 @@ public: int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ); void simplify( FullModelChecker * mc, FirstOrderModelFmc * m ); void debugPrint(const char * tr, Node op, FullModelChecker * m); -}; +};/* class Def */ class FullModelChecker : public QModelBuilder @@ -151,11 +151,11 @@ public: Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial ); bool useSimpleModels(); -}; +};/* class FullModelChecker */ -} -} -} -} +}/* CVC4::theory::quantifiers::fmcheck namespace */ +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index e5705882a..c8a08dad9 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,10 +31,15 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){ } +InstantiationEngine::~InstantiationEngine() { + delete d_i_ag; + delete d_isup; +} + void InstantiationEngine::finishInit(){ //for UF terms if( !options::finiteModelFind() || options::fmfInstEngine() ){ @@ -48,14 +53,14 @@ void InstantiationEngine::finishInit(){ }else{ d_isup = NULL; } - InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, 3 ); - i_ag->setGenerateAdditional( true ); - addInstStrategy( i_ag ); + d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, 3 ); + d_i_ag->setGenerateAdditional( true ); + addInstStrategy( d_i_ag ); //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) ); if( !options::finiteModelFind() && options::fullSaturateQuant() ){ addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) ); } - //d_isup->setPriorityOver( i_ag ); + //d_isup->setPriorityOver( d_i_ag ); //d_isup->setPriorityOver( i_agm ); //i_ag->setPriorityOver( i_agm ); } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 394d53d42..53777d362 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -25,6 +25,7 @@ namespace theory { namespace quantifiers { class InstStrategyUserPatterns; +class InstStrategyAutoGenTriggers; /** instantiation strategy class */ class InstStrategy { @@ -79,6 +80,8 @@ private: std::map< InstStrategy*, bool > d_instStrategyActive; /** user-pattern instantiation strategy */ InstStrategyUserPatterns* d_isup; + /** auto gen triggers; only kept for destructor cleanup */ + InstStrategyAutoGenTriggers* d_i_ag; /** is instantiation strategy active */ bool isActiveStrategy( InstStrategy* is ) { return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is]; @@ -123,7 +126,7 @@ private: void debugSat( int reason ); public: InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true ); - ~InstantiationEngine(){} + ~InstantiationEngine(); /** initialize */ void finishInit(); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index d7b074acc..3a4879b42 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -53,6 +53,10 @@ QuantifiersModule( qe ){ } } +ModelEngine::~ModelEngine() { + delete d_builder; +} + void ModelEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ int addedLemmas = 0; diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 3b34f7504..79bdcd19b 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -48,7 +48,7 @@ private: int d_totalLemmas; public: ModelEngine( context::Context* c, QuantifiersEngine* qe ); - ~ModelEngine(){} + virtual ~ModelEngine(); //get the builder QModelBuilder* getModelBuilder() { return d_builder; } public: diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 8a0d956ac..71e967653 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -125,6 +125,7 @@ private: //for completing match std::vector< int > d_una_eqc_count;
public:
QuantInfo() : d_mg( NULL ) {}
+ ~QuantInfo() { delete d_mg; }
std::vector< TNode > d_vars;
std::map< TNode, int > d_var_num;
std::map< TNode, bool > d_nbeneathQuant;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index be011cdb6..b79c0da69 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -113,11 +113,20 @@ d_lemmas_produced_c(u){ } QuantifiersEngine::~QuantifiersEngine(){ + 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; + for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) { + delete (*i).second; + } } EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index f207bdb8e..7187a373f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -27,7 +27,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; -TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) : +TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) : d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) { d_true = NodeManager::currentNM()->mkConst( true ); @@ -46,6 +46,12 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc d_eeContext->push(); } +TheoryModel::~TheoryModel() { + d_eeContext->pop(); + delete d_equalityEngine; + delete d_eeContext; +} + void TheoryModel::reset(){ d_reps.clear(); d_rep_set.clear(); diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 598db2683..65b09befc 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -38,7 +38,7 @@ protected: SubstitutionMap d_substitutions; public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); - virtual ~TheoryModel(){} + virtual ~TheoryModel(); /** special local context for our equalityEngine so we can clear it independently of search context */ context::Context* d_eeContext; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index b9ca17154..938fc4f67 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -183,6 +183,7 @@ public: ++i) { delete i->second; } + delete d_thss; } void setMasterEqualityEngine(eq::EqualityEngine* eq); |