## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### 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'll try to integrate the clausification ( simplification of âŠ¤ and âŠ¥) with the saturation loop.
Jannik Vierling
@jvierling
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
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.