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

  • 01e9a19b61 Merge branch 'topic/free_clause' into 'master' master v26.0.0 v25.0.0 26.1 26.0 25.2 25.1 25.0 25-sustained Raphaël Amiard 2024-01-03 17:00:52 +00:00
  • 593416e78e Expose procedure for deallocating a Clause. Romain Beguet 2023-12-22 12:06:31 +01:00
  • f20d814a4b Merge branch 'topic/24.1' into '24.1' 24.2 24.1 24-sustained Romain Béguet 2023-12-14 13:12:24 +00:00
  • 88335657f8 Fix memory leak in test. Romain Beguet 2023-12-14 12:20:19 +01:00
  • 64a3da5136 Merge branch 'topic/leak_test' into 'master' Romain Béguet 2023-12-14 11:24:05 +00:00
  • da722226d3 Fix memory leak in test. Romain Beguet 2023-12-14 12:20:19 +01:00
  • 1390025423 Merge branch '241_fast_forward' into '24.1' Romain Béguet 2023-12-11 15:21:28 +00:00
  • b1dd7ff0e9 Merge branch 'topic/improve_resolution' into 'master' Romain Béguet 2023-11-06 10:22:39 +00:00
  • 66f6607e18 Avoid unnecessary cycles in conflict resolution. Romain Beguet 2023-05-30 11:56:07 +02:00
  • 4a316fe76a Merge branch 'topic/lal-1108' into 'master' Romain Béguet 2023-10-31 10:30:28 +00:00
  • 4efe6a48d3 Allocate data structures on the heap. Romain Beguet 2023-10-19 10:05:18 +02:00
  • f2e06e4a8a Merge branch 'pmderodat/ci' into 'master' Pierre-Marie de Rodat 2023-10-25 10:09:10 +00:00
  • 910db1aaf3 Various CI cleanups Pierre-Marie de Rodat 2023-10-25 08:22:38 +00:00
  • 3ed4895b3a Merge branch 'pmderodat/ci' into 'master' v24.0.0 24.0 Pierre-Marie de Rodat 2023-09-26 14:17:06 +00:00
  • 32496cb7ef CI: add MR issue checker Pierre-Marie de Rodat 2023-09-26 15:54:38 +02:00
  • 55b2b3c404 Merge branch 'pmderodat/cb' into 'master' Pierre-Marie de Rodat 2023-06-21 12:52:03 +00:00
  • 7b167fc433 CB: refactor to use common config from the Libadalang repository Pierre-Marie de Rodat 2023-06-21 12:38:08 +00:00
  • 354e7a2201 Merge branch 'pmderodat/cb' into 'master' Pierre-Marie de Rodat 2023-06-20 14:50:43 +00:00
  • 53e9dc5d89 .gitlab-ci.yml: switch CB to --smart-rebuild Pierre-Marie de Rodat 2023-06-20 12:03:52 +00:00
  • 420b26dcb6 Merge branch 'pmderodat/cb' into 'master' Pierre-Marie de Rodat 2023-06-05 12:39:55 +00:00
  • 08088e9027 .gitlab-ci.yml: add a CB for AdaSAT Pierre-Marie de Rodat 2023-06-05 11:10:16 +00:00
  • 319c2b00e1 Merge branch 'topic/update-license' into 'master' Romain Béguet 2023-05-30 16:52:32 +00:00
  • e0c4774a4e Re-license AdaSAT to Apache 2.0 + LLVM Exception. Romain Beguet 2023-05-30 12:03:08 +02:00
  • f948e2271a VB22-027: Fix potential leak when resolution fails early in backjumping routine. Romain Beguet 2023-01-20 14:48:09 +01:00
  • 9314120fa8 VB22-027: Avoid leaking when theory check raises an exception. Romain Beguet 2023-01-12 15:36:21 +01:00
  • d4bcffad68 VB22-027: Avoid memory leak when resolution fails early. Romain Beguet 2023-01-12 11:28:27 +01:00
  • 05f486b280 Testsuite: add a mode to run tests under Valgrind Pierre-Marie de Rodat 2023-01-12 14:35:58 +00:00
  • 49fb5ee0d1 Address comment from Raph's review. Romain Beguet 2022-12-19 13:00:05 +01:00
  • 4be0f21454 Add -flto flag to prod builds. Romain Beguet 2022-12-06 10:36:59 +01:00
  • 8c79a6ae03 VB22-027: Mention python instead of python3 in testsuite runner. Romain Beguet 2022-12-20 14:47:03 +01:00
  • 6fd0822586 VB22-027: Quote paths given to relocate-build-tree. Romain Beguet 2022-12-20 14:31:26 +01:00
  • 856f864dac Minor fixes Raphaël AMIARD 2022-12-13 10:33:14 +00:00
  • c0dcb32803 Minor fixes in the README Raphaël AMIARD 2022-12-12 14:08:36 +00:00
  • 480f42937c Fix erroneous assumption when propagating AMO constraint. Romain Beguet 2022-11-21 18:00:25 +01:00
  • 5d5a2beb49 Remove useless code. Romain Beguet 2022-11-16 12:31:01 +01:00
  • 67136017b2 Minor: add missing subprogram box. Romain Beguet 2022-11-16 11:57:02 +01:00
  • 0d84d973f8 VB22-027: Add makefile to simplify anod spec. Romain Beguet 2022-11-22 12:48:24 +01:00
  • e1ed3a29ff Add fancy WaveFunctionCollapse test. Romain Beguet 2022-11-15 11:01:07 +01:00
  • de347fdf37 Allow custom decision procedures. Romain Beguet 2022-11-15 10:52:09 +01:00
  • 34bcfc9e22 Update README.md Beguet Romain 2022-11-10 16:09:03 +01:00
  • 97907a8ceb Add license. Romain Beguet 2022-11-10 15:54:40 +01:00
  • 33659924da Add test for custom theories. Romain Beguet 2022-11-10 15:53:56 +01:00
  • e6c864bfbc Add test for AMO constraints. Romain Beguet 2022-11-10 14:49:56 +01:00
  • 6dbef8e7c9 Propagate directly inside Check_Assign. Romain Beguet 2022-11-10 14:49:24 +01:00
  • d8d5aeb688 Allow copying Formula_Builder objects. Romain Beguet 2022-11-10 14:49:10 +01:00
  • 230c80a12b Setup e3-testsuite. Romain Beguet 2022-11-10 12:10:37 +01:00
  • d2f7ed0975 Slightly improve documentation of Is_Feasible. Romain Beguet 2022-11-10 11:35:10 +01:00
  • 633440bcbe Fix handling of AMO constraints in Add_Simplify. Romain Beguet 2022-11-10 11:34:43 +01:00
  • 223faaf883 Move creation of AMO constraints to Builders package. Romain Beguet 2022-11-09 16:14:34 +01:00
  • b5836ca12b Add more documentation. Romain Beguet 2022-11-09 15:43:53 +01:00
  • 1eba0a4a34 Remove unused AdaSAT.Propositions package and test. Romain Beguet 2022-11-09 15:31:17 +01:00
  • 439a877080 Add missing subprogram boxes. Romain Beguet 2022-11-09 15:27:51 +01:00
  • 2297b1ca2b Add Helpers package with empty theory to simplify tests. Romain Beguet 2022-11-09 15:23:00 +01:00
  • fadaa4836b Add more documentation. Romain Beguet 2022-11-09 15:03:32 +01:00
  • 8be46c91aa Fix and improve the Builders package. Romain Beguet 2022-11-09 12:52:55 +01:00
  • 364a545391 Add license headers. Romain Beguet 2022-11-09 12:19:19 +01:00
  • c0ceca90b3 Refactor slightly the theory Check subprogram. Romain Beguet 2022-11-09 12:10:18 +01:00
  • 725c9db6c6 Simplify Clause_Builder API. Romain Beguet 2022-11-09 11:58:46 +01:00
  • e384201446 Change project name to AdaSAT. Romain Beguet 2022-11-08 12:27:08 +01:00
  • b32b8a64fe Improve handling of 1 literal clauses. Romain Beguet 2022-11-07 14:28:26 +01:00
  • de8094ebd6 Fix memory leaks in Add_Simplify. Romain Beguet 2022-11-07 12:03:26 +01:00
  • e1c932c8f9 Reset blocking literal in all code paths. Romain Beguet 2022-11-04 17:48:03 +01:00
  • c360103863 Update tests. Romain Beguet 2022-11-04 17:30:06 +01:00
  • a51e1f8274 Update README.md Romain Beguet 2022-11-04 17:12:46 +01:00
  • 3e763e6ea7 Document and simplify unit propagation. Romain Beguet 2022-11-04 15:52:39 +01:00
  • eeb0bb7f28 Use proper iteration bounds for clause re-ordering. Romain Beguet 2022-11-04 15:17:09 +01:00
  • aacd0b5980 Improve explanations of the backjumping routine. Romain Beguet 2022-11-04 15:12:19 +01:00
  • 70d27a878c Simplify backjumping. Romain Beguet 2022-11-04 12:56:35 +01:00
  • 88366bcb8b Remove obselete code. Romain Beguet 2022-11-04 12:43:34 +01:00
  • 636bbb124a Factor out clause re-ordering. Romain Beguet 2022-11-04 12:42:31 +01:00
  • ce3e464ebb Remove temporary counter. Romain Beguet 2022-11-03 15:23:24 +01:00
  • 60e40a3a56 Further implement 2-watched literals. Romain Beguet 2022-11-03 15:17:48 +01:00
  • d7cc592a75 Implement Add_Simplify on clause builders. Romain Beguet 2022-11-03 15:15:49 +01:00
  • 0e4327d9af Simplify propagation of binary clauses. Romain Beguet 2022-11-02 21:08:28 +01:00
  • 682519bf73 Start implementing the two-watched literals scheme. Romain Beguet 2022-11-02 18:47:44 +01:00
  • b228291b38 Add some debug logging. Romain Beguet 2022-11-02 16:59:21 +01:00
  • 038f492ecd Add Reserve on clause builders. Romain Beguet 2022-11-02 15:32:54 +01:00
  • 0b5c94ef1d Add built-in support for AMO constraints. Romain Beguet 2022-10-29 03:03:16 +02:00
  • f39f19829d Use vectors for formulas. Romain Beguet 2022-10-29 03:01:56 +02:00
  • 1ab449feb5 Use default argument instead of alternative subp. Romain Beguet 2022-10-28 11:37:28 +02:00
  • d90a93d0e7 Simplify clauses holder component in internal formula. Romain Beguet 2022-10-27 15:04:40 +02:00
  • 95327666ea Simplify unit propagation. Romain Beguet 2022-10-26 12:38:39 +02:00
  • f710ad24b9 Minor tweaks. Romain Beguet 2022-10-25 15:37:54 +02:00
  • 0050b0c268 Fix crash on empty explanations. Romain Beguet 2022-10-25 15:37:37 +02:00
  • d388d42605 Implement Is_Feasible. Romain Beguet 2022-10-25 00:42:13 +02:00
  • 6116bfe367 Introduce watchers. Romain Beguet 2022-10-24 17:04:09 +02:00
  • 4323c8e95c Fix erroneous loop bounds. Romain Beguet 2022-10-24 12:23:57 +02:00
  • 3bda51f4a8 Rework theory API to allow user contexts. Romain Beguet 2022-10-03 17:36:59 +02:00
  • 4777e0d83f Provide Add_Simplify in clause builders. Romain Beguet 2022-10-03 17:36:06 +02:00
  • a4e380dee4 Add 'profile' build mode. Romain Beguet 2022-10-03 17:35:28 +02:00
  • 4b0367fdab Fix memory leaks. Romain Beguet 2022-09-26 14:23:01 +02:00
  • 058e8cb690 Remove leftover logging. Romain Beguet 2022-07-04 23:53:01 +02:00
  • b440f4d9b6 Optimize adding elements to propagation stack. Romain Beguet 2022-07-04 22:59:39 +02:00
  • 81cc7019e6 Add partial solve implementation. Romain Beguet 2022-07-04 22:16:17 +02:00
  • 85e8189d79 Fix backjump after T-Explanation. Romain Beguet 2022-07-02 00:07:39 +02:00
  • 167b04d0a5 Relocate true literal in front of the clause. Romain Beguet 2022-07-01 23:31:41 +02:00
  • 4b5278de0b Early exit from unit clause detection. Romain Beguet 2022-07-01 23:30:32 +02:00
  • 472a156b1c Optimize vector iteration. Romain Beguet 2022-07-01 16:21:48 +02:00
  • a53430b06b Extend formula builders API. Romain Beguet 2022-07-01 01:02:49 +02:00
  • 9d2aea9645 Provide formula builders. Romain Beguet 2022-06-30 22:39:27 +02:00