patrick
/
anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
162 Commits 1 Branch 3 Tags 380 KiB
Commit Graph

25 Commits

Author SHA1 Message Date
Patrick Lühne 9b6632cc94
Check that only input predicates are used in assumptions 2020-05-29 17:42:05 +02:00
Patrick Lühne 93db8d02b5
Implement tightness check 2020-05-29 14:57:00 +02:00
Patrick Lühne b52ca236e2
Handle private predicates in specification 2020-05-28 07:27:29 +02:00
Patrick Lühne 491a255811
Require supertight programs for backward proof 2020-05-28 05:03:56 +02:00
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 ab7c6d1828
Rename ScopedFormula to OpenFormula 2020-05-11 03:58:30 +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 7c36c4b239
Move closure functions to separate module 2020-05-11 03:41:33 +02:00
Patrick Lühne 0011fd9d4c
Add to-do note 2020-05-11 03:40:27 +02:00
Patrick Lühne cede63b7e4
Remove unused code 2020-05-11 03:37:57 +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 e6cf79ad1e
Remove unneeded indirection 2020-04-17 03:37:53 +02:00
Patrick Lühne 84bec338ae
Use foliage’s built-in variable declaration stack 2020-04-17 01:45:41 +02:00
Patrick Lühne becd8d4c19
Upgrade to foliage 0.2 development version 2020-04-17 00:09:44 +02:00
Patrick Lühne f83695b5dc
Move closure functions to utils module 2020-02-09 10:26:24 +07:00
Patrick Lühne ca5cca8701
Default to 0-ary predicates when omitting arity 2020-02-05 19:42:53 +01:00
Patrick Lühne b6ecf37211
Add option for input constants 2020-02-05 19:40:21 +01:00
Patrick Lühne 26c1bde49b
Move variable declaration stack from foliage crate 2020-02-05 02:30:17 +01:00
Patrick Lühne caab0a618e
Add option for input predicates 2020-02-05 01:10:33 +01:00
Patrick Lühne ce19860325
Make all terms compatible in TPTP 2020-02-04 23:33:59 +01:00
Patrick Lühne 87a3517bfb
Restructure project 2020-02-04 16:42:50 +01:00