From 4f0531d3225b3ae79060414377638b9b4a22d34a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Luk=C3=A1=C5=A1=20Chud=C3=AD=C4=8Dek?= Date: Sat, 30 Sep 2023 16:49:43 +0200 Subject: [PATCH] refactor: able to create valuation conveniently & evaluate UpdateFn in it --- data/dataset.sbml | 6 +- src/prototype/update_fn_bdd.rs | 108 ++++++++++++++++++++++++++++++++- src/symbolic_domain.rs | 6 ++ 3 files changed, 114 insertions(+), 6 deletions(-) diff --git a/data/dataset.sbml b/data/dataset.sbml index 8af14e2..433004b 100644 --- a/data/dataset.sbml +++ b/data/dataset.sbml @@ -306,14 +306,14 @@ qual:id="tr_p53_out" /> - + - + Mdm2nuc - 3 + 0 diff --git a/src/prototype/update_fn_bdd.rs b/src/prototype/update_fn_bdd.rs index 3c51565..f2e10cc 100644 --- a/src/prototype/update_fn_bdd.rs +++ b/src/prototype/update_fn_bdd.rs @@ -2,7 +2,9 @@ use crate::{Expression, SymbolicDomain, UnaryIntegerDomain, UpdateFn}; use std::collections::HashMap; -use biodivine_lib_bdd::{Bdd, BddValuation, BddVariableSet, BddVariableSetBuilder}; +use biodivine_lib_bdd::{ + Bdd, BddPartialValuation, BddValuation, BddVariableSet, BddVariableSetBuilder, +}; use super::expression::Proposition; @@ -116,6 +118,35 @@ impl UpdateFnBdd { .map(|(val, _)| *val) .unwrap_or(self.default) } + + /// returns fully specified valuation representing all the symbolic variables + /// being set to 0 + /// todo maybe useless; get_default_valuation_but_partial is more useful + pub fn get_default_valuation(&self) -> BddValuation { + self.named_symbolic_domains + .values() + .fold(BddPartialValuation::empty(), |mut acc, domain| { + domain.encode_bits(&mut acc, &0); + acc + }) + .try_into() + .unwrap() + } + + /// returns fully specified valuation representing all the symbolic variables + /// being set to 0 + /// but also this valuation is partial, so that it can be updated later + /// since all are set, you can build BddValuation from it at any time and + /// evaluate the update function using this + pub fn get_default_valuation_but_partial(&self) -> BddPartialValuation { + self.named_symbolic_domains.values().fold( + BddPartialValuation::empty(), + |mut acc, domain| { + domain.encode_bits(&mut acc, &0); + acc + }, + ) + } } // todo this should be applied to each term directly while loading the xml; no need to even have the intermediate representation @@ -171,9 +202,75 @@ fn leq( } mod tests { - use biodivine_lib_bdd::{BddPartialValuation, BddValuation}; + use biodivine_lib_bdd::{BddPartialValuation, BddValuation, BddVariableSetBuilder}; - use crate::{SymbolicDomain, UpdateFnBdd}; + use crate::{SymbolicDomain, UnaryIntegerDomain, UpdateFnBdd}; + + #[test] + // yeah more of a playground rather than a test + fn test_valuation_update_symbolic() { + let update_fn: UpdateFnBdd = get_update_fn().into(); + let some_bdd = update_fn.terms[0].1.clone(); + // some_bdd.random_valuation(rng::thread_rng()); + // some_bdd.random_valuation() + + // todo how do i get a valuation i can manipulate with? feel like the bdd api should provide that; something like + // let valuation: &BddValuation = some_bdd.all_false_valuation(); + // let mut new_valuation = some + + // let var_builder = BddVariableSetBuilder::new(); // todo this obj (finished/built) should be available for each UpdateFnBdd so that you can create new valuations + + let default_valuation = update_fn.get_default_valuation(); + println!("default valuation: {:?}", default_valuation); + + // some_bdd.eval_in(&default_valuation); + + let res = update_fn.eval_in(&default_valuation); + println!("res: {}", res); + + let mut updating_valuation = update_fn.get_default_valuation_but_partial(); + update_fn + .named_symbolic_domains + .get("Mdm2nuc") + .unwrap() + .encode_bits(&mut updating_valuation, &1); + println!("valuation updated to 1: {:?}", updating_valuation); + + let res = update_fn.eval_in(&updating_valuation.try_into().unwrap()); + println!("res with valuation of 1: {}", res); + + let mut updating_valuation = update_fn.get_default_valuation_but_partial(); + update_fn + .named_symbolic_domains + .get("Mdm2nuc") + .unwrap() + .encode_bits(&mut updating_valuation, &2); + println!("valuation updated to 2: {:?}", updating_valuation); + + let res = update_fn.eval_in(&updating_valuation.try_into().unwrap()); + println!("res with valuation of 2: {}", res); + + let mut updating_valuation = update_fn.get_default_valuation_but_partial(); + update_fn + .named_symbolic_domains + .get("Mdm2nuc") + .unwrap() + .encode_bits(&mut updating_valuation, &3); + println!("valuation updated to 3: {:?}", updating_valuation); + + let res = update_fn.eval_in(&updating_valuation.try_into().unwrap()); + println!("res with valuation of 3: {}", res); + + let mut updating_valuation = update_fn.get_default_valuation_but_partial(); + update_fn + .named_symbolic_domains + .get("Mdm2nuc") + .unwrap() + .encode_bits(&mut updating_valuation, &100); + + let res = update_fn.eval_in(&updating_valuation.try_into().unwrap()); + println!("res with valuation of 100: {}", res); + } #[test] fn test_update_fn_result() { @@ -228,6 +325,11 @@ mod tests { // update_fn.eval_in(&BddValuation::new(vec![true, true])) // ); + let mut builder = BddVariableSetBuilder::new(); + let sym_val = UnaryIntegerDomain::new(&mut builder, "Mdm2nuc", 2); + let vars = builder.build(); + sym_val.encode_one(&vars, &1); + let valuation = BddValuation::new(vec![false, false]); let accepted = update_fn.terms[0].1.eval_in(&valuation); println!("accepted for valuation {}?: {}", valuation, accepted); diff --git a/src/symbolic_domain.rs b/src/symbolic_domain.rs index 51b1ee8..88d6eb9 100644 --- a/src/symbolic_domain.rs +++ b/src/symbolic_domain.rs @@ -29,6 +29,7 @@ pub trait SymbolicDomain: Clone { /// /// *Contract:* This method only modifies the symbolic variables from /// `Self::symbolic_variables`. No other parts of the `BddPartialValuation` are affected. + /// todo: might want to panic if the input is not in the domain; eg if the value is too big - see unary domain fn encode_bits(&self, bdd_valuation: &mut BddPartialValuation, value: &T); /// Decode a value from the provided `BddPartialValuation`. @@ -182,6 +183,11 @@ impl UnaryIntegerDomain { impl SymbolicDomain for UnaryIntegerDomain { fn encode_bits(&self, bdd_valuation: &mut BddPartialValuation, value: &u8) { + // todo do we want this check here or not? + if value > &(self.variables.len() as u8) { + panic!("Value is too big for this domain") + } + for (i, var) in self.variables.iter().enumerate() { bdd_valuation.set_value(*var, i < (*value as usize)); }