diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-22 10:59:16 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-22 10:59:16 -0500 |
| commit | e131c151279dc90063b999d229cc27bc45aa5211 (patch) | |
| tree | 98965dc4b1fa2efc20ef09fb275359dd15a7fac1 /src/theory/sep | |
| parent | b5956e457da61e4d49cd35e0a73ba423230a25e0 (diff) | |
Minor, error handling for polymorphism + sep logic.
Diffstat (limited to 'src/theory/sep')
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index f4c3a712e..dcba4c379 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -945,6 +945,9 @@ TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n, Trace("sep-type-debug") << "visit : " << n << " : " << atom << " " << index << std::endl; visited[n] = -1; if( n.getKind()==kind::SEP_PTO ){ + //TODO: when THEORY_SETS supports mixed Int/Real sets + //TypeNode tn1 = n[0].getType().getBaseType(); + //TypeNode tn2 = n[1].getType().getBaseType(); TypeNode tn1 = n[0].getType(); TypeNode tn2 = n[1].getType(); if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){ @@ -956,6 +959,13 @@ TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n, } std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 ); if( itt==d_loc_to_data_type.end() ){ + if( !d_loc_to_data_type.empty() ){ + TypeNode te1 = d_loc_to_data_type.begin()->first; + std::stringstream ss; + ss << "ERROR: specifying heap constraints for two different types : " << tn1 << " -> " << tn2 << " and " << te1 << " -> " << d_loc_to_data_type[te1] << std::endl; + throw LogicException(ss.str()); + Assert( false ); + } Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl; d_loc_to_data_type[tn1] = tn2; }else{ |