diff options
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 3add7a9d7..a2a2e99c6 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -295,6 +295,11 @@ void RewriteEngine::assertNode( Node n ) { } +bool RewriteEngine::checkCompleteFor( Node q ) { + // by semantics of rewrite rules, saturation -> SAT + return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end(); +} + Node RewriteEngine::getInstConstNode( Node n, Node q ) { std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n ); if( it==d_inst_const_node[q].end() ){ |