Unit tests for solvers/refinement/string_constraint_instantiation.cpp:instantiate_not_contains

src/solvers/Makefile

@@ -171,6 +171,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/string_constraint_generator_testing.cpp \
       refinement/string_constraint_generator_transformation.cpp \
       refinement/string_constraint_generator_valueof.cpp \
+      refinement/string_constraint_instantiation.cpp \
       sat/cnf.cpp \
       sat/cnf_clause_list.cpp \
       sat/dimacs_cnf.cpp \

src/solvers/refinement/string_constraint.h

@@ -24,6 +24,7 @@ Author: Romain Brenguier, [email protected]
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <util/refined_string_type.h>
+#include <util/string_expr.h>
 #include <langapi/language_util.h>
 
 /*! \brief Universally quantified string constraint
@@ -138,12 +139,20 @@ extern inline string_constraintt &to_string_constraint(exprt &expr)
   return static_cast<string_constraintt &>(expr);
 }
 
+/// Used for debug printing.
+/// \param [in] ns: namespace for `from_expr`
+/// \param [in] identifier: identifier for `from_expr`
+/// \param [in] expr: constraint to render
+/// \return rendered string
 inline static std::string from_expr(
   const namespacet &ns,
   const irep_idt &identifier,
   const string_constraintt &expr)
 {
-  return from_expr(ns, identifier, expr.premise())+" => "+
+  return "forall "+from_expr(ns, identifier, expr.univ_var())+" in ["+
+    from_expr(ns, identifier, expr.lower_bound())+", "+
+    from_expr(ns, identifier, expr.upper_bound())+"). "+
+    from_expr(ns, identifier, expr.premise())+" => "+
     from_expr(ns, identifier, expr.body());
 }
 
@@ -204,6 +213,26 @@ class string_not_contains_constraintt: public exprt
   }
 };
 
+/// Used for debug printing.
+/// \param [in] ns: namespace for `from_expr`
+/// \param [in] identifier: identifier for `from_expr`
+/// \param [in] expr: constraint to render
+/// \return rendered string
+inline static std::string from_expr(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const string_not_contains_constraintt &expr)
+{
+  return "forall x in ["+
+    from_expr(ns, identifier, expr.univ_lower_bound())+", "+
+    from_expr(ns, identifier, expr.univ_upper_bound())+"). "+
+    from_expr(ns, identifier, expr.premise())+" => ("+
+    "exists y in ["+from_expr(ns, identifier, expr.exists_lower_bound())+", "+
+    from_expr(ns, identifier, expr.exists_upper_bound())+"). "+
+    from_expr(ns, identifier, expr.s0())+"[x+y] != "+
+    from_expr(ns, identifier, expr.s1())+"[y])";
+}
+
 inline const string_not_contains_constraintt
 &to_string_not_contains_constraint(const exprt &expr)
 {

src/solvers/refinement/string_constraint_instantiation.cpp

@@ -0,0 +1,71 @@
+/*******************************************************************\
+
+Module: Defines functions related to string constraints.
+
+Author: Jesse Sigal, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Defines related function for string constraints.
+
+#include <solvers/refinement/string_constraint_instantiation.h>
+
+#include <solvers/refinement/string_constraint.h>
+#include <solvers/refinement/string_constraint_generator.h>
+#include <solvers/refinement/string_refinement.h>
+
+/// Instantiates a quantified formula representing `not_contains` by
+/// substituting the quantifiers and generating axioms.
+/// \related string_refinementt
+/// \param [in] axiom: the axiom to instantiate
+/// \param [in] index_set0: the index set for `axiom.s0()`
+/// \param [in] index_set1: the index set for `axiom.s1()`
+/// \param [in] generator: generator to be used to get `axiom`'s witness
+/// \return the lemmas produced through instantiation
+std::vector<exprt> instantiate_not_contains(
+  const string_not_contains_constraintt &axiom,
+  const std::set<exprt> &index_set0,
+  const std::set<exprt> &index_set1,
+  const string_constraint_generatort &generator)
+{
+  std::vector<exprt> lemmas;
+
+  const string_exprt s0=to_string_expr(axiom.s0());
+  const string_exprt s1=to_string_expr(axiom.s1());
+
+  for(const auto &i0 : index_set0)
+    for(const auto &i1 : index_set1)
+    {
+      const minus_exprt val(i0, i1);
+      const exprt witness=generator.get_witness_of(axiom, val);
+      const and_exprt prem_and_is_witness(
+        axiom.premise(),
+        equal_exprt(witness, i1));
+
+      const not_exprt differ(equal_exprt(s0[i0], s1[i1]));
+      const implies_exprt lemma(prem_and_is_witness, differ);
+      lemmas.push_back(lemma);
+
+      // we put bounds on the witnesses:
+      // 0 <= v <= |s0| - |s1| ==> 0 <= v+w[v] < |s0| && 0 <= w[v] < |s1|
+      const exprt zero=from_integer(0, val.type());
+      const binary_relation_exprt c1(zero, ID_le, plus_exprt(val, witness));
+      const binary_relation_exprt c2(
+        s0.length(), ID_gt, plus_exprt(val, witness));
+      const binary_relation_exprt c3(s1.length(), ID_gt, witness);
+      const binary_relation_exprt c4(zero, ID_le, witness);
+
+      const minus_exprt diff(s0.length(), s1.length());
+
+      const and_exprt premise(
+        binary_relation_exprt(zero, ID_le, val),
+        binary_relation_exprt(diff, ID_ge, val));
+      const implies_exprt witness_bounds(
+        premise,
+        and_exprt(and_exprt(c1, c2), and_exprt(c3, c4)));
+      lemmas.push_back(witness_bounds);
+    }
+
+  return lemmas;
+}

src/solvers/refinement/string_constraint_instantiation.h

@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Defines related function for string constraints.
+
+Author: Jesse Sigal, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Defines related function for string constraints.
+
+#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
+#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
+
+#include <solvers/refinement/string_constraint.h>
+#include <solvers/refinement/string_constraint_generator.h>
+
+std::vector<exprt> instantiate_not_contains(
+  const string_not_contains_constraintt &axiom,
+  const std::set<exprt> &index_set0,
+  const std::set<exprt> &index_set1,
+  const string_constraint_generatort &generator);
+
+#endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H

src/solvers/refinement/string_refinement.cpp

@@ -29,6 +29,7 @@ Author: Alberto Griggio, [email protected]
 #include <util/simplify_expr.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_refinement_invariant.h>
+#include <solvers/refinement/string_constraint_instantiation.h>
 #include <langapi/language_util.h>
 #include <java_bytecode/java_types.h>
 
@@ -606,8 +607,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       for(unsigned i=0; i<not_contains_axioms.size(); i++)
       {
         debug()<< "constraint " << i << eom;
-        std::list<exprt> lemmas;
-        instantiate_not_contains(not_contains_axioms[i], lemmas);
+        const std::vector<exprt> lemmas=
+          instantiate_not_contains(not_contains_axioms[i]);
         for(const exprt &lemma : lemmas)
           add_lemma(lemma);
       }
@@ -1603,60 +1604,23 @@ exprt string_refinementt::instantiate(
   return implies_exprt(bounds, instance);
 }
 
-/// instantiate a quantified formula representing `not_contains` by substituting
-/// the quantifiers and generating axioms
-/// \par parameters: a quantified formula representing `not_contains`, and a
-/// list to which to add the created lemmas to
-void string_refinementt::instantiate_not_contains(
-  const string_not_contains_constraintt &axiom, std::list<exprt> &new_lemmas)
+/// Instantiates a quantified formula representing `not_contains` by
+/// substituting the quantifiers and generating axioms.
+/// \param [in] axiom: the axiom to instantiate
+/// \return the lemmas produced through instantiation
+std::vector<exprt> string_refinementt::instantiate_not_contains(
+  const string_not_contains_constraintt &axiom)
 {
-  exprt s0=axiom.s0();
-  exprt s1=axiom.s1();
+  const string_exprt s0=to_string_expr(axiom.s0());
+  const string_exprt s1=to_string_expr(axiom.s1());
 
   debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : "
           << from_expr(ns, "", s1) << eom;
-  expr_sett index_set0=index_set[to_string_expr(s0).content()];
-  expr_sett index_set1=index_set[to_string_expr(s1).content()];
+  const expr_sett index_set0=index_set[s0.content()];
+  const expr_sett index_set1=index_set[s1.content()];
 
-  for(auto it0 : index_set0)
-    for(auto it1 : index_set1)
-    {
-      debug() << from_expr(ns, "", it0) << " : " << from_expr(ns, "", it1)
-              << eom;
-      exprt val=minus_exprt(it0, it1);
-      exprt witness=generator.get_witness_of(axiom, val);
-      and_exprt prem_and_is_witness(
-        axiom.premise(),
-        equal_exprt(witness, it1));
-
-      not_exprt differ(
-        equal_exprt(
-          to_string_expr(s0)[it0],
-          to_string_expr(s1)[it1]));
-      exprt lemma=implies_exprt(prem_and_is_witness, differ);
-
-      new_lemmas.push_back(lemma);
-      // we put bounds on the witnesses:
-      // 0 <= v <= |s0| - |s1| ==> 0 <= v+w[v] < |s0| && 0 <= w[v] < |s1|
-      exprt zero=from_integer(0, val.type());
-      binary_relation_exprt c1(zero, ID_le, plus_exprt(val, witness));
-      binary_relation_exprt c2
-        (to_string_expr(s0).length(), ID_gt, plus_exprt(val, witness));
-      binary_relation_exprt c3(to_string_expr(s1).length(), ID_gt, witness);
-      binary_relation_exprt c4(zero, ID_le, witness);
-
-      minus_exprt diff(
-        to_string_expr(s0).length(),
-        to_string_expr(s1).length());
-
-      and_exprt premise(
-        binary_relation_exprt(zero, ID_le, val),
-        binary_relation_exprt(diff, ID_ge, val));
-      exprt witness_bounds=implies_exprt(
-        premise,
-        and_exprt(and_exprt(c1, c2), and_exprt(c3, c4)));
-      new_lemmas.push_back(witness_bounds);
-    }
+  return ::instantiate_not_contains(
+    axiom, index_set0, index_set1, generator);
 }
 
 /// replace array-lists by 'with' expressions

src/solvers/refinement/string_refinement.h

@@ -133,9 +133,8 @@ class string_refinementt: public bv_refinementt
   exprt instantiate(
     const string_constraintt &axiom, const exprt &str, const exprt &val);
 
-  void instantiate_not_contains(
-    const string_not_contains_constraintt &axiom,
-    std::list<exprt> &new_lemmas);
+  std::vector<exprt> instantiate_not_contains(
+    const string_not_contains_constraintt &axiom);
 
   exprt substitute_array_lists(exprt) const;
 

unit/Makefile

@@ -24,6 +24,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix_lower_case.cpp \
+       solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
        catch_example.cpp \
        # Empty last line