diff options
| author | Tim King <taking@google.com> | 2017-03-27 10:24:13 -0700 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2017-03-27 10:24:13 -0700 |
| commit | 4930de53415ffbf614d6965af59b1f44e405451c (patch) | |
| tree | 5fb07f7dfbf7b358c6d79a92d8af6376e33147cf /src/theory/sep | |
| parent | 09d14ac7f81111882327cb168f100e9f998611ac (diff) | |
Making ppNotifyAssertions take a const vector.
Diffstat (limited to 'src/theory/sep')
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 22 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.h | 4 |
2 files changed, 14 insertions, 12 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 4f31f10b5..3f9f70c25 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -881,18 +881,20 @@ TypeNode TheorySep::getDataType( Node n ) { return d_type_data; } -//must process assertions at preprocess so that quantified assertions are processed properly -void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) { - std::map< int, std::map< Node, int > > visited; - std::map< int, std::map< Node, std::vector< Node > > > references; - std::map< int, std::map< Node, bool > > references_strict; - for( unsigned i=0; i<assertions.size(); i++ ){ +// Must process assertions at preprocess so that quantified assertions are +// processed properly. +void TheorySep::ppNotifyAssertions(const std::vector<Node>& assertions) { + std::map<int, std::map<Node, int> > visited; + std::map<int, std::map<Node, std::vector<Node> > > references; + std::map<int, std::map<Node, bool> > references_strict; + for (unsigned i = 0; i < assertions.size(); i++) { Trace("sep-pp") << "Process assertion : " << assertions[i] << std::endl; - processAssertion( assertions[i], visited, references, references_strict, true, true, false ); + processAssertion(assertions[i], visited, references, references_strict, + true, true, false); } - //if data type is unconstrained, assume a fresh uninterpreted sort - if( !d_type_ref.isNull() ){ - if( d_type_data.isNull() ){ + // if data type is unconstrained, assume a fresh uninterpreted sort + if (!d_type_ref.isNull()) { + if (d_type_data.isNull()) { d_type_data = NodeManager::currentNM()->mkSort("_sep_U"); Trace("sep-type") << "Sep: assume data type " << d_type_data << std::endl; d_loc_to_data_type[d_type_ref] = d_type_data; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 816f91c5f..bdbea7e6c 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -79,8 +79,8 @@ class TheorySep : public Theory { PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); Node ppRewrite(TNode atom); - - void ppNotifyAssertions( std::vector< Node >& assertions ); + + void ppNotifyAssertions(const std::vector<Node>& assertions); ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// |