From: Tianyi Liang Date: Mon, 17 Mar 2014 18:17:12 +0000 (-0500) Subject: hot fix for pre-reg term caching in strings X-Git-Tag: cvc5-1.0.0~7014^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b6343f2c8760676ae266122647bd87f07bbebd5;p=cvc5.git hot fix for pre-reg term caching in strings --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 448b94fd2..a4d3145d9 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -43,8 +43,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_nf_pairs(c), d_loop_antec(u), d_length_intro_vars(u), + d_prereg_cached(u), + d_length_nodes(u), d_length_inst(u), - d_length_nodes(c), d_str_pos_ctn(c), d_str_neg_ctn(c), d_neg_ctn_eqlen(u), @@ -401,9 +402,10 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { ///////////////////////////////////////////////////////////////////////////// void TheoryStrings::preRegisterTerm(TNode n) { - Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl; - //collectTerms( n ); - switch (n.getKind()) { + if(d_prereg_cached.find(n) == d_prereg_cached.end()) { + Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl; + //collectTerms( n ); + switch (n.getKind()) { case kind::EQUAL: d_equalityEngine.addTriggerEquality(n); break; @@ -456,6 +458,8 @@ void TheoryStrings::preRegisterTerm(TNode n) { d_equalityEngine.addTerm(n); } } + } + d_prereg_cached.insert(n); } } @@ -1788,40 +1792,41 @@ bool TheoryStrings::checkSimple() { //then, add lemma if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { if( d_length_nodes.find(n)==d_length_nodes.end() ) { - if( d_length_inst.find(n)==d_length_inst.end() ) { + Trace("strings-debug") << "get n: " << n << endl; + Node sk; + //if( d_length_inst.find(n)==d_length_inst.end() ) { //Node nr = d_equalityEngine.getRepresentative( n ); - //if( d_length_nodes.find(nr)==d_length_nodes.end() ) { - d_length_inst.insert(n); - Trace("strings-debug") << "get n: " << n << endl; - Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" ); - d_statistics.d_new_skolems += 1; - d_length_intro_vars.insert( sk ); - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); - eq = Rewriter::rewrite(eq); - Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl; - d_out->lemma(eq); - Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - Node lsum; - if( n.getKind() == kind::STRING_CONCAT ) { - //add lemma - std::vector node_vec; - for( unsigned i=0; imkNode( kind::STRING_LENGTH, n[i] ); - node_vec.push_back(lni); - } - lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) ); - } else if( n.getKind() == kind::CONST_STRING ) { - //add lemma - lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); - } - Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); - ceq = Rewriter::rewrite(ceq); - Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; - d_out->lemma(ceq); - addedLemma = true; - //} + sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" ); + d_statistics.d_new_skolems += 1; + d_length_intro_vars.insert( sk ); + Node eq = sk.eqNode(n); + eq = Rewriter::rewrite(eq); + Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl; + d_out->lemma(eq); + //} else { + // sk = d_length_inst[n]; + //} + Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + Node lsum; + if( n.getKind() == kind::STRING_CONCAT ) { + //add lemma + std::vector node_vec; + for( unsigned i=0; imkNode( kind::STRING_LENGTH, n[i] ); + node_vec.push_back(lni); + } + lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) ); + } else if( n.getKind() == kind::CONST_STRING ) { + //add lemma + lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); } - d_length_nodes[n] = true; + Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); + ceq = Rewriter::rewrite(ceq); + Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; + d_out->lemma(ceq); + addedLemma = true; + + d_length_nodes.insert(n); } } ++eqc_i; @@ -2734,9 +2739,13 @@ void TheoryStrings::assertNode( Node lit ) { } Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero ) { - Node sk = NodeManager::currentNM()->mkSkolem( c, lhs.getType(), info ); + Node sk = NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), info ); d_statistics.d_new_skolems += 1; - Node eq = lhs.eqNode( mkConcat( rhs, sk ) ); + Node cc = mkConcat( rhs, sk ); + //if(rhs.isConst()) { + // d_length_inst[cc] = lhs; + //} + Node eq = lhs.eqNode( cc ); eq = Rewriter::rewrite( eq ); if( lgtZero ) { Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c8a374893..902b902b6 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -157,6 +157,8 @@ private: // loop ant NodeSet d_loop_antec; NodeSet d_length_intro_vars; + // preReg cache + NodeSet d_prereg_cached; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION @@ -194,8 +196,8 @@ private: std::map< Node, EqcInfo* > d_eqc_info; EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); //maintain which concat terms have the length lemma instantiated - NodeSet d_length_inst; - NodeBoolMap d_length_nodes; + NodeSet d_length_nodes; + NodeNodeMap d_length_inst; private: void mergeCstVec(std::vector< Node > &vec_strings); bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,