Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pretty print model as Essence #582

Merged
merged 4 commits into from
Jan 10, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions conjure_oxide/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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"
})
})
Expand All @@ -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"
})
})
Expand All @@ -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
Expand All @@ -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
Expand Down
29 changes: 13 additions & 16 deletions conjure_oxide/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
}
};
Expand All @@ -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
Expand All @@ -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"
))?;
Expand Down Expand Up @@ -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)?;
Expand Down
5 changes: 2 additions & 3 deletions conjure_oxide/src/utils/essence_parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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) {
Expand Down
19 changes: 15 additions & 4 deletions conjure_oxide/tests/generated_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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);
Expand All @@ -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)?;
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
Model before rewriting:

find x: bool

such that



--

Final model:

find x: bool

such that



Original file line number Diff line number Diff line change
@@ -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



Original file line number Diff line number Diff line change
@@ -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)

Original file line number Diff line number Diff line change
@@ -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)

Original file line number Diff line number Diff line change
@@ -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)}
Expand Down Expand Up @@ -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)])

Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -10,3 +20,11 @@ Ineq(2, a, 0)

--

Final model:

find a: int(0..3)

such that

Ineq(2, a, 0)

Original file line number Diff line number Diff line change
@@ -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)}
Expand Down Expand Up @@ -28,3 +38,11 @@ DivEq(8, a, 2)

--

Final model:

find a: int(0..9)

such that

And([DivEq(8, a, 2), (a != 0)])

Original file line number Diff line number Diff line change
@@ -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)}
Expand Down Expand Up @@ -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)

Loading
Loading