Cadical: Add ability to clone solver

pindakaashq · Jan 24, 2024 · ad5bcd9 · ad5bcd9
1 parent 60c79e9
commit ad5bcd9
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 2 deletions.
diff --git a/crates/pindakaas-cadical/src/ccadical_override.cpp b/crates/pindakaas-cadical/src/ccadical_override.cpp
@@ -172,4 +172,10 @@ void ccadical_phase(CCaDiCaL *slv, int lit) {
 void ccadical_unphase(CCaDiCaL *slv, int lit) {
   ((Wrapper *)slv)->solver->unphase(lit);
 }
+
+CCaDiCaL *ccadical_copy(CCaDiCaL *slv) {
+  auto *cp = new Wrapper();
+  ((Wrapper *)slv)->solver->copy(*cp->solver);
+  return (CCaDiCaL *)cp;
+}
 }
diff --git a/crates/pindakaas-cadical/src/ccadical_up.h b/crates/pindakaas-cadical/src/ccadical_up.h
@@ -57,6 +57,7 @@ void ccadical_prop_set_add_external_clause_lit(
 
 void ccadical_phase(CCaDiCaL *, int lit);
 void ccadical_unphase(CCaDiCaL *, int lit);
+CCaDiCaL *ccadical_copy(CCaDiCaL *slv);
 
 /*------------------------------------------------------------------------*/
 

diff --git a/crates/pindakaas-cadical/src/lib.rs b/crates/pindakaas-cadical/src/lib.rs
@@ -24,4 +24,5 @@ extern "C" {
 	pub fn ccadical_simplify(slv: *mut c_void) -> c_int;
 	pub fn ccadical_terminate(slv: *mut c_void);
 	pub fn ccadical_unphase(slv: *mut c_void, lit: i32);
+	pub fn ccadical_copy(slv: *const c_void) -> *mut c_void;
 }
diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs
@@ -1,3 +1,4 @@
+use pindakaas_cadical::{ccadical_copy, ccadical_phase, ccadical_unphase};
 use pindakaas_derive::IpasirSolver;
 
 use super::VarFactory;
@@ -23,13 +24,25 @@ impl Default for Cadical {
 	}
 }
 
+impl Clone for Cadical {
+	fn clone(&self) -> Self {
+		let ptr = unsafe { ccadical_copy(self.ptr) };
+		Self {
+			ptr,
+			vars: self.vars,
+			#[cfg(feature = "ipasir-up")]
+			prop: None,
+		}
+	}
+}
+
 impl Cadical {
 	pub fn phase(&mut self, lit: Lit) {
-		unsafe { pindakaas_cadical::ccadical_phase(self.ptr, lit.0.get()) }
+		unsafe { ccadical_phase(self.ptr, lit.0.get()) }
 	}
 
 	pub fn unphase(&mut self, lit: Lit) {
-		unsafe { pindakaas_cadical::ccadical_unphase(self.ptr, lit.0.get()) }
+		unsafe { ccadical_unphase(self.ptr, lit.0.get()) }
 	}
 }
 
@@ -68,6 +81,14 @@ mod tests {
 			)
 		});
 		assert_eq!(res, SolveResult::Sat);
+		// Test clone implementation
+		let mut cp = slv.clone();
+		cp.solve(|value| {
+			assert!(
+				(value(!a).unwrap() && value(b).unwrap())
+					|| (value(a).unwrap() && value(!b).unwrap()),
+			)
+		});
 	}
 
 	#[cfg(feature = "ipasir-up")]