gapt/gapt

Great Audience for Posting Troubles

Andreas H. From

@andreasfrom

So the 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.

Jannik Vierling

@jvierling

The symbol apply1 is stored in TipProblem.uninterpretedConsts, because it has no definition.

Andreas H. From

@andreasfrom

Why doesn't ∀x apply1(lam, x) = return(x) constitute a definition?

Jannik Vierling

@jvierling

Actually by definition I meant a definition in terms of define-fun or define-fun-rec or define-funs-rec. Actually the tip tool adds the definition that you gave as an assertion with a :definition keyword, but currently the tip importer does not inspect these keywords.

Andreas H. From

@andreasfrom

Oh right. Okay, thank you.

Jannik Vierling

@jvierling

Next week when I am back i'll try to spend some time to improve the tip importer.

Andreas H. From

@andreasfrom

It's not urgent for my purposes.

Andreas H. From

@andreasfrom

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

Gabriel Ebner

@gebner

@andreasfrom I'm going to use clogic89 over the weekend again.

Andreas H. From

@andreasfrom

@gebner roger.

Andreas H. From

@andreasfrom

@shetzl We talked about going to and from an expansion proof to reduce the proof, but I've got one here (for isaplanner/prop_57.smt2) which has around 2000 steps as an LK proof and going back from expansion to LK is taking more than 20 minutes. So that doesn't seem feasible(?)

Andreas H. From

@andreasfrom

Wait, I realised I could cleanStructuralRules it first and then it roundtrips quickly.

Stefan Hetzl

@shetzl

@andreasfrom Yes, cleanStructuralRules should always be cheap.

Jannik Vierling

@jvierling

@gebner How are our substitutions on term and types supposed to behave when one substitutes both term-level variables and type variables simultaneously? Should type variables be substituted before substituting the term variables?

@gebner I am asking this because I ran into a problem with the syntactic unification where the resulting substitution does not unfiy the expressions but I am not sure whether this is a bug in the unification algorithm or in the way the substitution is applied to the term.

@gebner Here is the example

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 ) )
}

Gabriel Ebner

@gebner

They are supposed to be applied simultaneously. For example you might have a substitution ?a -> list ?b, (x: ?a) -> (nil : list ?b).

Gabriel Ebner

@gebner

Yes, 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?

Jannik Vierling

@jvierling

I will look into it.

Jannik Vierling

@jvierling

@gebner Why is hof"⊤" not considered to be an Atom (hof"⊤".asInstanceOf[Atom] fails) ?

Gabriel Ebner

@gebner

Because it's a logical connective.

Treating true/false as atoms can easily lead to bugs: e.g. gapt/gapt#309 If they are not atoms, it's clear that you need to treat them specially.

Jannik Vierling

@jvierling

Ok thanks.

Jannik Vierling

@jvierling

@gebner How does Escargot deal with ⊤ and ⊥? Does it avoid to generate these connectives? The problem is that at some point a ⊤ ends up as a component by splitting but it is apparently not meant to be there.

Gabriel Ebner

@gebner

There should not be any ⊤ or ⊥ left after clausification.

You can integrate clausification into the saturation loop using this inference: https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L179

But for first-order problems, clausification happens before the main loop is even started.

Jannik Vierling

@jvierling

I am running Escargot on a tip problem which uses formulas on term level, this introduces ⊤ after clausificiation.

Gabriel Ebner

@gebner

Goodbye completeness, I think. But yeah, I'd just add the clausification inference rule and see what happens.

Jannik Vierling

@jvierling

I'll try to integrate the clausification ( simplification of ⊤ and ⊥) with the saturation loop.

Jannik Vierling

@jvierling

@gebner At https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L454 what are the positions pos2 supposed to represent?

Jannik Vierling

@jvierling

I think these positions are the positions of some subterms of the forms_ in c_2.conclusion(i2). Is that correct?

Gabriel Ebner

@gebner

The first line of the function arguments describes the equation (i1th formula in clause c1, we want to rewrite t_ to s_), the second line describes the other clause that we want to rewrite (i2th 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_).

Andreas H. From

@andreasfrom

If I run ./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?

Jannik Vierling

@jvierling

@andreasfrom Thanks for reporting this. I fixed the problem.

Andreas H. From

@andreasfrom

@shetzl Generalization only makes a difference for one file: prod/prop_15. Removing testing means going from 127 solved to 97.

Gabriel Ebner

@gebner

@andreasfrom What are your plans for clogic89 for the next few days? Can I have it?

Andreas H. From

@andreasfrom

@gebner Yes, knock yourself out.

Andreas H. From

@andreasfrom

@gebner Please let me know when you're done with it :)

Gabriel Ebner

@gebner

According to parallel, the ETA is 8 d + 8 h + 50 min. But I think it will be finished a bit sooner, since I expect the jobs at the beginning to take significantly longer than the rest.

I can interrupt it though if it's urgent.

Andreas H. From

@andreasfrom

No hurry, thanks for the ETA.

Gabriel Ebner

@gebner

@andreasfrom It's finished now. Do you want to run something now or should I start something else?

Andreas H. From

@andreasfrom

I'll run something over night real quick.

Andreas H. From

@andreasfrom

@gebner clogic89 is yours again. Thanks.

Andreas H. From

@andreasfrom

What's the clogic89 status? I would like to run some (hopefully final) benchmarks this week.

Gabriel Ebner

@gebner

It's yours. Tell me when you're finished.

Andreas H. From

@andreasfrom

Thanks. I expect around 24 hours. I'll let you know.

Andreas H. From

@andreasfrom

@gebner I'm finished.

Gabriel Ebner

@gebner

@jannikvierling https://wwww.easychair.org/publications/preprint/xNWL

Where communities thrive

People

Repo info

Activity