jvierling on develop
fix comment (compare)
jvierling on develop
use quantifier block instead of… make leancop parser a bit more … improve formatting and 3 more (compare)
jvierling on leancopparser
Ermine516 on leancopparser
Current stage of development Instance file production is now… Updating Dummy Prover and 10 more (compare)
Ermine516 on InstanceConstructionAndDummyProver
Bump version to 2.16-SNAPSHOT update iProver output parser disable superposition and non e… and 32 more (compare)
jvierling on leancopparser
improve formatting refactor definitional clausal f… refactor expansion proof constr… (compare)
jvierling on leancopparser
make leancop parser a bit more … (compare)
Ermine516 on InstanceConstructionAndDummyProver
Some unimportant changes (compare)
Ermine516 on InstanceConstructionAndDummyProver
minor changes (compare)
jvierling on develop
fix export for variables starti… (compare)
jvierling on leancopparser
use quantifier block instead of… (compare)
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
object Example extends scala.App {
implicit var ctx = Context()
ctx += hoc"P{?a}: ?a > o"
ctx += Ti
ctx += hoc"c:i"
val t1 = le"P(x:?a)"
val t2 = le"P(c)"
val Some( subst ) = syntacticMGU( t1, t2 )
require( subst( t1 ) == subst( t2 ) )
}
pos2
supposed to represent?
i1
th formula in clause c1
, we want to rewrite t_
to s_
), the second line describes the other clause that we want to rewrite (i2
th formula in clause c2
). pos2
are positions in c2.conclusion(i2)
that can be unified with t_
(the left-hand side of the equation, if leftToRight
is true). https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L460 These positions are then replaced by the right-hand side of the equation, i.e., mgu(s_)
.
./viper.sh --analytic isaplanner/prop_17.smt2
it fails with a gapt.proofs.gaptic.TacticFailureException
and the message goal is not subsumed by provided proof:
. This also affects at least prop_25, 33 and 34 and is the same for the spind mode. Is this is a known thing?