Skip to content

boolean formular manager: horn api#655

Open
Bixilon wants to merge 3 commits intomasterfrom
horn-clauses
Open

boolean formular manager: horn api#655
Bixilon wants to merge 3 commits intomasterfrom
horn-clauses

Conversation

@Bixilon
Copy link
Copy Markdown
Collaborator

@Bixilon Bixilon commented Apr 27, 2026

This makes it easy to create horn clauses in the form: (constraint \/ body) => head.

This is the "base" for adding eldarica as an additional parser.

I am not sure what to put into the debugging delegate manager, as all called functions are from the debugging interface. Does it make sense to add all the assertions again?

This makes it easy to create horn clauses in the form: `(constraint \/ body) => head`.
@Bixilon Bixilon requested a review from baierd April 27, 2026 18:33
Bixilon added 2 commits April 27, 2026 23:58
This makes it easy to create horn clauses in the form: `(constraint \/ body) => head`.
This makes it easy to create horn clauses in the form: `(constraint \/ body) => head`.
@baierd
Copy link
Copy Markdown
Contributor

baierd commented May 5, 2026

I am not sure whether we need this explicitly.

Spacer (Z3) simply does not work well in cases that are distinct from HORN clauses. But it does work well if you resolve the default form of horn-clauses into conjunctions for example.

Eldarica seems to also allow this according to its tests.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants