analyze db

src/main.rs

@@ -1,67 +1,66 @@
 // Copyright Pierre Carbonnelle, 2025.
 
-pub mod api;
-pub mod error;
-pub mod grammar;
-pub mod solver;
-mod private;
+// cargo run --release
 
-use std::fs;
-use std::path::PathBuf;
+use std::time::Instant;
 
-use clap::Parser;
+use rusqlite::params;
 
-use crate::solver::Solver;
+use xmtlib::solver::Solver;
 
-/// A high-level language for interacting with SMT solvers
-#[derive(Parser)]
-#[command(author, version, about, long_about = None)]
-struct Cli {
-    /// Path to the problem file in XMT-Lib format.
-    file_path: PathBuf,
+fn execute(solver: &mut Solver, commands: &str) -> () {
+    let results = solver.parse_and_execute(&commands);
+    for _result in results {
+        //println!("{}", _result);
+    }
 }
 
-fn main() {
-    let args = Cli::parse();
+fn main() -> Result<(), Box<dyn std::error::Error>> {
+    let n = 10000+1;
 
-    if args.file_path.exists() {
-        let source = fs::read_to_string(args.file_path).unwrap();
-        let mut solver = Solver::default();
-        let results = solver.parse_and_execute(&source);
-        for result in results {
-            println!("{}", result);
-        }
-    } else {
-        eprintln!("Error: File '{:?}' does not exist.", args.file_path);
-        std::process::exit(1);
-    }
-}
+    let start = Instant::now();
+    let mut solver = Solver::default();
 
+    let nodes = (1..n).map( |i| format!("(|{}|)", i) ).collect::<Vec<String>>().join("");
 
-#[cfg(test)]
-mod tests {
-    use std::fs::File;
+    execute(&mut solver, format!(r#"
+    (set-option :backend z3)
+    (declare-datatype Node ({nodes}))
+    (declare-fun Edge (Node Node) Bool)
+    (declare-fun phi (Node Node Node) Bool)
+    (x-interpret-pred Edge)"#).as_str());
 
-    use simplelog::*;
-    use crate::solver::Solver;
+    let declaration = Instant::now();
+    println!("Declarations: {:?}", declaration.duration_since(start));
 
-    fn tester(source: &str, output: &str) {
-        let mut solver = Solver::default();
-        let results = solver.parse_and_execute(source);
-        assert_eq!(results.into_iter().collect::<Vec<_>>().join("\n"), output);
+    {
+        let mut stmt = solver.conn.prepare("INSERT INTO Edge_T (a_0, a_1) VALUES (?, ?)")?;
+        for i in 1..n {
+            for j in 1..4 {
+                if i+j < n {
+                    stmt.execute(params![format!("|{i}|"), format!("|{}|", i+j)])?;
+                }
+            }
+        }
     }
+    let data_entry = Instant::now();
+    println!("Data entry: {:?}", data_entry.duration_since(declaration));
 
-    #[test]
-    fn sandbox() {
-        let config = ConfigBuilder::new()
-            .set_time_level(LevelFilter::Off)
-            .build();
-        let _ = WriteLogger::init(LevelFilter::Trace, config, File::create("xmtlib.log").unwrap());
+    let source = r#"
+(assert (forall ((x Node) (y Node) (z Node))
+            (=> (and (Edge x y) (Edge y z) (Edge x z))
+                     (phi x y z)
+            )))
+(x-ground)
+    "#;
+    execute(&mut solver, source);
+    let grounding = Instant::now();
+    println!("Grounding: {:?}", grounding.duration_since(data_entry));
 
-        tester( "(assert false)
-            (check-sat)",
+    execute(&mut solver, "(check-sat)");
+    let solving = Instant::now();
+    println!("Solving: {:?}", solving.duration_since(grounding));
+    println!("Total: {:?}", solving.duration_since(start));
 
-        "\n\n\n\n\nunsat\n"
-        );
-    }
+    Ok(())
 }

src/private/a_sort.rs

@@ -62,7 +62,7 @@ pub(crate) fn declare_datatypes(
     solver: &mut Solver
 ) -> Result<String, SolverError> {
 
-    let out = solver.exec(&command)?;  // this also validates the declaration
+    let out = solver.backend.exec(&command)?;  // this also validates the declaration
 
     // collect the declared symbols, for recursivity detection
     let declaring = sort_decs.iter().map(|sd| {
@@ -90,7 +90,7 @@ pub(crate) fn declare_sort(
     solver: &mut Solver
 ) -> Result<String, SolverError> {
 
-    let out = solver.exec(&command)?;
+    let out = solver.backend.exec(&command)?;
 
     if numeral.0 == 0 {
         let sort = Sort::Sort(Identifier::Simple(symb));
@@ -111,7 +111,7 @@ pub(crate) fn define_sort(
     solver: &mut Solver
 ) -> Result<String, SolverError> {
 
-    let out = solver.exec(&command)?;
+    let out = solver.backend.exec(&command)?;
 
     if variables.len() == 0 {  // non-parametric
         let declaring = IndexSet::new();

src/private/b_fun.rs

@@ -50,7 +50,7 @@ pub(crate) fn declare_fun(
     solver: &mut Solver
 ) -> Result<String, SolverError> {
 
-    let out = solver.exec(&command)?;  // this also validates the declaration
+    let out = solver.backend.exec(&command)?;  // this also validates the declaration
 
     // instantiate the sorts, if needed
     let declaring = IndexSet::new();

src/private/d_ground.rs

@@ -43,16 +43,19 @@ pub(crate) fn ground(
 ) -> Gen<Result<String, SolverError>, (), impl Future<Output = ()> + '_> {
 
     gen!({
+        // update statistics in DB
+        solver.conn.execute("ANALYZE", []).unwrap();
+
         // extract terms and commands
         let (commands, terms) = solver.assertions_to_ground.iter()
             .map(|(command, term)| (command.clone(), term.clone()))
             .collect::<(Vec<_>, Vec<_>)>();
 
         for (term, command) in terms.iter().zip(commands) {
             // push and pop, to avoid polluting the SMT state
-            yield_!(solver.exec("(push)"));
-            yield_!(solver.exec(&command));
-            yield_!(solver.exec("(pop)"));
+            yield_!(solver.backend.exec("(push)"));
+            yield_!(solver.backend.exec(&command));
+            yield_!(solver.backend.exec("(pop)"));
 
             match ground_term(&term, true, solver) {
                 Ok(g) => {
@@ -64,10 +67,11 @@ pub(crate) fn ground(
                             match execute_query(query, &mut solver.conn) {
                                 Ok(asserts) => {
                                     for assert in asserts {
-                                        yield_!(solver.exec(&assert));
+                                        yield_!(solver.backend.exec(&assert));
                                     }
                                 },
-                                Err(e) => yield_!(Err(e))
+                                Err(e) =>
+                                    yield_!(Err(e))
                             }
                         }
                     }

src/solver.rs

@@ -28,7 +28,7 @@ pub(crate) type TermId = usize;
 
 pub struct Solver {
     pub(crate) backend: Backend,
-    pub(crate) conn: Connection,
+    pub conn: Connection,
 
     // contains only parametric data type declarations
     pub(crate) parametric_sorts: IndexMap<Symbol, ParametricObject>,
@@ -208,7 +208,7 @@ impl Solver {
                     for res in ground(self) {
                         yield_!(res)
                     }
-                    match self.exec(&command) {
+                    match self.backend.exec(&command) {
                         Ok(res) => yield_!(Ok(res)),
                         Err(err) => {
                             yield_!(Err(err));
@@ -338,7 +338,7 @@ impl Solver {
                 }
 
                 Command::Verbatim(_) => {
-                    match self.exec(&command) {
+                    match self.backend.exec(&command) {
                         Ok(res) => yield_!(Ok(res)),
                         Err(err) => {
                             yield_!(Err(err));
@@ -349,29 +349,10 @@ impl Solver {
         })
     }
 
-    // execute a command string
-    pub(crate) fn exec(&mut self, cmd: &str) -> Result<String, SolverError> {
-        match self.backend {
-            Backend::NoDriver => {
-                return Ok(cmd.to_string())
-            },
-            Backend::Z3(ctx) => {
-                unsafe {
-                    let c_cmd = std::ffi::CString::new(cmd).unwrap();
-                    let response = Z3_eval_smtlib2_string(ctx, c_cmd.as_ptr());
-                    let c_str: &std::ffi::CStr = std::ffi::CStr::from_ptr(response);
-                    let str_slice: &str = c_str.to_str().unwrap();
-                    let result: String = str_slice.to_owned();
-                    return Ok(result)
-                }
-            }
-        }
-    }
-
     pub(crate) fn set_option(&mut self, option: Option_, cmd: String) -> Result<String, SolverError> {
         match option {
             Option_::Attribute(Attribute::Keyword(_)) => {
-                self.exec(&cmd)
+                self.backend.exec(&cmd)
             },
             Option_::Attribute(Attribute::WithValue(keyword, value)) => {
                 match (keyword.0.as_str(), value) {
@@ -389,11 +370,35 @@ impl Solver {
                         }
                         Ok("".to_string())
                     },
-                    _ => self.exec(&cmd)
+                    _ => self.backend.exec(&cmd)
                 }
 
             },
         }
     }
 
 }
+
+
+impl Backend {
+
+    /// execute a command string
+    pub(crate) fn exec(&mut self, cmd: &str) -> Result<String, SolverError> {
+        match self {
+            Backend::NoDriver => {
+                return Ok(cmd.to_string())
+            },
+            Backend::Z3(ctx) => {
+                unsafe {
+                    let c_cmd = std::ffi::CString::new(cmd).unwrap();
+                    let response = Z3_eval_smtlib2_string(*ctx, c_cmd.as_ptr());
+                    let c_str: &std::ffi::CStr = std::ffi::CStr::from_ptr(response);
+                    let str_slice: &str = c_str.to_str().unwrap();
+                    let result: String = str_slice.to_owned();
+                    return Ok(result)
+                }
+            }
+        }
+    }
+
+}

tests/triangle.smt2

@@ -1,3 +1,4 @@
+(set-option :backend none)
 (declare-datatype Node ( ( |1| ) ( |2| ) ( |3| )))
 (declare-fun Edge (Node Node) Bool)
 (declare-fun phi (Node Node Node) Bool)
@@ -16,14 +17,15 @@
 (check-sat)
 -------------------------
 
-
-
+(declare-datatype Node ((|1| ) (|2| ) (|3| )))
+(declare-fun Edge (Node Node) Bool)
+(declare-fun phi (Node Node Node) Bool)
 (x-interpret-pred Edge (|1| |2|) (|2| |3|) (|1| |3|))
 
-
-
-
-
+(push)
+(assert (forall ((x Node) (y Node) (z Node)) (=> (and (Edge x y) (Edge y z) (Edge x z)) (phi x y z))))
+(pop)
+(assert (phi |1| |2| |3|))
 Groundings:
  - x: SELECT Node.G AS x, Node.G AS G FROM Node
  - y: SELECT Node_1.G AS y, Node_1.G AS G FROM Node AS Node_1
@@ -64,4 +66,4 @@ Groundings:
     TU: SELECT Agg_0_TU.G AS G FROM Agg_0_TU
     UF: SELECT Agg_0_UF.G AS G FROM Agg_0_UF
     G : SELECT Agg_0_G.G AS G FROM Agg_0_G
-sat
+(check-sat)