TG-634 Functional style for string refinement #1404

LAJW · 2017-09-19T08:18:39Z

Replaces private member functions of string refinement with free local functions

String refinement overhaul pt.1
@jasigal @romainbrenguier Please, review

jasigal · 2017-09-19T10:03:56Z

src/solvers/refinement/string_constraint_generator.h

    /// Max length of non-deterministic strings
    size_t string_max_length=std::numeric_limits<size_t>::max();
    /// Prefer printable characters in non-deterministic strings
    bool string_printable=false;
  };

-  explicit string_constraint_generatort(const infot& info);
+  explicit string_constraint_generatort(
+    const infot& info, const namespacet& ns);


The other infot structs contain all needed constructor arguments. An exception is warranted here because namespacet in string_constraint_generatort is used only for debug printing, whereas in other classes it has a "real" use. Hence, in order to avoid inheritance namespace collisions with infots, namespacet is excluded.

romainbrenguier

Very good. Although some functions end up with lots of arguments, ultimately we should find a way of avoiding that.

romainbrenguier · 2017-09-19T10:23:13Z

src/solvers/refinement/string_constraint_generator.h

    /// Max length of non-deterministic strings
    size_t string_max_length=std::numeric_limits<size_t>::max();
    /// Prefer printable characters in non-deterministic strings
    bool string_printable=false;
  };

-  explicit string_constraint_generatort(const infot& info);
+  explicit string_constraint_generatort(


explicit not needed there

romainbrenguier · 2017-09-19T10:47:53Z

src/solvers/refinement/string_refinement.cpp

+}
+
+template<typename T>
+T expr_cast_v(const exprt& expr)


_v for value

romainbrenguier · 2017-09-19T10:51:49Z

src/solvers/refinement/string_refinement.cpp

@@ -221,13 +362,14 @@ void string_refinementt::set_char_array_equality(
 /// remove functions applications and create the necessary axioms
 /// \par parameters: an expression containing function applications
 /// \return an expression containing no function application
-exprt string_refinementt::substitute_function_applications(exprt expr)
+exprt substitute_function_applications(
+  string_constraint_generatort& generator, exprt expr)


This could go to the string_constraint_generatort class

expr can be made const.

expr is modified in this function.

romainbrenguier · 2017-09-19T10:59:36Z

src/solvers/refinement/string_refinement.cpp

+    stream << violated.size()
+           << " universal string axioms can be violated" << eom;
+    stream << violated_not_contains.size()
+           << " not_contains string axioms can be violated" << eom;

    if(use_counter_example)


lemmas is non-empty only when we use counter examples. Maybe we should get this block out in a separate function which would be called when use_counter_example is true

check_axioms can be separated into 3-4 smaller functions. I wanted to restrict changes in this PR.

romainbrenguier · 2017-09-19T11:27:27Z

src/solvers/refinement/string_refinement.cpp

@@ -1417,8 +1713,8 @@ exprt string_refinementt::compute_inverse_function(
      string_refinement_invariantt("a proper function must have exactly one "
        "occurrences after reduction, or it canceled out, and it does not have "
        " one"));
-    debug() << "in string_refinementt::compute_inverse_function:"
-            << " warning: occurrences of qvar canceled out " << eom;
+    // debug() << "in string_refinementt::compute_inverse_function:"


use #if 0 to comment code and actually this one can be removed

romainbrenguier · 2017-09-19T11:28:53Z

src/solvers/refinement/string_refinement.cpp

+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const exprt &s, exprt i)


exprt i should be on a new line

romainbrenguier · 2017-09-19T11:38:52Z

src/solvers/refinement/string_refinement.cpp

 {
  simplify(i, ns);
-  if(i.id()==ID_constant)
+  if(i.id()!=ID_constant || expr_cast<size_t>(i))


to preserve the semantic expr_cast<size_t>(i) should be compared using >= 0

size_t is unsigned, no need to do that comparison. If expression evaluates to something smaller than 0, it will return an empty optional, which will evaluate to false.

I think that process is too implicit, I would appreciate if it was slightly longer, for example assigning expr_cast<size_t>(i) to a descriptive variable, e.g. is_nonneg_size.

romainbrenguier · 2017-09-19T11:40:20Z

src/solvers/refinement/string_refinement.cpp

-
-  return ::instantiate_not_contains(
-    axiom, index_set0, index_set1, generator);
+  // debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : "


remove or use #if 0 or #ifdef DEBUG

romainbrenguier · 2017-09-19T11:44:33Z

src/solvers/refinement/string_refinement.cpp

+  ui_message_handlert::uit ui,
+  const exprt &axiom,
+  const symbol_exprt& var,
+  exprt &witness)


Could be made to return an optional witness instead of a bool and affecting the reference. But then for clarity it should be renamed something like find_counter_example

jasigal

Great changes finally.

jasigal · 2017-09-19T10:14:18Z

src/solvers/refinement/string_refinement.h


  exprt get(const exprt &expr) const override;
-
-protected:
+  void set_to(const exprt &expr, bool value) override;


To quote CLion: virtual is redundant since the function is already declared override.

virtual removed.

jasigal · 2017-09-19T12:01:19Z

src/solvers/refinement/string_refinement.cpp

@@ -221,13 +362,14 @@ void string_refinementt::set_char_array_equality(
 /// remove functions applications and create the necessary axioms
 /// \par parameters: an expression containing function applications
 /// \return an expression containing no function application
-exprt string_refinementt::substitute_function_applications(exprt expr)
+exprt substitute_function_applications(
+  string_constraint_generatort& generator, exprt expr)


expr can be made const.

jasigal · 2017-09-19T12:10:35Z

src/solvers/refinement/string_refinement.cpp

    found_content[content]=arr;
  }
 }

 /// For each string whose length has been solved, add constants to the index set
 /// to force the solver to pick concrete values for each character, and fill the
 /// map `found_length`
-void string_refinementt::concretize_results()
+std::vector<exprt> concretize_results(


get and max_string_length can be made const.

jasigal · 2017-09-19T12:11:22Z

src/solvers/refinement/string_refinement.cpp

@@ -326,85 +469,126 @@ std::size_t expr_cast<std::size_t>(const exprt& val_expr)
 /// same value as the next index that is present in the index set.
 /// We do so by traversing the array backward, remembering the
 /// last value that has been initialized.
-void string_refinementt::concretize_string(const exprt &expr)
+static void concretize_string(


get and max_string_length can be made const.

Arguments have been made const.

jasigal · 2017-09-19T12:12:13Z

src/solvers/refinement/string_refinement.cpp

 }

 /// For each string whose length has been solved, add constants to the map
 /// `found_length`
-void string_refinementt::concretize_lengths()
+void concretize_lengths(


get can be const.

Argument has been made const.

jasigal · 2017-09-19T12:42:51Z

src/solvers/refinement/string_refinement.cpp

@@ -777,62 +1046,73 @@ std::string string_refinementt::string_of_array(const array_exprt &arr)

 /// Display part of the current model by mapping the variables created by the
 /// solver to constant expressions given by the current model
-void string_refinementt::debug_model()
+void debug_model(


super_get and max_string_length can be const.

Arguments have been made const (it would be helpful if those comments were just below those non-const arguments, rather than at the top of the function).

jasigal · 2017-09-19T12:43:04Z

src/solvers/refinement/string_refinement.cpp

  const std::string indent("  ");
  for(auto it : symbol_resolve)
  {
-    if(is_refined_string_type(it.second.type()))
+    if(const auto refined=expr_cast<string_exprt>(it.second))


Maybe add clarifying comment as mentioned before.

jasigal · 2017-09-19T12:50:46Z

src/solvers/refinement/string_refinement.cpp

 {
  simplify(i, ns);
-  if(i.id()==ID_constant)
+  if(i.id()!=ID_constant || expr_cast<size_t>(i))


I think that process is too implicit, I would appreciate if it was slightly longer, for example assigning expr_cast<size_t>(i) to a descriptive variable, e.g. is_nonneg_size.

jasigal · 2017-09-19T12:55:56Z

src/solvers/refinement/string_refinement.cpp

 {
  satcheck_no_simplifiert sat_check;
-  supert::infot info;
+  bv_refinementt::infot info;


Should keep supert.

Can't do that. Either this or string_refinementt::supert.

Then the second option I'd say.

jasigal · 2017-09-19T12:56:09Z

src/solvers/refinement/string_refinement.cpp

  info.ns=&ns;
  info.prop=&sat_check;
  info.refine_arithmetic=true;
  info.refine_arrays=true;
  info.max_node_refinement=5;
  info.ui=ui;
-  supert solver(info);
+  bv_refinementt solver(info);


Should keep supert.

Can't do that. Either this or string_refinementt::supert.

Then the second option I'd say.

LAJW · 2017-09-19T15:36:47Z

Changes applied or commented. Re-review please.

jasigal

LGTM

peterschrammel · 2017-09-19T15:28:29Z

src/solvers/refinement/bv_refinement_loop.cpp

  progress(false),
-  ui(info.ui)
+  config_(info)


The underscore seems unnecessary.

peterschrammel · 2017-09-19T15:30:45Z

src/solvers/refinement/bv_refinement_loop.cpp

@@ -44,7 +41,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
    status() << "BV-Refinement: iteration " << iteration << eom;

    // output the very same information in a structured fashion
-    if(ui==ui_message_handlert::uit::XML_UI)
+    if(config_.ui==ui_message_handlert::uit::XML_UI)
    {
      xmlt xml("refinement-iteration");
      xml.data=std::to_string(iteration);


(improvement) replace cout by status() << xml;

does this not require a status() << preformatted_output() << xml @peterschrammel?

I don't think it's relevant, there was no preprocessing before.

peterschrammel · 2017-09-19T16:02:42Z

src/solvers/refinement/string_constraint_generator_main.cpp

+  const exprt& expr)
+{
+  exprt copy=expr;
+  for(size_t i=0; i<copy.operands().size(); ++i)


ranged for?

~~i is used.~~

peterschrammel · 2017-09-19T16:04:56Z

src/solvers/refinement/string_refinement.cpp

+    for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
+    {
+      const std::size_t index=it->first;
+      const T value=it->second;


peterschrammel · 2017-09-19T16:05:26Z

src/solvers/refinement/string_refinement.cpp

-void string_refinementt::display_index_set()
+static void display_index_set(
+  messaget::mstreamt stream,
+  const namespacet& ns,


peterschrammel · 2017-09-19T16:08:35Z

src/solvers/refinement/string_refinement.cpp

-    const string_exprt str=to_string_expr(expr);
-    const exprt length=get(str.length());
-    exprt content=str.content();
+    const auto& eom=messaget::eom;


What's the point of that?

eom's used quite often, will store as value.

peterschrammel · 2017-09-19T16:09:33Z

src/solvers/refinement/string_refinement.cpp

+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const std::set<string_exprt> &created_strings,
+  const std::map<exprt, std::set<exprt>>& current_index_set,


&current_index_set

peterschrammel · 2017-09-19T16:10:20Z

src/solvers/refinement/string_refinement.cpp

+        ns,
+        lhs,
+        subst_rhs);
+      for(const auto& lemma : lemmas)


peterschrammel · 2017-09-19T16:10:33Z

src/solvers/refinement/string_refinement.cpp

@@ -533,42 +719,84 @@ decision_proceduret::resultt string_refinementt::dec_solve()
  found_length.clear();
  found_content.clear();

+  const auto get = [this](const exprt& expr) { return this->get(expr); };


no spaces around =

peterschrammel · 2017-09-19T16:11:06Z

src/solvers/refinement/string_refinement.cpp

  cur.clear();
-  add_instantiations();
+  for(const auto& lemma :


peterschrammel · 2017-09-19T16:12:02Z

src/solvers/refinement/string_refinement.h

-  unsigned initial_loop_bound;
-
+  const configt config_;
+  unsigned loop_bound_;


use size_t
no underscore suffixes

But we already agreed on underscore suffixes ;(

I think we should at least consider underscore suffixes for data members in new code. It makes it much easier to differentiate data members from global data or method parameters.

peterschrammel · 2017-09-19T16:13:34Z

src/solvers/refinement/string_refinement.cpp

      cur.clear();
-      add_instantiations();
+      for(const auto& lemma :
+            generate_instantiations(


assign to a separate variable for clarity

peterschrammel · 2017-09-19T16:13:46Z

src/solvers/refinement/string_refinement.cpp

+            generator.get_created_strings(),
+            current_index_set,
+            universal_axioms);
+          for(const auto& lemma : lemmas)


peterschrammel · 2017-09-19T16:14:03Z

src/solvers/refinement/string_refinement.cpp

@@ -598,18 +844,20 @@ decision_proceduret::resultt string_refinementt::dec_solve()
        }
      }

-      display_index_set();
+      display_index_set(debug(), ns, current_index_set, index_set);
      debug()<< "instantiating NOT_CONTAINS constraints" << eom;
      for(unsigned i=0; i<not_contains_axioms.size(); i++)
      {
        debug()<< "constraint " << i << eom;


peterschrammel · 2017-09-19T16:14:26Z

src/solvers/refinement/string_refinement.cpp

@@ -665,10 +912,15 @@ void string_refinementt::add_lemma(
 /// \par parameters: an expression representing an array and an expression
 /// representing an integer
 /// \return an array expression or an array_of_exprt
-exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
+static exprt get_array(
+  const std::function<exprt(const exprt&)> super_get,


peterschrammel · 2017-09-19T16:21:03Z

src/solvers/refinement/string_refinement.cpp

+/// \return: the witness of the satisfying assignment if one
+/// exists. If UNSAT, then behaviour is undefined.
+static optionalt<exprt> find_counter_example(
+  const namespacet& ns,


peterschrammel · 2017-09-19T16:21:10Z

src/solvers/refinement/string_refinement.cpp

+  const namespacet& ns,
+  const ui_message_handlert::uit ui,
+  const exprt &axiom,
+  const symbol_exprt& var)


peterschrammel · 2017-09-19T16:21:28Z

src/solvers/refinement/string_refinement.cpp

@@ -1887,21 +2198,24 @@ static bool universal_only_in_index(const string_constraintt &expr)
 /// \related string_constraintt
 /// \param [in] expr: the string constraint to check
 /// \return whether the constraint satisfies the invariant
-bool string_refinementt::is_valid_string_constraint(
+static bool is_valid_string_constraint(
+  messaget::mstreamt& stream,


peterschrammel · 2017-09-19T16:21:34Z

src/solvers/refinement/string_refinement.cpp

-bool string_refinementt::is_valid_string_constraint(
+static bool is_valid_string_constraint(
+  messaget::mstreamt& stream,
+  const namespacet& ns,


peterschrammel · 2017-09-19T16:21:42Z

src/solvers/refinement/string_refinement.cpp

  const string_constraintt &expr)
 {
+  const auto eom = messaget::eom;


no spaces around =

peterschrammel · 2017-09-19T16:47:05Z

src/solvers/refinement/bv_refinement.h

+public:
+  struct infot:public configt
+  {
+    const namespacet *ns=nullptr;


Making this hold a reference would be better instead of reintroducing pointers...

This is the solution to the problem of functions requiring too many arguments. Either we'd use this (essence pattern) or the builder pattern. Both of which use null pointers to hold the default value for a reference (but builder is more verbose, restricted to constructors only and not composable).

The only solution that allows usage of both arguments and references at the same time, are C++20 named arguments.

LAJW · 2017-09-20T09:56:03Z

@peterschrammel Your comments have been addressed.

d0d3620 Merge remote-tracking branch 'upstream/develop' into security-scanner-support 875d554 Merge branch 'develop' of github.com:diffblue/cbmc into develop 3a06eda don't rely on index expressions to be vector or arrays 6d6e1df Merge pull request diffblue#1407 from jasigal/fix/instantiate-not-contains#TG-592 8da3eef Merge pull request diffblue#1414 from antlechner/antonia/Character 0b56d97 Fix signatures for methods in java.lang.Character e4e2b10 TG-592 Implemented the correct instantiation procedure for not contains constraints ae83e4e Added install command for required projects. 0e70863 Merge pull request diffblue#1279 from NathanJPhillips/feature/expr_dynamic_cast 1e9837e Merge pull request diffblue#1405 from smowton/cleanup/remove_instanceof 7eb3c76 Merge pull request diffblue#1411 from diffblue/revert-1322-feature/java_support_generics 3b3fee3 Revert "TG-374 Feature/java support generics" 0e14431 Merge pull request diffblue#1408 from reuk/reuk/regression-filenames 2ddb0bc Simplify remove_instanceof logic b4f57ee Merge pull request diffblue#1410 from LAJW/fix-test-gen bcfb914 Remove invariant causing failure in unit test generation involving CharSequences 93149be Merge pull request diffblue#1322 from mgudemann/feature/java_support_generics c731b98 Merge pull request diffblue#1404 from LAJW/string-refinement-functional e5f5e8b Use `optionalt` for signature f68e817 Parse LocalVariabletypetable / Signature attributes use in types 585fb66 Merge pull request diffblue#1400 from reuk/reuk/enable-compile-commands da4df03 Switch from pointers to optionalt 413fc1b Automatically deduce test names from dir names 05d5a9b Address commenters' suggestions c48170e Merge pull request diffblue#192 from diffblue/smowton/feature/split_frontend_final_stage 0823f05 allow goto-cc -E 00cbad7 test for va_args 96f2d9e Added a PRECONDITION assert/invariant b8ab624 Code review fixup 775d9dd Renamed can_cast_expr c372eb3 Used typeinfo functions instead of rolling own 95f6505 Comment on types for which expr_dynamic_cast is not implemented d35710f Made validate_expr non-template de8a8d0 Implementation of expr_dynamic_cast f763691 Tidy up remove_instanceof f4df5c6 Add tests for mixed GOTO and C input 215d5bf Split the entry-point-generation phase into two parts ab347d5 Merge pull request diffblue#195 from diffblue/bugfix/missing-const_cast 73fba6e Fixed missing const_cast 751e8f5 Adhere to lintage b544a4b Fix unit test build 9b8a025 Fix get lambdas bee20f1 Remove unused add_lemma parameter d03866d static add axioms for string assings 1531f0e static debug_model f5c1b29 static get_array 7f11ccf static set_char_array_equality 229568a static Instantiate not contains 78303df Static concretize strings, lengths and results 918297c static concretize length a4c8cf5 Static index set functions e5e1ff4 static index_set functions 65ad3db Public methods made public 2eed573 Static add_axioms for strings 666c146 make static check_axioms bcd6111 Static is_axiom_sat 01b8301 static is_valid_string_constraint cfb47db Remove unused functions from string_refinement header 8e69d6d Make functions static 0cec13d Merge pull request diffblue#1360 from KPouliasis/konst_splice_call 9f9f30d fixup return value eaf97f6 Simplify remove_instanceof logic bc30987 Merge pull request diffblue#1235 from romainbrenguier/feature/string-max-input-length#948 0323ed0 Merge pull request diffblue#1349 from peterschrammel/cleanup/use-preformatted-output 621da87 Tests for new option string-max-input-length 440d19f Adding string max input length option e957025 Print results to result stream instead of status ad6484e Print XML and JSON objects on message stream 4969295 Tidy up remove_instanceof 6cb2f90 Merge pull request diffblue#1398 from diffblue/json_direct_return f365afe Merge pull request diffblue#1392 from reuk/reuk/fixup-appveyor-regressions 4a1565b Enable compile command output 523f028 Merge pull request diffblue#1368 from diffblue/use_size_t 358b435 prefer a ranged for over indexed iteration 69a8eaf use std::size_t for container indices cef7659 counters need to be size_t 2a7a0e8 the step number needs to be a size_t 9d48225 json_irept now returns ireps and jsont directly f22a864 Merge pull request diffblue#1386 from diffblue/return_directly 2b050a0 Merge pull request diffblue#1372 from diffblue/preconditions 6a509a8 goto-instrument no longer needs partial inlining by default e3f75d3 fixup coverage tests 1ff6bf2 missing include ac022e2 inlined functions are no longer ignored when doing coverage 4cb72b3 check error message in test 3a4ebeb use preconditions in the library f443b18 partial inlining is no longer needed 5624b15 instrumentation for preconditions 54e80da added __CPROVER_precondtion(c, d) 1d81035 Merge pull request diffblue#1393 from diffblue/byte_extract_is_binary 4e1fe93 Merge pull request diffblue#1396 from diffblue/String6-fixup 9497b02 Merge pull request diffblue#1395 from diffblue/msvc_unistd 17c6ca0 MSVC doesn't have strcasecmp and strncasecmp; use header for free() 237b31a Visual Studio doesn't have unistd.h; signal.h isn't needed for the MSVC build 5ef9c17 Revert 20e4def (preformatted_output flag) 3d4c794 Pass ostream instead of using cout in natural_loops 2716410 Update linter to cope with CBMC subtree 63fc53b Stop using sed to modify scripts! 58b75cf Merge pull request diffblue#1307 from zemanlx/coverity da91319 Adapt to upstream change in write_goto_binary interface and languaget 177a13d Add Coverity scan 22fb7c1 added splice-call feature in goto instrument It prepends a nullary function call say foo in the body of another call say moo when called as --splice-call moo,foo added tests a400c23 Merge pull request diffblue#1387 from thk123/feature/disable-mac-builds 68f2862 byte_extract expressions are binary expressions ec6ad09 Merge pull request diffblue#1379 from diffblue/remove-symex 1c1d3c2 remove path-symex and the symex tool f96ff48 Merge pull request diffblue#1384 from thk123/bugfix/regresssion-makefile 785bf43 Disable OSX builds 428b985 return STL containers directly for some variants of compute_called_functions 4bdd9c4 Corrected regression makefile 2b2a841 Convert display_index_set to a free function 9fff116 Remove constructor boilerplate 150bab1 Group string_refinement arguments 317c1c6 Group bv_refinement config variables bf47f81 Use expr_cast in string_exprt casts c5fa708 Refactor integer conversions f99c8ff Replace exceptions with optional git-subtree-dir: cbmc git-subtree-split: d0d3620

Lukasz A.J. Wrona added 26 commits September 12, 2017 17:15

Replace exceptions with optional

f99c8ff

Refactor integer conversions

c5fa708

Use expr_cast in string_exprt casts

bf47f81

Group bv_refinement config variables

317c1c6

Group string_refinement arguments

150bab1

Remove constructor boilerplate

9fff116

Convert display_index_set to a free function

2b2a841

Make functions static

8e69d6d

Remove unused functions from string_refinement header

cfb47db

static is_valid_string_constraint

01b8301

Static is_axiom_sat

bcd6111

make static check_axioms

666c146

Static add_axioms for strings

2eed573

Public methods made public

65ad3db

static index_set functions

e5e1ff4

Static index set functions

a4c8cf5

static concretize length

918297c

Static concretize strings, lengths and results

78303df

static Instantiate not contains

229568a

static set_char_array_equality

7f11ccf

static get_array

f5c1b29

static debug_model

1531f0e

static add axioms for string assings

d03866d

Remove unused add_lemma parameter

bee20f1

Fix get lambdas

9b8a025

Fix unit test build

b544a4b

LAJW mentioned this pull request Sep 19, 2017

[Don't Merge] TG-634 String refinement overhaul #1399

Closed

Adhere to lintage

751e8f5

romainbrenguier requested review from jasigal and romainbrenguier September 19, 2017 09:17

jasigal reviewed Sep 19, 2017

View reviewed changes

romainbrenguier suggested changes Sep 19, 2017

View reviewed changes

jasigal suggested changes Sep 19, 2017

View reviewed changes

jasigal approved these changes Sep 19, 2017

View reviewed changes

peterschrammel requested changes Sep 19, 2017

View reviewed changes

peterschrammel reviewed Sep 19, 2017

View reviewed changes

romainbrenguier approved these changes Sep 19, 2017

View reviewed changes

Address commenters' suggestions

05d5a9b

peterschrammel approved these changes Sep 20, 2017

View reviewed changes

thk123 merged commit c731b98 into diffblue:develop Sep 20, 2017

TG-634 Functional style for string refinement #1404

TG-634 Functional style for string refinement #1404

Conversation

LAJW commented Sep 19, 2017

Choose a reason for hiding this comment

romainbrenguier left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW Sep 19, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jasigal left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW Sep 19, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW Sep 19, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW commented Sep 19, 2017

jasigal left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW Sep 19, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW Sep 20, 2017 • edited Loading

Choose a reason for hiding this comment

LAJW Sep 19, 2017 •

edited

Loading

LAJW Sep 19, 2017 •

edited

Loading

LAJW Sep 19, 2017 •

edited

Loading

LAJW Sep 19, 2017 •

edited

Loading

LAJW Sep 20, 2017 •

edited

Loading