Interpolation-based Transition Invariants for Termination#159
Interpolation-based Transition Invariants for Termination#159BritikovKI wants to merge 90 commits into
Conversation
|
The implementation of interpolation-based generation of well-founded transition invariants for Termination proofs. The changes to SingleLoopTransformations are made to make initial states meaningful. Instead of being a negation of all locations, it is now the locations which can be initial + corresponding variable values. |
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
from
c3a86ac to
6f0817f
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
from
d59dda6 to
5674ec7
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
4 times, most recently
from
d75d58e to
8d885de
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
4 times, most recently
from
c8d751a to
2eca1f7
Compare
blishko
left a comment
blishko
left a comment
There was a problem hiding this comment.
A few comments from first glance.
I'll take a proper look at the algorithm later.
| auto it = logic.getPterm(atom).begin(); | ||
| while (it != logic.getPterm(atom).end()) { | ||
| unrollAtom(logic, coefs, *it, reverse); | ||
| it++; | ||
| } |
There was a problem hiding this comment.
I don't think this is safe, since you are potentially creating new terms in unrollAtom.
You have to use index access to subterms.
| } | ||
|
|
||
| // This function is needed to extract specific atoms from the arithmetic formula | ||
| void unrollAtom(ArithLogic & logic, std::vector<PTRef> & coefs, PTRef atom, bool reverse) { |
There was a problem hiding this comment.
I don't understand the purpose of this function.
| } | ||
|
|
||
| // Function to turn everything in <= formulas | ||
| void lequalize(PTRef conjunct, vec<PTRef> & leqs, vec<PTRef> & bools, ArithLogic & logic) { |
There was a problem hiding this comment.
Doesn't Logic already do this for you?
There was a problem hiding this comment.
Hmm, I need to check
From what I get at least equalities remain in the formulas
We also introduce some >= during preprocessing
Otherwise you might be right...
There was a problem hiding this comment.
OK, I just wanted to double check.
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
2 times, most recently
from
e68c993 to
4850548
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
from
5a4049a to
4850548
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
from
83d39ed to
4850548
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
from
4850548 to
f09f7e0
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
from
89dce2e to
6cff093
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
from
973c37e to
3bc844d
Compare
BritikovKI
force-pushed
the
safe-nonterm-exp
branch
from
1158f71 to
9786dc2
Compare
2 participants
Extension of the safety-based nontermination detection with the parallel construction of transition invariants for transition relation reusing detected terminating traces by the safety-based nontermination.
These transition invariants are used to attempt proving termination during the nontermination detection procedure.