feat(domain_debugging): add a pretty output option for domain of expressions

crates/conjure-cp-cli/src/pretty.rs

@@ -3,7 +3,7 @@ use std::{path::PathBuf, sync::Arc};
 use anyhow::anyhow;
 use clap::ValueHint;
 
-use conjure_cp_cli::utils::testing::serialize_model;
+use conjure_cp_cli::utils::testing::{serialize_domains, serialize_model};
 
 use crate::cli::{GlobalArgs, LOGGING_HELP_HEADING};
 use crate::solve::{init_context, parse};
@@ -28,10 +28,11 @@ pub fn run_pretty_command(global_args: GlobalArgs, pretty_args: Args) -> anyhow:
     // Running the correct method to acquire pretty string
     let output = match pretty_args.output_format.as_str() {
         "ast-json" => serialize_model(&model),
+        "expression-domains" => serialize_domains(&model),
         // "add_new_flag" => method(),
         _ => {
             return Err(anyhow!(
-                "Unknown output format {}; supports [ast-json]",
+                "Unknown output format {}; supports [ast-json, expression-domains]",
                 &pretty_args.output_format
             ));
         }

crates/conjure-cp-cli/src/utils/testing.rs

@@ -13,7 +13,7 @@ use std::io::{BufRead, BufReader, Write};
 use std::sync::{Arc, RwLock};
 use uniplate::Uniplate;
 
-use conjure_cp::ast::{AbstractLiteral, GroundDomain, Moo, SerdeModel};
+use conjure_cp::ast::{AbstractLiteral, Expression, GroundDomain, Moo, SerdeModel};
 use conjure_cp::context::Context;
 use serde_json::{Error as JsonError, Value as JsonValue};
 
@@ -115,6 +115,27 @@ pub fn serialize_model(model: &ConjureModel) -> Result<String, JsonError> {
     serde_json::to_string_pretty(&sorted_json)
 }
 
+pub fn serialize_domains(model: &ConjureModel) -> Result<String, JsonError> {
+    let mut output = String::new();
+    for constraint in model.constraints() {
+        serialize_domains_expr(constraint, 0, &mut output);
+    }
+    Ok(output)
+}
+
+fn serialize_domains_expr(expr: &Expression, depth: usize, output: &mut String) {
+    let domain = expr
+        .domain_of()
+        .map(|domain| domain.to_string())
+        .unwrap_or_else(|| "<unknown>".to_owned());
+    output.push_str(&" ".repeat(depth));
+    output.push_str(&format!("{expr} :: {domain}\n"));
+
+    for child in expr.children() {
+        serialize_domains_expr(&child, depth + 1, output);
+    }
+}
+
 pub fn save_model_json(
     model: &ConjureModel,
     path: &str,

crates/conjure-cp-core/src/ast/domains/attrs.rs

@@ -44,10 +44,10 @@ impl<A> Default for SetAttr<A> {
 impl<A: Display> Display for SetAttr<A> {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         match &self.size {
-            Range::Single(x) => write!(f, "(size({x}))"),
-            Range::Bounded(l, r) => write!(f, "(minSize({l}), maxSize({r}))"),
-            Range::UnboundedL(r) => write!(f, "(maxSize({r}))"),
-            Range::UnboundedR(l) => write!(f, "(minSize({l}))"),
+            Range::Single(x) => write!(f, "(size {x})"),
+            Range::Bounded(l, r) => write!(f, "(minSize {l}, maxSize {r})"),
+            Range::UnboundedL(r) => write!(f, "(maxSize {r})"),
+            Range::UnboundedR(l) => write!(f, "(minSize {l})"),
             Range::Unbounded => write!(f, ""),
         }
     }

crates/conjure-cp-core/src/ast/model.rs

@@ -3,6 +3,7 @@ use std::fmt::{Debug, Display};
 use std::hash::Hash;
 use std::sync::{Arc, RwLock};
 
+use crate::ast::Domain;
 use crate::context::Context;
 use crate::{bug, into_matrix_expr};
 use derivative::Derivative;
@@ -549,3 +550,26 @@ impl SerdeModel {
         model.collect_stable_id_mapping()
     }
 }
+
+/// A struct for the information about expressions
+#[serde_as]
+#[derive(Serialize)]
+pub struct ExprInfo {
+    pretty: String,
+    domain: Option<Moo<Domain>>,
+    children: Vec<ExprInfo>,
+}
+
+impl ExprInfo {
+    pub fn create(expr: &Expression) -> ExprInfo {
+        let pretty = expr.to_string();
+        let domain = expr.domain_of();
+        let children = expr.children().iter().map(Self::create).collect();
+
+        ExprInfo {
+            pretty,
+            domain,
+            children,
+        }
+    }
+}

tests-integration/tests/custom/expression-domains/01/model.essence

@@ -0,0 +1,24 @@
+find x : set (maxSize 1) of int(1..2)
+find y : set (maxSize 1) of int(2..3)
+find a : set (maxSize 2) of int(1..2)
+find b : set (maxSize 2) of int(1..3)
+such that x union y subsetEq a intersect b
+
+
+$ initial domains
+$ ((x union y) subsetEq (a intersect b)) :: bool
+$ (x union y) :: set (maxSize 2) of int(1..3)
+$  x :: set (maxSize 1) of int(1..2)
+$  y :: set (maxSize 1) of int(2..3)
+$ (a intersect b) :: set (maxSize 2) of int(1..2)
+$  a :: set (maxSize 2) of int(1..2)
+$  b :: set (maxSize 2) of int(1..3)
+
+$ pruned domains
+$ ((x union y) subsetEq (a intersect b)) :: bool
+$ (x union y) :: set (maxSize 2) of int(1..2)
+$  x :: set (maxSize 1) of int(1..2)
+$  y :: set (maxSize 1) of int(2..2)
+$ (a intersect b) :: set (maxSize 2) of int(1..2)
+$  a :: set (maxSize 2) of int(1..2)
+$  b :: set (maxSize 2) of int(1..3)

tests-integration/tests/custom/expression-domains/01/run.sh

@@ -0,0 +1 @@
+conjure-oxide pretty model.essence --output-format=expression-domains

tests-integration/tests/custom/expression-domains/01/stdout.expected

@@ -0,0 +1,7 @@
+((x union y) subsetEq (a intersect b)) :: bool
+ (x union y) :: set  of set  of int(1..3)
+  x :: set (maxSize 1) of int(1..2)
+  y :: set (maxSize 1) of int(2..3)
+ (a intersect b) :: set  of set  of int(1..2)
+  a :: set (maxSize 2) of int(1..2)
+  b :: set (maxSize 2) of int(1..3)

tests-integration/tests/custom/expression-domains/02/model.essence

@@ -0,0 +1,23 @@
+find x : set (maxSize 1) of int(1..2)
+find y : set (maxSize 1) of int(3..4)
+find a : set (maxSize 2) of int(1..3)
+find b : set (maxSize 2) of int(1..2)
+such that x union y subsetEq a intersect b
+
+$ initial domains
+$ ((x union y) subsetEq (a intersect b)) :: bool
+$ (x union y) :: set (maxSize 2) of int(1..4)
+$  x :: set (maxSize 1) of int(1..2)
+$  y :: set (maxSize 1) of int(3..4)
+$ (a intersect b) :: set (maxSize 2) of int(1..2)
+$  a :: set (maxSize 2) of int(1..3)
+$  b :: set (maxSize 2) of int(1..2)
+
+$ pruned domains
+$ ((x union y) subsetEq (a intersect b)) :: bool
+$ (x union y) :: set (maxSize 1) of int(1..2)
+$  x :: set (maxSize 1) of int(1..2)
+$  y :: set (maxSize 0) of int(3..4)
+$ (a intersect b) :: set (maxSize 2) of int(1..2)
+$  a :: set (maxSize 2) of int(1..3)
+$  b :: set (maxSize 2) of int(1..2)

tests-integration/tests/custom/expression-domains/02/run.sh

@@ -0,0 +1 @@
+conjure-oxide pretty model.essence --output-format=expression-domains

tests-integration/tests/custom/expression-domains/02/stdout.expected

@@ -0,0 +1,7 @@
+((x union y) subsetEq (a intersect b)) :: bool
+ (x union y) :: set  of set  of int(1..4)
+  x :: set (maxSize 1) of int(1..2)
+  y :: set (maxSize 1) of int(3..4)
+ (a intersect b) :: set  of set  of int(1..2)
+  a :: set (maxSize 2) of int(1..3)
+  b :: set (maxSize 2) of int(1..2)

tests-integration/tests/custom/expression-domains/03/model.essence

@@ -0,0 +1,23 @@
+find x : set (minSize 1, maxSize 1) of int(2..3)
+find y : set (minSize 1, maxSize 1) of int(1..2)
+find a : set (minSize 1, maxSize 2) of int(1..3)
+find b : set (minSize 1, maxSize 2) of int(2..4)
+such that x union y subsetEq a intersect b
+
+$ initial domains
+$ ((x union y) subsetEq (a intersect b)) :: bool
+$ (x union y) :: set (minSize 1, maxSize 2) of int(1..3)
+$  x :: set (minSize 1, maxSize 1) of int(2..3)
+$  y :: set (minSize 1, maxSize 1) of int(1..2)
+$ (a intersect b) :: set (maxSize 2) of int(2..3)
+$  a :: set (minSize 1, maxSize 2) of int(1..3)
+$  b :: set (minSize 1, maxSize 2) of int(2..4)
+
+$ pruned domains
+$ ((x union y) subsetEq (a intersect b)) :: bool
+$ (x union y) :: set (minSize 1, maxSize 2) of int(2..3)
+$  x :: set (minSize 1, maxSize 1) of int(2..3)
+$  y :: set (minSize 1, maxSize 1) of int(2..2)
+$ (a intersect b) :: set (maxSize 2) of int(2..3)
+$  a :: set (minSize 1, maxSize 2) of int(2..3)
+$  b :: set (minSize 1, maxSize 2) of int(2..3)

tests-integration/tests/custom/expression-domains/03/run.sh

@@ -0,0 +1 @@
+conjure-oxide pretty model.essence --output-format=expression-domains

tests-integration/tests/custom/expression-domains/03/stdout.expected

@@ -0,0 +1,7 @@
+((x union y) subsetEq (a intersect b)) :: bool
+ (x union y) :: set  of set  of int(1..3)
+  x :: set (minSize 1, maxSize 1) of int(2..3)
+  y :: set (minSize 1, maxSize 1) of int(1..2)
+ (a intersect b) :: set  of set  of int(2..3)
+  a :: set (minSize 1, maxSize 2) of int(1..3)
+  b :: set (minSize 1, maxSize 2) of int(2..4)

tests-integration/tests/custom/expression-domains/04/model.essence

@@ -0,0 +1,23 @@
+find x : set (minSize 1, maxSize 2) of int(1..3)
+find y : set (minSize 1, maxSize 1) of int(2..4)
+find a : set (minSize 1, maxSize 2) of int(2..3)
+find b : set (minSize 1, maxSize 2) of int(1..2)
+such that x union y = a intersect b
+
+$ initial domains
+$ ((x union y) = (a intersect b)) :: bool
+$ (x union y) :: set (minSize 1, maxSize 3) of int(1..4)
+$  x :: set (minSize 1, maxSize 2) of int(1..3)
+$  y :: set (minSize 1, maxSize 1) of int(2..4)
+$ (a intersect b) :: set (maxSize 2) of int(2..2)
+$  a :: set (minSize 1, maxSize 2) of int(2..3)
+$  b :: set (minSize 1, maxSize 2) of int(1..2)
+
+$ pruned domains
+$ ((x union y) = (a intersect b)) :: bool
+$ (x union y) :: set (minSize 1, maxSize 1) of int(2..2)
+$  x :: set (minSize 1, maxSize 2) of int(2..2)
+$  y :: set (minSize 1, maxSize 1) of int(2..2)
+$ (a intersect b) :: set (minSize 1, maxSize 1) of int(2..2)
+$  a :: set (minSize 1, maxSize 2) of int(2..3), with 2 definitely in
+$  b :: set (minSize 1, maxSize 2) of int(1..2), with 2 definitely in

tests-integration/tests/custom/expression-domains/04/run.sh

@@ -0,0 +1 @@
+conjure-oxide pretty model.essence --output-format=expression-domains

tests-integration/tests/custom/expression-domains/04/stdout.expected

@@ -0,0 +1,7 @@
+((x union y) = (a intersect b)) :: bool
+ (x union y) :: set  of set  of int(1..4)
+  x :: set (minSize 1, maxSize 2) of int(1..3)
+  y :: set (minSize 1, maxSize 1) of int(2..4)
+ (a intersect b) :: set  of set  of int(2)
+  a :: set (minSize 1, maxSize 2) of int(2..3)
+  b :: set (minSize 1, maxSize 2) of int(1..2)

tests-integration/tests/custom/expression-domains/05/model.essence

@@ -0,0 +1,23 @@
+find x : set (minSize 2, maxSize 2) of int(1..3)
+find y : set (minSize 1, maxSize 1) of int(3..4)
+find a : set (minSize 2, maxSize 2) of int(2..4)
+find b : set (minSize 2, maxSize 2) of int(1..3)
+such that x union y = a intersect b
+
+$ initial domains
+$ ((x union y) = (a intersect b)) :: bool
+$ (x union y) :: set (minSize 2, maxSize 3) of int(1..4)
+$  x :: set (minSize 2, maxSize 2) of int(1..3)
+$  y :: set (minSize 1, maxSize 1) of int(3..4)
+$ (a intersect b) :: set (maxSize 2) of int(2..3)
+$  a :: set (minSize 2, maxSize 2) of int(2..4)
+$  b :: set (minSize 2, maxSize 2) of int(1..3)
+
+$ pruned domains
+$ ((x union y) = (a intersect b)) :: bool
+$ (x union y) :: set (minSize 2, maxSize 2) of int(2..3)
+$  x :: set (minSize 2, maxSize 2) of int(2..3)
+$  y :: set (minSize 1, maxSize 1) of int(3..3)
+$ (a intersect b) :: set (minSize 2, maxSize 2) of int(2..3)
+$  a :: set (minSize 2, maxSize 2) of int(2..3)
+$  b :: set (minSize 2, maxSize 2) of int(2..3)

tests-integration/tests/custom/expression-domains/05/run.sh

@@ -0,0 +1 @@
+conjure-oxide pretty model.essence --output-format=expression-domains

tests-integration/tests/custom/expression-domains/05/stdout.expected

@@ -0,0 +1,7 @@
+((x union y) = (a intersect b)) :: bool
+ (x union y) :: set  of set  of int(1..4)
+  x :: set (minSize 2, maxSize 2) of int(1..3)
+  y :: set (minSize 1, maxSize 1) of int(3..4)
+ (a intersect b) :: set  of set  of int(2..3)
+  a :: set (minSize 2, maxSize 2) of int(2..4)
+  b :: set (minSize 2, maxSize 2) of int(1..3)

tests-integration/tests/custom/pretty-02/model.essence

@@ -0,0 +1,3 @@
+find x,y,z : int(1..3)
+find a,b,c : int(0..4)
+such that (x+y < z-2) -> a + b > c

tests-integration/tests/custom/pretty-02/run.sh

@@ -0,0 +1 @@
+conjure-oxide pretty model.essence --output-format=expression-domains

tests-integration/tests/custom/pretty-02/stdout.expected

@@ -0,0 +1,15 @@
+((sum([x,y;int(1..2)]) < (z - 2))) -> ((sum([a,b;int(1..2)]) > c)) :: bool
+ (sum([x,y;int(1..2)]) < (z - 2)) :: bool
+  sum([x,y;int(1..2)]) :: int(2..6)
+   [x,y;int(1..2)] :: matrix indexed by [int(1..2)] of int(1..3)
+    x :: int(1..3)
+    y :: int(1..3)
+  (z - 2) :: int(-1..1)
+   z :: int(1..3)
+   2 :: int(2)
+ (sum([a,b;int(1..2)]) > c) :: bool
+  sum([a,b;int(1..2)]) :: int(0..8)
+   [a,b;int(1..2)] :: matrix indexed by [int(1..2)] of int(0..4)
+    a :: int(0..4)
+    b :: int(0..4)
+  c :: int(0..4)

tests-integration/tests/integration/smt/set/eq/via-conjure-naive-via-solver-ac-smt-lia-arrays-expected-rule-trace.txt

@@ -1,7 +1,7 @@
 Model before rewriting:
 
-find a: set (minSize(1)) of int(1..2)
-find b: set (minSize(1)) of int(1..2)
+find a: set (minSize 1) of int(1..2)
+find b: set (minSize 1) of int(1..2)
 
 such that
 
@@ -24,8 +24,8 @@ and([(1 in a) <-> (1 in b),(2 in a) <-> (2 in b);int(1..)]),
 
 Final model:
 
-find a: set (minSize(1)) of int(1..2)
-find b: set (minSize(1)) of int(1..2)
+find a: set (minSize 1) of int(1..2)
+find b: set (minSize 1) of int(1..2)
 
 such that
 

tests-integration/tests/integration/smt/set/eq_overlap/via-conjure-naive-via-solver-ac-smt-lia-arrays-expected-rule-trace.txt

@@ -1,7 +1,7 @@
 Model before rewriting:
 
-find a: set (minSize(1)) of int(1..2)
-find b: set (minSize(1)) of int(2..3)
+find a: set (minSize 1) of int(1..2)
+find b: set (minSize 1) of int(2..3)
 
 such that
 
@@ -25,8 +25,8 @@ and([!(1 in a),(2 in a) <-> (2 in b),!(3 in b);int(1..)]),
 
 Final model:
 
-find a: set (minSize(1)) of int(1..2)
-find b: set (minSize(1)) of int(2..3)
+find a: set (minSize 1) of int(1..2)
+find b: set (minSize 1) of int(2..3)
 
 such that
 

tests-integration/tests/integration/smt/set/subset-sum/via-conjure-naive-via-solver-ac-smt-lia-arrays-expected-rule-trace.txt

@@ -1,7 +1,7 @@
 Model before rewriting:
 
 letting s be 0
-find x: set (minSize(1)) of int(-7, -3..-2, 5, 8)
+find x: set (minSize 1) of int(-7, -3..-2, 5, 8)
 
 such that
 
@@ -24,7 +24,7 @@ sum([product([-7,toInt(-7 in x);int(1..)]),product([-3,toInt(-3 in x);int(1..)])
 Final model:
 
 letting s be 0
-find x: set (minSize(1)) of int(-7, -3..-2, 5, 8)
+find x: set (minSize 1) of int(-7, -3..-2, 5, 8)
 
 such that
 

tests-integration/tests/roundtrip/set_attrs/via-conjure.expected.essence

@@ -1,4 +1,4 @@
-find s: set (size(2)) of int(1..3)
+find s: set (size 2) of int(1..3)
 
 such that