feat: Parser and AST support for dominanceRelation (#691)

* feat: add parser support for dominance relations

* test: add dominance parsing tests

* make clippy happy

* fix clippy

Author: gskorokhod

Cargo.lock

@@ -35,12 +35,17 @@ glob = "0.3.2"
 rand = "0.9.0"
 tracing-appender = "0.2"
 tracing-log = "0.2.0"
-tracing-subscriber = { version = "0.3.18", features = ["ansi", "env-filter", "json"] }
+tracing-subscriber = { version = "0.3.18", features = [
+    "ansi",
+    "env-filter",
+    "json",
+] }
 tracing = "0.1.41"
 tree-sitter = "0.24.7"
 tree-sitter-essence = { version = "0.1.0", path = "../crates/tree-sitter-essence" }
 tree-sitter-haskell = "0.23.0"
 git-version = "0.3.9"
+project-root = "0.2.2"
 
 [features]
 

conjure_oxide/Cargo.toml

@@ -6,7 +6,7 @@ use conjure_core::{
     ast::{Literal, Name},
     solver::{adaptors::Minion, states::ExecutionSuccess},
 };
-use conjure_oxide::defaults::get_default_rule_sets;
+use conjure_oxide::defaults::DEFAULT_RULE_SETS;
 use itertools::Itertools;
 use std::collections::HashMap;
 
@@ -25,7 +25,7 @@ pub fn main() {
     println!("Input model: \n {model} \n",);
 
     // TODO: We will have a nicer way to do this in the future
-    let rule_sets = resolve_rule_sets(SolverFamily::Minion, &get_default_rule_sets()).unwrap();
+    let rule_sets = resolve_rule_sets(SolverFamily::Minion, DEFAULT_RULE_SETS).unwrap();
 
     let model = rewrite_model(&model, &rule_sets).unwrap();
     println!("Rewritten model: \n {model} \n",);

conjure_oxide/examples/solver-hello-minion.rs

@@ -1,8 +1 @@
-/// Returns the default rule sets, excluding solver specific ones.
-pub fn get_default_rule_sets() -> Vec<String> {
-    vec![
-        "Base".to_string(),
-        "Constant".to_string(),
-        "Bubble".to_string(),
-    ]
-}
+pub static DEFAULT_RULE_SETS: &[&str] = &["Base", "Constant", "Bubble"];

conjure_oxide/src/defaults.rs

@@ -7,24 +7,24 @@ use std::sync::Arc;
 use anyhow::Result as AnyhowResult;
 use anyhow::{anyhow, bail};
 use clap::{arg, command, Parser};
-use conjure_core::rule_engine::rewrite_naive;
-use conjure_core::Model;
-use conjure_oxide::defaults::get_default_rule_sets;
+use git_version::git_version;
 use schemars::schema_for;
 use serde_json::to_string_pretty;
+use tracing_subscriber::filter::LevelFilter;
+use tracing_subscriber::layer::SubscriberExt as _;
+use tracing_subscriber::util::SubscriberInitExt as _;
+use tracing_subscriber::{EnvFilter, Layer};
 
 use conjure_core::context::Context;
+use conjure_core::rule_engine::rewrite_naive;
+use conjure_core::Model;
+
+use conjure_oxide::defaults::DEFAULT_RULE_SETS;
 use conjure_oxide::find_conjure::conjure_executable;
 use conjure_oxide::rule_engine::{resolve_rule_sets, rewrite_model};
-use conjure_oxide::{get_rules, model_from_json};
-
 use conjure_oxide::utils::conjure::{get_minion_solutions, minion_solutions_to_json};
 use conjure_oxide::SolverFamily;
-use git_version::git_version;
-use tracing_subscriber::filter::LevelFilter;
-use tracing_subscriber::layer::SubscriberExt as _;
-use tracing_subscriber::util::SubscriberInitExt as _;
-use tracing_subscriber::{EnvFilter, Layer};
+use conjure_oxide::{get_rules, model_from_json};
 
 static AFTER_HELP_TEXT: &str = include_str!("help_text.txt");
 
@@ -129,8 +129,10 @@ pub fn main() -> AnyhowResult<()> {
     }
 
     let target_family = cli.solver.unwrap_or(SolverFamily::Minion);
-    let mut extra_rule_sets: Vec<String> = get_default_rule_sets();
-    extra_rule_sets.extend(cli.extra_rule_sets.clone());
+    let mut extra_rule_sets: Vec<&str> = DEFAULT_RULE_SETS.to_vec();
+    for rs in &cli.extra_rule_sets {
+        extra_rule_sets.push(rs.as_str());
+    }
 
     // Logging:
     //
@@ -264,7 +266,7 @@ pub fn main() -> AnyhowResult<()> {
 
     let context = Context::new_ptr(
         target_family,
-        extra_rule_sets.clone(),
+        extra_rule_sets.iter().map(|rs| rs.to_string()).collect(),
         rules,
         rule_sets.clone(),
     );

conjure_oxide/src/main.rs

@@ -41,7 +41,7 @@ pub fn parse_essence_file_native(
                 let mut constraint_vec: Vec<Expression> = Vec::new();
                 for constraint in named_children(&statement) {
                     if constraint.kind() != "single_line_comment" {
-                        constraint_vec.push(parse_constraint(constraint, &source_code));
+                        constraint_vec.push(parse_constraint(constraint, &source_code, &statement));
                     }
                 }
                 model.as_submodel_mut().add_constraints(constraint_vec);
@@ -51,6 +51,19 @@ pub fn parse_essence_file_native(
                 let letting_vars = parse_letting_statement(statement, &source_code);
                 model.as_submodel_mut().symbols_mut().extend(letting_vars);
             }
+            "dominance_relation" => {
+                let inner = statement
+                    .child(1)
+                    .expect("Expected a sub-expression inside `dominanceRelation`");
+                let expr = parse_constraint(inner, &source_code, &statement);
+                let dominance = Expression::DominanceRelation(Metadata::new(), Box::new(expr));
+                if model.dominance.is_some() {
+                    return Err(EssenceParseError::ParseError(Error::Parse(
+                        "Duplicate dominance relation".to_owned(),
+                    )));
+                }
+                model.dominance = Some(dominance);
+            }
             _ => {
                 let kind = statement.kind();
                 return Err(EssenceParseError::ParseError(Error::Parse(
@@ -63,8 +76,9 @@ pub fn parse_essence_file_native(
 }
 
 fn get_tree(path: &str, filename: &str, extension: &str) -> (Tree, String) {
-    let source_code = fs::read_to_string(format!("{path}/{filename}.{extension}"))
-        .expect("Failed to read the source code file");
+    let pth = format!("{path}/{filename}.{extension}");
+    let source_code = fs::read_to_string(&pth)
+        .unwrap_or_else(|_| panic!("Failed to read the source code file {}", pth));
     let mut parser = Parser::new();
     parser.set_language(&LANGUAGE.into()).unwrap();
     (
@@ -201,7 +215,7 @@ fn parse_letting_statement(letting_statement_list: Node, source_code: &str) -> S
                 for name in temp_symbols {
                     symbol_table.insert(Rc::new(Declaration::new_value_letting(
                         Name::UserName(String::from(name)),
-                        parse_constraint(expr_or_domain, source_code),
+                        parse_constraint(expr_or_domain, source_code, &letting_statement_list),
                     )));
                 }
             }
@@ -219,24 +233,24 @@ fn parse_letting_statement(letting_statement_list: Node, source_code: &str) -> S
     symbol_table
 }
 
-fn parse_constraint(constraint: Node, source_code: &str) -> Expression {
+fn parse_constraint(constraint: Node, source_code: &str, root: &Node) -> Expression {
     match constraint.kind() {
-        "constraint" | "expression" => child_expr(constraint, source_code),
+        "constraint" | "expression" => child_expr(constraint, source_code, root),
         "not_expr" => Expression::Not(
             Metadata::new(),
-            Box::new(child_expr(constraint, source_code)),
+            Box::new(child_expr(constraint, source_code, root)),
         ),
         "abs_value" => Expression::Abs(
             Metadata::new(),
-            Box::new(child_expr(constraint, source_code)),
+            Box::new(child_expr(constraint, source_code, root)),
         ),
         "negative_expr" => Expression::Neg(
             Metadata::new(),
-            Box::new(child_expr(constraint, source_code)),
+            Box::new(child_expr(constraint, source_code, root)),
         ),
         "exponent" | "product_expr" | "sum_expr" | "comparison" | "and_expr" | "or_expr"
         | "implication" => {
-            let expr1 = child_expr(constraint, source_code);
+            let expr1 = child_expr(constraint, source_code, root);
             let op = constraint.child(1).unwrap_or_else(|| {
                 panic!(
                     "Error: missing node in expression of kind {}",
@@ -250,7 +264,7 @@ fn parse_constraint(constraint: Node, source_code: &str) -> Expression {
                     constraint.kind()
                 )
             });
-            let expr2 = parse_constraint(expr2_node, source_code);
+            let expr2 = parse_constraint(expr2_node, source_code, root);
 
             match op_type {
                 "**" => Expression::UnsafePow(Metadata::new(), Box::new(expr1), Box::new(expr2)),
@@ -280,7 +294,7 @@ fn parse_constraint(constraint: Node, source_code: &str) -> Expression {
         "quantifier_expr" => {
             let mut expr_list = Vec::new();
             for expr in named_children(&constraint) {
-                expr_list.push(parse_constraint(expr, source_code));
+                expr_list.push(parse_constraint(expr, source_code, root));
             }
 
             let quantifier = constraint.child(0).unwrap_or_else(|| {
@@ -331,6 +345,18 @@ fn parse_constraint(constraint: Node, source_code: &str) -> Expression {
                 Atom::Reference(Name::UserName(variable_name)),
             )
         }
+        "from_solution" => match root.kind() {
+            "dominance_relation" => {
+                let inner = child_expr(constraint, source_code, root);
+                match inner {
+                    Expression::Atomic(_, _) => {
+                        Expression::FromSolution(Metadata::new(), Box::new(inner))
+                    }
+                    _ => panic!("Expression inside a `fromSolution()` must be a variable name"),
+                }
+            }
+            _ => panic!("`fromSolution()` is only allowed inside dominance relation definitions"),
+        },
         _ => panic!("{} is not a recognized node kind", constraint.kind()),
     }
 }
@@ -339,9 +365,9 @@ fn named_children<'a>(node: &'a Node<'a>) -> impl Iterator<Item = Node<'a>> + 'a
     (0..node.named_child_count()).filter_map(|i| node.named_child(i))
 }
 
-fn child_expr(node: Node, source_code: &str) -> Expression {
+fn child_expr(node: Node, source_code: &str, root: &Node) -> Expression {
     let child = node
         .named_child(0)
         .unwrap_or_else(|| panic!("Error: missing node in expression of kind {}", node.kind()));
-    parse_constraint(child, source_code)
+    parse_constraint(child, source_code, root)
 }

conjure_oxide/src/utils/essence_parser.rs

@@ -2,16 +2,16 @@
 
 use conjure_core::rule_engine::rewrite_model;
 use conjure_core::rule_engine::rewrite_naive;
+use conjure_oxide::defaults::DEFAULT_RULE_SETS;
 use conjure_oxide::utils::essence_parser::parse_essence_file_native;
-use conjure_oxide::utils::testing::{read_human_rule_trace, read_rule_trace};
+use conjure_oxide::utils::testing::read_human_rule_trace;
 use glob::glob;
 use itertools::Itertools;
 use std::collections::BTreeMap;
 use std::env;
 use std::error::Error;
 use std::fs;
 use std::fs::File;
-use std::str::FromStr;
 use tracing::{span, Level, Metadata as OtherMetadata};
 use tracing_subscriber::{
     filter::EnvFilter, filter::FilterFn, fmt, layer::SubscriberExt, Layer, Registry,
@@ -27,7 +27,6 @@ use std::sync::RwLock;
 use conjure_core::ast::Atom;
 use conjure_core::ast::{Expression, Literal, Name};
 use conjure_core::context::Context;
-use conjure_oxide::defaults::get_default_rule_sets;
 use conjure_oxide::rule_engine::resolve_rule_sets;
 use conjure_oxide::utils::conjure::minion_solutions_to_json;
 use conjure_oxide::utils::conjure::{
@@ -258,7 +257,7 @@ fn integration_test_inner(
 
     // Stage 2a: Rewrite the model using the rule engine (run unless explicitly disabled)
     let rewritten_model = if config.apply_rewrite_rules {
-        let rule_sets = resolve_rule_sets(SolverFamily::Minion, &get_default_rule_sets())?;
+        let rule_sets = resolve_rule_sets(SolverFamily::Minion, DEFAULT_RULE_SETS)?;
 
         let rewritten = if config.enable_native_impl {
             rewrite_model(

conjure_oxide/tests/generated_tests.rs

@@ -0,0 +1,13 @@
+find cost: int(1..10)
+find carbon: int(1..10)
+
+such that (cost + carbon) <= 15
+
+dominanceRelation (
+    (cost <= fromSolution(cost)) /\
+    (carbon <= fromSolution(carbon)) /\
+    (
+        (cost < fromSolution(cost)) \/
+        (carbon < fromSolution(carbon))
+    )
+)

conjure_oxide/tests/parser_tests/dominance_simple.essence

@@ -0,0 +1,17 @@
+find cost: int(1..10)
+find carbon: int(1..10)
+
+such that (cost + carbon) <= 15
+
+dominanceRelation (
+    (cost <= fromSolution(cost)) /\
+    (carbon <= fromSolution(carbon)) /\
+    (
+        (cost < fromSolution(cost)) \/
+        (carbon < fromSolution(carbon))
+    )
+)
+
+dominanceRelation (
+    (cost <= fromSolution(cost))
+)