From 18a73042e5d599748cd12f4e90548d7f8a9222a0 Mon Sep 17 00:00:00 2001
From: Adrien Champion <adrien.champion@protonmail.com>
Date: Mon, 15 Jan 2024 11:25:03 +0100
Subject: [PATCH] fix: improve preproc triviality checks

---
 src/common/config.rs |  8 ++++-
 src/common/smt.rs    | 73 +++++++++++++++++++++++++++++++++++++++++---
 src/teacher.rs       |  2 +-
 3 files changed, 76 insertions(+), 7 deletions(-)

diff --git a/src/common/config.rs b/src/common/config.rs
index cfdf3253..b956d93a 100644
--- a/src/common/config.rs
+++ b/src/common/config.rs
@@ -16,7 +16,7 @@ use crate::{common::mk_dir, errors::*, instance::Instance};
 macro_rules! app_fun {
     // Internal rules.
     (@app $app:expr, $order:expr =>) => ($app);
-    (@app $app:expr, $o7rder:expr =>
+    (@app $app:expr, $order:expr =>
         , $($tail:tt)*
     ) => (
         app_fun!(@app $app, $order => $($tail)*)
@@ -1179,6 +1179,12 @@ impl Config {
         self.check.as_ref()
     }
 
+    /// True if a timeout was specified.
+    #[inline]
+    pub fn has_timeout(&self) -> bool {
+        self.timeout.is_some()
+    }
+
     /// Checks if we're out of time.
     #[inline]
     pub fn check_timeout(&self) -> Res<()> {
diff --git a/src/common/smt.rs b/src/common/smt.rs
index 6116046e..d975c319 100644
--- a/src/common/smt.rs
+++ b/src/common/smt.rs
@@ -62,7 +62,7 @@ pub fn preproc_reset<P>(solver: &mut Solver<P>) -> Res<()> {
 }
 
 /// Performs a check-sat.
-pub fn tmo_multi_try_check_sat<P, F>(
+pub fn tmo_multi_try_check_sat_legacy<P, F>(
     solver: &mut Solver<P>,
     tmo: ::std::time::Duration,
     do_stuff: F,
@@ -87,6 +87,44 @@ where
     }
 }
 
+/// Performs a check-sat.
+pub fn tmo_multi_check_sat<P, F>(
+    solver: &mut Solver<P>,
+    tmo: ::std::time::Duration,
+    do_stuff: F,
+) -> Res<bool>
+where
+    F: FnOnce(&mut Solver<P>) -> Res<()>,
+{
+    solver.set_option(":timeout", &format!("{}000", tmo.as_secs()))?;
+    if let Some(res) = multi_try_check_sat_or_unk(solver)? {
+        return Ok(res);
+    }
+    do_stuff(solver)?;
+    if let Some(res) = multi_try_check_sat_or_unk(solver)? {
+        Ok(res)
+    } else {
+        bail!(crate::errors::ErrorKind::Unknown)
+    }
+}
+
+/// Performs a check-sat.
+pub fn tmo_multi_try_check_sat<P, F>(
+    solver: &mut Solver<P>,
+    tmo: ::std::time::Duration,
+    do_stuff: F,
+) -> Res<Option<bool>>
+where
+    F: FnOnce(&mut Solver<P>) -> Res<()>,
+{
+    solver.set_option(":timeout", &format!("{}000", tmo.as_secs()))?;
+    if let Some(res) = multi_try_check_sat_or_unk(solver)? {
+        return Ok(Some(res));
+    }
+    do_stuff(solver)?;
+    multi_try_check_sat_or_unk(solver)
+}
+
 /// Performs a check-sat.
 ///
 /// Tries to check-sat a solver with various strategies. Returns the result of the first tries that
@@ -298,19 +336,44 @@ where
         }
 
         solver.assert_with(self, false)?;
-        let sat = tmo_multi_try_check_sat(
+        let sat = tmo_multi_check_sat(
             solver,
             conf.until_timeout()
-                .map(|time| time / 20)
+                .map(|time| time / 100)
                 .unwrap_or_else(|| ::std::time::Duration::new(1, 0)),
             |solver| {
                 solver.assert_with(self, true)?;
                 Ok(())
             },
-            true,
         )?;
         Ok(!sat)
     }
+
+    /// Checks if this conjunction is unsatisfiable.
+    fn try_is_unsat<Parser: Copy>(&self, solver: &mut Solver<Parser>) -> Res<Option<bool>> {
+        if self.terms.len() == 0 {
+            return Ok(Some(false));
+        }
+        for var in self.infos {
+            if var.active {
+                solver.declare_const(&var.idx, var.typ.get())?
+            }
+        }
+
+        solver.assert_with(self, false)?;
+        let is_unsat = tmo_multi_try_check_sat(
+            solver,
+            conf.until_timeout()
+                .map(|time| time / 100)
+                .unwrap_or_else(|| ::std::time::Duration::new(1, 0)),
+            |solver| {
+                solver.assert_with(self, true)?;
+                Ok(())
+            },
+        )?
+        .map(|b| !b);
+        Ok(is_unsat)
+    }
 }
 
 impl<'a, 'b, Trms> Expr2Smt<bool> for SmtConj<'b, Trms>
@@ -1033,7 +1096,7 @@ impl<Parser: Copy> ClauseTrivialExt for Solver<Parser> {
                 if lhs.is_empty() {
                     Ok(Some(false))
                 } else {
-                    conj.is_unsat(self).map(Some)
+                    conj.try_is_unsat(self)
                 }
             }
         };
diff --git a/src/teacher.rs b/src/teacher.rs
index 80bad166..d0516ddf 100644
--- a/src/teacher.rs
+++ b/src/teacher.rs
@@ -1013,7 +1013,7 @@ impl<'a> Teacher<'a> {
                         let tru_preds = & self.tru_preds;
                         let fls_preds = & self.fls_preds;
                         let instance = & self.instance;
-                        smt::tmo_multi_try_check_sat(
+                        smt::tmo_multi_try_check_sat_legacy(
                             solver,
                             conf.until_timeout().map(
                                 |time| time / 20