summaryrefslogtreecommitdiff
path: root/src/theory/sep/theory_sep.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sep/theory_sep.cpp')
-rw-r--r--src/theory/sep/theory_sep.cpp466
1 files changed, 253 insertions, 213 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index dcba4c379..42c6d1219 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -26,6 +26,7 @@
#include "smt/logic_exception.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/term_database.h"
+#include "options/quantifiers_options.h"
using namespace std;
@@ -35,6 +36,7 @@ namespace sep {
TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
+ d_lemmas_produced_c(u),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true),
d_conflict(c, false),
@@ -45,7 +47,8 @@ TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel
{
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
-
+ d_bounds_init = false;
+
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::SEP_PTO);
//d_equalityEngine.addFunctionKind(kind::SEP_STAR);
@@ -79,47 +82,9 @@ Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
Node TheorySep::ppRewrite(TNode term) {
Trace("sep-pp") << "ppRewrite : " << term << std::endl;
-/*
- Node s_atom = term.getKind()==kind::NOT ? term[0] : term;
- if( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_EMP ){
- //get the reference type (will compute d_type_references)
- int card = 0;
- TypeNode tn = getReferenceType( s_atom, card );
- Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl;
- }
-*/
return term;
}
-//must process assertions at preprocess so that quantified assertions are processed properly
-void TheorySep::processAssertions( std::vector< Node >& assertions ) {
- d_pp_nils.clear();
- std::map< Node, bool > visited;
- for( unsigned i=0; i<assertions.size(); i++ ){
- processAssertion( assertions[i], visited );
- }
-}
-
-void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
- if( visited.find( n )==visited.end() ){
- visited[n] = true;
- if( n.getKind()==kind::SEP_NIL ){
- if( std::find( d_pp_nils.begin(), d_pp_nils.end(), n )==d_pp_nils.end() ){
- d_pp_nils.push_back( n );
- }
- }else if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){
- //get the reference type (will compute d_type_references)
- int card = 0;
- TypeNode tn = getReferenceType( n, card );
- Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl;
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- processAssertion( n[i], visited );
- }
- }
- }
-}
-
Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
return PP_ASSERT_STATUS_UNSOLVED;
@@ -164,43 +129,6 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
}
}
-void TheorySep::preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ) {
- if( visited.find( t )==visited.end() ){
- visited[t] = true;
- Trace("sep-prereg-debug") << "Preregister : " << t << std::endl;
- if( t.getKind()==kind::SEP_NIL ){
- Trace("sep-prereg") << "Preregister nil : " << t << std::endl;
- //per type, all nil variable references are equal
- TypeNode tn = t.getType();
- 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;
- setNilRef( tn, t );
- }else{
- Node nr = it->second;
- Trace("sep-prereg") << "...reference is " << nr << "." << std::endl;
- if( t!=nr ){
- if( d_reduce.find( t )==d_reduce.end() ){
- d_reduce.insert( t );
- Node lem = NodeManager::currentNM()->mkNode( tn.isBoolean() ? kind::IFF : kind::EQUAL, t, nr );
- Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl;
- d_out->lemma( lem );
- }
- }
- }
- }else{
- for( unsigned i=0; i<t.getNumChildren(); i++ ){
- preRegisterTermRec( t[i], visited );
- }
- }
- }
-}
-
-void TheorySep::preRegisterTerm(TNode term){
- std::map< TNode, bool > visited;
- preRegisterTermRec( term, visited );
-}
-
void TheorySep::propagate(Effort e){
@@ -272,14 +200,12 @@ void TheorySep::computeCareGraph() {
/////////////////////////////////////////////////////////////////////////////
-void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel )
-{
+void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){
// Send the equality engine information to the model
m->assertEqualityEngine( &d_equalityEngine );
-
}
-void TheorySep::postProcessModel(TheoryModel* m) {
+void TheorySep::postProcessModel( TheoryModel* m ){
Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
std::vector< Node > sep_children;
@@ -291,11 +217,9 @@ void TheorySep::postProcessModel(TheoryModel* m) {
Assert( d_loc_to_data_type.find( it->first )!=d_loc_to_data_type.end() );
Trace("sep-model") << "Model for heap, type = " << it->first << " with data type " << d_loc_to_data_type[it->first] << " : " << std::endl;
TypeEnumerator te_range( d_loc_to_data_type[it->first] );
- //m->d_comment_str << "Model for heap, type = " << it->first << " : " << std::endl;
computeLabelModel( it->second, d_tmodel );
if( d_label_model[it->second].d_heap_locs_model.empty() ){
Trace("sep-model") << " [empty]" << std::endl;
- //m->d_comment_str << " [empty]" << std::endl;
}else{
for( unsigned j=0; j<d_label_model[it->second].d_heap_locs_model.size(); j++ ){
Assert( d_label_model[it->second].d_heap_locs_model[j].getKind()==kind::SINGLETON );
@@ -304,20 +228,17 @@ void TheorySep::postProcessModel(TheoryModel* m) {
Assert( l.isConst() );
pto_children.push_back( l );
Trace("sep-model") << " " << l << " -> ";
- //m->d_comment_str << " " << l << " -> ";
if( d_pto_model[l].isNull() ){
Trace("sep-model") << "_";
//m->d_comment_str << "_";
pto_children.push_back( *te_range );
}else{
Trace("sep-model") << d_pto_model[l];
- //m->d_comment_str << d_pto_model[l];
Node vpto = d_valuation.getModel()->getRepresentative( d_pto_model[l] );
Assert( vpto.isConst() );
pto_children.push_back( vpto );
}
Trace("sep-model") << std::endl;
- //m->d_comment_str << std::endl;
sep_children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_PTO, pto_children ) );
}
}
@@ -326,8 +247,6 @@ void TheorySep::postProcessModel(TheoryModel* m) {
m_neq = NodeManager::currentNM()->mkNode( nil.getType().isBoolean() ? kind::IFF : kind::EQUAL, nil, vnil );
Trace("sep-model") << "sep.nil = " << vnil << std::endl;
Trace("sep-model") << std::endl;
- //m->d_comment_str << "sep.nil = " << vnil << std::endl;
- //m->d_comment_str << std::endl;
if( sep_children.empty() ){
TypeEnumerator te_domain( it->first );
m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain );
@@ -337,8 +256,6 @@ void TheorySep::postProcessModel(TheoryModel* m) {
m_heap = NodeManager::currentNM()->mkNode( kind::SEP_STAR, sep_children );
}
m->setHeapModel( m_heap, m_neq );
- //m->d_comment_str << m->d_sep_heap << std::endl;
- //m->d_comment_str << m->d_sep_nil_eq << std::endl;
}
Trace("sep-model") << "Finished printing model for TheorySep." << std::endl;
}
@@ -351,13 +268,6 @@ void TheorySep::postProcessModel(TheoryModel* m) {
void TheorySep::presolve() {
Trace("sep-pp") << "Presolving" << std::endl;
//TODO: cleanup if incremental?
-
- //we must preregister all instances of sep.nil to ensure they are made equal
- for( unsigned i=0; i<d_pp_nils.size(); i++ ){
- std::map< TNode, bool > visited;
- preRegisterTermRec( d_pp_nils[i], visited );
- }
- d_pp_nils.clear();
}
@@ -401,9 +311,8 @@ void TheorySep::check(Effort e) {
Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl;
d_reduce.insert( fact );
//introduce top-level label, add iff
- int card;
- TypeNode refType = getReferenceType( s_atom, card );
- Trace("sep-lemma-debug") << "...reference type is : " << refType << ", card is " << card << std::endl;
+ TypeNode refType = getReferenceType( s_atom );
+ Trace("sep-lemma-debug") << "...reference type is : " << refType << std::endl;
Node b_lbl = getBaseLabel( refType );
Node s_atom_new = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, s_atom, b_lbl );
Node lem;
@@ -428,44 +337,9 @@ void TheorySep::check(Effort e) {
if( s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND ){
std::vector< Node > children;
std::vector< Node > c_lems;
- int card;
- TypeNode tn = getReferenceType( s_atom, card );
+ TypeNode tn = getReferenceType( s_atom );
Assert( d_reference_bound.find( tn )!=d_reference_bound.end() );
c_lems.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, s_lbl, d_reference_bound[tn] ) );
- if( options::sepPreciseBound() ){
- //more precise bound
- Trace("sep-bound") << "Propagate Bound(" << s_lbl << ") = ";
- Assert( d_lbl_reference_bound.find( s_lbl )!=d_lbl_reference_bound.end() );
- for( unsigned j=0; j<d_lbl_reference_bound[s_lbl].size(); j++ ){
- Trace("sep-bound") << d_lbl_reference_bound[s_lbl][j] << " ";
- }
- Trace("sep-bound") << std::endl << " to children of " << s_atom << std::endl;
- //int rb_start = 0;
- for( unsigned j=0; j<s_atom.getNumChildren(); j++ ){
- int ccard = 0;
- getReferenceType( s_atom, ccard, j );
- Node c_lbl = getLabel( s_atom, j, s_lbl );
- Trace("sep-bound") << " for " << c_lbl << ", card = " << ccard << " : ";
- std::vector< Node > bound_loc;
- bound_loc.insert( bound_loc.end(), d_references[s_atom][j].begin(), d_references[s_atom][j].end() );
-/* //this is unsound
- for( int k=0; k<ccard; k++ ){
- Assert( rb_start<(int)d_lbl_reference_bound[s_lbl].size() );
- d_lbl_reference_bound[c_lbl].push_back( d_lbl_reference_bound[s_lbl][rb_start] );
- Trace("sep-bound") << d_lbl_reference_bound[s_lbl][rb_start] << " ";
- bound_loc.push_back( d_lbl_reference_bound[s_lbl][rb_start] );
- rb_start++;
- }
-*/
- //carry all locations for now
- bound_loc.insert( bound_loc.end(), d_lbl_reference_bound[s_lbl].begin(), d_lbl_reference_bound[s_lbl].end() );
- Trace("sep-bound") << std::endl;
- Node bound_v = mkUnion( tn, bound_loc );
- Trace("sep-bound") << " ...bound value : " << bound_v << std::endl;
- children.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, c_lbl, bound_v ) );
- }
- Trace("sep-bound") << "Done propagate Bound(" << s_lbl << ")" << std::endl;
- }
std::vector< Node > labels;
getLabelChildren( s_atom, s_lbl, children, labels );
Node empSet = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType()));
@@ -568,13 +442,9 @@ void TheorySep::check(Effort e) {
Trace("sep-assert") << "Done asserting " << atom << " to EE." << std::endl;
}else if( s_atom.getKind()==kind::SEP_PTO ){
Node pto_lbl = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] );
- if( polarity && s_lbl!=pto_lbl ){
- //also propagate equality
- Node eq = s_lbl.eqNode( pto_lbl );
- Trace("sep-assert") << "Asserting implied equality " << eq << " to EE..." << std::endl;
- d_equalityEngine.assertEquality(eq, true, fact);
- Trace("sep-assert") << "Done asserting implied equality " << eq << " to EE." << std::endl;
- }
+ Assert( s_lbl==pto_lbl );
+ Trace("sep-assert") << "Asserting " << s_atom << std::endl;
+ d_equalityEngine.assertPredicate(s_atom, polarity, fact);
//associate the equivalence class of the lhs with this pto
Node r = getRepresentative( s_lbl );
HeapAssertInfo * ei = getOrMakeEqcInfo( r, true );
@@ -595,6 +465,7 @@ void TheorySep::check(Effort e) {
d_tmodel.clear();
d_pto_model.clear();
Trace("sep-process") << "---Locations---" << std::endl;
+ std::map< Node, int > min_id;
for( std::map< TypeNode, std::vector< Node > >::iterator itt = d_type_references_all.begin(); itt != d_type_references_all.end(); ++itt ){
for( unsigned k=0; k<itt->second.size(); k++ ){
Node t = itt->second[k];
@@ -602,7 +473,19 @@ void TheorySep::check(Effort e) {
if( d_valuation.getModel()->hasTerm( t ) ){
Node v = d_valuation.getModel()->getRepresentative( t );
Trace("sep-process") << v << std::endl;
- d_tmodel[v] = t;
+ //take minimal id
+ std::map< Node, unsigned >::iterator itrc = d_type_ref_card_id.find( t );
+ int tid = itrc==d_type_ref_card_id.end() ? -1 : (int)itrc->second;
+ bool set_term_model;
+ if( d_tmodel.find( v )==d_tmodel.end() ){
+ set_term_model = true;
+ }else{
+ set_term_model = min_id[v]>tid;
+ }
+ if( set_term_model ){
+ d_tmodel[v] = t;
+ min_id[v] = tid;
+ }
}else{
Trace("sep-process") << "?" << std::endl;
}
@@ -737,8 +620,7 @@ void TheorySep::check(Effort e) {
//add refinement lemma
if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){
needAddLemma = true;
- int card;
- TypeNode tn = getReferenceType( s_atom, card );
+ TypeNode tn = getReferenceType( s_atom );
tn = NodeManager::currentNM()->mkSetType(tn);
//tn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
Node o_b_lbl_mval = d_label_model[s_lbl].getValue( tn );
@@ -885,17 +767,62 @@ TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) {
}
}
-TypeNode TheorySep::getReferenceType( Node atom, int& card, int index ) {
- Trace("sep-type") << "getReference type " << atom << " " << index << std::endl;
+//for now, assume all constraints are for the same heap type (ensured by logic exceptions thrown in computeReferenceType2)
+TypeNode TheorySep::getReferenceType( Node n ) {
+ Assert( !d_type_ref.isNull() );
+ return d_type_ref;
+}
+
+TypeNode TheorySep::getDataType( Node n ) {
+ Assert( !d_type_data.isNull() );
+ 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< Node, bool > visited;
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ Trace("sep-pp") << "Process assertion : " << assertions[i] << std::endl;
+ processAssertion( assertions[i], visited );
+ }
+ //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;
+ }
+ }
+}
+
+void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ Trace("sep-pp-debug") << "process assertion : " << n << std::endl;
+ if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){
+ //get the reference type (will compute d_type_references)
+ int card = 0;
+ TypeNode tn = computeReferenceType( n, card );
+ Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl;
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ processAssertion( n[i], visited );
+ }
+ }
+ }
+}
+
+TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) {
+ Trace("sep-pp-debug") << "getReference type " << atom << " " << index << std::endl;
Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::SEP_EMP || index!=-1 );
std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index );
if( it==d_reference_type[atom].end() ){
card = 0;
- TypeNode tn;
+ TypeNode tn;
if( index==-1 && ( atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND ) ){
for( unsigned i=0; i<atom.getNumChildren(); i++ ){
int cardc = 0;
- TypeNode ctn = getReferenceType( atom, cardc, i );
+ TypeNode ctn = computeReferenceType( atom, cardc, i );
if( !ctn.isNull() ){
tn = ctn;
}
@@ -910,7 +837,7 @@ TypeNode TheorySep::getReferenceType( Node atom, int& card, int index ) {
Node n = index==-1 ? atom : atom[index];
//will compute d_references as well
std::map< Node, int > visited;
- tn = getReferenceType2( atom, card, index, n, visited );
+ tn = computeReferenceType2( atom, card, index, n, visited );
}
if( tn.isNull() && index==-1 ){
tn = NodeManager::currentNM()->booleanType();
@@ -940,9 +867,9 @@ TypeNode TheorySep::getReferenceType( Node atom, int& card, int index ) {
}
}
-TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited ) {
+TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited ) {
if( visited.find( n )==visited.end() ){
- Trace("sep-type-debug") << "visit : " << n << " : " << atom << " " << index << std::endl;
+ Trace("sep-pp-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
@@ -951,44 +878,34 @@ TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n,
TypeNode tn1 = n[0].getType();
TypeNode tn2 = n[1].getType();
if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){
- d_reference_bound_invalid[tn1] = true;
+ if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){
+ // still valid : bound on heap models will include Herbrand universe of n[0].getType()
+ d_reference_bound_fv[tn1] = true;
+ }else{
+ d_reference_bound_invalid[tn1] = true;
+ Trace("sep-bound") << "reference cannot be bound (due to quantified pto)." << std::endl;
+ }
}else{
if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), n[0] )==d_references[atom][index].end() ){
d_references[atom][index].push_back( n[0] );
}
}
- 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{
- if( itt->second!=tn2 ){
- std::stringstream ss;
- ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl;
- throw LogicException(ss.str());
- Assert( false );
- }
- }
+ registerRefDataTypes( tn1, tn2, atom );
card = 1;
visited[n] = card;
return tn1;
- //return n[1].getType();
}else if( n.getKind()==kind::SEP_EMP ){
+ TypeNode tn = n[0].getType();
+ TypeNode tnd;
+ registerRefDataTypes( tn, tnd, atom );
card = 1;
visited[n] = card;
- return n[0].getType();
+ return tn;
}else if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){
Assert( n!=atom );
//get the references
card = 0;
- TypeNode tn = getReferenceType( n, card );
+ TypeNode tn = computeReferenceType( n, card );
for( unsigned j=0; j<d_references[n][-1].size(); j++ ){
if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), d_references[n][-1][j] )==d_references[atom][index].end() ){
d_references[atom][index].push_back( d_references[n][-1][j] );
@@ -996,12 +913,17 @@ TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n,
}
visited[n] = card;
return tn;
+ }else if( n.getKind()==kind::SEP_NIL ){
+ TypeNode tn = n.getType();
+ TypeNode tnd;
+ registerRefDataTypes( tn, tnd, n );
+ return tn;
}else{
card = 0;
TypeNode otn;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
int cardc = 0;
- TypeNode tn = getReferenceType2( atom, cardc, index, n[i], visited );
+ TypeNode tn = computeReferenceType2( atom, cardc, index, n[i], visited );
if( !tn.isNull() ){
otn = tn;
}
@@ -1016,27 +938,108 @@ TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n,
return TypeNode::null();
}
}
-/*
-int TheorySep::getCardinality( Node n, std::vector< Node >& refs ) {
- std::map< Node, int > visited;
- return getCardinality2( n, refs, visited );
+void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){
+ //separation logic is effectively enabled when we find at least one spatial constraint occurs in the input
+ if( options::incrementalSolving() ){
+ std::stringstream ss;
+ ss << "ERROR: cannot use separation logic in incremental mode." << std::endl;
+ throw LogicException(ss.str());
+ }
+ 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 );
+ }
+ if( tn2.isNull() ){
+ Trace("sep-type") << "Sep: assume location type " << tn1 << " (from " << atom << ")" << std::endl;
+ }else{
+ 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;
+ //for now, we only allow heap constraints of one type
+ d_type_ref = tn1;
+ d_type_data = tn2;
+ }else{
+ if( !tn2.isNull() ){
+ if( itt->second!=tn2 ){
+ if( itt->second.isNull() ){
+ Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
+ //now we know data type
+ d_loc_to_data_type[tn1] = tn2;
+ d_type_data = tn2;
+ }else{
+ std::stringstream ss;
+ ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl;
+ throw LogicException(ss.str());
+ Assert( false );
+ }
+ }
+ }
+ }
}
-int TheorySep::getCardinality2( Node n, std::vector< Node >& refs, std::map< Node, int >& visited ) {
- std::map< Node, int >::iterator it = visited.find( n );
- if( it!=visited.end() ){
- return it->second;
- }else{
-
-
+void TheorySep::initializeBounds() {
+ if( !d_bounds_init ){
+ Trace("sep-bound") << "Initialize sep bounds..." << std::endl;
+ d_bounds_init = true;
+ for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){
+ TypeNode tn = it->first;
+ Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl;
+ QuantEPR * qepr = getLogicInfo().isQuantified() ? getQuantifiersEngine()->getQuantEPR() : NULL;
+ //if pto had free variable reference
+ if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
+ if( d_reference_bound_fv.find( tn )!=d_reference_bound_fv.end() ){
+ //include Herbrand universe of tn
+ if( qepr && qepr->isEPR( tn ) ){
+ for( unsigned j=0; j<qepr->d_consts[tn].size(); j++ ){
+ Node k = qepr->d_consts[tn][j];
+ if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), k )==d_type_references[tn].end() ){
+ d_type_references[tn].push_back( k );
+ }
+ }
+ }else{
+ d_reference_bound_invalid[tn] = true;
+ Trace("sep-bound") << "reference cannot be bound (due to non-EPR variable)." << std::endl;
+ }
+ }
+ }
+ unsigned n_emp = 0;
+ if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
+ n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()];
+ }else if( d_type_references[tn].empty() ){
+ //must include at least one constant
+ n_emp = 1;
+ }
+ Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl;
+ for( unsigned r=0; r<n_emp; r++ ){
+ Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
+ d_type_references_card[tn].push_back( e );
+ d_type_ref_card_id[e] = r;
+ //must include this constant back into EPR handling
+ if( qepr && qepr->isEPR( tn ) ){
+ qepr->addEPRConstant( tn, e );
+ }
+ }
+ //EPR must include nil ref
+ if( qepr && qepr->isEPR( tn ) ){
+ Node nr = getNilRef( tn );
+ if( !qepr->isEPRConstant( tn, nr ) ){
+ qepr->addEPRConstant( tn, nr );
+ }
+ }
+ }
}
}
-*/
Node TheorySep::getBaseLabel( TypeNode tn ) {
std::map< TypeNode, Node >::iterator it = d_base_label.find( tn );
if( it==d_base_label.end() ){
+ initializeBounds();
Trace("sep") << "Make base label for " << tn << std::endl;
std::stringstream ss;
ss << "__Lb";
@@ -1050,35 +1053,62 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
ss2 << "__Lu";
d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" );
d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() );
+
+ //check whether monotonic (elements can be added to tn without effecting satisfiability)
+ bool tn_is_monotonic = true;
+ if( tn.isSort() ){
+ //TODO: use monotonicity inference
+ tn_is_monotonic = !getLogicInfo().isQuantified();
+ }else{
+ tn_is_monotonic = tn.getCardinality().isInfinite();
+ }
//add a reference type for maximum occurrences of empty in a constraint
- unsigned n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()];
- for( unsigned r=0; r<n_emp; r++ ){
- Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
- //d_type_references_all[tn].push_back( NodeManager::currentNM()->mkSkolem( "e", NodeManager::currentNM()->mkRefType(tn) ) );
- if( options::sepDisequalC() ){
+ if( options::sepDisequalC() && tn_is_monotonic ){
+ for( unsigned r=0; r<d_type_references_card[tn].size(); r++ ){
+ Node e = d_type_references_card[tn][r];
//ensure that it is distinct from all other references so far
for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
Node eq = NodeManager::currentNM()->mkNode( e.getType().isBoolean() ? kind::IFF : kind::EQUAL, e, d_type_references_all[tn][j] );
d_out->lemma( eq.negate() );
}
+ d_type_references_all[tn].push_back( e );
}
- d_type_references_all[tn].push_back( e );
- d_lbl_reference_bound[d_base_label[tn]].push_back( e );
+ }else{
+ //break symmetries TODO
+
+ d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() );
}
- //construct bound
- d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
- Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
+ Assert( !d_type_references_all[tn].empty() );
+
+ if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
+ //construct bound
+ d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
+ Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
- if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
Node slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_reference_bound[tn], d_reference_bound_max[tn] );
Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl;
d_out->lemma( slem );
- }else{
- Trace("sep-bound") << "reference cannot be bound (possibly due to quantified pto)." << std::endl;
+ //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
+ //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
+ //d_out->lemma( slem );
+
+ //symmetry breaking
+ std::map< unsigned, Node > lit_mem_map;
+ for( unsigned i=0; i<d_type_references_card[tn].size(); i++ ){
+ lit_mem_map[i] = NodeManager::currentNM()->mkNode( kind::MEMBER, d_type_references_card[tn][i], d_reference_bound[tn]);
+ }
+ for( unsigned i=0; i<(d_type_references_card[tn].size()-1); i++ ){
+ std::vector< Node > children;
+ for( unsigned j=(i+1); j<d_type_references_card[tn].size(); j++ ){
+ children.push_back( lit_mem_map[j].negate() );
+ }
+ Assert( !children.empty() );
+ Node sym_lem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children );
+ sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, lit_mem_map[i].negate(), sym_lem );
+ Trace("sep-lemma") << "Sep::Lemma: symmetry breaking lemma : " << sym_lem << std::endl;
+ d_out->lemma( sym_lem );
+ }
}
- //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
- //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
- //d_out->lemma( slem );
//assert that nil ref is not in base label
Node nr = getNilRef( tn );
@@ -1095,7 +1125,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
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 );
+ Node nil = NodeManager::currentNM()->mkUniqueVar( tn, kind::SEP_NIL );
setNilRef( tn, nil );
return nil;
}else{
@@ -1132,7 +1162,7 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child );
if( it==d_label_map[atom][lbl].end() ){
int card;
- TypeNode refType = getReferenceType( atom, card );
+ TypeNode refType = computeReferenceType( atom, card );
std::stringstream ss;
ss << "__Lc" << child;
TypeNode ltn = NodeManager::currentNM()->mkSetType(refType);
@@ -1372,7 +1402,6 @@ void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) {
Assert( false );
}
}
- //end hack
for( unsigned j=0; j<d_label_model[lbl].d_heap_locs_model.size(); j++ ){
Node u = d_label_model[lbl].d_heap_locs_model[j];
Assert( u.getKind()==kind::SINGLETON );
@@ -1386,7 +1415,8 @@ void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) {
//TypeNode tn = u.getType().getRefConstituentType();
TypeNode tn = u.getType();
Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << ", cref type " << tn << std::endl;
- Assert( d_type_references_all.find( tn )!=d_type_references_all.end() && !d_type_references_all[tn].empty() );
+ Assert( d_type_references_all.find( tn )!=d_type_references_all.end() );
+ Assert( !d_type_references_all[tn].empty() );
tt = d_type_references_all[tn][0];
}else{
tt = itm->second;
@@ -1489,7 +1519,11 @@ void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity )
Assert( areEqual( pb[1], p[1] ) );
std::vector< Node > exp;
if( pb[1]!=p[1] ){
+ //if( pb[1].getKind()==kind::SINGLETON && p[1].getKind()==kind::SINGLETON ){
+ // exp.push_back( pb[1][0].eqNode( p[1][0] ) );
+ //}else{
exp.push_back( pb[1].eqNode( p[1] ) );
+ //}
}
exp.push_back( pb );
exp.push_back( p.negate() );
@@ -1497,10 +1531,12 @@ void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity )
if( pb[0][1]!=p[0][1] ){
conc.push_back( pb[0][1].eqNode( p[0][1] ).negate() );
}
- if( pb[1]!=p[1] ){
- conc.push_back( pb[1].eqNode( p[1] ).negate() );
- }
+ //if( pb[1]!=p[1] ){
+ // conc.push_back( pb[1].eqNode( p[1] ).negate() );
+ //}
Node n_conc = conc.empty() ? d_false : ( conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::OR, conc ) );
+ Trace("sep-pto") << "Conclusion is " << n_conc << std::endl;
+ // propagation for (pto x y) ^ ~(pto z w) ^ x = z => y != w
sendLemma( exp, n_conc, "PTO_NEG_PROP" );
}
}else{
@@ -1525,6 +1561,7 @@ void TheorySep::mergePto( Node p1, Node p2 ) {
}
exp.push_back( p1 );
exp.push_back( p2 );
+ //enforces injectiveness of pto : (pto x y) ^ (pto y w) ^ x = y => y = w
sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" );
}
}
@@ -1598,8 +1635,11 @@ void TheorySep::doPendingFacts() {
}
int index = d_pending_lem[i];
Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, d_pending_exp[index], d_pending[index] );
- d_out->lemma( lem );
- Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl;
+ if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
+ d_lemmas_produced_c.insert( lem );
+ d_out->lemma( lem );
+ Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl;
+ }
}
}
d_pending_exp.clear();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback