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
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
Simon Cruanes
2bce3e6dd9
refactor(LRA): custom iterators in simplex, makes code more readable
2022-01-11 14:00:03 -05:00
Simon Cruanes
2d9f17b5b1
fix(sat): use a set of delayed actions
...
this prevents some bad interactions caused by mixing propagations
(which can backjump) and iterating on the trail from a theory.
2022-01-11 14:00:03 -05:00
Simon Cruanes
8b263d4d46
fix(sat): when theory-propagating a literal below current level, backtrack
...
it can be triggered by local clause addition (in DT for example), which
is hard to avoid.
2022-01-11 14:00:03 -05:00
Simon Cruanes
1ffe778951
feat(solver): eager checking of proofs for theory propagation
...
bugs where a literal is propagated "too late" (at current level)
when the cause stems from previous levels, thus leading to invalid
clause learning (non UIP clauses) since some literals are not resolved
away as they're "too low", are hard to debug.
so we just check that propagation level coincides with current level.
2022-01-11 14:00:03 -05:00
Simon Cruanes
a33029129e
fix(CC): bug introduced by sharing mutable lazy state
2022-01-10 12:11:32 -05:00
Simon Cruanes
78df8252dc
bugfix in CC explanations
2022-01-05 10:31:33 -05:00
Simon Cruanes
0afdb06f6c
Merge branch 'wip-datatype-proofs'
2022-01-04 09:46:10 -05:00
Simon Cruanes
b6df2cd974
clause-less steps in proofs
...
these steps are checked only once, to accelerate checking, but the
result isn't known.
2022-01-03 22:59:43 -05:00
Simon Cruanes
88f57d213a
rename stat
2022-01-03 17:13:55 -05:00
Simon Cruanes
dbba6719bc
fix compilation after rebase
2022-01-03 17:13:55 -05:00
Simon Cruanes
9d3da47f3b
fix: missing implied bound update
2022-01-03 17:13:55 -05:00
Simon Cruanes
73c9878554
wip: feat(lra): clarify construction of bounds; fix sign error
2022-01-03 17:13:55 -05:00
Simon Cruanes
721c01d12c
feat(lra): make Erat.{plus,minus}_inf saturating
2022-01-03 17:13:54 -05:00
Simon Cruanes
34b1aa1799
wip: feat(lra): propagate literals based on implied bounds for basic vars
2022-01-03 17:13:54 -05:00
Simon Cruanes
63f50d03fa
feat: proper proof production for theory merges in CC
...
this involves resolution steps between the lemma (typically a kind of
horn clause with the merge as conclusion) and a bunch of literals
responsible for some equational hypotheses of this horn clause, being true
2021-12-29 15:56:54 -05:00
Simon Cruanes
80cb096e8a
feat: change signature of explanations for CC theory merges
2021-12-28 23:07:27 -05:00
Simon Cruanes
be1c1573b1
feat(proof): emit is-a terms properly
...
these occur in datatypes proofs.
2021-12-28 16:46:59 -05:00
Simon Cruanes
584b56075f
feat: add push/pop for assumptions; add check_sat_propagation_only
...
this gives the user the possibility of controlling search by mostly
using assumptions (and the underlying assumption stack) as well as
boolean+theory propagation. The result is **not** complete, but can
still help as a beefed-up contextual simplifier.
2021-12-20 15:34:34 -05:00
Simon Cruanes
5d2f8a1d3d
feat(api): add callbacks to measure progress or ask solver to stop
2021-12-20 13:51:59 -05:00
Simon Cruanes
c03fc97f00
better debug in CC
2021-12-17 16:41:00 -05:00
Simon Cruanes
be2d57a717
feat(cc): add an invariant check before returning a model
2021-12-17 16:41:00 -05:00
Simon Cruanes
b19d80e443
debug
2021-12-17 16:40:59 -05:00
Simon Cruanes
44c63d4c13
debug
2021-12-17 16:40:52 -05:00
Simon Cruanes
f9f471ce12
details
2021-12-17 13:46:48 -05:00
Simon Cruanes
2d24a21908
fix: do not preprocess but add equations eagerly for single-cstor terms
2021-12-17 11:58:39 -05:00
Simon Cruanes
6d72203437
fix: avoid preprocessing loops
2021-12-17 11:48:41 -05:00
