Conversation
|
Please do not use dashs in filenames for consistency.
I'd say we add them to the ITS, we just store linear and
So far, every original rule and every learned rule has a unique
Yes, that's right.
Yes, I hope so. If they aren't, we should adapt that.
An object o of type std::variant<A, B> can store either an https://en.cppreference.com/w/cpp/utility/variant/holds_alternative
Yes, and LocationIdx is just a number. So for example, we could
Right. Then c.lhs.loc would be 1.
No, it's a variable that stores the current location during a run
No, with
as 1 represents F. |
Ah ok. So we don't keep track of the source nodes of each transition with dedicated fields on the |
|
Yes, but to work around that, we use the dependency graph. It's a graph whose nodes are transitions, and there is an edge from t1 to t2 if t2 can be applied after t1. It's pre-computed once in the beginning of the analysis. So we can just use the successors of the transition that was used for previous step as candidate transitions for the next step. Note that locations are a somewhat arbitrary way to encode the control-flow. No one prevents you from writing, e.g.,
which is "recursive" if you just consider the locations, but in fact it's not. Thus, the dependency graph is a better way to represent the control-flow. |
But if we have a non-linear CHC: Then it's technically a sink transition, right? But we wouldn't add it to the set of |
|
Yes, so But you are right, we have to be a bit careful about the semantics of the data-structures that store transitions, since it might not always be obvious whether they are for linear transitions, non-linear transitions, or both. As long as we deal with linear or non-linear transitions directly, the difference can be seen on type-level, but |
I see. But if we can use the dependency graph, why put the extra condition in the guard then? Isn't it tautological then during analysis? Do we just need it to compute the dependency graph in the beginning? Then why not keep track of the source node explicitly and build up the dependency graph that way?
Ok so with the nonlinear rules, we have to extend the dependency graph whenever we derive new linear rules, right? |
For ADCL we wouldn't need the extra condition, but there are other engines in LoAT (BMC and ABMC) that need it.
We need to add nodes to it whenever we learn new transitions.
We keep track of the source and target locations of all transitions in
Yes, but we already do that when ADCL learns new clauses. I guess
should do what you want. It returns the index of the newly added transition. Afterwards, you can invoke
to refine the dependency graph locally, i.e., just in the neighborhood of the newly added transition. |
|
Ok, to figure out how data-model the nonlinear rules, I'm trying to understand how resolution for linear rules is implemented currently. As far as I can tell the magic is happening here. But how does this line eliminate the predicate on the left-hand-side of and we want to make sure, the resolvent doesn't have the literal |
|
The guard of the chained rule (aka resolvent) is where So if |
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
0c03262 to
728fc05
Compare
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
372aa7d to
dc3b889
Compare
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
0cf55fa to
05c8155
Compare
|
Ok, I think it's time to justify some design decisions 😁 Remember that we said, the non-linear solver should represent the CHCs simply with the Now the non-linear solver must be able to restore There is another reason, I need the program variables on the ITS: When the non-linear solver derives a new linear CHC it needs to convert it into an ITS transition and add it to the ITS problem. For this conversion I need to essentially invoke this preprocessing logic that is already implemented in the parser. So to do that and to avoid redundancy, I extracted this logic and also turned it into a new ITS method. That logic in turn also needs access to the program variables, so that's the second reason why I think it makes sense to add them to the ITS problem class. |
gruhn
force-pushed
the
polyaccel-nonlinear
branch
2 times, most recently
from
2e38b40 to
8719963
Compare
|
So I did some tests with the LIA benchmark. I just did one round of resolution of all linear clauses with all non-linear clauses and added the resolvents to the ITS. Apparently, that can prove UNSAT of quite a few instances already (assuming my implementation is correct). For comparison, I also ran ADCL against the LIA instances by just ignoring all the non-linear CHCs. That wasn't so successful. However, I also got segmentation faults on quite a few instances. I dug into it and they occur here in this preprocessing step. If I understand correctly, in this step we remove transitions that are not "forward" reachable from any of the initial transitions or "backwards" reachable from any of the sink transitions. I think what's happening is that sometimes the sink transitions are only reachable via non-linear CHCs. But because they are not accounted for in the dependency graph initially, we falsely remove the sink transitions in the "forward" preprocessing step. And then during "backward" preprocessing, there are no sink transitions anymore, so we So I guess we can either skip preprocessing or we extend the dependency graph with all possible transitions, but I don't know what effects this might have. Can we have dependencies, although there are no associated rules in the ITS? |
All kinds of variables (
I think you need to be able to differentiate between program variables and temporary variables, correct? To do so, you can use
Sounds great!
Correct.
Yes, that makes sense.
From the point of view of the linear solver, we are solving a problem 'incrementally', i.e., we do not know all clauses when the analysis starts. So far, that was not the case -- we always knew all clauses from the very beginning. In such an incremental setting, it makes little sense to remove transitions because they are not reachable, as they might become reachable later on. Thus, we should disable this particular preprocessing step if the problem is non-linear. However, as the non-linear solver only learns facts, that's only true for forward reachability. Removing clauses that are not backward-reachable from querys / sink transitions should still make sense. |
|
For the record: The following part of my last post is wrong.
The non-linear part learns rules, not facts, so we should disable the pre-processing entirely. |
|
Also just noticed, Parsing gives me an integer overflow. Looks like the parser is storing integers in a normal |
That's surprising. Constants are parsed by this line: Here, |
|
Ah ok! I tracked it down. The problem is specific to div/mod expressions. Here is the offending line: https://github.com/LoAT-developers/LoAT/blob/termcomp23/src/parser/chc/CHCParseVisitor.cpp#L432 This fixes the issue for me: 4d99e1a |
|
@ffrohn can you help me understand what https://github.com/LoAT-developers/LoAT/blob/termcomp23/src/analysis/reachability.cpp#L335 What is the meaning of this pair of integers? Do I have to be careful invoking this function too often? I was planning to restart the linear solver for every linear clause that is added to the ITS. But that would mean that I sometimes restart the solver multiple times in a row, and thereby invoke this |
|
See this paper. It's just a heuristic to determine how often one should perform a restart that works very well for SAT solving, so we adapted it to our setting. If you invoke |
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
31709e8 to
c7890de
Compare
|
FYI: just noticed that for |
No. Refutational completeness of ADCL just means that there is a run of ADCL that proves unsat. Since ADCL is inherently non-deterministic, that does not imply that the actual run which is performed by the implementation proves unsat. Moreover, refutational completeness only holds under the assumption that we have a complete SMT solver, a complete redundancy check, and complete acceleration techniques. In practice, all of these things are incomplete. In other words: Refutational completeness is a property of the calculus, it's not a property of the implementation. |
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
c7890de to
c6928b7
Compare
When computing the resolvent of two clauses we compute a unifier
of the resolved predicates. Previously, we simply mapped the
variables directly:
F(a, b)
v v
F(x, y)
However, apparently a predicate may not have disjoint arguments.
That means, the arguments can encode implicit equalities, which
are lost during unification:
F(a, a)
v v
F(x, y)
Taking this into account seems to fix several LIA benchmark instances
where we gave UNSAT although Z3 gaves SAT:
066,108,235,236,244,355,359
put benchmark results for Z3 and ADCL in the same file so they can be compared during a test run more easily.
Actually we get UNSAT on quite some more instances where we got a timeout before. Seems also related to disabling the linear path chaining.
1) Previously, the non-linear solver generated redundant resolvents.
For example, for the CHC problem
F(1)
F(x) /\ F(y) /\ F(z) ==> G(x,y,z)
we get the resolvent
F(z) ==> G(1,1,z)
twice by either resolving F(1) with F(x) first and then F(y) or
with F(y) first and then F(x). We now avoid that by always
picking the resolved predicates in order, namely:
F(x) < F(y) < F(z)
This should avoid redundant resolvents as long as the given
facts and non-linear CHCs are not already redundant.
2) Also storing clauses in sets now (instead of lists) to
automatically filter out (syntactically) redundant clauses.
For that also making sure to remove the location variable from
constraints when converting ITS rules to Clauses because they
otherwise introduce a variable that is unique for every
resolvent even if the same two clauses are resolved twice in
a row. Thus, we loose easily detectable syntactic redundance.
Previously, when simplifying boolean expressions, only temporary boolean variables were propagated. For example in (b1 \/ b2) /\ !b2 ==> F(b1) the temporary variable `b2` can be propagated, which simplifies the clause to b1 ==> F(b1) But program variables were not propagated. For example (b1 \/ b2) /\ !b2 ==> F(b1, b2) would not propagate `b2` since it's a program variable. When propagating program variables we have to make sure to not eliminate them completely like temporary variables. Otherwise we loose information. Instead the expected result is: b1 /\ !b2 ==> F(b1, b2) This simplification can speed up ADCL because potentially fewer conjunctive variants of the clause have to generated (observed in LIA instance 69).
Introduce constraint tiers: Linear, Polynomial, Exponential. Here "linear" does NOT refer the plurality of left-hand-side predicates but the clause constraint. For example: - linear constraint : F(x) /\ 2*x=4 ==> F(x) - polynomial constraint : F(x) /\ x^2=4 ==> F(x) - exponential constraint : F(x) /\ 2^x=4 ==> F(x) The distinction is for optimization. Because the constraint tiers are successively harder to deal with for SMT solvers, we can first try to solve a CHC problem by only considering "easy" linear constraints first and only consider harder polynomial and exponential constraints if necessary.
Run LIA benchmark with 10 second timeout instead of 5 seconds.
In many cases the linear solver produces facts that syntactically
redundant up to renaming. This seems to happen quite a lot. Consider
the CHC problem:
(c1) fib(0, 1)
(c2) fib(1, 1)
(c3) fib(x1, y1) /\ fib(x2, y2) /\ x1+1 = x2 ==> fib(x2+1, y1+y2)
Resolution of c1 with the *first* predicate of c3 gives:
res(c1,c3) == fib(x2, y2) /\ 1+1 = x2 ==> fib(x2+1, 1+y2)
== fib(1, y) ==> fib(2, y+1)
Resolution of c2 with the *second* predicate of c3 gives:
res(c2,c3) == fib(x1,y1) /\ x1+1 = 1 ==> fib(1+1,1+y2)
== fib(0, y) ==> fib(2,y+1)
Then the linear solver derives the fact `fib(2,2)` with two non-redundant
traces:
[c2, res(c1, c3)] = [f(1,1), fib(1, y) ==> fib(2, y+1)] = fib(2,2)
[c1, res(c2, c3)] = [f(0,1), fib(0, y) ==> fib(2, y+1)] = fib(2,2)
The LIA benchmark has a lot of Fibonacci related CHC instances. See for
example:
081,093,090,086,098,353,354,077,345,073,080,076,343,344
And in all of these, the above issue seems to occur. Filtering out the
redundant facts doesn't seem to help much though.
For some reason, callling `refineDependencyGraph` after passing new clauses to the linear solver, doesn't terminate or takes a very long on some instances. Calling it also seems to be unecessary since we call it again as part of the preprocessing step. This change gives `unsat` on 8 new instances.
The commit titled:
non-linear: detect redundant (up to renaming) facts
introduced a syntactic redundancy check in the non-linear solver.
This allows the non-linear solver to filter out syntactially
redundant facts derived by the linear solver. Thus, we do fewer
resolution steps in the non-linear solver and produce fewer rules
that are passed to the linear solver.
However, the linear solver still spends a lot of time deriving
these redundant facts. By moving the redundancy check into the
linear solver, it can backtrack immediatly when encountering a
redundant fact.
With that we get `unsat` on 7 new instances.
If a predicate only occurs on the RHS of a single CHC, then there is only one choice how to eliminate the predicate on the LHS of other CHCs. Thus, we can pre-compute all resolvents where one of parent clauses has a unique RHS. Previously the CHC parser would directly output an ITS instance. But it's hard to reason about the side effect of deleting/modifying rules in the ITS. It's more convenient to preprocess the CHCs first and then construct the ITS instance from it. Thus, the CHC parser now outputs a set of clauses. With this change we get: - chc comp 2022: +16 UNSAT - chc comp 2023: +9 UNSAT
Assume we have facts F,G,H and a non-linear CHC:
F /\ G /\ H ==> false
When we recursively compute all resolvents, the iterator on the LHS
predicates should match the call tree depth. So at depth 1 the iterator
should point to the first predicate. At depth 2 the iterator should always
point on the second predicate. Let `*` denote the iterator position and
let `_` denote an eliminated predicate, then the (partial) call tree should
look like this:
F* /\ G /\ H ==> false
--> _ /\ G* /\ H ==> false
--> _ /\ _ /\ H* ==> false
(...)
--> F /\ G* /\ H ==> false
--> F /\ _ /\ H* ==> false
--> F /\ _ /\ _ ==> false
(...)
However, when we compute a resolvent the iterator was "reset" to the first
predicate, which is a problem when we are in a sub-tree, where the iterator
is not pointing on the first non-eliminated predicate. That is, we actually
got:
F* /\ G /\ H ==> false
--> _ /\ G* /\ H ==> false
--> _ /\ _ /\ H* ==> false (original resolvent)
(...)
--> F /\ G* /\ H ==> false
--> F* /\ _ /\ H ==> false (iterator reset)
--> _ /\ _ /\ H* ==> false (redundant resolvent)
(...)
The iterator is "reset" because iterators are only defined for a concrete
collection. The resolvent stores its LHS predicate in a new collection.
We fix this by using an normal index on the LHS predicates instead of an
iterator.
Another way we derive redundant resolvents is when clauses are "symmetric".
For example, exchanging `F(x)` and `F(y)` in
F(x) /\ F(y) /\ F(z) ==> G(x+y)
does not change the meaning of the clause. Now, with the single fact `F(1)`
we would get the derivation:
F(x)* /\ F(y) /\ F(z) ==> G(x+y)
--> ___ /\ F(y) /\ F(z) ==> G(1+y)
(...)
--> F(x) /\ F(y)* /\ F(z) ==> G(x+y)
--> F(x) /\ ___ /\ F(z) ==> G(x+1)
(...)
We can detect that the two resolvents
F(y) /\ F(z) ==> G(1+y)
F(x) /\ F(z) ==> G(x+1)
are syntactially equivalent (up-to renmaing). And in particular, all resolvents
that derived from these clauses are also equivalent. So we now prune the call tree
when we detect a redundant resolvent.
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
08d69cc to
eb6bd51
Compare
Computing all resolvents is exponential in the number of LHS predicates
of a non-linear clause. So it's worth eliminating as many predicates as
possible. In preprocessing we already eliminate predicates if there is
only one resolution candidate.
By merging facts we can reduce resolution candidates. For example, here
have two candidates for `F(x)`:
x=0 ==> F(x)
x>0 ==> F(x)
we can merge these facts into one clause by disjoining the constraints:
(x=0 \/ x>0) ==> F(x)
This can make all facts unilaterally resolvable as long as the RHS
predicate does not also occur on the RHS of a rule.
Arguably, that just off-loads dealing with disjunctions to the linear
solver. We also loose some CHC structure pushing disjunctions into the
clause constraint. However, ADCL is designed to deal with disjunctions.
And computing all resolvents in the non-linear solver is worst-case
exponential in the number of LHS predicates, so it's probably worth it.
Benchmark results:
- CHC comp 2022: +6 UNSAT
- CHC comp 2023: +3 UNSAT
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
43d8cc2 to
ad2c2ed
Compare
Even after the fixes getting a lot of regressions on the benchmarks. Since nonlinear preprocessing can eliminate all CHCs in some cases, we also get SAT sometimes now. Benchmark results: * chc comp 2022: -17 unsat, +1 unsat, +40 sat * chc comp 2023: -5 unsat, +2 unsat, +26 sat On instance 248 from chc comp 2023 we get SAT where Z3 gives Unsat. This seems to be unrelated to the nonlinear solver though.
of chc comp 2023 instance 248 by commit: c7f7c40
Consider the CHC problem:
x>0 ==> F(x)
x<0 ==> G(y)
F(x) /\ G(x) /\ H(x) ==> false
We derive linear clauses by recursively resolving all facts with
previously computed non-linear resolvents:
F(x) /\ G(x) /\ H(x) ==> false
|
+-- G(x) /\ H(x) /\ x>0 ==> false
|
+-- H(x) /\ x>0 /\ x<0 ==> false
We stop expanding this call tree when a resolvents constraint is UNSAT,
because all following resolvents will also have UNSAT constraint.
Previously, we queried the SMT solver each time we get a new resolvent.
This is costly. However, when going deeper into the tree, we only
*add* constraints, so we can leverage incremental SMT.
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
ad2c2ed to
7c815d8
Compare
Can't reproduce many UNSAT anymore that Z3 gave on CHC comp 23. Did we use a different version? Now tested with: Z3 version 4.12.5 - 64 bit
gruhn
force-pushed
the
polyaccel-nonlinear
branch
3 times, most recently
from
a6ba0ab to
fa6f11a
Compare
gruhn
force-pushed
the
polyaccel-nonlinear
branch
from
29a9953 to
20fe058
Compare
2 participants
Ignore my changes in all non cpp/hpp files (Dockerfile, docker-compose.yaml, etc.). I'll remove them before merging.
I mainly want feedback on some questions, that I have written down as inline comments marked with
QUESTION.