diff --git a/.github/workflows/code-coverage.yml b/.github/workflows/code-coverage.yml index 49f259d3b..a62476b7b 100644 --- a/.github/workflows/code-coverage.yml +++ b/.github/workflows/code-coverage.yml @@ -8,12 +8,14 @@ on: - Cargo.* - conjure-oxide/** - solvers/** + - crates/** - .github/actions/code-coverage.yml pull_request: paths: - Cargo.* - conjure-oxide/** - solvers/** + - crates/** - .github/actions/code-coverage.yml workflow_dispatch: diff --git a/.github/workflows/doc-coverage.yml b/.github/workflows/doc-coverage.yml index b3525e0da..aa5cfb79e 100644 --- a/.github/workflows/doc-coverage.yml +++ b/.github/workflows/doc-coverage.yml @@ -8,12 +8,14 @@ on: - Cargo.* - conjure-oxide/** - solvers/** + - crates/** - .github/actions/doc-coverage.yml pull_request: paths: - Cargo.* - conjure-oxide/** - solvers/** + - crates/** - .github/actions/doc-coverage.yml workflow_dispatch: diff --git a/.github/workflows/docs-deploy.yml b/.github/workflows/docs-deploy.yml index c77673292..f99d71472 100644 --- a/.github/workflows/docs-deploy.yml +++ b/.github/workflows/docs-deploy.yml @@ -42,7 +42,7 @@ jobs: uses: dawidd6/action-download-artifact@v2 with: name: docs-${{ steps.sha.outputs.result }} - workflow: docs.yml + workflow: docs-generate.yml path: ./deploy - name: Deploy to Github Pages diff --git a/.github/workflows/docs.yml b/.github/workflows/docs-generate.yml similarity index 100% rename from .github/workflows/docs.yml rename to .github/workflows/docs-generate.yml diff --git a/.github/workflows/format.yml b/.github/workflows/format.yml index e86856d72..ac52dce62 100644 --- a/.github/workflows/format.yml +++ b/.github/workflows/format.yml @@ -10,12 +10,14 @@ on: - Cargo.* - conjure-oxide/** - solvers/** + - crates/** - .github/actions/format.yml pull_request: paths: - Cargo.* - conjure-oxide/** - solvers/** + - crates/** - .github/actions/format.yml workflow_dispatch: diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 396cc68cc..52f137595 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -6,21 +6,25 @@ on: - main # run for pushes to the main branch. other branches need to create a PR if they want testing. paths: - conjure_oxide/** + - solvers/** + - crates/** - Cargo.* - .github/workflows/test.yml pull_request: paths: - conjure_oxide/** + - solvers/** + - crates/** - Cargo.* - .github/workflows/test.yml workflow_dispatch: - jobs: - - Job: - + build-and-test: + name: "Build and Test" strategy: + # run all combinations of the matrix even if one combination fails. + fail-fast: false matrix: rust_release: - stable @@ -57,7 +61,7 @@ jobs: - run: rustup update ${{ matrix.rust_release }} && rustup default ${{ matrix.rust_release }} - - run: cargo build -vv + - run: cargo build -vv --workspace - name: Add conjure to PATH run: echo "${HOME}/.cargo/bin/conjure-v${{ matrix.conjure_version }}-${{ matrix.release_suffix }}-with-solvers" >> ${GITHUB_PATH} @@ -76,6 +80,19 @@ jobs: fi conjure --version - - run: cargo test + - run: cargo test --workspace + audit: + name: "Dependency Audit" + runs-on: ubuntu-latest + strategy: + # run all combinations of the matrix even if one combination fails. + fail-fast: false + matrix: + rust_release: + - stable + - nightly + steps: + - uses: actions/checkout@v3 + - run: rustup update ${{ matrix.rust_release }} && rustup default ${{ matrix.rust_release }} - run: cargo audit diff --git a/.idea/.gitignore b/.idea/.gitignore new file mode 100644 index 000000000..13566b81b --- /dev/null +++ b/.idea/.gitignore @@ -0,0 +1,8 @@ +# Default ignored files +/shelf/ +/workspace.xml +# Editor-based HTTP Client requests +/httpRequests/ +# Datasource local storage ignored files +/dataSources/ +/dataSources.local.xml diff --git a/.idea/conjure-oxide.iml b/.idea/conjure-oxide.iml new file mode 100644 index 000000000..46331c8c5 --- /dev/null +++ b/.idea/conjure-oxide.iml @@ -0,0 +1,28 @@ + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/.idea/inspectionProfiles/Project_Default.xml b/.idea/inspectionProfiles/Project_Default.xml new file mode 100644 index 000000000..ec06bf780 --- /dev/null +++ b/.idea/inspectionProfiles/Project_Default.xml @@ -0,0 +1,41 @@ + + + + \ No newline at end of file diff --git a/.idea/inspectionProfiles/profiles_settings.xml b/.idea/inspectionProfiles/profiles_settings.xml new file mode 100644 index 000000000..105ce2da2 --- /dev/null +++ b/.idea/inspectionProfiles/profiles_settings.xml @@ -0,0 +1,6 @@ + + + + \ No newline at end of file diff --git a/.idea/misc.xml b/.idea/misc.xml new file mode 100644 index 000000000..3b9e0f3cb --- /dev/null +++ b/.idea/misc.xml @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/.idea/vcs.xml b/.idea/vcs.xml new file mode 100644 index 000000000..35eb1ddfb --- /dev/null +++ b/.idea/vcs.xml @@ -0,0 +1,6 @@ + + + + + + \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json index 03de4a74d..cf916d511 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,4 +1,5 @@ -"rust": { +{ + "rust-analyzer.check.command": "check", "editor.defaultFormatter": "rust-lang.rust-analyzer", - "editor.formatOnSave": true + "editor.formatOnSave": true, } diff --git a/conjure_oxide/src/lib.rs b/conjure_oxide/src/lib.rs index e7f1a854a..05c3581b3 100644 --- a/conjure_oxide/src/lib.rs +++ b/conjure_oxide/src/lib.rs @@ -1,11 +1,11 @@ pub mod error; pub mod find_conjure; pub mod parse; -pub mod rules; -mod solvers; +mod rules; +pub mod solvers; pub use conjure_core::ast; // re-export core::ast as conjure_oxide::ast pub use conjure_core::ast::Model; // rexport core::ast::Model as conjure_oxide::Model pub use conjure_core::solvers::Solver; -pub use error::Error; +pub use error::Error; \ No newline at end of file diff --git a/conjure_oxide/src/rules/mod.rs b/conjure_oxide/src/rules/mod.rs index 4d4702c64..09f07fe44 100644 --- a/conjure_oxide/src/rules/mod.rs +++ b/conjure_oxide/src/rules/mod.rs @@ -1,7 +1,81 @@ -use conjure_core::{ast::Expression, rule::RuleApplicationError}; +use conjure_core::{ast::Expression as Expr, rule::RuleApplicationError}; use conjure_rules::register_rule; +// #[register_rule] +// fn identity(expr: &Expr) -> Result { +// Ok(expr.clone()) +// } + +#[register_rule] +fn sum_constants(expr: &Expr) -> Result { + match expr { + Expr::Sum(exprs) => { + let mut sum = 0; + let mut new_exprs = Vec::new(); + let mut changed = false; + for e in exprs { + match e { + Expr::ConstantInt(i) => { + sum += i; + changed = true; + } + _ => new_exprs.push(e.clone()), + } + } + if !changed { + return Err(RuleApplicationError::RuleNotApplicable); + } + new_exprs.push(Expr::ConstantInt(sum)); + Ok(Expr::Sum(new_exprs)) // Let other rules handle only one Expr being contained in the sum + } + _ => Err(RuleApplicationError::RuleNotApplicable), + } +} + +#[register_rule] +fn unwrap_sum(expr: &Expr) -> Result { + match expr { + Expr::Sum(exprs) if (exprs.len() == 1) => Ok(exprs[0].clone()), + _ => Err(RuleApplicationError::RuleNotApplicable), + } +} + +#[register_rule] +fn flatten_sum_geq(expr: &Expr) -> Result { + match expr { + Expr::Geq(a, b) => { + let exprs = match a.as_ref() { + Expr::Sum(exprs) => Ok(exprs), + _ => Err(RuleApplicationError::RuleNotApplicable), + }?; + Ok(Expr::SumGeq(exprs.clone(), b.clone())) + } + _ => Err(RuleApplicationError::RuleNotApplicable), + } +} + +#[register_rule] +fn sum_leq_to_sumleq(expr: &Expr) -> Result { + match expr { + Expr::Leq(a, b) => { + let exprs = match a.as_ref() { + Expr::Sum(exprs) => Ok(exprs), + _ => Err(RuleApplicationError::RuleNotApplicable), + }?; + Ok(Expr::SumLeq(exprs.clone(), b.clone())) + } + _ => Err(RuleApplicationError::RuleNotApplicable), + } +} + #[register_rule] -fn identity(expr: &Expression) -> Result { - Ok(expr.clone()) +fn lt_to_ineq(expr: &Expr) -> Result { + match expr { + Expr::Lt(a, b) => Ok(Expr::Ineq( + a.clone(), + b.clone(), + Box::new(Expr::ConstantInt(-1)), + )), + _ => Err(RuleApplicationError::RuleNotApplicable), + } } diff --git a/conjure_oxide/src/solvers/minion.rs b/conjure_oxide/src/solvers/minion.rs index f3eea6095..76ab90414 100644 --- a/conjure_oxide/src/solvers/minion.rs +++ b/conjure_oxide/src/solvers/minion.rs @@ -7,9 +7,10 @@ use crate::ast::{ DecisionVariable, Domain as ConjureDomain, Expression as ConjureExpression, Model as ConjureModel, Name as ConjureName, Range as ConjureRange, }; +pub use minion_rs::ast::Model as MinionModel; use minion_rs::ast::{ - Constant as MinionConstant, Constraint as MinionConstraint, Model as MinionModel, - Var as MinionVar, VarDomain as MinionDomain, + Constant as MinionConstant, Constraint as MinionConstraint, Var as MinionVar, + VarDomain as MinionDomain, }; const SOLVER: Solver = Solver::Minion; diff --git a/conjure_oxide/src/solvers/mod.rs b/conjure_oxide/src/solvers/mod.rs index c7ea0f194..85c04d25b 100644 --- a/conjure_oxide/src/solvers/mod.rs +++ b/conjure_oxide/src/solvers/mod.rs @@ -1,5 +1,4 @@ mod error; - pub mod minion; pub mod kissat; diff --git a/conjure_oxide/tests/rewrite_tests.rs b/conjure_oxide/tests/rewrite_tests.rs index 2cd58b827..db4197ada 100644 --- a/conjure_oxide/tests/rewrite_tests.rs +++ b/conjure_oxide/tests/rewrite_tests.rs @@ -1,8 +1,20 @@ // Tests for rewriting/simplifying parts of the AST use core::panic; +use std::collections::HashMap; -use conjure_oxide::ast::*; +use conjure_oxide::{ + ast::*, + solvers::{minion, FromConjureModel}, +}; +use conjure_rules::{get_rule_by_name, get_rules}; +use minion_rs::ast::{Constant, VarName}; + +#[test] +fn rules_present() { + let rules = get_rules(); + assert!(rules.len() > 0); +} #[test] fn rules_present() { @@ -97,3 +109,160 @@ fn simplify_expression(expr: Expression) -> Expression { _ => expr, } } + +#[test] +fn rule_sum_constants() { + let sum_constants = get_rule_by_name("sum_constants").unwrap(); + let unwrap_sum = get_rule_by_name("unwrap_sum").unwrap(); + + let mut expr = Expression::Sum(vec![ + Expression::ConstantInt(1), + Expression::ConstantInt(2), + Expression::ConstantInt(3), + ]); + + expr = sum_constants.apply(&expr).unwrap(); + expr = unwrap_sum.apply(&expr).unwrap(); + + assert_eq!(expr, Expression::ConstantInt(6)); +} + +#[test] +fn rule_sum_mixed() { + let sum_constants = get_rule_by_name("sum_constants").unwrap(); + + let mut expr = Expression::Sum(vec![ + Expression::ConstantInt(1), + Expression::ConstantInt(2), + Expression::Reference(Name::UserName(String::from("a"))), + ]); + + expr = sum_constants.apply(&expr).unwrap(); + + assert_eq!( + expr, + Expression::Sum(vec![ + Expression::Reference(Name::UserName(String::from("a"))), + Expression::ConstantInt(3), + ]) + ); +} + +#[test] +fn rule_sum_geq() { + let flatten_sum_geq = get_rule_by_name("flatten_sum_geq").unwrap(); + + let mut expr = Expression::Geq( + Box::new(Expression::Sum(vec![ + Expression::ConstantInt(1), + Expression::ConstantInt(2), + ])), + Box::new(Expression::ConstantInt(3)), + ); + + expr = flatten_sum_geq.apply(&expr).unwrap(); + + assert_eq!( + expr, + Expression::SumGeq( + vec![Expression::ConstantInt(1), Expression::ConstantInt(2),], + Box::new(Expression::ConstantInt(3)) + ) + ); +} + +fn callback(solution: HashMap) -> bool { + println!("Solution: {:?}", solution); + false +} + +/// +/// Reduce and solve: +/// ```text +/// find a,b,c : int(1..3) +/// such that a + b + c <= 2 + 3 - 1 +/// such that a < b +/// ``` +#[test] +fn reduce_solve_xyz() { + println!("Rules: {:?}", conjure_rules::get_rules()); + let sum_constants = get_rule_by_name("sum_constants").unwrap(); + let unwrap_sum = get_rule_by_name("unwrap_sum").unwrap(); + let lt_to_ineq = get_rule_by_name("lt_to_ineq").unwrap(); + let sum_leq_to_sumleq = get_rule_by_name("sum_leq_to_sumleq").unwrap(); + + // 2 + 3 - 1 + let mut expr1 = Expression::Sum(vec![ + Expression::ConstantInt(2), + Expression::ConstantInt(3), + Expression::ConstantInt(-1), + ]); + + expr1 = sum_constants.apply(&expr1).unwrap(); + expr1 = unwrap_sum.apply(&expr1).unwrap(); + assert_eq!(expr1, Expression::ConstantInt(4)); + + // a + b + c = 4 + expr1 = Expression::Leq( + Box::new(Expression::Sum(vec![ + Expression::Reference(Name::UserName(String::from("a"))), + Expression::Reference(Name::UserName(String::from("b"))), + Expression::Reference(Name::UserName(String::from("c"))), + ])), + Box::new(expr1), + ); + expr1 = sum_leq_to_sumleq.apply(&expr1).unwrap(); + assert_eq!( + expr1, + Expression::SumLeq( + vec![ + Expression::Reference(Name::UserName(String::from("a"))), + Expression::Reference(Name::UserName(String::from("b"))), + Expression::Reference(Name::UserName(String::from("c"))), + ], + Box::new(Expression::ConstantInt(4)) + ) + ); + + // a < b + let mut expr2 = Expression::Lt( + Box::new(Expression::Reference(Name::UserName(String::from("a")))), + Box::new(Expression::Reference(Name::UserName(String::from("b")))), + ); + expr2 = lt_to_ineq.apply(&expr2).unwrap(); + assert_eq!( + expr2, + Expression::Ineq( + Box::new(Expression::Reference(Name::UserName(String::from("a")))), + Box::new(Expression::Reference(Name::UserName(String::from("b")))), + Box::new(Expression::ConstantInt(-1)) + ) + ); + + let mut model = Model { + variables: HashMap::new(), + constraints: vec![expr1, expr2], + }; + model.variables.insert( + Name::UserName(String::from("a")), + DecisionVariable { + domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]), + }, + ); + model.variables.insert( + Name::UserName(String::from("b")), + DecisionVariable { + domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]), + }, + ); + model.variables.insert( + Name::UserName(String::from("c")), + DecisionVariable { + domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]), + }, + ); + + let minion_model = conjure_oxide::solvers::minion::MinionModel::from_conjure(model).unwrap(); + + minion_rs::run_minion(minion_model, callback).unwrap(); +} diff --git a/crates/conjure_rules/src/lib.rs b/crates/conjure_rules/src/lib.rs index 7ce4b1e87..a3064653d 100644 --- a/crates/conjure_rules/src/lib.rs +++ b/crates/conjure_rules/src/lib.rs @@ -64,6 +64,10 @@ pub fn get_rules() -> Vec> { RULES_DISTRIBUTED_SLICE.to_vec() } +pub fn get_rule_by_name(name: &str) -> Option> { + get_rules().iter().find(|rule| rule.name == name).cloned() +} + /// This procedural macro registers a decorated function with `conjure_rules`' global registry. /// It may be used in any downstream crate. For more information on linker magic, see the [`linkme`](https://docs.rs/linkme/latest/linkme/) crate. /// diff --git a/solvers/minion/src/raw_bindings.rs b/solvers/minion/src/raw_bindings.rs deleted file mode 100644 index 4fac11941..000000000 --- a/solvers/minion/src/raw_bindings.rs +++ /dev/null @@ -1,105 +0,0 @@ -#![allow(warnings)] -include!(concat!(env!("OUT_DIR"), "/bindings.rs")); - -#[cfg(test)] -mod tests { - - use super::*; - use std::ffi::CString; - - // solutions - static mut X_VAL: i32 = 0; - static mut Y_VAL: i32 = 0; - static mut Z_VAL: i32 = 0; - - #[no_mangle] - pub extern "C" fn hello_from_rust() -> bool { - unsafe { - X_VAL = printMatrix_getValue(0) as _; - Y_VAL = printMatrix_getValue(1) as _; - Z_VAL = printMatrix_getValue(2) as _; - return true; - } - } - - #[test] - fn xyz_raw() { - // A simple constraints model, manually written using FFI functions. - // Testing to see if it does not segfault. - // Results can be manually inspected in the outputted minion logs. - unsafe { - // See https://rust-lang.github.io/rust-bindgen/cpp.html - let options = newSearchOptions(); - let args = newSearchMethod(); - let instance = newInstance(); - - let x_str = CString::new("x").expect("bad x"); - let y_str = CString::new("y").expect("bad y"); - let z_str = CString::new("z").expect("bad z"); - - newVar_ffi(instance, x_str.as_ptr() as _, VariableType_VAR_BOUND, 1, 3); - newVar_ffi(instance, y_str.as_ptr() as _, VariableType_VAR_BOUND, 2, 4); - newVar_ffi(instance, z_str.as_ptr() as _, VariableType_VAR_BOUND, 1, 5); - - let x = getVarByName(instance, x_str.as_ptr() as _); - let y = getVarByName(instance, y_str.as_ptr() as _); - let z = getVarByName(instance, z_str.as_ptr() as _); - - // PRINT - printMatrix_addVar(instance, x); - printMatrix_addVar(instance, y); - printMatrix_addVar(instance, z); - - // VARORDER - let search_vars = vec_var_new(); - vec_var_push_back(search_vars as _, x); - vec_var_push_back(search_vars as _, y); - vec_var_push_back(search_vars as _, z); - let search_order = newSearchOrder(search_vars as _, VarOrderEnum_ORDER_STATIC, false); - instance_addSearchOrder(instance, search_order); - - // CONSTRAINTS - let leq = newConstraintBlob(ConstraintType_CT_LEQSUM); - let geq = newConstraintBlob(ConstraintType_CT_GEQSUM); - let ineq = newConstraintBlob(ConstraintType_CT_INEQ); - - let rhs_vars = vec_var_new(); - vec_var_push_back(rhs_vars, constantAsVar(4)); - - // leq / geq : [var] [var] - constraint_addVarList(leq, search_vars as _); - constraint_addVarList(leq, rhs_vars as _); - - constraint_addVarList(geq, search_vars as _); - constraint_addVarList(geq, rhs_vars as _); - - // ineq: [var] [var] [const] - let x_vec = vec_var_new(); - vec_var_push_back(x_vec, x); - - let y_vec = vec_var_new(); - vec_var_push_back(y_vec, y); - - let const_vec = vec_int_new(); - vec_int_push_back(const_vec, -1); - - constraint_addVarList(ineq, x_vec as _); - constraint_addVarList(ineq, y_vec as _); - constraint_addConstantList(ineq, const_vec as _); - - instance_addConstraint(instance, leq); - instance_addConstraint(instance, geq); - instance_addConstraint(instance, ineq); - - let res = runMinion(options, args, instance, Some(hello_from_rust)); - - // does it get this far? - assert_eq!(res, 0); - - // test if solutions are correct - assert_eq!(X_VAL, 1); - assert_eq!(Y_VAL, 2); - assert_eq!(Z_VAL, 1); - } - } -}