From ffaf556b34e3ef2972b47caea00b7da149aeea8f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 1 Dec 2016 10:47:31 -0600 Subject: [PATCH] Improvement and bug fix for str.indexof reduction, add regression. Other minor changes. --- src/theory/quantifiers/model_engine.cpp | 6 +++++- src/theory/sep/kinds | 2 +- src/theory/strings/theory_strings_preprocess.cpp | 16 +++++++--------- test/regress/regress0/strings/Makefile.am | 3 ++- .../regress0/strings/strings-index-empty.smt2 | 11 +++++++++++ 5 files changed, 26 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress0/strings/strings-index-empty.smt2 diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 1a0faa021..20f5eae7b 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -231,7 +231,11 @@ int ModelEngine::checkModel(){ } bool ModelEngine::considerQuantifiedFormula( Node q ) { - if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) || !d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ + Trace("model-engine-debug") << "Model builder inactive : " << q << std::endl; + return false; + }else if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){ + Trace("model-engine-debug") << "Model inactive : " << q << std::endl; return false; }else{ if( options::fmfEmptySorts() ){ diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 318442ba5..5cd9093f4 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -25,7 +25,7 @@ operator SEP_EMP 2 "separation empty heap" operator SEP_PTO 2 "points to relation" operator SEP_STAR 2: "separation star" operator SEP_WAND 2 "separation magic wand" -operator SEP_LABEL 2 "separation label" +operator SEP_LABEL 2 "separation label (internal use only)" typerule SEP_NIL_REF ::CVC4::theory::sep::SepNilRefTypeRule typerule SEP_EMP ::CVC4::theory::sep::SepEmpTypeRule diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a697dad75..c8fe1fb00 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -116,25 +116,23 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" ); } Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) ); + //TODO: simplify this (only applies when idof != -1) Node eq = st.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4 ) ); new_nodes.push_back( eq ); + + //learn range of idof? Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone ); new_nodes.push_back( krange ); krange = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk); new_nodes.push_back( krange ); - krange = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero); - new_nodes.push_back( krange ); - Node start_valid = NodeManager::currentNM()->mkNode( kind::GEQ, t[2], d_zero); - //str.len(s1) < y + str.len(s2) - Node c1 = NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )), - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] )); + // s2 = "" + Node c1 = t[1].eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); //~contain(t234, s2) Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, st, t[1] ).negate(); //left - Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, c3, start_valid.negate() ); + Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, c3 ); //t3 = s2 Node c4 = t[1].eqNode( sk3 ); //~contain(t2, s2) @@ -149,7 +147,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 )) ); //right - Node right = NodeManager::currentNM()->mkNode( kind::AND, c4, c5, c6, start_valid ); + Node right = NodeManager::currentNM()->mkNode( kind::AND, c4, c5, c6, c1.negate() ); Node cond = skk.eqNode( negone ); Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right ); new_nodes.push_back( rr ); diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 21d51199d..70fec7b82 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -83,7 +83,8 @@ TESTS = \ csp-prefix-exp-bug.smt2 \ cmu-substr-rw.smt2 \ gm-inc-071516-2.smt2 \ - cmu-inc-nlpp-071516.smt2 + cmu-inc-nlpp-071516.smt2 \ + strings-index-empty.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/strings-index-empty.smt2 b/test/regress/regress0/strings/strings-index-empty.smt2 new file mode 100644 index 000000000..a726d9cab --- /dev/null +++ b/test/regress/regress0/strings/strings-index-empty.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --simplification=none --strings-exp --no-strings-lazy-pp +; EXPECT: sat +(set-logic SLIA) +(set-info :status sat) +(declare-fun x () String) +(declare-fun f () String) +(declare-fun y () Int) +(assert (= (str.len f) 0)) +; command line options ensure reduction is invoked for indexof, f is "", should return -1 +(assert (= (str.indexof x f 4) y)) +(check-sat) -- 2.30.2