From bd284aa3cbe8960937e8ed8f140b12b3f5a446d3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 9 Aug 2016 13:11:07 -0500 Subject: [PATCH] Fixes for sep star rewrite. --- src/theory/sep/theory_sep_rewriter.cpp | 22 ++++++++-------------- test/regress/regress0/sep/Makefile.am | 3 ++- test/regress/regress0/sep/dup-nemp.smt2 | 7 +++++++ 3 files changed, 17 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress0/sep/dup-nemp.smt2 diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index d58c2c13d..3e74bd61e 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -24,6 +24,7 @@ namespace sep { void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ){ Assert( n.getKind()==kind::SEP_STAR ); + Node tr = NodeManager::currentNM()->mkConst( true ); for( unsigned i=0; i& s_children getAndChildren( n[i], temp_s_children, ns_children ); Node to_add; if( temp_s_children.size()==0 ){ - to_add = NodeManager::currentNM()->mkConst( true ); - }else{ - //remove empty star - std::vector< Node > temp_s_children2; - for( unsigned i=0; i1 ){ - to_add = NodeManager::currentNM()->mkNode( kind::AND, temp_s_children2 ); + if( std::find( s_children.begin(), s_children.end(), tr )==s_children.end() ){ + to_add = tr; } + }else if( temp_s_children.size()==1 ){ + to_add = temp_s_children[0]; + }else{ + to_add = NodeManager::currentNM()->mkNode( kind::AND, temp_s_children ); } if( !to_add.isNull() ){ //flatten star if( to_add.getKind()==kind::SEP_STAR ){ getStarChildren( to_add, s_children, ns_children ); - }else if( std::find( s_children.begin(), s_children.end(), to_add )==s_children.end() ){ + }else if( to_add.getKind()!=kind::SEP_EMP || s_children.empty() ){ //remove sep emp s_children.push_back( to_add ); } } diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index d72e02d97..6078bfa19 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -55,7 +55,8 @@ TESTS = \ quant_wand.smt2 \ fmf-nemp-2.smt2 \ trees-1.smt2 \ - wand-false.smt2 + wand-false.smt2 \ + dup-nemp.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 new file mode 100644 index 000000000..009561128 --- /dev/null +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-sort Loc 0) +(declare-const l Loc) +(assert (sep (not (emp l)) (not (emp l)))) +(assert (pto l l)) +(check-sat) -- 2.30.2