From fb407f3f385c9ea4079f65022e673ca7fee151da Mon Sep 17 00:00:00 2001 From: Pedro Gronda Garrigues Date: Wed, 21 Feb 2024 20:09:14 +0000 Subject: [PATCH] Model example library for testing (#157) * Eliminated example/ dir to integrate with conjure_oxide/tests/integration dir * init attempt for generate_custom.rs for example custom string input * Added comprehension and enumerate essence file examples * generate_custom.rs temporary fix for walkdir filter filename [DOESN'T COMPILE] * added finite given [set] tests * fix for generate_custom.rs get_example_model: only filename and correct walkdir filter * added 'interesting tests' to integration test dir * fix dependencies in main.rs for custom_example * (ignore) playing around with code coverage sample yml file * final changes custom return model function * changed main.rs cfg tests to xyz instead of bool (no current support) * eliminated yaml code-coverage file for PR test passing * debug boolean 01/02/03 integration test with cargo test * removed conjure-output for basic/01 bool tests folder --- conjure_oxide/Cargo.toml | 3 +- conjure_oxide/src/generate_custom.rs | 160 ++++++++++++++++++ conjure_oxide/src/lib.rs | 1 + conjure_oxide/src/main.rs | 30 ++++ conjure_oxide/tests/generated_tests.rs | 2 +- .../tests/integration/abc/abc.essence.disabed | 0 .../comprehension-01-1.essence.disabled | 4 + .../comprehension-01-2.essence.disabled | 7 + .../comprehension-02-1.essence.disabled | 4 + .../comprehension-02-2.essence.disabled | 8 + .../comprehension-03-1.essence.disabled | 4 + .../comprehension-03-2.essence.disabled | 7 + .../comprehension-04-1.essence.disabled | 4 + .../comprehension-04-2.essence.disabled | 8 + .../basic/enum-01/enum-01.essence.disabled | 11 ++ .../basic/enum-02/enum-02.essence.disabled | 8 + .../basic/enum-03/enum-03.essence.disabled | 9 + .../finite-givens-set01.essence.disabled | 7 + .../finite-givens-set-02.essence.disabled | 4 + .../finite-givens-set03.essence.disabled | 9 + .../finite-givens-set04.essence.disabled | 5 + .../finite-givens-set05.essence.disabled | 5 + .../cyclic-graph/cyc1.param | 7 + .../cyclic-graph/cyc2.param | 8 + .../cyclic_graph.essence.disabled | 30 ++++ .../gchq-2016/gchq.essence.disabled | 95 +++++++++++ .../mildly-interesting/gchq-2016/inst.param | 86 ++++++++++ .../mildly-interesting/subset-sum/p1.param | 4 + .../mildly-interesting/subset-sum/p2.param | 4 + .../subset-sum/subsetSum.essence.disabled | 8 + .../xkcd287/xkcd287.essence.disabled | 23 +++ examples/abc.json | 62 ------- 32 files changed, 563 insertions(+), 64 deletions(-) create mode 100644 conjure_oxide/src/generate_custom.rs rename examples/abc.essence => conjure_oxide/tests/integration/abc/abc.essence.disabed (100%) create mode 100644 conjure_oxide/tests/integration/basic/comprehension-01-1/comprehension-01-1.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/comprehension-01-2/comprehension-01-2.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/comprehension-02-1/comprehension-02-1.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/comprehension-02-2/comprehension-02-2.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/comprehension-03-1/comprehension-03-1.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/comprehension-03-2/comprehension-03-2.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/comprehension-04-1/comprehension-04-1.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/comprehension-04-2/comprehension-04-2.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/enum-01/enum-01.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/enum-02/enum-02.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/enum-03/enum-03.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/finite-givens-set01/finite-givens-set01.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/finite-givens-set02/finite-givens-set-02.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/finite-givens-set03/finite-givens-set03.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/finite-givens-set04/finite-givens-set04.essence.disabled create mode 100644 conjure_oxide/tests/integration/basic/finite-givens-set05/finite-givens-set05.essence.disabled create mode 100644 conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyc1.param create mode 100644 conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyc2.param create mode 100644 conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyclic_graph.essence.disabled create mode 100644 conjure_oxide/tests/integration/mildly-interesting/gchq-2016/gchq.essence.disabled create mode 100644 conjure_oxide/tests/integration/mildly-interesting/gchq-2016/inst.param create mode 100644 conjure_oxide/tests/integration/mildly-interesting/subset-sum/p1.param create mode 100644 conjure_oxide/tests/integration/mildly-interesting/subset-sum/p2.param create mode 100644 conjure_oxide/tests/integration/mildly-interesting/subset-sum/subsetSum.essence.disabled create mode 100644 conjure_oxide/tests/integration/mildly-interesting/xkcd287/xkcd287.essence.disabled delete mode 100644 examples/abc.json diff --git a/conjure_oxide/Cargo.toml b/conjure_oxide/Cargo.toml index 382a86e3c0..27152b6367 100644 --- a/conjure_oxide/Cargo.toml +++ b/conjure_oxide/Cargo.toml @@ -22,7 +22,8 @@ clap = { version = "4.5.1", features = ["derive"] } strum_macros = "0.26.1" strum = "0.26.1" versions = "6.1.0" -linkme = "0.3.23" +linkme = "0.3.22" +walkdir = "2.4.0" [features] diff --git a/conjure_oxide/src/generate_custom.rs b/conjure_oxide/src/generate_custom.rs new file mode 100644 index 0000000000..a3670319e1 --- /dev/null +++ b/conjure_oxide/src/generate_custom.rs @@ -0,0 +1,160 @@ +// generate_custom.rs with get_example_model function + +// dependencies +use crate::parse::model_from_json; +use conjure_core::ast::Model; +use std::env; +use std::error::Error; +use std::fs::{copy, read_to_string, File}; +use std::io::Write; +use std::path::PathBuf; +use walkdir::WalkDir; + +use serde_json::Value; + +/// Searches recursively in `../tests/integration` folder for an `.essence` file matching the given filename, +/// then uses conjure to process it into astjson, and returns the parsed model. +/// +/// # Arguments +/// +/// * `filename` - A string slice that holds filename without extension +/// +/// # Returns +/// +/// Function returns a `Result>`, where `Value` is the parsed model +pub fn get_example_model(filename: &str) -> Result> { + // define relative path -> integration tests dir + let base_dir = "tests/integration"; + let mut essence_path = PathBuf::new(); + + // walk through directory tree recursively starting at base + for entry in WalkDir::new(base_dir).into_iter().filter_map(|e| e.ok()) { + let path = entry.path(); + if path.is_file() + && path.extension().map_or(false, |e| e == "essence") + && path.file_stem() == Some(std::ffi::OsStr::new(filename)) + { + essence_path = path.to_path_buf(); + break; + } + } + + println!("PATH TO FILE: {}", essence_path.display()); + + // return error if file not found + if essence_path.as_os_str().is_empty() { + return Err(Box::new(std::io::Error::new( + std::io::ErrorKind::NotFound, + "ERROR: File not found in any subdirectory", + ))); + } + + // let path = PathBuf::from(format!("../tests/integration/basic/comprehension{}.essence", filename)); + let mut cmd = std::process::Command::new("conjure"); + let output = cmd + .arg("pretty") + .arg("--output-format=astjson") + .arg(essence_path) + .output()?; + + // convert Conjure's stdout from bytes to string + let astjson = String::from_utf8(output.stdout)?; + + println!("ASTJSON: {}", astjson); + + // parse AST JSON from desired Model format + let generated_mdl = model_from_json(&astjson)?; + + Ok(generated_mdl) +} + +/// Searches for an `.essence` file at the given filepath, +/// then uses conjure to process it into astjson, and returns the parsed model. +/// +/// # Arguments +/// +/// * `filepath` - A string slice that holds the full file path +/// +/// # Returns +/// +/// Function returns a `Result>`, where `Value` is the parsed model +pub fn get_example_model_by_path(filepath: &str) -> Result> { + let essence_path = PathBuf::from(filepath); + + // return error if file not found + if essence_path.as_os_str().is_empty() { + return Err(Box::new(std::io::Error::new( + std::io::ErrorKind::NotFound, + "ERROR: File not found in any subdirectory", + ))); + } + + println!("PATH TO FILE: {}", essence_path.display()); + + // Command execution using 'conjure' CLI tool with provided path + let mut cmd = std::process::Command::new("conjure"); + let output = cmd + .arg("pretty") + .arg("--output-format=astjson") + .arg(&essence_path) + .output()?; + + // convert Conjure's stdout from bytes to string + let astjson = String::from_utf8(output.stdout)?; + + println!("ASTJSON: {}", astjson); + + // parse AST JSON into the desired Model format + let generated_model = model_from_json(&astjson)?; + + Ok(generated_model) +} + +/// Recursively sorts the keys of all JSON objects within the provided JSON value. +/// +/// serde_json will output JSON objects in an arbitrary key order. +/// this is normally fine, except in our use case we wouldn't want to update the expected output again and again. +/// so a consistent (sorted) ordering of the keys is desirable. +fn sort_json_object(value: &Value) -> Value { + match value { + Value::Object(obj) => { + let mut ordered: Vec<(String, Value)> = obj + .iter() + .map(|(k, v)| { + if k == "variables" { + (k.clone(), sort_json_variables(v)) + } else { + (k.clone(), sort_json_object(v)) + } + }) + // .map(|(k, v)| (k.clone(), sort_json_object(v))) + .collect(); + ordered.sort_by(|a, b| a.0.cmp(&b.0)); + + Value::Object(ordered.into_iter().collect()) + } + Value::Array(arr) => Value::Array(arr.iter().map(sort_json_object).collect()), + _ => value.clone(), + } +} + +/// Sort the "variables" field by name. +/// We have to do this separately becasue that field is not a JSON object, instead it's an array of tuples. +fn sort_json_variables(value: &Value) -> Value { + match value { + Value::Array(vars) => { + let mut vars_sorted = vars.clone(); + vars_sorted.sort_by(|a, b| { + let a_obj = &a.as_array().unwrap()[0]; + let a_name: crate::ast::Name = serde_json::from_value(a_obj.clone()).unwrap(); + + let b_obj = &b.as_array().unwrap()[0]; + let b_name: crate::ast::Name = serde_json::from_value(b_obj.clone()).unwrap(); + + a_name.cmp(&b_name) + }); + Value::Array(vars_sorted) + } + _ => value.clone(), + } +} diff --git a/conjure_oxide/src/lib.rs b/conjure_oxide/src/lib.rs index fc7315617e..4435dffd5a 100644 --- a/conjure_oxide/src/lib.rs +++ b/conjure_oxide/src/lib.rs @@ -2,6 +2,7 @@ pub mod error; pub mod find_conjure; +pub mod generate_custom; pub mod parse; pub mod rule_engine; mod rules; diff --git a/conjure_oxide/src/main.rs b/conjure_oxide/src/main.rs index 5d244613d5..a3e8bfa332 100644 --- a/conjure_oxide/src/main.rs +++ b/conjure_oxide/src/main.rs @@ -10,6 +10,7 @@ use std::sync::Mutex; use anyhow::Result as AnyhowResult; use clap::{arg, command, Parser}; use conjure_oxide::find_conjure::conjure_executable; +use conjure_oxide::generate_custom::{get_example_model, get_example_model_by_path}; use conjure_oxide::parse::model_from_json; use conjure_oxide::rule_engine::resolve_rules::{ get_rule_priorities, get_rules_vec, resolve_rule_sets, @@ -121,3 +122,32 @@ pub fn main() -> AnyhowResult<()> { Ok(()) } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_get_example_model_success() { + let filename = "input"; + get_example_model(filename).unwrap(); + } + + #[test] + fn test_get_example_model_by_filepath() { + let filepath = "tests/integration/xyz/input.essence"; + get_example_model_by_path(filepath).unwrap(); + } + + #[test] + fn test_get_example_model_fail_empty_filename() { + let filename = ""; + get_example_model(filename).unwrap_err(); + } + + #[test] + fn test_get_example_model_fail_empty_filepath() { + let filepath = ""; + get_example_model_by_path(filepath).unwrap_err(); + } +} diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs index 9c35e63dff..8159ef002f 100644 --- a/conjure_oxide/tests/generated_tests.rs +++ b/conjure_oxide/tests/generated_tests.rs @@ -24,7 +24,7 @@ fn main() { } } -fn integration_test(path: &str, essence_base: &str) -> Result<(), Box> { +pub fn integration_test(path: &str, essence_base: &str) -> Result<(), Box> { // -------------------------------------------------------------------------------- // -- parsing the essence file diff --git a/examples/abc.essence b/conjure_oxide/tests/integration/abc/abc.essence.disabed similarity index 100% rename from examples/abc.essence rename to conjure_oxide/tests/integration/abc/abc.essence.disabed diff --git a/conjure_oxide/tests/integration/basic/comprehension-01-1/comprehension-01-1.essence.disabled b/conjure_oxide/tests/integration/basic/comprehension-01-1/comprehension-01-1.essence.disabled new file mode 100644 index 0000000000..e505aeda43 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/comprehension-01-1/comprehension-01-1.essence.disabled @@ -0,0 +1,4 @@ +language Essence 1.3 + +find x : int(0..1000) +such that x = sum([ 1 | i : set (size 2) of int(7..9) ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/comprehension-01-2/comprehension-01-2.essence.disabled b/conjure_oxide/tests/integration/basic/comprehension-01-2/comprehension-01-2.essence.disabled new file mode 100644 index 0000000000..2ea06c74e8 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/comprehension-01-2/comprehension-01-2.essence.disabled @@ -0,0 +1,7 @@ +language Essence 1.3 + +find x : int(0..1000) +find y : int(7,8) +such that x = sum([ 1 | i : set (size 2) of int(7..9) + , y in i + ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/comprehension-02-1/comprehension-02-1.essence.disabled b/conjure_oxide/tests/integration/basic/comprehension-02-1/comprehension-02-1.essence.disabled new file mode 100644 index 0000000000..310055077b --- /dev/null +++ b/conjure_oxide/tests/integration/basic/comprehension-02-1/comprehension-02-1.essence.disabled @@ -0,0 +1,4 @@ +language Essence 1.3 + +find x : int(0..1000) +such that x = sum([ j | i : set (minSize 1, maxSize 2) of int(7..8), j <- i ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/comprehension-02-2/comprehension-02-2.essence.disabled b/conjure_oxide/tests/integration/basic/comprehension-02-2/comprehension-02-2.essence.disabled new file mode 100644 index 0000000000..cf83c925de --- /dev/null +++ b/conjure_oxide/tests/integration/basic/comprehension-02-2/comprehension-02-2.essence.disabled @@ -0,0 +1,8 @@ +language Essence 1.3 + +find x : int(0..1000) +find y : int(7,8) +such that x = sum([ j | i : set (minSize 1, maxSize 2) of int(7..8) + , y in i + , j <- i + ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/comprehension-03-1/comprehension-03-1.essence.disabled b/conjure_oxide/tests/integration/basic/comprehension-03-1/comprehension-03-1.essence.disabled new file mode 100644 index 0000000000..da4a072692 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/comprehension-03-1/comprehension-03-1.essence.disabled @@ -0,0 +1,4 @@ +language Essence 1.3 + +find x : int(0..1000) +such that x = sum([ 1 | i : set (minSize 1, maxSize 2) of int(7..9) ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/comprehension-03-2/comprehension-03-2.essence.disabled b/conjure_oxide/tests/integration/basic/comprehension-03-2/comprehension-03-2.essence.disabled new file mode 100644 index 0000000000..a7eda51c6d --- /dev/null +++ b/conjure_oxide/tests/integration/basic/comprehension-03-2/comprehension-03-2.essence.disabled @@ -0,0 +1,7 @@ +language Essence 1.3 + +find x : int(0..1000) +find y : int(7,8) +such that x = sum([ 1 | i : set (minSize 1, maxSize 2) of int(7..9) + , y in i + ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/comprehension-04-1/comprehension-04-1.essence.disabled b/conjure_oxide/tests/integration/basic/comprehension-04-1/comprehension-04-1.essence.disabled new file mode 100644 index 0000000000..adc73bb45a --- /dev/null +++ b/conjure_oxide/tests/integration/basic/comprehension-04-1/comprehension-04-1.essence.disabled @@ -0,0 +1,4 @@ +language Essence 1.3 + +find x : int(0..1000) +such that x = sum([ 1 | i : set (minSize 1, maxSize 2) of (int(7..9), bool) ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/comprehension-04-2/comprehension-04-2.essence.disabled b/conjure_oxide/tests/integration/basic/comprehension-04-2/comprehension-04-2.essence.disabled new file mode 100644 index 0000000000..199ec4927f --- /dev/null +++ b/conjure_oxide/tests/integration/basic/comprehension-04-2/comprehension-04-2.essence.disabled @@ -0,0 +1,8 @@ +language Essence 1.3 + +find x : int(0..1000) +find y : int(7,8) +find z : bool +such that x = sum([ 1 | i : set (minSize 1, maxSize 2) of (int(7..9), bool) + , (y,z) in i + ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/enum-01/enum-01.essence.disabled b/conjure_oxide/tests/integration/basic/enum-01/enum-01.essence.disabled new file mode 100644 index 0000000000..9fbf96f58f --- /dev/null +++ b/conjure_oxide/tests/integration/basic/enum-01/enum-01.essence.disabled @@ -0,0 +1,11 @@ +language Essence 1.3 + +given E1 new type enum +find x : E1 + +letting E2 be new type enum {a,b,c,d} +find y : E2 +find z : E2(a..c) +find t : E2(b,d) + +such that y = z, z = t \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/enum-02/enum-02.essence.disabled b/conjure_oxide/tests/integration/basic/enum-02/enum-02.essence.disabled new file mode 100644 index 0000000000..d808e204cf --- /dev/null +++ b/conjure_oxide/tests/integration/basic/enum-02/enum-02.essence.disabled @@ -0,0 +1,8 @@ +language Essence 1.3 + +given E1 new type enum +letting E2 be new type enum {a,b,c,d} + +find x : (E1, E2) + +such that x[2] = a \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/enum-03/enum-03.essence.disabled b/conjure_oxide/tests/integration/basic/enum-03/enum-03.essence.disabled new file mode 100644 index 0000000000..953cbd67e0 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/enum-03/enum-03.essence.disabled @@ -0,0 +1,9 @@ +language Essence 1.3 + +given E1 new type enum +find x : E1 +such that forAll i : E1 . x <= i + +letting E2 be new type enum {a,b,c,d} +find y : E2 +such that forAll j : E2 . y <= j \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/finite-givens-set01/finite-givens-set01.essence.disabled b/conjure_oxide/tests/integration/basic/finite-givens-set01/finite-givens-set01.essence.disabled new file mode 100644 index 0000000000..8ed21ce1e4 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/finite-givens-set01/finite-givens-set01.essence.disabled @@ -0,0 +1,7 @@ +language Essence 1.3 + +given a : set of int +find x,y,z : int(0..100) +such that x = |a| +such that y = min(a) +such that z = max(a) diff --git a/conjure_oxide/tests/integration/basic/finite-givens-set02/finite-givens-set-02.essence.disabled b/conjure_oxide/tests/integration/basic/finite-givens-set02/finite-givens-set-02.essence.disabled new file mode 100644 index 0000000000..d6d9e6d3bd --- /dev/null +++ b/conjure_oxide/tests/integration/basic/finite-givens-set02/finite-givens-set-02.essence.disabled @@ -0,0 +1,4 @@ +language Essence 1.3 + +given a : set of int +find x : int(|a|) diff --git a/conjure_oxide/tests/integration/basic/finite-givens-set03/finite-givens-set03.essence.disabled b/conjure_oxide/tests/integration/basic/finite-givens-set03/finite-givens-set03.essence.disabled new file mode 100644 index 0000000000..f98f480550 --- /dev/null +++ b/conjure_oxide/tests/integration/basic/finite-givens-set03/finite-givens-set03.essence.disabled @@ -0,0 +1,9 @@ +language Essence 1.3 + +given a : set of int +find x,y,z,t : int(0..100) +such that x = |a| +such that y = min(a) +such that z = max(a) +such that allDiff([x,y,z,t]) +such that t in a $ refer to a diff --git a/conjure_oxide/tests/integration/basic/finite-givens-set04/finite-givens-set04.essence.disabled b/conjure_oxide/tests/integration/basic/finite-givens-set04/finite-givens-set04.essence.disabled new file mode 100644 index 0000000000..221c83964b --- /dev/null +++ b/conjure_oxide/tests/integration/basic/finite-givens-set04/finite-givens-set04.essence.disabled @@ -0,0 +1,5 @@ +language Essence 1.3 + +given a : set of set of int +find x : int(-1000..1000) +such that x = max([ max(i) | i <- a ]) diff --git a/conjure_oxide/tests/integration/basic/finite-givens-set05/finite-givens-set05.essence.disabled b/conjure_oxide/tests/integration/basic/finite-givens-set05/finite-givens-set05.essence.disabled new file mode 100644 index 0000000000..ef61e904cc --- /dev/null +++ b/conjure_oxide/tests/integration/basic/finite-givens-set05/finite-givens-set05.essence.disabled @@ -0,0 +1,5 @@ +language Essence 1.3 + +given s: set of set (minSize 0) of int(2..5, 4) +find x : int(0..9) +such that exists s' in s . x in s' diff --git a/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyc1.param b/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyc1.param new file mode 100644 index 0000000000..9f4a5cf82c --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyc1.param @@ -0,0 +1,7 @@ +language Essence 1.3 + +letting n be 5 +letting g be relation + ( (1,2) + , (2,1) + ) diff --git a/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyc2.param b/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyc2.param new file mode 100644 index 0000000000..7a82fb869c --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyc2.param @@ -0,0 +1,8 @@ +language Essence 1.3 + +letting n be 5 +letting g be relation + ( (1,2) + , (2,3) + , (3,1) + ) diff --git a/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyclic_graph.essence.disabled b/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyclic_graph.essence.disabled new file mode 100644 index 0000000000..78fb842f2c --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/cyclic-graph/cyclic_graph.essence.disabled @@ -0,0 +1,30 @@ +language Essence 1.3 + +given n : int +letting N be domain int(1..n) +given g : relation of (N * N) + +$ where +$ forAll (i,j) in g . $ i is directly connected to j +$ $ there cannot be a path from j to i +$ !( +$ +$ $ an immediate connection from j to i +$ ((j,i) in g) +$ +$ \/ +$ +$ $ a path where number of nodes is between 1 and (n-2) +$ (exists path : sequence (minSize 1, maxSize n-2, injective) of N . +$ +$ $ j is connected to the first node in `path` +$ (j, path(1)) in g +$ +$ $ the last node in `path` is connected to i +$ /\ (path(|path|), i) in g +$ +$ $ and adjacent nodes in `path` are connected +$ /\ and([ (path(x), path(x+1)) in g | x : int(1..|path|-1) ])) +$ ) + +find b : int(0) diff --git a/conjure_oxide/tests/integration/mildly-interesting/gchq-2016/gchq.essence.disabled b/conjure_oxide/tests/integration/mildly-interesting/gchq-2016/gchq.essence.disabled new file mode 100644 index 0000000000..b8c116fc13 --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/gchq-2016/gchq.essence.disabled @@ -0,0 +1,95 @@ +language Essence 1.3 + +$ from: http://www.bbc.co.uk/news/uk-35058761 + +given n : int $ board size +letting ADDR be domain int(1..n) + +given horizontalClues : matrix indexed by [ADDR] of sequence (maxSize n) of ADDR $ per row +find horizontalLocs : matrix indexed by [ADDR] of sequence (maxSize n) of ADDR $ starting positions of each shape +such that + forAll row : ADDR . |horizontalLocs[row]| = |horizontalClues[row]| +such that + forAll row : ADDR . forAll (index, _) in horizontalClues[row] , index > 1 . + horizontalLocs[row](index) > horizontalLocs[row](index-1) + horizontalClues[row](index-1) + +given verticalClues : matrix indexed by [ADDR] of sequence (maxSize n) of ADDR $ per column +find verticalLocs : matrix indexed by [ADDR] of sequence (maxSize n) of ADDR $ starting positions of each shape +such that + forAll col : ADDR . |verticalLocs[col]| = |verticalClues[col]| +such that + forAll col : ADDR . forAll (index, _) in verticalClues[col] , index > 1 . + verticalLocs[col](index) > verticalLocs[col](index-1) + verticalClues[col](index-1) + +find bitmap : matrix indexed by [ADDR, ADDR] of bool + +given prefilled : set of (ADDR, ADDR) +such that + forAll (i,j) in prefilled . bitmap[i,j] = true + + +$ channelling the horizontal placements to the bitmap +such that + and([ and([ bitmap[row,i] = true $ the shape itself + | i : ADDR + , i >= thisStart + , i <= thisFinish + ]) /\ + and([ bitmap[row,i] = false $ the shape is the first, before it is empty + | i : ADDR + , i < thisStart + , index = 1 $ (the first) + ]) /\ + and([ bitmap[row,i] = false $ the shape is the last, after it is empty + | i : ADDR + , i > thisFinish + , index = lastIndex $ (the last) + ]) /\ + and([ bitmap[row,i] = false $ the shape is in the middle, the gap is empty + | i : ADDR + , letting nextStart be horizontalLocs[row](index+1) + , i > thisFinish + , i < nextStart + , index < lastIndex $ (in the middle) + ]) + | row : ADDR + , letting lastIndex be |horizontalClues[row]| + , index : ADDR + , index <= lastIndex + , letting thisStart be horizontalLocs[row](index) + , letting thisWidth be horizontalClues[row](index) + , letting thisFinish be thisStart + thisWidth - 1 + ]) + +$ channelling the vertical placements to the bitmap +such that + and([ and([ bitmap[i,col] = true $ the shape itself + | i : ADDR + , i >= thisStart + , i <= thisFinish + ]) /\ + and([ bitmap[i,col] = false $ the shape is the first, before it is empty + | i : ADDR + , i < thisStart + , index = 1 $ (the first) + ]) /\ + and([ bitmap[i,col] = false $ the shape is the last, after it is empty + | i : ADDR + , i > thisFinish + , index = lastIndex $ (the last) + ]) /\ + and([ bitmap[i,col] = false $ the shape is in the middle, the gap is empty + | i : ADDR + , letting nextStart be verticalLocs[col](index+1) + , i > thisFinish + , i < nextStart + , index < lastIndex $ (in the middle) + ]) + | col : ADDR + , letting lastIndex be |verticalClues[col]| + , index : ADDR + , index <= lastIndex + , letting thisStart be verticalLocs[col](index) + , letting thisWidth be verticalClues[col](index) + , letting thisFinish be thisStart + thisWidth - 1 + ]) \ No newline at end of file diff --git a/conjure_oxide/tests/integration/mildly-interesting/gchq-2016/inst.param b/conjure_oxide/tests/integration/mildly-interesting/gchq-2016/inst.param new file mode 100644 index 0000000000..c8f0b140d6 --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/gchq-2016/inst.param @@ -0,0 +1,86 @@ +language Essence 1.3 + +$ from: http://www.bbc.co.uk/news/uk-35058761 + +letting n be 25 + +letting horizontalClues be + [ sequence(7, 3, 1, 1, 7) + , sequence(1, 1, 2, 2, 1, 1) + , sequence(1, 3, 1, 3, 1, 1, 3, 1) + , sequence(1, 3, 1, 1, 6, 1, 3, 1) + , sequence(1, 3, 1, 5, 2, 1, 3, 1) + , sequence(1, 1, 2, 1, 1) + , sequence(7, 1, 1, 1, 1, 1, 7) + , sequence(3, 3) + , sequence(1, 2, 3, 1, 1, 3, 1, 1, 2) + , sequence(1, 1, 3, 2, 1, 1) + , sequence(4, 1, 4, 2, 1, 2) + , sequence(1, 1, 1, 1, 1, 4, 1, 3) + , sequence(2, 1, 1, 1, 2, 5) + , sequence(3, 2, 2, 6, 3, 1) + , sequence(1, 9, 1, 1, 2, 1) + , sequence(2, 1, 2, 2, 3, 1) + , sequence(3, 1, 1, 1, 1, 5, 1) + , sequence(1, 2, 2, 5) + , sequence(7, 1, 2, 1, 1, 1, 3) + , sequence(1, 1, 2, 1, 2, 2, 1) + , sequence(1, 3, 1, 4, 5, 1) + , sequence(1, 3, 1, 3, 10, 2) + , sequence(1, 3, 1, 1, 6, 6) + , sequence(1, 1, 2, 1, 1, 2) + , sequence(7, 2, 1, 2, 5) + ] + +letting verticalClues be + [ sequence(7, 2, 1, 1, 7) + , sequence(1, 1, 2, 2, 1, 1) + , sequence(1, 3, 1, 3, 1, 3, 1, 3, 1) + , sequence(1, 3, 1, 1, 5, 1, 3, 1) + , sequence(1, 3, 1, 1, 4, 1, 3, 1) + , sequence(1, 1, 1, 2, 1, 1) + , sequence(7, 1, 1, 1, 1, 1, 7) + , sequence(1, 1, 3) + , sequence(2, 1, 2, 1, 8, 2, 1) + , sequence(2, 2, 1, 2, 1, 1, 1, 2) + , sequence(1, 7, 3, 2, 1) + , sequence(1, 2, 3, 1, 1, 1, 1, 1) + , sequence(4, 1, 1, 2, 6) + , sequence(3, 3, 1, 1, 1, 3, 1) + , sequence(1, 2, 5, 2, 2) + , sequence(2, 2, 1, 1, 1, 1, 1, 2, 1) + , sequence(1, 3, 3, 2, 1, 8, 1) + , sequence(6, 2, 1) + , sequence(7, 1, 4, 1, 1, 3) + , sequence(1, 1, 1, 1, 4) + , sequence(1, 3, 1, 3, 7, 1) + , sequence(1, 3, 1, 1, 1, 2, 1, 1, 4) + , sequence(1, 3, 1, 4, 3, 3) + , sequence(1, 1, 2, 2, 2, 6, 1) + , sequence(7, 1, 3, 2, 1, 1) + ] + +letting prefilled be + { (4, 4) + , (4, 5) + , (4, 13) + , (4, 14) + , (4, 22) + , (9, 7) + , (9, 8) + , (9, 11) + , (9, 15) + , (9, 16) + , (9, 19) + , (17, 7) + , (17, 12) + , (17, 17) + , (17, 21) + , (22, 4) + , (22, 5) + , (22, 10) + , (22, 11) + , (22, 16) + , (22, 21) + , (22, 22) + } \ No newline at end of file diff --git a/conjure_oxide/tests/integration/mildly-interesting/subset-sum/p1.param b/conjure_oxide/tests/integration/mildly-interesting/subset-sum/p1.param new file mode 100644 index 0000000000..4e93c1cb57 --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/subset-sum/p1.param @@ -0,0 +1,4 @@ +language Essence 1.3 + +letting s be 0 +letting nums be {-7, -3, -2, 5, 8} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/mildly-interesting/subset-sum/p2.param b/conjure_oxide/tests/integration/mildly-interesting/subset-sum/p2.param new file mode 100644 index 0000000000..f116101214 --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/subset-sum/p2.param @@ -0,0 +1,4 @@ +language Essence 1.3 + +letting s be 0 +letting nums be {1, 2, 3, 4, -5} \ No newline at end of file diff --git a/conjure_oxide/tests/integration/mildly-interesting/subset-sum/subsetSum.essence.disabled b/conjure_oxide/tests/integration/mildly-interesting/subset-sum/subsetSum.essence.disabled new file mode 100644 index 0000000000..1cbe3764be --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/subset-sum/subsetSum.essence.disabled @@ -0,0 +1,8 @@ +language Essence 1.3 + +$ https://en.wikipedia.org/wiki/Subset_sum_problem + +given s : int +given nums : set of int +find x : set (minSize 1, maxSize |nums|) of int([ i | i <- nums]) +such that x subsetEq nums, s = sum i in x . i \ No newline at end of file diff --git a/conjure_oxide/tests/integration/mildly-interesting/xkcd287/xkcd287.essence.disabled b/conjure_oxide/tests/integration/mildly-interesting/xkcd287/xkcd287.essence.disabled new file mode 100644 index 0000000000..1a22f264ad --- /dev/null +++ b/conjure_oxide/tests/integration/mildly-interesting/xkcd287/xkcd287.essence.disabled @@ -0,0 +1,23 @@ + +$ see https://xkcd.com/287 + +letting appetizer be new type enum + { mixedFruit, frenchFries + , sideSalad, hotWings + , mozzarellaSticks, samplerPlate + } + +letting price be function + ( mixedFruit --> 215 + , frenchFries --> 275 + , sideSalad --> 335 + , hotWings --> 355 + , mozzarellaSticks --> 420 + , samplerPlate --> 580 + ) + +letting worth be 1505 + +find order : function appetizer --> int(1..10) + +such that worth = sum (a,n) in order . price(a) * n \ No newline at end of file diff --git a/examples/abc.json b/examples/abc.json deleted file mode 100644 index 30a6d503c2..0000000000 --- a/examples/abc.json +++ /dev/null @@ -1,62 +0,0 @@ -{"mInfo": - {"finds": [], "givens": [], "enumGivens": [], "enumLettings": [], "lettings": [], "unnameds": [], - "strategyQ": {"Auto": {"Interactive": []}}, "strategyA": {"Auto": {"Interactive": []}}, "trailCompact": [], - "nameGenState": [], "nbExtraGivens": 0, "representations": [], "representationsTree": [], "originalDomains": [], - "trailGeneralised": [], "trailVerbose": [], "trailRewrites": []}, - "mLanguage": {"language": {"Name": "Essence"}, "version": [1, 3]}, - "mStatements": - [{"Declaration": - {"FindOrGiven": - ["Find", {"Name": "a"}, - {"DomainInt": - [{"TagInt": []}, - [{"RangeBounded": - [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, - {"Constant": {"ConstantInt": [{"TagInt": []}, 3]}}]}]]}]}}, - {"Declaration": - {"FindOrGiven": - ["Find", {"Name": "b"}, - {"DomainInt": - [{"TagInt": []}, - [{"RangeBounded": - [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, - {"Constant": {"ConstantInt": [{"TagInt": []}, 3]}}]}]]}]}}, - {"Declaration": - {"FindOrGiven": - ["Find", {"Name": "c"}, - {"DomainInt": - [{"TagInt": []}, - [{"RangeSingle": {"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}}, - {"RangeSingle": {"Constant": {"ConstantInt": [{"TagInt": []}, 2]}}}, - {"RangeSingle": {"Constant": {"ConstantInt": [{"TagInt": []}, 3]}}}]]}]}}, - {"SuchThat": - [{"Op": - {"MkOpEq": - [{"Op": - {"MkOpSum": - {"AbstractLiteral": - {"AbsLitMatrix": - [{"DomainInt": - [{"TagInt": []}, - [{"RangeBounded": - [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, - {"Constant": {"ConstantInt": [{"TagInt": []}, 2]}}]}]]}, - [{"Op": - {"MkOpSum": - {"AbstractLiteral": - {"AbsLitMatrix": - [{"DomainInt": - [{"TagInt": []}, - [{"RangeBounded": - [{"Constant": - {"ConstantInt": - [{"TagInt": []}, 1]}}, - {"Constant": - {"ConstantInt": - [{"TagInt": []}, 2]}}]}]]}, - [{"Reference": [{"Name": "a"}, null]}, - {"Reference": [{"Name": "b"}, null]}]]}}}}, - {"Reference": [{"Name": "c"}, null]}]]}}}}, - {"Constant": {"ConstantInt": [{"TagInt": []}, 4]}}]}}]}, - {"SuchThat": - [{"Op": {"MkOpGeq": [{"Reference": [{"Name": "a"}, null]}, {"Reference": [{"Name": "b"}, null]}]}}]}]}