mode analytic_independent 17 analytic_sequential 39 spind 6 treegrammar 6
fixupAndLoadjust gives a different error (because of this, I think):
scala> val problem = TipSmtImporter.fixupAndLoad("benchmarks/isaplanner/prop_02.smt2") java.util.NoSuchElementException: None.get
mode analytic_independent 17 analytic_sequential 40 spind 15 treegrammar 7
I have a question about importing TIP problems. The file
tip2015/list_return_2.smt2 looks like this:
; List monad laws (declare-datatypes (a) ((list (nil) (cons (head a) (tail (list a)))))) (define-fun (par (a) (return ((x a)) (list a) (cons x (_ nil a))))) (define-fun-rec (par (a) (++ ((x (list a)) (y (list a))) (list a) (match x (case nil y) (case (cons z xs) (cons z (++ xs y))))))) (define-fun-rec (par (a b) (>>= ((x (list a)) (y (=> a (list b)))) (list b) (match x (case nil (_ nil b)) (case (cons z xs) (++ (@ y z) (>>= xs y))))))) (prove (par (a) (forall ((xs (list a))) (= (>>= xs (lambda ((x a)) (return x))) xs))))
∀x0 ∀x1 head(cons(x0, x1)) = x0, ∀x0 ∀x1 tail(cons(x0, x1)) = x1, ∀x return(x) = cons(x, nil), lam2 = lam, ∀y ++(nil, y) = y, ∀y ∀z ∀xs ++(cons(z, xs), y) = cons(z, ++(xs, y)), ∀y >>=(nil, y) = nil, ∀y ∀z ∀xs >>=(cons(z, xs), y) = ++(apply1(y, z), >>=(xs, y)), ∀y0 ∀y1 nil != cons(y0, y1), ∀x apply1(lam, x) = return(x) ⊢ ∀xs >>=(xs, lam2) = xs
apply1must be introduced by the
tiptool, but it does not show up in
TipProblem.functionswhich I am using to generate reduction rules for testing.
Here's an update:
mode analytic_independent 43 analytic_sequential 75 spind 34 treegrammar 16
All the problems solved by the analytic independent mode are affected by the tip importer thing mentioned above which makes my testing of conjectures less efficient or straight up breaks it. Three of them are solved if I just disable testing.
Spind is currently a little slower in total on the problems they have in common:
spind 118,666ms analytic_independent 93,527ms