integrate sca into the simplify tool

Author: ekiwi

patronus-sca/src/lib.rs

@@ -387,6 +387,12 @@ pub struct ScaEqualityProblem {
     word_level: ExprRef,
 }
 
+impl ScaEqualityProblem {
+    pub fn equality_expr(&self) -> ExprRef {
+        self.equality
+    }
+}
+
 pub fn find_sca_simplification_candidates(ctx: &Context, e: ExprRef) -> Vec<ScaEqualityProblem> {
     let mut problems = vec![];
     let _ = traversal::bottom_up(ctx, e, |ctx, e, children: &[AnalysisResult]| {

patronus/src/smt/parser.rs

@@ -358,6 +358,7 @@ pub fn parse_command(ctx: &mut Context, st: &SymbolTable, input: &[u8]) -> Resul
         Some(Token::Value(name)) => match name {
             b"exit" => SmtCommand::Exit,
             b"check-sat" => SmtCommand::CheckSat,
+            b"reset" => SmtCommand::Reset,
             b"set-logic" => {
                 let logic = parse_logic(&mut lexer)?;
                 SmtCommand::SetLogic(logic)

patronus/src/smt/serialize.rs

@@ -290,6 +290,7 @@ pub fn serialize_cmd(out: &mut impl Write, ctx: Option<&Context>, cmd: &SmtComma
     match cmd {
         SmtCommand::Exit => writeln!(out, "(exit)"),
         SmtCommand::CheckSat => writeln!(out, "(check-sat)"),
+        SmtCommand::Reset => writeln!(out, "(reset)"),
         SmtCommand::SetLogic(logic) => writeln!(out, "(set-logic {})", logic.to_smt_str()),
         SmtCommand::SetOption(name, value) => {
             writeln!(out, "(set-option :{name} {})", escape_smt_identifier(value))

patronus/src/smt/solver.rs

@@ -65,6 +65,8 @@ pub enum SmtCommand {
     Push(u64),
     Pop(u64),
     GetValue(ExprRef),
+    /// Resets the solver to the startup state
+    Reset,
 }
 
 /// The result of a `(check-sat)` command.

tools/simplify/Cargo.toml

@@ -12,3 +12,4 @@ rust-version.workspace = true
 patronus.workspace = true
 clap.workspace = true
 rustc-hash.workspace = true
+patronus-sca = {path="../../patronus-sca"}

tools/simplify/src/main.rs

@@ -5,6 +5,7 @@
 use clap::Parser;
 use patronus::expr::*;
 use patronus::smt::{SmtCommand, read_command, serialize_cmd};
+use patronus_sca::*;
 use rustc_hash::FxHashMap;
 use std::io::{BufReader, BufWriter};
 use std::path::PathBuf;
@@ -17,6 +18,8 @@ use std::path::PathBuf;
 struct Args {
     #[arg(long)]
     do_not_simplify: bool,
+    #[arg(long)]
+    skip_sca: bool,
     #[arg(value_name = "INPUT", index = 1)]
     input_file: PathBuf,
     #[arg(value_name = "OUTPUT", index = 2)]
@@ -45,22 +48,44 @@ fn main() {
         let cmd = if args.do_not_simplify {
             cmd
         } else {
-            simplify(&mut ctx, &mut simplifier, cmd)
+            simplify_cmd(cmd, |e| {
+                let e_after_sca = if args.skip_sca {
+                    e
+                } else {
+                    let p = find_sca_simplification_candidates(&ctx, e);
+                    let subs: FxHashMap<_, _> = p
+                        .into_iter()
+                        .flat_map(|p| match verify_word_level_equality(&mut ctx, p) {
+                            ScaVerifyResult::Equal => Some((p.equality_expr(), ctx.get_true())),
+                            ScaVerifyResult::Unknown => None,
+                            ScaVerifyResult::Unequal(_) => {
+                                Some((p.equality_expr(), ctx.get_false()))
+                            }
+                        })
+                        .collect();
+                    substitute(&mut ctx, e, subs)
+                };
+                simplifier.simplify(&mut ctx, e_after_sca)
+            })
         };
         serialize_cmd(&mut out, Some(&ctx), &cmd).expect("failed to write command");
     }
 }
 
-fn simplify<T: ExprMap<Option<ExprRef>>>(
-    ctx: &mut Context,
-    s: &mut Simplifier<T>,
-    cmd: SmtCommand,
-) -> SmtCommand {
+fn substitute(ctx: &mut Context, e: ExprRef, subs: FxHashMap<ExprRef, ExprRef>) -> ExprRef {
+    if subs.is_empty() {
+        e
+    } else {
+        simple_transform_expr(ctx, e, |_, e, _| subs.get(&e).cloned())
+    }
+}
+
+fn simplify_cmd(cmd: SmtCommand, mut simplify: impl FnMut(ExprRef) -> ExprRef) -> SmtCommand {
     match cmd {
-        SmtCommand::Assert(e) => SmtCommand::Assert(s.simplify(ctx, e)),
-        SmtCommand::DefineConst(sym, value) => SmtCommand::DefineConst(sym, s.simplify(ctx, value)),
+        SmtCommand::Assert(e) => SmtCommand::Assert(simplify(e)),
+        SmtCommand::DefineConst(sym, value) => SmtCommand::DefineConst(sym, simplify(value)),
         SmtCommand::CheckSatAssuming(e) => {
-            SmtCommand::CheckSatAssuming(e.into_iter().map(|e| s.simplify(ctx, e)).collect())
+            SmtCommand::CheckSatAssuming(e.into_iter().map(|e| simplify(e)).collect())
         }
         other => other,
     }