Merge pull request #1407 from jasigal/fix/instantiate-not-contains#TG-592

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

Author: kroening

src/solvers/refinement/string_constraint_instantiation.cpp

@@ -11,61 +11,46 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 
 #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, jesse.sigal@diffblue.com
 
 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);