more APIs in cadical

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 ====================================================
 

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*************************************************************
 

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

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

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

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 *);
 
 /*------------------------------------------------------------------------*/