diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-28 09:13:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-28 09:13:13 -0500 |
commit | 34e84a25a044e3af192bb69089467c2125911900 (patch) | |
tree | 924a3ae0894bfec136f91949a1bf55e19c4125da /src/theory/quantifiers/term_database.cpp | |
parent | 675e82e32a34911163f9de0e6389eb107be5b0f1 (diff) |
Document term db (#1220)
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206.
* Minor
* Minor
* Change namespace style.
* Address review
* Fix incorrectly merged portion that led to regression failures.
* New clang format, fully document relevant domain.
* Clang format again.
* Minor
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 */ |