ada/AdaSAT
0
0
Fork 0
mirror of https://github.com/AdaCore/AdaSAT.git synced 2026-02-12 13:11:23 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 3b5987efac Fix Internal_Array function for empty vectors. Romain Beguet 2022-06-30 22:37:02 +02:00
  • d0e81f49ee Improve CNF transformation of or conjunctives. Romain Beguet 2022-06-28 15:27:46 +02:00
  • 6042cd9fd9 Implement 'Exactly_One' proposition combinator. Romain Beguet 2022-06-27 21:08:02 +02:00
  • 6fffbbf5c2 Add Image subprogram on models. Romain Beguet 2022-06-27 17:54:28 +02:00
  • 3a82fda338 Implement not xor proposition. Romain Beguet 2022-06-27 17:54:18 +02:00
  • 375662ba4c Fix 'and' combinator. Romain Beguet 2022-06-27 17:54:03 +02:00
  • 38cc3c4f72 Fix regression with empty formulas. Romain Beguet 2022-06-25 12:22:34 +02:00
  • b9756540c1 Minor: style fix. Romain Beguet 2022-06-25 01:51:10 +02:00
  • 871d411099 Occur list indices should be literals. Romain Beguet 2022-06-25 01:41:23 +02:00
  • b35c90c5d1 Use manual iteration. Romain Beguet 2022-06-24 14:37:01 +02:00
  • 4d76734a8a Propagate relevant literals after T-Conflict. Romain Beguet 2022-06-24 13:45:00 +02:00
  • a6fc916cc8 Track next variable to decide. Romain Beguet 2022-06-24 00:54:53 +02:00
  • 7c323db609 Implement backjumping from theory conflicts. Romain Beguet 2022-06-24 00:37:11 +02:00
  • 9d2399b238 Add the 'implies' logical connective. Romain Beguet 2022-06-23 22:57:44 +02:00
  • 56fdc846f5 Minor tweak. Romain Beguet 2022-06-23 22:56:22 +02:00
  • 454c067140 Handle empty proposition in combinators. Romain Beguet 2022-06-23 22:55:59 +02:00
  • bc994af168 Fix crashes on trivial instances. Romain Beguet 2022-06-23 19:48:03 +02:00
  • d3a96b8970 Minor: add missing constant markers. Romain Beguet 2022-06-23 12:14:54 +02:00
  • 64ad40c158 Provide empty proposition object. Romain Beguet 2022-06-23 01:24:45 +02:00
  • 61630c4cc8 Allow destroying empty vectors. Romain Beguet 2022-06-23 01:24:32 +02:00
  • f3c2f4a757 Allow multiple CNF transformations. Romain Beguet 2022-06-22 21:00:55 +02:00
  • 86449b860c Implement Image on formulas and fix image for clauses. Romain Beguet 2022-06-22 20:59:52 +02:00
  • bb54cd0438 Add package for writing problems in propositional logic. Romain Beguet 2022-06-22 20:19:11 +02:00
  • e2d90fd629 Fix double free on UNSAT instances. Romain Beguet 2022-06-22 20:15:46 +02:00
  • 079d99fdf2 Minor: remove leftover comments. Romain Beguet 2022-06-22 20:14:36 +02:00
  • 6305521d3b Call system memory free directly. Romain Beguet 2022-06-22 20:14:12 +02:00
  • 5115c42786 Minor tweaks and style fixes. Romain Beguet 2022-06-22 16:40:48 +02:00
  • a3ee115039 Propagate pivot after backjumping. Romain Beguet 2022-06-22 16:28:55 +02:00
  • d9e1d44c08 Use custom realloc-based vector implementation. Romain Beguet 2022-06-22 14:12:14 +02:00
  • e7a200c749 Implement Image for Clause objects. Romain Beguet 2022-06-21 01:49:54 +02:00
  • 8a952b9924 Make sure pivot appears only once to optimize its removal. Romain Beguet 2022-06-21 01:35:47 +02:00
  • ff725ea669 Optimize resolution routine. Romain Beguet 2022-06-21 01:20:28 +02:00
  • f1e674e33a Aggressively inline common variable/literal ops. Romain Beguet 2022-06-21 00:58:45 +02:00
  • 4dfca41c51 Keep first pivot found. Romain Beguet 2022-06-20 23:54:17 +02:00
  • 1e1b9a62a8 Update README.md Beguet Romain 2022-06-20 23:41:04 +02:00
  • 7da146ea35 Add lib/ folder to gitignore. Romain Beguet 2022-06-20 23:40:23 +02:00
  • 52e4e04c07 Add empty sudoku grid. Romain Beguet 2022-06-20 23:39:46 +02:00
  • dc7ca920b2 Implement occurrence lists. Romain Beguet 2022-06-20 22:38:39 +02:00
  • 733e91ddd3 Introduce an internal representation of the formula that uses a vector. Romain Beguet 2022-06-20 22:35:22 +02:00
  • 6df4a3eb00 Minor: rename variable. Romain Beguet 2022-06-20 18:43:34 +02:00
  • 069ccc55d8 Create README.md Beguet Romain 2022-06-20 00:07:08 +02:00
  • bc2b2a4faf Implement sudoku solver. Romain Beguet 2022-06-19 23:37:56 +02:00
  • 328060e997 Update project compilation switches. Romain Beguet 2022-06-19 23:37:24 +02:00
  • c03965c68a Remove logging. Romain Beguet 2022-06-19 22:50:47 +02:00
  • fe17c64b00 Add more documentation. Romain Beguet 2022-06-19 18:33:01 +02:00
  • fc941dc731 Use clause access directly instead of array indirection. Romain Beguet 2022-06-19 17:52:38 +02:00
  • 4766c27f3b Clarify types and add some documentation. Romain Beguet 2022-06-19 17:37:45 +02:00
  • 5c232c22b1 Distinguish variables and literals at the type-level- Romain Beguet 2022-06-19 17:13:42 +02:00
  • 1919ed92b2 Implement conflict analysis and backjumping. Romain Beguet 2022-06-19 16:13:49 +02:00
  • 1686406338 Allow theory to return empty clauses. Romain Beguet 2022-06-19 16:13:39 +02:00
  • e90f7f9ebc Initial commit. Romain Beguet 2022-06-05 15:13:57 +02:00