Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Declare all Bool combinator equations simplifications (to disambiguate cases) #3786

Closed
wants to merge 5 commits into from
+45 −45
Closed

Declare all Bool combinator equations simplifications (to disambiguate cases) #3786

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e07bf61
domains.md: remove trailing whitespace
jberthold Nov 1, 2023
12d5ffd
Mark rules focussing on 2nd arg of Bool combinators as simplifications
jberthold Nov 1, 2023
2b93d97
declare _all_ operations simplifications (all op.s are hooked anyway)
jberthold Nov 2, 2023
e6259dd
Text in domains.md: add b to backends
jberthold Nov 2, 2023
6e20118
Merge branch 'develop' into jb/disambiguate-bool-combinator-rules
jberthold Nov 2, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
90 changes: 45 additions & 45 deletions k-distribution/include/kframework/builtin/domains.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -303,7 +303,7 @@ effectively constant.

You can remove the key/value pairs in a map that are present in another map in
O(N*log(M)) time (where M is the size of the first map and N is the size of the
second), or effectively linear. Note that only keys whose value is the same
second), or effectively linear. Note that only keys whose value is the same
in both maps are removed. To remove all the keys in one map from another map,
you can say `removeAll(M1, keys(M2))`.

Expand Down Expand Up @@ -489,7 +489,7 @@ module RANGEMAP

```k
syntax Range ::= "[" KItem "," KItem ")" [klabel(Rangemap:Range), symbol]

syntax RangeMap [hook(RANGEMAP.RangeMap)]
```

Expand Down Expand Up @@ -686,7 +686,7 @@ endmodule
Sets
----

Provided here is the syntax of an implementation of immutable, associative,
Provided here is the syntax of an implementation of immutable, associative,
commutative sets of `KItem`. This type is hooked to an implementation of sets
provided by the backend. For more information on matching on sets and allowable
patterns for doing so, refer to K's
Expand Down Expand Up @@ -741,7 +741,7 @@ An element of a `Set` is constructed via the `SetItem` operator.

You can compute the union of two sets in O(N*log(M)) time (Where N is the size
of the smaller set). Note that the base of the logarithm is a relatively high
number and thus the time is effectively linear. The union consists of all the
number and thus the time is effectively linear. The union consists of all the
elements present in either set.

```k
Expand Down Expand Up @@ -1093,8 +1093,8 @@ You can:
* Check inequality of two boolean values.

Note that only `andThenBool` and `orElseBool` are short-circuiting. `andBool`
and `orBool` may be short-circuited in concrete backends, but in symbolic
ackends, both arguments will be evaluated.
and `orBool` may be short-circuited in concrete backends, but in symbolic
backends, both arguments will be evaluated.

```k
syntax Bool ::= "notBool" Bool [function, total, klabel(notBool_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Bool}{#1}), hook(BOOL.not)]
Expand All @@ -1107,6 +1107,7 @@ ackends, both arguments will be evaluated.
> left:
Bool "==Bool" Bool [function, total, klabel(_==Bool_), symbol, left, comm, smt-hook(=), hook(BOOL.eq)]
| Bool "=/=Bool" Bool [function, total, klabel(_=/=Bool_), symbol, left, comm, smt-hook(distinct), hook(BOOL.ne)]
endmodule
```

### Implementation of Booleans
Expand All @@ -1115,43 +1116,42 @@ The remainder of this section consists of an implementation in K of the
operations listed above.

```k
module BOOL-KORE [kore, symbolic]
imports BOOL-COMMON

rule notBool true => false
rule notBool false => true

rule true andBool B:Bool => B:Bool
rule B:Bool andBool true => B:Bool
rule false andBool _:Bool => false
rule _:Bool andBool false => false

rule true andThenBool K::Bool => K
rule K::Bool andThenBool true => K
rule false andThenBool _ => false
rule _ andThenBool false => false
rule true andBool B:Bool => B:Bool [simplification]
rule B:Bool andBool true => B:Bool [simplification]
rule false andBool _:Bool => false [simplification]
rule _:Bool andBool false => false [simplification]
Comment on lines +1125 to +1128
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we mark them all as simplification rules? I guess this is so that we will always optimistically try them, allowing any of them to apply? My intuition would be to provide a set of complete rules for booleans (non simplification), then add simplification rules as well as needed.

So maybe we have a sepraate module with a set of complete and mutually exclusive rules for boolean (for concrete simplifications)?

rule true andBool B => B
rule false andBool _ => false
rule notBool true => false
rule notBool false => true
rule true orBool _ => true
rule false orBool B => B
....

Then have this separate module with all the rules as simplificatino rules.

Maybe there should also be a way for the user to declare that this set of rules are confluent, so that the booster can just assume that?

Copy link
Member Author

@jberthold jberthold Nov 2, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That would be possible, too. I don' thave a full set of measurements for it but I tested the performance for a variant where all rules that focus on the 2nd argument were declared [simplification], leaving the other rules (the ones you quote above, focussing on the 1st arg) as they were.

OTOH all these rules become obsolete as soon as a backend with an implemented hook is used. Therefore I kept all rules together in one module and made them all [simplification] for homogenous appearance.
If the variant with both simplification rules and defining equations is desired, I can change the code.


rule false xorBool B:Bool => B:Bool
rule B:Bool xorBool false => B:Bool
rule B:Bool xorBool B:Bool => false
rule true andThenBool K::Bool => K [simplification]
rule K::Bool andThenBool true => K [simplification]
rule false andThenBool _ => false [simplification]
rule _ andThenBool false => false [simplification]

rule true orBool _:Bool => true
rule _:Bool orBool true => true
rule false orBool B:Bool => B
rule B:Bool orBool false => B
rule false xorBool B:Bool => B:Bool [simplification]
rule B:Bool xorBool false => B:Bool [simplification]
rule B:Bool xorBool B:Bool => false [simplification]

rule true orElseBool _ => true
rule _ orElseBool true => true
rule false orElseBool K::Bool => K
rule K::Bool orElseBool false => K
rule true orBool _:Bool => true [simplification]
rule _:Bool orBool true => true [simplification]
rule false orBool B:Bool => B [simplification]
rule B:Bool orBool false => B [simplification]

rule true impliesBool B:Bool => B
rule false impliesBool _:Bool => true
rule _:Bool impliesBool true => true
rule B:Bool impliesBool false => notBool B
rule true orElseBool _ => true [simplification]
rule _ orElseBool true => true [simplification]
rule false orElseBool K::Bool => K [simplification]
rule K::Bool orElseBool false => K [simplification]

rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2)
endmodule
rule true impliesBool B:Bool => B [simplification]
rule false impliesBool _:Bool => true [simplification]
rule _:Bool impliesBool true => true [simplification]
rule B:Bool impliesBool false => notBool B [simplification]

module BOOL-KORE [kore, symbolic]
imports BOOL-COMMON
rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2) [simplification]

rule {true #Equals notBool @B} => {false #Equals @B} [simplification]
rule {notBool @B #Equals true} => {@B #Equals false} [simplification]
Expand Down Expand Up @@ -1311,7 +1311,7 @@ greater than or equal to, greater than, equal, or unequal to another integer.

### Divides

You can compute whether one integer evenly divides another. This is the
You can compute whether one integer evenly divides another. This is the
case when the second integer modulo the first integer is equal to zero.

```k
Expand Down Expand Up @@ -1439,14 +1439,14 @@ IEEE 754 Floating-point Numbers

Provided here is the syntax of an implementation of arbitrary-precision
floating-point arithmetic in K based on a generalization of the IEEE 754
standard. This type is hooked to an implementation of floats provided by the
standard. This type is hooked to an implementation of floats provided by the
backend.

The syntax of ordinary floating-point values in K consists of an optional sign
(+ or -) followed by an optional integer part, followed by a decimal point,
followed by an optional fractional part. Either the integer part or the
followed by an optional fractional part. Either the integer part or the
fractional part must be specified. The mantissa is followed by an optional
exponent part, which consists of an `e` or `E`, an optional sign (+ or -),
exponent part, which consists of an `e` or `E`, an optional sign (+ or -),
and an integer. The expoennt is followed by an optional suffix, which can be
either `f`, `F`, `d`, `D`, or `pNxM` where `N` and `M` are positive integers.
`p` and `x` can be either upper or lowercase.
Expand Down Expand Up @@ -2455,7 +2455,7 @@ known to K, `#unknownIOError` is returned along with the integer errno value.

### I/O result sorts

Here we see sorts defined to contain either an `Int` or an `IOError`, or
Here we see sorts defined to contain either an `Int` or an `IOError`, or
either a `String` or an `IOError`. These sorts are used to implement the
return sort of functions that may succeed, in which case they return a value,
or may fail, in which case their return value indicates an error and the
Expand Down Expand Up @@ -2509,7 +2509,7 @@ requested. A string of zero length being returned indicates end-of-file.

### Write to file

You can write a single character to a file using `#putc`. You can also write
You can write a single character to a file using `#putc`. You can also write
a string to a file using `#write`. The returned value on success is `.K`.

```k
Expand All @@ -2527,7 +2527,7 @@ You can close a file using `#close`. The returned value on success is `.K`.

### Locking/unlocking a file

You can lock or unlock parts of a file using the `#lock` and `#unlock`
You can lock or unlock parts of a file using the `#lock` and `#unlock`
functions. The lock starts at the beginning of the file and continues for
`endIndex` bytes. Note that Unix systems do not actually prevent locked files
from being read and modified; you will have to lock both sides of a concurrent
Expand All @@ -2540,7 +2540,7 @@ access to guarantee exclusivity.

### Networking

You can accept a connection on a socket using `#accept`, or shut down the
You can accept a connection on a socket using `#accept`, or shut down the
write end of a socket with `#shutdownWrite`. Note that facility is not provided
for opening, binding, and listening on sockets. These functions are implemented
in order to support creating stateful request/response servers where the
Expand Down Expand Up @@ -2860,7 +2860,7 @@ You can get the number of bits of width in an MInt using `bitwidthMInt`.

### Int and MInt conversions

You can convert from an `MInt` to an `Int` using the `MInt2Signed` and
You can convert from an `MInt` to an `Int` using the `MInt2Signed` and
`MInt2Unsigned` functions. an `MInt` does not have a sign; its sign is instead
reflected in how operators interpret its value either as a signed integer or as
an unsigned integer. Thus, you can interpret a `MInt` as a signed integer witth
Expand All @@ -2880,8 +2880,8 @@ has the correct bitwidth, as this will influence the width of the resulting

### MInt min and max values

You can get the minimum and maximum values of a signed or unsigned `MInt`
with az specified bit width using `sminMInt`, `smaxMInt`, `uminMInt`, and
You can get the minimum and maximum values of a signed or unsigned `MInt`
with az specified bit width using `sminMInt`, `smaxMInt`, `uminMInt`, and
`umaxMInt`.

```k
Expand Down