From: ajreynol Date: Mon, 28 Sep 2015 12:12:48 +0000 (+0200) Subject: Minor fixes to strings, add regressions. X-Git-Tag: cvc5-1.0.0~6226 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=da790d921114f250597606313245f9fe7fcb72d5;p=cvc5.git Minor fixes to strings, add regressions. --- diff --git a/src/theory/strings/options b/src/theory/strings/options index eb49e686d..858a9e21c 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -42,5 +42,7 @@ option stringLenNorm strings-len-norm --strings-len-norm bool :default true strings length normalization lemma option stringSplitEmp strings-sp-emp --strings-sp-emp bool :default true strings split on empty string +option stringInferSym strings-infer-sym --strings-infer-sym bool :default true + strings split on empty string endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d5b738fac..4a1001a04 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -616,10 +616,8 @@ void TheoryStrings::check(Effort e) { addedLemma = checkNormalForms(); Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if(!d_conflict && !addedLemma) { - if( options::stringLenNorm() ){ - addedLemma = checkLengthsEqc(); - Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - } + addedLemma = checkLengthsEqc(); + Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if(!d_conflict && !addedLemma) { addedLemma = checkExtendedFuncs(); Trace("strings-process") << "Done check extended functions, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; @@ -1208,11 +1206,11 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, } return true; } -Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c ){ - std::map< Node, Node >::iterator it = d_skolem_cache[a].find( b ); - if( it==d_skolem_cache[a].end() ){ - Node sk = mkSkolemS( c ); - d_skolem_cache[a][b] = sk; +Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit ){ + std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( isLenSplit ); + if( it==d_skolem_cache[a][b].end() ){ + Node sk = mkSkolemS( c, isLenSplit ); + d_skolem_cache[a][b][isLenSplit] = sk; return sk; }else{ return it->second; @@ -1377,7 +1375,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms } //Node sk = mkSkolemS( "v_spt", 1 ); - Node sk = mkSkolemSplit( normal_forms[i][index_i], normal_forms[j][index_j], "v_spt" ); + Node sk = mkSkolemSplit( normal_forms[i][index_i], normal_forms[j][index_j], "v_spt", 1 ); Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) ); Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) ); conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 )); @@ -1949,17 +1947,18 @@ void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) { sendLemma( eq_exp, eq, c ); } else { Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl; - - std::vector< Node > vars; - std::vector< Node > subs; - std::vector< Node > unproc; - std::vector< Node > exps; - inferSubstitutionProxyVars( eq_exp, vars, subs, unproc, exps ); - if( unproc.empty() ){ - Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - Trace("strings-lemma") << "Strings::Infer Alternate : " << eqs << std::endl; - sendLemma( mkAnd( exps ), eqs, c ); - return; + if( options::stringInferSym() ){ + std::vector< Node > vars; + std::vector< Node > subs; + std::vector< Node > unproc; + std::vector< Node > exps; + inferSubstitutionProxyVars( eq_exp, vars, subs, unproc, exps ); + if( unproc.empty() ){ + Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + Trace("strings-lemma") << "Strings::Infer Alternate : " << eqs << std::endl; + sendLemma( mkAnd( exps ), eqs, c ); + return; + } } Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl; d_pending.push_back( eq ); @@ -2332,36 +2331,38 @@ void TheoryStrings::checkDeqNF() { bool TheoryStrings::checkLengthsEqc() { bool addedLemma = false; - std::vector< Node > nodes; - getEquivalenceClasses( nodes ); - for( unsigned i=0; i1 ) { - Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl; - //check if there is a length term for this equivalence class - EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false ); - Node lt = ei ? ei->d_length_term : Node::null(); - if( !lt.isNull() ) { - Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); - //now, check if length normalization has occurred - if( ei->d_normalized_length.get().isNull() ) { - //if not, add the lemma - std::vector< Node > ant; - ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() ); - ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) ); - Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) ); - lc = Rewriter::rewrite( lc ); - Node eq = llt.eqNode( lc ); - ei->d_normalized_length.set( eq ); - sendLemma( mkExplain( ant ), eq, "LEN-NORM" ); - addedLemma = true; + if( options::stringLenNorm() ){ + std::vector< Node > nodes; + getEquivalenceClasses( nodes ); + for( unsigned i=0; i1 ) { + Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl; + //check if there is a length term for this equivalence class + EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false ); + Node lt = ei ? ei->d_length_term : Node::null(); + if( !lt.isNull() ) { + Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); + //now, check if length normalization has occurred + if( ei->d_normalized_length.get().isNull() ) { + //if not, add the lemma + std::vector< Node > ant; + ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() ); + ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) ); + Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) ); + lc = Rewriter::rewrite( lc ); + Node eq = llt.eqNode( lc ); + ei->d_normalized_length.set( eq ); + sendLemma( mkExplain( ant ), eq, "LEN-NORM" ); + addedLemma = true; + } } + } else { + Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl; } - } else { - Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl; } - } - if( addedLemma ){ - doPendingLemmas(); + if( addedLemma ){ + doPendingLemmas(); + } } return addedLemma; } @@ -3307,6 +3308,8 @@ bool TheoryStrings::checkExtendedFuncsEval() { Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl; nrs = Node::null(); } + }else{ + Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl; } Node conc; Node expl; @@ -3320,18 +3323,18 @@ bool TheoryStrings::checkExtendedFuncsEval() { conc = nrs.eqNode( nrc ); } exp.clear(); - expl = mkAnd( exps ); - //expl = d_true; + //expl = mkAnd( exps ); + expl = d_true; } }else{ if( !areEqual( n, nrc ) ){ + expl = mkExplain( exp ); if( n.getType().isBoolean() ){ - exp.push_back( n.negate() ); + exp.push_back( nrc==d_true ? n.negate() : n ); conc = d_false; }else{ conc = n.eqNode( nrc ); } - expl = mkExplain( exp ); } } if( !conc.isNull() ){ @@ -3343,6 +3346,9 @@ bool TheoryStrings::checkExtendedFuncsEval() { sendInfer( expl, conc, "EXTF" ); } if( d_conflict ){ + Trace("strings-extf") << " conflict, return." << std::endl; + doPendingFacts(); + doPendingLemmas(); return true; } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 7ecfaa69b..fb52b6413 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -329,8 +329,8 @@ protected: void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc, std::vector< Node >& exp ); - std::map< Node, std::map< Node, Node > > d_skolem_cache; - Node mkSkolemSplit( Node a, Node b, const char * c ); + std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache; + Node mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit = 0 ); private: Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero ); diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index e880d3edc..716d41365 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -56,7 +56,9 @@ TESTS = \ artemis-0512-nonterm.smt2 \ indexof-sym-simp.smt2 \ bug613.smt2 \ - idof-triv.smt2 + idof-triv.smt2 \ + chapman150408.smt2 \ + pierre150331.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/chapman150408.smt2 b/test/regress/regress0/strings/chapman150408.smt2 new file mode 100644 index 000000000..546c46e32 --- /dev/null +++ b/test/regress/regress0/strings/chapman150408.smt2 @@ -0,0 +1,10 @@ +(set-logic SLIA) +(set-info :status sat) +(set-option :strings-exp true) +(set-option :rewrite-divk true) +(declare-fun string () String) +(assert (and + (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0) + 0)))) (not (= (ite (not (= (str.len string) 0)) 1 0) 0))) (not + (not (= (ite (str.contains string "]") 1 0) 0))))) +(check-sat) diff --git a/test/regress/regress0/strings/pierre150331.smt2 b/test/regress/regress0/strings/pierre150331.smt2 new file mode 100644 index 000000000..88d5ec10c --- /dev/null +++ b/test/regress/regress0/strings/pierre150331.smt2 @@ -0,0 +1,13 @@ +(set-logic SLIA) +(set-info :status sat) +(set-info :smt-lib-version 2.5) +(set-option :strings-exp true) +(define-fun stringEval ((?s String)) Bool (str.in.re ?s +(re.union +(str.to.re "H") +(re.++ (re.loop (str.to.re "{") 2 2 ) (re.loop (re.union re.nostr (re.range "" "]") (re.range "" "^") ) 2 4 ) ) ) ) ) +(declare-fun s0() String) +(declare-fun s1() String) +(declare-fun s2() String) +(assert (and true (stringEval s0) (stringEval s1) (distinct s0 s1) (stringEval s2) (distinct s0 s2) (distinct s1 s2) ) ) +(check-sat) \ No newline at end of file