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

1778 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
20791a551f
feat: enforce time/memory limits in main runner 2022-02-17 13:09:48 -05:00
Simon Cruanes
e177534a46
chore: ugprade bare encoding 2022-02-16 14:20:27 -05:00
Simon Cruanes
c0288902c0
feat: check on_progress in more places 2022-02-16 13:24:43 -05:00
Simon Cruanes
5b0a2ad4a4
debug 2022-02-15 16:57:25 -05:00
Simon Cruanes
f3947f2237
update model construction function 2022-02-15 12:23:04 -05:00
Simon Cruanes
7f45cc6967
fix test 2022-02-14 11:36:50 -05:00
Simon Cruanes
fb552ba8b2
update expected test 2022-02-14 11:20:59 -05:00
Simon Cruanes
98c30bf0cc
updates and cleanup 2022-02-14 10:46:08 -05:00
Simon Cruanes
73289d1ded
test: regressions test for LRA 2022-02-08 13:45:43 -05:00
Simon Cruanes
e481c74398
refactor(LRA): new preprocessing, new shape of terms 2022-02-08 13:14:24 -05:00
Simon Cruanes
c22fc62f3e
base: remove simplex cases in arith terms 2022-02-08 13:14:07 -05:00
Simon Cruanes
f268e86100
refactor(smt-solver): preprocess literals in push_decision 2022-02-08 13:13:23 -05:00
Simon Cruanes
a81a21c341
core: add n_levels to monoid 2022-02-08 13:13:00 -05:00
Simon Cruanes
1d702029ee
fix(typecheck): use logic to decide default type of numerals 2022-02-08 13:12:29 -05:00
Simon Cruanes
82acf271d3
improve zarith and backtrackable table 2022-02-08 13:12:07 -05:00
Simon Cruanes
fbf7c5e090
chore: makefile 2022-02-08 13:11:36 -05:00
Simon Cruanes
d9a701140c
debug 2022-02-07 10:57:39 -05:00
Simon Cruanes
d11b9d585c
fix(smt): improve theory combination a bit 2022-02-04 16:40:55 -05:00
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