Ermine516 on InstanceConstructionAndDummyProver
Working PLCOP prover integration (compare)
Ermine516 on InstanceConstructionAndDummyProver
changes for rebase make leancop parser a bit more … changes for rebase and 14 more (compare)
Ermine516 on InstanceConstructionAndDummyProver
added deskolemization (compare)
jvierling on develop
remove some unused code and var… (compare)
jvierling on develop
support more strong quantifiers… (compare)
Ermine516 on InstanceConstructionAndDummyProver
left merge traces (compare)
Ermine516 on InstanceConstructionAndDummyProver
Forgot to add (compare)
Ermine516 on InstanceConstructionAndDummyProver
minor changes (compare)
Ermine516 on InstanceConstructionAndDummyProver
extractInductionGrammar: drop g… sipReconstruct: use metrics Viper: add --metrics option and 66 more (compare)
fixupAndLoad
just 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))))
and after fixupAndLoad
becomes:
∀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
apply1
must be introduced by the tip
tool, but it does not show up in TipProblem.functions
which 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