diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-25 15:41:27 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-25 15:41:27 -0500 |
| commit | 2e7ec13174e165cccc74159b5c6590d12894a674 (patch) | |
| tree | b6c8603af05019571671798ac373ffa3e51d3335 /src/theory/sep | |
| parent | dce53c4de6dd7482d9784388cc61753352f241d8 (diff) | |
Minor cleanup preprocessing, add ppNotifyAssertions.
Diffstat (limited to 'src/theory/sep')
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 2 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.h | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index dcba4c379..6735b40de 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -92,7 +92,7 @@ Node TheorySep::ppRewrite(TNode term) { } //must process assertions at preprocess so that quantified assertions are processed properly -void TheorySep::processAssertions( std::vector< Node >& assertions ) { +void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) { d_pp_nils.clear(); std::map< Node, bool > visited; for( unsigned i=0; i<assertions.size(); i++ ){ diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 29e7a008c..ac7ae9cf4 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -75,7 +75,7 @@ class TheorySep : public Theory { PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); Node ppRewrite(TNode atom); - void processAssertions( std::vector< Node >& assertions ); + void ppNotifyAssertions( std::vector< Node >& assertions ); ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// |