Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
+ free(extra_argv);
+
return nonOptions;
}
static const char* smtOptions[] = {
${all_modules_smt_options},
-#line 577 "${template}"
+#line 579 "${template}"
NULL
};/* smtOptions[] */
${all_modules_get_options}
-#line 599 "${template}"
+#line 601 "${template}"
return SExpr(opts);
}
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) {
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);
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) {
class DecisionEngine;
class TheoryEngine;
+namespace theory {
+ class TheoryRegistrar;
+}/* CVC4::theory namespace */
+
namespace prop {
class CnfStream;
/** 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;
** 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
**
};/* 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 */
d_queue(context)
{}
+inline TheoryProxy::~TheoryProxy() {
+ /* nothing to do for now */
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
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();
Bitblaster::~Bitblaster() {
delete d_cnfStream;
+ delete d_nullContext;
+ delete d_nullRegistrar;
delete d_satSolver;
+ delete d_notify;
}
#include "bitblast_strategies.h"
#include "prop/sat_solver.h"
+#include "prop/registrar.h"
namespace CVC4 {
// 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;
}
+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();
class QuantifiersEngine;
-namespace quantifiers{
+namespace quantifiers {
class TermDb;
class FirstOrderModelIG;
+
namespace fmcheck {
class FirstOrderModelFmc;
-}
+}/* CVC4::theory::quantifiers::fmcheck namespace */
+
class FirstOrderModelQInt;
struct IsStarAttributeId {};
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; }
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 {
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 );
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;
unsigned getOrderedNumVars( Node q );
TypeNode getOrderedVarType( Node q, int i );
int getOrderedVarNumToVarNum( Node q, int i );
-};
+};/* class FirstOrderModelQInt */
}/* CVC4::theory::quantifiers namespace */
** 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
**
#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"
void collectIndices(Node c, int index, std::vector< int >& indices );
bool isComplete(FirstOrderModelFmc * m, Node c, int index);
-};
+};/* class EntryTrie */
class Def
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
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 */
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() ){
}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 );
}
namespace quantifiers {
class InstStrategyUserPatterns;
+class InstStrategyAutoGenTriggers;
/** instantiation strategy class */
class InstStrategy {
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];
void debugSat( int reason );
public:
InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
- ~InstantiationEngine(){}
+ ~InstantiationEngine();
/** initialize */
void finishInit();
}
}
+ModelEngine::~ModelEngine() {
+ delete d_builder;
+}
+
void ModelEngine::check( Theory::Effort e ){
if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
int addedLemmas = 0;
int d_totalLemmas;
public:
ModelEngine( context::Context* c, QuantifiersEngine* qe );
- ~ModelEngine(){}
+ virtual ~ModelEngine();
//get the builder
QModelBuilder* getModelBuilder() { return d_builder; }
public:
std::vector< int > d_una_eqc_count;\r
public:\r
QuantInfo() : d_mg( NULL ) {}\r
+ ~QuantInfo() { delete d_mg; }\r
std::vector< TNode > d_vars;\r
std::map< TNode, int > d_var_num;\r
std::map< TNode, bool > d_nbeneathQuant;\r
}
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() {
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 );
d_eeContext->push();
}
+TheoryModel::~TheoryModel() {
+ d_eeContext->pop();
+ delete d_equalityEngine;
+ delete d_eeContext;
+}
+
void TheoryModel::reset(){
d_reps.clear();
d_rep_set.clear();
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;
++i) {
delete i->second;
}
+ delete d_thss;
}
void setMasterEqualityEngine(eq::EqualityEngine* eq);
projects / cvc5.git / commitdiff