Add declare_fresh

xlsynth-g8r/src/equiv/bitwuzla_backend.rs

@@ -80,6 +80,7 @@ impl Drop for RawBitwuzla {
 /// A Bitwuzla-rawd SMT solver implementing the `Solver` trait.
 pub struct Bitwuzla {
     bitwuzla: Arc<RawBitwuzla>,
+    fresh_counter: u64,
 }
 
 impl Bitwuzla {
@@ -672,9 +673,16 @@ impl Solver for Bitwuzla {
         let instance = RawBitwuzla::new(config.options.raw);
         Ok(Bitwuzla {
             bitwuzla: Arc::new(instance),
+            fresh_counter: 0,
         })
     }
 
+    fn fresh_symbol(&mut self, name: &str) -> io::Result<String> {
+        let symbol = format!("__bitwuzla_fresh_{}_{}", name, self.fresh_counter);
+        self.fresh_counter += 1;
+        Ok(symbol)
+    }
+
     fn declare(&mut self, name: &str, width: usize) -> io::Result<BitVec<Self::Term>> {
         if width == 0 {
             return Ok(BitVec::ZeroWidth);

xlsynth-g8r/src/equiv/boolector_backend.rs

@@ -57,6 +57,7 @@ impl Drop for RawBtor {
 #[derive(Clone)]
 pub struct Boolector {
     btor: Arc<RawBtor>,
+    fresh_counter: u64,
 }
 
 impl Boolector {
@@ -207,6 +208,7 @@ impl Solver for Boolector {
         }
         Ok(Boolector {
             btor: Arc::new(btor),
+            fresh_counter: 0,
         })
     }
 
@@ -223,6 +225,12 @@ impl Solver for Boolector {
         })
     }
 
+    fn fresh_symbol(&mut self, name: &str) -> io::Result<String> {
+        let symbol = format!("__boolector_fresh_{}_{}", name, self.fresh_counter);
+        self.fresh_counter += 1;
+        Ok(symbol)
+    }
+
     fn numerical(&mut self, width: usize, mut value: u64) -> BitVec<Self::Term> {
         assert!(width > 0, "Width must be positive");
         if width < 64 {

xlsynth-g8r/src/equiv/easy_smt_backend.rs

@@ -113,6 +113,7 @@ pub struct EasySmtSolver {
     next_name_index: usize,
     term_cache: HashMap<String, SExpr>,
     reverse_cache: HashMap<SExpr, String>,
+    fresh_counter: u64,
 }
 
 impl EasySmtSolver {
@@ -286,9 +287,16 @@ impl Solver for EasySmtSolver {
             next_name_index: 0,
             term_cache: HashMap::new(),
             reverse_cache: HashMap::new(),
+            fresh_counter: 0,
         })
     }
 
+    fn fresh_symbol(&mut self, name: &str) -> io::Result<String> {
+        let symbol = format!("__easy_smt_fresh_{}_{}", name, self.fresh_counter);
+        self.fresh_counter += 1;
+        Ok(symbol)
+    }
+
     fn declare(&mut self, name: &str, width: usize) -> io::Result<BitVec<SExpr>> {
         if width == 0 {
             return Ok(BitVec::ZeroWidth);

xlsynth-g8r/src/equiv/solver_interface.rs

@@ -39,6 +39,11 @@ pub trait Solver: Sized {
     type Config: Send + Sync;
     fn new(config: &Self::Config) -> io::Result<Self>;
     fn declare(&mut self, name: &str, width: usize) -> io::Result<BitVec<Self::Term>>;
+    fn fresh_symbol(&mut self, name: &str) -> io::Result<String>;
+    fn declare_fresh(&mut self, name: &str, width: usize) -> io::Result<BitVec<Self::Term>> {
+        let symbol = self.fresh_symbol(name)?;
+        self.declare(&symbol, width)
+    }
     fn numerical(&mut self, width: usize, value: u64) -> BitVec<Self::Term>;
     fn zero(&mut self, width: usize) -> BitVec<Self::Term> {
         self.numerical(width, 0)
@@ -1098,6 +1103,37 @@ macro_rules! test_solver {
                 test_utils::test_slice(&mut solver);
             }
 
+            // New tests for declare_fresh symbol generation behavior
+            #[test]
+            fn test_declare_fresh_generates_unique_symbols() {
+                let mut solver = $solver;
+                let f1 = solver.declare_fresh("a", 8).unwrap();
+                let f2 = solver.declare_fresh("a", 8).unwrap();
+                solver.push().unwrap();
+                let ne = solver.ne(&f1, &f2);
+                solver.assert(&ne).unwrap();
+                assert_eq!(
+                    solver.check().unwrap(),
+                    crate::equiv::solver_interface::Response::Sat
+                );
+                solver.pop().unwrap();
+            }
+
+            #[test]
+            fn test_declare_fresh_differs_from_declare() {
+                let mut solver = $solver;
+                let d = solver.declare("a", 8).unwrap();
+                let f = solver.declare_fresh("a", 8).unwrap();
+                solver.push().unwrap();
+                let ne = solver.ne(&d, &f);
+                solver.assert(&ne).unwrap();
+                assert_eq!(
+                    solver.check().unwrap(),
+                    crate::equiv::solver_interface::Response::Sat
+                );
+                solver.pop().unwrap();
+            }
+
             crate::test_solver_unary!(test_not, $solver, not, 8, 0x89, 8, 0x76);
             crate::test_solver_unary!(test_neg, $solver, neg, 8, 0x05, 8, 0xFB);