From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 17 Oct 2018 16:14:49 +0000 (-0500)
Subject:  Fix context-dependent for positive contains reduction (#2644)
X-Git-Tag: cvc5-1.0.0~4413
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1823d6d537a59d85a17f09f53c8128d934c420a3;p=cvc5.git

 Fix context-dependent for positive contains reduction (#2644)
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 984b47e72..883683f52 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -493,6 +493,10 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on positive contain reduction."
         << std::endl;
+    Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
+                               << " => " << eq << std::endl;
+    // context-dependent because it depends on the polarity of n itself
+    isCd = true;
   }
   else if (k != kind::STRING_CODE)
   {
@@ -513,8 +517,8 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
     sendInference(d_empty_vec, nnlem, "Reduction", true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
+    isCd = false;
   }
-  isCd = false;
   return true;
 }
 
@@ -1001,6 +1005,7 @@ void TheoryStrings::checkExtfReductions( int effort ) {
   Trace("strings-process") << "  checking " << extf.size() << " active extf"
                            << std::endl;
   for( unsigned i=0; i<extf.size(); i++ ){
+    Assert(!d_conflict);
     Node n = extf[i];
     Trace("strings-process") << "  check " << n << ", active in model="
                              << d_extf_info_tmp[n].d_model_active << std::endl;