Skip to content

Commit

Permalink
Fix formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
gskorokhod committed Jan 26, 2024
1 parent dd0e2d6 commit c643cf6
Show file tree
Hide file tree
Showing 5 changed files with 51 additions and 32 deletions.
2 changes: 1 addition & 1 deletion conjure_oxide/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,4 +8,4 @@ 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;
39 changes: 20 additions & 19 deletions conjure_oxide/src/solvers/kissat.rs
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
use std::collections::HashMap;
use thiserror::Error;
use super::{FromConjureModel, SolverError};
use crate::Solver;
use std::collections::HashMap;
use thiserror::Error;

use crate::ast::{Domain as ConjureDomain, Expression as ConjureExpression,
Model as ConjureModel, Name as ConjureName,
use crate::ast::{
Domain as ConjureDomain, Expression as ConjureExpression, Model as ConjureModel,
Name as ConjureName,
};

const SOLVER: Solver = Solver::KissSAT;
Expand All @@ -26,11 +27,13 @@ pub enum CNFError {
#[error("Unexpected Expression `{0}` inside Not(). Only Not(Reference) allowed!")]
UnexpectedExpressionInsideNot(ConjureExpression),

#[error("Unexpected Expression `{0}` found. Only Reference, Not(Reference) and Or(...) allowed!")]
#[error(
"Unexpected Expression `{0}` found. Only Reference, Not(Reference) and Or(...) allowed!"
)]
UnexpectedExpression(ConjureExpression),

#[error("Unexpected nested And: {0}")]
NestedAnd(ConjureExpression)
NestedAnd(ConjureExpression),
}

impl CNF {
Expand Down Expand Up @@ -113,7 +116,8 @@ impl CNF {
if *idx > 0 {
ans.push(ConjureExpression::Reference(name.clone()))
} else {
let expression: ConjureExpression = ConjureExpression::Reference(name.clone());
let expression: ConjureExpression =
ConjureExpression::Reference(name.clone());
ans.push(ConjureExpression::Not(Box::from(expression)))
}
}
Expand All @@ -125,9 +129,7 @@ impl CNF {

fn get_reference_index(&self, name: &ConjureName) -> Result<i32, CNFError> {
match self.get_index(name) {
None => {
Err(CNFError::VariableNameNotFound(name.clone()))
}
None => Err(CNFError::VariableNameNotFound(name.clone())),
Some(ind) => Ok(ind),
}
}
Expand Down Expand Up @@ -220,7 +222,10 @@ impl FromConjureModel for CNF {
// Check that domain has the correct type
let decision_var = conjure_model.variables.get(var).unwrap();
if decision_var.domain != ConjureDomain::BoolDomain {
return Err(SolverError::NotSupported(SOLVER, format!("variable {:?} is not BoolDomain", decision_var)))
return Err(SolverError::NotSupported(
SOLVER,
format!("variable {:?} is not BoolDomain", decision_var),
));
}

ans.add_variable(var);
Expand All @@ -233,7 +238,7 @@ impl FromConjureModel for CNF {
let message = format!("Error converting to CNF: {:?}", error);
// Nik has said that InvalidInstance should be thrown for cases where the model cannot be converted
// So, we use the actual CNF error as the message and throw a SolverError from it
return Err(SolverError::InvalidInstance(SOLVER, message))
return Err(SolverError::InvalidInstance(SOLVER, message));
}
}
}
Expand All @@ -248,11 +253,11 @@ mod tests {
use crate::ast::Expression::{And, Not, Or, Reference};
use crate::ast::{DecisionVariable, Model};
use crate::ast::{Expression, Name};
use crate::solvers::kissat::{CNF};
use crate::solvers::kissat::CNF;
use crate::solvers::{FromConjureModel, SolverError};
use std::collections::HashSet;
use std::fmt::Debug;
use std::hash::Hash;
use crate::solvers::{FromConjureModel, SolverError};

fn to_set<T: Eq + Hash + Debug + Clone>(a: &Vec<T>) -> HashSet<T> {
let mut a_set: HashSet<T> = HashSet::new();
Expand Down Expand Up @@ -308,7 +313,6 @@ mod tests {
assert_eq!(cnf.get_name(1).unwrap(), &x);

assert_eq!(cnf.clauses, vec![vec![1]]);

}

#[test]
Expand Down Expand Up @@ -353,10 +357,7 @@ mod tests {

assert_eq!(
if_ok(cnf.as_expression()),
And(vec![Or(vec![
Reference(x.clone()),
Reference(y.clone())
])])
And(vec![Or(vec![Reference(x.clone()), Reference(y.clone())])])
)
}

Expand Down
2 changes: 1 addition & 1 deletion conjure_oxide/src/solvers/mod.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
mod error;
pub mod minion;
pub mod kissat;
pub mod minion;

pub use crate::ast::Model;
pub use error::*;
Expand Down
7 changes: 2 additions & 5 deletions conjure_oxide/tests/rewrite_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,8 @@
use core::panic;
use std::collections::HashMap;

use conjure_oxide::{
ast::*,
solvers::{FromConjureModel},
};
use conjure_rules::{get_rule_by_name};
use conjure_oxide::{ast::*, solvers::FromConjureModel};
use conjure_rules::get_rule_by_name;
use minion_rs::ast::{Constant, VarName};

#[test]
Expand Down
33 changes: 27 additions & 6 deletions crates/conjure_core/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -124,9 +124,20 @@ pub enum Expression {

fn display_expressions(expressions: &Vec<Expression>) -> String {
if expressions.len() <= 3 {
format!("Sum({})", expressions.iter().map(|e| e.to_string()).collect::<Vec<String>>().join(", "))
format!(
"Sum({})",
expressions
.iter()
.map(|e| e.to_string())
.collect::<Vec<String>>()
.join(", ")
)
} else {
format!("Sum({}..{})", expressions[0], expressions[expressions.len() - 1])
format!(
"Sum({}..{})",
expressions[0],
expressions[expressions.len() - 1]
)
}
}

Expand All @@ -145,9 +156,19 @@ impl Display for Expression {
Expression::Leq(box1, box2) => write!(f, "Leq({}, {})", box1.clone(), box2.clone()),
Expression::Gt(box1, box2) => write!(f, "Gt({}, {})", box1.clone(), box2.clone()),
Expression::Lt(box1, box2) => write!(f, "Lt({}, {})", box1.clone(), box2.clone()),
Expression::SumGeq(box1, box2) => write!(f, "SumGeq({}, {})", display_expressions(box1), box2.clone()),
Expression::SumLeq(box1, box2) => write!(f, "SumLeq({}, {})", display_expressions(box1), box2.clone()),
Expression::Ineq(box1, box2, box3) => write!(f, "Ineq({}, {}, {})", box1.clone(), box2.clone(), box3.clone()),
Expression::SumGeq(box1, box2) => {
write!(f, "SumGeq({}, {})", display_expressions(box1), box2.clone())
}
Expression::SumLeq(box1, box2) => {
write!(f, "SumLeq({}, {})", display_expressions(box1), box2.clone())
}
Expression::Ineq(box1, box2, box3) => write!(
f,
"Ineq({}, {}, {})",
box1.clone(),
box2.clone(),
box3.clone()
),
}
}
}
}

0 comments on commit c643cf6

Please sign in to comment.