TG-592 Implemented the correct instantiation procedure for not contains constraints

The method of insantiating not contains constraints is correct, see TG-591. This involved a localized change to `string_constraint_instantiation.cpp:instantiate_not_contains`, but also involved the activation of counter-examples in `string_refinementt`. The reason for this is that the new (correct) instances are relatively weak, and the solver will end up with an empty index set. The current behavior of returning SAT in this case is incorrect, and will be fixed shortly by TG-672. Additionally, the choice of indices at which to instantiate not contains constraints has been changed to be more sensible. Finally, the relevant unit tests have been updated.

Author: jasigal

src/solvers/refinement/string_constraint_instantiation.cpp

@@ -11,61 +11,46 @@ Author: Jesse Sigal, [email protected]
 
 #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] index_pairs: the pairs of indices to at which to instantiate
 /// \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 std::set<std::pair<exprt, exprt>> &index_pairs,
   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);
-    }
+  const string_exprt &s0=to_string_expr(axiom.s0());
+  const string_exprt &s1=to_string_expr(axiom.s1());
+
+  for(const auto &pair : index_pairs)
+  {
+    // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1
+    // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1.
+    const exprt &i0=pair.first;
+    const exprt &i1=pair.second;
+    const minus_exprt val(i0, i1);
+    const and_exprt universal_bound(
+      binary_relation_exprt(axiom.univ_lower_bound(), ID_le, val),
+      binary_relation_exprt(axiom.univ_upper_bound(), ID_gt, val));
+    const exprt f=generator.get_witness_of(axiom, val);
+    const equal_exprt relevancy(f, i1);
+    const and_exprt premise(relevancy, axiom.premise(), universal_bound);
+
+    const notequal_exprt differ(s0[i0], s1[i1]);
+    const and_exprt existential_bound(
+      binary_relation_exprt(axiom.exists_lower_bound(), ID_le, i1),
+      binary_relation_exprt(axiom.exists_upper_bound(), ID_gt, i1));
+    const and_exprt body(differ, existential_bound);
+
+    const implies_exprt lemma(premise, body);
+    lemmas.push_back(lemma);
+  }
 
   return lemmas;
 }

src/solvers/refinement/string_constraint_instantiation.h

@@ -17,8 +17,7 @@ Author: Jesse Sigal, [email protected]
 
 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 std::set<std::pair<exprt, exprt>> &index_pairs,
   const string_constraint_generatort &generator);
 
 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H

src/solvers/refinement/string_refinement.cpp

@@ -99,6 +99,7 @@ static std::vector<exprt> instantiate_not_contains(
   const namespacet &ns,
   const string_not_contains_constraintt &axiom,
   const std::map<exprt, std::set<exprt>> &index_set,
+  const std::map<exprt, std::set<exprt>> &current_index_set,
   const string_constraint_generatort &generator);
 
 static exprt get_array(
@@ -850,7 +851,12 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         debug() << "constraint " << i << '\n';
         const std::vector<exprt> lemmas=
           instantiate_not_contains(
-            debug(), ns, not_contains_axioms[i], index_set, generator);
+            debug(),
+            ns,
+            not_contains_axioms[i],
+            index_set,
+            current_index_set,
+            generator);
         for(const exprt &lemma : lemmas)
           add_lemma(lemma);
       }
@@ -1510,23 +1516,26 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 
     if(use_counter_example)
     {
-      // TODO: add counter examples for not_contains?
+      stream << "Adding counter-examples: " << eom;
+      // TODO: add counter-examples for universal constraints?
 
-      // Checking if the current solution satisfies the constraints
       std::vector<exprt> lemmas;
-      for(const auto &v : violated)
+      for(const auto &v : violated_not_contains)
       {
         const exprt &val=v.second;
-        const string_constraintt &axiom=universal_axioms[v.first];
-
-        exprt premise(axiom.premise());
-        exprt body(axiom.body());
-        implies_exprt instance(premise, body);
-        replace_expr(symbol_resolve, instance);
-        replace_expr(axiom.univ_var(), val, instance);
-        stream << "adding counter example " << from_expr(ns, "", instance)
-               << eom;
-        lemmas.push_back(instance);
+        const string_not_contains_constraintt &axiom=
+          not_contains_axioms[v.first];
+
+        const exprt func_val=generator.get_witness_of(axiom, val);
+        const exprt comp_val=simplify_sum(plus_exprt(val, func_val));
+
+        std::set<std::pair<exprt, exprt>> indices;
+        indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
+        const exprt counter=::instantiate_not_contains(
+          axiom, indices, generator)[0];
+
+        stream << "    -  " << from_expr(ns, "", counter) << eom;
+        lemmas.push_back(counter);
       }
       return { false, lemmas };
     }
@@ -1960,19 +1969,36 @@ static std::vector<exprt> instantiate_not_contains(
   const namespacet &ns,
   const string_not_contains_constraintt &axiom,
   const std::map<exprt, std::set<exprt>> &index_set,
+  const std::map<exprt, std::set<exprt>> &current_index_set,
   const string_constraint_generatort &generator)
 {
-  const string_exprt s0=to_string_expr(axiom.s0());
-  const string_exprt s1=to_string_expr(axiom.s1());
+  const string_exprt &s0=axiom.s0();
+  const string_exprt &s1=axiom.s1();
 
   stream << "instantiate not contains " << from_expr(ns, "", s0) << " : "
          << from_expr(ns, "", s1) << messaget::eom;
-  const auto &i0=index_set.find(s0.content());
-  const auto &i1=index_set.find(s1.content());
-  if(i0!=index_set.end() && i1!=index_set.end())
+
+  const auto &index_set0=index_set.find(s0.content());
+  const auto &index_set1=index_set.find(s1.content());
+  const auto &current_index_set0=current_index_set.find(s0.content());
+  const auto &current_index_set1=current_index_set.find(s1.content());
+
+  if(index_set0!=index_set.end() &&
+     index_set1!=index_set.end() &&
+     current_index_set0!=index_set.end() &&
+     current_index_set1!=index_set.end())
   {
-    return ::instantiate_not_contains(
-      axiom, i0->second, i1->second, generator);
+    typedef std::pair<exprt, exprt> expr_pairt;
+    std::set<expr_pairt> index_pairs;
+
+    for(const auto &ic0 : current_index_set0->second)
+      for(const auto &i1 : index_set1->second)
+        index_pairs.insert(expr_pairt(ic0, i1));
+    for(const auto &ic1 : current_index_set1->second)
+      for(const auto &i0 : index_set0->second)
+        index_pairs.insert(expr_pairt(i0, ic1));
+
+    return ::instantiate_not_contains(axiom, index_pairs, generator);
   }
   return { };
 }

src/solvers/refinement/string_refinement.h

@@ -39,7 +39,7 @@ class string_refinementt final: public bv_refinementt
     bool string_non_empty=false;
     /// Concretize strings after solver is finished
     bool trace=false;
-    bool use_counter_example=false;
+    bool use_counter_example=true;
   };
 public:
   /// string_refinementt constructor arguments

unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -11,12 +11,9 @@
 #include <solvers/refinement/string_constraint_instantiation.h>
 
 #include <solvers/sat/satcheck.h>
-#include <solvers/refinement/bv_refinement.h>
 #include <java_bytecode/java_types.h>
 #include <langapi/mode.h>
 #include <java_bytecode/java_bytecode_language.h>
-#include <util/namespace.h>
-#include <util/symbol_table.h>
 #include <util/simplify_expr.h>
 
 /// \class Types used throughout the test. Currently it is impossible to
@@ -48,7 +45,7 @@ const tt t;
 /// Creates a `constant_exprt` of the proper length type.
 /// \param [in] i: integer to convert
 /// \return corresponding `constant_exprt`
-constant_exprt from_integer(const mp_integer i)
+constant_exprt from_integer(const mp_integer &i)
 {
   return from_integer(i, t.length_type());
 }
@@ -81,6 +78,17 @@ std::set<exprt> full_index_set(const string_exprt &s)
   return ret;
 }
 
+/// Create the cartesian product of two sets.
+template<class T, class U>
+std::set<std::pair<T, U>> product(const std::set<T> ts, const std::set<U> us)
+{
+  std::set<std::pair<T, U>> s;
+  for(const auto &t : ts)
+    for(const auto &u : us)
+      s.insert(std::pair<T, U>(t, u));
+  return s;
+}
+
 /// Simplifies, and returns the conjunction of the lemmas.
 /// \param [in] lemmas: lemmas to process
 /// \param [in] ns: namespace for simplifying
@@ -152,7 +160,7 @@ SCENARIO("instantiate_not_contains",
 
     // Generating the corresponding axioms and simplifying, recording info
     symbol_tablet symtab;
-    namespacet empty_ns(symtab);
+    const namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
     string_constraint_generatort generator(info, ns);
     exprt res=generator.add_axioms_for_function_application(func);
@@ -196,7 +204,7 @@ SCENARIO("instantiate_not_contains",
       for(const auto &axiom : nc_axioms)
       {
         const std::vector<exprt> l=instantiate_not_contains(
-          axiom, index_set_ab, index_set_b, generator);
+          axiom, product(index_set_ab, index_set_b), generator);
         lemmas.insert(lemmas.end(), l.begin(), l.end());
       }
 
@@ -239,7 +247,7 @@ SCENARIO("instantiate_not_contains",
 
     // Create witness for axiom
     symbol_tablet symtab;
-    namespacet empty_ns(symtab);
+    const namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
     string_constraint_generatort generator(info, ns);
     generator.witness[vacuous]=
@@ -255,7 +263,7 @@ SCENARIO("instantiate_not_contains",
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas=instantiate_not_contains(
-        vacuous, index_set_a, index_set_a, generator);
+        vacuous, product(index_set_a, index_set_a), generator);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);
@@ -297,7 +305,7 @@ SCENARIO("instantiate_not_contains",
 
     // Create witness for axiom
     symbol_tablet symtab;
-    namespacet ns(symtab);
+    const namespacet ns(symtab);
     string_constraint_generatort::infot info;
     string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
@@ -314,7 +322,7 @@ SCENARIO("instantiate_not_contains",
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas=instantiate_not_contains(
-        trivial, index_set_a, index_set_b, generator);
+        trivial, product(index_set_a, index_set_b), generator);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);
@@ -356,7 +364,7 @@ SCENARIO("instantiate_not_contains",
 
     // Create witness for axiom
     symbol_tablet symtab;
-    namespacet empty_ns(symtab);
+    const namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
     string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
@@ -374,7 +382,7 @@ SCENARIO("instantiate_not_contains",
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas=instantiate_not_contains(
-        trivial, index_set_a, index_set_empty, generator);
+        trivial, product(index_set_a, index_set_empty), generator);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);
@@ -416,7 +424,7 @@ SCENARIO("instantiate_not_contains",
 
     // Create witness for axiom
     symbol_tablet symtab;
-    namespacet empty_ns(symtab);
+    const namespacet empty_ns(symtab);
 
     string_constraint_generatort::infot info;
     string_constraint_generatort generator(info, ns);
@@ -433,7 +441,7 @@ SCENARIO("instantiate_not_contains",
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas=instantiate_not_contains(
-        trivial, index_set_ab, index_set_ab, generator);
+        trivial, product(index_set_ab, index_set_ab), generator);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);
@@ -476,7 +484,7 @@ SCENARIO("instantiate_not_contains",
 
     // Create witness for axiom
     symbol_tablet symtab;
-    namespacet empty_ns(symtab);
+    const namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
     string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
@@ -493,7 +501,7 @@ SCENARIO("instantiate_not_contains",
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas=instantiate_not_contains(
-        trivial, index_set_ab, index_set_cd, generator);
+        trivial, product(index_set_ab, index_set_cd), generator);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);