From 5e03f9fefa6caa3348b8a2fbd306e37222580d41 Mon Sep 17 00:00:00 2001
From: MyskYko <yoyuohlhjl@yahoo.co.jp>
Date: Fri, 20 Jun 2025 15:55:31 -0700
Subject: [PATCH] more APIs in cadical

---
 src/sat/cadical/cadical.hpp          |  4 ++++
 src/sat/cadical/cadicalSolver.c      | 30 ++++++++++++++++++++++++++++
 src/sat/cadical/cadicalSolver.h      |  2 ++
 src/sat/cadical/cadical_ccadical.cpp |  8 ++++++++
 src/sat/cadical/cadical_solver.cpp   | 10 ++++++++++
 src/sat/cadical/ccadical.h           |  2 ++
 6 files changed, 56 insertions(+)

diff --git a/src/sat/cadical/cadical.hpp b/src/sat/cadical/cadical.hpp
index c9ed41332..64a5d9ef7 100644
--- a/src/sat/cadical/cadical.hpp
+++ b/src/sat/cadical/cadical.hpp
@@ -982,6 +982,10 @@ public:
   //
   static void build (FILE *file, const char *prefix = "c ");
 
+  // Extra APIs
+  int clauses ();
+  int conflicts ();
+
 private:
   //==== start of state ====================================================
 
diff --git a/src/sat/cadical/cadicalSolver.c b/src/sat/cadical/cadicalSolver.c
index bf6df9512..dee2beaf3 100644
--- a/src/sat/cadical/cadicalSolver.c
+++ b/src/sat/cadical/cadicalSolver.c
@@ -261,6 +261,36 @@ int cadical_solver_get_var_value(cadical_solver* s, int v) {
   return ccadical_val((CCaDiCaL*)s->p, v + 1) > 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [get number of clauses]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int cadical_solver_nclauses(cadical_solver* s) {
+  return ccadical_clauses((CCaDiCaL*)s->p);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [get number of conflicts]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int cadical_solver_nconflicts(cadical_solver* s) {
+  return ccadical_conflicts((CCaDiCaL*)s->p);
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/sat/cadical/cadicalSolver.h b/src/sat/cadical/cadicalSolver.h
index 0192ada3c..2aec06c2a 100644
--- a/src/sat/cadical/cadicalSolver.h
+++ b/src/sat/cadical/cadicalSolver.h
@@ -65,6 +65,8 @@ extern int              cadical_solver_nvars(cadical_solver* s);
 extern int              cadical_solver_addvar(cadical_solver* s);
 extern void             cadical_solver_setnvars(cadical_solver* s,int n);
 extern int              cadical_solver_get_var_value(cadical_solver* s, int v);
+extern int              cadical_solver_nclauses(cadical_solver* s);
+extern int              cadical_solver_nconflicts(cadical_solver* s);
 extern Vec_Int_t *      cadical_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose );
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/cadical/cadical_ccadical.cpp b/src/sat/cadical/cadical_ccadical.cpp
index ae5c1093f..ccc616c80 100644
--- a/src/sat/cadical/cadical_ccadical.cpp
+++ b/src/sat/cadical/cadical_ccadical.cpp
@@ -208,4 +208,12 @@ int ccadical_is_inconsistent(CCaDiCaL *ptr) {
   return ((Wrapper *) ptr)->solver->inconsistent ();
 }
 
+int ccadical_clauses(CCaDiCaL *ptr) {
+  return ((Wrapper *) ptr)->solver->clauses ();
+}
+
+int ccadical_conflicts(CCaDiCaL *ptr) {
+  return ((Wrapper *) ptr)->solver->conflicts ();
+}
+
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/cadical/cadical_solver.cpp b/src/sat/cadical/cadical_solver.cpp
index df051f4de..84d350cf2 100644
--- a/src/sat/cadical/cadical_solver.cpp
+++ b/src/sat/cadical/cadical_solver.cpp
@@ -1759,6 +1759,16 @@ void Solver::error (const char *fmt, ...) {
   va_end (ap);
 }
 
+/*------------------------------------------------------------------------*/
+
+int Solver::clauses () {
+  return internal->stats.added.total;
+}
+
+int Solver::conflicts () {
+    return internal->stats.conflicts;
+}
+
 } // namespace CaDiCaL
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/cadical/ccadical.h b/src/sat/cadical/ccadical.h
index ec5292a79..d4c2ce8f0 100644
--- a/src/sat/cadical/ccadical.h
+++ b/src/sat/cadical/ccadical.h
@@ -58,6 +58,8 @@ int ccadical_reserve_difference (CCaDiCaL *, int number_of_vars);
 
 void ccadical_reserve(CCaDiCaL *, int min_max_var);
 int ccadical_is_inconsistent(CCaDiCaL *);
+int ccadical_clauses(CCaDiCaL *);
+int ccadical_conflicts(CCaDiCaL *);
 
 /*------------------------------------------------------------------------*/