From 64871caf35cd9dc2520a4de3a9f39b30155c88d4 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 29 Jul 2024 09:06:27 +1000 Subject: [PATCH 1/2] Update Kissat to version 4.0.0 --- crates/pindakaas-kissat/Cargo.toml | 2 +- crates/pindakaas-kissat/build.rs | 10 ++++++++++ crates/pindakaas-kissat/vendor/kissat | 2 +- 3 files changed, 12 insertions(+), 2 deletions(-) diff --git a/crates/pindakaas-kissat/Cargo.toml b/crates/pindakaas-kissat/Cargo.toml index b8d79bf45c..71c34caa5d 100644 --- a/crates/pindakaas-kissat/Cargo.toml +++ b/crates/pindakaas-kissat/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "pindakaas-kissat" -version = "3.1.1" +version = "4.0.0" edition = "2021" build = "build.rs" links = "kissat" diff --git a/crates/pindakaas-kissat/build.rs b/crates/pindakaas-kissat/build.rs index 7823146607..2b4bdaabce 100644 --- a/crates/pindakaas-kissat/build.rs +++ b/crates/pindakaas-kissat/build.rs @@ -14,11 +14,13 @@ fn main() { "vendor/kissat/src/build.c", "vendor/kissat/src/bump.c", "vendor/kissat/src/check.c", + "vendor/kissat/src/classify.c", "vendor/kissat/src/clause.c", "vendor/kissat/src/collect.c", "vendor/kissat/src/colors.c", "vendor/kissat/src/compact.c", "vendor/kissat/src/config.c", + "vendor/kissat/src/congruence.c", "vendor/kissat/src/decide.c", "vendor/kissat/src/deduce.c", "vendor/kissat/src/definition.c", @@ -27,6 +29,8 @@ fn main() { "vendor/kissat/src/eliminate.c", "vendor/kissat/src/equivalences.c", "vendor/kissat/src/error.c", + "vendor/kissat/src/factor.c", + "vendor/kissat/src/fastel.c", "vendor/kissat/src/extend.c", "vendor/kissat/src/file.c", "vendor/kissat/src/flags.c", @@ -39,14 +43,17 @@ fn main() { "vendor/kissat/src/import.c", "vendor/kissat/src/internal.c", "vendor/kissat/src/kimits.c", + "vendor/kissat/src/krite.c", "vendor/kissat/src/kitten.c", "vendor/kissat/src/learn.c", "vendor/kissat/src/logging.c", + "vendor/kissat/src/lucky.c", "vendor/kissat/src/minimize.c", "vendor/kissat/src/mode.c", "vendor/kissat/src/options.c", "vendor/kissat/src/parse.c", "vendor/kissat/src/phases.c", + "vendor/kissat/src/preprocess.c", "vendor/kissat/src/print.c", "vendor/kissat/src/probe.c", "vendor/kissat/src/profile.c", @@ -54,10 +61,12 @@ fn main() { "vendor/kissat/src/proof.c", "vendor/kissat/src/propbeyond.c", "vendor/kissat/src/propdense.c", + "vendor/kissat/src/propinitially.c", "vendor/kissat/src/proprobe.c", "vendor/kissat/src/propsearch.c", "vendor/kissat/src/queue.c", "vendor/kissat/src/reduce.c", + "vendor/kissat/src/reorder.c", "vendor/kissat/src/reluctant.c", "vendor/kissat/src/rephase.c", "vendor/kissat/src/report.c", @@ -75,6 +84,7 @@ fn main() { "vendor/kissat/src/substitute.c", "vendor/kissat/src/sweep.c", "vendor/kissat/src/terminate.c", + "vendor/kissat/src/tiers.c", "vendor/kissat/src/trail.c", "vendor/kissat/src/transitive.c", "vendor/kissat/src/utilities.c", diff --git a/crates/pindakaas-kissat/vendor/kissat b/crates/pindakaas-kissat/vendor/kissat index 71caafb4d1..36acc9e6e4 160000 --- a/crates/pindakaas-kissat/vendor/kissat +++ b/crates/pindakaas-kissat/vendor/kissat @@ -1 +1 @@ -Subproject commit 71caafb4d182ced9f76cef45b00f37cc598f2a37 +Subproject commit 36acc9e6e410090f4ea0e41a129da5f896b3771a From dbded2ba5ae6101d305a1bcb6b21f0e19cdd81f3 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 29 Jul 2024 09:37:08 +1000 Subject: [PATCH 2/2] Silence clippy: unused `Incomplete` error type --- crates/pindakaas/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index 46e8505b77..0ff6a8aa9b 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -220,6 +220,7 @@ pub trait Checker { /// Incomplete is a error type returned by a [`Checker`] type when the #[derive(Clone, Debug, PartialEq, Eq, PartialOrd)] +#[allow(dead_code)] // TODO pub struct Incomplete { missing: Box<[Lit]>, }