!!! Manual stratergy for avl-implies-bst

nishantjr · nishantjr · commit 9394d7266f60 · 2020-02-12T01:35:46.000+05:30
diff --git a/prover/t/avl-implies-bst.kore b/prover/t/avl-implies-bst.kore
@@ -18,11 +18,10 @@ claim \implies( \and( avl( H { ArrayIntInt }
                          )
                     )
               )
-strategy search-fol(bound: 3)
-//strategy simplify . kt . simplify
-//       . ( (right-unfold-Nth(0,0) . simplify . instantiate-existentials . smt )
-//         | (right-unfold-Nth(0,1) . simplify . instantiate-existentials . smt )
-//         | (instantiate-existentials . smt )
-//         | (right-unfold-Nth(0,2) . simplify . instantiate-existentials . smt )
-//         | noop
-//         )
+// strategy search-fol(bound: 3)
+strategy normalize . simplify . kt . normalize . simplify
+       . ( (right-unfold-Nth(0,0) . normalize . simplify . instantiate-existentials . smt )
+         | (right-unfold-Nth(0,1) . normalize . simplify . instantiate-existentials . smt )
+         | (instantiate-existentials . smt )
+         | (right-unfold-Nth(0,2) . normalize . simplify . instantiate-existentials . smt )
+         )

Original file line number	Diff line number	Diff line change
`@@ -18,11 +18,10 @@ claim \implies( \and( avl( H { ArrayIntInt }`
`18`	`18`	`)`
`19`	`19`	`)`
`20`	`20`	`)`
`21`		`-strategy search-fol(bound: 3)`
`22`		`-//strategy simplify . kt . simplify`
`23`		`-// . ( (right-unfold-Nth(0,0) . simplify . instantiate-existentials . smt )`
`24`		`-// \| (right-unfold-Nth(0,1) . simplify . instantiate-existentials . smt )`
`25`		`-// \| (instantiate-existentials . smt )`
`26`		`-// \| (right-unfold-Nth(0,2) . simplify . instantiate-existentials . smt )`
`27`		`-// \| noop`
`28`		`-// )`
	`21`	`+// strategy search-fol(bound: 3)`
	`22`	`+strategy normalize . simplify . kt . normalize . simplify`
	`23`	`+ . ( (right-unfold-Nth(0,0) . normalize . simplify . instantiate-existentials . smt )`
	`24`	`+ \| (right-unfold-Nth(0,1) . normalize . simplify . instantiate-existentials . smt )`
	`25`	`+ \| (instantiate-existentials . smt )`
	`26`	`+ \| (right-unfold-Nth(0,2) . normalize . simplify . instantiate-existentials . smt )`
	`27`	`+ )`