simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 17:04:39 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 50bfe79b6a
         test: use dune options, so, release mode Simon Cruanes 2022-02-02 16:12:29 -05:00
  • dbb9dabd1d
         simpler printing of models Simon Cruanes 2022-02-02 16:12:11 -05:00
  • a0a67549de
         feat(lra): proper model production from the simplex Simon Cruanes 2022-02-02 16:02:23 -05:00
  • 3fdb07b533
         feat: handle get-model/get-value from smtlib inputs Simon Cruanes 2022-02-02 15:51:44 -05:00
  • 3b1535e70a deploy: 4cdbaf17bf c-cube 2022-02-02 03:26:50 +00:00
  • 4cdbaf17bf
         fix opam file Simon Cruanes 2022-02-01 22:21:03 -05:00
  • 70206101f0
         feat: update bare Simon Cruanes 2022-02-01 22:10:31 -05:00
  • c99e02b38a
         try to fix tests for now Simon Cruanes 2022-01-31 15:45:15 -05:00
  • 44ad0935fe
         chore: add QF_UFLIA to makefile Simon Cruanes 2022-01-31 15:45:02 -05:00
  • cb369ec68d
         easier list of known logic Simon Cruanes 2022-01-31 15:28:02 -05:00
  • 3c41ab2484
         refactor: new term representation for LIA/LRA Simon Cruanes 2022-01-31 15:13:25 -05:00
  • d4cf722d32
         wip: LIA: just relax to LRA for now Simon Cruanes 2022-01-31 15:12:55 -05:00
  • 8b78057058
         test: detail Simon Cruanes 2022-01-31 11:08:46 -05:00
  • 10c8006597
         intsolver: partial implementation Simon Cruanes 2022-01-31 11:08:20 -05:00
  • be7451b070
         add ediv to arith Simon Cruanes 2022-01-31 11:08:01 -05:00
  • e77d2b81ca
         wip: feat(intsolver): classify constraints into sets E,L,G,M Simon Cruanes 2022-01-19 11:43:35 -05:00
  • 04e9d5b93c
         test: limit size of linexps in simplex tests Simon Cruanes 2022-01-19 11:43:22 -05:00
  • a6c056969c
         test: limit size of linexps in intsolver tests Simon Cruanes 2022-01-19 11:42:42 -05:00
  • 7ea4c4fb4a
         arith: more functions in Int Simon Cruanes 2022-01-19 11:42:31 -05:00
  • 417f4cf8ec
         wip: intsolver Simon Cruanes 2022-01-14 13:50:07 -05:00
  • f713106514
         lia: use branch and bound a bit Simon Cruanes 2022-01-14 13:34:23 -05:00
  • eaf56a941f
         test: hook intsolver tests Simon Cruanes 2022-01-14 13:34:15 -05:00
  • af1a1478f2
         wip: feat(intsolver): new integer solver based on FM extension (Williams '75) Simon Cruanes 2022-01-14 13:31:17 -05:00
  • 6e0358f5e1
         refactor(simplex): small changes, mostly debug Simon Cruanes 2022-01-14 13:30:50 -05:00
  • 4a9a128ab0
         test: rename test simplex Simon Cruanes 2022-01-14 11:35:25 -05:00
  • 38a6727f44
         udpate test Simon Cruanes 2022-01-14 11:35:04 -05:00
  • 5989d686da
         chore: add target to makefile Simon Cruanes 2022-01-13 12:55:15 -05:00
  • 4b2afd7a05
         wip: LIA theory Simon Cruanes 2022-01-13 12:54:35 -05:00
  • 7f2e92fe88
         feat(arith): more functions in Q Simon Cruanes 2022-01-13 12:54:09 -05:00
  • f1f1967059
         refactor: move simplex to its own library sidekick.simplex Simon Cruanes 2022-01-13 12:50:22 -05:00
  • 803b40bccf
         refactor(sat): cleaner store for delayed actions Simon Cruanes 2022-01-11 16:50:59 -05:00
  • 999e83f91c
         fix(lra): remove bound propagation, it is sometimes late to the party Simon Cruanes 2022-01-11 12:22:46 -05:00
  • 44af0afd59
         fix(lia): problems with only integer constants are not incomplete Simon Cruanes 2022-01-11 13:17:01 -05:00
  • 8410a57f1a
         wip: feat(LIA): LIA solver, will rely on LRA solver Simon Cruanes 2022-01-10 16:51:45 -05:00
  • fb0668e7ba
         wip: feat(lra): expose state via a registry key Simon Cruanes 2022-01-10 16:51:30 -05:00
  • f7195bf980
         feat(smt): ability for a theory to declare we're in incomplete fragment Simon Cruanes 2022-01-10 16:50:55 -05:00
  • af8ab338e6
         feat(smt): add a registry to share values between theories Simon Cruanes 2022-01-10 16:50:38 -05:00
  • 849d4319f2
         fix theory combination for LRA Simon Cruanes 2022-01-05 11:59:50 -05:00
  • eb97161992
         better debug Simon Cruanes 2022-01-05 11:21:58 -05:00
  • 2378fc37ac
         fix LIA->LRA cast operation Simon Cruanes 2022-01-04 18:36:00 -05:00
  • 671fa6515a
         fix missing conversions Simon Cruanes 2022-01-04 18:25:28 -05:00
  • 3477f39b73
         fix handling of numeral constants Simon Cruanes 2022-01-04 18:18:33 -05:00
  • 691ff12a01
         wip: support LIA in input AST and base terms Simon Cruanes 2022-01-04 18:16:16 -05:00
  • 02a9abde3e
         feat: add Q.is_int Simon Cruanes 2022-01-04 11:11:30 -05:00
  • 2bce3e6dd9
         refactor(LRA): custom iterators in simplex, makes code more readable Simon Cruanes 2022-01-04 11:09:25 -05:00
  • 2d9f17b5b1
         fix(sat): use a set of delayed actions Simon Cruanes 2022-01-11 13:17:18 -05:00
  • 8b263d4d46
         fix(sat): when theory-propagating a literal below current level, backtrack Simon Cruanes 2022-01-11 12:35:03 -05:00
  • 1ffe778951
         feat(solver): eager checking of proofs for theory propagation Simon Cruanes 2022-01-11 12:21:17 -05:00
  • a33029129e
         fix(CC): bug introduced by sharing mutable lazy state Simon Cruanes 2022-01-10 12:11:32 -05:00
  • 78df8252dc
         bugfix in CC explanations Simon Cruanes 2022-01-05 10:31:33 -05:00
  • df033eaa7e deploy: 0afdb06f6c c-cube 2022-01-04 14:50:36 +00:00
  • 0afdb06f6c
         Merge branch 'wip-datatype-proofs' Simon Cruanes 2022-01-04 09:46:10 -05:00
  • b6df2cd974
         clause-less steps in proofs wip-datatype-proofs Simon Cruanes 2022-01-03 22:59:31 -05:00
  • 2e26fc79df deploy: 88f57d213a c-cube 2022-01-03 22:15:13 +00:00
  • 88f57d213a
         rename stat Simon Cruanes 2021-12-20 16:40:22 -05:00
  • dbba6719bc
         fix compilation after rebase Simon Cruanes 2021-12-20 13:57:41 -05:00
  • 9d3da47f3b
         fix: missing implied bound update Simon Cruanes 2021-03-21 18:51:44 -04:00
  • 73c9878554
         wip: feat(lra): clarify construction of bounds; fix sign error Simon Cruanes 2021-03-21 01:22:51 -04:00
  • 721c01d12c
         feat(lra): make Erat.{plus,minus}_inf saturating Simon Cruanes 2021-03-21 01:22:30 -04:00
  • 34b1aa1799
         wip: feat(lra): propagate literals based on implied bounds for basic vars Simon Cruanes 2021-03-21 01:14:33 -04:00
  • ab4e115b32
         tmp: restore some preprocessing wip-lra-simplex-propagations-implied-tmp-2022-01-03 Simon Cruanes 2022-01-03 16:15:42 -05:00
  • 63f50d03fa
         feat: proper proof production for theory merges in CC Simon Cruanes 2021-12-29 15:56:54 -05:00
  • 80cb096e8a
         feat: change signature of explanations for CC theory merges Simon Cruanes 2021-12-28 23:07:10 -05:00
  • 45845072af deploy: be1c1573b1 c-cube 2021-12-28 21:48:24 +00:00
  • be1c1573b1
         feat(proof): emit is-a terms properly Simon Cruanes 2021-12-28 16:46:59 -05:00
  • 8958301a8e
         fix: update quip CLI arguments Simon Cruanes 2021-12-28 10:57:30 -05:00
  • b2e8f8b29d
         chore: disable CI on windows temporarily Simon Cruanes 2021-12-21 11:31:53 -05:00
  • 6970c83ff1
         rename stat Simon Cruanes 2021-12-20 16:40:22 -05:00
  • 6d46d2225b deploy: 584b56075f c-cube 2021-12-20 20:47:54 +00:00
  • 584b56075f
         feat: add push/pop for assumptions; add check_sat_propagation_only Simon Cruanes 2021-12-20 15:34:34 -05:00
  • 1e48bd54c6
         fix compilation after rebase Simon Cruanes 2021-12-20 13:57:41 -05:00
  • 6900fb2f72
         fix: missing implied bound update Simon Cruanes 2021-03-21 18:51:44 -04:00
  • 135ca2319a
         wip: feat(lra): clarify construction of bounds; fix sign error Simon Cruanes 2021-03-21 01:22:51 -04:00
  • fc46cb53e0
         feat(lra): make Erat.{plus,minus}_inf saturating Simon Cruanes 2021-03-21 01:22:30 -04:00
  • 4a26e3cd3e
         wip: feat(lra): propagate literals based on implied bounds for basic vars Simon Cruanes 2021-03-21 01:14:33 -04:00
  • 054fd84a0c deploy: 5d2f8a1d3d c-cube 2021-12-20 18:53:21 +00:00
  • 5d2f8a1d3d
         feat(api): add callbacks to measure progress or ask solver to stop Simon Cruanes 2021-12-20 13:51:59 -05:00
  • c03fc97f00
         better debug in CC Simon Cruanes 2021-12-17 16:40:03 -05:00
  • be2d57a717
         feat(cc): add an invariant check before returning a model Simon Cruanes 2021-12-17 15:29:28 -05:00
  • b19d80e443
         debug Simon Cruanes 2021-12-17 15:13:48 -05:00
  • 44c63d4c13
         debug Simon Cruanes 2021-12-17 16:40:52 -05:00
  • f9f471ce12
         details Simon Cruanes 2021-12-17 13:46:48 -05:00
  • 46b13d08d0
         add regression test Simon Cruanes 2021-12-17 13:21:30 -05:00
  • 2d24a21908
         fix: do not preprocess but add equations eagerly for single-cstor terms Simon Cruanes 2021-12-17 11:58:39 -05:00
  • 6d72203437
         fix: avoid preprocessing loops Simon Cruanes 2021-12-17 11:48:41 -05:00
  • eca5139a03 deploy: 0841bddbaf c-cube 2021-12-17 16:41:10 +00:00
  • 0841bddbaf
         feat(data): preprocessing step for single-cstor types Simon Cruanes 2021-12-17 11:39:25 -05:00
  • 63eeb81290
         refactor: modify interface of Th_data Simon Cruanes 2021-12-17 11:38:52 -05:00
  • 3b409c8944
         feat(proof): add proof_r1 as a pendant to proof_p1 for non-equations Simon Cruanes 2021-12-17 11:38:07 -05:00
  • 3ab1ddfea8
         fix: ensure all functions in SMT solver preprocess their literals Simon Cruanes 2021-12-16 13:49:43 -05:00
  • 2b48901535 deploy: 4ac2eb25a6 c-cube 2021-12-08 02:30:55 +00:00
  • 4ac2eb25a6
         use TEF in sudoku; improve a bit its ergonomics Simon Cruanes 2021-12-07 21:29:51 -05:00
  • e64013c660
         chore: upgrade bare autogen-code Simon Cruanes 2021-12-07 21:16:25 -05:00
  • 110f3f8527
         update benchpress file to actually run proofs Simon Cruanes 2021-12-07 21:16:12 -05:00
  • 2d8fc78bc4
         add expect test for the sudoku solver Simon Cruanes 2021-12-07 14:19:25 -05:00
  • 49009aa346 deploy: 72d121fa64 c-cube 2021-12-07 19:11:45 +00:00
  • 72d121fa64
         add example: the suduko solver, adapted from msat Simon Cruanes 2021-12-07 14:10:36 -05:00
  • cfede762c9
         feat(sat): provide a proof_dumm module Simon Cruanes 2021-12-07 14:08:16 -05:00
  • 9517e88467
         feat(util): add backtrackable ref Simon Cruanes 2021-12-07 14:07:41 -05:00
  • 8030393136 deploy: a614fdb2e1 c-cube 2021-12-07 15:22:59 +00:00