Skip to content

Feature/extend safety #375

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 51 commits into from
Jun 20, 2022
Merged

Feature/extend safety #375

merged 51 commits into from
Jun 20, 2022

Conversation

rkaminsk
Copy link
Member

@rkaminsk rkaminsk commented Jun 3, 2022 •
edited
Loading

Compute intervals by computing bounds for linear equations given by comparison literals to extend safety. The examples below give an overview of contexts where this feature is applicable.

% conjunction
2 { p(1..3) } 3.
q :- p(X): 1 <= X <= 3.
% disjunction
p(X): 1 <= X <= 3.
% head aggregate
2 { p(X): 1 <= X <= 3 } 3.
2 #count { X: p(X): 1 <= X <= 3 } 3.
% body aggregate
2 { p(1..3) } 3.
q :- 2 { p(X): 1 <= X <= 3 } 3.
q :- 2 #count { X: p(X), 1 <= X <= 3 } 3.
% rule
0 { p(1..3) } 2.
q :- p(X), 1 <= X <= 3.

rkaminsk added 30 commits May 18, 2022 18:15
@rkaminsk
begin to implement #366
cab5176
@rkaminsk
add basic bound computation algorithm
34d4e2c
@rkaminsk
add function to add terms to linear terms for the iesolver
778715e
@rkaminsk
add function to add inequalities to solver
1705fb2 
- this can be done nicer still
- this can be extended to further conjunctive contexts
@rkaminsk
refactor
6ec59c6
@rkaminsk
refactor
1c76259
@rkaminsk
refactor utility.hh
bfdcc70
@rkaminsk
refactor program builder
f609df2
@rkaminsk
whitespace
f8ba571
@rkaminsk
refactor (non)groundparser
3ad0f79
@rkaminsk
refactor sources in input and base
e466f3a 
- headers in base are still missing
@rkaminsk
refactor a bit
76d074b
@rkaminsk
refactor
0e722ac
@rkaminsk
refactor graph
2ce5216
@rkaminsk
cleanup interface
2d1a47f
@rkaminsk
refactor hash_set
19b937e
@rkaminsk
refactor interval and lexerstate
f760611
@rkaminsk
refactor backtrace.hh
9cd3d05
@rkaminsk
refactor logger
653e5f2
@rkaminsk
refactor output/aggregates
9ffc4de
@rkaminsk
refactor output/backends
16ab9e1
@rkaminsk
refactor output/literal
19604b9
@rkaminsk
refactor output literals
161937e
@rkaminsk
refactor output/output
ca9e134
@rkaminsk
refactor output/statement
7decdb0
@rkaminsk
refactor output/statements
da741dd
@rkaminsk
refactor output/theory
4959493
@rkaminsk
refactor output
922f6d5
@rkaminsk
remove/distribute some forward declarations
5a6b270
@rkaminsk
install libffi
2b0f034
@rkaminsk rkaminsk linked an issue Jun 3, 2022 that may be closed by this pull request
Extend safety by computing intervals from comparisons #366
Closed
rkaminsk added 5 commits June 7, 2022 16:32
@rkaminsk
create interfaces for nested iesolver
79ee0f9
@rkaminsk
prepare for nested ie solving
450c9c5 
- remove unused beforeRewrite logic
- introdcue ie contexts for nested solving
@rkaminsk
implement nested bound computation for body aggregates
d731bc4 
- this provides the basic infrastructure to implement bound computation
  for the remaining language constructs
- the tests for the ie solver should be extended for nested scopes
@rkaminsk
compute bounds for head and body aggregates
7618021 
- this commit also refactors head aggregate elements
- tests are still missing
@rkaminsk
simplify
79e75ea
@rkaminsk rkaminsk force-pushed the feature/extend-safety branch 2 times, most recently from 1f796a1 to 79e75ea Compare June 10, 2022 16:20
@rkaminsk rkaminsk force-pushed the feature/extend-safety branch from 0683928 to cbf4384 Compare June 19, 2022 11:44
@rkaminsk rkaminsk self-assigned this Jun 20, 2022
@rkaminsk rkaminsk merged commit 8084ebd into wip Jun 20, 2022
@rkaminsk rkaminsk deleted the feature/extend-safety branch June 28, 2022 12:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@rkaminsk rkaminsk

Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Extend safety by computing intervals from comparisons
1 participant
@rkaminsk