try to disable z3

babaeee · Jan 18, 2024 · aad203c · aad203c
1 parent 78171cf
commit aad203c
Show file tree

Hide file tree

Showing 5 changed files with 26 additions and 7 deletions.
diff --git a/front/src/index.html b/front/src/index.html
@@ -11,9 +11,9 @@
     <script src="/static/hakim-json.js"></script>
 </body>
 
-<script src="/z3-built.js"></script>
+<!-- script src="/z3-built.js"></script >
 <script>
     globalThis.global = { initZ3: globalThis.initZ3 };
-</script>
+</script-->
 
 </html>
diff --git a/hakim-engine/Cargo.toml b/hakim-engine/Cargo.toml
@@ -14,12 +14,15 @@ 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", features = [
+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", features = [
+z3-sys = { git = "https://github.com/arshiamoeini/my_z3.git", optional = true, features = [
     "static-link-z3",
 ] }
 
+[features]
+z3 = ["dep:z3", "dep:z3-sys"]
+
 [dev-dependencies]
 rayon = "1.6.0"
diff --git a/hakim-engine/src/interactive.rs b/hakim-engine/src/interactive.rs
@@ -8,6 +8,7 @@ use crate::interactive::suggest::Applicablity;
 use crate::library::{engine_from_middle_of_lib, proof_of_theorem};
 use crate::parser::is_whity_char;
 
+#[cfg(feature = "z3")]
 pub use tactic::Z3_TIMEOUT;
 
 #[cfg(test)]
@@ -33,8 +34,10 @@ 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, z3_auto,
+    add_from_lib, assumption, auto_list, auto_set, chain, remove_hyp, revert, unfold,
 };
 
 #[derive(Debug, Clone, Serialize, Deserialize)]
@@ -280,6 +283,8 @@ impl Session {
         }
         self.last_snapshot().last_frame()?.try_auto()
     }
+
+    #[cfg(feature = "z3")]
     pub fn z3_get_state(&self) -> Option<String> {
         Some(z3_auto(self.last_snapshot().last_frame()?.clone()))
     }
@@ -482,6 +487,7 @@ 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
@@ -34,7 +34,9 @@ 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-json/src/lib.rs b/hakim-json/src/lib.rs
@@ -3,10 +3,13 @@ use std::time::Duration;
 use hakim_engine::{
     all_library_data,
     engine::Engine,
-    interactive::{tactic, Session, Suggestion, Z3_TIMEOUT},
+    interactive::{tactic, Session, Suggestion},
     notation_list,
 };
 
+#[cfg(feature = "z3")]
+use hakim_engine::interactive::Z3_TIMEOUT;
+
 use hakim_engine::library::LIB_TEXT_STORE;
 
 use serde::{Deserialize, Serialize};
@@ -54,6 +57,7 @@ pub enum Command {
     Check(String),
     ActionOfTactic(String),
     TryTactic(String),
+    #[cfg(feature = "z3")]
     ChangeZ3Timeout(u64),
     Z3Solved,
 }
@@ -143,8 +147,11 @@ pub fn run_command(command: Command, state: &mut State) -> String {
             if let Some(x) = s.try_auto() {
                 serialize(x)
             } else {
-                serialize(s.z3_get_state().map(Z3State))
+                serialize(None::<String>)
             }
+            // 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())),
@@ -292,6 +299,7 @@ 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);