From 9736850000f8d996e71bee31fc128fbffb716859 Mon Sep 17 00:00:00 2001 From: Pierre Carbonnelle Date: Fri, 14 Feb 2025 09:28:58 +0100 Subject: [PATCH 1/2] triangle.rs --- src/main.rs | 96 ++++++++++++++++++++--------------------- src/private/a_sort.rs | 6 +-- src/private/b_fun.rs | 2 +- src/private/d_ground.rs | 11 ++--- src/solver.rs | 53 ++++++++++++----------- tests/triangle.smt2 | 16 ++++--- 6 files changed, 95 insertions(+), 89 deletions(-) diff --git a/src/main.rs b/src/main.rs index 0b42c7a..8ce6784 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,67 +1,65 @@ // 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> { + 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::>().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::>().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)); - "\n\n\n\n\nunsat\n" - ); - } + Ok(()) } \ No newline at end of file diff --git a/src/private/a_sort.rs b/src/private/a_sort.rs index 20e2d0c..bdc7618 100644 --- a/src/private/a_sort.rs +++ b/src/private/a_sort.rs @@ -62,7 +62,7 @@ pub(crate) fn declare_datatypes( solver: &mut Solver ) -> Result { - 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 { - 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 { - let out = solver.exec(&command)?; + let out = solver.backend.exec(&command)?; if variables.len() == 0 { // non-parametric let declaring = IndexSet::new(); diff --git a/src/private/b_fun.rs b/src/private/b_fun.rs index 49f6e36..cc561c1 100644 --- a/src/private/b_fun.rs +++ b/src/private/b_fun.rs @@ -50,7 +50,7 @@ pub(crate) fn declare_fun( solver: &mut Solver ) -> Result { - 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(); diff --git a/src/private/d_ground.rs b/src/private/d_ground.rs index 1d69518..c3c6536 100644 --- a/src/private/d_ground.rs +++ b/src/private/d_ground.rs @@ -50,9 +50,9 @@ pub(crate) fn ground( 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 +64,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)) } } } diff --git a/src/solver.rs b/src/solver.rs index d0780c7..c096ecd 100644 --- a/src/solver.rs +++ b/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, @@ -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 { - 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 { 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,7 +370,7 @@ impl Solver { } Ok("".to_string()) }, - _ => self.exec(&cmd) + _ => self.backend.exec(&cmd) } }, @@ -397,3 +378,27 @@ impl Solver { } } + + +impl Backend { + + /// execute a command string + pub(crate) fn exec(&mut self, cmd: &str) -> Result { + 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) + } + } + } + } + +} diff --git a/tests/triangle.smt2 b/tests/triangle.smt2 index b19b2bd..3c2bcf3 100644 --- a/tests/triangle.smt2 +++ b/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) \ No newline at end of file From 85c55b12ea3be34296ad5be75cacbcb39175a65d Mon Sep 17 00:00:00 2001 From: Pierre Carbonnelle Date: Fri, 14 Feb 2025 16:54:41 +0100 Subject: [PATCH 2/2] analyze db --- src/main.rs | 1 + src/private/d_ground.rs | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/main.rs b/src/main.rs index 8ce6784..071b66b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -60,6 +60,7 @@ fn main() -> Result<(), Box> { execute(&mut solver, "(check-sat)"); let solving = Instant::now(); println!("Solving: {:?}", solving.duration_since(grounding)); + println!("Total: {:?}", solving.duration_since(start)); Ok(()) } \ No newline at end of file diff --git a/src/private/d_ground.rs b/src/private/d_ground.rs index c3c6536..34bfc03 100644 --- a/src/private/d_ground.rs +++ b/src/private/d_ground.rs @@ -43,6 +43,9 @@ pub(crate) fn ground( ) -> Gen, (), impl Future + '_> { 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()))