diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d4a71e43c..59405a5d5 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -104,6 +104,13 @@ void TermDb::registerQuantifier( Node q ) { } } +unsigned TermDb::getNumOperators() { return d_ops.size(); } +Node TermDb::getOperator(unsigned i) +{ + Assert(i < d_ops.size()); + return d_ops[i]; +} + /** ground terms */ unsigned TermDb::getNumGroundTerms( Node f ) { std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); @@ -178,6 +185,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi Node op = getMatchOperator( n ); Trace("term-db-debug") << " match operator is : " << op << std::endl; + d_ops.push_back(op); d_op_map[op].push_back( n ); added.insert( n ); @@ -720,7 +728,9 @@ void TermDb::setHasTerm( Node n ) { void TermDb::presolve() { if( options::incrementalSolving() ){ - //reset the caches that are SAT context-independent + // reset the caches that are SAT context-independent but user + // context-dependent + d_ops.clear(); d_op_map.clear(); d_type_map.clear(); d_processed.clear(); @@ -969,6 +979,12 @@ void TermDb::computeModelBasisArgAttribute( Node n ){ } } +unsigned TermDb::getModelBasisArg(Node n) +{ + computeModelBasisArgAttribute(n); + return n.getAttribute(ModelBasisArgAttribute()); +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |