addressed bug #87; fixed the translation of str.prefixof to equations

uuverifiers · Sep 10, 2024 · 71e402f · 71e402f
1 parent f41eab0
commit 71e402f
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 16 deletions.
diff --git a/src/main/scala/ostrich/OstrichPreprocessor.scala b/src/main/scala/ostrich/OstrichPreprocessor.scala
@@ -81,37 +81,37 @@ class OstrichPreprocessor(theory : OstrichStringTheory)
     }
  */
 
-    case (IAtom(`str_prefixof`, _),
-          Seq(subStr@ConcreteString(_), bigStr : ITerm)) => {
-      val asRE = re_++(str_to_re(subStr), re_all())
-      str_in_re(bigStr, asRE)
-    }
-
-  /**  case (IAtom(`str_prefixof`, _),
-    Seq(x,y)) if (x == y) => {
+    case (IAtom(`str_prefixof`, _), Seq(x,y)) if (x == y) => {
         IBoolLit(true)
-    } */
+    }
 
     case (IAtom(`str_suffixof`, _), Seq(x,y)) if (x == y) => {
       IBoolLit(true)
     }
+
     case (IAtom(`str_contains`, _), Seq(x,y)) if (x == y) => {
       IBoolLit(true)
     }
-/*
+
+    case (IAtom(`str_prefixof`, _),
+          Seq(subStr@ConcreteString(_), bigStr : ITerm)) => {
+      val asRE = re_++(str_to_re(subStr), re_all())
+      str_in_re(bigStr, asRE)
+    }
+
     case (IAtom(`str_prefixof`, _),
           Seq(subStr : ITerm, bigStr : ITerm)) if ctxt.polarity < 0 => {
       val s = VariableShiftVisitor(subStr, 0, 1)
       val t = VariableShiftVisitor(bigStr, 0, 1)
       StringSort.ex(str_++(s, v(0, StringSort)) === t)
     }
- */
 
     case (IAtom(`str_suffixof`, _),
           Seq(subStr@ConcreteString(_), bigStr : ITerm)) => {
       val asRE = re_++(re_all(), str_to_re(subStr))
       str_in_re(bigStr, asRE)
     }
+
     case (IAtom(`str_suffixof`, _),
           Seq(subStr : ITerm, bigStr : ITerm)) if ctxt.polarity < 0 => {
       val s = VariableShiftVisitor(subStr, 0, 1)

diff --git a/src/main/scala/ostrich/OstrichSolver.scala b/src/main/scala/ostrich/OstrichSolver.scala
@@ -87,7 +87,6 @@ class OstrichSolver(theory : OstrichStringTheory,
                  re_from_ecma2020, re_from_ecma2020_flags,
                  re_case_insensitive,
                  str_replace, str_replacere, str_replaceall, str_replaceallre,
-                 str_prefixof,
                  re_none, re_all, re_allchar, re_charrange,
                  re_++, re_union, re_inter, re_diff, re_*, re_*?, re_+, re_+?, re_opt, re_opt_?,
                  re_comp, re_loop, re_loop_?, re_eps, re_capture, re_reference,
@@ -193,10 +192,6 @@ class OstrichSolver(theory : OstrichStringTheory,
       case FunPred(`str_char_count`) => {
         // ignore
       }
-      case `str_prefixof` => {
-        val rightVar = theory.StringSort.newConstant("rhs")
-        funApps += ((ConcatPreOp, List(a(0), rightVar), a(1)))
-      }
       case FunPred(f) if rexOps contains f =>
         // nothing
       case p if (theory.predicates contains p) =>

diff --git a/src/test/scala/SMTLIBTests.scala b/src/test/scala/SMTLIBTests.scala
@@ -65,6 +65,9 @@ object SMTLIBTests extends Properties("SMTLIBTests") {
   property("suffix-5.smt2") =
     checkFile("tests/suffix-5.smt2", "unsat")
 
+  property("prefix-suffix.smt2") =
+    checkFile("tests/prefix-suffix.smt2", "unsat")
+
   property("contains-1.smt2") =
     checkFile("tests/contains-1.smt2", "sat")
   property("contains-2.smt2") =

diff --git a/tests/prefix-suffix.smt2 b/tests/prefix-suffix.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_S)
+
+; UNSAT
+
+(declare-fun a () String)
+(declare-fun b () String)
+
+(assert (not (=> (and (str.prefixof a b) (str.suffixof b a)) (= a b))))
+
+(check-sat)