jvierling on develop
declare constant 'minus' (compare)
jvierling on develop
Replacement for ND Merge pull request #758 from ge… (compare)
jvierling on develop
Remove extraneous asterisk. Merge pull request #757 from ge… (compare)
jvierling on develop
Alternative version of pushEqua… Merge pull request #756 from ge… (compare)
jvierling on develop
Add helper functions, convenien… Better extractor types. syntacticMGU: more functions and 1 more (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 ) )
}