[TG-634] Logical expression building utility #1424

LAJW · 2017-09-26T14:48:09Z

This PR implements an exprt wrapper for constructing logical expression hierarchies using C++ operators.

Additionally, this PR contains small refactor on one of the most used string functions to show that it's working as intended.

For example, it lets following code:

exprt res_length=plus_exprt( 
  s1.length(), minus_exprt(end_index, start_index));
binary_relation_exprt prem(end_index, ID_gt, start_index); 
implies_exprt a1(prem, equal_exprt(res.length(), res_length));

be expressed this way:

exprt a1 = end_index > start_index >>=
           axt(s1.length()) + end_index - start_index == axt(res.length());

Part 2 of String Refinement overhaul PR

LAJW · 2017-09-26T15:35:07Z

@reuk @jasigal @romainbrenguier Take a look if you have some spare time on your hands.

reuk

Nice and idiomatic 👍

jasigal

Looks good :)

jasigal · 2017-09-29T09:28:56Z

src/solvers/refinement/axt.h

+  axt operator==(const axt& rhs) const
+    { return axt(equal_exprt(expr_, rhs.expr_)); }
+  // Implication
+  axt operator>>=(const axt& rhs) const


Can we not use ->?

No, because -> is an unary operator. An alias for (*ptr).<method_name>

jasigal · 2017-09-29T09:30:02Z

src/solvers/refinement/axt.h

+  axt operator||(const axt& rhs) const
+  { return axt(or_exprt(expr_, rhs.expr_)); }
+  axt operator[](const axt& index) const
+  { return axt(to_string_expr(expr_)[index.expr_]); }


Why do we cast to a string expression? Is this only going to be for the string solver?

For now it's only used in the string solver, but ultimately this should represent index_of_exprt (taking an array_exprt on the left) this will be unified once the new version of the string solver is merged as strings will be represented by arrays.

romainbrenguier · 2017-09-29T09:26:35Z

src/solvers/refinement/axt.h

+  { return !(*this<rhs); }
+  axt operator<=(const axt& rhs) const
+  { return !(*this>rhs); }
+  axt operator==(const axt& rhs) const


could we also add != for notequal_exprt?

romainbrenguier · 2017-09-29T09:27:17Z

src/solvers/refinement/axt.h

+  axt operator||(const axt& rhs) const
+  { return axt(or_exprt(expr_, rhs.expr_)); }
+  axt operator[](const axt& index) const
+  { return axt(to_string_expr(expr_)[index.expr_]); }


We may want to use this for index_exprt in case it's not a string_exprt

I shall wait then until they become one and the same thing.

jasigal · 2017-09-29T09:50:00Z

src/solvers/refinement/axt.h

+  axt operator<(const axt& rhs) const
+  { return axt(binary_relation_exprt(expr_, ID_lt, rhs.expr_)); }
+  axt operator>=(const axt& rhs) const
+  { return !(*this<rhs); }


Should use axt(binary_relation_exprt(expr_, ID_ge, rhs.expr_))

jasigal · 2017-09-29T09:50:30Z

src/solvers/refinement/axt.h

+  axt operator>=(const axt& rhs) const
+  { return !(*this<rhs); }
+  axt operator<=(const axt& rhs) const
+  { return !(*this>rhs); }


Should use axt(binary_relation_exprt(expr_, ID_le, rhs.expr_))

martin-cs · 2017-10-02T08:13:37Z

We had this code; pretty much exactly. It was called oexpr and in util/oexpr.h. It was deleted by PR #347 : 2db625 as part of a clean up in moving to a new C++ version, having been marked as "old" 346495 .

As I recall, I thought of it and suggested it to Daniel on the basis you could have one piece of code that was both concrete or symbolic depending on the types used (of course you can also achieve this by doing everything symbolically and then constant folding via simply_expr, anyway, I thought I was clever at the time), he implemented it because, why not, it then sat there and wasn't used because it turns out to not be as useful as you'd originally think and then was removed because it wasn't being used.

I guess there are multiple conclusions one could draw from this story and I'll let you pick your own.

Implements an exprt wrapper for constructing logical and arithmetic expressions using C++ operators.

martin-cs

Over all ... I'm not convinced it gains us that much. A slight reduction in characters in long lines but that is traded against obfuscating what is symbolic and what is literal.

As I said before, I used to think this was a great idea but I've not yet seen a compelling use-case.

martin-cs · 2017-11-16T18:00:59Z

src/solvers/refinement/axt.h

+
+#include <util/expr.h>
+#include <util/string_expr.h>
+


I would have thought this would be happier in util/ as nothing it does is specific to refinement. Also, maybe we should just resurrect oexpr.

martin-cs · 2017-11-16T18:02:06Z

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -12,6 +12,7 @@ Author: Romain Brenguier, [email protected]
 ///   strings

 #include <solvers/refinement/string_constraint_generator.h>
+#include "axt.h"


Please include in the usual style.

martin-cs · 2017-11-16T18:02:23Z

src/solvers/refinement/string_constraint_generator_concat.cpp

+  const array_string_exprt &s1_,
+  const array_string_exprt &s2_,
+  const exprt &start_index_,
+  const exprt &end_index_)
 {


Why are these renamed?

LAJW · 2020-01-09T23:30:40Z

Change too controversial, was attempted before and rejected. Closing.

reuk approved these changes Sep 26, 2017

View reviewed changes

jasigal reviewed Sep 29, 2017

View reviewed changes

romainbrenguier reviewed Sep 29, 2017

View reviewed changes

jasigal suggested changes Sep 29, 2017

View reviewed changes

Lukasz A.J. Wrona added 2 commits November 16, 2017 08:22

Axt: exprt wrapper for logical operations

13f3271

Implements an exprt wrapper for constructing logical and arithmetic expressions using C++ operators.

Use axt in concat implementation

36c6946

LAJW requested review from martin-cs and peterschrammel as code owners November 16, 2017 08:30

martin-cs requested changes Nov 16, 2017

View reviewed changes

tautschnig assigned LAJW Nov 30, 2017

LAJW changed the title ~~TG-634 Logical expression building utility~~ [TG-634] Logical expression building utility Mar 14, 2018

LAJW closed this Jan 9, 2020

[TG-634] Logical expression building utility #1424

[TG-634] Logical expression building utility #1424

Uh oh!

Conversation

LAJW commented Sep 26, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

LAJW commented Sep 26, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

reuk left a comment

Choose a reason for hiding this comment

Uh oh!

jasigal left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Oct 2, 2017

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LAJW commented Jan 9, 2020

Uh oh!

Uh oh!

LAJW commented Sep 26, 2017 •

edited

Loading

LAJW commented Sep 26, 2017 •

edited

Loading