strategy to remove constraints from lhs, lsegex4_slk-1 goes through

kframework · May 5, 2020 · f4a6e03 · f4a6e03
1 parent be93ff7
commit f4a6e03
Show file tree

Hide file tree

Showing 3 changed files with 36 additions and 0 deletions.
diff --git a/prover/lib/testlists.py b/prover/lib/testlists.py
@@ -192,6 +192,25 @@ def read_list(file):
     ) .
 """.replace('\n', ' ')
 
+lsegex4_slk_1_strategy = """
+    normalize . or-split-rhs
+  . lift-constraints . instantiate-existentials . substitute-equals-for-equals
+  . left-unfold-Nth(0)
+  . ( ( normalize . or-split-rhs . lift-constraints
+      . instantiate-existentials . substitute-equals-for-equals
+      . check-lhs-constraint-unsat . fail
+      )
+    | ( normalize . or-split-rhs . lift-constraints
+      . instantiate-existentials . substitute-equals-for-equals
+      . right-unfold-Nth(0,0)
+      . normalize . or-split-rhs . lift-constraints
+      . instantiate-existentials . substitute-equals-for-equals
+      . remove-constraints
+      . search-sl(kt-bound: 2, unfold-bound: 2)
+      )
+    ) .
+""".replace('\n', ' ')
+
     #         prefix   KT  RU timeout tests
 test_lists = [ ('unfold-mut-recs . ',    3,  3,  '5m', read_list('t/test-lists/passing-3-3-5'))
              , ('unfold-mut-recs . ',    5, 12, '40m', read_list('t/test-lists/passing-5-12-40'))
@@ -309,6 +328,7 @@ def read_list(file):
              , (nll_vc08_10_strategy, 2,  2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/nll-vc08.smt2'])
              , (nll_vc08_10_strategy, 2,  2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/nll-vc10.smt2'])
              , ('', 3,  2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/tseg_join_tree_entail_tseg.sb.smt2'])
+             , (lsegex4_slk_1_strategy, 2,  2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/lsegex4_slk-1.smt2'])
              ]
 qf_shid_entl_unsat_tests = read_list('t/test-lists/qf_shid_entl.unsat')
 

diff --git a/prover/prover.md b/prover/prover.md
@@ -65,6 +65,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                     | "match" | "match-debug" | "match-pto"
                     | "frame"
                     | "footprint-analysis" | "nullity-analysis" "(" Strategy ")"
+                    | "remove-constraints"
                     | "unfold-mut-recs"
                     | "apply-equation"
                         RewriteDirection AxiomOrClaimName

diff --git a/prover/strategies/simplification.md b/prover/strategies/simplification.md
@@ -563,6 +563,21 @@ We define a similar strategy for quantified implication contexts:
   rule removeTrivialEqualities(P, Ps) => P, removeTrivialEqualities(Ps) [owise]
 ```
 
+### Substitute Equals for equals
+
+```
+      PHI /\ C => PSI
+     -----------------  where C is a predicate pattern
+         PHI -> PSI
+```
+
+```k
+  rule <k> \implies(\and(LHS), RHS)
+            => \implies(\and(LHS -Patterns getPredicatePatterns(LHS)), RHS)
+       </k>
+       <strategy> remove-constraints => noop ... </strategy>
+```
+
 ```k
 endmodule
 ```