From: ajreynol Date: Sun, 11 Oct 2015 13:35:14 +0000 (+0200) Subject: Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastructure... X-Git-Tag: cvc5-1.0.0~6211 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6179b1922e0366acec51eec24a2023d21354030;p=cvc5.git Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastructure for str.contains inferences. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 337c5104c..a1eca35fa 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -88,7 +88,7 @@ #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/options.h" #include "theory/datatypes/options.h" -#include "theory/strings/theory_strings_preprocess.h" +#include "theory/strings/theory_strings.h" #include "printer/options.h" #include "theory/arith/pseudoboolean_proc.h" @@ -3297,8 +3297,7 @@ void SmtEnginePrivate::processAssertions() { if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; dumpAssertions("pre-strings-pp", d_assertions); - CVC4::theory::strings::StringsPreprocess sp; - sp.simplify( d_assertions.ref() ); + ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() ); //for (unsigned i = 0; i < d_assertions.size(); ++ i) { // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); //} diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f4019450d..997c47776 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -68,7 +68,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_loop_antec(u), d_length_intro_vars(u), d_registered_terms_cache(u), + d_preproc(u), d_preproc_cache(u), + d_extf_infer_cache(c), d_proxy_var(u), d_proxy_var_to_length(u), d_neg_ctn_eqlen(u), @@ -2054,8 +2056,8 @@ void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) { Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl; d_pending.push_back( eq ); d_pending_exp[eq] = eq_exp; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); + d_infer.push_back( eq ); + d_infer_exp.push_back( eq_exp ); } } @@ -3832,12 +3834,20 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ if( (*it).second ){ Node n = (*it).first; + int n_pol = 0; + if( n.getType().isBoolean() ){ + if( areEqual( n, d_true ) ){ + n_pol = 1; + }else if( areEqual( n, d_false ) ){ + n_pol = -1; + } + } Trace("strings-extf-debug") << "Check extf " << n << "..." << std::endl; if( effort==0 ){ std::map< Node, bool > visited; collectVars( n, d_extf_vars[n], visited ); } - //build up a best current substitution for the variables in the term + //build up a best current substitution for the variables in the term, exp is explanation for substitution std::vector< Node > exp; std::vector< Node > var; std::vector< Node > sub; @@ -3873,7 +3883,7 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { } } } - + Node to_reduce; if( !var.empty() ){ Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() ); Node nrc = Rewriter::rewrite( nr ); @@ -3929,16 +3939,46 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { return; } } + }else if( ( nrc.getKind()==kind::OR && n_pol==-1 ) || ( nrc.getKind()==kind::AND && n_pol==1 ) ){ + //infer the consequence of each + d_ext_func_terms[n] = false; + exp.push_back( n_pol==-1 ? n.negate() : n ); + Trace("strings-extf-debug") << " decomposable..." << std::endl; + Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << n_pol << std::endl; + for( unsigned i=0; i& exp, int effort ){ + if( n_pol!=0 ){ + if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){ + d_extf_infer_cache.insert( nr ); + if( nr.getKind()==kind::STRING_STRCTN ){ + if( ( n_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( n_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){ + //one argument does (not) contain each of the components of the other argument + exp.push_back( n_pol==1 ? n : n.negate() ); + int index = n_pol==1 ? 1 : 0; + for( unsigned i=0; i d_pending; std::vector< Node > d_lemma_cache; std::map< Node, bool > d_pending_req_phase; - /** inferences */ + /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeList d_infer; NodeList d_infer_exp; /** normal forms */ @@ -177,6 +177,8 @@ private: // preprocess cache StringsPreprocess d_preproc; NodeBoolMap d_preproc_cache; + // extended functions inferences cache + NodeSet d_extf_infer_cache; bool doPreprocess( Node atom ); bool hasProcessed(); @@ -277,6 +279,7 @@ private: void checkInit(); void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ); void checkExtendedFuncsEval( int effort = 0 ); + void checkExtfInference( Node n, Node nr, int n_pol, std::vector< Node >& exp, int effort ); void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ); void checkNormalForms(); Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); @@ -319,6 +322,8 @@ public: void eqNotifyPostMerge(TNode t1, TNode t2); /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + /** get preprocess */ + StringsPreprocess * getPreprocess() { return &d_preproc; } protected: /** compute care graph */ void computeCareGraph(); @@ -360,7 +365,7 @@ protected: void printConcat( std::vector< Node >& n, const char * c ); void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ); - + enum { sk_id_c_spt, sk_id_vc_spt, diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 4e2b00fb1..b2b7bac5e 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -25,7 +25,7 @@ namespace CVC4 { namespace theory { namespace strings { -StringsPreprocess::StringsPreprocess() { +StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){ //Constants d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); } @@ -119,7 +119,9 @@ void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret bool StringsPreprocess::checkStarPlus( Node t ) { if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) { for( unsigned i = 0; i &new_nodes, bool during_pp ) { - std::hash_map::const_iterator i = d_cache.find(t); + NodeNodeMap::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { return (*i).second.isNull() ? t : (*i).second; } @@ -568,7 +570,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d } Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool during_pp) { - std::hash_map::const_iterator i = d_cache.find(t); + NodeNodeMap::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { return (*i).second.isNull() ? t : (*i).second; } diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 1255d93e0..a5ba1f615 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -23,14 +23,17 @@ #include "util/hash.h" #include "theory/theory.h" #include "theory/rewriter.h" +#include "context/cdchunk_list.h" +#include "context/cdhashmap.h" namespace CVC4 { namespace theory { namespace strings { class StringsPreprocess { + typedef context::CDHashMap NodeNodeMap; // NOTE: this class is NOT context-dependent - std::hash_map d_cache; + NodeNodeMap d_cache; //Constants Node d_zero; private: @@ -39,7 +42,7 @@ private: void processRegExp( Node s, Node r, std::vector< Node > &ret ); Node simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ); public: - StringsPreprocess(); + StringsPreprocess( context::UserContext* u ); Node decompose( Node t, std::vector< Node > &new_nodes, bool during_pp = false ); void simplify(std::vector< Node > &vec_node); diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index a8a8e968f..45a7fb802 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -68,7 +68,8 @@ TESTS = \ bug615.smt2 \ kaluza-fl.smt2 \ norn-ab.smt2 \ - idof-rewrites.smt2 + idof-rewrites.smt2 \ + bug682.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/bug682.smt2 b/test/regress/regress0/strings/bug682.smt2 new file mode 100644 index 000000000..6617b6b97 --- /dev/null +++ b/test/regress/regress0/strings/bug682.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --incremental --strings-exp +(set-logic QF_S) + +(declare-fun a () String) +(define-fun replace3 ((x String) (y String) (z String)) String (str.replace x y z) ) + +(push 1) +(assert (= (replace3 a "5" "3") "333")) +(assert (str.contains a "5")) +; EXPECT: sat +(check-sat) +(pop 1) + +(push 1) +(assert (= (replace3 a "5" "3") "333")) +(assert (str.contains a "5")) +; EXPECT: sat +(check-sat) +(pop 1)