Merge pull request #232 from d702e20/lcgs-new-intermediate

Use new AST for LCGS and give better errors

benches/benchmark_solver.rs

@@ -13,10 +13,11 @@ use cgaal_engine::algorithms::global::multithread::MultithreadedGlobalAlgorithm;
 use cgaal_engine::algorithms::global::singlethread::SinglethreadedGlobalAlgorithm;
 use cgaal_engine::atl::Phi;
 use cgaal_engine::edg::atledg::{vertex::AtlVertex, AtlDependencyGraph};
-use cgaal_engine::game_structure::lcgs::ir::intermediate::IntermediateLcgs;
-use cgaal_engine::game_structure::lcgs::parse::parse_lcgs;
+use cgaal_engine::game_structure::lcgs::intermediate::IntermediateLcgs;
 use cgaal_engine::game_structure::EagerGameStructure;
 use cgaal_engine::game_structure::GameStructure;
+use cgaal_engine::parsing::errors::ErrorLog;
+use cgaal_engine::parsing::parse_lcgs;
 use criterion::{criterion_group, criterion_main, BenchmarkId, Criterion};
 use std::cmp::Ordering;
 use std::env;
@@ -59,7 +60,10 @@ macro_rules! bench_json {
                     )))
                     .unwrap();
 
-                    let v0 = AtlVertex::Full { state: 0, formula };
+                    let v0 = AtlVertex::Full {
+                        state: cgaal_engine::game_structure::StateIdx(0),
+                        formula,
+                    };
 
                     distributed_certain_zero(
                         graph,
@@ -83,10 +87,14 @@ macro_rules! bench_lcgs {
             eprintln!(concat!("[stats] bench_run_start: ", stringify!($name)));
             c.bench_function(stringify!($name), |b| {
                 b.iter(|| {
-                    let lcgs = parse_lcgs(include_str!(concat!(lcgs_model_path_prefix!(), $model)))
-                        .expect(&format!("Could not read model {}", $model));
+                    let errors = ErrorLog::new();
+                    let lcgs = parse_lcgs(
+                        include_str!(concat!(lcgs_model_path_prefix!(), $model)),
+                        &errors,
+                    )
+                    .expect(&format!("Could not read model {}", $model));
                     let game_structure =
-                        IntermediateLcgs::create(lcgs).expect("Could not symbolcheck");
+                        IntermediateLcgs::create(lcgs, &errors).expect("Could not symbolcheck");
                     let graph = AtlDependencyGraph { game_structure };
 
                     let formula = serde_json::from_str(include_str!(concat!(
@@ -165,13 +173,14 @@ macro_rules! bench_lcgs_threads {
                     &core_count,
                     |b, &core_count| {
                         b.iter(|| {
-                            let lcgs = parse_lcgs(include_str!(concat!(
-                                lcgs_model_path_prefix!(),
-                                $model
-                            )))
+                            let errors = ErrorLog::new();
+                            let lcgs = parse_lcgs(
+                                include_str!(concat!(lcgs_model_path_prefix!(), $model)),
+                                &errors,
+                            )
                             .expect(&format!("Could not read model {}", $model));
-                            let game_structure =
-                                IntermediateLcgs::create(lcgs).expect("Could not symbolcheck");
+                            let game_structure = IntermediateLcgs::create(lcgs, &errors)
+                                .expect("Could not symbolcheck");
                             let graph = AtlDependencyGraph { game_structure };
 
                             let formula = serde_json::from_str(include_str!(concat!(

cgaal-cli/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "cgaal"
-version = "2.0.1"
+version = "2.0.2"
 authors = [
     "Asger Weirsøe <asger@weircon.dk>",
     "Falke Carlsen <falkeboc@cs.aau.dk>",
@@ -24,4 +24,4 @@ tracing-subscriber = "0.2.17"
 serde_json = "1.0.83"
 regex = { version = "1", features = ["unicode-case"] }
 humantime = "2.1.0"
-cgaal-engine = { path = "../cgaal-engine", version = "1.0.3" }
+cgaal-engine = { path = "../cgaal-engine", version = "2.0.0" }

cgaal-cli/src/load.rs

@@ -1,13 +1,12 @@
-use cgaal_engine::atl::convert::convert_expr_to_phi;
 use cgaal_engine::atl::Phi;
 use std::fs::File;
 use std::io::Read;
 
-use cgaal_engine::game_structure::lcgs::ir::intermediate::IntermediateLcgs;
-use cgaal_engine::game_structure::lcgs::parse::parse_lcgs;
+use cgaal_engine::game_structure::lcgs::convert_expr_to_phi;
+use cgaal_engine::game_structure::lcgs::intermediate::IntermediateLcgs;
 use cgaal_engine::game_structure::EagerGameStructure;
 use cgaal_engine::parsing::errors::ErrorLog;
-use cgaal_engine::parsing::parse_atl;
+use cgaal_engine::parsing::{parse_atl, parse_lcgs};
 
 use crate::options::{FormulaFormat, ModelFormat};
 
@@ -56,11 +55,16 @@ pub fn load_model(model_path: &str, model_format: Option<ModelFormat>) -> Result
             Ok(Model::Json(game_structure))
         }
         ModelFormat::Lcgs => {
-            let lcgs = parse_lcgs(&content)
-                .map_err(|err| format!("Failed to parse the LCGS program. {}", err))?;
+            let errors = ErrorLog::new();
+            let lcgs = parse_lcgs(&content, &errors).ok_or_else(|| {
+                format!(
+                    "Failed to parse the LCGS program.\n{}",
+                    errors.to_string(&content)
+                )
+            })?;
 
-            let game_structure = IntermediateLcgs::create(lcgs)
-                .map_err(|err| format!("Invalid LCGS program. {}", err))?;
+            let game_structure = IntermediateLcgs::create(lcgs, &errors)
+                .map_err(|_| format!("Invalid LCGS program.\n{}", errors.to_string(&content)))?;
 
             Ok(Model::Lcgs(game_structure))
         }
@@ -105,10 +109,10 @@ pub fn load_formula(
             let game =
                 game.ok_or_else(|| "Cannot load ATL formula without a game structure".to_string())?;
 
-            let mut errors = ErrorLog::new();
-            parse_atl(&content, &mut errors)
-                .and_then(|expr| convert_expr_to_phi(&expr, game, &mut errors))
-                .ok_or_else(|| {
+            let errors = ErrorLog::new();
+            parse_atl(&content, &errors)
+                .and_then(|expr| convert_expr_to_phi(expr, game, &errors))
+                .map_err(|_| {
                     format!(
                         "Invalid ATL formula provided:\n{}",
                         errors.to_string(&content)

cgaal-cli/src/main.rs

@@ -18,9 +18,8 @@ use cgaal_engine::analyse::analyse;
 use cgaal_engine::atl::Phi;
 use cgaal_engine::edg::atledg::vertex::AtlVertex;
 use cgaal_engine::edg::atledg::AtlDependencyGraph;
-use cgaal_engine::game_structure::lcgs::ast::DeclKind;
-use cgaal_engine::game_structure::lcgs::ir::symbol_table::Owner;
 use cgaal_engine::game_structure::GameStructure;
+use cgaal_engine::parsing::ast::DeclKind;
 #[cfg(feature = "graph-printer")]
 use cgaal_engine::printer::print_graph;
 
@@ -55,19 +54,16 @@ fn main_inner() -> Result<(), String> {
                 .ok_or("The 'index' command is only valid for LCGS models")?;
 
             println!("Players:");
-            for player in &ir.get_player() {
-                println!("{} : {}", player.get_name(), player.index())
+            for player in ir.get_players() {
+                let decl = ir.get_decl(&player.symbol_index).unwrap();
+                println!("{} : {}", decl.ident, player.player_index);
             }
 
             println!("\nLabels:");
-            for label_symbol in &ir.get_labels() {
+            for label_symbol in ir.get_labels() {
                 let label_decl = ir.get_decl(label_symbol).unwrap();
-                if let DeclKind::Label(label) = &label_decl.kind {
-                    if Owner::Global == label_symbol.owner {
-                        println!("{} : {}", &label_symbol.name, label.index)
-                    } else {
-                        println!("{} : {}", &label_symbol, label.index)
-                    }
+                if let DeclKind::StateLabel(idx, _) = &label_decl.kind {
+                    println!("{} : {}", &label_decl.ident, idx);
                 }
             }
         }

cgaal-engine/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "cgaal-engine"
-version = "1.0.3"
+version = "2.0.0"
 authors = [
     "Asger Weirsøe <asger@weircon.dk>",
     "Falke Carlsen <falkeboc@cs.aau.dk>",

cgaal-engine/src/algorithms/certain_zero/search_strategy/instability_heuristic_search.rs

@@ -7,10 +7,10 @@ use crate::algorithms::certain_zero::search_strategy::{SearchStrategy, SearchStr
 use crate::atl::Phi;
 use crate::edg::atledg::vertex::AtlVertex;
 use crate::edg::Edge;
-use crate::game_structure::lcgs::ast::{BinaryOpKind, DeclKind, Expr, ExprKind, UnaryOpKind};
-use crate::game_structure::lcgs::ir::eval::Evaluator;
-use crate::game_structure::lcgs::ir::intermediate::{IntermediateLcgs, State};
-use crate::game_structure::Proposition;
+use crate::game_structure::lcgs::eval::Evaluator;
+use crate::game_structure::lcgs::intermediate::{IntermediateLcgs, State};
+use crate::game_structure::PropIdx;
+use crate::parsing::ast::{BinaryOpKind, DeclKind, Expr, ExprKind, UnaryOpKind};
 
 /// A [BiTruthDist] is an abstract metric describing how close a boolean expression is
 /// to changing truth-value of a constituent clause.
@@ -218,10 +218,10 @@ impl InstabilityHeuristicSearch {
         }
     }
 
-    fn bidist_of_proposition(&self, state: &State, prop: &Proposition) -> BiTruthDist {
+    fn bidist_of_proposition(&self, state: &State, prop: &PropIdx) -> BiTruthDist {
         let decl = self.game.label_index_to_decl(*prop);
-        if let DeclKind::Label(label) = &decl.kind {
-            InstabilityHeuristicSearch::bidist_of_expr(state, &label.condition)
+        if let DeclKind::StateLabel(_, expr) = &decl.kind {
+            InstabilityHeuristicSearch::bidist_of_expr(state, expr)
         } else {
             panic!("Non-propositions symbol in ATL formula")
         }
@@ -233,41 +233,37 @@ impl InstabilityHeuristicSearch {
         // For the remaining expressions, we evaluate them and use their negative distance to 0 (false).
         match &expr.kind {
             // Boolean operators
-            ExprKind::UnaryOp(UnaryOpKind::Not, e) => {
+            ExprKind::Unary(UnaryOpKind::Not, e) => {
                 !InstabilityHeuristicSearch::bidist_of_expr(state, e)
             }
-            ExprKind::BinaryOp(BinaryOpKind::And, lhs, rhs) => {
+            ExprKind::Binary(BinaryOpKind::And, lhs, rhs) => {
                 InstabilityHeuristicSearch::bidist_of_expr(state, lhs)
                     & InstabilityHeuristicSearch::bidist_of_expr(state, rhs)
             }
-            ExprKind::BinaryOp(BinaryOpKind::Or, lhs, rhs) => {
+            ExprKind::Binary(BinaryOpKind::Or, lhs, rhs) => {
                 InstabilityHeuristicSearch::bidist_of_expr(state, lhs)
                     | InstabilityHeuristicSearch::bidist_of_expr(state, rhs)
             }
-            ExprKind::BinaryOp(BinaryOpKind::Xor, lhs, rhs) => {
+            ExprKind::Binary(BinaryOpKind::Xor, lhs, rhs) => {
                 (InstabilityHeuristicSearch::bidist_of_expr(state, lhs)
                     & !InstabilityHeuristicSearch::bidist_of_expr(state, rhs))
                     | (!InstabilityHeuristicSearch::bidist_of_expr(state, lhs)
                         & InstabilityHeuristicSearch::bidist_of_expr(state, rhs))
             }
-            ExprKind::BinaryOp(BinaryOpKind::Implication, lhs, rhs) => {
+            ExprKind::Binary(BinaryOpKind::Implies, lhs, rhs) => {
                 !InstabilityHeuristicSearch::bidist_of_expr(state, lhs)
                     | InstabilityHeuristicSearch::bidist_of_expr(state, rhs)
             }
             // Comparisons
-            ExprKind::BinaryOp(BinaryOpKind::LessThan | BinaryOpKind::LessOrEqual, lhs, rhs) => {
+            ExprKind::Binary(BinaryOpKind::Lt | BinaryOpKind::Leq, lhs, rhs) => {
                 let evaluator = Evaluator::new(state);
                 BiTruthDist::from(evaluator.eval(lhs) - evaluator.eval(rhs))
             }
-            ExprKind::BinaryOp(
-                BinaryOpKind::GreaterThan | BinaryOpKind::GreaterOrEqual,
-                lhs,
-                rhs,
-            ) => {
+            ExprKind::Binary(BinaryOpKind::Gt | BinaryOpKind::Geq, lhs, rhs) => {
                 let evaluator = Evaluator::new(state);
                 BiTruthDist::from(evaluator.eval(rhs) - evaluator.eval(lhs))
             }
-            ExprKind::BinaryOp(BinaryOpKind::Equality, lhs, rhs) => {
+            ExprKind::Binary(BinaryOpKind::Eq, lhs, rhs) => {
                 let evaluator = Evaluator::new(state);
                 let abs_diff = (evaluator.eval(rhs) - evaluator.eval(lhs)).abs();
                 if abs_diff == 0 {
@@ -276,7 +272,7 @@ impl InstabilityHeuristicSearch {
                     BiTruthDist::from(abs_diff) // abs_diff from true
                 }
             }
-            ExprKind::BinaryOp(BinaryOpKind::Inequality, lhs, rhs) => {
+            ExprKind::Binary(BinaryOpKind::Neq, lhs, rhs) => {
                 let evaluator = Evaluator::new(state);
                 let abs_diff = (evaluator.eval(rhs) - evaluator.eval(lhs)).abs();
                 if abs_diff == 0 {

cgaal-engine/src/algorithms/certain_zero/search_strategy/linear_constrained_phi.rs

@@ -2,11 +2,9 @@ use crate::algorithms::certain_zero::search_strategy::linear_constraints::{
     ComparisonOp, LinearConstraint, LinearConstraintExtractor,
 };
 use crate::atl::Phi;
-use crate::game_structure::lcgs::ast::{
-    BinaryOpKind, DeclKind, Expr, ExprKind, Identifier, UnaryOpKind,
-};
-use crate::game_structure::lcgs::ir::intermediate::IntermediateLcgs;
-use crate::game_structure::Proposition;
+use crate::game_structure::lcgs::intermediate::IntermediateLcgs;
+use crate::game_structure::PropIdx;
+use crate::parsing::ast::{BinaryOpKind, DeclKind, Expr, ExprKind, UnaryOpKind};
 use std::cell::RefCell;
 use std::collections::HashMap;
 
@@ -48,7 +46,7 @@ impl LinearConstrainedPhi {
 
 pub struct ConstrainedPhiMaker {
     /// Cached LinearConstrainedPhi of propositions. The bool is true for negated propositions.
-    proposition_cache: RefCell<HashMap<(Proposition, bool), LinearConstrainedPhi>>,
+    proposition_cache: RefCell<HashMap<(PropIdx, bool), LinearConstrainedPhi>>,
 }
 
 impl ConstrainedPhiMaker {
@@ -94,8 +92,8 @@ impl ConstrainedPhiMaker {
                 maybe_constraint.unwrap_or_else(|| {
                     // We have not mapped this proposition yet
                     let decl = game.label_index_to_decl(*proposition);
-                    if let DeclKind::Label(label) = &decl.kind {
-                        let mapped_expr = Self::map_expr_to_constraints(&label.condition, negated);
+                    if let DeclKind::StateLabel(_, expr) = &decl.kind {
+                        let mapped_expr = Self::map_expr_to_constraints(expr, negated);
                         // Save result in cache
                         self.proposition_cache
                             .borrow_mut()
@@ -163,16 +161,16 @@ impl ConstrainedPhiMaker {
     /// Takes an expression and maps it to a LinearConstrainedPhi
     fn map_expr_to_constraints(expr: &Expr, negated: bool) -> LinearConstrainedPhi {
         match &expr.kind {
-            ExprKind::UnaryOp(UnaryOpKind::Not, sub_expr) => {
+            ExprKind::Unary(UnaryOpKind::Not, sub_expr) => {
                 return Self::map_expr_to_constraints(sub_expr, !negated);
             }
-            ExprKind::BinaryOp(operator, lhs, rhs) => {
+            ExprKind::Binary(operator, lhs, rhs) => {
                 match operator {
-                    BinaryOpKind::Equality
-                    | BinaryOpKind::GreaterThan
-                    | BinaryOpKind::GreaterOrEqual
-                    | BinaryOpKind::LessThan
-                    | BinaryOpKind::LessOrEqual => {
+                    BinaryOpKind::Eq
+                    | BinaryOpKind::Gt
+                    | BinaryOpKind::Geq
+                    | BinaryOpKind::Lt
+                    | BinaryOpKind::Leq => {
                         let lin_expr = LinearConstraintExtractor::extract(expr);
                         return if let Some(lin_expr) = lin_expr {
                             if !negated {
@@ -203,7 +201,7 @@ impl ConstrainedPhiMaker {
                         };
                     }
                     // P -> Q == not P v Q
-                    BinaryOpKind::Implication => {
+                    BinaryOpKind::Implies => {
                         let lhs_con = Self::map_expr_to_constraints(lhs, !negated);
                         let rhs_con = Self::map_expr_to_constraints(rhs, negated);
                         return if !negated {
@@ -215,7 +213,7 @@ impl ConstrainedPhiMaker {
                     _ => {}
                 }
             }
-            ExprKind::Number(n) => {
+            ExprKind::Num(n) => {
                 // Think of != as XOR in this situation
                 return if (*n == 0) != negated {
                     LinearConstrainedPhi::False
@@ -248,11 +246,9 @@ impl ConstrainedPhiMaker {
                 };
             }
             // This is essentially x != 0, if x is the name of the symbol
-            ExprKind::OwnedIdent(ident) => {
+            ExprKind::Symbol(symb) => {
                 let mut terms_hashmap = HashMap::new();
-                if let Identifier::Resolved { owner, name } = ident.as_ref() {
-                    terms_hashmap.insert(owner.symbol_id(name), 1.0);
-                }
+                terms_hashmap.insert(*symb, 1.0);
 
                 let operator = if !negated {
                     ComparisonOp::NotEqual
@@ -269,7 +265,6 @@ impl ConstrainedPhiMaker {
 
                 return LinearConstrainedPhi::Constraint(constraint);
             }
-            // TODO Other expression can be converted to a comparisons since everything != 0 is true
             _ => {}
         }