From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 1 Dec 2016 16:47:31 +0000 (-0600)
Subject: Improvement and bug fix for str.indexof reduction, add regression. Other minor changes.
X-Git-Tag: cvc5-1.0.0~5963
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ffaf556b34e3ef2972b47caea00b7da149aeea8f;p=cvc5.git

Improvement and bug fix for str.indexof reduction, add regression. Other minor changes.
---

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)