Skip to content

Commit

Permalink
Remove Nothings
Browse files Browse the repository at this point in the history
For now, we would treat top as Expression::And(Metadata::new, Vec::new())
  • Loading branch information
YehorBoiar committed Nov 8, 2024
1 parent d2dca79 commit c85e827
Show file tree
Hide file tree
Showing 10 changed files with 68 additions and 101 deletions.
1 change: 0 additions & 1 deletion conjure_oxide/tests/generated_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -233,7 +233,6 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model)
model.constraints.transform(Arc::new(|x| {
use conjure_core::ast::Expression::*;
match &x {
Nothing => (),
Bubble(_, _, _) => (),
Constant(_, _) => (),
Reference(_, _) => (),
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,13 @@
{
"constraints": "Nothing",
"constraints": {
"And": [
{
"clean": false,
"etype": null
},
[]
]
},
"next_var": 0,
"variables": [
[
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,15 @@
{
"constraints": "Nothing",
"constraints": {
"Constant": [
{
"clean": false,
"etype": null
},
{
"Bool": true
}
]
},
"next_var": 0,
"variables": [
[
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,13 @@
{
"constraints": "Nothing",
"constraints": {
"And": [
{
"clean": false,
"etype": null
},
[]
]
},
"next_var": 0,
"variables": [
[
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,15 @@
{
"constraints": "Nothing",
"constraints": {
"Constant": [
{
"clean": false,
"etype": null
},
{
"Bool": true
}
]
},
"next_var": 0,
"variables": [
[
Expand Down
8 changes: 0 additions & 8 deletions crates/conjure_core/src/ast/expressions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,6 @@ use super::{Domain, Range};
#[biplate(to=Constant)]
#[biplate(to=Metadata)]
pub enum Expression {
/**
* Represents an empty expression
* NB: we only expect this at the top level of a model (if there is no constraints)
*/
Nothing,

/// An expression representing "A is valid as long as B is true"
/// Turns into a conjunction when it reaches a boolean context
Bubble(Metadata, Box<Expression>, Box<Expression>),
Expand Down Expand Up @@ -246,7 +240,6 @@ impl Expression {
Expression::Ineq(_, _, _, _) => Some(ReturnType::Bool),
Expression::AllDiff(_, _) => Some(ReturnType::Bool),
Expression::Bubble(_, _, _) => None, // TODO: (flm8) should this be a bool?
Expression::Nothing => None,
Expression::WatchedLiteral(_, _, _) => Some(ReturnType::Bool),
Expression::Reify(_, _, _) => Some(ReturnType::Bool),
}
Expand Down Expand Up @@ -307,7 +300,6 @@ impl Display for Expression {
Name::MachineName(n) => write!(f, "_{}", n),
Name::UserName(s) => write!(f, "{}", s),
},
Expression::Nothing => write!(f, "Nothing"),
Expression::Sum(_, expressions) => {
write!(f, "Sum({})", display_expressions(expressions))
}
Expand Down
9 changes: 6 additions & 3 deletions crates/conjure_core/src/model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,11 @@ impl Model {
}

pub fn new_empty(context: Arc<RwLock<Context<'static>>>) -> Model {
Model::new(Default::default(), Expression::Nothing, context)
Model::new(
Default::default(),
Expression::And(Metadata::new(), Vec::new()),
context,
)
}
// Function to update a DecisionVariable based on its Name
pub fn update_domain(&mut self, name: &Name, new_domain: Domain) {
Expand All @@ -89,14 +93,13 @@ impl Model {
pub fn get_constraints_vec(&self) -> Vec<Expression> {
match &self.constraints {
Expression::And(_, constraints) => constraints.clone(),
Expression::Nothing => vec![],
_ => vec![self.constraints.clone()],
}
}

pub fn set_constraints(&mut self, constraints: Vec<Expression>) {
if constraints.is_empty() {
self.constraints = Expression::Nothing;
self.constraints = Expression::And(Metadata::new(), Vec::new());
} else if constraints.len() == 1 {
self.constraints = constraints[0].clone();
} else {
Expand Down
36 changes: 20 additions & 16 deletions crates/conjure_core/src/rule_engine/rule.rs
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ impl Reduction {
pub fn pure(new_expression: Expression) -> Self {
Self {
new_expression,
new_top: Expression::Nothing,
new_top: Expression::And(Metadata::new(), Vec::new()),
symbols: SymbolTable::new(),
}
}
Expand All @@ -84,7 +84,7 @@ impl Reduction {
pub fn with_symbols(new_expression: Expression, symbols: SymbolTable) -> Self {
Self {
new_expression,
new_top: Expression::Nothing,
new_top: Expression::And(Metadata::new(), Vec::new()),
symbols,
}
}
Expand All @@ -101,21 +101,25 @@ impl Reduction {
// Apply side-effects (e.g. symbol table updates
pub fn apply(self, model: &mut Model) {
model.variables.extend(self.symbols); // Add new assignments to the symbol table
if let Expression::Nothing = self.new_top {
model.constraints = self.new_expression.clone();
} else {
model.constraints = match self.new_expression {
Expression::And(metadata, mut exprs) => {
// Avoid creating a nested conjunction
exprs.push(self.new_top.clone());
Expression::And(metadata.clone_dirty(), exprs)
}
_ => Expression::And(
Metadata::new(),
vec![self.new_expression.clone(), self.new_top],
),
};
// TODO: (yb33) Remove it when we change constraints to a vector
if let Expression::And(_, exprs) = &self.new_top {
if exprs.is_empty() {
model.constraints = self.new_expression.clone();
return;
}
}

model.constraints = match self.new_expression {
Expression::And(metadata, mut exprs) => {
// Avoid creating a nested conjunction
exprs.push(self.new_top.clone());
Expression::And(metadata.clone_dirty(), exprs)
}
_ => Expression::And(
Metadata::new(),
vec![self.new_expression.clone(), self.new_top],
),
};
}
}

Expand Down
70 changes: 2 additions & 68 deletions crates/conjure_core/src/rules/base.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,71 +12,6 @@ use uniplate::Uniplate;

register_rule_set!("Base", 100, ());

/**
* Remove nothing's from expressions:
* ```text
* and([a, nothing, b]) = and([a, b])
* sum([a, nothing, b]) = sum([a, b])
* sum_leq([a, nothing, b], c) = sum_leq([a, b], c)
* ...
* ```
*/
#[register_rule(("Base", 8800))]
fn remove_nothings(expr: &Expr, _: &Model) -> ApplicationResult {
fn remove_nothings(exprs: Vec<Expr>) -> Result<Vec<Expr>, ApplicationError> {
let mut changed = false;
let mut new_exprs = Vec::new();

for e in exprs {
match e.clone() {
Expr::Nothing => {
changed = true;
}
_ => new_exprs.push(e),
}
}

if changed {
Ok(new_exprs)
} else {
Err(ApplicationError::RuleNotApplicable)
}
}

fn get_lhs_rhs(sub: Vec<Expr>) -> (Vec<Expr>, Box<Expr>) {
if sub.is_empty() {
return (Vec::new(), Box::new(Expr::Nothing));
}

let lhs = sub[..(sub.len() - 1)].to_vec();
let rhs = Box::new(sub[sub.len() - 1].clone());
(lhs, rhs)
}

// FIXME (niklasdewally): temporary conversion until I get the Uniplate APIs figured out
// Uniplate *should* support Vec<> not im::Vector
let new_sub = remove_nothings(expr.children().into_iter().collect())?;

match expr {
Expr::And(md, _) => Ok(Reduction::pure(Expr::And(md.clone(), new_sub))),
Expr::Or(md, _) => Ok(Reduction::pure(Expr::Or(md.clone(), new_sub))),
Expr::Sum(md, _) => Ok(Reduction::pure(Expr::Sum(md.clone(), new_sub))),
Expr::SumEq(md, _, _) => {
let (lhs, rhs) = get_lhs_rhs(new_sub);
Ok(Reduction::pure(Expr::SumEq(md.clone(), lhs, rhs)))
}
Expr::SumLeq(md, _lhs, _rhs) => {
let (lhs, rhs) = get_lhs_rhs(new_sub);
Ok(Reduction::pure(Expr::SumLeq(md.clone(), lhs, rhs)))
}
Expr::SumGeq(md, _lhs, _rhs) => {
let (lhs, rhs) = get_lhs_rhs(new_sub);
Ok(Reduction::pure(Expr::SumGeq(md.clone(), lhs, rhs)))
}
_ => Err(ApplicationError::RuleNotApplicable),
}
}

/// This rule simplifies expressions where the operator is applied to an empty set of sub-expressions.
///
/// For example:
Expand All @@ -94,7 +29,7 @@ fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult {
// excluded expressions
if matches!(
expr,
Nothing | Reference(_, _) | Constant(_, _) | WatchedLiteral(_, _, _)
Reference(_, _) | Constant(_, _) | WatchedLiteral(_, _, _)
) {
return Err(ApplicationError::RuleNotApplicable);
}
Expand All @@ -105,8 +40,7 @@ fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult {

let new_expr = match expr {
Or(_, _) => Constant(Metadata::new(), Const::Bool(false)),
And(_, _) => Constant(Metadata::new(), Const::Bool(true)),
_ => Nothing,
_ => And(Metadata::new(), vec![]),
};

Ok(Reduction::pure(new_expr))
Expand Down
1 change: 0 additions & 1 deletion crates/conjure_core/src/rules/partial_eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult {
// rule infinitely!
// This is why we always check whether we found a constant or not.
match expr.clone() {
Nothing => Err(RuleNotApplicable),
Bubble(_, _, _) => Err(RuleNotApplicable),
Constant(_, _) => Err(RuleNotApplicable),
Reference(_, _) => Err(RuleNotApplicable),
Expand Down

0 comments on commit c85e827

Please sign in to comment.