Add support for eldarica horn solver - #683

Open

Bixilon wants to merge 82 commits into

eldarica-benchexec

Commits on Mar 4, 2026

add eldarica to classpath
Bixilon
committed
92b8777

Commits on Mar 14, 2026

Cmdline: Added `JavaSMTMain` class, main entry point for the cmdline interface.
gcarpio21
committed
0d749c9
Cmdline: Added `CmdLineArgument` class.
gcarpio21
committed
6d2edd4
Cmdline: Added `CmdLineArguments` class.
gcarpio21
committed
fcb24db
Cmdline: Added `InvalidCmdlineArgumentException` class.
gcarpio21
committed
b2f8b28
Cmdline: Added `Output` class.
gcarpio21
committed
6af7ff8
Cmdline: Added `JavaSMTMainTest` test class.
gcarpio21
committed
df6dd0c
Cmdline: Added package info to `cmdline`.
gcarpio21
committed
685ecfd

Commits on Mar 19, 2026

refaster.
gcarpio21
committed
9f678f0
checkstyle.
gcarpio21
committed
b4a89b6
Cmdline: removed unused argument in a helper function from `CmdLineArgument`.
gcarpio21
committed
aba6237
format.
gcarpio21
committed
e90044b

Commits on Mar 31, 2026

Cmdline: removed preconditions check that the (set-logic) command should be at the start of the smt2 file to be parsed set by private helper method `sanitize` in `AbstractFormulaManager`.
gcarpio21
committed
7e5485a

Commits on Apr 27, 2026

boolean formular manager: horn api
Bixilon
committed
2fbab21
boolean formular manager: horn api
Bixilon
committed
2bee1ac

Commits on Apr 28, 2026

boolean formular manager: horn api
Bixilon
committed
1bfacde

Commits on May 5, 2026

add eldarica to classpath
Bixilon
committed
62dda73
eldarica: boolean -> horn converter
Bixilon
committed
8889ec5
HornProverEnvironment
Bixilon
committed
cb3b195
princess: add eldarica as horn prover environment
Bixilon
committed
8cd2f12
solver context: add eldarica as parser
Bixilon
committed
7625b0a

Commits on May 11, 2026

Merge remote-tracking branch 'origin/adding_eldarica' into adding_eldarica
Bixilon
committed
6b2e514

Commits on May 14, 2026

Merge branch 'master' into adding_eldarica
Bixilon
committed
4f4ead6
eldarica horn prover: support for quantifiers, improvements
Bixilon
committed
2bb4808
intellij classpath fixes
Bixilon
committed
3518963

Commits on May 19, 2026

eldarica: split horn converter from horn prover, deduplicate predicates
Bixilon
committed
7aaf6a9

Commits on May 26, 2026

various eldarica converter fixes
Bixilon
committed
813f5d6
horn sample test
Bixilon
committed
bcba11a

Commits on May 31, 2026

more smt tests
Bixilon
committed
3d1c0b5
eldarica horn converter: fix parameter as constraint rewriting
Bixilon
committed
8d7d0e8
fix all the conversion errors
Bixilon
committed
8e3ab2c

Commits on Jun 6, 2026

Commits on Jun 9, 2026

Commits on Jun 15, 2026

fix bad import :)
Bixilon
committed
7350c89

Commits on Jun 19, 2026

eldarica: horn: ITermITE
Bixilon
committed
ff7a6ce
fix all the code warnings
Bixilon
committed
2a5e5d3
bump princess
Bixilon
committed
ed0ee53
bump eldarica
Bixilon
committed
1d8449a
eldarica debug logging
Bixilon
committed
9c75aa6
git: ignore CPALog.txt*
Bixilon
committed
d975012

Commits on Jun 22, 2026

horn converter: crash more agressively
Bixilon
committed
acfdb5e
fix more conversion issues
Bixilon
committed
ae7fd42
smt2 tokenizer: allow declare-datatypes
Bixilon
committed
f940d0f
princess: map custom sorts to types
Bixilon
committed
9eba9ee

Commits on Jun 23, 2026

more conversion fixes
Bixilon
committed
b2b0d1b

Commits on Jun 24, 2026

horn converter: fix if then else
Bixilon
committed
2b83399

Commits on Jun 25, 2026

fix double simplification
Bixilon
committed
5f03487
fix ite conversion
Bixilon
committed
67e58d5

Commits on Jun 29, 2026

Commits on Jun 30, 2026

readme: add eldarica horn solver
Bixilon
committed
fef85df

Commits on Jul 6, 2026

Merge remote-tracking branch 'origin/master' into eldarica-benchexec
Bixilon
committed
b72bca1
web example: fix wrong princess version
Bixilon
committed
9540ef4
horn tests: use parameterized test
Bixilon
committed
6b52461

Commits on Jul 7, 2026

eldarica: wip model generation
Bixilon
committed
2f5fd8e

Commits on Jul 9, 2026

apply some suggestions

Bixilon
and
baierd
committed
47555e7

Commits on Jul 11, 2026

document EldaricaHornProver::solve

Bixilon
and
baierd
committed
75d01ad
eldarica: avoid using this. and parameter shadowing

Bixilon
and
baierd
committed
729b52d
eldarica: model retrieving
Bixilon
committed
cb11e42
eldarica: handle bool models properly
Bixilon
committed
c2faa77
eldarica horn prover: don't use var model
Bixilon
committed
2746273

Commits on Jul 19, 2026

eldarica: rewrite epsilon terms and quantifier
Bixilon
committed
ac16790

Commits on Jul 20, 2026

eldarica: fix rewriting of simple ite terms
Bixilon
committed
c9b9ef4
horn: test for epsilon rewriting and quation ite rewriting
Bixilon
committed
59d3aa8
only temporary disable some tests for eldarica, not horn in general
Bixilon
committed
8628f95
eldarica: explain better why ite is not supported
Bixilon
committed
53a8821
eldarica: properly rewrite ite terms
Bixilon
committed
11d5b1b
properly rewrite epsilon terms
Bixilon
committed
3fb9749
eldarica: don't support quantifiers inside formula
Bixilon
committed
df6ec6a

Commits on Jul 21, 2026

Commits on Jul 22, 2026

properly exclude CPALog.txt files
Bixilon
committed
b5717c8
eldarica: properly rewrite (nested) epsilon terms
Bixilon
committed
c07065d