From 442c809911bcc45ae45dc97650146c459a841ea3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 12 Sep 2016 13:43:02 -0500 Subject: [PATCH] Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking in theory sep. --- src/expr/expr_manager_template.cpp | 4 +- src/expr/node_manager.cpp | 23 ++++++------ src/expr/node_manager.h | 6 ++- src/theory/sep/theory_sep.cpp | 47 +++++++++++------------- src/theory/sep/theory_sep.h | 2 - test/regress/regress0/sep/Makefile.am | 3 +- test/regress/regress0/sep/dispose-1.smt2 | 17 +++++++++ 7 files changed, 59 insertions(+), 43 deletions(-) create mode 100644 test/regress/regress0/sep/dispose-1.smt2 diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 2dc3aebe5..aa5634e7a 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -943,7 +943,9 @@ Expr ExprManager::mkBoundVar(Type type) { Expr ExprManager::mkSepNil(Type type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode)); + Node n = d_nodeManager->mkSepNil(*type.d_typeNode); + return n.toExpr(); + //return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode)); } Expr ExprManager::mkAssociative(Kind kind, diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index d2ac7e2a1..94b136c46 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -169,6 +169,8 @@ NodeManager::~NodeManager() { for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { d_operators[i] = Node::null(); } + + d_sep_nils.clear(); //d_tupleAndRecordTypes.clear(); d_tt_cache.d_children.clear(); @@ -682,17 +684,16 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { } Node NodeManager::mkSepNil(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::SEP_NIL); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); - return n; -} - -Node* NodeManager::mkSepNilPtr(const TypeNode& type) { - Node* n = NodeBuilder<0>(this, kind::SEP_NIL).constructNodePtr(); - setAttribute(*n, TypeAttr(), type); - setAttribute(*n, TypeCheckedAttr(), true); - return n; + std::map< TypeNode, Node >::iterator it = d_sep_nils.find( type ); + if( it==d_sep_nils.end() ){ + Node n = NodeBuilder<0>(this, kind::SEP_NIL); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + d_sep_nils[type] = n; + return n; + }else{ + return it->second; + } } Node NodeManager::mkAbstractValue(const TypeNode& type) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index dcd7005f8..79c7320f7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -157,6 +157,9 @@ class NodeManager { * plusOperator->getConst(), you get kind::PLUS back. */ Node d_operators[kind::LAST_KIND]; + + /** sep nil per type */ + std::map< TypeNode, Node > d_sep_nils; /** * A list of subscribers for NodeManager events. @@ -487,9 +490,8 @@ public: /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); - /** Create nil reference for separation logic with the given type. */ + /** Create nil reference for separation logic with the given type (unique per type). */ Node mkSepNil(const TypeNode& type); - Node* mkSepNilPtr(const TypeNode& type); /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index eefc0e779..fcf5ec88d 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -267,20 +267,6 @@ void TheorySep::postProcessModel( TheoryModel* m ){ void TheorySep::presolve() { Trace("sep-pp") << "Presolving" << std::endl; //TODO: cleanup if incremental? - - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_pp_nils.begin(); it != d_pp_nils.end(); ++it ){ - Trace("sep-pp") << it->second.size() << " nil references of type " << it->first << std::endl; - if( !it->second.empty() ){ - setNilRef( it->first, it->second[0] ); - //ensure all instances of sep.nil are made equal - for( unsigned i=1; isecond.size(); i++ ){ - Node lem = NodeManager::currentNM()->mkNode( it->first.isBoolean() ? kind::IFF : kind::EQUAL, it->second[i], it->second[0] ); - Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl; - d_out->lemma( lem ); - } - } - } - d_pp_nils.clear(); } @@ -784,7 +770,6 @@ TypeNode TheorySep::getDataType( Node n ) { //must process assertions at preprocess so that quantified assertions are processed properly void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) { - d_pp_nils.clear(); std::map< Node, bool > visited; for( unsigned i=0; i& assertions ) { 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 ){ - TypeNode tn = n.getType(); - if( std::find( d_pp_nils[tn].begin(), d_pp_nils[tn].end(), n )==d_pp_nils[tn].end() ){ - d_pp_nils[tn].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 ){ + 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 ); @@ -822,7 +803,7 @@ void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) { } TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) { - Trace("sep-type") << "getReference type " << atom << " " << index << std::endl; + 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() ){ @@ -878,7 +859,7 @@ TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) { 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 @@ -926,9 +907,6 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node TypeNode tn = n.getType(); TypeNode tnd; registerRefDataTypes( tn, tnd, n ); - if( std::find( d_pp_nils[tn].begin(), d_pp_nils[tn].end(), n )==d_pp_nils[tn].end() ){ - d_pp_nils[tn].push_back( n ); - } return tn; }else{ card = 0; @@ -1095,6 +1073,23 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { //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; imkNode( 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); jmkNode( 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 ); + } } //assert that nil ref is not in base label diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 4f60c5781..a7ca3aff3 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -53,8 +53,6 @@ class TheorySep : public Theory { //whether bounds have been initialized bool d_bounds_init; - - std::map< TypeNode, std::vector< Node > > d_pp_nils; Node mkAnd( std::vector< TNode >& assumptions ); diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 7bcd700bd..b43a9a570 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -57,7 +57,8 @@ TESTS = \ trees-1.smt2 \ wand-false.smt2 \ dup-nemp.smt2 \ - emp2-quant-unsat.smt2 + emp2-quant-unsat.smt2 \ + dispose-1.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2 new file mode 100644 index 000000000..3c0e7df32 --- /dev/null +++ b/test/regress/regress0/sep/dispose-1.smt2 @@ -0,0 +1,17 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const w Int) +(declare-const w1 Int) +(declare-const w2 Int) + +;------- f ------- +(assert (= w1 (as sep.nil Int))) +(assert (= w2 (as sep.nil Int))) +;----------------- + +(assert (pto w (as sep.nil Int))) +(assert (not (and (sep (and (emp 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true)))) + +(check-sat) +;(get-model) -- 2.30.2