Patrick Lühne
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
Patrick Lühne
86d2857494
Start implementation of simplifications
2020-05-19 12:56:46 +02:00
Patrick Lühne
82422cc28f
Support hiding auxiliary predicates
2020-05-13 08:02:04 +02:00
Patrick Lühne
b5d049a82a
Move InputConstantDeclarationDomains to problem module
2020-05-11 03:48:14 +02:00
Patrick Lühne
0d51053b88
Move ProofDirection type to separate module
2020-05-11 03:46:11 +02:00
Patrick Lühne
b55bc82b1d
Add option for proof direction
2020-05-07 02:53:48 +02:00
Patrick Lühne
e118442e16
Work in progress
2020-05-05 19:40:57 +02:00
Patrick Lühne
b6ecf37211
Add option for input constants
2020-02-05 19:40:21 +01:00
Patrick Lühne
caab0a618e
Add option for input predicates
2020-02-05 01:10:33 +01:00
Patrick Lühne
d7f04da0bd
Restructure project
2020-02-04 16:53:52 +01:00
Patrick Lühne
3dbe11be61
Restructure project
2020-02-04 16:45:13 +01:00
Patrick Lühne
9f4b7946f5
Add option for output format
2020-02-03 22:51:19 +01:00
Patrick Lühne
0714bed2cc
Start supporting TPTP output
2020-02-02 20:27:30 +01:00
Patrick Lühne
24980d5a8d
Refactoring to drop Context type
2020-02-01 19:20:46 +01:00
Patrick Lühne
6145c2cf1a
Translate body of rules for verifying properties
2020-01-31 17:19:44 +01:00
Patrick Lühne
a7e8368634
Work in progress
2020-01-24 13:32:43 +01:00