Merge pull request #2695 from romainbrenguier/clean-up/string-constraint-generator

Refactor string_constraint_generatort

Author: romainbrenguier

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -196,38 +196,40 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
     string_constraint_generatort generator(ns);
-    exprt res=generator.add_axioms_for_function_application(func);
+    const auto pair = generator.add_axioms_for_function_application(
+      generator.fresh_symbol, func);
+    const exprt &res = pair.first;
+    const string_constraintst &constraints = pair.second;
+
     std::string axioms;
     std::vector<string_not_contains_constraintt> nc_axioms;
+    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
 
-    const auto constraints = generator.get_constraints();
     std::accumulate(
-      constraints.begin(),
-      constraints.end(),
+      constraints.universal.begin(),
+      constraints.universal.end(),
       axioms,
       [&](const std::string &accu, string_constraintt sc) {
         simplify(sc.body, ns);
         return accu + to_string(sc) + "\n\n";
       });
 
-    const auto nc_contraints = generator.get_not_contains_constraints();
     axioms = std::accumulate(
-      nc_contraints.begin(),
-      nc_contraints.end(),
+      constraints.not_contains.begin(),
+      constraints.not_contains.end(),
       axioms,
       [&](const std::string &accu, string_not_contains_constraintt sc) {
         simplify(sc, ns);
-        generator.witness[sc] = generator.fresh_symbol("w", t.witness_type());
+        witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
         nc_axioms.push_back(sc);
         std::string s;
         java_lang->from_expr(sc, s, ns);
         return accu + s + "\n\n";
       });
 
-    const auto lemmas = generator.get_lemmas();
     axioms = std::accumulate(
-      lemmas.begin(),
-      lemmas.end(),
+      constraints.existential.begin(),
+      constraints.existential.end(),
       axioms,
       [&](const std::string &accu, exprt axiom) {
         simplify(axiom, ns);
@@ -251,8 +253,8 @@ SCENARIO("instantiate_not_contains",
       // Instantiate the lemmas
       for(const auto &axiom : nc_axioms)
       {
-        const std::vector<exprt> l=instantiate_not_contains(
-          axiom, product(index_set_ab, index_set_b), generator);
+        const std::vector<exprt> l = instantiate_not_contains(
+          axiom, product(index_set_ab, index_set_b), witnesses);
         lemmas.insert(lemmas.end(), l.begin(), l.end());
       }
 
@@ -294,8 +296,8 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
     string_constraint_generatort generator(ns);
-    generator.witness[vacuous]=
-      generator.fresh_symbol("w", t.witness_type());
+    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
     std::string s;
@@ -308,8 +310,8 @@ SCENARIO("instantiate_not_contains",
       const std::set<exprt> index_set_a = full_index_set(a_array);
 
       // Instantiate the lemmas
-      std::vector<exprt> lemmas=instantiate_not_contains(
-        vacuous, product(index_set_a, index_set_a), generator);
+      std::vector<exprt> lemmas = instantiate_not_contains(
+        vacuous, product(index_set_a, index_set_a), witnesses);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);
@@ -349,8 +351,8 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     const namespacet ns(symtab);
     string_constraint_generatort generator(ns);
-    generator.witness[trivial]=
-      generator.fresh_symbol("w", t.witness_type());
+    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
     std::string s;
@@ -364,8 +366,8 @@ SCENARIO("instantiate_not_contains",
       const std::set<exprt> index_set_b = full_index_set(b_array);
 
       // Instantiate the lemmas
-      std::vector<exprt> lemmas=instantiate_not_contains(
-        trivial, product(index_set_a, index_set_b), generator);
+      std::vector<exprt> lemmas = instantiate_not_contains(
+        trivial, product(index_set_a, index_set_b), witnesses);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);
@@ -405,8 +407,8 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
     string_constraint_generatort generator(ns);
-    generator.witness[trivial]=
-      generator.fresh_symbol("w", t.witness_type());
+    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
     std::string s;
@@ -417,12 +419,12 @@ SCENARIO("instantiate_not_contains",
     {
       // Making index sets
       const std::set<exprt> index_set_a = full_index_set(a_array);
-      const std::set<exprt> index_set_empty=
-        {generator.fresh_exist_index("z", t.length_type())};
+      const std::set<exprt> index_set_empty = {
+        generator.fresh_symbol("z", t.length_type())};
 
       // Instantiate the lemmas
-      std::vector<exprt> lemmas=instantiate_not_contains(
-        trivial, product(index_set_a, index_set_empty), generator);
+      std::vector<exprt> lemmas = instantiate_not_contains(
+        trivial, product(index_set_a, index_set_empty), witnesses);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);
@@ -464,8 +466,8 @@ SCENARIO("instantiate_not_contains",
     const namespacet empty_ns(symtab);
 
     string_constraint_generatort generator(ns);
-    generator.witness[trivial]=
-      generator.fresh_symbol("w", t.witness_type());
+    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
     std::string s;
@@ -478,8 +480,8 @@ SCENARIO("instantiate_not_contains",
       const std::set<exprt> index_set_ab = full_index_set(ab_array);
 
       // Instantiate the lemmas
-      std::vector<exprt> lemmas=instantiate_not_contains(
-        trivial, product(index_set_ab, index_set_ab), generator);
+      std::vector<exprt> lemmas = instantiate_not_contains(
+        trivial, product(index_set_ab, index_set_ab), witnesses);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);
@@ -520,8 +522,8 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
     string_constraint_generatort generator(ns);
-    generator.witness[trivial]=
-      generator.fresh_symbol("w", t.witness_type());
+    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
     std::string s;
@@ -535,8 +537,8 @@ SCENARIO("instantiate_not_contains",
       const std::set<exprt> index_set_cd = full_index_set(cd_array);
 
       // Instantiate the lemmas
-      std::vector<exprt> lemmas=instantiate_not_contains(
-        trivial, product(index_set_ab, index_set_cd), generator);
+      std::vector<exprt> lemmas = instantiate_not_contains(
+        trivial, product(index_set_ab, index_set_cd), witnesses);
 
       const exprt conj=combine_lemmas(lemmas, ns);
       const std::string info=create_info(lemmas, ns);