diff options
Diffstat (limited to 'src/theory/sep/theory_sep.cpp')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 38 |
1 files changed, 31 insertions, 7 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 1b25bb0f4..4a7f4367e 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -102,6 +102,15 @@ void TheorySep::finishInit() // we could but don't do congruence on SEP_STAR here. } +void TheorySep::preRegisterTerm(TNode n) +{ + Kind k = n.getKind(); + if (k == SEP_PTO || k == SEP_EMP || k == SEP_STAR || k == SEP_WAND) + { + registerRefDataTypesAtom(n); + } +} + Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) { if( assumptions.empty() ){ return d_true; @@ -1009,9 +1018,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& if( it==visited[index].end() ){ Trace("sep-pp-debug") << "process assertion : " << n << ", index = " << index << std::endl; if( n.getKind()==kind::SEP_EMP ){ - TypeNode tn = n[0].getType(); - TypeNode tnd = n[1].getType(); - registerRefDataTypes( tn, tnd, n ); + registerRefDataTypesAtom(n); if( hasPol && pol ){ references[index][n].clear(); references_strict[index][n] = true; @@ -1019,10 +1026,9 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& card = 1; } }else if( n.getKind()==kind::SEP_PTO ){ - TypeNode tn1 = n[0].getType(); - TypeNode tn2 = n[1].getType(); - registerRefDataTypes( tn1, tn2, n ); + registerRefDataTypesAtom(n); if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){ + TypeNode tn1 = n[0].getType(); if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){ if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){ // still valid : bound on heap models will include Herbrand universe of n[0].getType() @@ -1133,7 +1139,25 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& return card; } -void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){ +void TheorySep::registerRefDataTypesAtom(Node atom) +{ + TypeNode tn1; + TypeNode tn2; + Kind k = atom.getKind(); + if (k == SEP_PTO || k == SEP_EMP) + { + tn1 = atom[0].getType(); + tn2 = atom[1].getType(); + } + else + { + Assert(k == SEP_STAR || k == SEP_WAND); + } + registerRefDataTypes(tn1, tn2, atom); +} + +void TheorySep::registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom) +{ if (!d_type_ref.isNull()) { Assert(!atom.isNull()); |