Commit Graph

16 Commits

Author SHA1 Message Date
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