diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
commit | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (patch) | |
tree | a79f142c5b6fbeaec34978f8da2b2db308a33e79 /src/theory/quantifiers/term_database.cpp | |
parent | 5b4c416608bda1df62e1ffe7131648a89882ddc7 (diff) |
cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 493b9e931..d637fa25f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -144,7 +144,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ computeModelBasisArgAttribute( n ); if( !n.getAttribute(NoMatchAttribute()) ){ if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){ - //only set no match if not a model basis argument term NoMatchAttribute nma; n.setAttribute(nma,true); congruentCount++; @@ -171,7 +170,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( !en.getAttribute(NoMatchAttribute()) ){ Node op = en.getOperator(); if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ - //only set no match if not a model basis argument term NoMatchAttribute nma; en.setAttribute(nma,true); congruentCount++; |