Merge branch 'main' into selection-strategies

conjure_oxide/build.rs

@@ -22,7 +22,7 @@ fn main() -> io::Result<()> {
                 let stems: Vec<String> = read_dir(subdir.path())?
                     .filter_map(Result::ok)
                     .filter(|entry| {
-                        entry.path().extension().map_or(false, |ext| {
+                        entry.path().extension().is_some_and(|ext| {
                             ext == "essence" || ext == "eprime" || ext == "disabled"
                         })
                     })
@@ -38,7 +38,7 @@ fn main() -> io::Result<()> {
                 let exts: Vec<String> = read_dir(subdir.path())?
                     .filter_map(Result::ok)
                     .filter(|entry| {
-                        entry.path().extension().map_or(false, |ext| {
+                        entry.path().extension().is_some_and(|ext| {
                             ext == "essence" || ext == "eprime" || ext == "disabled"
                         })
                     })
@@ -61,7 +61,7 @@ fn main() -> io::Result<()> {
                         entry
                             .path()
                             .extension()
-                            .map_or(false, |ext| ext == "essence" || ext == "eprime")
+                            .is_some_and(|ext| ext == "essence" || ext == "eprime")
                     })
                     .filter_map(|entry| {
                         entry
@@ -78,7 +78,7 @@ fn main() -> io::Result<()> {
                         entry
                             .path()
                             .extension()
-                            .map_or(false, |ext| ext == "essence" || ext == "eprime")
+                            .is_some_and(|ext| ext == "essence" || ext == "eprime")
                     })
                     .filter_map(|entry| {
                         entry

conjure_oxide/src/main.rs

@@ -7,11 +7,9 @@ use std::sync::Arc;
 use anyhow::Result as AnyhowResult;
 use anyhow::{anyhow, bail};
 use clap::{arg, command, Parser};
-use conjure_core::ast::pretty::pretty_expressions_as_top_level;
 use conjure_core::rule_engine::rewrite_naive;
 use conjure_oxide::defaults::get_default_rule_sets;
 use schemars::schema_for;
-use serde_json::json;
 use serde_json::to_string_pretty;
 
 use conjure_core::context::Context;
@@ -181,14 +179,14 @@ pub fn main() -> AnyhowResult<()> {
         .init();
 
     if target_family != SolverFamily::Minion {
-        log::error!("Only the Minion solver is currently supported!");
+        tracing::error!("Only the Minion solver is currently supported!");
         exit(1);
     }
 
     let rule_sets = match resolve_rule_sets(target_family, &extra_rule_sets) {
         Ok(rs) => rs,
         Err(e) => {
-            log::error!("Error resolving rule sets: {}", e);
+            tracing::error!("Error resolving rule sets: {}", e);
             exit(1);
         }
     };
@@ -200,7 +198,7 @@ pub fn main() -> AnyhowResult<()> {
         .join(", ");
 
     println!("Enabled rule sets: [{}]", pretty_rule_sets);
-    log::info!(
+    tracing::info!(
         target: "file",
         "Rule sets: {}",
         pretty_rule_sets
@@ -209,14 +207,14 @@ pub fn main() -> AnyhowResult<()> {
     let rule_priorities = get_rule_priorities(&rule_sets)?;
     let rules_vec = get_rules_vec(&rule_priorities);
 
-    log::info!(target: "file",
+    tracing::info!(target: "file",
          "Rules and priorities: {}",
          rules_vec.iter()
             .map(|rule| format!("{}: {}", rule.name, rule_priorities.get(rule).unwrap_or(&0)))
             .collect::<Vec<_>>()
             .join(", "));
 
-    log::info!(target: "file", "Input file: {}", cli.input_file.display());
+    tracing::info!(target: "file", "Input file: {}", cli.input_file.display());
     let input_file: &str = cli.input_file.to_str().ok_or(anyhow!(
         "Given input_file could not be converted to a string"
     ))?;
@@ -252,30 +250,29 @@ pub fn main() -> AnyhowResult<()> {
     context.write().unwrap().file_name = Some(cli.input_file.to_str().expect("").into());
 
     if cfg!(feature = "extra-rule-checks") {
-        log::info!("extra-rule-checks: enabled");
+        tracing::info!("extra-rule-checks: enabled");
     } else {
-        log::info!("extra-rule-checks: disabled");
+        tracing::info!("extra-rule-checks: disabled");
     }
 
     let mut model = model_from_json(&astjson, context.clone())?;
 
-    log::info!(target: "file", "Initial model: {}", json!(model));
+    tracing::info!("Initial model: \n{}\n", model);
 
-    log::info!(target: "file", "Rewriting model...");
+    tracing::info!("Rewriting model...");
 
     if cli.use_optimising_rewriter {
-        log::info!(target: "file", "Using the dirty-clean rewriter...");
+        tracing::info!("Using the dirty-clean rewriter...");
         model = rewrite_model(&model, &rule_sets)?;
     } else {
-        log::info!(target: "file", "Rewriting model...");
+        tracing::info!("Rewriting model...");
         model = rewrite_naive(&model, &rule_sets, false)?;
     }
 
-    let constraints_string = pretty_expressions_as_top_level(&model.constraints);
-    tracing::info!(constraints=%constraints_string, model=%json!(model),"Rewritten model");
+    tracing::info!("Rewritten model: \n{}\n", model);
 
     let solutions = get_minion_solutions(model, cli.number_of_solutions)?; // ToDo we need to properly set the solver adaptor here, not hard code minion
-    log::info!(target: "file", "Solutions: {}", minion_solutions_to_json(&solutions));
+    tracing::info!(target: "file", "Solutions: {}", minion_solutions_to_json(&solutions));
 
     let solutions_json = minion_solutions_to_json(&solutions);
     let solutions_str = to_string_pretty(&solutions_json)?;

conjure_oxide/src/utils/essence_parser.rs

@@ -13,8 +13,7 @@ use crate::utils::conjure::EssenceParseError;
 use conjure_core::context::Context;
 use conjure_core::metadata::Metadata;
 use conjure_core::Model;
-use std::collections::BTreeSet;
-use std::collections::HashMap;
+use std::collections::{BTreeMap, BTreeSet};
 
 pub fn parse_essence_file_native(
     path: &str,
@@ -72,7 +71,7 @@ fn get_tree(path: &str, filename: &str, extension: &str) -> (Tree, String) {
 fn parse_find_statement(
     find_statement_list: Node,
     source_code: &str,
-) -> HashMap<Name, DecisionVariable> {
+) -> BTreeMap<Name, DecisionVariable> {
     let mut symbol_table = SymbolTable::new();
 
     for find_statement in named_children(&find_statement_list) {

conjure_oxide/tests/generated_tests.rs

@@ -177,7 +177,7 @@ fn integration_test_inner(
     // Stage 1: Read the essence file and check that the model is parsed correctly
     let model = parse_essence_file(path, essence_base, extension, context.clone())?;
     if verbose {
-        println!("Parsed model: {:#?}", model)
+        println!("Parsed model: {}", model)
     }
 
     context.as_ref().write().unwrap().file_name =
@@ -186,7 +186,7 @@ fn integration_test_inner(
     save_model_json(&model, path, essence_base, "parse", accept)?;
     let expected_model = read_model_json(path, essence_base, "expected", "parse")?;
     if verbose {
-        println!("Expected model: {:#?}", expected_model)
+        println!("Expected model: {}", expected_model)
     }
 
     assert_eq!(model, expected_model);
@@ -202,10 +202,21 @@ fn integration_test_inner(
     // } else {
     //     rewrite_model(&model, &rule_sets)?
     // };
+
+    tracing::trace!(
+        target: "rule_engine_human",
+        "Model before rewriting:\n\n{}\n--\n",
+        model
+    );
     let model = rewrite_naive(&model, &rule_sets, false)?;
 
+    tracing::trace!(
+        target: "rule_engine_human",
+        "Final model:\n\n{}",
+        model
+    );
     if verbose {
-        println!("Rewritten model: {:#?}", model)
+        println!("Rewritten model: {}", model)
     }
 
     save_model_json(&model, path, essence_base, "rewrite", accept)?;
@@ -223,7 +234,7 @@ fn integration_test_inner(
 
     let expected_model = read_model_json(path, essence_base, "expected", "rewrite")?;
     if verbose {
-        println!("Expected model: {:#?}", expected_model)
+        println!("Expected model: {}", expected_model)
     }
 
     assert_eq!(model, expected_model);

conjure_oxide/tests/integration/basic/bool/01/bool-01-expected-rule-trace-human.txt

@@ -0,0 +1,18 @@
+Model before rewriting:
+
+find x: bool
+
+such that
+
+
+
+--
+
+Final model:
+
+find x: bool
+
+such that
+
+
+

conjure_oxide/tests/integration/basic/bool/02/bool-02-expected-rule-trace-human.txt

@@ -0,0 +1,20 @@
+Model before rewriting:
+
+find x: bool
+find y: bool
+
+such that
+
+
+
+--
+
+Final model:
+
+find x: bool
+find y: bool
+
+such that
+
+
+

conjure_oxide/tests/integration/basic/bool/03/bool-03-expected-rule-trace-human.txt

@@ -0,0 +1,20 @@
+Model before rewriting:
+
+find x: bool
+find y: bool
+
+such that
+
+(x != y)
+
+--
+
+Final model:
+
+find x: bool
+find y: bool
+
+such that
+
+(x != y)
+

conjure_oxide/tests/integration/basic/bool/04/bool-04-expected-rule-trace-human.txt

@@ -0,0 +1,24 @@
+Model before rewriting:
+
+find x: bool
+find y: bool
+find z: int(42)
+
+such that
+
+(x = true),
+(y != false)
+
+--
+
+Final model:
+
+find x: bool
+find y: bool
+find z: int(42)
+
+such that
+
+(x = true),
+(y != false)
+

conjure_oxide/tests/integration/basic/div/01/input-expected-rule-trace-human.txt

@@ -1,3 +1,14 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+
+such that
+
+(UnsafeDiv(a, b) = 1)
+
+--
+
 UnsafeDiv(a, b), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(a, b) @ (b != 0)} 
@@ -28,3 +39,12 @@ DivEq(a, b, 1)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+
+such that
+
+And([DivEq(a, b, 1), (b != 0)])
+

conjure_oxide/tests/integration/basic/div/02/input-expected-rule-trace-human.txt

@@ -1,3 +1,13 @@
+Model before rewriting:
+
+find a: int(0..3)
+
+such that
+
+(a >= UnsafeDiv(4, 2))
+
+--
+
 UnsafeDiv(4, 2), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
 2 
@@ -10,3 +20,11 @@ Ineq(2, a, 0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+
+such that
+
+Ineq(2, a, 0)
+

conjure_oxide/tests/integration/basic/div/03/input-expected-rule-trace-human.txt

@@ -1,3 +1,13 @@
+Model before rewriting:
+
+find a: int(0..9)
+
+such that
+
+(2 = UnsafeDiv(8, a))
+
+--
+
 UnsafeDiv(8, a), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(8, a) @ (a != 0)} 
@@ -28,3 +38,11 @@ DivEq(8, a, 2)
 
 --
 
+Final model:
+
+find a: int(0..9)
+
+such that
+
+And([DivEq(8, a, 2), (a != 0)])
+

conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt

@@ -1,3 +1,15 @@
+Model before rewriting:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+
+such that
+
+Not((a = UnsafeDiv(b, c)))
+
+--
+
 UnsafeDiv(b, c), 
    ~~> div_to_bubble ([("Bubble", 6000)]) 
 {SafeDiv(b, c) @ (c != 0)} 
@@ -55,3 +67,15 @@ DivEq(b, c, __0)
 
 --
 
+Final model:
+
+find a: int(0..3)
+find b: int(0..3)
+find c: int(0..3)
+find __0: int(0..3)
+
+such that
+
+Or([(a != __0), (c = 0)]),
+DivEq(b, c, __0)
+