Commit Graph

12 Commits

Author SHA1 Message Date
8c801426a5 Allow U, V, and W for program variables 2020-06-05 18:50:09 +02:00
27fff47c91 Minor refactoring 2020-05-29 18:42:14 +02:00
fc34aadf90 Show all predicates used in specification by default 2020-05-29 18:41:16 +02:00
93db8d02b5 Implement tightness check 2020-05-29 14:57:00 +02:00
e57a1859d2 Fix supertightness check 2020-05-28 18:37:34 +02:00
870fdd048c Handle input predicates correctly 2020-05-28 06:29:57 +02:00
491a255811 Require supertight programs for backward proof 2020-05-28 05:03:56 +02:00
9b7895a032 Don’t append variable ID if there is only one 2020-05-22 19:43:41 +02:00
116f74f63e Minor clean-up 2020-05-22 18:17:00 +02:00
81ddfd450a Use custom foliage flavor
With this patch, properties specific to variable, function, and
predicate declarations are directly stored within those objects rather
than external maps that need to be queried via traits. This greatly
simplifies many parts of the logic.

This is made possible by implementing a custom foliage flavor, which
makes it possible to swap the built-in declaration types for extended
versions of those types that fulfill certain requirements.
2020-05-22 02:25:00 +02:00
c3860c1bf1 Check variable declaration stack before using it 2020-02-09 10:22:08 +07:00
a7e8368634 Work in progress 2020-01-24 13:32:43 +01:00