Skip to content

Commit

Permalink
more wip on until implies eventually
Browse files Browse the repository at this point in the history
  • Loading branch information
@lucaspena @nishantjr
lucaspena authored and nishantjr committed May 9, 2020
1 parent b40b25e commit 8939328
Show file tree
Hide file tree
Showing 7 changed files with 107 additions and 22 deletions.
14 changes: 10 additions & 4 deletions prover/lang/kore-lang.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,12 +141,15 @@ only in this scenario*.
```k
syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)]
syntax SetVariable ::= SharpName [klabel(setVariable)]
syntax Context ::= VariableName "[" Pattern "]" [klabel(context)]
syntax Pattern ::= Int
| Variable
| SetVariable
| Symbol
| Symbol "(" Patterns ")" [klabel(apply)]
| Context
| "\\top" "(" ")" [klabel(top)]
| "\\bottom" "(" ")" [klabel(bottom)]
| "\\equals" "(" Pattern "," Pattern ")" [klabel(equals)]
Expand Down Expand Up @@ -359,8 +362,8 @@ module KORE-HELPERS
rule getReturnSort(\exists{Vs} P) => getReturnSort(P)
syntax Sort ::= "TopSort" [token]
| "BottomSort" [token]
syntax UpperName ::= "TopSort" [token]
| "BottomSort" [token]
syntax Sort ::= unionSort(Sort, Sort) [function]
rule unionSort(TopSort, S) => TopSort
Expand Down Expand Up @@ -833,10 +836,10 @@ Simplifications
// TODO: This should use an axiom, similar to `functional` instead: `axiom predicate(P)`
rule isPredicatePattern(S:Symbol(ARGS)) => true
requires getReturnSort(S(ARGS)) =/=K Heap
requires getReturnSort(S(ARGS)) ==K Bool
rule isPredicatePattern(S:Symbol(ARGS)) => false
requires getReturnSort(S(ARGS)) ==K Heap
requires getReturnSort(S(ARGS)) =/=K Bool
rule isPredicatePattern(emp(.Patterns)) => false
rule isPredicatePattern(\exists{Vs} P) => isPredicatePattern(P)
rule isPredicatePattern(\forall{Vs} P) => isPredicatePattern(P)
Expand All @@ -857,6 +860,8 @@ Simplifications
rule isSpatialPattern(\or(_)) => false
rule isSpatialPattern(S:Symbol(ARGS)) => true
requires S =/=K sep andBool getReturnSort(S(ARGS)) ==K Heap
rule isSpatialPattern(S:Symbol(ARGS)) => false
requires getReturnSort(S(ARGS)) =/=K Heap
rule isSpatialPattern(#hole { Bool }) => false
rule isSpatialPattern(#hole { Heap }) => true
rule isSpatialPattern(V:VariableName { Heap }) => true
Expand Down Expand Up @@ -918,6 +923,7 @@ Simplifications
rule hasImplicationContext(\functionalPattern(P)) => hasImplicationContext(P)
rule hasImplicationContext(\exists{ _ } P ) => hasImplicationContext(P)
rule hasImplicationContext(\forall{ _ } P ) => hasImplicationContext(P)
rule hasImplicationContext(\mu X . P) => hasImplicationContext(P)
rule hasImplicationContext(implicationContext(_, _)) => true
rule hasImplicationContextPs(.Patterns) => false
rule hasImplicationContextPs(P, Ps)
Expand Down
4 changes: 2 additions & 2 deletions prover/strategies/core.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -290,8 +290,8 @@ Internal strategy used to implement `or-split` and `and-split`.
`rhs-top` evaluates to success if the right hand side is top

```k
rule <k> \implies(LHS, \exists{.Patterns} \and(.Patterns)) </k>
<strategy> rhs-top => success ... </strategy>
rule <claim> \implies(LHS, \exists{.Patterns} \and(.Patterns)) </claim>
<k> rhs-top => success ... </k>
```

If-then-else-fi strategy is useful for implementing other strategies:
Expand Down
48 changes: 47 additions & 1 deletion prover/strategies/knaster-tarski.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -384,7 +384,9 @@ Move #holes to the front
```

```k
rule <claim> \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { SORT }, _) , _ ) , _ ) , _ ) </claim>
rule <claim> \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { Bool }, _) , _ ) , _ ) , _ ) </claim>
<k> normalize-implication-context => noop ... </k>
rule <claim> \implies(\and( S:Symbol(\forall { UNIVs } implicationContext( \and(#hole { TopSort }, _) , _ )) , _ ) , _ ) </claim>
<k> normalize-implication-context => noop ... </k>
rule <claim> \implies(\and( sep(\forall { UNIVs } implicationContext( \and(sep(#hole { Heap }, _), _) , _ ) , _ ), _ ), _ ) </claim>
<k> normalize-implication-context => noop ... </k>
Expand Down Expand Up @@ -496,6 +498,50 @@ of heaps.
</k>
```

```k
syntax UpperName ::= "#rest" [token]
rule <claim> \implies( \and( S:Symbol ( \forall { UNIVs }
implicationContext(\and(CTXLHS), CTXRHS)
)
, LHS:Patterns
)
, RHS:Pattern
)
</claim>
<k> kt-collapse
=> with-each-match( #matchAssoc( terms: S( #hole { TopSort } )
, pattern: #rest[CTXLHS]
, variables: #rest { TopSort }
, subst: .Map
, rest: .Patterns
)
, kt-collapse
, kt-collapse-no-match
)
...
</k>
```

```k
rule <claim> \implies( \and( S:Symbol ( \forall { .Patterns }
implicationContext( \and(_), CTXRHS )
)
, LHS:Patterns
)
, RHS:Pattern
)
=> \implies( \and( subst({SUBST[#rest { TopSort }]}:>Pattern, #hole { TopSort }, CTXRHS)
, LHS
)
, RHS
)
</claim>
<k> ( #matchResult(subst: SUBST, rest: .Patterns) ~> kt-collapse )
=> noop
...
</k>
```

In the context of the heuristics we implement, this becomes the following, where
REST is obtained via matching:

Expand Down
41 changes: 27 additions & 14 deletions prover/strategies/matching.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,19 @@ Work around OCaml not producing reasonable error messages:
Recurse over assoc-only constructors (including `pto`):

```k
// TODO: matching over context patterns
rule #matchAssoc( terms: S:Symbol(T), .Patterns
, pattern: V[T], .Patterns
, variables: Vs
, subst: SUBST
, rest: REST
)
=> #matchResult( subst: SUBST V { getReturnSort(S(T)) } |-> S( #hole { getReturnSort(T) })
, rest: .Patterns
)
, .MatchResults
requires V { getReturnSort(S(T)) } in Vs
// Base case
rule #matchAssoc( terms: .Patterns
, pattern: .Patterns
Expand Down Expand Up @@ -679,37 +692,37 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil
If the RHS is empty, we have nothing to do

```k
rule <k> \implies(LHS, \exists { Vs } \and(.Patterns)) </k>
<strategy> patterns-equal => noop ... </strategy>
rule <claim> \implies(LHS, \exists { Vs } \and(.Patterns)) </claim>
<k> patterns-equal => noop ... </k>
```

Remove any patterns on the RHS that match a pattern on the LHS:

```k
rule <k> \implies(\and(LHS), \exists{Vs} \and(RHS, REST)) </k>
<strategy> patterns-equal
rule <claim> \implies(\and(LHS), \exists{Vs} \and(RHS, REST)) </claim>
<k> patterns-equal
=> with-each-match( #match( terms: LHS
, pattern: RHS
, variables: .Patterns
)
, patterns-equal
)
...
</strategy>
rule <k> \implies(LHS, \exists{ Vs } \and(RHS, REST))
=> \implies(LHS, \exists{ Vs } \and(REST))
</k>
<strategy> #matchResult(subst: .Map , rest: .Patterns)
rule <claim> \implies(LHS, \exists{ Vs } \and(RHS, REST))
=> \implies(LHS, \exists{ Vs } \and(REST))
</claim>
<k> #matchResult(subst: .Map , rest: .Patterns)
~> patterns-equal
=> patterns-equal
...
</strategy>
</k>
rule <strategy> #matchResult(subst: .Map , rest: P, Ps)
~> patterns-equal
=> fail
...
</strategy>
rule <k> #matchResult(subst: .Map , rest: P, Ps)
~> patterns-equal
=> fail
...
</k>
```

If the RHS has no spatial part, then there is nothing to do:
Expand Down
2 changes: 2 additions & 0 deletions prover/strategies/simplification.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -342,6 +342,8 @@ Bring predicate constraints to the top of a term.
syntax Pattern ::= #liftConstraints(Pattern) [function]
syntax Patterns ::= #liftConstraintsPs(Patterns) [function]
// rule #liftConstraints(S:Symbol(\and(P1, P2, Ps), ARGs)) => #liftConstraints(\and(S(P1, ARGs), S(\and(P2, Ps), ARGs)))
// rule #liftConstraints(S:Symbol(\and(P, .Patterns), ARGs)) => #liftConstraints(\and(S(P, ARGs)))
rule #liftConstraints(\and(Ps)) => \and(#liftConstraintsPs(Ps))
rule #liftConstraintsPs(.Patterns) => .Patterns
rule #liftConstraintsPs(sep(\and(.Patterns), .Patterns), REST) => #liftConstraintsPs(REST)
Expand Down
4 changes: 3 additions & 1 deletion prover/t/ltl/until-implies-eventually.kore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,4 +37,6 @@ right-unfold-Nth(0, 1)
phi-implies-phi
*/

strategy normalize . kt . right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top
strategy normalize . kt . ( ( right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top )
| ( right-unfold-Nth(0, 1) . normalize . lift-constraints . wait . patterns-equal . rhs-top )
)
16 changes: 16 additions & 0 deletions prover/t/unit/match-assoc.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,7 @@ module TEST-MATCH-ASSOC
// Match constructor against variable
rule test("match-assoc", 9)
=> symbol pto ( Loc, Data ) : Heap
symbol c ( Data ) : Data
assert( #error("Constructors do not match")
, .MatchResults
== #matchAssoc( terms: X0 { Loc }, Y0 { Data }
Expand All @@ -120,4 +121,19 @@ module TEST-MATCH-ASSOC
)
)
.Declarations
// Match multiple occurances of a variable
rule test("match-assoc", 10)
=> symbol c ( Data ) : Data
assert( #matchResult( subst: X0 |-> c( #hole { Data } )
, rest: .Patterns
)
, .MatchResults
== #matchAssoc( terms: c( W { Data } )
, pattern: X0[W { Data }]
, variables: X0 { Data }
, subst: .Map
, rest: .Patterns
)
)
.Declarations
endmodule

0 comments on commit 8939328

Please sign in to comment.