Ermine516 on InstanceConstructionAndDummyProver
Current stage of development (compare)
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)
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?