jvierling on develop
fix predicate reduction (compare)
jvierling on develop
add the trait LogicalConstant t… cover equality in tests of cons… Merge branch 'logical-equality'… (compare)
jvierling on develop
remove useless tests use matchers instead of assignm… (compare)
jvierling on develop
update year in copyright notice (compare)
jvierling on logical-equality
add the trait LogicalConstant t… cover equality in tests of cons… (compare)
jvierling on develop
fix a typo in a comment remove unused variable remove an unused variable and 3 more (compare)
jvierling on push-equality-inferences-to-leaves
jvierling on equality-left-elimination
jvierling on escargot-sat-recompute
jvierling on tgpe
jvierling on update-scala-version
jvierling on push_version_2.13.3
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 ) )
}
syntacticMGU
is buggy here. There are at least two issues with type variables there. Do you want to look into it, or should I just push the fix?
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?