diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 11:08:11 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 11:08:22 -0500 |
commit | ae7434f94a1bc66ee12474414985249a71881b6c (patch) | |
tree | 84e2852eebf4baac995917b9e7f9197c08e4a738 /src/theory/sep | |
parent | 6fa28b63b3345d64de3a1ac55b2e41600c678424 (diff) |
Infer conflicts in strings based on abstracting equality as contains. Minor cleanup.
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 20 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 1 |
2 files changed, 17 insertions, 4 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index d9416fbc6..53fcce26b 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -175,7 +175,7 @@ void TheorySep::preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ) { std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); if( it==d_nil_ref.end() ){ Trace("sep-prereg") << "...set as reference." << std::endl; - d_nil_ref[tn] = t; + setNilRef( tn, t ); }else{ Node nr = it->second; Trace("sep-prereg") << "...reference is " << nr << "." << std::endl; @@ -999,7 +999,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { ss << "__Lb"; TypeNode ltn = NodeManager::currentNM()->mkSetType(tn); //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn)); - Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" ); + Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "base label" ); d_base_label[tn] = n_lbl; //make reference bound Trace("sep") << "Make reference bound label for " << tn << std::endl; @@ -1046,13 +1046,25 @@ Node TheorySep::getNilRef( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); if( it==d_nil_ref.end() ){ Node nil = NodeManager::currentNM()->mkSepNil( tn ); - d_nil_ref[tn] = nil; + setNilRef( tn, nil ); return nil; }else{ return it->second; } } +void TheorySep::setNilRef( TypeNode tn, Node n ) { + Assert( n.getType()==tn ); + d_nil_ref[tn] = n; + /* + //must add unit lemma to ensure nil is always a term in model construction + Node k = NodeManager::currentNM()->mkSkolem( "nk", tn ); + Node eq = NodeManager::currentNM()->mkNode( tn.isBoolean() ? kind::IFF : kind::EQUAL, k, n ); + d_out->lemma( eq ); + */ + //TODO: must not occur in base label +} + Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { Node u; if( locs.empty() ){ @@ -1082,7 +1094,7 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) { ss << "__Lc" << child; TypeNode ltn = NodeManager::currentNM()->mkSetType(refType); //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType)); - Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" ); + Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "sep label" ); d_label_map[atom][lbl][child] = n_lbl; d_label_map_parent[n_lbl] = lbl; return n_lbl; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 85d987cc9..98a4f63c5 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -248,6 +248,7 @@ class TheorySep : public Theory { //get the base label for the spatial assertion Node getBaseLabel( TypeNode tn ); Node getNilRef( TypeNode tn ); + void setNilRef( TypeNode tn, Node n ); Node getLabel( Node atom, int child, Node lbl ); Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ); void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels ); |