Out of memory errors

.github/workflows/capi.yml

@@ -37,6 +37,8 @@ jobs:
     name: Ensure C-API crate version is in sync
     runs-on: ubuntu-latest
     steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
       - name: Check
         run: "[ \"$(grep '^version = ' rustsat/Cargo.toml)\" = \"$(grep '^version = ' capi/Cargo.toml)\" ]"
 

.github/workflows/pyapi.yml

@@ -54,6 +54,8 @@ jobs:
     name: Ensure Python API crate version is in sync
     runs-on: ubuntu-latest
     steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
       - name: Check
         run: "[ \"$(grep '^version = ' rustsat/Cargo.toml)\" = \"$(grep '^version = ' pyapi/Cargo.toml)\" ]"
 

cadical/Cargo.toml

@@ -53,3 +53,5 @@ chrono = "0.4.31"
 
 [dev-dependencies]
 rustsat-solvertests = { path = "../solvertests" }
+clap = { version = "4.5.4", features = ["derive"] }
+signal-hook = { version = "0.3.17" }

cadical/examples/cadical-cli.rs

@@ -0,0 +1,129 @@
+//! # CaDiCaL CLI Tool
+//!
+//! A simple CLI wrapper around the CaDiCaL solver Rust interface. This is just an example, if you
+//! want to use CaDiCaL from the CLI, compile the binary from the C++ source directly.
+
+use std::{
+    io,
+    path::{Path, PathBuf},
+    thread,
+};
+
+use anyhow::Context;
+use clap::Parser;
+use rustsat::{
+    instances::{fio::opb, ManageVars, SatInstance},
+    solvers::{Interrupt, InterruptSolver, Solve, SolveStats, SolverResult},
+};
+use rustsat_cadical::CaDiCaL;
+
+enum FileType {
+    Cnf,
+    Opb,
+}
+
+#[derive(Parser)]
+#[command(author, version, about, long_about = None)]
+struct Args {
+    /// The DIMACS CNF input file. Reads from `stdin` if not given.
+    in_path: Option<PathBuf>,
+    /// Parse the input as an OPB file by default
+    #[arg(short, long)]
+    opb: bool,
+}
+
+fn main() -> anyhow::Result<()> {
+    let args = Args::parse();
+
+    let inst: SatInstance = if let Some(in_path) = args.in_path {
+        match determine_file_type(&in_path, args.opb) {
+            FileType::Cnf => SatInstance::from_dimacs_path(in_path)
+                .context("error parsing the input file as CNF")?,
+            FileType::Opb => SatInstance::from_opb_path(in_path, opb::Options::default())
+                .context("error parsing the input file as OPB")?,
+        }
+    } else if args.opb {
+        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb::Options::default())
+            .context("error parsing input as OPB")?
+    } else {
+        SatInstance::from_dimacs(io::BufReader::new(io::stdin()))
+            .context("error parsing input as CNF")?
+    };
+
+    solve::<CaDiCaL>(inst)
+}
+
+fn solve<S: Solve + SolveStats + Interrupt + Default>(inst: SatInstance) -> anyhow::Result<()> {
+    let mut solver = S::default();
+
+    #[cfg(not(target_family = "windows"))]
+    {
+        // Setup signal handling
+        let interrupter = solver.interrupter();
+        let mut signals = signal_hook::iterator::Signals::new([
+            signal_hook::consts::SIGTERM,
+            signal_hook::consts::SIGINT,
+            signal_hook::consts::SIGXCPU,
+            signal_hook::consts::SIGABRT,
+        ])?;
+        // Thread for catching incoming signals
+        thread::spawn(move || {
+            for _ in signals.forever() {
+                interrupter.interrupt();
+            }
+        });
+    }
+
+    let (cnf, vm) = inst.into_cnf();
+    if let Some(max_var) = vm.max_var() {
+        solver.reserve(max_var)?;
+    }
+    solver.add_cnf(cnf)?;
+    match solver.solve() {
+        Err(err) => {
+            println!("s UNKNOWN");
+            return Err(err);
+        }
+        Ok(res) => match res {
+            SolverResult::Sat => {
+                println!("s SATISFIABLE");
+                println!("v {}", solver.full_solution()?);
+            }
+            SolverResult::Unsat => println!("s UNSATISFIABLE"),
+            SolverResult::Interrupted => println!("s UNKNOWN"),
+        },
+    };
+    Ok(())
+}
+
+macro_rules! is_one_of {
+    ($a:expr, $($b:expr),*) => {
+        $( $a == $b || )* false
+    }
+}
+
+fn determine_file_type(in_path: &Path, opb_default: bool) -> FileType {
+    if let Some(ext) = in_path.extension() {
+        let path_without_compr = in_path.with_extension("");
+        let ext = if is_one_of!(ext, "gz", "bz2") {
+            // Strip compression extension
+            match path_without_compr.extension() {
+                Some(ext) => ext,
+                None => return FileType::Cnf, // Fallback default
+            }
+        } else {
+            ext
+        };
+        if "opb" == ext {
+            return FileType::Opb;
+        };
+        if "cnf" == ext {
+            return FileType::Cnf;
+        }
+    };
+    if opb_default {
+        FileType::Opb
+    } else {
+        FileType::Cnf
+    } // Fallback default
+}

cadical/patches/v150.patch

@@ -1,14 +1,14 @@
-From d153963a145ae94c0f3ce695ec1dc89fe73a9815 Mon Sep 17 00:00:00 2001
+From cc5a76a68bd5f05b0b45c9d335605521228e7d5d Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <[email protected]>
-Date: Wed, 23 Aug 2023 11:30:43 +0300
+Date: Thu, 18 Apr 2024 15:04:18 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 ++++++
- src/ccadical.cpp | 54 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 17 +++++++++++++++
- src/solver.cpp   | 24 +++++++++++++++++++++
- 4 files changed, 101 insertions(+)
+ src/cadical.hpp  |  6 ++++
+ src/ccadical.cpp | 94 ++++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   | 24 +++++++++++++
+ src/solver.cpp   | 24 +++++++++++++
+ 4 files changed, 148 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index cbe476d..e5e8a9f 100644
@@ -28,17 +28,52 @@ index cbe476d..e5e8a9f 100644
 
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index e6e7d28..7fabb24 100644
+index e6e7d28..853d11c 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -177,4 +177,58 @@ int ccadical_frozen (CCaDiCaL * ptr, int lit) {
+@@ -177,4 +177,98 @@ int ccadical_frozen (CCaDiCaL * ptr, int lit) {
    return ((Wrapper*) ptr)->solver->frozen (lit);
  }
 
 +/*------------------------------------------------------------------------*/
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -72,8 +107,13 @@ index e6e7d28..7fabb24 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -91,15 +131,22 @@ index e6e7d28..7fabb24 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 332f842..1a141f4 100644
+index 332f842..db41678 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,23 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,30 @@ int ccadical_simplify (CCaDiCaL *);
 
  /*------------------------------------------------------------------------*/
 
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -108,7 +155,7 @@ index 332f842..1a141f4 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -154,5 +201,5 @@ index 31b1610..a079861 100644
 
  void Solver::freeze (int lit) {
 -- 
-2.41.0
+2.44.0