diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-12 14:25:25 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-12 14:25:25 -0500 |
commit | 8b41e8d8128752eba75f32f751ec9c095a6b1d87 (patch) | |
tree | 68559af9be49966dedfa877b124f76d3af152b7b /src/theory/quantifiers/term_database.cpp | |
parent | 15d36d99363b4ee20754498b566bd315150953fc (diff) |
Work on array pf signature, add working example. Add quantifiers proof signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 29 |
1 files changed, 26 insertions, 3 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 08a9f5d9f..ea1231e7a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -46,6 +46,20 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ } } +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) { + +} + +/** ground terms */ +unsigned TermDb::getNumGroundTerms( Node f ) { + std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); + if( it!=d_op_map.end() ){ + return it->second.size(); + }else{ + return 0; + } + //return d_op_ccount[f]; +} Node TermDb::getOperator( Node n ) { //return n.getOperator(); @@ -89,6 +103,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Trace("term-db") << "register term in db " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; Node op = getOperator( n ); + /* + int occ = d_op_ccount[op]; + if( occ<(int)d_op_map[op].size() ){ + d_op_map[op][occ] = n; + }else{ + d_op_map[op].push_back( n ); + } + d_op_ccount[op].set( occ + 1 ); + */ d_op_map[op].push_back( n ); added.insert( n ); @@ -120,7 +143,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ int alreadyCongruentCount = 0; //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - d_op_count[ it->first ] = 0; + d_op_nonred_count[ it->first ] = 0; if( !it->second.empty() ){ if( it->second[0].getType().isBoolean() ){ d_pred_map_trie[ 0 ][ it->first ].d_data.clear(); @@ -138,7 +161,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ congruentCount++; }else{ nonCongruentCount++; - d_op_count[ it->first ]++; + d_op_nonred_count[ it->first ]++; } }else{ congruentCount++; @@ -166,7 +189,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ congruentCount++; }else{ nonCongruentCount++; - d_op_count[ op ]++; + d_op_nonred_count[ op ]++; } }else{ alreadyCongruentCount++; |