simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
1710 commits 53 branches 1 tag 17 MiB
Commit graph

1710 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
ab74b1a792
fix(lra): preprocessing of linexps with non-zero constants 2022-02-04 16:16:00 -05:00
Simon Cruanes
cbc9c5ac6f
refactor(smt): preprocessing is now using a queue of delayed actions 
- preprocessing doesn't simplify anymore, it assumes terms are already
  simplified. It only adds clauses/adds literals, it does not return
  new terms.
- adding clauses/literals to SAT is done as delayed actions, to avoid
  issues of reentrancy.
  These actions are performed after preprocessing, in a loop that has
  access to the SAT solver.
 2022-02-04 16:08:01 -05:00
Simon Cruanes
f9036fa33b
feat(bool): do not eliminate ite terms. 
API users might need to traverse the terms they gave to sidekick, and
analyze their structure. This can't work if we have removed some of it,
like `ite`.
 2022-02-04 09:24:27 -05:00
Simon Cruanes
2885563929
fix(lra): better handling of model production for preprocessed-away terms 2022-02-03 14:24:07 -05:00
Simon Cruanes
9cf9b025ab
debug 2022-02-03 14:20:32 -05:00
Simon Cruanes
a98132ed0c
feat(model): add theory hooks to "complete" models 
these hooks are allowed to add terms to the model, that are not in the
congruence closure (for example in LRA, terms that were preprocessed
away).
 2022-02-03 14:00:43 -05:00
Simon Cruanes
c4bbaddc06
new regression test for (get-model); fix mdx test 2022-02-02 16:12:55 -05:00
Simon Cruanes
50bfe79b6a
test: use dune options, so, release mode 2022-02-02 16:12:29 -05:00
Simon Cruanes
dbb9dabd1d
simpler printing of models 2022-02-02 16:12:11 -05:00
Simon Cruanes
a0a67549de
feat(lra): proper model production from the simplex 2022-02-02 16:02:23 -05:00
Simon Cruanes
3fdb07b533
feat: handle get-model/get-value from smtlib inputs 2022-02-02 15:51:44 -05:00
Simon Cruanes
4cdbaf17bf
fix opam file 2022-02-01 22:21:03 -05:00
Simon Cruanes
70206101f0
feat: update bare 2022-02-01 22:10:31 -05:00
Simon Cruanes
c99e02b38a
try to fix tests for now 2022-01-31 15:45:15 -05:00
Simon Cruanes
44ad0935fe
chore: add QF_UFLIA to makefile 2022-01-31 15:45:02 -05:00
Simon Cruanes
cb369ec68d
easier list of known logic 2022-01-31 15:28:02 -05:00
Simon Cruanes
3c41ab2484
refactor: new term representation for LIA/LRA 2022-01-31 15:13:25 -05:00
Simon Cruanes
d4cf722d32
wip: LIA: just relax to LRA for now 2022-01-31 15:12:55 -05:00
Simon Cruanes
8b78057058
test: detail 2022-01-31 11:08:46 -05:00
Simon Cruanes
10c8006597
intsolver: partial implementation 2022-01-31 11:08:20 -05:00
Simon Cruanes
be7451b070
add ediv to arith 2022-01-31 11:08:01 -05:00
Simon Cruanes
e77d2b81ca
wip: feat(intsolver): classify constraints into sets E,L,G,M 2022-01-19 11:43:35 -05:00
Simon Cruanes
04e9d5b93c
test: limit size of linexps in simplex tests 2022-01-19 11:43:22 -05:00
Simon Cruanes
a6c056969c
test: limit size of linexps in intsolver tests 2022-01-19 11:42:42 -05:00
Simon Cruanes
7ea4c4fb4a
arith: more functions in Int 2022-01-19 11:42:31 -05:00
Simon Cruanes
417f4cf8ec
wip: intsolver 2022-01-14 13:50:07 -05:00
Simon Cruanes
f713106514
lia: use branch and bound a bit 
this should be removed when we use the intsolver, alongside a pure real
relaxation of int constraints…
 2022-01-14 13:34:23 -05:00
Simon Cruanes
eaf56a941f
test: hook intsolver tests 2022-01-14 13:34:15 -05:00
Simon Cruanes
af1a1478f2
wip: feat(intsolver): new integer solver based on FM extension (Williams '75) 2022-01-14 13:31:17 -05:00
Simon Cruanes
6e0358f5e1
refactor(simplex): small changes, mostly debug 2022-01-14 13:30:50 -05:00
Simon Cruanes
4a9a128ab0
test: rename test simplex 2022-01-14 11:35:25 -05:00
Simon Cruanes
38a6727f44
udpate test 2022-01-14 11:35:04 -05:00
Simon Cruanes
5989d686da
chore: add target to makefile 2022-01-13 12:55:36 -05:00
Simon Cruanes
4b2afd7a05
wip: LIA theory 2022-01-13 12:55:36 -05:00
Simon Cruanes
7f2e92fe88
feat(arith): more functions in Q 2022-01-13 12:55:35 -05:00
Simon Cruanes
f1f1967059
refactor: move simplex to its own library sidekick.simplex 
also start branch and bound
 2022-01-13 12:55:35 -05:00
Simon Cruanes
803b40bccf
refactor(sat): cleaner store for delayed actions 
handles clauses to add, propagations, and decisions. The latter ones are
cleared on backtrack (but not clauses).
 2022-01-11 16:50:59 -05:00
Simon Cruanes
999e83f91c
fix(lra): remove bound propagation, it is sometimes late to the party 
propagation at the wrong level is not supported.
 2022-01-11 14:00:05 -05:00
Simon Cruanes
44af0afd59
fix(lia): problems with only integer constants are not incomplete 2022-01-11 14:00:05 -05:00
Simon Cruanes
8410a57f1a
wip: feat(LIA): LIA solver, will rely on LRA solver 
we want to reuse the simplex, but do branch and bound + cutting planes
 2022-01-11 14:00:04 -05:00
Simon Cruanes
fb0668e7ba
wip: feat(lra): expose state via a registry key 2022-01-11 14:00:04 -05:00
Simon Cruanes
f7195bf980
feat(smt): ability for a theory to declare we're in incomplete fragment 2022-01-11 14:00:04 -05:00
Simon Cruanes
af8ab338e6
feat(smt): add a registry to share values between theories 2022-01-11 14:00:04 -05:00
Simon Cruanes
849d4319f2
fix theory combination for LRA 2022-01-11 14:00:04 -05:00
Simon Cruanes
eb97161992
better debug 2022-01-11 14:00:04 -05:00
Simon Cruanes
2378fc37ac
fix LIA->LRA cast operation 2022-01-11 14:00:04 -05:00
Simon Cruanes
671fa6515a
fix missing conversions 2022-01-11 14:00:04 -05:00
Simon Cruanes
3477f39b73
fix handling of numeral constants 2022-01-11 14:00:04 -05:00
Simon Cruanes
691ff12a01
wip: support LIA in input AST and base terms 2022-01-11 14:00:03 -05:00
Simon Cruanes
02a9abde3e
feat: add Q.is_int 2022-01-11 14:00:03 -05:00