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 committed May 7, 2020
1 parent ba192d5 commit a906f53
Show file tree
Hide file tree
Showing 6 changed files with 91 additions and 6 deletions.
14 changes: 10 additions & 4 deletions prover/lang/kore-lang.md
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 @@ -326,8 +329,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 @@ -771,10 +774,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 @@ -795,6 +798,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 @@ -856,6 +861,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
48 changes: 47 additions & 1 deletion prover/strategies/knaster-tarski.md
Original file line number Diff line number Diff line change
Expand Up @@ -384,7 +384,9 @@ Move #holes to the front
```

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

```k
syntax UpperName ::= "#rest" [token]
rule <k> \implies( \and( S:Symbol ( \forall { UNIVs }
implicationContext(\and(CTXLHS), CTXRHS)
)
, LHS:Patterns
)
, RHS:Pattern
)
</k>
<strategy> 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
)
...
</strategy>
```

```k
rule <k> \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
)
</k>
<strategy> ( #matchResult(subst: SUBST, rest: .Patterns) ~> kt-collapse )
=> noop
...
</strategy>
```

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

Expand Down
13 changes: 13 additions & 0 deletions prover/strategies/matching.md
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
2 changes: 2 additions & 0 deletions prover/strategies/simplification.md
Original file line number Diff line number Diff line change
Expand Up @@ -341,6 +341,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
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
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 a906f53

Please sign in to comment.