Where communities thrive

Join over 1.5M+ people
Join over 100K+ communities
Free without limits
Create your own community

Explore more communities

gapt/gapt

Great Audience for Posting Troubles

People

Repo info

Activity

Feb 28 13:37

fachammer synchronize #741
Feb 28 13:37

fachammer on dls-algorithm-for-formula-equations

return simpler witness when onl… (compare)
Feb 28 13:35

fachammer commented #745
Feb 28 09:43

shetzl opened #745
Feb 28 09:39

shetzl closed #743
Feb 28 09:39

shetzl commented #743
Feb 19 17:07

fachammer synchronize #741
Feb 19 17:07

fachammer on dls-algorithm-for-formula-equations

improve criterion in documentat… (compare)
Feb 18 16:42

fachammer synchronize #741
Feb 18 16:42

fachammer on dls-algorithm-for-formula-equations

improve solveFormulaEquation -… remove unnecessary code fix formatting and 4 more (compare)
Feb 12 20:20

Jenkins nightly build failure
Feb 12 20:03

Jenkins nightly build failure
Feb 06 13:56

Travis gapt/gapt (dls-algorithm-for-formula-equations) passed (4032)
Feb 06 13:24

fachammer synchronize #741
Feb 06 13:24

fachammer on dls-algorithm-for-formula-equations

put advanced simplify into solv… (compare)
Feb 05 19:35

jvierling labeled #742
Feb 05 19:29

jvierling labeled #744
Feb 05 19:26

jvierling assigned #744
Feb 05 19:26

jvierling opened #744
Feb 05 19:18

jvierling commented #741

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

Jannik Vierling

@jvierling

Thanks

Gabriel Ebner

@gebner

fyi using clogic89 today

Jannik Vierling

@jvierling

@gebner Why does ./gapt.sh somescript execute everything that extends Script?

Gabriel Ebner

@gebner

@jvierling Because someone asked me to make ./gapt.sh poset/cutintro.scala work. 🤷 (I think the request was for another script file though..)

Jannik Vierling

@jvierling

@gebner Thanks for the reply. I was a bit surprised to see ./gapt.sh somescript start to evaluate all Script objects.