From b484399c4fefbe0a60ac61139705bf7eeb6cc91b Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Sun, 13 Mar 2022 13:12:33 +0100 Subject: [PATCH 1/5] freeze --- src/main.rs | 2 ++ src/parser.rs | 27 +++++++++++++++++++++++++-- 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/src/main.rs b/src/main.rs index d287267..289da6e 100644 --- a/src/main.rs +++ b/src/main.rs @@ -211,6 +211,8 @@ fn print_true_vars_recursive( for (i, v) in values.iter().enumerate() { if *v == TruthTableEntry::True { vars_str.push(vars[i].clone()); + } else if *v == TruthTableEntry::Any { + vars_str.push(vars[i].clone() + "*"); } } println!("{};", vars_str.join(", ")); diff --git a/src/parser.rs b/src/parser.rs index b2840e4..3a44774 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -101,6 +101,8 @@ impl ParsedFormula { pub fn new(contents: &mut dyn BufRead) -> io::Result { let tokens = SymbolicBDD::tokenize(contents)?; + let formula = SymbolicBDD::parse_formula(&mut tokens.iter().peekable())?; + let vars = tokens .iter() .filter_map(|t| match t { @@ -108,12 +110,13 @@ impl ParsedFormula { _ => None, }) .unique() + .filter(|v| !formula.var_is_bound(v)) .collect(); - let formula = SymbolicBDD::parse_formula(&mut tokens.iter().peekable())?; + dbg!(&vars); Ok(ParsedFormula { - vars, + vars: vars, bdd: formula, env: RefCell::new(BDDEnv::new()), }) @@ -218,6 +221,26 @@ impl SymbolicBDD { Ok(result) } + // check whether a given variable is bound by a quantifier in the formula + pub fn var_is_bound(&self, var: &String) -> bool { + match self { + SymbolicBDD::Var(v) if v == var => false, + SymbolicBDD::Quantifier(_, vars, f) => { + if !vars.contains(var) { + f.var_is_bound(var) + } else { + false + } + }, + SymbolicBDD::Ite(a, b, c) => a.var_is_bound(var) || b.var_is_bound(var) || c.var_is_bound(var), + SymbolicBDD::Not(f) => f.var_is_bound(var), + SymbolicBDD::BinaryOp(_, a, b) => a.var_is_bound(var) || b.var_is_bound(var), + SymbolicBDD::CountableConst(_, sub, _) => sub.iter().any(|f| f.var_is_bound(var)), + SymbolicBDD::CountableVariable(_, l, r) => l.iter().any(|f| f.var_is_bound(var)) || r.iter().any(|f| f.var_is_bound(var)), + _ => false, + } + } + fn parse_simple_sub_formula(tokens: &mut TokenReader) -> io::Result { match tokens.peek() { Some(SymbolicBDDToken::OpenParen) => SymbolicBDD::parse_parentized_formula(tokens), From 53f5ca418dca7b382ba4a5143bd9a4e5ca21053e Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Sun, 13 Mar 2022 13:38:23 +0100 Subject: [PATCH 2/5] filter free variables --- src/main.rs | 6 +++--- src/parser.rs | 35 +++++++++++++++++++++-------------- 2 files changed, 24 insertions(+), 17 deletions(-) diff --git a/src/main.rs b/src/main.rs index 289da6e..4c5c52d 100644 --- a/src/main.rs +++ b/src/main.rs @@ -97,7 +97,7 @@ fn main() { print_truth_table_recursive( &result, input_parsed - .vars + .free_vars .iter() .map(|_| TruthTableEntry::Any) .collect(), @@ -109,11 +109,11 @@ fn main() { print_true_vars_recursive( &result, input_parsed - .vars + .free_vars .iter() .map(|_| TruthTableEntry::Any) .collect(), - &input_parsed.vars, + &input_parsed.free_vars, ); } diff --git a/src/parser.rs b/src/parser.rs index 3a44774..9df13a2 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -91,6 +91,7 @@ pub enum SymbolicBDD { #[derive(Debug, Clone)] pub struct ParsedFormula { pub vars: Vec, + pub free_vars: Vec, pub bdd: SymbolicBDD, pub env: RefCell>, } @@ -103,20 +104,22 @@ impl ParsedFormula { let formula = SymbolicBDD::parse_formula(&mut tokens.iter().peekable())?; - let vars = tokens + let vars: Vec = tokens .iter() .filter_map(|t| match t { SymbolicBDDToken::Var(v) => Some(v.clone()), _ => None, }) .unique() - .filter(|v| !formula.var_is_bound(v)) .collect(); - dbg!(&vars); - Ok(ParsedFormula { - vars: vars, + vars: vars.clone(), + free_vars: vars + .iter() + .filter(|v| formula.var_is_free(v)) + .cloned() + .collect(), bdd: formula, env: RefCell::new(BDDEnv::new()), }) @@ -222,21 +225,25 @@ impl SymbolicBDD { } // check whether a given variable is bound by a quantifier in the formula - pub fn var_is_bound(&self, var: &String) -> bool { + pub fn var_is_free(&self, var: &String) -> bool { match self { - SymbolicBDD::Var(v) if v == var => false, + SymbolicBDD::Var(v) if v == var => true, SymbolicBDD::Quantifier(_, vars, f) => { if !vars.contains(var) { - f.var_is_bound(var) + f.var_is_free(var) } else { false } - }, - SymbolicBDD::Ite(a, b, c) => a.var_is_bound(var) || b.var_is_bound(var) || c.var_is_bound(var), - SymbolicBDD::Not(f) => f.var_is_bound(var), - SymbolicBDD::BinaryOp(_, a, b) => a.var_is_bound(var) || b.var_is_bound(var), - SymbolicBDD::CountableConst(_, sub, _) => sub.iter().any(|f| f.var_is_bound(var)), - SymbolicBDD::CountableVariable(_, l, r) => l.iter().any(|f| f.var_is_bound(var)) || r.iter().any(|f| f.var_is_bound(var)), + } + SymbolicBDD::Ite(a, b, c) => { + a.var_is_free(var) || b.var_is_free(var) || c.var_is_free(var) + } + SymbolicBDD::Not(f) => f.var_is_free(var), + SymbolicBDD::BinaryOp(_, a, b) => a.var_is_free(var) || b.var_is_free(var), + SymbolicBDD::CountableConst(_, sub, _) => sub.iter().any(|f| f.var_is_free(var)), + SymbolicBDD::CountableVariable(_, l, r) => { + l.iter().any(|f| f.var_is_free(var)) || r.iter().any(|f| f.var_is_free(var)) + } _ => false, } } From a2c0cfc5c0188f36b30caf8ab29f7e6a49ff6eb8 Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Sun, 13 Mar 2022 15:32:54 +0100 Subject: [PATCH 3/5] add end-to-end cliques test --- tests/parser_test.rs | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/tests/parser_test.rs b/tests/parser_test.rs index 42a78bb..9c6755c 100644 --- a/tests/parser_test.rs +++ b/tests/parser_test.rs @@ -129,3 +129,45 @@ fn test_4_queens_file() -> io::Result<()> { Ok(()) } + +#[test] +fn test_cliques_file() -> io::Result<()> { + let input_file = File::open("examples/cliques.txt").expect("Could not open input file"); + + let input_parsed = + ParsedFormula::new(&mut BufReader::new(input_file)).expect("Could not parse input file"); + + let input_evaluated = input_parsed.eval(); + + let model = input_parsed.env.borrow().model(input_evaluated.clone()); + + let var_map: Vec<(String, (bool, bool))> = input_parsed + .free_vars + .iter() + .map(|v| { + ( + v.clone(), + input_parsed + .env + .borrow() + .infer(model.clone(), input_parsed.name2var(v)), + ) + }) + .collect(); + + dbg!(&var_map); + + let reference: Vec<(String, (bool, bool))> = vec![ + ("a".to_string(), (false, false)), + ("f".to_string(), (true, true)), + ("g".to_string(), (true, true)), + ("b".to_string(), (false, false)), + ("d".to_string(), (true, true)), + ("e".to_string(), (true, true)), + ("c".to_string(), (false, false)), + ]; + + assert_eq!(var_map, reference); + + Ok(()) +} From ce71744ec95b7635b7cae1bff50629d840f7c52a Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Sun, 13 Mar 2022 15:34:31 +0100 Subject: [PATCH 4/5] add simplified songfestival example showing all cliques --- examples/songfestival_all.txt | 1610 +++++++++++++++++++++++++++++++++ 1 file changed, 1610 insertions(+) create mode 100644 examples/songfestival_all.txt diff --git a/examples/songfestival_all.txt b/examples/songfestival_all.txt new file mode 100644 index 0000000..e4d2f5e --- /dev/null +++ b/examples/songfestival_all.txt @@ -0,0 +1,1610 @@ +"Generated by max-clique-gen version 0.5.1" + +"Property: if two vertices are in a clique, then they should be connected." +"Property: if two vertices are not connected, they cannot be in the same clique." + +-(Germany & Ireland) & +-(Germany & France) & +-(Germany & Switzerland) & +-(Germany & United_Kingdom) & +-(Germany & Slovakia) & +-(Germany & Macedonia) & +-(Germany & Hungary) & +-(Germany & Sweden) & +-(Germany & Portugal) & +-(Germany & Montenegro) & +-(Germany & Monaco) & +-(Germany & Albania) & +-(Germany & Spain) & +-(Germany & Armenia) & +-(Germany & Bosnia_and_Herzegovina) & +-(Germany & Azerbaijan) & +-(Germany & Romania) & +-(Germany & Ukraine) & +-(Germany & Israel) & +-(Germany & Bulgaria) & +-(Germany & Russia) & +-(Germany & Belarus) & +-(Germany & Austria) & +-(Germany & Cyprus) & +-(Germany & Iceland) & +-(Germany & Czech_Republic) & +-(Germany & Moldova) & +-(Germany & Lithuania) & +-(Germany & San_Marino) & +-(Germany & Georgia) & +-(Germany & Slovenia) & +-(Germany & Netherlands) & +-(Germany & Andorra) & +-(Ireland & Germany) & +-(Ireland & France) & +-(Ireland & Switzerland) & +-(Ireland & Slovakia) & +-(Ireland & Macedonia) & +-(Ireland & Hungary) & +-(Ireland & Portugal) & +-(Ireland & Montenegro) & +-(Ireland & Monaco) & +-(Ireland & Albania) & +-(Ireland & Spain) & +-(Ireland & Bosnia_and_Herzegovina) & +-(Ireland & Azerbaijan) & +-(Ireland & Romania) & +-(Ireland & Turkey) & +-(Ireland & Serbia) & +-(Ireland & Ukraine) & +-(Ireland & Israel) & +-(Ireland & Bulgaria) & +-(Ireland & Belarus) & +-(Ireland & Greece) & +-(Ireland & Austria) & +-(Ireland & Croatia) & +-(Ireland & Czech_Republic) & +-(Ireland & Moldova) & +-(Ireland & San_Marino) & +-(Ireland & Georgia) & +-(Ireland & Andorra) & +-(Denmark & Ireland) & +-(Denmark & France) & +-(Denmark & Switzerland) & +-(Denmark & United_Kingdom) & +-(Denmark & Slovakia) & +-(Denmark & Macedonia) & +-(Denmark & Hungary) & +-(Denmark & Portugal) & +-(Denmark & Montenegro) & +-(Denmark & Monaco) & +-(Denmark & Albania) & +-(Denmark & Spain) & +-(Denmark & Latvia) & +-(Denmark & Armenia) & +-(Denmark & Bosnia_and_Herzegovina) & +-(Denmark & Azerbaijan) & +-(Denmark & Romania) & +-(Denmark & Serbia) & +-(Denmark & Ukraine) & +-(Denmark & Israel) & +-(Denmark & Bulgaria) & +-(Denmark & Russia) & +-(Denmark & Belarus) & +-(Denmark & Greece) & +-(Denmark & Austria) & +-(Denmark & Poland) & +-(Denmark & Cyprus) & +-(Denmark & Croatia) & +-(Denmark & Czech_Republic) & +-(Denmark & Estonia) & +-(Denmark & Moldova) & +-(Denmark & Lithuania) & +-(Denmark & San_Marino) & +-(Denmark & Georgia) & +-(Denmark & Slovenia) & +-(Denmark & Netherlands) & +-(Denmark & Andorra) & +-(France & Ireland) & +-(France & Denmark) & +-(France & Switzerland) & +-(France & United_Kingdom) & +-(France & Slovakia) & +-(France & Finland) & +-(France & Macedonia) & +-(France & Hungary) & +-(France & Sweden) & +-(France & Montenegro) & +-(France & Monaco) & +-(France & Albania) & +-(France & Latvia) & +-(France & Bosnia_and_Herzegovina) & +-(France & Azerbaijan) & +-(France & Romania) & +-(France & Ukraine) & +-(France & Norway) & +-(France & Bulgaria) & +-(France & Russia) & +-(France & Belarus) & +-(France & Greece) & +-(France & Austria) & +-(France & Poland) & +-(France & Cyprus) & +-(France & Croatia) & +-(France & Malta) & +-(France & Iceland) & +-(France & Czech_Republic) & +-(France & Estonia) & +-(France & Moldova) & +-(France & Lithuania) & +-(France & San_Marino) & +-(France & Georgia) & +-(France & Slovenia) & +-(France & Netherlands) & +-(France & Andorra) & +-(Switzerland & Ireland) & +-(Switzerland & United_Kingdom) & +-(Switzerland & Slovakia) & +-(Switzerland & Finland) & +-(Switzerland & Macedonia) & +-(Switzerland & Hungary) & +-(Switzerland & Sweden) & +-(Switzerland & Monaco) & +-(Switzerland & Latvia) & +-(Switzerland & Armenia) & +-(Switzerland & Azerbaijan) & +-(Switzerland & Romania) & +-(Switzerland & Ukraine) & +-(Switzerland & Norway) & +-(Switzerland & Bulgaria) & +-(Switzerland & Russia) & +-(Switzerland & Belarus) & +-(Switzerland & Greece) & +-(Switzerland & Austria) & +-(Switzerland & Poland) & +-(Switzerland & Cyprus) & +-(Switzerland & Croatia) & +-(Switzerland & Malta) & +-(Switzerland & Iceland) & +-(Switzerland & Czech_Republic) & +-(Switzerland & Estonia) & +-(Switzerland & Moldova) & +-(Switzerland & Lithuania) & +-(Switzerland & San_Marino) & +-(Switzerland & Georgia) & +-(Switzerland & Belgium) & +-(Switzerland & Slovenia) & +-(Switzerland & Netherlands) & +-(Switzerland & Andorra) & +-(United_Kingdom & Germany) & +-(United_Kingdom & Switzerland) & +-(United_Kingdom & Slovakia) & +-(United_Kingdom & Macedonia) & +-(United_Kingdom & Hungary) & +-(United_Kingdom & Portugal) & +-(United_Kingdom & Montenegro) & +-(United_Kingdom & Monaco) & +-(United_Kingdom & Albania) & +-(United_Kingdom & Spain) & +-(United_Kingdom & Armenia) & +-(United_Kingdom & Bosnia_and_Herzegovina) & +-(United_Kingdom & Azerbaijan) & +-(United_Kingdom & Romania) & +-(United_Kingdom & Serbia) & +-(United_Kingdom & Ukraine) & +-(United_Kingdom & Israel) & +-(United_Kingdom & Bulgaria) & +-(United_Kingdom & Russia) & +-(United_Kingdom & Belarus) & +-(United_Kingdom & Austria) & +-(United_Kingdom & Poland) & +-(United_Kingdom & Croatia) & +-(United_Kingdom & Czech_Republic) & +-(United_Kingdom & Moldova) & +-(United_Kingdom & San_Marino) & +-(United_Kingdom & Georgia) & +-(United_Kingdom & Belgium) & +-(United_Kingdom & Slovenia) & +-(United_Kingdom & Andorra) & +-(Slovakia & Ireland) & +-(Slovakia & Denmark) & +-(Slovakia & France) & +-(Slovakia & Switzerland) & +-(Slovakia & United_Kingdom) & +-(Slovakia & Finland) & +-(Slovakia & Macedonia) & +-(Slovakia & Hungary) & +-(Slovakia & Sweden) & +-(Slovakia & Portugal) & +-(Slovakia & Montenegro) & +-(Slovakia & Monaco) & +-(Slovakia & Albania) & +-(Slovakia & Spain) & +-(Slovakia & Latvia) & +-(Slovakia & Armenia) & +-(Slovakia & Bosnia_and_Herzegovina) & +-(Slovakia & Azerbaijan) & +-(Slovakia & Romania) & +-(Slovakia & Turkey) & +-(Slovakia & Serbia) & +-(Slovakia & Ukraine) & +-(Slovakia & Israel) & +-(Slovakia & Bulgaria) & +-(Slovakia & Russia) & +-(Slovakia & Belarus) & +-(Slovakia & Greece) & +-(Slovakia & Austria) & +-(Slovakia & Poland) & +-(Slovakia & Cyprus) & +-(Slovakia & Iceland) & +-(Slovakia & Czech_Republic) & +-(Slovakia & Moldova) & +-(Slovakia & Lithuania) & +-(Slovakia & San_Marino) & +-(Slovakia & Georgia) & +-(Slovakia & Slovenia) & +-(Slovakia & Netherlands) & +-(Slovakia & Andorra) & +-(Finland & Ireland) & +-(Finland & United_Kingdom) & +-(Finland & Slovakia) & +-(Finland & Macedonia) & +-(Finland & Portugal) & +-(Finland & Monaco) & +-(Finland & Albania) & +-(Finland & Spain) & +-(Finland & Armenia) & +-(Finland & Azerbaijan) & +-(Finland & Romania) & +-(Finland & Turkey) & +-(Finland & Ukraine) & +-(Finland & Bulgaria) & +-(Finland & Belarus) & +-(Finland & Greece) & +-(Finland & Austria) & +-(Finland & Poland) & +-(Finland & Cyprus) & +-(Finland & Croatia) & +-(Finland & Malta) & +-(Finland & Czech_Republic) & +-(Finland & Moldova) & +-(Finland & Lithuania) & +-(Finland & San_Marino) & +-(Finland & Georgia) & +-(Finland & Belgium) & +-(Finland & Slovenia) & +-(Finland & Netherlands) & +-(Finland & Andorra) & +-(Macedonia & Germany) & +-(Macedonia & Ireland) & +-(Macedonia & Denmark) & +-(Macedonia & France) & +-(Macedonia & Switzerland) & +-(Macedonia & Slovakia) & +-(Macedonia & Finland) & +-(Macedonia & Hungary) & +-(Macedonia & Sweden) & +-(Macedonia & Portugal) & +-(Macedonia & Monaco) & +-(Macedonia & Spain) & +-(Macedonia & Latvia) & +-(Macedonia & Armenia) & +-(Macedonia & Azerbaijan) & +-(Macedonia & Ukraine) & +-(Macedonia & Israel) & +-(Macedonia & Norway) & +-(Macedonia & Bulgaria) & +-(Macedonia & Russia) & +-(Macedonia & Belarus) & +-(Macedonia & Greece) & +-(Macedonia & Austria) & +-(Macedonia & Poland) & +-(Macedonia & Cyprus) & +-(Macedonia & Iceland) & +-(Macedonia & Czech_Republic) & +-(Macedonia & Estonia) & +-(Macedonia & Moldova) & +-(Macedonia & Lithuania) & +-(Macedonia & San_Marino) & +-(Macedonia & Georgia) & +-(Macedonia & Belgium) & +-(Macedonia & Slovenia) & +-(Macedonia & Netherlands) & +-(Macedonia & Andorra) & +-(Hungary & Germany) & +-(Hungary & Ireland) & +-(Hungary & France) & +-(Hungary & Switzerland) & +-(Hungary & Slovakia) & +-(Hungary & Finland) & +-(Hungary & Macedonia) & +-(Hungary & Sweden) & +-(Hungary & Portugal) & +-(Hungary & Montenegro) & +-(Hungary & Monaco) & +-(Hungary & Albania) & +-(Hungary & Spain) & +-(Hungary & Latvia) & +-(Hungary & Armenia) & +-(Hungary & Bosnia_and_Herzegovina) & +-(Hungary & Turkey) & +-(Hungary & Ukraine) & +-(Hungary & Israel) & +-(Hungary & Belarus) & +-(Hungary & Austria) & +-(Hungary & Poland) & +-(Hungary & Cyprus) & +-(Hungary & Croatia) & +-(Hungary & Malta) & +-(Hungary & Iceland) & +-(Hungary & Czech_Republic) & +-(Hungary & Estonia) & +-(Hungary & Moldova) & +-(Hungary & Lithuania) & +-(Hungary & San_Marino) & +-(Hungary & Georgia) & +-(Hungary & Slovenia) & +-(Hungary & Andorra) & +-(Sweden & Ireland) & +-(Sweden & France) & +-(Sweden & Switzerland) & +-(Sweden & United_Kingdom) & +-(Sweden & Slovakia) & +-(Sweden & Macedonia) & +-(Sweden & Hungary) & +-(Sweden & Portugal) & +-(Sweden & Monaco) & +-(Sweden & Albania) & +-(Sweden & Spain) & +-(Sweden & Armenia) & +-(Sweden & Azerbaijan) & +-(Sweden & Turkey) & +-(Sweden & Israel) & +-(Sweden & Bulgaria) & +-(Sweden & Russia) & +-(Sweden & Belarus) & +-(Sweden & Austria) & +-(Sweden & Poland) & +-(Sweden & Cyprus) & +-(Sweden & Croatia) & +-(Sweden & Malta) & +-(Sweden & Czech_Republic) & +-(Sweden & Moldova) & +-(Sweden & Lithuania) & +-(Sweden & San_Marino) & +-(Sweden & Georgia) & +-(Sweden & Belgium) & +-(Sweden & Slovenia) & +-(Sweden & Netherlands) & +-(Sweden & Andorra) & +-(Portugal & Ireland) & +-(Portugal & Denmark) & +-(Portugal & Switzerland) & +-(Portugal & Slovakia) & +-(Portugal & Finland) & +-(Portugal & Macedonia) & +-(Portugal & Hungary) & +-(Portugal & Montenegro) & +-(Portugal & Monaco) & +-(Portugal & Albania) & +-(Portugal & Latvia) & +-(Portugal & Armenia) & +-(Portugal & Bosnia_and_Herzegovina) & +-(Portugal & Azerbaijan) & +-(Portugal & Turkey) & +-(Portugal & Serbia) & +-(Portugal & Norway) & +-(Portugal & Bulgaria) & +-(Portugal & Russia) & +-(Portugal & Belarus) & +-(Portugal & Greece) & +-(Portugal & Poland) & +-(Portugal & Cyprus) & +-(Portugal & Croatia) & +-(Portugal & Malta) & +-(Portugal & Iceland) & +-(Portugal & Czech_Republic) & +-(Portugal & Estonia) & +-(Portugal & Lithuania) & +-(Portugal & San_Marino) & +-(Portugal & Georgia) & +-(Portugal & Belgium) & +-(Portugal & Slovenia) & +-(Portugal & Netherlands) & +-(Portugal & Andorra) & +-(Montenegro & Germany) & +-(Montenegro & Ireland) & +-(Montenegro & Denmark) & +-(Montenegro & France) & +-(Montenegro & Switzerland) & +-(Montenegro & United_Kingdom) & +-(Montenegro & Slovakia) & +-(Montenegro & Finland) & +-(Montenegro & Hungary) & +-(Montenegro & Sweden) & +-(Montenegro & Portugal) & +-(Montenegro & Monaco) & +-(Montenegro & Albania) & +-(Montenegro & Spain) & +-(Montenegro & Latvia) & +-(Montenegro & Armenia) & +-(Montenegro & Azerbaijan) & +-(Montenegro & Romania) & +-(Montenegro & Turkey) & +-(Montenegro & Ukraine) & +-(Montenegro & Israel) & +-(Montenegro & Bulgaria) & +-(Montenegro & Russia) & +-(Montenegro & Belarus) & +-(Montenegro & Austria) & +-(Montenegro & Poland) & +-(Montenegro & Cyprus) & +-(Montenegro & Malta) & +-(Montenegro & Iceland) & +-(Montenegro & Czech_Republic) & +-(Montenegro & Estonia) & +-(Montenegro & Moldova) & +-(Montenegro & Lithuania) & +-(Montenegro & San_Marino) & +-(Montenegro & Georgia) & +-(Montenegro & Belgium) & +-(Montenegro & Slovenia) & +-(Montenegro & Netherlands) & +-(Montenegro & Andorra) & +-(Monaco & Germany) & +-(Monaco & Switzerland) & +-(Monaco & United_Kingdom) & +-(Monaco & Slovakia) & +-(Monaco & Finland) & +-(Monaco & Macedonia) & +-(Monaco & Hungary) & +-(Monaco & Sweden) & +-(Monaco & Portugal) & +-(Monaco & Montenegro) & +-(Monaco & Albania) & +-(Monaco & Spain) & +-(Monaco & Latvia) & +-(Monaco & Armenia) & +-(Monaco & Azerbaijan) & +-(Monaco & Romania) & +-(Monaco & Turkey) & +-(Monaco & Serbia) & +-(Monaco & Ukraine) & +-(Monaco & Norway) & +-(Monaco & Bulgaria) & +-(Monaco & Russia) & +-(Monaco & Belarus) & +-(Monaco & Austria) & +-(Monaco & Poland) & +-(Monaco & Cyprus) & +-(Monaco & Croatia) & +-(Monaco & Malta) & +-(Monaco & Iceland) & +-(Monaco & Czech_Republic) & +-(Monaco & Estonia) & +-(Monaco & Moldova) & +-(Monaco & Lithuania) & +-(Monaco & San_Marino) & +-(Monaco & Georgia) & +-(Monaco & Belgium) & +-(Monaco & Slovenia) & +-(Monaco & Netherlands) & +-(Monaco & Andorra) & +-(Albania & Ireland) & +-(Albania & Denmark) & +-(Albania & France) & +-(Albania & Switzerland) & +-(Albania & United_Kingdom) & +-(Albania & Slovakia) & +-(Albania & Finland) & +-(Albania & Hungary) & +-(Albania & Portugal) & +-(Albania & Montenegro) & +-(Albania & Monaco) & +-(Albania & Latvia) & +-(Albania & Armenia) & +-(Albania & Azerbaijan) & +-(Albania & Romania) & +-(Albania & Serbia) & +-(Albania & Ukraine) & +-(Albania & Israel) & +-(Albania & Norway) & +-(Albania & Bulgaria) & +-(Albania & Russia) & +-(Albania & Belarus) & +-(Albania & Austria) & +-(Albania & Poland) & +-(Albania & Cyprus) & +-(Albania & Croatia) & +-(Albania & Malta) & +-(Albania & Iceland) & +-(Albania & Czech_Republic) & +-(Albania & Estonia) & +-(Albania & Moldova) & +-(Albania & Lithuania) & +-(Albania & San_Marino) & +-(Albania & Georgia) & +-(Albania & Belgium) & +-(Albania & Slovenia) & +-(Albania & Netherlands) & +-(Albania & Andorra) & +-(Spain & Ireland) & +-(Spain & France) & +-(Spain & Switzerland) & +-(Spain & Slovakia) & +-(Spain & Macedonia) & +-(Spain & Hungary) & +-(Spain & Sweden) & +-(Spain & Portugal) & +-(Spain & Montenegro) & +-(Spain & Monaco) & +-(Spain & Albania) & +-(Spain & Bosnia_and_Herzegovina) & +-(Spain & Azerbaijan) & +-(Spain & Turkey) & +-(Spain & Serbia) & +-(Spain & Ukraine) & +-(Spain & Russia) & +-(Spain & Belarus) & +-(Spain & Austria) & +-(Spain & Poland) & +-(Spain & Cyprus) & +-(Spain & Czech_Republic) & +-(Spain & Estonia) & +-(Spain & Moldova) & +-(Spain & Lithuania) & +-(Spain & San_Marino) & +-(Spain & Georgia) & +-(Spain & Slovenia) & +-(Spain & Netherlands) & +-(Spain & Andorra) & +-(Latvia & Ireland) & +-(Latvia & France) & +-(Latvia & United_Kingdom) & +-(Latvia & Slovakia) & +-(Latvia & Finland) & +-(Latvia & Macedonia) & +-(Latvia & Hungary) & +-(Latvia & Sweden) & +-(Latvia & Portugal) & +-(Latvia & Montenegro) & +-(Latvia & Monaco) & +-(Latvia & Albania) & +-(Latvia & Spain) & +-(Latvia & Armenia) & +-(Latvia & Bosnia_and_Herzegovina) & +-(Latvia & Azerbaijan) & +-(Latvia & Romania) & +-(Latvia & Turkey) & +-(Latvia & Serbia) & +-(Latvia & Israel) & +-(Latvia & Bulgaria) & +-(Latvia & Belarus) & +-(Latvia & Greece) & +-(Latvia & Austria) & +-(Latvia & Poland) & +-(Latvia & Cyprus) & +-(Latvia & Croatia) & +-(Latvia & Malta) & +-(Latvia & Iceland) & +-(Latvia & Czech_Republic) & +-(Latvia & Moldova) & +-(Latvia & San_Marino) & +-(Latvia & Georgia) & +-(Latvia & Slovenia) & +-(Latvia & Netherlands) & +-(Latvia & Andorra) & +-(Armenia & Germany) & +-(Armenia & Ireland) & +-(Armenia & Denmark) & +-(Armenia & France) & +-(Armenia & Switzerland) & +-(Armenia & United_Kingdom) & +-(Armenia & Slovakia) & +-(Armenia & Finland) & +-(Armenia & Macedonia) & +-(Armenia & Hungary) & +-(Armenia & Sweden) & +-(Armenia & Portugal) & +-(Armenia & Montenegro) & +-(Armenia & Monaco) & +-(Armenia & Albania) & +-(Armenia & Spain) & +-(Armenia & Latvia) & +-(Armenia & Bosnia_and_Herzegovina) & +-(Armenia & Azerbaijan) & +-(Armenia & Romania) & +-(Armenia & Turkey) & +-(Armenia & Serbia) & +-(Armenia & Israel) & +-(Armenia & Norway) & +-(Armenia & Bulgaria) & +-(Armenia & Austria) & +-(Armenia & Poland) & +-(Armenia & Cyprus) & +-(Armenia & Croatia) & +-(Armenia & Malta) & +-(Armenia & Iceland) & +-(Armenia & Czech_Republic) & +-(Armenia & Estonia) & +-(Armenia & Moldova) & +-(Armenia & Lithuania) & +-(Armenia & San_Marino) & +-(Armenia & Belgium) & +-(Armenia & Slovenia) & +-(Armenia & Netherlands) & +-(Armenia & Andorra) & +-(Bosnia_and_Herzegovina & Ireland) & +-(Bosnia_and_Herzegovina & Denmark) & +-(Bosnia_and_Herzegovina & Switzerland) & +-(Bosnia_and_Herzegovina & United_Kingdom) & +-(Bosnia_and_Herzegovina & Slovakia) & +-(Bosnia_and_Herzegovina & Finland) & +-(Bosnia_and_Herzegovina & Macedonia) & +-(Bosnia_and_Herzegovina & Hungary) & +-(Bosnia_and_Herzegovina & Portugal) & +-(Bosnia_and_Herzegovina & Monaco) & +-(Bosnia_and_Herzegovina & Albania) & +-(Bosnia_and_Herzegovina & Spain) & +-(Bosnia_and_Herzegovina & Latvia) & +-(Bosnia_and_Herzegovina & Armenia) & +-(Bosnia_and_Herzegovina & Azerbaijan) & +-(Bosnia_and_Herzegovina & Romania) & +-(Bosnia_and_Herzegovina & Ukraine) & +-(Bosnia_and_Herzegovina & Israel) & +-(Bosnia_and_Herzegovina & Bulgaria) & +-(Bosnia_and_Herzegovina & Russia) & +-(Bosnia_and_Herzegovina & Belarus) & +-(Bosnia_and_Herzegovina & Greece) & +-(Bosnia_and_Herzegovina & Austria) & +-(Bosnia_and_Herzegovina & Poland) & +-(Bosnia_and_Herzegovina & Cyprus) & +-(Bosnia_and_Herzegovina & Malta) & +-(Bosnia_and_Herzegovina & Iceland) & +-(Bosnia_and_Herzegovina & Czech_Republic) & +-(Bosnia_and_Herzegovina & Moldova) & +-(Bosnia_and_Herzegovina & Lithuania) & +-(Bosnia_and_Herzegovina & San_Marino) & +-(Bosnia_and_Herzegovina & Georgia) & +-(Bosnia_and_Herzegovina & Netherlands) & +-(Bosnia_and_Herzegovina & Andorra) & +-(Azerbaijan & Germany) & +-(Azerbaijan & Ireland) & +-(Azerbaijan & Denmark) & +-(Azerbaijan & France) & +-(Azerbaijan & Switzerland) & +-(Azerbaijan & United_Kingdom) & +-(Azerbaijan & Slovakia) & +-(Azerbaijan & Finland) & +-(Azerbaijan & Macedonia) & +-(Azerbaijan & Hungary) & +-(Azerbaijan & Sweden) & +-(Azerbaijan & Portugal) & +-(Azerbaijan & Montenegro) & +-(Azerbaijan & Monaco) & +-(Azerbaijan & Albania) & +-(Azerbaijan & Spain) & +-(Azerbaijan & Latvia) & +-(Azerbaijan & Armenia) & +-(Azerbaijan & Bosnia_and_Herzegovina) & +-(Azerbaijan & Romania) & +-(Azerbaijan & Serbia) & +-(Azerbaijan & Israel) & +-(Azerbaijan & Norway) & +-(Azerbaijan & Bulgaria) & +-(Azerbaijan & Russia) & +-(Azerbaijan & Belarus) & +-(Azerbaijan & Greece) & +-(Azerbaijan & Austria) & +-(Azerbaijan & Poland) & +-(Azerbaijan & Cyprus) & +-(Azerbaijan & Croatia) & +-(Azerbaijan & Malta) & +-(Azerbaijan & Iceland) & +-(Azerbaijan & Czech_Republic) & +-(Azerbaijan & Estonia) & +-(Azerbaijan & Moldova) & +-(Azerbaijan & Lithuania) & +-(Azerbaijan & San_Marino) & +-(Azerbaijan & Georgia) & +-(Azerbaijan & Belgium) & +-(Azerbaijan & Slovenia) & +-(Azerbaijan & Netherlands) & +-(Azerbaijan & Andorra) & +-(Romania & Germany) & +-(Romania & Ireland) & +-(Romania & France) & +-(Romania & Switzerland) & +-(Romania & Slovakia) & +-(Romania & Finland) & +-(Romania & Hungary) & +-(Romania & Portugal) & +-(Romania & Montenegro) & +-(Romania & Monaco) & +-(Romania & Albania) & +-(Romania & Spain) & +-(Romania & Latvia) & +-(Romania & Armenia) & +-(Romania & Bosnia_and_Herzegovina) & +-(Romania & Azerbaijan) & +-(Romania & Serbia) & +-(Romania & Ukraine) & +-(Romania & Israel) & +-(Romania & Norway) & +-(Romania & Bulgaria) & +-(Romania & Belarus) & +-(Romania & Austria) & +-(Romania & Cyprus) & +-(Romania & Croatia) & +-(Romania & Malta) & +-(Romania & Czech_Republic) & +-(Romania & Estonia) & +-(Romania & Lithuania) & +-(Romania & San_Marino) & +-(Romania & Georgia) & +-(Romania & Belgium) & +-(Romania & Slovenia) & +-(Romania & Netherlands) & +-(Romania & Andorra) & +-(Turkey & Ireland) & +-(Turkey & Denmark) & +-(Turkey & France) & +-(Turkey & Switzerland) & +-(Turkey & Slovakia) & +-(Turkey & Finland) & +-(Turkey & Macedonia) & +-(Turkey & Hungary) & +-(Turkey & Portugal) & +-(Turkey & Montenegro) & +-(Turkey & Monaco) & +-(Turkey & Spain) & +-(Turkey & Latvia) & +-(Turkey & Romania) & +-(Turkey & Serbia) & +-(Turkey & Israel) & +-(Turkey & Bulgaria) & +-(Turkey & Belarus) & +-(Turkey & Poland) & +-(Turkey & Cyprus) & +-(Turkey & Czech_Republic) & +-(Turkey & Moldova) & +-(Turkey & Lithuania) & +-(Turkey & San_Marino) & +-(Turkey & Georgia) & +-(Turkey & Slovenia) & +-(Turkey & Netherlands) & +-(Turkey & Andorra) & +-(Serbia & Germany) & +-(Serbia & Ireland) & +-(Serbia & Denmark) & +-(Serbia & France) & +-(Serbia & Switzerland) & +-(Serbia & United_Kingdom) & +-(Serbia & Slovakia) & +-(Serbia & Finland) & +-(Serbia & Sweden) & +-(Serbia & Portugal) & +-(Serbia & Montenegro) & +-(Serbia & Monaco) & +-(Serbia & Albania) & +-(Serbia & Spain) & +-(Serbia & Latvia) & +-(Serbia & Armenia) & +-(Serbia & Azerbaijan) & +-(Serbia & Romania) & +-(Serbia & Turkey) & +-(Serbia & Israel) & +-(Serbia & Bulgaria) & +-(Serbia & Belarus) & +-(Serbia & Austria) & +-(Serbia & Poland) & +-(Serbia & Cyprus) & +-(Serbia & Malta) & +-(Serbia & Iceland) & +-(Serbia & Czech_Republic) & +-(Serbia & Estonia) & +-(Serbia & Moldova) & +-(Serbia & Lithuania) & +-(Serbia & San_Marino) & +-(Serbia & Georgia) & +-(Serbia & Belgium) & +-(Serbia & Slovenia) & +-(Serbia & Netherlands) & +-(Serbia & Andorra) & +-(Ukraine & Germany) & +-(Ukraine & Ireland) & +-(Ukraine & Denmark) & +-(Ukraine & France) & +-(Ukraine & Switzerland) & +-(Ukraine & United_Kingdom) & +-(Ukraine & Slovakia) & +-(Ukraine & Finland) & +-(Ukraine & Macedonia) & +-(Ukraine & Hungary) & +-(Ukraine & Sweden) & +-(Ukraine & Portugal) & +-(Ukraine & Montenegro) & +-(Ukraine & Monaco) & +-(Ukraine & Albania) & +-(Ukraine & Spain) & +-(Ukraine & Latvia) & +-(Ukraine & Armenia) & +-(Ukraine & Romania) & +-(Ukraine & Turkey) & +-(Ukraine & Israel) & +-(Ukraine & Bulgaria) & +-(Ukraine & Greece) & +-(Ukraine & Austria) & +-(Ukraine & Poland) & +-(Ukraine & Cyprus) & +-(Ukraine & Croatia) & +-(Ukraine & Iceland) & +-(Ukraine & Czech_Republic) & +-(Ukraine & Estonia) & +-(Ukraine & Lithuania) & +-(Ukraine & San_Marino) & +-(Ukraine & Georgia) & +-(Ukraine & Slovenia) & +-(Ukraine & Netherlands) & +-(Ukraine & Andorra) & +-(Israel & Ireland) & +-(Israel & France) & +-(Israel & Switzerland) & +-(Israel & Slovakia) & +-(Israel & Finland) & +-(Israel & Macedonia) & +-(Israel & Hungary) & +-(Israel & Sweden) & +-(Israel & Portugal) & +-(Israel & Montenegro) & +-(Israel & Monaco) & +-(Israel & Albania) & +-(Israel & Armenia) & +-(Israel & Bosnia_and_Herzegovina) & +-(Israel & Azerbaijan) & +-(Israel & Turkey) & +-(Israel & Serbia) & +-(Israel & Bulgaria) & +-(Israel & Austria) & +-(Israel & Poland) & +-(Israel & Cyprus) & +-(Israel & Czech_Republic) & +-(Israel & Estonia) & +-(Israel & Moldova) & +-(Israel & Lithuania) & +-(Israel & San_Marino) & +-(Israel & Georgia) & +-(Israel & Belgium) & +-(Israel & Slovenia) & +-(Israel & Netherlands) & +-(Israel & Andorra) & +-(Norway & Ireland) & +-(Norway & France) & +-(Norway & Switzerland) & +-(Norway & United_Kingdom) & +-(Norway & Slovakia) & +-(Norway & Macedonia) & +-(Norway & Hungary) & +-(Norway & Portugal) & +-(Norway & Montenegro) & +-(Norway & Monaco) & +-(Norway & Albania) & +-(Norway & Spain) & +-(Norway & Armenia) & +-(Norway & Ukraine) & +-(Norway & Israel) & +-(Norway & Bulgaria) & +-(Norway & Russia) & +-(Norway & Belarus) & +-(Norway & Greece) & +-(Norway & Austria) & +-(Norway & Poland) & +-(Norway & Cyprus) & +-(Norway & Croatia) & +-(Norway & Czech_Republic) & +-(Norway & Moldova) & +-(Norway & Lithuania) & +-(Norway & San_Marino) & +-(Norway & Georgia) & +-(Norway & Belgium) & +-(Norway & Slovenia) & +-(Norway & Netherlands) & +-(Norway & Andorra) & +-(Bulgaria & Ireland) & +-(Bulgaria & Denmark) & +-(Bulgaria & France) & +-(Bulgaria & Switzerland) & +-(Bulgaria & United_Kingdom) & +-(Bulgaria & Slovakia) & +-(Bulgaria & Finland) & +-(Bulgaria & Hungary) & +-(Bulgaria & Sweden) & +-(Bulgaria & Portugal) & +-(Bulgaria & Montenegro) & +-(Bulgaria & Monaco) & +-(Bulgaria & Albania) & +-(Bulgaria & Spain) & +-(Bulgaria & Latvia) & +-(Bulgaria & Armenia) & +-(Bulgaria & Bosnia_and_Herzegovina) & +-(Bulgaria & Romania) & +-(Bulgaria & Serbia) & +-(Bulgaria & Ukraine) & +-(Bulgaria & Israel) & +-(Bulgaria & Norway) & +-(Bulgaria & Belarus) & +-(Bulgaria & Austria) & +-(Bulgaria & Poland) & +-(Bulgaria & Croatia) & +-(Bulgaria & Malta) & +-(Bulgaria & Iceland) & +-(Bulgaria & Czech_Republic) & +-(Bulgaria & Estonia) & +-(Bulgaria & Moldova) & +-(Bulgaria & Lithuania) & +-(Bulgaria & San_Marino) & +-(Bulgaria & Georgia) & +-(Bulgaria & Belgium) & +-(Bulgaria & Slovenia) & +-(Bulgaria & Netherlands) & +-(Bulgaria & Andorra) & +-(Russia & Germany) & +-(Russia & Ireland) & +-(Russia & Switzerland) & +-(Russia & United_Kingdom) & +-(Russia & Slovakia) & +-(Russia & Finland) & +-(Russia & Macedonia) & +-(Russia & Hungary) & +-(Russia & Sweden) & +-(Russia & Portugal) & +-(Russia & Montenegro) & +-(Russia & Monaco) & +-(Russia & Albania) & +-(Russia & Spain) & +-(Russia & Bosnia_and_Herzegovina) & +-(Russia & Turkey) & +-(Russia & Israel) & +-(Russia & Bulgaria) & +-(Russia & Greece) & +-(Russia & Austria) & +-(Russia & Poland) & +-(Russia & Cyprus) & +-(Russia & Iceland) & +-(Russia & Czech_Republic) & +-(Russia & Estonia) & +-(Russia & San_Marino) & +-(Russia & Belgium) & +-(Russia & Slovenia) & +-(Russia & Andorra) & +-(Belarus & Germany) & +-(Belarus & Ireland) & +-(Belarus & Denmark) & +-(Belarus & France) & +-(Belarus & United_Kingdom) & +-(Belarus & Slovakia) & +-(Belarus & Finland) & +-(Belarus & Macedonia) & +-(Belarus & Hungary) & +-(Belarus & Sweden) & +-(Belarus & Portugal) & +-(Belarus & Montenegro) & +-(Belarus & Monaco) & +-(Belarus & Albania) & +-(Belarus & Spain) & +-(Belarus & Latvia) & +-(Belarus & Armenia) & +-(Belarus & Bosnia_and_Herzegovina) & +-(Belarus & Romania) & +-(Belarus & Turkey) & +-(Belarus & Serbia) & +-(Belarus & Israel) & +-(Belarus & Bulgaria) & +-(Belarus & Greece) & +-(Belarus & Austria) & +-(Belarus & Poland) & +-(Belarus & Cyprus) & +-(Belarus & Croatia) & +-(Belarus & Malta) & +-(Belarus & Iceland) & +-(Belarus & Czech_Republic) & +-(Belarus & Estonia) & +-(Belarus & Moldova) & +-(Belarus & Lithuania) & +-(Belarus & San_Marino) & +-(Belarus & Georgia) & +-(Belarus & Belgium) & +-(Belarus & Slovenia) & +-(Belarus & Netherlands) & +-(Belarus & Andorra) & +-(Greece & Germany) & +-(Greece & Ireland) & +-(Greece & Denmark) & +-(Greece & France) & +-(Greece & Switzerland) & +-(Greece & Slovakia) & +-(Greece & Macedonia) & +-(Greece & Hungary) & +-(Greece & Sweden) & +-(Greece & Portugal) & +-(Greece & Montenegro) & +-(Greece & Monaco) & +-(Greece & Spain) & +-(Greece & Bosnia_and_Herzegovina) & +-(Greece & Azerbaijan) & +-(Greece & Romania) & +-(Greece & Serbia) & +-(Greece & Ukraine) & +-(Greece & Belarus) & +-(Greece & Austria) & +-(Greece & Poland) & +-(Greece & Croatia) & +-(Greece & Malta) & +-(Greece & Iceland) & +-(Greece & Czech_Republic) & +-(Greece & Lithuania) & +-(Greece & San_Marino) & +-(Greece & Georgia) & +-(Greece & Belgium) & +-(Greece & Slovenia) & +-(Greece & Netherlands) & +-(Greece & Andorra) & +-(Austria & Ireland) & +-(Austria & France) & +-(Austria & Switzerland) & +-(Austria & Slovakia) & +-(Austria & Finland) & +-(Austria & Macedonia) & +-(Austria & Hungary) & +-(Austria & Sweden) & +-(Austria & Portugal) & +-(Austria & Monaco) & +-(Austria & Albania) & +-(Austria & Spain) & +-(Austria & Armenia) & +-(Austria & Azerbaijan) & +-(Austria & Romania) & +-(Austria & Ukraine) & +-(Austria & Israel) & +-(Austria & Norway) & +-(Austria & Bulgaria) & +-(Austria & Russia) & +-(Austria & Belarus) & +-(Austria & Greece) & +-(Austria & Cyprus) & +-(Austria & Croatia) & +-(Austria & Malta) & +-(Austria & Iceland) & +-(Austria & Czech_Republic) & +-(Austria & Estonia) & +-(Austria & Moldova) & +-(Austria & Lithuania) & +-(Austria & San_Marino) & +-(Austria & Georgia) & +-(Austria & Belgium) & +-(Austria & Slovenia) & +-(Austria & Netherlands) & +-(Austria & Andorra) & +-(Poland & Ireland) & +-(Poland & Switzerland) & +-(Poland & United_Kingdom) & +-(Poland & Slovakia) & +-(Poland & Macedonia) & +-(Poland & Portugal) & +-(Poland & Montenegro) & +-(Poland & Monaco) & +-(Poland & Albania) & +-(Poland & Spain) & +-(Poland & Latvia) & +-(Poland & Bosnia_and_Herzegovina) & +-(Poland & Azerbaijan) & +-(Poland & Romania) & +-(Poland & Turkey) & +-(Poland & Serbia) & +-(Poland & Bulgaria) & +-(Poland & Belarus) & +-(Poland & Greece) & +-(Poland & Austria) & +-(Poland & Cyprus) & +-(Poland & Croatia) & +-(Poland & Malta) & +-(Poland & Iceland) & +-(Poland & Czech_Republic) & +-(Poland & Moldova) & +-(Poland & Lithuania) & +-(Poland & San_Marino) & +-(Poland & Georgia) & +-(Poland & Slovenia) & +-(Poland & Netherlands) & +-(Poland & Andorra) & +-(Cyprus & Germany) & +-(Cyprus & Ireland) & +-(Cyprus & Denmark) & +-(Cyprus & France) & +-(Cyprus & Switzerland) & +-(Cyprus & United_Kingdom) & +-(Cyprus & Slovakia) & +-(Cyprus & Finland) & +-(Cyprus & Macedonia) & +-(Cyprus & Hungary) & +-(Cyprus & Sweden) & +-(Cyprus & Portugal) & +-(Cyprus & Monaco) & +-(Cyprus & Albania) & +-(Cyprus & Latvia) & +-(Cyprus & Bosnia_and_Herzegovina) & +-(Cyprus & Ukraine) & +-(Cyprus & Belarus) & +-(Cyprus & Austria) & +-(Cyprus & Poland) & +-(Cyprus & Croatia) & +-(Cyprus & Czech_Republic) & +-(Cyprus & Estonia) & +-(Cyprus & Moldova) & +-(Cyprus & Lithuania) & +-(Cyprus & San_Marino) & +-(Cyprus & Georgia) & +-(Cyprus & Belgium) & +-(Cyprus & Slovenia) & +-(Cyprus & Netherlands) & +-(Cyprus & Andorra) & +-(Croatia & Germany) & +-(Croatia & Ireland) & +-(Croatia & France) & +-(Croatia & Switzerland) & +-(Croatia & Slovakia) & +-(Croatia & Hungary) & +-(Croatia & Sweden) & +-(Croatia & Portugal) & +-(Croatia & Monaco) & +-(Croatia & Albania) & +-(Croatia & Spain) & +-(Croatia & Latvia) & +-(Croatia & Armenia) & +-(Croatia & Romania) & +-(Croatia & Ukraine) & +-(Croatia & Israel) & +-(Croatia & Norway) & +-(Croatia & Bulgaria) & +-(Croatia & Belarus) & +-(Croatia & Greece) & +-(Croatia & Austria) & +-(Croatia & Poland) & +-(Croatia & Iceland) & +-(Croatia & Czech_Republic) & +-(Croatia & Estonia) & +-(Croatia & Moldova) & +-(Croatia & Lithuania) & +-(Croatia & San_Marino) & +-(Croatia & Georgia) & +-(Croatia & Belgium) & +-(Croatia & Andorra) & +-(Malta & Germany) & +-(Malta & Denmark) & +-(Malta & France) & +-(Malta & Slovakia) & +-(Malta & Finland) & +-(Malta & Macedonia) & +-(Malta & Hungary) & +-(Malta & Portugal) & +-(Malta & Montenegro) & +-(Malta & Monaco) & +-(Malta & Spain) & +-(Malta & Armenia) & +-(Malta & Bosnia_and_Herzegovina) & +-(Malta & Turkey) & +-(Malta & Serbia) & +-(Malta & Norway) & +-(Malta & Bulgaria) & +-(Malta & Austria) & +-(Malta & Czech_Republic) & +-(Malta & Moldova) & +-(Malta & Lithuania) & +-(Malta & San_Marino) & +-(Malta & Georgia) & +-(Malta & Slovenia) & +-(Malta & Netherlands) & +-(Malta & Andorra) & +-(Iceland & Germany) & +-(Iceland & Ireland) & +-(Iceland & France) & +-(Iceland & Switzerland) & +-(Iceland & United_Kingdom) & +-(Iceland & Slovakia) & +-(Iceland & Macedonia) & +-(Iceland & Hungary) & +-(Iceland & Portugal) & +-(Iceland & Montenegro) & +-(Iceland & Monaco) & +-(Iceland & Albania) & +-(Iceland & Spain) & +-(Iceland & Armenia) & +-(Iceland & Bosnia_and_Herzegovina) & +-(Iceland & Azerbaijan) & +-(Iceland & Romania) & +-(Iceland & Turkey) & +-(Iceland & Serbia) & +-(Iceland & Israel) & +-(Iceland & Bulgaria) & +-(Iceland & Russia) & +-(Iceland & Belarus) & +-(Iceland & Greece) & +-(Iceland & Poland) & +-(Iceland & Croatia) & +-(Iceland & Malta) & +-(Iceland & Czech_Republic) & +-(Iceland & Moldova) & +-(Iceland & San_Marino) & +-(Iceland & Georgia) & +-(Iceland & Slovenia) & +-(Iceland & Netherlands) & +-(Iceland & Andorra) & +-(Czech_Republic & Germany) & +-(Czech_Republic & Ireland) & +-(Czech_Republic & Denmark) & +-(Czech_Republic & France) & +-(Czech_Republic & Switzerland) & +-(Czech_Republic & United_Kingdom) & +-(Czech_Republic & Slovakia) & +-(Czech_Republic & Finland) & +-(Czech_Republic & Macedonia) & +-(Czech_Republic & Hungary) & +-(Czech_Republic & Sweden) & +-(Czech_Republic & Portugal) & +-(Czech_Republic & Montenegro) & +-(Czech_Republic & Monaco) & +-(Czech_Republic & Albania) & +-(Czech_Republic & Spain) & +-(Czech_Republic & Latvia) & +-(Czech_Republic & Bosnia_and_Herzegovina) & +-(Czech_Republic & Romania) & +-(Czech_Republic & Turkey) & +-(Czech_Republic & Serbia) & +-(Czech_Republic & Israel) & +-(Czech_Republic & Norway) & +-(Czech_Republic & Bulgaria) & +-(Czech_Republic & Russia) & +-(Czech_Republic & Belarus) & +-(Czech_Republic & Greece) & +-(Czech_Republic & Austria) & +-(Czech_Republic & Poland) & +-(Czech_Republic & Cyprus) & +-(Czech_Republic & Croatia) & +-(Czech_Republic & Malta) & +-(Czech_Republic & Iceland) & +-(Czech_Republic & Estonia) & +-(Czech_Republic & Moldova) & +-(Czech_Republic & Lithuania) & +-(Czech_Republic & San_Marino) & +-(Czech_Republic & Georgia) & +-(Czech_Republic & Belgium) & +-(Czech_Republic & Slovenia) & +-(Czech_Republic & Netherlands) & +-(Czech_Republic & Andorra) & +-(Estonia & Ireland) & +-(Estonia & United_Kingdom) & +-(Estonia & Slovakia) & +-(Estonia & Macedonia) & +-(Estonia & Hungary) & +-(Estonia & Portugal) & +-(Estonia & Montenegro) & +-(Estonia & Monaco) & +-(Estonia & Albania) & +-(Estonia & Spain) & +-(Estonia & Armenia) & +-(Estonia & Bosnia_and_Herzegovina) & +-(Estonia & Azerbaijan) & +-(Estonia & Romania) & +-(Estonia & Turkey) & +-(Estonia & Serbia) & +-(Estonia & Israel) & +-(Estonia & Bulgaria) & +-(Estonia & Belarus) & +-(Estonia & Greece) & +-(Estonia & Austria) & +-(Estonia & Poland) & +-(Estonia & Cyprus) & +-(Estonia & Croatia) & +-(Estonia & Malta) & +-(Estonia & Czech_Republic) & +-(Estonia & Moldova) & +-(Estonia & Lithuania) & +-(Estonia & San_Marino) & +-(Estonia & Georgia) & +-(Estonia & Belgium) & +-(Estonia & Slovenia) & +-(Estonia & Netherlands) & +-(Estonia & Andorra) & +-(Moldova & Germany) & +-(Moldova & Ireland) & +-(Moldova & Denmark) & +-(Moldova & France) & +-(Moldova & Switzerland) & +-(Moldova & United_Kingdom) & +-(Moldova & Slovakia) & +-(Moldova & Finland) & +-(Moldova & Macedonia) & +-(Moldova & Hungary) & +-(Moldova & Sweden) & +-(Moldova & Portugal) & +-(Moldova & Montenegro) & +-(Moldova & Monaco) & +-(Moldova & Albania) & +-(Moldova & Spain) & +-(Moldova & Armenia) & +-(Moldova & Bosnia_and_Herzegovina) & +-(Moldova & Turkey) & +-(Moldova & Serbia) & +-(Moldova & Ukraine) & +-(Moldova & Israel) & +-(Moldova & Norway) & +-(Moldova & Bulgaria) & +-(Moldova & Greece) & +-(Moldova & Austria) & +-(Moldova & Poland) & +-(Moldova & Cyprus) & +-(Moldova & Croatia) & +-(Moldova & Malta) & +-(Moldova & Iceland) & +-(Moldova & Czech_Republic) & +-(Moldova & Estonia) & +-(Moldova & Lithuania) & +-(Moldova & San_Marino) & +-(Moldova & Georgia) & +-(Moldova & Belgium) & +-(Moldova & Slovenia) & +-(Moldova & Netherlands) & +-(Moldova & Andorra) & +-(Lithuania & Denmark) & +-(Lithuania & France) & +-(Lithuania & Switzerland) & +-(Lithuania & United_Kingdom) & +-(Lithuania & Slovakia) & +-(Lithuania & Macedonia) & +-(Lithuania & Hungary) & +-(Lithuania & Portugal) & +-(Lithuania & Montenegro) & +-(Lithuania & Monaco) & +-(Lithuania & Albania) & +-(Lithuania & Spain) & +-(Lithuania & Armenia) & +-(Lithuania & Bosnia_and_Herzegovina) & +-(Lithuania & Azerbaijan) & +-(Lithuania & Romania) & +-(Lithuania & Turkey) & +-(Lithuania & Serbia) & +-(Lithuania & Israel) & +-(Lithuania & Bulgaria) & +-(Lithuania & Belarus) & +-(Lithuania & Austria) & +-(Lithuania & Poland) & +-(Lithuania & Cyprus) & +-(Lithuania & Croatia) & +-(Lithuania & Malta) & +-(Lithuania & Iceland) & +-(Lithuania & Czech_Republic) & +-(Lithuania & San_Marino) & +-(Lithuania & Belgium) & +-(Lithuania & Netherlands) & +-(Lithuania & Andorra) & +-(San_Marino & Germany) & +-(San_Marino & Ireland) & +-(San_Marino & Denmark) & +-(San_Marino & France) & +-(San_Marino & Switzerland) & +-(San_Marino & United_Kingdom) & +-(San_Marino & Slovakia) & +-(San_Marino & Finland) & +-(San_Marino & Macedonia) & +-(San_Marino & Hungary) & +-(San_Marino & Sweden) & +-(San_Marino & Portugal) & +-(San_Marino & Montenegro) & +-(San_Marino & Monaco) & +-(San_Marino & Albania) & +-(San_Marino & Spain) & +-(San_Marino & Latvia) & +-(San_Marino & Armenia) & +-(San_Marino & Bosnia_and_Herzegovina) & +-(San_Marino & Azerbaijan) & +-(San_Marino & Romania) & +-(San_Marino & Turkey) & +-(San_Marino & Serbia) & +-(San_Marino & Ukraine) & +-(San_Marino & Norway) & +-(San_Marino & Bulgaria) & +-(San_Marino & Russia) & +-(San_Marino & Belarus) & +-(San_Marino & Austria) & +-(San_Marino & Poland) & +-(San_Marino & Cyprus) & +-(San_Marino & Croatia) & +-(San_Marino & Malta) & +-(San_Marino & Iceland) & +-(San_Marino & Czech_Republic) & +-(San_Marino & Estonia) & +-(San_Marino & Moldova) & +-(San_Marino & Lithuania) & +-(San_Marino & Georgia) & +-(San_Marino & Belgium) & +-(San_Marino & Slovenia) & +-(San_Marino & Netherlands) & +-(San_Marino & Andorra) & +-(Georgia & Germany) & +-(Georgia & Ireland) & +-(Georgia & Denmark) & +-(Georgia & France) & +-(Georgia & Switzerland) & +-(Georgia & United_Kingdom) & +-(Georgia & Slovakia) & +-(Georgia & Finland) & +-(Georgia & Macedonia) & +-(Georgia & Hungary) & +-(Georgia & Sweden) & +-(Georgia & Portugal) & +-(Georgia & Montenegro) & +-(Georgia & Monaco) & +-(Georgia & Albania) & +-(Georgia & Spain) & +-(Georgia & Latvia) & +-(Georgia & Bosnia_and_Herzegovina) & +-(Georgia & Azerbaijan) & +-(Georgia & Romania) & +-(Georgia & Turkey) & +-(Georgia & Serbia) & +-(Georgia & Israel) & +-(Georgia & Norway) & +-(Georgia & Bulgaria) & +-(Georgia & Russia) & +-(Georgia & Greece) & +-(Georgia & Austria) & +-(Georgia & Poland) & +-(Georgia & Cyprus) & +-(Georgia & Croatia) & +-(Georgia & Malta) & +-(Georgia & Iceland) & +-(Georgia & Czech_Republic) & +-(Georgia & Estonia) & +-(Georgia & Moldova) & +-(Georgia & Lithuania) & +-(Georgia & San_Marino) & +-(Georgia & Belgium) & +-(Georgia & Slovenia) & +-(Georgia & Netherlands) & +-(Georgia & Andorra) & +-(Belgium & Ireland) & +-(Belgium & Switzerland) & +-(Belgium & United_Kingdom) & +-(Belgium & Slovakia) & +-(Belgium & Finland) & +-(Belgium & Macedonia) & +-(Belgium & Hungary) & +-(Belgium & Sweden) & +-(Belgium & Portugal) & +-(Belgium & Montenegro) & +-(Belgium & Monaco) & +-(Belgium & Albania) & +-(Belgium & Bosnia_and_Herzegovina) & +-(Belgium & Azerbaijan) & +-(Belgium & Serbia) & +-(Belgium & Ukraine) & +-(Belgium & Bulgaria) & +-(Belgium & Russia) & +-(Belgium & Belarus) & +-(Belgium & Austria) & +-(Belgium & Poland) & +-(Belgium & Cyprus) & +-(Belgium & Croatia) & +-(Belgium & Malta) & +-(Belgium & Iceland) & +-(Belgium & Czech_Republic) & +-(Belgium & Estonia) & +-(Belgium & Moldova) & +-(Belgium & Lithuania) & +-(Belgium & San_Marino) & +-(Belgium & Georgia) & +-(Belgium & Slovenia) & +-(Belgium & Andorra) & +-(Slovenia & Ireland) & +-(Slovenia & France) & +-(Slovenia & Switzerland) & +-(Slovenia & United_Kingdom) & +-(Slovenia & Slovakia) & +-(Slovenia & Finland) & +-(Slovenia & Hungary) & +-(Slovenia & Sweden) & +-(Slovenia & Portugal) & +-(Slovenia & Monaco) & +-(Slovenia & Albania) & +-(Slovenia & Spain) & +-(Slovenia & Latvia) & +-(Slovenia & Armenia) & +-(Slovenia & Azerbaijan) & +-(Slovenia & Romania) & +-(Slovenia & Ukraine) & +-(Slovenia & Israel) & +-(Slovenia & Bulgaria) & +-(Slovenia & Belarus) & +-(Slovenia & Greece) & +-(Slovenia & Austria) & +-(Slovenia & Poland) & +-(Slovenia & Cyprus) & +-(Slovenia & Iceland) & +-(Slovenia & Czech_Republic) & +-(Slovenia & Moldova) & +-(Slovenia & Lithuania) & +-(Slovenia & San_Marino) & +-(Slovenia & Georgia) & +-(Slovenia & Belgium) & +-(Slovenia & Netherlands) & +-(Slovenia & Andorra) & +-(Netherlands & Ireland) & +-(Netherlands & France) & +-(Netherlands & Switzerland) & +-(Netherlands & United_Kingdom) & +-(Netherlands & Slovakia) & +-(Netherlands & Finland) & +-(Netherlands & Macedonia) & +-(Netherlands & Hungary) & +-(Netherlands & Sweden) & +-(Netherlands & Portugal) & +-(Netherlands & Monaco) & +-(Netherlands & Albania) & +-(Netherlands & Spain) & +-(Netherlands & Latvia) & +-(Netherlands & Bosnia_and_Herzegovina) & +-(Netherlands & Romania) & +-(Netherlands & Serbia) & +-(Netherlands & Ukraine) & +-(Netherlands & Bulgaria) & +-(Netherlands & Russia) & +-(Netherlands & Belarus) & +-(Netherlands & Austria) & +-(Netherlands & Poland) & +-(Netherlands & Cyprus) & +-(Netherlands & Croatia) & +-(Netherlands & Malta) & +-(Netherlands & Iceland) & +-(Netherlands & Czech_Republic) & +-(Netherlands & Moldova) & +-(Netherlands & Lithuania) & +-(Netherlands & San_Marino) & +-(Netherlands & Georgia) & +-(Netherlands & Slovenia) & +-(Netherlands & Andorra) & +-(Andorra & Germany) & +-(Andorra & Ireland) & +-(Andorra & Denmark) & +-(Andorra & France) & +-(Andorra & Switzerland) & +-(Andorra & United_Kingdom) & +-(Andorra & Slovakia) & +-(Andorra & Macedonia) & +-(Andorra & Hungary) & +-(Andorra & Sweden) & +-(Andorra & Montenegro) & +-(Andorra & Monaco) & +-(Andorra & Albania) & +-(Andorra & Armenia) & +-(Andorra & Bosnia_and_Herzegovina) & +-(Andorra & Azerbaijan) & +-(Andorra & Turkey) & +-(Andorra & Serbia) & +-(Andorra & Israel) & +-(Andorra & Bulgaria) & +-(Andorra & Russia) & +-(Andorra & Belarus) & +-(Andorra & Greece) & +-(Andorra & Austria) & +-(Andorra & Poland) & +-(Andorra & Cyprus) & +-(Andorra & Croatia) & +-(Andorra & Malta) & +-(Andorra & Iceland) & +-(Andorra & Czech_Republic) & +-(Andorra & Estonia) & +-(Andorra & Moldova) & +-(Andorra & Lithuania) & +-(Andorra & San_Marino) & +-(Andorra & Georgia) & +-(Andorra & Belgium) & +-(Andorra & Slovenia) & +-(Andorra & Netherlands) & + +true From 3cdaf3cd8c804b769a42f774cac7a16510fe5dbe Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Sun, 13 Mar 2022 15:41:57 +0100 Subject: [PATCH 5/5] add comments to ParsedFormula struct --- src/parser.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/parser.rs b/src/parser.rs index 9df13a2..0c2a52b 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -90,9 +90,13 @@ pub enum SymbolicBDD { #[derive(Debug, Clone)] pub struct ParsedFormula { + // all variables in the parse tree pub vars: Vec, + // all variables not bound by a quantifier in the parse tree pub free_vars: Vec, + // the parse tree pub bdd: SymbolicBDD, + // the environment pub env: RefCell>, }