diff options
author | Tim King <taking@google.com> | 2016-09-25 20:28:30 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-09-25 20:28:30 -0700 |
commit | 8cd543e7463fd4d382b9e87df7235ad1b7641a94 (patch) | |
tree | 05b02e6a64507f895b50ad79d8c97064cbb746bc /src/theory/quantifiers/term_database.cpp | |
parent | caff26cca60c3ab5a8f967e762c824b9b3806b30 (diff) |
Adding a destructor to TermDb.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 38 |
1 files changed, 25 insertions, 13 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ff11babc9..740e76d63 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -33,14 +33,14 @@ #include "util/bitvector.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - using namespace CVC4::theory::inst; +namespace CVC4 { +namespace theory { +namespace quantifiers { + TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) { if( argIndex==(int)reps.size() ){ if( d_data.empty() ){ @@ -84,15 +84,24 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { - d_true = NodeManager::currentNM()->mkConst( true ); - d_false = NodeManager::currentNM()->mkConst( false ); - d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - if( options::ceGuidedInst() ){ - d_sygus_tdb = new TermDbSygus( c, qe ); - }else{ - d_sygus_tdb = NULL; +TermDb::TermDb(context::Context* c, context::UserContext* u, + QuantifiersEngine* qe) + : d_quantEngine(qe), + d_inactive_map(c), + d_op_id_count(0), + d_typ_id_count(0), + d_sygus_tdb(NULL) { + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); + if (options::ceGuidedInst()) { + d_sygus_tdb = new TermDbSygus(c, qe); + } +} +TermDb::~TermDb(){ + if(d_sygus_tdb) { + delete d_sygus_tdb; } } @@ -3298,3 +3307,6 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems } } +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |