Exponential search / Reasoning horizon

src/cli.rs

@@ -258,6 +258,25 @@ pub fn args() -> Command {
                         .allow_hyphen_values(true)
                         .num_args(1..)
                 )
+                .arg(
+                    Arg::new("stride")
+                        .help("Find unroll level where SMT solver times out")
+                        .short('l')
+                        .long("stride")
+                        .num_args(0)
+                        // TODO: Set base via argument
+                        // .value_name("NUMBER")
+                        // .value_parser(value_parser!(u64)),
+                )
+                .arg(
+                    Arg::new("time-budget")
+                        .help("Set an overall time budget in milliseconds")
+                        .short('g')
+                        .long("time-budget")
+                        .num_args(1)
+                        .value_name("NUMBER")
+                        .value_parser(value_parser!(u64))
+                )
         )
         .subcommand(
             Command::new("qubot")

src/main.rs

@@ -12,18 +12,29 @@ use crate::unicorn::codegen::compile_model_into_program;
 use crate::unicorn::dimacs_parser::load_dimacs_as_gatemodel;
 use crate::unicorn::emulate_loader::load_model_into_emulator;
 use crate::unicorn::memory::replace_memory;
-use crate::unicorn::optimize::{optimize_model_with_input, optimize_model_with_solver};
+// use crate::unicorn::optimize::{
+//     optimize_model_with_input,
+//     optimize_model_with_solver
+// };
 use crate::unicorn::qubot::{InputEvaluator, Qubot};
 use crate::unicorn::sat_solver::solve_bad_states;
-use crate::unicorn::smt_solver::*;
-use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model};
+// use crate::unicorn::smt_solver::*;
+use crate::unicorn::unroller::renumber_model;
 use crate::unicorn::write_model;
+use crate::unicorn::horizon::compute_reasoning_horizon;
 
 use ::unicorn::disassemble::disassemble;
 use ::unicorn::emulate::EmulatorState;
 use anyhow::{Context, Result};
 use bytesize::ByteSize;
-use cli::{collect_arg_values, expect_arg, expect_optional_arg, LogLevel, SatType, SmtType};
+use cli::{
+    collect_arg_values,
+    expect_arg,
+    expect_optional_arg,
+    LogLevel,
+    SatType,
+    SmtType
+};
 use env_logger::{Env, TimestampPrecision};
 use riscu::load_object_file;
 use std::{
@@ -32,7 +43,7 @@ use std::{
     io::{stdout, Write},
     path::PathBuf,
     str::FromStr,
-    time::Duration,
+    time::Duration
 };
 
 fn main() -> Result<()> {
@@ -87,6 +98,8 @@ fn main() -> Result<()> {
             let input_is_dimacs = !is_beator && args.get_flag("from-dimacs");
             let compile_model = is_beator && args.get_flag("compile");
             let emulate_model = is_beator && args.get_flag("emulate");
+            let stride = args.get_flag("stride");
+            let solver_time_budget = args.get_one::<u64>("time-budget");
             let arg0 = expect_arg::<String>(args, "input-file")?;
             let extras = collect_arg_values(args, "extras");
 
@@ -114,32 +127,29 @@ fn main() -> Result<()> {
                     } else {
                         vec![]
                     };
-                    for n in 0..unroll_depth {
-                        unroll_model(&mut model, n);
-                        if has_concrete_inputs {
-                            optimize_model_with_input(&mut model, &mut input_values)
-                        }
-                    }
-                    if prune {
-                        prune_model(&mut model);
-                    }
+
                     let timeout = solver_timeout.map(|&ms| Duration::from_millis(ms));
-                    match smt_solver {
-                        #[rustfmt::skip]
-                        SmtType::Generic => {
-                            optimize_model_with_solver::<none_impl::NoneSolver>(&mut model, timeout, minimize, terminate_on_bad, one_query)
-                        },
-                        #[rustfmt::skip]
-                        #[cfg(feature = "boolector")]
-                        SmtType::Boolector => {
-                            optimize_model_with_solver::<boolector_impl::BoolectorSolver>(&mut model, timeout, minimize, terminate_on_bad, one_query)
-                        },
-                        #[rustfmt::skip]
-                        #[cfg(feature = "z3")]
-                        SmtType::Z3 => {
-                            optimize_model_with_solver::<z3solver_impl::Z3SolverWrapper>(&mut model, timeout, minimize, terminate_on_bad, one_query)
-                        },
-                    }
+
+                    let mut time_budget = solver_time_budget.map(
+                        |&ms| Duration::from_millis(ms)
+                    );
+
+                    // TODO: Refactor the subsequent loop (reasoning horizon)
+                    compute_reasoning_horizon(
+                        &mut model,
+                        has_concrete_inputs,
+                        &mut input_values,
+                        unroll_depth,
+                        prune,
+                        stride,
+                        &smt_solver,
+                        timeout,
+                        minimize,
+                        terminate_on_bad,
+                        one_query,
+                        &mut time_budget
+                    );
+
                     if renumber {
                         renumber_model(&mut model);
                     }

src/unicorn/horizon.rs

@@ -0,0 +1,257 @@
+use crate::unicorn::{Node, NodeRef, Model};
+use crate::cli::{SmtType};
+use crate::unicorn::unroller::{prune_model, unroll_model};
+use crate::unicorn::optimize::{
+    optimize_model_with_input,
+    optimize_model_with_solver,
+    // optimize_model_with_solver_n
+};
+use crate::unicorn::smt_solver::*;
+
+use log::{debug, warn};
+use std::{
+    cmp::min,
+    time::{Duration,Instant}
+};
+
+//
+// Public Interface
+//
+
+pub fn compute_reasoning_horizon(
+    model: &mut Model,
+    has_concrete_inputs: bool,
+    input_values: &mut Vec<u64>,
+    unroll_depth: usize,
+    prune: bool,
+    stride: bool,
+    smt_solver: &SmtType,
+    timeout: Option<Duration>,
+    minimize: bool,
+    terminate_on_bad: bool,
+    one_query: bool,
+    time_budget: &mut Option<Duration>
+) {
+    let has_time_budget = !time_budget.is_none();
+
+    let mut n: usize = if stride { 1 } else { unroll_depth };
+    let mut prev_n: usize = 0;
+
+    let mut exec_time = Duration::from_millis(0);
+
+    loop {
+        // TODO(1): Maybe we can get rid of this clone for each
+        // iteration, which is basically required if pruning is
+        // enabled. However, it is much faster this way than
+        // without pruning and not cloning the model.
+        let (elapsed, bad_states_initial) = reason(
+            &mut model.clone(),
+            has_concrete_inputs,
+            input_values,
+            prev_n,
+            n,
+            prune,
+            stride,
+            &smt_solver,
+            timeout,
+            minimize,
+            terminate_on_bad,
+            one_query
+        );
+
+        exec_time += elapsed;
+
+        if has_time_budget && time_budget.unwrap() < exec_time {
+            exec_time -= elapsed;
+
+            debug!("Time budget exceeded: {:#?} ({:#?}+{:#?}; elapsed time) / {:#?} (time budget)", exec_time+elapsed, exec_time, elapsed, time_budget.unwrap());
+
+            // TODO(2): Cf. TODO(1)
+            let r = reason_backwards(
+                &mut model.clone(),
+                &bad_states_initial,
+                prev_n,
+                n,
+                prune,
+                stride,
+                &smt_solver,
+                timeout,
+                minimize,
+                terminate_on_bad,
+                one_query,
+                &mut(time_budget.unwrap() - exec_time)
+            );
+
+            warn!("Reasoning horizon: depth [n={}] in {:#?} (elapsed time) / {:#?} (time budget)", prev_n + r.0, exec_time + r.1, time_budget.unwrap());
+            break;
+        }
+
+        if !stride || !model.bad_states_initial.is_empty() {
+            if !model.bad_states_initial.is_empty() {
+                print_reasoning_horizon(model);
+            }
+
+            break;
+        }
+
+        if has_time_budget {
+            debug!("Remaining time budget: {:#?} ...", time_budget.unwrap() - exec_time);
+        }
+
+        prev_n = n;
+        n = min(2*n, unroll_depth);
+    }
+}
+
+pub fn reason(
+    model: &mut Model,
+    has_concrete_inputs: bool,
+    input_values: &mut Vec<u64>,
+    start: usize,
+    end: usize,
+    prune: bool,
+    stride: bool,
+    smt_solver: &SmtType,
+    timeout: Option<Duration>,
+    minimize: bool,
+    terminate_on_bad: bool,
+    one_query: bool
+) -> (Duration, Vec<NodeRef>) {
+    let now = Instant::now();
+
+    for m in start..end {
+        unroll_model(model, m);
+
+        if has_concrete_inputs {
+            optimize_model_with_input(model, input_values)
+        }
+    }
+
+    if prune {
+        prune_model(model);
+    }
+
+    let bad_states_initial = model.bad_states_initial.clone();
+
+    match smt_solver {
+        #[rustfmt::skip]
+        SmtType::Generic => {
+            optimize_model_with_solver::<none_impl::NoneSolver>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+        },
+        #[rustfmt::skip]
+        #[cfg(feature = "boolector")]
+        SmtType::Boolector => {
+            optimize_model_with_solver::<boolector_impl::BoolectorSolver>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+        },
+        #[rustfmt::skip]
+        #[cfg(feature = "z3")]
+        SmtType::Z3 => {
+            optimize_model_with_solver::<z3solver_impl::Z3SolverWrapper>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+        },
+    }
+
+    (now.elapsed(), bad_states_initial)
+}
+
+//
+// Private Interface
+//
+
+fn reason_backwards(
+  model: &mut Model,
+  bad_states_initial: &Vec<NodeRef>,
+  prev_n: usize,
+  n: usize,
+  prune: bool,
+  stride: bool,
+  smt_solver: &SmtType,
+  timeout: Option<Duration>,
+  minimize: bool,
+  terminate_on_bad: bool,
+  one_query: bool,
+  time_budget: &mut Duration,
+) -> (usize, Duration) {
+  debug!("Backwards reasoning (binary search) for the last {} bad states ...", bad_states_initial.len());
+
+  if prune {
+      prune_model(model)
+  }
+
+  let mut start: usize = 0;
+  let mut end: usize = n - prev_n;
+
+  let mut exec_n: usize = end;
+  let mut exec_time = Duration::from_millis(0);
+
+  let mut mid: usize = start + (end - start) / 2;
+  let mut prev_mid: usize;
+
+  while start < end {
+      debug!("Trying to fit remaining time budget {:#?} into the last {} steps ({} to {}) ...", time_budget, mid, mid, end);
+
+      let now = Instant::now();
+
+      model.bad_states_initial =
+          bad_states_initial.clone()[mid * 10 .. end * 10].to_vec();
+
+      match smt_solver {
+          #[rustfmt::skip]
+          SmtType::Generic => {
+              optimize_model_with_solver::<none_impl::NoneSolver>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+          },
+          #[rustfmt::skip]
+          #[cfg(feature = "boolector")]
+          SmtType::Boolector => {
+              optimize_model_with_solver::<boolector_impl::BoolectorSolver>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+          },
+          #[rustfmt::skip]
+          #[cfg(feature = "z3")]
+          SmtType::Z3 => {
+              optimize_model_with_solver::<z3solver_impl::Z3SolverWrapper>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+          },
+      }
+
+      let elapsed = now.elapsed();
+
+      if *time_budget > elapsed {
+        end = mid;
+
+        exec_time += elapsed;
+          *time_budget -= elapsed;
+
+          debug!("Elapsed time for the last {} steps: {:#?}", mid, elapsed);
+      } else if *time_budget < elapsed {
+          start = mid;
+
+          exec_n = mid;
+          exec_time = elapsed;
+
+          debug!("Elapsed time for the last {} steps: {:#?}", mid, elapsed);
+      }
+
+      // since we will not find a perfectly fitting time budget (as is the case
+      // in a traditional binary search), we need an additional termination
+      // criterion to avoid endless loops:
+      // We terminate once the pivot does not change anymore.
+      prev_mid = mid;
+      mid = start + (end - start)/2;
+
+      if prev_mid == mid {
+          break;
+      }
+
+  }
+
+  (exec_n, exec_time)
+}
+
+fn print_reasoning_horizon(model: &mut Model) {
+    let v: Option<String>;
+    v = match &*model.bad_states_initial[0].borrow() {
+        Node::Bad { name, ..} => name.clone(),
+        _ => None
+    };
+
+    let bad_state = v.as_ref().expect("Bad state must have an unrolling depth");
+    warn!("(Initial) Bad state '{}' is satisfiable.", bad_state);
+}