diff --git a/src/main.rs b/src/main.rs index f276d46..ebffe6b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,6 +5,7 @@ mod random; use clap::{arg, Parser}; +use patronus::ir::{replace_anonymous_inputs_with_zero, simplify_expressions}; use patronus::*; use random::*; @@ -27,7 +28,13 @@ static RANDOM_OPTS: RandomOptions = RandomOptions { fn main() { let args = Args::parse(); - let (mut ctx, sys) = btor2::parse_file(&args.filename).expect("Failed to load btor2 file!"); + + // load system + let (mut ctx, mut sys) = btor2::parse_file(&args.filename).expect("Failed to load btor2 file!"); + + // simplify system + replace_anonymous_inputs_with_zero(&mut ctx, &mut sys); + simplify_expressions(&mut ctx, &mut sys); // try random testing match random_testing(&mut ctx, sys, RANDOM_OPTS) { diff --git a/src/random.rs b/src/random.rs index 0093ada..af305ff 100644 --- a/src/random.rs +++ b/src/random.rs @@ -4,7 +4,10 @@ // // Random testing strategy to finding counter examples. -use patronus::ir::{Context, GetNode, SerializableIrNode, TransitionSystem, TypeCheck}; +use patronus::ir::{ + cone_of_influence, cone_of_influence_comb, cone_of_influence_init, Context, ExprRef, GetNode, + SerializableIrNode, TransitionSystem, TypeCheck, +}; use patronus::sim; #[derive(Debug, Copy, Clone)] @@ -28,22 +31,69 @@ pub fn random_testing( let sim_ctx = ctx.clone(); let mut sim = sim::interpreter::Interpreter::new(&sim_ctx, &sys); - // show all inputs - let inputs = sys.get_signals(|s| s.is_input()); - println!("INPUTS:"); - for (expr_ref, input) in inputs.iter() { - let expr = ctx.get(*expr_ref); - println!("{} : {:?}", expr.serialize_to_str(ctx), expr.get_type(ctx)); - } + // // show all inputs + // let inputs = sys.get_signals(|s| s.is_input()); + // println!("INPUTS:"); + // for (expr_ref, input) in inputs.iter() { + // let expr = ctx.get(*expr_ref); + // println!("{} : {:?}", expr.serialize_to_str(ctx), expr.get_type(ctx)); + // } + // + // // show all states + // println!("\nSTATES:"); + // for (state_ref, state) in sys.states() { + // let expr = ctx.get(state.symbol); + // println!("{} : {:?}", expr.serialize_to_str(ctx), expr.get_type(ctx)); + // } - // show all states - println!("\nSTATES:"); - for (state_ref, state) in sys.states() { - let expr = ctx.get(state.symbol); - println!("{} : {:?}", expr.serialize_to_str(ctx), expr.get_type(ctx)); - } + // show system + println!("{}", sys.serialize_to_str(ctx)); + + // analyze constraint dependencies + let constraints = analyze_constraints(ctx, &sys, false); + println!("{constraints:?}"); // TODO RandomResult::None } + +struct Constraints { + /// Single input constraints can be checked when we are sampling the input. + /// The tuple is (constraint ref, input ref) + single_input: Vec<(ExprRef, ExprRef)>, + /// State only constraints which we essentially just need to check once and give up if they fail. + state_only: Vec, + /// All other constraints we currently rejection sample after an input has been chosen. + others: Vec, +} + +#[derive(Debug, Clone)] +struct Constraint { + expr: ExprRef, + inputs: Vec, + states: Vec, +} + +/// Check to see which constraints we can fulfill +fn analyze_constraints(ctx: &Context, sys: &TransitionSystem, init: bool) -> Vec { + let states = sys.state_map(); + let mut out = Vec::new(); + // we want to see which constraints depends on which inputs + for (expr_ref, info) in sys.constraints() { + // + let cone = if init { + cone_of_influence_init(ctx, sys, expr_ref) + } else { + cone_of_influence_comb(ctx, sys, expr_ref) + }; + let (states, inputs) = cone.iter().partition(|e| states.contains_key(e)); + let constraint = Constraint { + expr: expr_ref, + inputs, + states, + }; + out.push(constraint); + } + out +}