Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
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'll try to integrate the clausification ( simplification of ⊤ and ⊥) with the saturation loop.
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.