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

- Feb 19 17:07fachammer synchronize #741
- Feb 19 17:07
fachammer on dls-algorithm-for-formula-equations

improve criterion in documentat… (compare)

- Feb 18 16:42fachammer 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:20Jenkins nightly build failure
- Feb 12 20:03Jenkins nightly build failure
- Feb 06 13:24fachammer synchronize #741
- Feb 06 13:24
fachammer on dls-algorithm-for-formula-equations

put advanced simplify into solv… (compare)

- Feb 05 19:35jvierling labeled #742
- Feb 05 19:29jvierling labeled #744
- Feb 05 19:26jvierling assigned #744
- Feb 05 19:26jvierling opened #744
- Feb 05 19:18jvierling commented #741
- Feb 05 15:43jvierling commented #741
- Feb 05 14:17shetzl commented #741
- Feb 05 14:13fachammer commented #741
- Feb 04 09:42Travis gapt/gapt#741 errored (4031)
- Feb 04 09:13fachammer synchronize #741

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.

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.

@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?
The first line of the function arguments describes the equation (

`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_)`

.
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?
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.