From e505efa8fdbb6ba3bebd9aa24dc2b969758dc98a Mon Sep 17 00:00:00 2001 From: arshiamoeini Date: Thu, 22 Feb 2024 14:55:51 +0330 Subject: [PATCH] generate z3-status with smt-lib2 language --- .vscode/settings.json | 6 +- Cargo.lock | 131 +-- front/package.json | 2 +- front/src/components/proof/Toolbar.tsx | 16 +- front/src/hakim/index.ts | 27 +- front/src/index.html | 4 +- front/yarn.lock | 8 +- hakim-engine/Cargo.toml | 15 +- hakim-engine/src/interactive.rs | 7 +- hakim-engine/src/interactive/tactic.rs | 2 - .../src/interactive/tactic/z3_auto.rs | 902 ++++++++---------- hakim-json/src/lib.rs | 11 +- 12 files changed, 431 insertions(+), 700 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index e95894f3..44b484dd 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,4 +1,8 @@ { "rust-analyzer.checkOnSave.command": "clippy", - "editor.formatOnSave": true + "editor.formatOnSave": true, + "rust-analyzer.linkedProjects": [ + "./hakim-engine/Cargo.toml" + ], + "rust-analyzer.checkOnSave": false } \ No newline at end of file diff --git a/Cargo.lock b/Cargo.lock index 84c8a9fa..45091240 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -339,26 +339,6 @@ version = "0.21.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "414dcefbc63d77c526a76b3afcf6fbb9b5e2791c19c3aa2297733208750c6e53" -[[package]] -name = "bindgen" -version = "0.66.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f2b84e06fc203107bfbad243f4aba2af864eb7db3b1cf46ea0a023b0b433d2a7" -dependencies = [ - "bitflags 2.4.0", - "cexpr", - "clang-sys", - "lazy_static", - "lazycell", - "peeking_take_while", - "proc-macro2", - "quote", - "regex", - "rustc-hash", - "shlex", - "syn 2.0.29", -] - [[package]] name = "bitflags" version = "1.3.2" @@ -441,15 +421,6 @@ dependencies = [ "libc", ] -[[package]] -name = "cexpr" -version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766" -dependencies = [ - "nom", -] - [[package]] name = "cfg-if" version = "0.1.10" @@ -462,17 +433,6 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" -[[package]] -name = "clang-sys" -version = "1.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c688fc74432808e3eb684cae8830a86be1d66a2bd58e1f248ed0960a590baf6f" -dependencies = [ - "glob", - "libc", - "libloading", -] - [[package]] name = "clap" version = "4.4.18" @@ -524,15 +484,6 @@ dependencies = [ "winapi", ] -[[package]] -name = "cmake" -version = "0.1.50" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a31c789563b815f77f4250caee12365734369f942439b7defd71e18a48197130" -dependencies = [ - "cc", -] - [[package]] name = "colorchoice" version = "1.0.0" @@ -832,12 +783,6 @@ version = "0.28.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6fb8d784f27acf97159b40fc4db5ecd8aa23b9ad5ef69cdd136d3bc80665f0c0" -[[package]] -name = "glob" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" - [[package]] name = "h2" version = "0.3.21" @@ -878,9 +823,8 @@ dependencies = [ "rayon", "regex", "serde", + "smt2", "typed-arena", - "z3", - "z3-sys", ] [[package]] @@ -1051,28 +995,12 @@ version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" -[[package]] -name = "lazycell" -version = "1.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55" - [[package]] name = "libc" version = "0.2.147" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b4668fb0ea861c1df094127ac5f1da3409a82116a4ba74fca2e58ef927159bb3" -[[package]] -name = "libloading" -version = "0.7.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b67380fd3b2fbe7527a606e18729d21c6f3951633d0500574c4dc22d2d638b9f" -dependencies = [ - "cfg-if 1.0.0", - "winapi", -] - [[package]] name = "linux-raw-sys" version = "0.4.5" @@ -1167,12 +1095,6 @@ dependencies = [ "sprs", ] -[[package]] -name = "minimal-lexical" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" - [[package]] name = "miniz_oxide" version = "0.7.1" @@ -1229,16 +1151,6 @@ dependencies = [ "memoffset 0.6.5", ] -[[package]] -name = "nom" -version = "7.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" -dependencies = [ - "memchr", - "minimal-lexical", -] - [[package]] name = "num-bigint" version = "0.4.4" @@ -1360,12 +1272,6 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8835116a5c179084a830efb3adc117ab007512b535bc1a21c991d3b32a6b44dd" -[[package]] -name = "peeking_take_while" -version = "0.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "19b17cddbe7ec3f8bc800887bab5e717348c95ea2ca0b1bf0837fb964dc67099" - [[package]] name = "percent-encoding" version = "2.3.0" @@ -1567,12 +1473,6 @@ version = "0.1.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" -[[package]] -name = "rustc-hash" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" - [[package]] name = "rustc_version" version = "0.4.0" @@ -1708,12 +1608,6 @@ dependencies = [ "digest", ] -[[package]] -name = "shlex" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "43b2853a4d09f215c24cc5489c992ce46052d359b5109343cbafbf26bc62f8a3" - [[package]] name = "signal-hook-registry" version = "1.4.1" @@ -1748,6 +1642,11 @@ version = "1.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "62bb4feee49fdd9f707ef802e22365a35de4b7b299de4763d44bfea899442ff9" +[[package]] +name = "smt2" +version = "0.1.0" +source = "git+https://github.com/achreto/rust-smtlib2#034f59ed198166a013c5aa45c86ecbcf03eda03b" + [[package]] name = "socket2" version = "0.5.3" @@ -2259,24 +2158,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04" -[[package]] -name = "z3" -version = "0.12.1" -source = "git+https://github.com/arshiamoeini/my_z3.git#fc489c4c3419add069b7e7177ec1328e54f00857" -dependencies = [ - "log", - "z3-sys", -] - -[[package]] -name = "z3-sys" -version = "0.8.1" -source = "git+https://github.com/arshiamoeini/my_z3.git#fc489c4c3419add069b7e7177ec1328e54f00857" -dependencies = [ - "bindgen", - "cmake", -] - [[package]] name = "zstd" version = "0.12.4" diff --git a/front/package.json b/front/package.json index 2feee39e..7a9ff131 100644 --- a/front/package.json +++ b/front/package.json @@ -81,7 +81,7 @@ "webpack-manifest-plugin": "4.0.2", "yaml-include-loader": "^1.0.0", "yaml-loader": "^0.6.0", - "z3-solver": "^4.12.4" + "z3-solver": "^4.12.5" }, "scripts": { "build": "webpack build --mode production", diff --git a/front/src/components/proof/Toolbar.tsx b/front/src/components/proof/Toolbar.tsx index c7e37f90..25bf748e 100644 --- a/front/src/components/proof/Toolbar.tsx +++ b/front/src/components/proof/Toolbar.tsx @@ -52,12 +52,8 @@ const AutoProofButton = () => { const r = await tryAuto(); if (mode === 'boost') { if (r.available) { - if (r.tactic[0] === "z3_solved") { - z3Solved(); - } else { - for (const tac of r.tactic) { - await sendTactic(tac); - } + for (const tac of r.tactic) { + await sendTactic(tac); } } } else { @@ -79,12 +75,8 @@ const AutoProofButton = () => { } if (s.available) { console.log(s.tactic[0]); - if (s.tactic[0] === "z3_solved") { - z3Solved(); - } else { - for (const tac of s.tactic) { - await sendTactic(tac); - } + for (const tac of s.tactic) { + await sendTactic(tac); } } else if (mode === 'boost') { setMode('normal'); diff --git a/front/src/hakim/index.ts b/front/src/hakim/index.ts index 1e97f712..1cddd491 100644 --- a/front/src/hakim/index.ts +++ b/front/src/hakim/index.ts @@ -2,6 +2,7 @@ import { normalPrompt } from "../dialog"; import { fromRust } from "../i18n"; import { loadLibText } from "./lib_text"; import { hakimQueryImpl } from "./wasm_provider"; +import { init } from "z3-solver"; declare let window: Window & { ask_question: (q: string) => Promise; @@ -47,6 +48,9 @@ await window.hakimQueryLoad; let queryLock = false; +const { Context, em } = await init(); +const Z3 = Context('main'); + const instance: Instance = new Proxy( {}, { @@ -66,16 +70,16 @@ const instance: Instance = new Proxy( }); } if (r && typeof r === "object" && r.Z3State) { - // const solver = new Z3.Solver(); - - // solver.fromString(r.Z3State); - // solver.set("timeout", 1500); - // let sat = await solver.check(); - // if (sat === 'unsat') { - // r = "z3_solved"; - // } else { - r = "z3_cant_solve"; - // } + const solver = new Z3.Solver(); + + solver.fromString(r.Z3State); + solver.set("timeout", 1500); + let sat = await solver.check(); + if (sat === 'unsat') { + r = "z3_solved"; + } else { + r = "z3_cant_solve"; + } } queryLock = false; return r; @@ -378,10 +382,11 @@ export const tryAuto = async (): Promise => { if (tactic) { if (tactic === 'z3_solved') { + console.log("z3 solved"); return { available: true, type: "normal", - tactic: ["z3_solved"], + tactic: ["z3"], }; } if (tactic !== 'z3_cant_solve') { diff --git a/front/src/index.html b/front/src/index.html index c8b260ba..eb07ee72 100644 --- a/front/src/index.html +++ b/front/src/index.html @@ -11,9 +11,9 @@ - + \ No newline at end of file diff --git a/front/yarn.lock b/front/yarn.lock index ab5c5d0f..4ff1f90e 100644 --- a/front/yarn.lock +++ b/front/yarn.lock @@ -10589,9 +10589,9 @@ yocto-queue@^0.1.0: resolved "https://registry.npmjs.org/yocto-queue/-/yocto-queue-0.1.0.tgz" integrity sha512-rVksvsnNCdJ/ohGc6xgPwyN8eheCxsiLM8mxuE/t/mOVqJewPuO1miLpTHQiRgTKCLexL4MeAFVagts7HmNZ2Q== -z3-solver@^4.12.4: - version "4.12.4" - resolved "https://registry.yarnpkg.com/z3-solver/-/z3-solver-4.12.4.tgz#3f7f7eca0d0e2afb5fda409e4ed3639507346c71" - integrity sha512-B9ymul40bvtGSW0OQYfcYan1EhGm0JV/HgbO24JikIhuEOUv2+mdcOVd4V3q89UOx2mA0MOv+6d5msVF+/yJ6g== +z3-solver@^4.12.5: + version "4.12.5" + resolved "https://registry.yarnpkg.com/z3-solver/-/z3-solver-4.12.5.tgz#ec8d4b17aa07b8792b9ab8b8f61dc8b0ea30d7b0" + integrity sha512-uh6zoe+ErxG2qLjWyOcZE41eb6CHUZ3IT7VYTh1SDswPaoe7I1mvC7ujA36TROdBdPm59UUFToDmRbfiyjdA1Q== dependencies: async-mutex "^0.3.2" diff --git a/hakim-engine/Cargo.toml b/hakim-engine/Cargo.toml index a8466793..6669ec24 100644 --- a/hakim-engine/Cargo.toml +++ b/hakim-engine/Cargo.toml @@ -14,15 +14,16 @@ typed-arena = "2.0.1" lazy_static = "1.2.0" minilp = { git = "https://github.com/HKalbasi/minilp" } pretty = "0.11.3" -z3 = { git = "https://github.com/arshiamoeini/my_z3.git", optional = true, features = [ - "static-link-z3", -] } -z3-sys = { git = "https://github.com/arshiamoeini/my_z3.git", optional = true, features = [ - "static-link-z3", -] } +smt2 = { git = "https://github.com/achreto/rust-smtlib2", features = ["z3"] } +#z3 = { git = "https://github.com/arshiamoeini/my_z3.git", features = [ +# "static-link-z3", +#] } +#z3-sys = { git = "https://github.com/arshiamoeini/my_z3.git", features = [ +# "static-link-z3", +#] } [features] -z3 = ["dep:z3", "dep:z3-sys"] +z3 = [] [dev-dependencies] rayon = "1.6.0" diff --git a/hakim-engine/src/interactive.rs b/hakim-engine/src/interactive.rs index 55ba2ddf..29ca9eb3 100644 --- a/hakim-engine/src/interactive.rs +++ b/hakim-engine/src/interactive.rs @@ -34,10 +34,9 @@ use self::suggest::{ pub use self::action_of_tactic::action_of_tactic; pub use self::suggest::{SuggClass, SuggRule, Suggestion}; -#[cfg(feature = "z3")] -use self::tactic::z3_auto; + use self::tactic::{ - add_from_lib, assumption, auto_list, auto_set, chain, remove_hyp, revert, unfold, + add_from_lib, assumption, auto_list, auto_set, chain, remove_hyp, revert, unfold, z3_auto, }; #[derive(Debug, Clone, Serialize, Deserialize)] @@ -284,7 +283,6 @@ impl Session { self.last_snapshot().last_frame()?.try_auto() } - #[cfg(feature = "z3")] pub fn z3_get_state(&self) -> Option { Some(z3_auto(self.last_snapshot().last_frame()?.clone())) } @@ -487,7 +485,6 @@ impl Frame { "auto_set" => auto_set(frame), "auto_list" => auto_list(frame), "assumption" => assumption(frame), - #[cfg(feature = "z3")] "z3" => Err(tactic::Error::Z3State(z3_auto(frame))), _ => Err(tactic::Error::UnknownTactic(name.to_string())), } diff --git a/hakim-engine/src/interactive/tactic.rs b/hakim-engine/src/interactive/tactic.rs index 3f5ec499..fde51393 100644 --- a/hakim-engine/src/interactive/tactic.rs +++ b/hakim-engine/src/interactive/tactic.rs @@ -34,9 +34,7 @@ pub(crate) use chain::{chain, destruct}; mod assumption; pub(crate) use assumption::assumption; -#[cfg(feature = "z3")] mod z3_auto; -#[cfg(feature = "z3")] pub use z3_auto::{z3_auto, Z3_TIMEOUT}; #[derive(Debug)] diff --git a/hakim-engine/src/interactive/tactic/z3_auto.rs b/hakim-engine/src/interactive/tactic/z3_auto.rs index 4207273f..af09d870 100644 --- a/hakim-engine/src/interactive/tactic/z3_auto.rs +++ b/hakim-engine/src/interactive/tactic/z3_auto.rs @@ -1,15 +1,19 @@ -use std::{cell::Cell, collections::HashSet, rc::Rc, sync::Mutex, time::Duration}; +use std::{ + cell::Cell, + collections::HashSet, + fmt::format, + ops::{Not, Shl}, + rc::Rc, + sync::Mutex, + time::Duration, +}; use im::HashMap; -use num_bigint::BigInt; -use z3::{ - ast::{self, forall_const, Ast, Bool, Dynamic, Set}, - Config, Context, FuncDecl, Solver, Sort, Symbol, Tactic, -}; +use smt2::*; use crate::{ - analysis::arith::{sigma_to_arith, SigmaSimplifier}, + analysis::arith::SigmaSimplifier, app_ref, brain::{ detect::{ @@ -18,7 +22,7 @@ use crate::{ remove_unused_var, type_of, Abstraction, Term, TermRef, }, interactive::Frame, - library::prelude::{abs, minus, r}, + library::prelude::{abs, minus, r, to_universe}, }; pub fn z3_auto(frame: Frame) -> String { @@ -36,6 +40,13 @@ fn lookup_in_cell_hashmap(x: &Cell>, key: TermRef) -> us r } +fn check_exists(x: &Cell>, key: TermRef) -> bool { + let h = x.take(); + let ex = h.contains_key(key.as_ref()); + x.set(h); + ex +} + fn check_exists_and_insert(x: &Cell>, key: usize) -> bool { let mut h = x.take(); let ex = h.insert(key); @@ -43,51 +54,55 @@ fn check_exists_and_insert(x: &Cell>, key: usize) -> bool { !ex } -struct Z3Manager<'a> { - ctx: &'a Context, +struct Z3Manager { + smt_ctx: Smt2Context, unknowns: Z3Names, finite_axioms: Cell>, - solver: Solver<'a>, is_calculator: bool, } -impl<'a> SigmaSimplifier for &Z3Manager<'a> { - type T = ast::Int<'a>; +impl<'a> SigmaSimplifier for &Z3Manager { + type T = String; fn handle_sigma_atom(self, r: TermRef, f: TermRef) -> Self::T { - let id = lookup_in_cell_hashmap(&self.unknowns.0, f); + todo!() + /* let id = lookup_in_cell_hashmap(&self.unknowns.0, f); let f = FuncDecl::new( self.ctx, format!("$sigma{id}"), &[&Sort::int(self.ctx)], &Sort::int(self.ctx), ); - f.apply(&[&self.handle_term(r)]).try_into().unwrap() + f.apply(&[&self.handle_term(r)]).try_into().unwrap()*/ } fn minus(self, x: Self::T, y: Self::T) -> Self::T { - x - y + todo!(); + // x - y } fn mult(self, x: Self::T, y: Self::T) -> Self::T { - x * y + todo!(); + //x * y } fn plus(self, x: Self::T, y: Self::T) -> Self::T { - x + y + todo!(); + // x + y } fn handle_term(self, t: TermRef) -> Self::T { - self.convert_int_term(t, &[]).unwrap() + todo!() + // self.convert_int_term(t, &[]).unwrap() } } -impl<'a> Z3Manager<'a> { +impl<'a> Z3Manager { fn covert_prop_to_z3_bool( - &self, + &mut self, t: TermRef, - bound_variable: &[Sort<'a>], - ) -> Option> { + bound_variable: &[String], + ) -> Option { if let Term::Forall(Abstraction { var_ty, body, @@ -97,7 +112,7 @@ impl<'a> Z3Manager<'a> { if let Some(body) = remove_unused_var(body.clone()) { let op1 = self.covert_prop_to_z3_bool(var_ty.clone(), bound_variable)?; let op2 = self.covert_prop_to_z3_bool(body, bound_variable)?; - return Some(op1.implies(&op2)); + return Some(op1.implies(op2)); } } if let Term::App { func, op: op2 } = t.as_ref() { @@ -106,10 +121,9 @@ impl<'a> Z3Manager<'a> { if unique_name == "and" || unique_name == "or" { let op1 = &self.covert_prop_to_z3_bool(op1.clone(), bound_variable)?; let op2 = &self.covert_prop_to_z3_bool(op2.clone(), bound_variable)?; - let values = &[op1, op2]; return Some(match unique_name.as_str() { - "and" => ast::Bool::and(self.ctx, values), - "or" => ast::Bool::or(self.ctx, values), + "and" => smt2::Term::land(op1.clone(), op2.clone()), + "or" => smt2::Term::lor(op1.clone(), op2.clone()), _ => unreachable!(), }); } @@ -118,14 +132,12 @@ impl<'a> Z3Manager<'a> { } if let Term::Axiom { unique_name, .. } = t.as_ref() { if unique_name == "False" || unique_name == "True" { - return Some(ast::Bool::from_bool( - self.ctx, - match unique_name.as_str() { - "True" => true, - "False" => false, - _ => unreachable!(), - }, - )); + let t = match unique_name.as_str() { + "True" => true, + "False" => false, + _ => unreachable!(), + }; + return Some(smt2::Term::Binary(t)); } } if let Term::App { func, op: op2 } = t.as_ref() { @@ -138,35 +150,34 @@ impl<'a> Z3Manager<'a> { "eq" => { let op1 = self.convert_general_term(op1, bound_variable)?; let op2 = self.convert_general_term(op2, bound_variable)?; - return Some(op1._safe_eq(&op2).unwrap()); + return Some(smt2::Term::bveq(op1, op2)); } "inset" => { - let op2 = self.convert_set_term(op2, bound_variable)?; + let op2 = self.convert_general_term(op2, bound_variable)?; let op1 = self.convert_general_term(op1, bound_variable)?; - dbg!(op2.get_sort().clone()); - dbg!(op1.get_sort().clone()); - return Some(op2.member(&op1)); + return Some(smt2::Term::select(op2, vec![op1])); } "inlist" => { - let ls = self.convert_list_term(op2, bound_variable)?; - let elem = self.convert_general_term(op1, &[])?; - return Some(ls.contains(&ast::Seq::unit(self.ctx, &elem))); + let ls = self.convert_general_term(op2, bound_variable)?; + let elem = self.convert_general_term(op1, &bound_variable)?; + return Some(smt2::Term::Identifier(format!( + "(seq.contains {ls} (seq.unit {elem}))" + ))); } "included" => { - let op2 = self.convert_set_term(op2, bound_variable)?; - let op1 = self.convert_set_term(op1, bound_variable)?; - return Some(op1.set_subset(&op2)); + let op2 = self.convert_general_term(op2, bound_variable)?; + let op1 = self.convert_general_term(op1, bound_variable)?; + return Some(smt2::Term::Identifier(format!( + "(subset {op1} {op2})" + ))); } "lt" => { - if detect_z_ty(ty) { - let op1 = self.convert_int_term(op1, bound_variable)?; - let op2 = self.convert_int_term(op2, bound_variable)?; - return Some(op1.lt(&op2)); - } - if detect_r_ty(ty) { - let op1 = self.convert_real_term(op1, bound_variable)?; - let op2 = self.convert_real_term(op2, bound_variable)?; - return Some(op1.lt(&op2)); + if detect_z_ty(ty) || detect_r_ty(ty) { + let op1 = self.convert_general_term(op1, bound_variable)?; + let op2 = self.convert_general_term(op2, bound_variable)?; + return Some(smt2::Term::Identifier(format!( + "(< {op1} {op2})" + ))); } } _ => (), @@ -176,517 +187,326 @@ impl<'a> Z3Manager<'a> { if let Term::Axiom { unique_name, .. } = func.as_ref() { match unique_name.as_str() { "divide" => { - let op1 = self.convert_int_term(op1, bound_variable)?; - let op2 = self.convert_int_term(op2, bound_variable)?; - let exp = op2 - .modulo(&op1) - ._safe_eq(&ast::Int::from_i64(self.ctx, 0)) - .ok()?; - return Some(exp); + let op1 = self.convert_general_term(op1, bound_variable)?; + let op2 = self.convert_general_term(op2, bound_variable)?; + return Some(smt2::Term::Identifier(format!( + "(= (rem {op2} {op1}) 0)" + ))); } "finite" => { - let x = self.get_finite_for_sort(op1)?; - let set = self.convert_general_term(op2, bound_variable)?; - return Some(x.apply(&[&set]).try_into().unwrap()); + // let x = self.get_finite_for_sort(op1)?; + // let set = self.convert_general_term(op2, bound_variable)?; + // return Some(x.apply(&[&set]).try_into().unwrap()); + return None; } _ => (), } } } } - Some( - self.generate_unknown(t, Sort::bool(self.ctx)) - .try_into() - .unwrap(), - ) - } - - fn generate_unknown(&self, key: TermRef, sort: Sort<'a>) -> ast::Dynamic<'a> { - let id = lookup_in_cell_hashmap(&self.unknowns.0, key); - ast::Dynamic::new_const(self.ctx, format!("$x{id}"), &sort) - } - - fn convert_int_term(&self, t: TermRef, bound_variable: &[Sort<'a>]) -> Option> { - Some( - self.convert_general_term(t, bound_variable)? - .try_into() - .expect("mismatched type"), - ) - } - - fn convert_set_term(&self, t: TermRef, bound_variable: &[Sort<'a>]) -> Option> { - Some( - self.convert_general_term(t, bound_variable)? - .try_into() - .expect("mismatched type"), - ) - } - - fn convert_real_term(&self, t: TermRef, bound_variable: &[Sort<'a>]) -> Option> { - Some( - self.convert_general_term(t, bound_variable)? - .try_into() - .expect("mismatched type"), - ) + Some(self.generate_unknown(t, "Bool".to_string()).unwrap()) } - fn convert_string_term( - &self, - t: TermRef, - bound_variable: &[Sort<'a>], - ) -> Option> { - Some( - self.convert_general_term(t, bound_variable)? - .try_into() - .expect("mismatched type"), - ) - } - - fn convert_list_term(&self, t: TermRef, bound_variable: &[Sort<'a>]) -> Option> { - Some( - self.convert_general_term(t, bound_variable)? - .try_into() - .expect("mismatched type"), - ) + fn generate_unknown(&mut self, key: TermRef, sort: String) -> Option { + let id = if !check_exists(&self.unknowns.0, key.clone()) { + let id = lookup_in_cell_hashmap(&self.unknowns.0, key); + self.smt_ctx + .variable(smt2::VarDecl::new(format!("$x{id}"), sort)); + id + } else { + lookup_in_cell_hashmap(&self.unknowns.0, key) + }; + return Some(smt2::Term::Identifier(format!("$x{id}"))); } - fn convert_array_term(&self, t: TermRef) -> Option> { + fn convert_array_term(&mut self, t: TermRef) -> Option { let mut bound_variable = vec![]; - let mut names = vec![]; + // let mut names = vec![]; let mut term_body = t; while let Term::Fun(a) = term_body.as_ref() { let sort = self.convert_sort(&a.var_ty)?; - bound_variable.push(sort); - names.push( - a.hint_name - .clone() - .unwrap_or(format!("$arg{}", names.len())), - ); + bound_variable.push(smt2::SortedVar::new(a.hint_name.clone().expect("_"), sort)); term_body = a.body.clone(); } - let body = self.convert_general_term(term_body, &bound_variable)?; + let names: Vec = bound_variable.iter().map(|var| var.ident.clone()).collect(); + let body = self.convert_general_term(term_body, names.as_slice())?; if bound_variable.is_empty() { - let t = body.as_array()?; - return Some(t); + return Some(format!("{body}")); } - let names: Vec<_> = names.into_iter().map(Symbol::from).collect(); - let sorts: Vec<_> = bound_variable.iter().rev().collect(); - return Some(ast::Array::lambda(self.ctx, &names, &sorts, body)); + let t = smt2::Term::lambda(bound_variable, body); + return Some(format!("{t}")); } #[allow(clippy::single_match)] fn convert_general_term( - &self, + &mut self, t: TermRef, - bound_variable: &[Sort<'a>], - ) -> Option> { + bound_variable: &[String], + ) -> Option { match t.as_ref() { Term::Axiom { ty, unique_name } => { if self.is_calculator { return None; } + if check_exists(&self.unknowns.0, t.clone()) { + return Some(smt2::Term::Identifier(unique_name.clone())); + } let sort = self.convert_sort(ty)?; - return Some(ast::Dynamic::new_const( - self.ctx, - unique_name.as_str(), - &sort, - )); + self.smt_ctx + .variable(VarDecl::new(unique_name.clone(), sort)); + lookup_in_cell_hashmap(&self.unknowns.0, t.clone()); + return Some(smt2::Term::Identifier(unique_name.clone())); } Term::Universe { .. } => (), Term::Forall(_) => todo!(), Term::Fun(_) => (), Term::Var { index } => { - let sort = bound_variable.get(*index)?; - return Some(ast::Dynamic::bound_varible(self.ctx, *index as u8, sort)); + let name = bound_variable.get(*index)?; + return Some(smt2::Term::Identifier(name.clone())); } Term::Number { value } => { - let x = ast::Int::from_i64(self.ctx, value.try_into().ok()?); - return Some(x.into()); + return Some(smt2::Term::Identifier(value.to_string())); } Term::NumberR { value, point } => { - let x = ast::Real::from_real( - self.ctx, - value.try_into().ok()?, - (*point < 10).then(|| 10_i32.pow(*point as u32))?, - ); - return Some(x.into()); + let mut value = value.to_string(); + if value.len() < *point { + let mut zeros: String = + std::iter::repeat('0').take(point - value.len()).collect(); + zeros.insert(0, '.'); + value.insert_str(0, zeros.as_str()) + } else { + value.insert(value.len() - point, '.'); + } + return Some(smt2::Term::Identifier(value)); } Term::App { func, op: op2 } => { + let op2_t = self + .convert_general_term(op2.clone(), bound_variable) + .unwrap_or(smt2::Term::Identifier("".to_string())); match func.as_ref() { Term::Axiom { unique_name, .. } => { if unique_name == "set_empty" { - return Some( - ast::Set::empty(self.ctx, &self.convert_sort(op2)?).into(), - ); + let sort = self.convert_sort(op2)?; + return Some(smt2::Term::Identifier(format!( + "((as const (Array {sort} Bool)) false)" + ))); } if unique_name == "nil" { if detect_char_ty(op2) { - let emp = ast::String::from_str(self.ctx, "").ok()?; - return Some(emp.into()); + let nil = ""; + return Some(smt2::Term::Identifier(nil.to_string())); } else { let sort = self.convert_sort(op2)?; - return Some(ast::Seq::empty(self.ctx, &sort).into()); + return Some(smt2::Term::Identifier(format!( + "(as seq.empty (Seq {sort}))" + ))); } } if unique_name == "chr" { let c = detect_char(&t)?; - let c = ast::String::from_str(self.ctx, c.to_string().as_str()).ok()?; - let c = unsafe { ast::Seq::wrap(self.ctx, c.get_z3_ast()) }; - return Some(c.nth(&ast::Int::from_i64(self.ctx, 0))); + let unicode = format!("{:X}", (c as u8)); + return Some(smt2::Term::Identifier(format!("#x{unicode}"))); } if unique_name == "sqrt" { - let op2 = self.convert_real_term(op2.clone(), bound_variable)?; - return Some(op2.power(&ast::Real::from_real(self.ctx, 5, 10)).into()); + return Some(smt2::Term::Identifier(format!("(^ {op2_t} 0.5"))); } if unique_name == "abs" { - let op2 = self.convert_real_term(op2.clone(), bound_variable)?; - return Some( - (op2.clone() - .ge(&ast::Real::from_real(self.ctx, 0, 1)) - .ite(&op2.clone(), &(-op2))) - .into(), - ); + return Some(smt2::Term::Identifier(format!( + "(ite (>= {op2_t} 0) {op2_t} (- {op2_t}))" + ))); } } - Term::App { func, op: op1 } => match func.as_ref() { - Term::App { func, op } => match func.as_ref() { - Term::Axiom { unique_name, .. } => match unique_name.as_str() { - "sigma" => { - return Some( - sigma_to_arith::<_, BigInt>( - op.clone(), - op1.clone(), - op2.clone(), - self, - ) - .into(), - ); - } - // "cnt" => { - // return cnt_to_arith(op.clone(), op1.clone(), op2.clone(), arena); - // } - "union" => { - let op2 = self.convert_set_term(op2.clone(), bound_variable)?; - let op1 = self.convert_set_term(op1.clone(), bound_variable)?; - return Some( - ast::Set::set_union(self.ctx, &[&op1, &op2]).into(), - ); - } - "intersection" => { - let op2 = self.convert_set_term(op2.clone(), bound_variable)?; - let op1 = self.convert_set_term(op1.clone(), bound_variable)?; - return Some( - ast::Set::intersect(self.ctx, &[&op1, &op2]).into(), - ); - } - "setminus" => { - let op2 = self - .convert_set_term(op2.clone(), bound_variable)? - .complement(); - let op1 = self.convert_set_term(op1.clone(), bound_variable)?; - return Some( - ast::Set::intersect(self.ctx, &[&op1, &op2]).into(), - ); - } - "plus" => { - if detect_z_ty(op) { - let op2 = - self.convert_int_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_int_term(op1.clone(), bound_variable)?; - return Some((op1 + op2).into()); + Term::App { func, op: op1 } => { + let op1_t = self + .convert_general_term(op1.clone(), bound_variable) + .unwrap_or(smt2::Term::Identifier("".to_string())); + match func.as_ref() { + Term::App { func, op } => match func.as_ref() { + Term::Axiom { unique_name, .. } => match unique_name.as_str() { + "sigma" => { + /* return Some( + sigma_to_arith::<_, BigInt>( + op.clone(), + op1.clone(), + op2.clone(), + self, + ) + .into(), + );*/ } - if detect_r_ty(op) { - let op2 = - self.convert_real_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_real_term(op1.clone(), bound_variable)?; - return Some((op1 + op2).into()); + // "cnt" => { + // return cnt_to_arith(op.clone(), op1.clone(), op2.clone(), arena); + // } + "union" => { + let sort = self.convert_sort(op)?; + return Some(smt2::Term::Identifier(format!( + "((as union (Array {sort} Bool)) {op1_t} {op2_t})" + ))); } - if let Some(elem_ty) = detect_list_ty(op) { - if detect_char_ty(&elem_ty) { - let a = self - .convert_string_term(op1.clone(), bound_variable)?; - let b = self - .convert_string_term(op2.clone(), bound_variable)?; - return Some( - ast::String::concat(self.ctx, &[&a, &b]).into(), - ); - } else { - let a = self - .convert_list_term(op2.clone(), bound_variable)?; - let b = self - .convert_list_term(op1.clone(), bound_variable)?; - return Some( - ast::Seq::concat(self.ctx, &[&a, &b]).into(), - ); - } + "intersection" => { + return Some(smt2::Term::Identifier(format!( + "(intersection {op1_t} {op2_t})" + ))); } - } - "minus" => { - if detect_z_ty(op) { - let op2 = - self.convert_int_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_int_term(op1.clone(), bound_variable)?; - return Some((op1 - op2).into()); + "setminus" => { + return Some(smt2::Term::Identifier(format!( + "(setminus {op1_t} {op2_t})" + ))); } - if detect_r_ty(op) { - let op2 = - self.convert_real_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_real_term(op1.clone(), bound_variable)?; - return Some((op1 - op2).into()); + "plus" => { + let add = if detect_z_ty(op) || detect_r_ty(op) { + "+" + } else if let Some(elem_ty) = detect_list_ty(op) { + if detect_char_ty(&elem_ty) { + "str.++" + } else { + "seq.++" + } + } else { + "" + }; + return Some(smt2::Term::Identifier(format!( + "({add} {op1_t} {op2_t})" + ))); } - } - "mult" => { - if detect_z_ty(op) { - let op2 = - self.convert_int_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_int_term(op1.clone(), bound_variable)?; - return Some((op1 * op2).into()); + "minus" => { + if detect_z_ty(op) || detect_r_ty(op) { + return Some(smt2::Term::Identifier(format!( + "(- {op1_t} {op2_t})" + ))); + } } - if detect_r_ty(op) { - let op2 = - self.convert_real_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_real_term(op1.clone(), bound_variable)?; - return Some((op1 * op2).into()); + "mult" => { + if detect_z_ty(op) || detect_r_ty(op) { + return Some(smt2::Term::Identifier(format!( + "(* {op1_t} {op2_t})" + ))); + } } - } - "div" => { - if definitely_zero(op2) { - return Some(ast::Real::from_real(self.ctx, 0, 1).into()); + "div" => { + if definitely_zero(op2) { + return Some(smt2::Term::Identifier("0.0".to_string())); + } + if detect_z_ty(op) || detect_r_ty(op) { + return Some(smt2::Term::Identifier(format!( + "(/ {op1_t} {op2_t})" + ))); + } } - if detect_z_ty(op) { - let op2 = ast::Real::from_int( - &self.convert_int_term(op2.clone(), bound_variable)?, - ); - let op1 = ast::Real::from_int( - &self.convert_int_term(op1.clone(), bound_variable)?, - ); - return Some((op1 / op2).into()); + "pow" => { + if detect_z_ty(op) || detect_r_ty(op) { + let mut real_pw = format!("(^ {op1_t} {op2_t})"); + if detect_z_ty(op) { + real_pw = format!("(to_int {real_pw})"); + } + return Some(smt2::Term::Identifier(real_pw)); + } + return None; } - if detect_r_ty(op) { - let op2 = - self.convert_real_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_real_term(op1.clone(), bound_variable)?; - return Some((op1 / op2).into()); + "cons" => { + return Some(smt2::Term::Identifier(format!( + "(seq.++ (seq.unit {op1_t}) {op2_t})" + ))); } - } - "pow" => { - if detect_z_ty(op) { - let op2 = - self.convert_int_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_int_term(op1.clone(), bound_variable)?; - let real_pw = - Dynamic::as_real(&op1.power(&op2.clone()).into())?; - return Some(real_pw.to_int().into()); + // call nth with index 0 + "head" => { + return Some(smt2::Term::Identifier(format!( + "(seq.nth {op2_t} 0)" + ))); } - if detect_r_ty(op) { - let op2 = - self.convert_real_term(op2.clone(), bound_variable)?; - let op1 = - self.convert_real_term(op1.clone(), bound_variable)?; - return Some(op1.power(&op2).into()); + "firstn" => { + return Some(smt2::Term::Identifier(format!( + "(seq.extract {op1_t} 0 {op2_t})" + ))); } - return None; - } - "cons" => { - /*if detect_char_ty(op) { - if let Some(s) = detect_string(&t) { - let s = - ast::String::from_str(self.ctx, s.as_str()).ok()?; - return Some(s.into()); - } - let s = - self.convert_string_term(op2.clone(), bound_variable)?; - let c = - self.convert_general_term(op1.clone(), bound_variable)?; - - return Some( - ast::String::concat(self.ctx, &[&c, &s]).into(), - ); - } else {*/ - let head = - self.convert_general_term(op1.clone(), bound_variable)?; - let head = ast::Seq::unit(self.ctx, &head); - let tail = - self.convert_list_term(op2.clone(), bound_variable)?; - return Some( - ast::Seq::concat(self.ctx, &[&head, &tail]).into(), - ); - //} - } - // call nth with index 0 - "head" => { - let ls = self.convert_list_term(op2.clone(), bound_variable)?; - return Some(ls.nth(&ast::Int::from_i64(self.ctx, 0))); - } - "firstn" => { - let length = - self.convert_int_term(op2.clone(), bound_variable)?; - let ls = self.convert_list_term(op1.clone(), bound_variable)?; - return Some( - ls.subsequance(ast::Int::from_i64(self.ctx, 0), length) - .into(), - ); - } - "skipn" => { - let start = - self.convert_int_term(op2.clone(), bound_variable)?; - let ls = self.convert_list_term(op1.clone(), bound_variable)?; - return Some( - ls.subsequance(start.clone(), ls.length() - start).into(), - ); - } - _ => (), - }, - Term::App { func, op: _ } => { - if let Term::Axiom { unique_name, .. } = func.as_ref() { - match unique_name.as_str() { - "if_f" => { - let prop = self.covert_prop_to_z3_bool( - op.clone(), - bound_variable, - )?; - let op1 = self.convert_general_term( - op1.clone(), - bound_variable, - )?; - let op2 = self.convert_general_term( - op2.clone(), - bound_variable, - )?; - return Some(prop.ite(&op1, &op2)); - } - "map" => { - if !detect_char_ty(op) { - let ls = self.convert_list_term( - op2.clone(), + "skipn" => { + return Some(smt2::Term::Identifier(format!( + "(seq.extract {op1_t} {op2_t} (- (seq.len {op1_t}) {op2_t}))" + ))); + } + _ => (), + }, + Term::App { func, op: _ } => { + if let Term::Axiom { unique_name, .. } = func.as_ref() { + match unique_name.as_str() { + "if_f" => { + let prop = self.covert_prop_to_z3_bool( + op.clone(), bound_variable, )?; - let fun_as_arr = - self.convert_array_term(op1.clone())?; - - //let maped_ls_sort = self.convert_sort(op)?; - let maped_ls_sort = - Sort::seq(self.ctx, &self.convert_sort(op)?); - let fun = self - .generate_unknown( - op1.clone(), - fun_as_arr.get_sort(), - ) - .as_array()?; - let from = self - .generate_unknown(op2.clone(), ls.get_sort()) - .as_seq()?; - let maped_ls = self - .generate_unknown(t.clone(), maped_ls_sort) - .as_seq()?; - let prob = self.ctx.from_string( - "(assert (= (seq.map fun from) to))", - &[], - &[], - &["fun", "from", "to"], - &[&fun.decl(), &from.decl(), &maped_ls.decl()], - ); - self.solver.assert(prob.first().unwrap()); - self.solver.assert(&from._eq(&ls)); - self.solver.assert(&fun._eq(&fun_as_arr)); - return Some(maped_ls.into()); + return Some(smt2::Term::Identifier(format!( + "(ite {prop} {op2_t} {op1_t})" + ))); } + "map" => { + if !detect_char_ty(op) { + let fun_as_arr = + self.convert_array_term(op1.clone())?; + return Some(smt2::Term::Identifier(format!( + "(seq.map {fun_as_arr} {op2_t})" + ))); + } + } + //nth: forall X, X -> list X -> Z -> X + "nth" => { + return Some(smt2::Term::Identifier(format!( + "(seq.nth {op1_t} {op2_t})" + ))); + } + _ => (), } - //nth: forall X, X -> list X -> Z -> X - "nth" => { - let index = - self.convert_int_term(op2.clone(), bound_variable)?; - let ls = self - .convert_list_term(op1.clone(), bound_variable)?; - return Some(ls.nth(&index)); - } - _ => (), } } - } - _ => (), - }, - Term::Axiom { unique_name, .. } => match unique_name.as_str() { - "set_singleton" => { - return Some( - ast::Set::empty(self.ctx, &self.convert_sort(op1)?) - .add( - &self.convert_general_term( - op2.clone(), - bound_variable, - )?, - ) - .into(), - ); - } - "mod_of" => { - let op2 = self.convert_int_term(op2.clone(), bound_variable)?; - let op1 = self.convert_int_term(op1.clone(), bound_variable)?; - return Some((op1.rem(&op2)).into()); - } - /* "pow" => { - let op2 = self.convert_int_term(op2.clone())?; - let op1 = self.convert_int_term(op1.clone())?; - return Some( - ast::Real::try_from(ast::Dynamic::from(op1.power(&op2))) - .unwrap() - .to_int() - .into(), - ); - }*/ - "neg" => { - if detect_z_ty(op1) { - let op = self.convert_int_term(op2.clone(), bound_variable)?; - return Some((-op).into()); - } else if detect_r_ty(op1) { - let op = self.convert_real_term(op2.clone(), bound_variable)?; - return Some((-op).into()); + _ => (), + }, + Term::Axiom { unique_name, .. } => match unique_name.as_str() { + "set_singleton" => { + let sort = self.convert_sort(op1)?; + return Some(smt2::Term::Identifier(format!( + "(store ((as const (Array {sort} Bool)) false) {op2_t} true)" + ))); } - } - "len1" => { - if detect_z_ty(op1) { - let a = self.convert_int_term(op2.clone(), bound_variable)?; - return Some( - a.clone() - .ge(&ast::Int::from_u64(self.ctx, 0)) - .ite(&a.clone(), &(-a)) - .into(), - ); - } else if detect_list_ty(op1).is_some() { - let l = self.convert_list_term(op2.clone(), bound_variable)?; - return Some(l.length().into()); + "mod_of" => { + return Some(smt2::Term::Identifier(format!( + "(rem {op1_t} {op2_t})" + ))); } - } - "Eucli" => { - let op = self.convert_general_term( - app_ref!( - abs(), - app_ref!(app_ref!(app_ref!(minus(), r()), op1), op2) - ), - bound_variable, - )?; - return Some(op); - } + "neg" => { + if detect_z_ty(op1) || detect_r_ty(op1) { + return Some(smt2::Term::Identifier(format!( + "(- {op2_t})" + ))); + } + } + "len1" => { + if detect_z_ty(op1) { + return Some(smt2::Term::Identifier(format!( + "(ite (>= {op2_t} 0) {op2_t} (- {op2_t}))" + ))); + } else if detect_list_ty(op1).is_some() { + return Some(smt2::Term::Identifier(format!( + "(seq.len {op2_t})" + ))); + } + } + "Eucli" => { + let op = self.convert_general_term( + app_ref!( + abs(), + app_ref!(app_ref!(app_ref!(minus(), r()), op1), op2) + ), + bound_variable, + )?; + return Some(op); + } + _ => (), + // "pow" => pow_to_arith(op1.clone(), op2.clone(), arena), + // "len1" => return len1_to_arith(op1.clone(), op2.clone(), arena), + // _ => atom_normalizer(t), + }, _ => (), - // "minus" => minus( - // term_ref_to_arith(op1.clone(), arena), - // term_ref_to_arith(op2.clone(), arena), - // arena, - // ), - // "pow" => pow_to_arith(op1.clone(), op2.clone(), arena), - // "len1" => return len1_to_arith(op1.clone(), op2.clone(), arena), - // _ => atom_normalizer(t), - }, - _ => (), - }, + } + } _ => (), } /*if let Some(func) = self.convert_array_term(func.clone()) { @@ -705,64 +525,74 @@ impl<'a> Z3Manager<'a> { return None; } let ty = type_of(t.clone()).unwrap(); + if let Term::Universe { .. } = ty.as_ref() { + return None; + } let sort = self.convert_sort(&ty)?; dbg!(sort.clone()); - Some(self.generate_unknown(t, sort)) + self.generate_unknown(t, sort) } - fn convert_sort(&self, t: &Term) -> Option> { + fn convert_sort(&mut self, t: &Term) -> Option { if detect_z_ty(t) { - return Some(Sort::int(self.ctx)); + return Some("Int".to_string()); } if detect_r_ty(t) { - return Some(Sort::real(self.ctx)); + return Some("Real".to_string()); } if detect_char_ty(t) { - let c = ast::String::from_str(self.ctx, "a").unwrap(); - let c = unsafe { ast::Seq::wrap(self.ctx, c.get_z3_ast()) }; - let c = c.nth(&ast::Int::from_i64(self.ctx, 0)); - return Some(c.get_sort()); + return Some("(_ BitVec 8)".to_string()); } if let Some(elt) = detect_list_ty(t) { if detect_char_ty(&elt) { - return Some(Sort::string(self.ctx)); + return Some("String".to_string()); } else { let elt = self.convert_sort(&elt)?; - return Some(Sort::seq(self.ctx, &elt)); + return Some(format!("(Seq {elt})")); } } if let Some(ty) = detect_set_ty(t) { let sort = self.convert_sort(&ty)?; - return Some(Sort::set(self.ctx, &sort)); + return Some(format!("(Seq {sort})")); } - if let Term::Axiom { ty, unique_name } = t { + /* if let Term::Axiom { ty, unique_name } = t { assert!(matches!(ty.as_ref(), Term::Universe { .. })); - return Some(Sort::uninterpreted( - self.ctx, - z3::Symbol::String(unique_name.to_string()), - )); - } + + if check_exists(&self.unknowns.0, TermRef::new(t.clone())) { + return Some(unique_name.clone()); + } + let sort = smt2::Sort::Declare(SortDecl::new(unique_name.clone(), 0)); + self.smt_ctx.sort(sort); + lookup_in_cell_hashmap(&self.unknowns.0, TermRef::new(t.clone())); + return Some(unique_name.clone()); + }*/ if let Term::Forall(a) = t { let domain = self.convert_sort(&a.var_ty)?; let range = self.convert_sort(&a.body)?; - return Some(Sort::array(self.ctx, &domain, &range)); + + return Some(format!("(Array {domain} {range})")); } let ty = type_of(Rc::new(t.clone())).ok()?; if let Term::Universe { index } = ty.as_ref() { if *index == 0 { - return Some(Sort::uninterpreted( - self.ctx, - z3::Symbol::String(format!("{:?}", t)), - )); + let key = app_ref!(to_universe(), TermRef::new(t.clone())); + let sort_name = format!("{:?}", t); + if check_exists(&self.unknowns.0, key.clone()) { + return Some(sort_name); + } + let sort = smt2::Sort::Declare(SortDecl::new(sort_name.clone(), 0)); + self.smt_ctx.sort(sort); + lookup_in_cell_hashmap(&self.unknowns.0, key); + return Some(sort_name); } } None } - fn get_finite_for_sort(&self, ty: TermRef) -> Option> { - let sort_elem = self.convert_sort(&ty)?; + fn get_finite_for_sort(&self, ty: TermRef) -> Option<()> { + /* let sort_elem = self.convert_sort(&ty)?; let sort = Sort::set(self.ctx, &sort_elem); - let id = lookup_in_cell_hashmap(&self.unknowns.0, ty); + let id: usize = lookup_in_cell_hashmap(&self.unknowns.0, ty); let r = FuncDecl::new( self.ctx, format!("$finite{id}"), @@ -809,7 +639,8 @@ impl<'a> Z3Manager<'a> { &s1f.implies(&set2.set_subset(&set1).implies(&s2f)), )); } - Some(r) + Some(r)*/ + None } } @@ -824,16 +655,15 @@ fn definitely_zero(op2: &Term) -> bool { pub static Z3_TIMEOUT: Mutex = Mutex::new(Duration::from_millis(2000)); fn z3_can_solve(frame: Frame) -> String { - let cfg = &Config::new(); + /*let cfg = &Config::new(); let ctx = &Context::new(cfg); let solver = Tactic::new(ctx, "default") .try_for(*Z3_TIMEOUT.lock().unwrap()) - .solver(); - let z3manager = Z3Manager { - ctx, + .solver();*/ + let mut z3manager = Z3Manager { + smt_ctx: Smt2Context::new(), unknowns: Z3Names::default(), finite_axioms: Cell::default(), - solver, is_calculator: frame.engine.params.get("auto_level") == Some(&"calculator".to_string()), }; for hyp in frame.hyps { @@ -841,19 +671,23 @@ fn z3_can_solve(frame: Frame) -> String { let Some(b) = z3manager.covert_prop_to_z3_bool(hyp.ty, &[]) else { continue; }; - z3manager.solver.assert(&b); + // dbg!(z3manager.smt_ctx.to_code(true)); + z3manager.smt_ctx.assert(b); } if let Some(b) = z3manager.covert_prop_to_z3_bool(frame.goal, &[]) { - z3manager.solver.assert(&b.not()); + z3manager.smt_ctx.assert(b.not()); } - - dbg!(&z3manager.solver); - z3manager.solver.to_string() + z3manager.smt_ctx.check_sat(); + let state = z3manager.smt_ctx.to_code(true); + dbg!(&state); + state } #[cfg(test)] mod tests { - use crate::interactive::tests::{run_interactive_to_end, run_interactive_to_fail}; + use crate::interactive::tests::{ + run_interactive, run_interactive_to_end, run_interactive_to_fail, EngineLevel, + }; fn success(goal: &str) { run_interactive_to_end(goal, "intros\nz3"); @@ -863,6 +697,30 @@ mod tests { run_interactive_to_fail(goal, "intros", "z3"); } + fn convert_check(term: &str, smt_lib2: &str) { + let session = run_interactive(term, "intros", EngineLevel::Full); + let state = session.z3_get_state().unwrap(); + assert_eq!(state, smt_lib2); + } + + #[test] + fn check() { + convert_check("∀ x c: ℤ, 2 * x = c -> False", "(declare-const $x0 Bool)\n(assert $x0)\n(assert $x0)\n(declare-const x Int)\n(declare-const c Int)\n(assert (= (* 2 x) c))\n(assert (not false))\n(check-sat)\n"); + convert_check("∀ x: ℝ, x = 3. -> x > 0.01", "(declare-const $x0 Bool)\n(assert $x0)\n(declare-const x Real)\n(assert (= x 3.))\n(assert (not (< .01 x)))\n(check-sat)\n"); + convert_check("∀ x: ℤ, x ∈ {2} -> x + x = 4", "(declare-const $x0 Bool)\n(assert $x0)\n(declare-const x Int)\n(assert (select (store ((as const (Array Int Bool)) false) 2 true) x))\n(assert (not (= (+ x x) 4)))\n(check-sat)\n"); + convert_check( + "Eucli 2. 4. = 2.", + "(assert (not (= (ite (>= (- 2. 4.) 0) (- 2. 4.) (- (- 2. 4.))) 2.)))\n(check-sat)\n", + ); + convert_check(r#"∀ x: char, 'a' = head '*' "a" "#, "(declare-const $x0 Bool)\n(assert $x0)\n(assert (not (= #x61 (seq.nth (seq.++ (seq.unit #x61) ) 0))))\n(check-sat)\n"); + convert_check( + "(∃ x, 2 < x) -> (∃ x, 2 < x)", + "(declare-const $x0 Bool)\n(assert $x0)\n(assert (not $x0))\n(check-sat)\n", + ); + convert_check(r#""s" + "l" + " a" = "sl a""#, "(assert (not (= (str.++ (str.++ (seq.++ (seq.unit #x73) ) (seq.++ (seq.unit #x6C) )) (seq.++ (seq.unit #x20) (seq.++ (seq.unit #x61) ))) (seq.++ (seq.unit #x73) (seq.++ (seq.unit #x6C) (seq.++ (seq.unit #x20) (seq.++ (seq.unit #x61) )))))))\n(check-sat)\n"); + convert_check(r#"nth '*' "aa" 0 ∈ member_set "a""#, "(declare-const $x0 (Seq (_ BitVec 8)))\n(assert (not (select $x0 (seq.nth (seq.++ (seq.unit #x61) (seq.++ (seq.unit #x61) )) 0))))\n(check-sat)\n"); + // convert_check(r#"map (λ x, 2*x) [2] = [4]"#, ""); + } #[test] fn simple() { success("False -> True"); diff --git a/hakim-json/src/lib.rs b/hakim-json/src/lib.rs index f946ab74..5f610e2a 100644 --- a/hakim-json/src/lib.rs +++ b/hakim-json/src/lib.rs @@ -57,7 +57,6 @@ pub enum Command { Check(String), ActionOfTactic(String), TryTactic(String), - #[cfg(feature = "z3")] ChangeZ3Timeout(u64), Z3Solved, } @@ -147,11 +146,8 @@ pub fn run_command(command: Command, state: &mut State) -> String { if let Some(x) = s.try_auto() { serialize(x) } else { - serialize(None::) + serialize(s.z3_get_state().map(Z3State)) } - // else { - // serialize(s.z3_get_state().map(Z3State)) - // } } TryAutoHistory => serialize(state.session.as_ref().and_then(|s| s.history_based_auto())), GetHistory => serialize(state.session.as_ref().map(|s| s.get_history())), @@ -299,10 +295,9 @@ pub fn run_command(command: Command, state: &mut State) -> String { }; serialize(state.session.as_ref().unwrap().pos_of_span_goal((l, r))) } - #[cfg(feature = "z3")] ChangeZ3Timeout(t) => { - let mut g = Z3_TIMEOUT.lock().unwrap(); - *g = Duration::from_millis(t); + //let mut g = Z3_TIMEOUT.lock().unwrap(); + //*g = Duration::from_millis(t); serialize(()) } Z3Solved => {