Conjure Oxide

Welcome to the documentation of Conjure Oxide, a next generation constraints modelling tool written in Rust. It supports models written in the Essence and Essence Prime constraints modelling languages.

Conjure Oxide is in the early stages of development, so most Essence language features are not supported yet. However, it does currently support most of Essence Prime.

This site contains the user documentation for Conjure Oxide; other useful links can be found on the useful links page.

Contributing

The project is primarily developed by students and staff at the University of St Andrews, but we also welcome outside contributors; for more information see the contributor’s guide.

Licence

The Conjure Oxide source and documentation are released under the Mozilla Public Licence v2.0.

Installation

To install Conjure Oxide, either build it from source, or use a nightly release.

Quick Start Guide to Running your first Essence Model

This guide walks you through running your first Essence model with Conjure Oxide.

Your First Problem

Create a file called my_problem.essence with the following content:

find x : int(1..3)
find y : int(2..5)

such that x > y

If you are curious about more complex models, you can check out the models that we use to test Conjure Oxide, available in the tests-integration/tests/integration directory of the repository.

Running with Different Solvers

SAT Solver

--sat-encoding specifies the encoding strategy used by the SAT solver. This affects performance and solution structure.

Supported options:

• log (default)
• direct
• order

Default usage (uses log):

cargo run -- solve --solver sat my_problem.essence

Specify an encoding:

cargo run -- solve --solver sat --sat-encoding direct my_problem.essence

Warning

Currently, running the command above will cause the following error:

model invalid: Only Boolean Decision Variables supported

This because the SAT option for the solver argument only currently enables the base (boolean) rule set and does not specify an integer SAT ruleset to include. This is something we are currently working on, and should be resolved soon.

Minion Solver

cargo run -- solve --solver minion my_problem.essence

Expected output for both solvers:

Solutions:
[
  {
    "x": {
      "Int": 3
    },
    "y": {
      "Int": 2
    }
  }
]

Understanding What Happened

Conjure Oxide transformed your high-level Essence model through several steps:

1. Parsing - Your Essence file was parsed into an internal AST
2. Rule Application - Backend-specific rules transformed the model
3. Solving - The transformed model was sent to the solver
4. Solution Extraction - The solver’s output was converted back to Essence format

Want to see exactly what rules were applied? Check out the Logging guide.

Functional Programming Style

For developers who come from programming languages like Scala or Haskell, or those who favour a functional programming style, we have a Functional Rust guide that you might find useful.

Logging

This document is a work in progress - for a full list of logging options, see Conjure Oxide’s --help output.

To stderr

Using --verbose, and the RUST_LOG environment variable, you can control the contents, and formatting of, Conjure Oxide’s stderr output:

• --verbose changes the formatting of the logs for improved readability, including printing source locations and line numbers for log events. It also enables the printing of the log levels INFO and above.

• The RUST_LOG environment variable can be used to customise the log levels that are printed depending on the module . For more information, see: https://docs.rs/env_logger/latest/env_logger/#enabling-logging.

Example: Logging Rule Applications

Different log levels provide different information about the rules applied to the model:

• INFO provides information on the rules that were applied to the model.

• TRACE additionally prints the rules that were attempted and why they were not applicable.

To see TRACE logs in a pretty format (mainly useful for debugging):

$ RUST_LOG=trace conjure-oxide solve --verbose <model>

Or, using cargo:

$ RUST_LOG=trace cargo run -- solve --verbose <model>

Example: Tracing SAT Solver Rules

When working with the SAT solver, you can trace the complete transformation pipeline:

RUST_LOG=TRACE cargo run -- solve --solver sat my_problem.essence --verbose

This will show:

• Integer-to-boolean conversions
• Operation transformations
• Tseytin transformations
• All rules that were tried and applied

For more detailed testing output (including JSON traces and rewritten models), run specific tests:

cargo test <test_name>

This generates .json and .txt files containing rule traces, parsed Essence, solutions, and the rewritten model.

Contributors Guide

We love your input! We want to make contributing to this project as easy and transparent as possible, whether it’s:

• Reporting a bug
• Discussing the current state of the code
• Submitting a fix
• Proposing new features
• Becoming a maintainer

Contributing

This project is open-source: you can find the source code on Github, and issues, questions, or feature requests can be posted on the Github issue tracker.

Currently, Conjure Oxide has been primarily developed by students and staff at the University of St Andrews. That being said, we welcome and encourage contributions from individuals outside the University. Over the course of this section, we will expand further into how you can contribute.

For more detailed information regarding our contributing process, please refer to CONTRIBUTING.md

Licence

This project is entirely open-source, with all code released under the MPL 2.0 license, unless stated otherwise.

This section had been adapted from the ‘home’ page of the conjure-oxide wiki, and CONTRIBUTING.md

How We Work

This is our Constitution, but in contrast to a real constitution of a company we intend this document to be a living document. Please feel free to suggest edits and improvements.

Principles

• Assume good faith.
• Take responsibility for your work.
• Look for opportunities to help others.
• Make it easy for others to help you.

Social contract

We agree to adhere to the following guidelines when engaging in group work.

• We communicate in English as a common, shared language.
• We include all group members in meetings, group chats, messages, and social events.
• We turn up on time to meetings.
• We pay attention and contribute to group discussions.
• We contribute to the group tasks.
• We listen to each other’s opinions.
• We share ideas and do not disregard other people’s thoughts or feelings.
• We are respectful towards one another and treat each other with care and courtesy.
• We complete tasks on time and to the best of our ability.
• We do not make assumptions about individual abilities.

Logistics

• GitHub: We use GitHub as our main platform for code collaboration and version control.
• Teams: We use Teams for day to day communications.
• Weekly report: We use a web form to provide an update to the supervisors every week. This is not assessed and doesn’t strictly follow the reflective writing methods. However, this resource on the Gibbs reflective cycle may still be helpful when approaching the weekly form and how to use the form effectively.
• Weekly meetings: The whole group meets once a week. Before this meeting everyone fills in the weekly report. We take minutes at these meetings.

Best Practices for Collaboration

1. Start with Early Pull Requests (PRs)

• Don’t wait until everything is perfect; submitting early PRs allows the team to provide feedback sooner. This helps catch potential issues early and encourages collaboration.
• Even if your code isn’t complete, opening a draft PR can be a good way to start discussions and ensure alignment.

2. Show, Don’t Tell

• Share your experiences and insights! Use GitHub or Microsoft Teams to share updates, challenges, and breakthroughs with the rest of the team.
• Showing real examples means other can more easily help you, it can help others understand your approach and may inspire new ideas.
• High-level explanations can inadvertently hide important details. Showing the actual artefact (whether it’s code, a design document or something else) together with your high-level commentary eliminates this risk.

3. Begin with Specifications

• Before you start coding, document your plan. Write out specifications or create a rough outline of what you’re working on, including examples where possible.
• Having a clear plan makes it easier to get feedback and helps others understand the purpose and scope of your work.

4. Share Failures as Much as Successes

• When something doesn’t work, share it! Learning from mistakes and discussing setbacks is invaluable.
• A failed attempt can often be as educational as a successful one, and it may prevent others from encountering the same issue.

5. Ask Good Questions

• Don’t hesitate to reach out when you’re stuck, but try to ask thoughtful, specific questions.
• Providing context and sharing what you’ve tried will help others give more helpful answers.

Final Thoughts

• Collaboration is key to our success, so feel free to communicate openly.
• Continuous improvement is encouraged—keep looking for ways to improve your code, processes, and knowledge.

This section had been taken from the ‘How we work’ page of the conjure-oxide wiki

Setting up your development environment

Conjure Oxide supports Linux and Mac.

Windows users should install WSL and follow the Linux (Ubuntu) instructions below:

Improving Compilation Speed

Installing sccache improves compilation speeds of this project by caching crates and C/C++ dependencies system-wide.

• Install sccache and follow the setup instructions for Rust. Minion detects and uses sccache out of the box, so no C++ specific installation steps are required.

This section had been taken from the ‘Setting up your development environment’ page of the conjure-oxide wiki

Onboarding

Congratulations you are joining a very exciting project, pushing forward the field of Constraint Programming. However, there is a lot to learn before you are up to speed. Expect to spend the first few weeks on the project learning, and so do not rush starting to contribute right away.

Here are some tips for starting out.

What You Need to Learn

The Conjure-Oxide project fundamentally involves the development of a constraint modelling tool in the Rust programming language. Therefore, learning about constraint programming and Rust will be your initial challenges. Getting a solid understanding of Rust and constraints now will stand you in good stead for the rest of the project so do not worry that spending time learning is not productive, this learning is expected.

Constraint Programming

Constraint programming is a paradigm for solving combinatorial problems. Instead of defining an algorithm to solve a complex problem, we instead model it as a constraint satisfaction problem (CSP), and let one of many optimised solver programs solve it from there.

Whilst not essential to be a fully-fledged constraint programmer it is useful to understand roughly how this works. There are good video lectures online that would be worth a watch for a general understanding, such as the CP Summer School lectures.

Conjure-Oxide uses the input language Essence. Getting an understanding of how to code in Essence will be really useful when it comes to debugging and testing anything. Reading through Essence’s documentation will be useful for this. Another very useful method of learning Essence and some aspects of constraint programming is to explore the selection of example Jupyter notebooks.

Conjure-Oxide is built to fulfil a similar role to Conjure. Conjure is the current constraint modelling tool built in Haskell, which we are basing a lot of our implementation around. Understanding a little bit about Conjure will be useful for you, as you may find yourself needing to refer to Conjure’s source code later in your project.

Rust

If you do not currently know how to program in Rust, this is very important to learn to contribute to most parts of the project. The best resource for learning Rust is The Rust Programming Language book, alongside the Rustlings resource. Rustlings will give you exercises to practice what you learned in the book as you go. If you find the book slow-going there are also great video tutorials available on YouTube that cover the book’s content. Whilst both resources are fantastic, you will most likely not find it necessary to complete them in their entirety. However, I would recommend you complete the Rustlings exercise 19_smart_pointers to understand concepts such as Box and Cow, as these are used heavily throughout Conure-Oxide’s codebase.

Understanding the Codebase

Once you have enough of an understanding to read Rust code you should start reading through Conjure-Oxide’s codebase. This is a large complex codebase, and it is likely that it will not all make sense initially. A good method of understanding the codebase is to follow the control flow of the program and try to understand why each step occurs. There will be areas of the code you do not need to understand the inner-workings of as a new user, and so gaining a full holistic understanding from the outset is not necessary. Instead focus on getting a good general understanding of Conjure-Oxide as a whole, including what each step in process does and where in the codebase it is located.

This is a fundamentally cooperative project, and so do not be afraid to ask for help from a more experienced member of the team if you are struggling to understand an important part of the code. Feel free to reach out through our GitHub Discussions page for help whenever you need it.

This stage will take a while, but understanding the core of the program will be tremendously helpful when you start implementing it.

Selecting a Project

Once you have spent time learning you will feel ready to select a project and begin contributing. There are lots that can be done in Conjure-Oxide, so if you have an idea of a project that is great, but also consider asking on our GitHub Discussions page for ideas, because there are many tasks new starts could reasonably achieve. Do not feel rushed into selecting a project. Having a good understanding of the system before you start writing code, will really facilitate your productivity later in the semester.

Selecting a Starter Project

Whilst you are familiarising yourself with the codebase, you may want to try tackling a couple smaller starter projects. There are always little issues in the codebase needing addressed and working on one of these, while you learn, can be a fantastic way to get a confidence boost from feeling productive. These issues are specifically marked with good first issue on GitHub. However, be aware that taking on a wide project with a lot of reach, even if small, can be very challenging for a new start, as it requires deeply understanding many different areas of the code.

Selecting a Project Early to Help Learn

If the scale of the codebase is feeling overwhelming, then consider talking to the project lead @ozgurakgun and selecting a project earlier on. The project would not need to be well defined at this point but even if you are not initially implementing features, having a project in mind can help focus your learning of the codebase. This narrows the scope of what you try to understand and helps make the codebase less overwhelming. However, you must ensure you still a good general understanding of Conjure-Oxide as a whole, or this will make expanding your project harder in the future.

The Most Important Things

You should realise that it is okay to spend time learning and not contributing, and you should not feel bad, it is expected. If you get a good understanding now it will help you in the future.

Also ensure to ask for help and talk to the rest of the team, using the GitHub Discussions. There will be people on the project who have done it for years now. Use their expertise.

Pull Requests

Tip

We Use Github Flow, so All Code Changes Happen Through Pull Requests

Our development process is as follows:

1. Make a fork.
2. Create a branch on your fork, do not develop on main.
3. Create a pull request as soon as you want others to be able to see your progress, comment, and/or help:
   • Err on the side of creating the pull request too early instead of too late. Having an active PR makes your work visible, allows others to help you and give feedback. Request reviews from people who have worked on similar parts of the project.
   • Keep the PR in draft status until you think it’s ready to be merged.
4. Assign PR to reviewer(s) when it’s ready to be merged.
   • Only Oz (@ozgurakgun) can merge PRs, so add him as a reviewer when you want your PR to be merged.
   • During reviewing, avoid force-pushing to the pull request, as this makes reviewing more difficult. Details on how to update a PR are given below.
5. Once Oz has approved the PR:
   • Update your PR to main by rebase or merge. This can be done through the Github UI or locally.
   • Cleanup your git history (see below) or request your PR to be squash merged.

Style

• Run cargo fmt in the project directory to automatically format code
• Use cargo clippy to lint the code and identify any common issues

See: [[Documentation Style]] and [[Rust Coding Style]] (TODO)

Commit and PR Titles

We use Semantic PR / Commit messages.

Format: <type>(<scope>): <subject> (<scope> is optional)

Example

feat(parser): add letting statements
^--^ ^----^   ^--------------------^
|    |        |
|    |        +--> Summary in present tense.
|    |
|    +--> Area of the project affected by the change.
|
+-------> Type: chore, docs, feat, fix, refactor, style, or test.

Types

• feat: new features for the end user
• chore: changes to build scripts, CI, dependency updates; does not affect production code
• fix: fixing bugs in production code
• style: purely stylistic changes to the code (e.g. indentation, semicolons, etc) that do not affect behaviour
• refactor: changes of production code that do not add new features or fix specific bugs
• test: adding, updating, or refactoring test code
• doc: adding or updating documentation

PR Messages

Your pull request should contain a brief description explaining:

• What changes you are making
• Why they are necessary
• Any significant changes that may break other people’s work

Additionally, you can link your PR to an issue. For example: closes issue #42.

Amending your PR and Force Pushes

You should avoid rebasing, amending, and force-pushing changes during PR review. This makes code review difficult by removing the context around code review comments and changes to a commit.

The recommended way to update PRs is to use git’s built-in support for fixups.

To make a change to a commit (e.g. addressing a code review comment):

git commit --fixup <commit>
git push

Once your PR is ready to merge, these fixup commits can be merged into their original commits like so:

git rebase --autosquash main
git push --force

We have CI checks to block accidental merging of fixup! commits.

See:

• https://rietta.com/blog/git-rebase-autosquash-code-reviews/
• https://git-scm.com/docs/git-commit#Documentation/git-commit.txt—fixupamendrewordltcommitgt

Before your PR is merged

When your PR is approved, you may need to rebase your branch onto main before it can be merged. Rebasing essentially adds all the latest commits from main to your branch if it has fallen behind main.

To do this:

1. Make sure that your main branch is synced to the main repo
2. Switch to the branch you’re making the PR from
3. Do:

   git rebase main
   git push --force
   

(Optional) Cleaning up your Git history

Additionally, if you are proficient with git, you can use interactive rebase to clean up your commit history. This allows you to reorder, drop, or amend commits arbitrarily.

See:

• How to keep your Git history clean with interactive rebase
• 7.6 Git Tools - Rewriting History

There are some GUI tools to help you do that, such as the GitHub Client, GitKraken, various VS Code extensions, etc.

Warning

Interactive rebase and force-pushing overwrites your git history, so it can be destructive. This is also not a requirement!

Squashing PRs

Alternatively, you can ask for the PR to be “squashed”. This combines all your commits into one merge commit. Squashing PRs helps keep the commit history on main clean and logical without requiring you to go back and manually edit your commits!

Creating Documentation

As an organisation, we want Conjure Oxide to be thoroughly documented so that new members of our growing team can integrate smoothly. Whether you are currently on a project or not, contributing to our documentation is essential to achieving this goal.

To make creating and implementing documentation as smooth as possible, we ask that you follow the workflow as outlined below.

Documentation Work Flow

1. Identify the documentation you will write.

   In many cases, documentation contributors will be writing about projects they are currently working on or have already completed. However, there are still plenty of opportunities to contribute to documentation, even if you are not actively involved in a project or are seeking a small side project. In such cases, please refer to issue #1334, which tracks all documentation writing tasks. All unassigned child issues are available for anyone to work on!

   You may come across instances where important or useful documentation is missing from this book. If you notice such gaps and would like to address them as a side project, we encourage you to do so!

2. If the issue is not already present, open a child issue on our documentation tracking issue #1334.

   Make the title of this issue the name of the documentation you will be writing.

3. Link your child issue to a pr request.

   File type and naming convention:

   All documentation for the Conjure Oxide book should be written in markdown. If you’re unfamiliar with markdown or need a refresher on its syntax, we recommend reviewing this guide.

   When naming your documentation file, match the file name as closely as possible to the heading of the documentation and use underscores (‘_’) to replace spaces. For example, if your documentation page is titled “Creating Documentation,” name the file creating_documentation.md.

   Where to place documentation:

   Place all documentation files in an appropriate location within the /docs/src directory. Each markdown file should be stored in the directory that matches its section in the documentation structure. For example, this file is located at /docs/src/developers_guide/contributors_guide/.

   If you know where your documentation belongs in the book, please place it in the appropriate directory. However, it’s not required to know the exact location—moving files is quick and easy. If you’re unsure where your documentation should go, place the file in /docs/src/misc so it can be relocated later to a more suitable section.

   Viewing documentation on the book:

   You must ensure that the documentation you write formats as expected in the book. To do so, follow these steps:

   • Open /docs/src/SUMMARY.md.
   • If you have a definite location for your documentation, link the documentation in the appropriate section using the following format: [ Section title ](path/to/file).
   • If you are unsure where your documentation should reside, place the documentation at any location, but remember to delete this link once you’re happy with your document’s formatting.
   • In your terminal, ensure that you are in the /docs directory and type in the following command mdbooks serve --open

   Important

   Be sure to assign yourself and any other contributors working on the documentation to your child issue and pull request. This helps us keep track of who is responsible for each piece of documentation and ensures proper assignment.

4. Once you are happy with your documentation, request a review from one or more other members of your team.

   Important

   Place any contributors to the documentation and the date where the documentation was last updated in a comment on the first and second lines of the file. For instance:

   [//]: # (Author: Jamie Melton)

   [//]: # (Last Updated: 09/12/2025)

   has been placed at the top of this file.

5. When your team is happy with this documentation, request a review from the current book editors.

   The current book editors are: JamieASM and HKhan-5.

6. Assuming no adjustments are required, the documentation will then be merged in, and the child issue will be closed.

Still unsure?

If you have any questions or concerns, please post them on the documentation discussion board. A book editor will respond to you promptly. Likewise, if you have suggestions for improving or streamlining this process, feel free to share your ideas with the book editors! Your feedback is always welcome.

“Omit needless words”

(c) William Strunk

Key Points

Resources

See:

• the Rust doc style conventions

Do’s

Our documentation is inline with the code. The reader is likely to skim it while scrolling through the file and trying to understand what it does. So, our doc strings should:

• Be as brief and clear as possible
• Ideally, fit comfortably on a standard monitor without obscuring the code
• Contain key information about the method / structure, such as:
  • A single sentence explaining its purpose
  • A brief overview of arguments / return types
  • Example snippets for non-trivial methods
• Explain any details that are not obvious from the method signature, such as:
  • Details of the method’s “contract” that can’t be easily encoded in the type system

    (E.g: “The input must be a sorted slice of positive integers”; “The given expression will be modified in-place”)

  • Non-trivial situations where the method may panic! or cause unintended behaviour

    (E.g: “Panics if the connection terminates while the stream is being read”)

  • Any unsafe things a method does

    (E.g: “We type-cast the given pointer with mem::transmute. This is safe because…”)

  • Special cases

Things to Avoid

Documentation generally should not:

• Repeat itself
• Use long, vague, or overly complex sentences
• Re-state things that are obvious from the types / signature of the method
• Explain implementation details
• Explain high-level architectural decisions (Consider making a wiki page or opening an RFC issue instead!)

And finally… Please, don’t ask ChatGPT to document your code for you! I know that writing documentation can be tedious, but you can always:

• Write a one-sentence doc string for now and come back to it later
• Ask others if you don’t quite understand what a method does

Types and Tests are Documentation

Documentation is great, but we should also use the type system and other rust features to our advantage!

• A lot of things (e.g: error conditions, thread safety, state) can be encoded in the types of arguments / return values. This is usually better than just panic!-ing and adding a doc string to explain why.

• Tests are also a great way to illustrate the behaviour of your code and any special cases - and they also help with catching bugs!

Example Snippets

For non-trivial methods and user-facing API’s, it may be useful to include an example. Examples should be minimal but complete snippets of code that illustrate a method’s behaviour.

If you wrap your example in a code block:

```rust ... ```

Our CI will even run it and complain if the example does not compile / contains an error!

However, don’t feel obliged to include an example for every method! For simple methods they may not be necessary.

Examples

⚠️ Good but a bit wordy:

#![allow(unused)]
fn main() {
/// Checks if the OPTIMIZATIONS environment variable is set to "1".
///
/// # Returns
/// - true if the environment variable is set to "1".
/// - false if the environment variable is not set or set to any other value.
fn optimizations_enabled() -> bool {
    match env::var("OPTIMIZATIONS") {
        Ok(val) => val == "1",
        Err(_) => false, // Assume optimizations are disabled if the environment variable is not set
    }
}
}

✅ Since everything else is obvious from the signature, we can just say:

#![allow(unused)]
fn main() {
/// Checks if the OPTIMIZATIONS environment variable is set to "1"
fn optimizations_enabled() -> bool { ... }
}

⚠️ Not bad, but sounds a bit robotic

# Side-Effects
- When the model is rewritten, related data structures such as the symbol table (which tracks variable names and types)
  or other top-level constraints may also be updated to reflect these changes. These updates are applied to the returned model,
  ensuring that all related components stay consistent and aligned with the changes made during the rewrite.
- The function collects statistics about the rewriting process, including the number of rule applications
  and the total runtime of the rewriter. These statistics are then stored in the model's context for
  performance monitoring and analysis.

✅ Same idea but shorter

# Side-Effects
- Rules can apply side-effects to the model (e.g. adding new constraints or variables).
  The original model is cloned and a modified copy is returned.
- Rule engine statistics (e.g. number of rule applications, run time) are collected and stored in the new model's context.

⚠️ A bit too detailed

# Parameters
- `expression`: A reference to the [`Expression`] that will be evaluated against the given rules. This is the main
   target for rule transformations and is expected to remain unchanged during the function execution.
- `model`: A reference to the [`Model`] that provides context for rule evaluation, such as constraints and symbols.
  Rules may depend on information in the model to determine if they can be applied.
- `rules`: A vector of references to [`Rule`]s that define the transformations to be applied to the expression.
  Each rule is applied independently, and all applicable rules are collected.
- `stats`: A mutable reference to [`RewriterStats`] used to track statistics about rule application, such as
  the number of attempts and successful applications.

✅ Just describing the meaning of arguments will do

(Details of the rewriting process belong on the wiki, and details of underlying types such as Model or Expression are already documented next to their implementations)

- `expression`: A reference to the [`Expression`] to evaluate.
- `model`: A reference to the [`Model`] for access to the symbol table and context.
- `rules`: A vector of references to [`Rule`]s to try.
- `stats`: A mutable reference to [`RewriterStats`] used to track the number of rule applications and other statistics.

Coding Resources and Conventions

Glossary

• PR: Pull request. It’s a proposal to merge code changes into the main branch, and allows collaborators to review and suggest modifications before it’s accepted.

• Branch: A branch contains a different history of code changes (commits). You can start a new branch A’ off of any branch A and push new commits to A’ without affecting the contents of A. Merging branch A’ into A adds all new changes from A’ to A.

• RFC: Request for Comments. It is a design proposal, often written before or alongside major changes.

• Essence: A high level constraint modelling language. Essence is declarative, i.e. it states the problem rather than how to solve it. It also lets us model things at the class level.

  • A class-level model (i.e. description of a problem) may have some parameters. To get from a class-level model to an instance model, we provide concrete values for all the parameters.

    The following describes a problem class:

    given N: int
    find x
    such that x < N
    

    The following are instances of that class:

    letting N be 3
    find x
    such that x < N
    

    letting N be 42
    find x
    such that x < N
    

• Conjure: Constraint modelling tool that translates Essence problem descriptions into Essence’ models that constraint solvers can execute.

• Essence’ (Essence prime): Intermediate representation automatically generated by Conjure

• Savile Row: It transforms high level Essence’ constraint models and outputs solver-specific model that can be executed. Written in Java.

• Minion: Constraint solver. It takes low level constraint models (like Savile Row output) and searches for solutions. Specifically, it has its own input language that is extensively documented.

For an in-depth glossary of GitHub terms, see the GitHub Docs Glossary. This Git Cheat Sheet also contains resources about git commands.

Functional Rust

Functional Rust

Consider the following oft-quoted statement about Rust:

Rust is blazingly fast and memory-efficient: with no runtime or garbage collector. Rust’s rich type system and ownership model guarantee memory-safety and thread-safety — enabling you to eliminate many classes of bugs at compile-time.

Taken specifically from the Rust Foundation’s¹ page talking about why Rust is a good language to use.

But let us focus on the implications of this statement on Conjure Oxide specifically. The key details that one needs to know here are that, despite arguably being imperative, Rust adopts many functional programming concepts in its design². This is significant because the Conjure Oxide codebase makes extensive use of these functional programming concepts.

Making use of them allows the codebase to leverage Rust’s type system to eliminate error cases through coding style, making the code more robust. It also makes the code easier to write, because Rust’s safety system enforces function return types.

Result

By using the Result type, functions can explicitly state success or failure. This also allows functions to call each other linearly in a safe manner³.

This enables the code to be written so that functions can do essentially whatever they need to do as side effects, as long as they record a success or failure result. The error type allows error propagation in a more sophisticated way than exit codes, while still being more efficient than exceptions. This structure is used in a lot of places in this codebase, because it allows for functions to be treated uniformly most anywhere⁴, meaning they can be called anywhere by any originator (or caller) function without having to resort to unsafe rust and sticking to the type safety scheme.

This also allows for the use of the ? operator⁵, which means that errors can be propagated up the call stack lazily.

Consider the following example, written imperatively in Java-like pseudocode:

public void fnReturnsError(a,b) {
    ...Some Code...
    // might throw error1
    int foo1 = maybeReturnsMyError1(a);
    ...Some More Code...
    // might throw error2
    int foo2 = maybeReturnsMyError2(b);
    ...Wow, when will this code end...
    // might throw error3
    int foo3 = maybeReturnsMyError3(a,b);
}

Alternatively, consider a lower-level language like C, which is far more comparable to Rust in its uses and applications, where there are no ‘error types’ and errors behave like either enums or just integral exit codes.

In a C-like language, a similar example would look like this:

int returnAnExitCode(int a, int b) {
    int exit_code = 0;
    ...Some Code Here Too...
    int exit_code = maybeReturnsMyExitCode1(a);
    ...Some More Code...
    int exit_code = maybeReturnsMyExitCode2(b);
    ...Why, if it isn't yet more code ...
    int exit_code = maybeReturnsMyExitCode3(a,b);

    return exit_code
}

This means that, like rust, an error is not an exception getting ‘thrown’, but a value that is being returned. However, unlike rust, they require these exit codes to be set and returned at the end.

This also means that the function calls must be done on some top-level data structure, and that global structure needs to be accessed at the end rather than being able to simply access the top-level data structure through the returned value.

In this type of application, Rust offers two advantages:

1. The Return type, even though it records a success/failure, can be pattern-matched using the match construct to access the data structure which the functions are performing side effects on.
2. The aforementioned ? operator can be used to force the code to return an error type as soon as it is ‘raised’ – that is, returned by one of the functions in the call stack.

This example would look like this in rust-like functional code:

#![allow(unused)]
fn main() {
fn returns_a_result(a: i32, b: i32) -> Result<i32, MyError> {
    // Some code here...
    
    // The ?  operator propagates errors immediately
    let foo1 = maybe_returns_my_error1(a)?;
    
    // Some more code...
    let foo2 = maybe_returns_my_error2(b)?;
    
    // Even more code...
    let foo3 = maybe_returns_my_error3(a, b)?;
    
    // If we get here, all operations succeeded
    Ok()
}
}

Side Effects

Throughout the above section, references are made to changing things through ‘function side effects’. Let us dive deeper into what this actually means.

Functions are fairly complex, but here is what Alonzo Church has to say about what they do, taken from his paper The Calculi of Lambda Conversion:

A function is a rule of correspondence by which when anything is given (as argument) another thing (the value of the function for that argument) may be obtained. That is, a function is an operation which may be applied on one thing (the argument) to yield another thing (the value of the function).

In quite an abstract sense, this passage establishes that a Function is simply a mapping from a set of inputs to a set of outputs.

Now, knowing this, the term side effect also begins to make sense – any persistent effects of a function which are not in the returned value are side effects. In a general sense, this is things like writing to files, printing and so on. More specifically in conjure oxide, almost all processing is done by way of side effects. While this makes sense even in an imperative context, imperative code can still have some functions chained together in ways that are only possible if the data structure being affected by them is actually returned by them. In rust, specifically when this side-effect-only style of programming is used, programs end up looking quite a bit more concise and readable.

Now, having all of this knowledge in the back of your head, you will understand why the following things must be kept in mind:

1. Make the greatest effort to treat Rust as a functional language when programming in this (and indeed any) codebase. Not only does this lead to cleaner, more concise and (arguably) more readable code, it actually helps avoid errors and edge cases.
2. Learn to leverage the Rust type and safety system instead of wrestling with by writing code that uses features in the language like Result<T,E> and Option<T>. This may involve learning where to use these instead of doing things that one cannot do in imperative languages like C.
3. Rust code is only properly ‘safe’ if it uses the type system properly, meaning it is a good idea to avoid things like returning null, unwrapping Result instances⁶.

1. Who are, of course, an entirely unbiased source ↩

2. Rust’s original implementation language was OCaml, which is functional ↩

3. Similar to calling functions in dynamically typed languages like Python, but with enforced types ↩

4. This is because, at their core, all functions are essentially of the type (..) -> ReturnType. Making the return type standard allows for all functions to be of similar types. ↩

5. Which immediately propagates the error up through the call stack in rust. ↩

6. This is what caused the infamous cloudflare outage. ↩

“Omit needless words”

(c) William Strunk

Key Points

Resources

See:

• the Rust doc style conventions

Do’s

Our documentation is inline with the code. The reader is likely to skim it while scrolling through the file and trying to understand what it does. So, our doc strings should:

• Be as brief and clear as possible
• Ideally, fit comfortably on a standard monitor without obscuring the code
• Contain key information about the method / structure, such as:
  • A single sentence explaining its purpose
  • A brief overview of arguments / return types
  • Example snippets for non-trivial methods
• Explain any details that are not obvious from the method signature, such as:
  • Details of the method’s “contract” that can’t be easily encoded in the type system

    (E.g: “The input must be a sorted slice of positive integers”; “The given expression will be modified in-place”)

  • Non-trivial situations where the method may panic! or cause unintended behaviour

    (E.g: “Panics if the connection terminates while the stream is being read”)

  • Any unsafe things a method does

    (E.g: “We type-cast the given pointer with mem::transmute. This is safe because…”)

  • Special cases

Things to Avoid

Documentation generally should not:

• Repeat itself
• Use long, vague, or overly complex sentences
• Re-state things that are obvious from the types / signature of the method
• Explain implementation details
• Explain high-level architectural decisions (Consider making a wiki page or opening an RFC issue instead!)

And finally… Please, don’t ask ChatGPT to document your code for you! I know that writing documentation can be tedious, but you can always:

• Write a one-sentence doc string for now and come back to it later
• Ask others if you don’t quite understand what a method does

Types and Tests are Documentation

Documentation is great, but we should also use the type system and other rust features to our advantage!

• A lot of things (e.g: error conditions, thread safety, state) can be encoded in the types of arguments / return values. This is usually better than just panic!-ing and adding a doc string to explain why.

• Tests are also a great way to illustrate the behaviour of your code and any special cases - and they also help with catching bugs!

Example Snippets

For non-trivial methods and user-facing API’s, it may be useful to include an example. Examples should be minimal but complete snippets of code that illustrate a method’s behaviour.

If you wrap your example in a code block:

```rust ... ```

Our CI will even run it and complain if the example does not compile / contains an error!

However, don’t feel obliged to include an example for every method! For simple methods they may not be necessary.

Examples

⚠️ Good but a bit wordy:

#![allow(unused)]
fn main() {
/// Checks if the OPTIMIZATIONS environment variable is set to "1".
///
/// # Returns
/// - true if the environment variable is set to "1".
/// - false if the environment variable is not set or set to any other value.
fn optimizations_enabled() -> bool {
    match env::var("OPTIMIZATIONS") {
        Ok(val) => val == "1",
        Err(_) => false, // Assume optimizations are disabled if the environment variable is not set
    }
}
}

✅ Since everything else is obvious from the signature, we can just say:

#![allow(unused)]
fn main() {
/// Checks if the OPTIMIZATIONS environment variable is set to "1"
fn optimizations_enabled() -> bool { ... }
}

⚠️ Not bad, but sounds a bit robotic

# Side-Effects
- When the model is rewritten, related data structures such as the symbol table (which tracks variable names and types)
  or other top-level constraints may also be updated to reflect these changes. These updates are applied to the returned model,
  ensuring that all related components stay consistent and aligned with the changes made during the rewrite.
- The function collects statistics about the rewriting process, including the number of rule applications
  and the total runtime of the rewriter. These statistics are then stored in the model's context for
  performance monitoring and analysis.

✅ Same idea but shorter

# Side-Effects
- Rules can apply side-effects to the model (e.g. adding new constraints or variables).
  The original model is cloned and a modified copy is returned.
- Rule engine statistics (e.g. number of rule applications, run time) are collected and stored in the new model's context.

⚠️ A bit too detailed

# Parameters
- `expression`: A reference to the [`Expression`] that will be evaluated against the given rules. This is the main
   target for rule transformations and is expected to remain unchanged during the function execution.
- `model`: A reference to the [`Model`] that provides context for rule evaluation, such as constraints and symbols.
  Rules may depend on information in the model to determine if they can be applied.
- `rules`: A vector of references to [`Rule`]s that define the transformations to be applied to the expression.
  Each rule is applied independently, and all applicable rules are collected.
- `stats`: A mutable reference to [`RewriterStats`] used to track statistics about rule application, such as
  the number of attempts and successful applications.

✅ Just describing the meaning of arguments will do

(Details of the rewriting process belong on the wiki, and details of underlying types such as Model or Expression are already documented next to their implementations)

- `expression`: A reference to the [`Expression`] to evaluate.
- `model`: A reference to the [`Model`] for access to the symbol table and context.
- `rules`: A vector of references to [`Rule`]s to try.
- `stats`: A mutable reference to [`RewriterStats`] used to track the number of rule applications and other statistics.

This section had been taken from the ‘Documentation Style’ page of the conjure-oxide wiki

Crate Structure

Overview

We follow a “monorepo” approach; That is, a number of related modules are developed in a single repository. This makes it easier to integrate them and test our entire project all at once.

Our repository can be broken down into four key components:

1. The user-facing conjure-oxide command line tool and library, and its integration tests. This is stored in conjure-oxide/conjure_oxide.
2. The AST type definitions, rewrite engine, and related implementation code. These are broken up into separate crates and stored in conjure-oxide/crates/.
3. Rust bindings for solvers; That is, wrapper code and build files that enable us to:

   • Compile solvers (which are developed outside of this project and written in other languages, such as C++) together with our project

   • “Hook into” solver methods and call them from inside our Rust code

     These are stored in conjure-oxide/solvers/ on a per-solver basis.

4. Various other scripts and tools that we use to build, document and test our project. These are stored in conjure-oxide/tools/.

CLI Tool

The command-line conjure-oxide tool is the final product we ship to users. All logic related to the CLI, parsing user input, and displaying solutions is implemented in conjure-oxide/conjure_oxide/src.

This module (called a “crate” in Rust) also re-exports some type definitions and functions from conjure_core and other crates. This is our public, user-facing API that could eventually be used by other people in their projects. At the moment, our project is under development and there is no stable API specification.

There are some examples/ illustrating how various parts of the project are used. Finally, for historical reasons, this folder contains some utility code that may be refactored or moved elsewhere in the future.

Tests

Our suite of integration tests runs automatically on every commit to the main repository. It tests conjure-oxide end-to-end: parsing an example Essence file, running the rewriter, calling the solver, and validating the solution.

The test files are stored in conjure_oxide/tests/integration/, sorted into sub-directories. Code to run our project on these files is contained in integration_tests.rs.

Crates

Most of our implementation is contained in the crates/ directory. Here is an overview of what each crate does:

• conjure_core contains:
  • Our rule engine implementation (conjure_core/src/rule_engine/)
  • The definition of our Abstract Syntax Tree (AST) for Essence; That is, the Rust representation of an Essence program (conjure_core/src/ast)
  • The generic SolverAdaptor interface for interacting with solvers (conjure_core/src/solver)
  • Concrete implementations of SolverAdaptor for each solver we support, such as Minion or RustSAT (conjure_core/src/solver/adaptors)
  • Other miscellaneous types and utilities
• conjure_rules defines rules and rule sets for our rewrite engine to use. Rules are grouped into files and directories based on their purpose: for example, all rules for normalising boolean expressions are in conjure_rules/src/normalisers/bool.rs
• conjure_rule_macros implements the #[register_rule(...)] and #[register_rule_set(...)] procedural macros. See also: Wiki - Rules and RuleSets.
• conjure_essence_parser implements the native Rust parser for Essence. It uses our Tree-sitter grammar, which is defined separately intree-sitter-essence
• conjure_essence_macros implements the essence_expr! procedural macro.
• enum_compatability_macro is a macro that allows us to indicate whether certain features of Essence are compatible with certain solvers, for documentation purposes.
• randicheck is a somewhat separate project developed by Ty (@TAswan) and others. It aims to use Conjure to automatically validate Haskell code and generate minimal failing tests. (TODO is this accurate?)
• tree_morph is a generic library for tree transformations. In the future, it will replace our current rule engine implementation.

Also:

• The uniplate crate, which we use to traverse the AST, used to be part of this repository. It is now maintained separately at https://github.com/conjure-cp/uniplate.

Dependencies

The dependencies between crates are shown bellow.

An arrow A -> B means that A imports from B. The diagram is made using Graphviz, and its source code is located TODO.

Why benchmark?

Benchmarking is an essential part of any coding project, especially when it is performance-oriented. While it can be a little daunting when first getting started, this guide aims to show that benchmarking can be integrated into conjure-oxide and its workflows with a little work.

criterion

By far, the most popular benchmarking tool currently available for Rust is the criterion crate. Based off the Haskell library of the same name, it is a statistics-based tool which aims to measure wall-clock time for individual functions. To get started on criterion benching in a rust project my_project, you first need to make a directory called benches, which Rust will recognise as holding all benchmarking files. Let’s now make a benchmark called my_bench.rs inside of my_project/benches

We now add the following changes to the crate’s cargo.toml file

#![allow(unused)]
fn main() {
[dev-dependencies]
criterion = "0.3"

[[bench]]
name = "my_bench"
harness = false
}

Suppose that we now want to create function to benchmark the addition of two numbers (which, as expected should be very fast!). We add the following to my_bench.

#![allow(unused)]
fn main() {
use criterion::{Criterion, black_box, criterion_group, criterion_main};

pub fn add(x: u64, y: u64) -> u64 {
    x + y
}

pub fn criterion_benchmark(c: &mut Criterion) {
    c.bench_function("add 20 + 20", |b| {
        b.iter(|| add(black_box(20), black_box(20)))
    });
}

criterion_group!(benches, criterion_benchmark);
criterion_main!(benches);
}

The .bench_function method creates an instance of a benchmark. Then the .iter method tells Criterion to repeatedly execute the provided closure. Finally, black_box is used to prevent the compiler from optimising away the code being benchmarked. To run the benchmark simply run cargo bench. Among other things, your terminal should show something alone the lines of: Which shows the average wall-clock time, as well as providing some information on outliers and performance against previous benchmarks. For the full details, see \target\criterion. The .html reports are especially good.

criterion is usually the right tool for most benchmarks, although there are issues. Due to the statistics-driven ethos of criterion, there is currently no one-shot support, with 10 samples being the minimum number of samples for a benchmark. Wall-clock time also gives little insight into where things are slowing in your code, and will not catch things like poor memory locality. Even more crucially, however, is how criterion performs in CI pipelines. The developer’s themselves say the following:

”You probably shouldn’t (or, if you do, don’t rely on the results). The virtualization used by Cloud-CI providers like Travis-CI and Github Actions introduces a great deal of noise into the benchmarking process, and Criterion.rs’ statistical analysis can only do so much to mitigate that. This can result in the appearance of large changes in the measured performance even if the actual performance of the code is not changing.“

As such, we need some other metric apart from wall-clock time to use in order to still run benchmarks in a CI pipeline. This is where the iai-callgrind crate comes in.

iai-callgrind

Iai-Callgrind is a benchmarking framework which uses Valgrind’s Callgrind and other to provide extremely accurate and consistent measurements of Rust code. It does not provide information on wall-clock time, instead focussing on metrics like instruction count and memory hit rates. It is important to note that this will only run on linux, due to the valgrind dependency. Let us create a benchmark called iai-bench in the benches folder. We add the following to cargo.toml

#![allow(unused)]
fn main() {
[profile.bench]
debug = true

[dev-dependencies]
iai-callgrind = "0.14.0"
criterion = "0.3"

[[bench]]
name = "iai-bench"
harness = false
}

To get the benchmarking runner, we can quickly compile from source with cargo install --version 0.14.0 iai-callgrind-runner. To benchmark add using iai-callgrind we add the following to benches/iai-bench.rs.

#![allow(unused)]
fn main() {
use iai_callgrind::{main, library_benchmark_group, library_benchmark};
use std::hint::black_box;

fn add(x: u64, y:u64) -> u64 {
   x+y
}

#[library_benchmark]
#[bench::name(20,20)]
fn bench_add(x: u64,y:u64) -> u64 {
    black_box(add(x,y))
}

library_benchmark_group!(
    name = bench_fibonacci_group;
    benchmarks = bench_add
);

main!(library_benchmark_groups = bench_fibonacci_group);
}

And again run using cargo bench. To specify only running this benchmark we can instead do cargo bench --bench iai-bench. Upon running, you should see something like the following.

As you can see, iai is lightweight, fast and can provide some really accurate statistics on instruction count and memory hits. This makes iai perfect for benching in CI workflows!

Workflows

Once benchmarking is established, workflows are not too difficult to add too. As discussed before, for CI workflows iai should be used, and not criterion. Take the following example from the tree-morph crate. I will put the code below and then briefly explain each portion. It should not be too difficult to adapt to other benchmarks.

name: "iai tree-morph Benchmarks"

on:
  push:
    branches:
      - main 
      - auto-bench 
    paths:
      - conjure_oxide/**
      - solvers/**
      - crates/**
      - Cargo.*
      - conjure_oxide/tests/**
      - .github/workflows/iai-tree-morph-benches.yml
  pull_request:
    paths:
      - conjure_oxide/**
      - solvers/**
      - crates/**
      - Cargo.*
      - conjure_oxide/tests/**
      - .github/workflows/iai-tree-morph-benches.yml
  workflow_dispatch:



jobs:
  benches:
    name: "Run iai tree-morph benchmarks"
    runs-on: ubuntu-latest
    timeout-minutes: 10

    strategy:
      # run all combinations of the matrix even if one combination fails.
      fail-fast: false
      matrix:
        rust_release:
          - stable
          - nightly
    steps:
      - uses: actions/checkout@v4

      - uses: dtolnay/rust-toolchain@stable
        with:
          toolchain: ${{ matrix.rust_release }}

      - name: "Cache Rust dependencies"
        uses: actions/cache@v4
        with:
            path: |
              ~/.cargo/registry
              ~/.cargo/git
              target
            key: ${{ runner.os }}-cargo-${{ matrix.rust_release }}-${{ hashFiles('**/Cargo.lock') }}
            restore-keys: |
              ${{ runner.os }}-cargo-${{ matrix.rust_release }}-
      - name: Install Valgrind
        run: sudo apt-get update && sudo apt-get install -y valgrind

      - name: Install iai-callgrind-runner
        run: cargo install --version 0.14.0 iai-callgrind-runner

      - name: Run tree-morph benchmarks with iai-callgrind
        run: cargo bench --manifest-path crates/tree_morph/Cargo.toml --bench iai-factorial --bench iai-identity --bench iai-modify_leafs > iai_callgrind_output.txt

      - name: Upload artefact
        uses: actions/upload-artifact@v4
        with:
          name: iai-callgrind-results-${{ matrix.rust_release }}
          path: iai_callgrind_output.txt

Some comments:

• name just tells GitHub what to call the workflows
• on tells GitHub when to run the workflow
• jobs is the core of the workflow:
  • strategy specifies that we want to run both nightly and stable rust
  • In steps, we first check out the repository code and set up a specific stable Rust toolchain based on a matrix variable, and then cache Rust dependencies. Next we install the necessary things for valgrind to run, before running benchmarks. We tell the virtual machine to an .txt file and upload it as an artefact.

Design Documents

2023‐11: High Level Plan

This page is a summary of discussions about the architecture of the project circa November 2023.

In brief:

Conjure Oxide

Model Rewriting Engine

The purpose of the model rewriting engine is to turn a high level constraints model into one that can be run by various solvers. It incrementally rewrites a given model by applying a series of rules.

Rules have the type:

rule :: fn(Expr) -> Result<Expr,Error>

The use of Result here allows for the type checking of the Model at each stage (amongst other things).

A sketch of a rewriting algorithm is below. As we are using a Result type, backtracks occur when an Err is returned.

fn apply(rules,x) {
  new_rules = getApplicable(rules)

  if shouldStop(x) {
    return Ok(x)
  }
 
 // Recursive case - multiple rules
  while len(rules') > 0 {
   rule = select(new_rules)
   new_rules.remove(rule)
   res = apply(rules,rule(x))

   if res is Ok, return Ok
  }

  // No rules - base case
  if (compatibleWithSolver(x)) {
    return Ok(x)
  }

  return Err()
}

This is, in effect, a recursive tree search algorithm. The behaviour of the search can be changed by changing the following functions:

• getApplicable: fn(Vec<Rule>) -> Vec<Rule>
• select: fn(Vec<Rule>) -> Vec<Rule>
• shouldStop: fn(x) -> bool

The following functions are also important to implement the rewriting engine:

domainOf:: Expr -> Domain
typeOf:: Expr -> Type
typeOfDomain:: Domain -> Type
categoryOf:: Expr -> Category

data Category = Decision | Unknown | Quantified

Solver Adaptors

Once we have a Model object that only uses constraints supported by a particular solver, we are able to translate it to a form the solver understands.

The solver adaptor layer translates a Model into solver specific data-structures, and then runs the solvers.

If the given Model isn’t compatible with the solver, the use of a Result type here could allow a type error to be thrown.

Other crates inside this repository

This repository contains the code for Conjure Oxide as well as the code for some of its dependencies and related works.

Currently, these are just Rust crates that provide low level bindings to various solvers.

There should be a strict separation of concerns between each crate and Conjure Oxide. In particular, each crate in this project should be considered a separate piece of work that could be independently published and used. Therefore:

• The crate should have its own complete documentation and examples.
• The public API should be safe and make sense outside the context of Conjure Oxide.

Solver Crates

Each solver crate should have a API that matches the data structures used by the solver itself.

Eventually, there will be a way to generically call solvers using common functions and data structures. However, this is to be defined entirely in Conjure Oxide and should not affect how the solver crates are written. See Solver Adaptors.

This section had been taken from the ‘2023‐11: High Level Plan’ page of the conjure-oxide wiki

2024‐03: Implementing Uniplates and Biplates with Structure Preserving Trees

Contents:

• Recap: Uniplates and Biplates
• Definition of Children
• Storing The Structure of Children
• Uniplates and Biplates Using Structure Preserving Trees

Comments and discussion about this document can be found in issue #261.

In #180 and #259 we implemented the basic Uniplate interface and a derive macro to automatically implement it for enum types. However, our current implementation is incorrect and problematic: we have defined children wrong; and our children list does not preserve structure, making more complex nested structures hard to recreate in the context function.

Recap: Uniplates and Biplates

A quick recap of what we are trying to do - for details, see the Uniplate Haskell docs, our Github Issues, and the paper.

Uniplates are an easy way to perform recursion over complex recursive data types.

It is typically used with enums containing multiple variants, many of which may be different types.

data T = A T [Integer]
       | B T T
       | C T U
       | D [T]

With Uniplate, one can perform a map over this with very little or no boilerplate.

This is implemented with a single function uniplate that returns a list of children of the current object and a context function to rebuild the object from a list of children.

Biplates provide recursion over instances of type T within some other type U. They are implemented with a single function biplate of similar type to uniplate (returning children and a context function).

These functions are able to be implemented on any data type through macros making Uniplate operations boilerplate free.

Definition of Children

We currently take children of T to mean direct descendants of T inside T. However, the correct definition of children is maximal substructures of type T.

For example, consider these Haskell types:

data T = A T [Integer]
       | B T T
       | C T U
       | D [T]

data U = E T T
       | F Integer
       | G [T] T

Our current implementation would define children as the following:

children (A t1 _) = [t1]
children (B t1 t2) = [t1, t2]
children (C t1 u) = [t1]
children (D ts) = ts

However, the proper definition should support transitive children - i.e. T contains a U which contains a T:

children (A t1 _) = [t1]
children (B t1 t2) = [t1, t2]
children (C t1 (E t2 t3)) = [t1,t2,t3]
children (C t1 (F _)) = [t1]
children (C t1 (G ts t3)) = [t1] ++ ts ++ [t3]
children (D ts) = ts

While a seemingly small difference, this complicates how we reconstruct a node from its children: we now need to create a context that takes a list of children and creates an arbitrarily deeply nested data structure containing multiple different types. In particular, the challenge is keeping track of which elements of the children list go into which fields of the enum we are creating.

We already had this problem dealing with children from lists, but a more general approach is needed.

Storing The Structure of Children

How do we know which children go into which fields of the enum variant?

For example, consider this complicated instance of T:

data T = A T [Integer]
       | B T T
       | C T U 
       | D [T]

data U = E T T
       | F Integer
       | G [T] T

myT = C(D([t0,...,t5),G([t6,...,t12],t13))

Its list of children is: [t0,...,t13].

Try creating a function to recreate myT based on a new list of children. Hint: it is difficult, and even more so in full generality!

If we instead consider children to be a tree, where each field in the original enum variant is its own branch, we get:

data Tree A = Zero | One A | Many [(Tree A)]

myTChildren = 
  Many [(Many [One(t0),...,One(t5)]),      -- C([XXX], _) field 1 of C
        (Many [                            -- C([_],XXX)  field 2 of C
          (Many [One(t6),...,One(t12)]),   -- G([XXX],_)  field 2.1 of C
          (One  t13))]                     -- G([_],XXX)) field 2.2 of C

This captures, in a type-independent way, the following structural information:

1. myT has two fields.
2. The first field is a container of Ts.
3. The second field contains two inner fields: one is a container of Ts, one is a single T.

Representing non-recursive and primitive types

Often primitive and non-recursive types are found in the middle of enum variants. How do we say “we don’t care about this field, it does not contain a T” with our Tree type? Zero can be used for this.

For example:

data V = V1 V Integer W
       | V2 Integer

data W = W1 V V

myV = (V1 
        (V2 1) 
        1 
        (W1 
          (V2 2) 
          (V2 3)))

myVChildren = 
  (Many [
    (One v1),  -- V1(XXX,_,_)
    Zero,      -- V1(_,XXX,_) 
    (Many [    -- V1(_,_,XXX)
      (One v2),
      (One v3)
   ]))

This additionally encodes the information that the second field of myV has no Ts at all.

While this information isn’t too useful for finding or traversing over the target type, it means that the tree structure defines the structure of the target type completely: there are always the same number of tree branches as there are fields in the enum variant.

Uniplates and Biplates Using Structure Preserving Trees

Recall that the uniplate function returns all children of a data structure alongside a context function that rebuilds the data structure using some new children.

To implement this, for each field in an enum variant, we need to ask the questions: “how do we get the type Ts in the type U”, and “how can we rebuild this U based on some new children of type T?”.

This is just a Biplate<U,T>, which gives us the type T children within a type U as well as a context function to reconstruct the U from the T.

Therefore:

• We build the children tree by combining the children trees of all fields of the enum (such that each field’s children is a branch on the tree).

• We build the context function by calling each fields context function on each branch of the input tree.

This is effectively a recursive invocation of Biplate.

What happens when we reach a T? Under the normal definition, Biplate<T,T> would return its children. This is wrong - we want to return T here, not its children!

When T == U we need to change the definition of a Biplate: Biplate<T,T> operates over the input structure, not its children.

For our example AST:

data T = A T [Integer]
       | B T T
       | C T U 
       | D [T]

data U = E T T
       | F Integer
       | G [T] T

Here are some Biplate and Uniplates and their resultant children trees:

• Biplate<Integer,T> 1 is Zero.

• Uniplate<T> (A t [1,2,3]) is (Many [Biplate<T,T> t ,Zero]).

  This evaluates to (Many [(One t),Zero])

• Biplate<T,T> t is One t.

• Biplate<T,U> (G ts t1) is (Many [Biplate<T,[T]> ts , Biplate<T,T> t ]).

  This evaluates to (Many [(Many [(One t0),...(One tn)]),(One t)])

• Uniplate<T,T> (C t (G ts t1)) is (Many [Biplate<T,T> t, Biplate<U,T> (G ts t1))

  This evaluates to (Many [(One t), (Many [(Many [(One t0),...,(One tn)]), (One t)]))

This section had been taken from the ‘2024‐03: Implementing Uniplates and Biplates with Structure Preserving Trees’ page of the conjure-oxide wiki

Semantics of Rewriting Expressions with Side‐Effects

Overview

When rewriting expressions, a rule may occasionally introduce new variables and constraints. For example, a rule which handles the Min expression may introduce a new variable aux which represents the minimum value itself, and introduce constraints aux <= x for each x in the original Min expression. Conjure and Conjure Oxide provide similar methods of achieving these “side-effects”.

Reductions

In Conjure Oxide, reduction rules return Reduction values. These contain a new expression, a new (possibly empty) set of top-level constraints, and a new (possibly empty) symbol table. The two latter values are brought up to the top of the AST during rewriting and joined to the model. These reductions, or “local sub-models” therefore can define new requirements which must hold across the model for the change that is made to a specific node of the AST to be valid.

The example with Min given in the overview is one case where plain Reductions are used, as a new variable with a new domain is introduced, along with constraints which must hold for that variable.

Bubbles

Reductions are not enough in all cases. For example, when handling a possibly undefined value, changes must be made in the context of the current expression. Simply introducing new top-level constraints may lead to incorrect reductions in these cases. The Bubble expression and associated rules take care of this, bringing new constraints up the tree gradually and expanding in the correct context.

Essentially, Bubble expressions are a way of attaching a constraint to an expression to say “X is only valid if Y holds”. One example of this is how Conjure Oxide handles division. Since the division expression may possibly be undefined, a constraint must be attached to it which asserts the divisor is != 0.

An example of division handling is shown below. Bubbles are shown as {X @ Y}, where X is the expression that Y is attached to.

!(a = b / c)                 Original expression

!(a = {(b / c) @ c != 0})    b/c is possibly undefined, so introduce a bubble saying the divisor is != 0

!({(a = b / c) @ c != 0})    "bubble up" the expression, since b / c is not a bool-type expression

!(a = b / c /\ c != 0)       Now that X is a bool-type expression, we can simply expand the bubble into a conjunction

Why not just use Reductions to assert at the top-level of the model that c != 0? In the context of undefinedness handling, the final reduction is dependent on the context it occurs in. In the above example, if we continue by simplifying (apply DeMorgan’s), we can see that it becomes a != b / c \/ c = 0. Thus, c = 0 is a valid assignment for this example to be true, and setting c != 0 on the top-level would be incorrect.

In Conjure Oxide, Bubbles are often combined with the power of Reductions to provide support for solvers like Minion.

This section had been taken from the ‘Semantics of Rewriting Expressions with Side‐Effects’ page of the conjure-oxide wiki

What we didn’t do

The intention of this page is to chronicle decisions made during the development of conjure-oxide. There have been many situations where we have thought of something interesting that ends up not being the best solution to a problem and we believe others may come up with the same ideas. This page should be read before contributing so that potential contributors do not go down rabbit holes that have already been thoroughly searched.

Nested expressions within the polymorphic metadata field

Background

As discussed in Issue 182, we wanted to create a polymorphic metadata field that would be contained within the expression struct and that could be changed on a case-by-case basis as metadata might only be needed for a single module for example.

What we thought of

One interesting idea that was suggested as a structure like this:

#![allow(unused)]
fn main() {
// Define a trait for metadata in each module.
pub trait Metadata {
    // Define methods specific to the metadata.
    fn print_metadata(&self);
    // Add other methods as needed.
}

// Module-specific metadata types.
pub mod module1 {
    pub struct Metadata1 {
        // Define fields specific to this metadata.
        pub clean: bool,
        // Add other fields as needed.
    }

    impl super::Metadata for Metadata1 {
        fn print_metadata(&self) {
            println!("Metadata1: Clean - {}", self.clean);
        }
    }
}

pub mod module2 {
    pub struct Metadata2 {
        // Define fields specific to this metadata.
        pub status: String,
        // Add other fields as needed.
    }

    impl super::Metadata for Metadata2 {
        fn print_metadata(&self) {
            println!("Metadata2: Status - {}", self.status);
        }
    }
}

// Modify the Expression enum to hold a trait object for metadata.
#[derive(Clone, Debug)]
pub enum Expression {
    // Existing enum variants here...
    WithMetadata(Box<Expression>, Option<Box<dyn Metadata>>),
}

impl Expression {
    // Create a new expression with metadata.
    pub fn with_metadata(expr: Expression, metadata: Option<Box<dyn Metadata>>) -> Expression {
        Expression::WithMetadata(Box::new(expr), metadata)
    }

    // Extract the expression and metadata.
    pub fn extract_metadata(self) -> (Expression, Option<Box<dyn Metadata>>) {
        match self {
            Expression::WithMetadata(expr, metadata) => (*expr, metadata),
            _ => (self, None),
        }
    }

    // Set metadata for an expression.
    pub fn set_metadata(&mut self, metadata: Option<Box<dyn Metadata>>) {
        if let Expression::WithMetadata(_, ref mut existing_metadata) = *self {
            *existing_metadata = metadata;
        }
    }

    // Get metadata for an expression.
    pub fn get_metadata(&self) -> Option<&dyn Metadata> {
        if let Expression::WithMetadata(_, Some(metadata)) = self {
            Some(metadata.as_ref())
        } else {
            None
        }
    }

    // Existing methods here...
}

}

Why we didn’t do it

This is nice in the sense that there is less “ugliness” when creating expressions as there is no need to have metadata in every enum variant. However, this severely effects the way that the rewriter traverses the AST as there is now WithMetadata objects sprinkled throughout the AST which would require some way to traverse up the tree while saving the context of nodes below the metadata object. This image shows the differences in a basic AST:

What we did do

Due to this issue we decided that a simpler implementation where metadata is explicitly required every time but could be set to some empty metadata object was more practical. More details on this implementation can found in Near Future PR

This section had been adapted from the ‘What we didn’t do’ page of the conjure-oxide wiki

CI/CD

Coverage

User Guide

1. Run coverage with ./tools/coverage.sh.

2. Open this in a web-browser by opening target/debug/coverage/index.html.

3. An lcov file is generated at target/debug/lcov.info for in-editor coverage.

   • If you use VSCode, configuration for this should be provided when you clone the repo. Click the “watch” button in the status bar to view coverage for a file.

Implementation

See the code for full details: tools/coverage.sh.

A high level overview is:

1. The project is built and tested using instrumentation based coverage.
2. Grcov is used to aggregate these reports into lcov.info and html formats.
3. The lcov.info file can be used with the lcov command to generate summaries and get coverage information. This is used to make the summaries in our PR coverage comments.

Reading:

1. grcov README - how to generate coverage reports.
2. rustc book - details on instrumentation based coverage.

Doc Coverage

Text: This prints a doc coverage table for all crates in the repo:

RUSTDOCFLAGS='-Z unstable-options --show-coverage' cargo +nightly doc --workspace --no-deps 

JSON: Although we don’t use it yet, we can get doc coverage information as JSON. This will be useful for prettier and more useful output:

RUSTDOCFLAGS='-Z unstable-options --show-coverage --output-format json' cargo +nightly doc --workspace --no-deps 

Reading

See the unstable options section of the rustdoc book. Link.

This section had been taken from the ‘Coverage’ page of the conjure-oxide wiki

Github Actions Cookbook

• This document lists common patterns and issues we’ve had in our Github actions, and practical solutions to them.
• The first point of reference should be the official documentation, but if that is ever unclear, here would be a good place to look!

Terminology used in this document:

• A workflow contains multiple independently ran tasks. Each task runs a series of steps. Steps can call predefined actions, or run shell commands.

I want to have a step output multilined / complex text

- name: Calculate PR doc coverage
  id: prddoc
  run: |
    RUSTDOCFLAGS='-Z unstable-options --show-coverage' cargo +nightly doc --workspace --no-deps > coverage.md
    echo 'coverage<<EOFABC' >> $GITHUB_OUTPUT
    echo "$(cat coverage.md)" >> $GITHUB_OUTPUT
    echo 'EOFABC' >> $GITHUB_OUTPUT```

The entire output of cargo doc can be substituted into later jobs by using ${{ steps.prdoc.outputs.coverage }}

workflow_run: I want a workflow that runs on a PR and can write to the repo

PR branches and their workflows typically live in on a branch on an external fork. Therefore, they cannot write to the repository. The solution is to split things into two workflows - one that runs on the PR with read-only permissions, and one that runs on main and can write to the repository. This is called a workflow_run workflow. Read the docs.

The workflow_run workflow should not run any user provided code as it has secrets in scope.

I want to access the calling PR in a workflow_run workflow

workflow_run jobs do not get access to the calling workflows detail. While one can access some things via the Github API such as head_sha, head_repo, this may not give any PR information. Github recommends saving the PR number to an artifact, and using this number to fetch the PR info through the API:

Example from this github blog post - see this for more explanation and details!

name: Receive PR

# read-only repo token
# no access to secrets
on:
  pull_request:

jobs:
  build:
    runs-on: ubuntu-latest

    steps:        
      - uses: actions/checkout@v2

      # imitation of a build process
      - name: Build
        run: /bin/bash ./build.sh

      - name: Save PR number
        run: |
          mkdir -p ./pr
          echo ${{ github.event.number }} > ./pr/NR
      - uses: actions/upload-artifact@v2
        with:
          name: pr
          path: pr/

name: Comment on the pull request

# read-write repo token
# access to secrets
on:
  workflow_run:
    workflows: ["Receive PR"]
    types:
      - completed

jobs:
  upload:
    runs-on: ubuntu-latest
    if: >
      github.event.workflow_run.event == 'pull_request' &&
      github.event.workflow_run.conclusion == 'success'
    steps:
      - name: 'Download artifact'
        uses: actions/github-script@v3.1.0
        with:
          script: |
            var artifacts = await github.actions.listWorkflowRunArtifacts({
               owner: context.repo.owner,
               repo: context.repo.repo,
               run_id: ${{github.event.workflow_run.id }},
            });
            var matchArtifact = artifacts.data.artifacts.filter((artifact) => {
              return artifact.name == "pr"
            })[0];
            var download = await github.actions.downloadArtifact({
               owner: context.repo.owner,
               repo: context.repo.repo,
               artifact_id: matchArtifact.id,
               archive_format: 'zip',
            });
            var fs = require('fs');
            fs.writeFileSync('${{github.workspace}}/pr.zip', Buffer.from(download.data));
      - run: unzip pr.zip

      - name: 'Comment on PR'
        uses: actions/github-script@v3
        with:
          github-token: ${{ secrets.GITHUB_TOKEN }}
          script: |
            var fs = require('fs');
            var issue_number = Number(fs.readFileSync('./NR'));
            await github.issues.createComment({
              owner: context.repo.owner,
              repo: context.repo.repo,
              issue_number: issue_number,
              body: 'Everything is OK. Thank you for the PR!'
            });

How do I get x commit inside a PR workflow? What do all the different github sha’s mean?

If you are running in a workflow_run workflow, you will need to get the calling PR first. See I want to access the calling PR in a workflow_run workflow instead.

The default github.sha is a temporary commit representing the state of the repo should the PR be merged now. You probably want github.event.pull_request.head.sha. Read The many SHAs of a github pull request.

This section had been taken from the ‘Github Actions’ page of the conjure-oxide wiki

Test GitHub Actions Locally With act

This guide shows how to run GitHub Actions workflows locally using act. It is useful for fast feedback on CI changes without waiting for a remote run.

For details on installation and advanced usage, see https://nektosact.com/.

Quick start

1. Install act (see the official site for the latest install steps).
2. From the repo root, run a workflow event, for example:

act --container-architecture linux/amd64

This repo works best with the catthehacker/ubuntu:act-latest image. It includes common CI tooling and matches GitHub-hosted Ubuntu runners more closely than the default image. The act default image can be configured at runtime; see https://nektosact.com/ for details.

Common usage patterns

• Run a specific workflow file:

act -W .github/workflows/ci.yml --container-architecture linux/amd64

• Run a specific job:

act -j test --container-architecture linux/amd64

• Provide secrets locally (example):

act --secret-file .secrets --container-architecture linux/amd64

• Run the Vale job for pull requests:

act pull_request --job vale --container-architecture linux/amd64

In this repo, the vale job is part of the pull request workflows, so this command runs that job locally against a simulated pull_request event. It uses the recommended catthehacker/ubuntu:act-latest image by default, and you can configure the image at runtime; see https://nektosact.com/usage/runners.html#alternative-runner-images/ for details.

Limitations to keep in mind

• Workflow triggers: some events (workflow_run, pull_request_target, scheduled jobs) do not behave exactly like GitHub and may need extra inputs or manual flags.
• GitHub API usage: steps that call the GitHub API (releases, issues, PR comments, status checks) require valid tokens and may still diverge from real GitHub behavior.
• Deployment workflows: jobs that deploy (cloud credentials, OIDC, environment protection rules) are hard to reproduce locally and are better validated in a real GitHub run.
• Hosted services and caches: actions depending on GitHub-hosted caches or services may be no-ops or behave differently.
• Matrix and concurrency: complex matrices, concurrency groups, and reusable workflows can be partially supported but may require extra configuration or run differently.

When in doubt, use act for fast iteration, then confirm changes with a real GitHub Actions run.

Overview

The parser converts incoming Essence programs to Conjure Oxide to the Model Object that the rule engine takes in. The relevant parts of the Model object are the SymbolTable and Expression objects. The symbol table is essentially a list of the variables and their corresponding domains. The Expression object is a recursive object that hold all the constraints of the problem, nested into one object. The parser has two main parts. The first the tree-sitter-essence crate, which is a general Essence parser using the library tree-sitter. The second part is the conjure_essence_parser crate which is Rust code that uses the grammar to parse Essence programs and convert them into the above-mentioned Model object.

Tree Sitter Grammar

Tree-sitter is a parsing library that creates concrete syntax trees from programs in various languages. It contains many languages already, but Essence is unfortunately not one of them. Therefore, this crate contains a JavaScript grammar for Essence, which tree-sitter uses to create a parser. The parser is not specific to Conjure Oxide as the grammar merely describes the general Essence language, but it is used in Conjure Oxide and currently covers only parts of the Essence language that Conjure Oxide deals with and has tests written for. Therefore, it is not extensive and relatively simple in structure.

General Structure

At the top level, there can be either find statements, letting statements, and constraint statements. Find statements consist of the keyword find, one or more variables, and then a domain of either type boolean or integer. Letting statements have the keyword letting, one or more variables, and an expression or domain to assign to those variables. Constraints contain the keyword such that and one or more logical or numerical expressions which include variables and constants.

Expression Hierarchy

Expressions in the grammar are broken down into boolean expressions, comparison expressions, and arithmetic expressions. This separation helps enforce semantic constraints inherent to the language. For example, expressions like x + 3 = y are allowed because an arithmetic expression is permitted on either side of a comparison, but chained comparisons like x = y = 3 are disallowed, since a comparison expression cannot itself contain another comparison expression as an operand. This also helps ensure the top-most expression in a constraint evaluates to a boolean (so such that x + 3 wouldn’t be valid). There are also atom expressions such as constants, identifiers, and structured values (tuples, matrices, or slices), which are allowed as operands to most expressions since they might be booleans. This does mean, however, that a constraint like such that y would be valid even though y might be an integer. Quantifier expressions are also separated into boolean and arithmetic quantifiers for this reason (so such that allDif{[a, b]} is valid but such that min{[a,b]} isn’t).

The precedence levels throughout the grammar are based on the Essence prime operator precedence table found in Appendix B of the Savile Row Manual. This is important to ensure that nested or complicated expressions such as (2*x) + (3*y) = 12 are parsed in the correct order, as this will determine the structure of the Expression object in the Model.

Issue #763

Currently, the grammar allows for any combination of letters, numbers, and underscores to be parsed as a variable identifiers. This includes reserved keywords of the Essence language such as ‘find’ or ‘letting’. This is incorrect and such keyword shouldn’t be allowed as variables. A solution to this problem hasn’t been found. Below are notes about possible solutions.

• Tree-sitter doesn’t support lookahead assertions so grammar rules cannot exclude specific patterns or words.
• Defining rules for each keyword (with higher precedence than the identifier rule) has been brought up but it doesn’t stop keywords from being parsed as variables within a rule searching for identifiers (more detail in linked issue).
• It is possible to manually check all identifier nodes in the parse tree within the Rust program against a list of keywords (or by defining rules for keywords and allowing identifiers to be parsed as them or a valid identifier). This would allow for rejecting Essence programs that merely use a keyword as an identifier and have no other errors but wouldn’t allow for correct parsing of errors such as the one in line 2 of the program below. The extra ‘=’ in line two causes ‘such’ in line 3 to be parsed as an identifier and thus the whole of line 3 is parsed as an error, even though it is valid. If ‘such’ could be excluded as a valid identifier, the error would be only in line 2.

find x,y,z : int(0..5)
such that x = y =
such that z = 3

Rust Parser

This is the second part of the parser and is contained in the conjure_essence_parser crate. The primary function is parse_essence_file_native, shown below, which takes in the path to the input and the context and returns the Model or an error.

pub fn parse_essence_file_native(
    path: &str,
    context: Arc<RwLock<Context<'static>>>,
) -> Result<Model, EssenceParseError> {...}

Within that function, the source code is read from the input and the tree-sitter grammar is used to parse that code and produce a parse tree. From there, a Model object is created and the SymbolTable and Expression fields are populated by traversing and extracting information from the parse tree.

General Structure and utils

The top level nodes (children of the root node), are either extras (comments or language labels), find statements, letting statements, or constraints. Find and letting statements provide info that is added to the SymbolTable while constraints are added to the Expression.

In general, kind() is used to determine which rule a node represents and the corresponding function or logic is then applied to that node. Child nodes are found using their field names or indexes and the named_children() function is used to iterate over the named child nodes of a node. The function child_expr returns the Expression parsed from the first named child of the given node.

Extracting from the source code (identifiers and constants)

The tree-sitter nodes have a start and end byte indicating where the node corresponds to in the source code. For variable identifiers, constants, and operators, these bytes are necessary to extract the actual values from the source code.

For example, the following code appears in the parse_find_statement function and is used to extract the specific variable name from the source code, which is represented simply by a tree-sitter node (named variable in this case).

let variable_name = &source_code[variable.start_byte()..variable.end_byte()];

Another example is when parsing expressions, the node representing the operator is not always ‘named’, meaning it is not its own rule in the grammar and rather specified directly in the rule (ex. exponent: $ => seq($.arithmetic_expr, "**", $.arithmetic_expr) (simplified)), or the operator one of multiple choices in a rule (ex. mulitcative_op: $ => choice("*", "/", "%")). In this situation, the same method as for the variable identifiers is used:

let op = constraint.child_by_field_name("operator").ok_or(format!(
        "Missing operator in expression {}",
        constraint.kind()
    ))?;
let op_type = &source_code[op.start_byte()..op.end_byte()];

Find and Letting Statements

Find and letting statements are parsed relatively intuitively. For find statements, the list of variables is iterated over and each is added to a hash map as the key. Then, the domain is parsed and added as the value for each variable it applies to. Once all variables and domains are parsed, the hash map is returned and the caller function iterates over it and adds each pair to the SymbolTable. For letting statements, a new SymbolTable is created. The variables are again iterated over and added to the table. Letting statements can either specify a domain or an expression for the variables so the type of node is checked and either parsed as an expression or domain before being added to the table. The SymbolTable is returned and the caller function adds it to the existing SymbolTable of the Model.

Constraints

Adding constraints to the overall constraints Expression requires nesting Expression objects in a consistent and clear manner. Each constraint is parsed using the parse_expression function, which returns an Expression object, and is then added to the model using the add_constraints function. The parse_expression function takes a node as a parameter and is recursive. It matches the node to its ‘kind’, recursively parses the children of the node, then returns an Expression object that correctly packages up the expressions returned from the parsing of the children nodes.

This structure allows for easy addition of more complex constraints as the grammar evolves. As more rules are added to the grammar, the corresponding code block must be added to the match statement in the parse_expression function.

Example

The constraint x = 3 would be represented by a comparison_expr node, which is defined in the grammar as:

comparison_expr: $ => prec(0, prec.left(seq(
      field("left", choice($.boolean_expr, $.arithmetic_expr)), 
      field("operator", $.comparative_op),
      field("right", choice($.boolean_expr, $.arithmetic_expr))
    ))),

In the parse_expression function, the left expression is parsed using the child_expr function. The returned Expression would represent the variable x and be saved as expr1. The operator is extracted from the source code and saved as op_type. The right expression node is then found using its field name ‘right’ and parsed. The returned Expression would represent the integer 3 and be saved as expr2.

let expr1 = child_expr(constraint, source_code, root)?;
            let op = constraint.child_by_field_name("operator").ok_or(format!(
                "Missing operator in expression {}",
                constraint.kind()
            ))?;
            let op_type = &source_code[op.start_byte()..op.end_byte()];
            let expr2_node = constraint.child_by_field_name("right").ok_or(format!(
                "Missing second operand in expression {}",
                constraint.kind()
            ))?;
            let expr2 = parse_expression(expr2_node, source_code, root)?;

            match op_type {...}

Depending on the operator type (in this case =), the left and right expressions are added to an Expression of the relevant type (in this case Eq), which is returned.

"=" => Ok(Expression::Eq(
                    Metadata::new(),
                    Box::new(expr1),
                    Box::new(expr2),
                )),

Tree-morph is a library that helps you perform boilerplate-free generic tree transformations. In its current state, tree-morph is able to perform transformations in a large number of test cases, and work is now being done to try to implement Essence with tree-morph. When completed, tree-morph will be a very powerful stand-alone crate, as well as sitting at the core of conjure-oxide. Despite its current power, there is a still a lot of work to be done on the tree-morph crate. It is currently in a completely unoptimised state, and will be very slow when performing on large trees with a rich rule set and rule hierarchy. In order to assess progress on new optimisations, it is essential to have a diverse list of benchmarks. All benchmarking has been done using the criterion crate. The following section outlines some of the most important benchmarks.

Benchmarks

identity

The identity benchmark is a test designed to capture how long one tree traversal takes. There is no metadata, and the only rule is do_nothing which is never evaluated. The helper function construct_tree creates a simple tree of variable depth. This is an important benchmark to make sure that new proposed changes do not negatively effect tree-morph traversal speed.

Filename: conjure-oxide/crates/tree_morph/benches/identity.rs

#![allow(unused)]
fn main() {
use criterion::{black_box, criterion_group, criterion_main, Criterion};
use tree_morph::prelude::*;
use uniplate::derive::Uniplate;

#[derive(Debug, Clone, PartialEq, Eq, Uniplate)]
#[uniplate()]
enum Expr {
    Branch(Box<Expr>, Box<Expr>),
    Val(i32),
}
struct Meta {}
fn do_nothing(cmds: &mut Commands<Expr, Meta>, subtree: &Expr, meta: &Meta) -> Option<Expr> {
    None
}

fn construct_tree(n: i32) -> Box<Expr> {
    if n == 1 {
        Box::new(Expr::Val(0))
    } else {
        Box::new(Expr::Branch(Box::new(Expr::Val(0)), construct_tree(n - 1)))
    }
}

pub fn criterion_benchmark(c: &mut Criterion) {
    let base: i32 = 2;
    let expr = *construct_tree(base.pow(5));
    let rules = vec![vec![do_nothing]];

    c.bench_function("Identity", |b| {
        b.iter(|| {
            morph(
                black_box(rules.clone()),
                select_first,
                black_box(expr.clone()),
                Meta {},
            )
        })
    });
}

criterion_group!(benches, criterion_benchmark);
criterion_main!(benches);
}

modify_leafs

The modify_leafs benchmark is designed to capture how long it takes for a simple modification rule to be applied to all of the leaf nodes. The function construct_tree creates a tree of variable depth with all leaf nodes initialised to 0. There is no metadata and the only function zero_to_one changes a leaf node of 0 to a leaf node of 1. It should be expected that this will take a lot longer than the identity benchmark, as when a node is changed in tree-morph, an entirely new tree is created.

Filename: conjure-oxide/crates/tree_morph/benches/modify_leafs.rs

#![allow(unused)]
fn main() {
use criterion::{black_box, criterion_group, criterion_main, Criterion};
use tree_morph::prelude::*;
use uniplate::derive::Uniplate;

#[derive(Debug, Clone, PartialEq, Eq, Uniplate)]
#[uniplate()]
enum Expr {
    Branch(Box<Expr>, Box<Expr>),
    Val(i32),
}

struct Meta {} // not relevant for this benchmark

fn zero_to_one(cmds: &mut Commands<Expr, Meta>, subtree: &Expr, meta: &Meta) -> Option<Expr> {
    if let Expr::Val(a) = subtree {
        if let 0 = *a {
            return Some(Expr::Val(1));
        }
    }
    None
}

fn construct_tree(n: i32) -> Box<Expr> {
    if n == 1 {
        Box::new(Expr::Val(0))
    } else {
        Box::new(Expr::Branch(Box::new(Expr::Val(0)), construct_tree(n - 1)))
    }
}

pub fn criterion_benchmark(c: &mut Criterion) {
    let base: i32 = 2;
    let expr = *construct_tree(base.pow(5));
    let rules = vec![vec![zero_to_one]];

    c.bench_function("Modify_leafs", |b| {
        b.iter(|| {
            morph(
                black_box(rules.clone()),
                select_first,
                black_box(expr.clone()),
                Meta {},
            )
        })
    });
}

criterion_group!(benches, criterion_benchmark);
criterion_main!(benches);
}

factorial

The factorial benchmark is the most difficult benchmark currently made, and an improved score on factorial will be indicative of serious gains in optimisations. As the name suggests, factorial is centred around the mathematical factorial operation (5! = 5*4*3*2*1), which will grow the tree depth, providing a rich set of transformations for tree-morph to calculate. The tree generating function random_exp_tree here takes as input a random seed and a max depth, and generates a tree of an arithmetic expression involving values, additions, multiplications and factorials. An example of such an expression with a random seed of 41 and a max depth of 5 is shown below.

(((8 + 1!) + (1 * 3)!) + (1!! * ((2 + 1) * (1 * 1))))!

It is worth mentioning that this expression is extremely large due to the nested factorials, and as such we need a way of making sure that calculations are bounded. This is achieved by modding the results of any additions and multiplications in the rule_eval_add and rule_eval_mul functions by 10, which will bound all factorial expressions by 10!. The benchmark counts the number of addition and multiplication rule applications, and also has a high priority dummy rule do_nothing, in order to increase the benchmark difficulty.

Filename: conjure-oxide/crates/tree_morph/benches/factorial.rs

#![allow(unused)]
fn main() {
use criterion::{black_box, criterion_group, criterion_main, Criterion};
use rand::rngs::StdRng;
use rand::{Rng, SeedableRng};
use tree_morph::prelude::*;
use uniplate::derive::Uniplate;

#[derive(Debug, Clone, PartialEq, Eq, Uniplate)]
#[uniplate()]
enum Expr {
    Add(Box<Expr>, Box<Expr>),
    Mul(Box<Expr>, Box<Expr>),
    Val(i32),
    Factorial(Box<Expr>),
}

fn random_exp_tree(rng: &mut StdRng, count: &mut usize, depth: usize) -> Expr {
    if depth == 0 {
        *count += 1;
        return Expr::Val(rng.random_range(1..=3));
    }

    match rng.random_range(1..=13) {
        x if (1..=4).contains(&x) => Expr::Add(
            Box::new(random_exp_tree(rng, count, depth - 1)),
            Box::new(random_exp_tree(rng, count, depth - 1)),
        ),
        x if (5..=8).contains(&x) => Expr::Mul(
            Box::new(random_exp_tree(rng, count, depth - 1)),
            Box::new(random_exp_tree(rng, count, depth - 1)),
        ),
        x if (8..=11).contains(&x) => {
            Expr::Factorial(Box::new(random_exp_tree(rng, count, depth - 1)))
        }
        _ => Expr::Val(rng.random_range(1..=10)),
    }
}
fn do_nothing(cmds: &mut Commands<Expr, Meta>, subtree: &Expr, meta: &Meta) -> Option<Expr> {
    None
}

fn factorial_eval(cmds: &mut Commands<Expr, Meta>, subtree: &Expr, meta: &Meta) -> Option<Expr> {
    if let Expr::Factorial(a) = subtree {
        if let Expr::Val(n) = *a.as_ref() {
            if n == 0 {
                return Some(Expr::Val(1));
            }
            return Some(Expr::Mul(
                Box::new(Expr::Val(n)),
                Box::new(Expr::Factorial(Box::new(Expr::Val(n - 1)))),
            ));
        }
    }
    None
}

fn rule_eval_add(cmds: &mut Commands<Expr, Meta>, subtree: &Expr, meta: &Meta) -> Option<Expr> {
    if let Expr::Add(a, b) = subtree {
        if let (Expr::Val(a_v), Expr::Val(b_v)) = (a.as_ref(), b.as_ref()) {
            cmds.mut_meta(|m| m.num_applications_addition += 1);
            return Some(Expr::Val((a_v + b_v) % 10));
        }
    }
    None
}

fn rule_eval_mul(cmds: &mut Commands<Expr, Meta>, subtree: &Expr, meta: &Meta) -> Option<Expr> {
    if let Expr::Mul(a, b) = subtree {
        if let (Expr::Val(a_v), Expr::Val(b_v)) = (a.as_ref(), b.as_ref()) {
            cmds.mut_meta(|m| m.num_applications_multiplication += 1);
            return Some(Expr::Val((a_v * b_v) % 10));
        }
    }
    None
}

#[derive(Debug)]
struct Meta {
    num_applications_addition: i32,
    num_applications_multiplication: i32,
}

pub fn criterion_benchmark(c: &mut Criterion) {
    let seed = [41; 32];
    let mut rng = StdRng::from_seed(seed);
    let mut count = 0;

    let my_expression = random_exp_tree(&mut rng, &mut count, 10);
    let rules = vec![
        rule_fns![do_nothing],
        rule_fns![rule_eval_add, rule_eval_mul, factorial_eval],
    ];

    c.bench_function("factorial", |b| {
        b.iter(|| {
            let meta = Meta {
                num_applications_addition: 0,
                num_applications_multiplication: 0,
            };
            morph(
                black_box(rules.clone()),
                select_first,
                black_box(my_expression.clone()),
                black_box(meta),
            )
        })
    });
}

criterion_group!(benches, criterion_benchmark);
criterion_main!(benches);
}

left_add/left_add_hard

The benchmarks left_add and left_add_hard are two benchmarks that evaluate a very simple nested addition expression (1+(1+(1+...))) of variable depth. In its unoptimised state, all but he final two instances of a 1 node will undergo several superfluous rule checks. The benchmark left_add_hard also is identical to left_add, except there are also four additional dummy rules, all assigned with a higher priority than the rule_eval_add. As expected, this will reduce code performance by about 400% (shown later). The code for left_add_hard is shown below, with left_add being very similar.

Filename: conjure-oxide/crates/tree_morph/benches/left_add_hard.rs

#![allow(unused)]
fn main() {
use criterion::{black_box, criterion_group, criterion_main, Criterion};
use tree_morph::prelude::*;
use uniplate::derive::Uniplate;

#[derive(Debug, Clone, PartialEq, Eq, Uniplate)]
#[uniplate()]
enum Expr {
    Add(Box<Expr>, Box<Expr>),
    Val(i32),
}

fn rule_eval_add(_: &mut Commands<Expr, Meta>, expr: &Expr, _: &Meta) -> Option<Expr> {
    match expr {
        Expr::Add(a, b) => match (a.as_ref(), b.as_ref()) {
            (Expr::Val(x), Expr::Val(y)) => Some(Expr::Val(x + y)),
            _ => None,
        },
        _ => None,
    }
}

#[derive(Clone)]
enum MyRule {
    EvalAdd,
    Fee,
    Fi,
    Fo,
    Fum,
}

impl Rule<Expr, Meta> for MyRule {
    fn apply(&self, cmd: &mut Commands<Expr, Meta>, expr: &Expr, meta: &Meta) -> Option<Expr> {
        cmd.mut_meta(|m| m.num_applications += 1); // Only applied if successful
        match self {
            MyRule::EvalAdd => rule_eval_add(cmd, expr, meta),
            MyRule::Fee => None,
            MyRule::Fi => None,
            MyRule::Fo => None,
            MyRule::Fum => None,
        }
    }
}

#[derive(Clone)]
struct Meta {
    num_applications: u32,
}

fn val(n: i32) -> Box<Expr> {
    Box::new(Expr::Val(n))
}

fn add(lhs: Box<Expr>, rhs: Box<Expr>) -> Box<Expr> {
    Box::new(Expr::Add(lhs, rhs))
}

fn nested_addition(n: i32) -> Box<Expr> {
    if n == 1 {
        val(1)
    } else {
        add(val(1), nested_addition(n - 1))
    }
}

pub fn criterion_benchmark(c: &mut Criterion) {
    let base: i32 = 2;
    let expr = *nested_addition(base.pow(5));
    let rules = vec![
        vec![MyRule::Fi],
        vec![MyRule::Fee],
        vec![MyRule::Fo],
        vec![MyRule::Fum],
        vec![MyRule::EvalAdd],
    ];

    c.bench_function("left_add_hard", |b| {
        b.iter(|| {
            let meta = Meta {
                num_applications: 0,
            };
            morph(rules.clone(), select_first, black_box(expr.clone()), meta)
        })
    });
}

criterion_group!(benches, criterion_benchmark);
criterion_main!(benches);
}

right_add

The benchmark right_add is identical to left_add, except there now we are evaluating ((...+1)+1) instead. This is designed to show the inherent left bias used in tree-morph. Performance is a little better than left_add. Due to the similarity with left_add, the code is omitted.

results

The most helpful feature that criterion produces is its automatic graphing software. Upon a run of cargo bench, criterion automatically produces html reports of all benchmarks, accessible in conjure-oxide/target/criterion. An example report is shown below. The left graph is a probability density function for the run time. It says that on average it takes 854.26 µs for identity to run at a fixed depth (in this case 2^5 was used). The right graph is a cumulative time plot. The fact that the line is almost straight indicates that the run times are all very comparable in time. The additional stats provided are all standard statistics measurements, with MAD standing for the mean absolute deviation.

identity vs modify_leafs

The probability density functions for identity and modify_leafs are shown below, both evaluated a tree depth of 2^5.

As you can see, modify_leafs takes significantly longer (2300%) than identity on average, showing how costly even simple tree transformations take. This is most likely due to the fact that tree-morph does not edit in-place, but rather constructs a new tree after applying a transformation.

factorial

The following is the probability density function for factorial, ran at a max depth of 10 and a seed of [41; 32].

As you can see, even for a relatively small max depth compute is large. Also note that factorial still has a very small amount of rule groupings, and performance would likely be orders of magnitude worse if a number of rules comparable to a conjure problem was presented. This shows a significant need for optimisations, and an improved score on factorial would indicate a lot of good progress.

left_add vs left_add_hard

A comparison between left_add and left_add_hard is a clear demonstration of how detrimental duplicate rule checks can be for performance.

Ignoring the differences between the shapes of the graphs (I am unsure why this is the case), we can immediately notice how the extra 4 dummy rules in left_add_hard lead to almost exactly a 400% increase in performance!

Further work

Benchmarks are still in an early stage, and there is lots more to do. Some ideas for future work include:

• Set up some automated infrastructure for running benchmarks automatically on GitHub
• Find out scaling laws for increasing tree depth for current benchmarks
• Set up some head to head tests between two functions
• Set up counters that can measure things like node counts, maximum tree depths and other useful information
• Benchmark individual functions (such as a rule application) in order to better understand how trees grow and shrink during transformations
• Benchmark meta applications

Overview

ProTrace is a tracing module created to trace rule applications on expressions when an Essence file is parsed and rewritten by Conjure Oxide. The purpose of the module is to visualise the rules applied on the expressions, and simplify the identification of errors for debugging. The module supports multiple output formats such as JSON or human readable, along with different verbosity levels to show only what the user would like to see.

Verbosity Level

The different verbosity levels include:

• High: All rule applications.
• Medium (default): Successful rule applications.
• Low: Only errors are shown (to be implemented).

Outputs of the trace can be saved in a JSON or text file (depending on the format of trace) when specified by the user, and if the file path is not given, the output will be stored in the location of the input Essence file by default.

The module also provides filtering functionalities for displaying specific rule or rule set applications.

Trace type

The module is capable of tracing two types of objects: rule and model. A trace can be created using capture_trace, which takes a consumer and a trace type (RuleTrace or ModelTrace).

#![allow(unused)]
fn main() {
pub fn capture_trace(consumer: &Consumer, trace: TraceType)
}

#![allow(unused)]
fn main() {
pub enum TraceType<'a> {
    RuleTrace(RuleTrace),
    ModelTrace(&'a ModelTrace),
}
}

Rule Trace

Rules are applied to a given expression to rewrite it into the syntax that Conjure understands. These rule applications can be traced by the module to show users what rules have been tried and successfully applied during parsing. A rule trace consists of:

• An initial expression
• The name of the rule being applied
• The priority of the rule being applied
• The rule set that the rule belongs to
• A transformed expression as a result of rule application
• An optional new variable created during the rule application
• An optional new constraint added to the top of the expression tree created during the rule application

#![allow(unused)]
fn main() {
pub struct RuleTrace {
    pub initial_expression: Expression,
    pub rule_name: String,
    pub rule_priority: u16,
    pub rule_set_name: String,
    pub transformed_expression: Option<Expression>,
    pub new_variables_str: Option<String>,
    pub top_level_str: Option<String>,
}
}

Model Trace

Models of the problem contain expressions along with some constraints. A model trace consists of:

• An initial model
• A rewritten model after rule application

#![allow(unused)]
fn main() {
pub struct ModelTrace {
    pub initial_model: Model,
    pub rewritten_model: Option<Model>,
}
}

Formatter

Formatters are responsible for converting trace information into a human-readable or JSON string format before it is output by a consumer.

At the core of this system is the MessageFormatter trait, which defines a common interface for all formatters. There are two built-in formatter implementations provided: HumanFormatter and JsonFormatter.

Message Formatter Trait

#![allow(unused)]
fn main() {
pub trait MessageFormatter: Any + Send + Sync {
    fn format(&self, trace: TraceType) -> String;
}
}

Human Formatter

#![allow(unused)]
fn main() {
pub struct HumanFormatter
}

The HumanFormatter implements the MessageFormatter trait by matching on TraceType and returning a formatted String. All TraceType variants implement the Display trait, which allows for easy string conversion.

Behaviour:

• Successful Rule Applications

  • A message “Successful Transformation” followed by the full formatted RuleTrace, displaying all of its fields.

• Unsuccessful Rule Applications

  • A message like “Unsuccessful Transformation” followed by a partial display showing only:

    • initial expression
    • rule name
    • rule priority
    • rule set name

  • Only shown if the VerbosityLevel is set to High.

• Model Traces

  • For ModelTrace, it simply displays the initial and rewritten model using its Display implementation.

Filtering: Before formatting, the HumanFormatter checks if a rule name filter or rule set name filter has been applied.

JSON Formatter

#![allow(unused)]
fn main() {
pub struct JsonFormatter
}

The JsonFormatter implements the MessageFormatter trait by matching on TraceType and returning a JSON-formatted String. It uses the serde_json library to serialize data into a pretty-printed JSON structure.

Behaviour:

• Rule Transformations

  • For RuleTrace, it serializes the entire RuleTrace object into a pretty-printed JSON string using serde_json::to_string_pretty.

  • Similar to HumanFormatter displays both successful and unsuccessful rule applications when the verbosity is high.

• Model Traces

  • For ModelTrace, no JSON output is generated. No need since the parsed and rewritten models are produced in JSON already.

Filtering: Before formatting, the JsonFormatter checks if a rule name filter or rule set name filter has been applied.

Consumer

The Consumer enum represents different types of endpoints that receive, format, and output TraceType data.

Consumers control where the trace data goes to and which format.

• StdoutConsumer prints out the trace to the console
• FileConsumer writes the trace data to a file in one of three ways: as human-readable text, as JSON-formatted text, or to both file types simultaneously.
• BothConsumer writes to both stdout and file(s).

#![allow(unused)]
fn main() {
pub enum Consumer {
    StdoutConsumer(StdoutConsumer),
    FileConsumer(FileConsumer),
    BothConsumer(BothConsumer),
}
}

Trace Trait

Each variant implements the Trace trait, meaning it can capture traces and send them to the appropriate destination.

#![allow(unused)]
fn main() {
pub trait Trace {
    fn capture(&self, trace: TraceType);
}
}

Stdout Consumer

A StdoutConsumer outputs the formatted trace data to standard output.

Holds:

• A reference-counted (Arc) formatter that implements the MessageFormatter trait.
  • Arc (Atomic Reference Counted pointer) allows safe shared ownership across multiple consumers.
  • Multiple Consumers might want to share the same formatter without each owning and duplicating it.
• A verbosity VerbosityLevel that can influence what gets printed.

#![allow(unused)]
fn main() {
pub struct StdoutConsumer {
    pub formatter: Arc<dyn MessageFormatter>,
    pub verbosity: VerbosityLevel,
}
}

dyn = dynamic dispatch. At runtime, it calls the correct format method for the actual formatter. When capturing a trace: It formats the trace using its assigned formatter.

File Consumer

A FileConsumer writes the formatted trace data to one or more files.

Holds:

• A reference-counted (Arc) formatter.
• A formatter type to determine whether to write in Human, JSON, or both formats.
• verbosity
• Path to the file for the JSON trace. (Optional)
• Path to the file for the human-readable trace. (Optional)
• is first flag used for managing JSON array formatting when appending traces.

#![allow(unused)]
fn main() {
pub struct FileConsumer {
    pub formatter: Arc<dyn MessageFormatter>,
    pub formatter_type: FormatterType,
    pub verbosity: VerbosityLevel,
    pub json_file_path: Option<String>, 
    pub human_file_path: Option<String>, 
    pub is_first: std::cell::Cell<bool>, 
}

}

When capturing a trace:

Based on the selected FormatterType: Human: Writes human-readable output to the human file. Json: Writes JSON output to the JSON file. Both: Writes to both files using respective formatters (HumanFormatter and JsonFormatter directly).

Both Consumer

A BothConsumersends the formatted trace data to both:

• Standard output (via an internal StdoutConsumer)
• Files (via an internal FileConsumer)

#![allow(unused)]
fn main() {
pub struct BothConsumer {
    stdout_consumer: StdoutConsumer,
    file_consumer: FileConsumer,
}

}

It combines the behaviours of StdoutConsumer and FileConsumer by calling method capture on both its fields.

Rule Filters

If users would like to only see specific rules or rule sets during rule application tracing, rule filters can be applied using the command-line argument --filter-rule-name or --filter-rule-set followed by comma-separated rule names or sets. The output will only show rules that is in the rule filters, otherwise the rule application will be completely skipped. This feature was added for the abstraction of unimportant rule applications during tracing, allowing users to only see the rules they require.

When both rule name and rule set filters are used in tandem, any rules that pass either the rule name or the rule set filter will be displayed. For example, if the rule name filter is normalise_associative_commutative and the rule set filter is Minion, any rule that has the rule name normalise_associative_commutative or is in the rule set Minion will be displayed.

Rule filters will be applied to both FileConsumer and StdoutConsumer.

Rule filters can also be hard-coded into the program or accessed using the following functions:

#![allow(unused)]
fn main() {
pub fn set_rule_filter(rule_name: Option<Vec<String>>)

pub fn get_rule_filter() -> Option<Vec<String>>

pub fn set_rule_set_filter(rule_set: Option<Vec<String>>)

pub fn get_rule_set_filter() -> Option<Vec<String>>
}

Capturing general messages (independent of the main tracing functionality set by)

This feature was motivated by the need for a unified interface that allows developers to capture messages—whether to stdout or a file—with the flexibility of a typical debug print statement, but with added control.

Default messages are always printed out and additional message types can be filtered and viewed using the command-line argument --get-info-about, followed by the desired message Kind.

For example, running --get-info-about rules will display all the enabled rule sets, individual rules, their assigned priorities, and the sets they belong to. To improve readability, output is color-coded: error messages appear in red, while all other information is shown in green.

#![allow(unused)]
fn main() {
pub enum Kind {
    Parser,
    Rules,
    Error,
    Solver,
    Model,
    Default,
}
fn display_message(message: String, file_path: Option<String>, kind: Kind)


}

Tracing in integration tests

Similar to how a Consumer is created in solve.rs for cargo run solve, a combined_consumer is manually constructed for each integration test, with its fields explicitly set rather than being derived from command-line arguments. This consumer is configured to log successful rule applications to two separate files—one in a human-readable format and the other in JSON. It is then passed to the rewrite_naive function. By establishing a uniform internal interface for tracing in both cargo run and cargo test, we were able to significantly reduce code duplication and streamline the overall tracing logic.

#![allow(unused)]
fn main() {
   let combined_consumer = create_consumer(
            "file",
            VerbosityLevel::Medium,
            "both",
            Some(format!("{path}/{essence_base}.generated-rule-trace.json")),
            Some(format!("{path}/{essence_base}.generated-rule-trace.txt")),
        );
}

The rule traces is verified using the functions read_human_rule_trace and read_json_rule_trace defined in testing.rs which compare the generated trace output to the expected one. read_json_rule_trace ignores the id fields since they can change from one run to another.

Command line arguments and flags

Enable rule tracing

-T, --tracing

Select output location for trace result: stdout or file [default: stdout]

-L, --trace-output <TRACE_OUTPUT>

Select verbosity level for trace [default: medium] [possible values: low, medium, high]

--verbosity <VERBOSITY>

Select the format of the trace output: human or json [default: human]

-F, --formatter <FORMATTER>

Optionally save traces to specific files: first for JSON, second for human format

-f, --trace-file [<JSON_TRACE> <HUMAN_TRACE>]

Filter messages by given kind [possible values: parser, rules, error, solver, model, default]

--get-info-about <KIND_FILTER>

Filter rule trace to only show given rule names (comma separated)

--filter-rule-name <RULE_NAME_FILTER>

Filter rule trace to only show given rule set names (comma separated)

--filter-rule-set <RULE_SET_FILTER>

NOTE: Once the rewrite engine API is finalized, we should possibly make a separate page for it

Expression rewriting, Rules and RuleSets

NOTE: Once the rewrite engine API is finalised, we should possibly make a separate page for it.

Overview

Conjure uses Essence, a high-level DSL for constraints modelling, and converts it into a solver-specific representation of the problem. To do that, we parse the Essence file into an AST, then use a rule engine to walk the expression tree and rewrite constraints into a format that is accepted by the solver before passing the AST to a solver adapter.

The high-level process is as follows:

1. Start with a deterministically ordered list of rules
2. For each node in the expression tree:
   • Find all rules that can be applied to it
   • If there are none, keep traversing the tree. Otherwise:
     • Take the rules with the highest priority
     • If there is only one, apply it
     • If there are multiple, use some strategy to choose a rule (the rule selection logic is separate from the rewrite engine itself). For testing, we currently just choose the first rule
3. When there are no more rules to apply, the rewrite is complete

We want the rewrite process to:

• be flexible - instead of hard coding the rules, we want an easy way to extend the list of rules and to decide which rules to use, both for ourselves and for any users who may wish to use conjure-oxide in their projects
• be deterministic (in a loose sense of the term) - for a given input, set of rules, and a given set of answers to all rule selection questions (see above), the rewriter must always produce the same output
• happen in a single step, instead of doing multiple passes over the model (like it is done in Savile Row currently)

Rules

Overview

Rules are the fundamental part of the rewrite engine. They consist of:

• A unique name
• An application function which takes an Expression and either rewrites it or errors if the rule is not applicable. (Checking applicability and applying the rule are not separated to avoid code duplication and inefficiency - their logic is the same)

We may also store other metadata in the Rule struct, for example the names of the RuleSets that it belongs to.

#![allow(unused)]
fn main() {
pub struct Rule<'a> {
    pub name: &'a str,
    pub application: fn(&Expression) -> Result<Expression, RuleApplicationError>,
    pub rule_sets: &'a [(&'a str, u8)], // (name, priority). At runtime, we add the rule to rulesets
}
}

Registering Rules

The main way to register rules is by defining their application function and decorating it with the #[register_rule()] macro. When this macro is invoked, it creates a static Rule object and adds it to a global rule registry. Rules may be registered from the conjure_oxide crate, or any downstream crate (so, users may define their own rules).

Currently, the register_rule macro has the following syntax:

#[register_rule(("<RuleSet name>", <Rule priority within the ruleset>))]

Example

#![allow(unused)]
fn main() {
use conjure_core::ast::Expression;
use conjure_core::rule::RuleApplicationError;
use conjure_rules::register_rule;

#[register_rule(("RuleSetName", 10))]
fn identity(expr: &Expression) -> Result<Expression, RuleApplicationError> {
   Ok(expr.clone())
}
}

Getting Rules from the registry

Rules may be retrieved using the following functions:

#![allow(unused)]
fn main() {
pub fn get_rule_by_name(name: &str) -> Option<&'static Rule<'static>>
}

#![allow(unused)]
fn main() {
pub fn get_rules() -> Vec<&'static Rule<'static>>
}

• get_rules() returns a vector of static references to Rule structs
• get_rule_by_name() returns a static reference to a specific rule, if it exists

Rule Sets

Rule sets group some Rules together and map them to their priorities. The rewrite function takes a set of RuleSets and uses it to resolve a final list of rules, ordered by their priority.

The RuleSet object contains the following fields:

• name The name of the rule set.
• order The order of the rule set.
• rules A map of rules to their priorities. This is evaluated lazily at runtime.
• solvers The solvers that this RuleSet applies for.
• solver_families The solver families that this RuleSet applies for.

Note

A RuleSet would apply if EITHER of the following is true:

• The target solver belongs to its list of solvers
• The target solver belongs to a family that is listed in solver_families, even if it is not explicitly named in solvers

It provides the following public methods:

• get_dependencies() -> &HashSet<&'static RuleSet> Get the dependency RuleSets of this RuleSet (evaluating them lazily if necessary)
• get_rules() -> &HashMap<&'a Rule<'a>, u8> Get a map of rules to their priorities (performing lazy evaluation - “reversing the arrows” - if necessary)

Registering Rule Sets

Like Rules, RuleSets may be registered from anywhere within the conjure_oxide crate or any downstream crate. They are registered using the register_rule_set! macro using the following syntax:

register_rule_set!("<Rule set name>", <order>, ("<name of dependency RuleSet>", ...), (<list of solver families>), (<list of solvers>));

If a bracketed list is omitted, the corresponding list would be empty. However, you must not break the order. For example:

#![allow(unused)]
fn main() {
register_rule_set!("MyRuleSet", 10) // This is legal (rule set will have no dependencies, solvers or solver families)
register_rule_set!("MyRuleSet", 10, ("DependencyRS")) // Also legal
register_rule_set!("MyRuleSet", 10, (SolverFamily::CNF)) // This is illegal because dependencies come before solver families
register_rule_set!("MyRuleSet", 10, (), (SolverFamily::CNF)) // But this is fine
}

Example

#![allow(unused)]
fn main() {
register_rule_set!("MyRuleSet", 10, ("DependencyRuleSet", "AnotherRuleSet"), (SolverFamily::CNF), (SolverName::Minion));
}

Adding Rules to RuleSets

Notice that we do not add any rules to the RuleSet when we register it. Instead, the Rule contains the names of the RuleSets that it needs to be added to.

At runtime, when we first request the rules from a RuleSet, it retrieves a list of all the rules that reference it by name from the registry, and stores static references to the rules along with their priorities.

This is done to allow us to statically initialise Rules and RuleSets in a decentralised way across multiple files and store them in a single registry. Dynamic data structures (like Vec or HashMap) cannot be initialised at this stage (Rust has no “life before main()”), so we have to initialise them lazily at runtime.

Internally, we would sometimes refer to this lazy initialisation as “reversing the arrows”.

Getting RuleSets from the registry

Similarly to Rules, RuleSets may be retrieved using the following functions:

#![allow(unused)]
fn main() {
pub fn get_rule_set_by_name(name: &str) -> Option<&'static RuleSet<'static>>
}

#![allow(unused)]
fn main() {
pub fn get_rule_sets() -> Vec<&'static RuleSet<'static>>
}

Resolving a final list of Rules

Our rewrite function takes an Expression along with a list of RuleSets to apply:

#![allow(unused)]
fn main() {
pub fn rewrite<'a>(
    expression: &Expression,
    rule_sets: &Vec<&'a RuleSet<'a>>,
) -> Result<Expression, RewriteError>
}

Before we start rewriting the AST, we must first resolve the final list of rules to apply.

This is done via the following steps:

1. Add all given RuleSets to a set of rulesets

2. Recursively look up all their dependencies by name and add them to the set as well

3. Once we have a final set of RuleSets:

   1. Construct a HashMap<&Rule, priority>). This will hold our final mapping of rules to priorities

   2. Loop over all the rules of every RuleSet

   3. If a rule is not yet present in the final HashMap, add it and its priority within the RuleSet

   4. If it is already present:

      • Compare the order of the current RuleSet and the one that the rule originally came from
      • If the new RuleSet has a higher order, update the Rule’s priority

4. Once all rules have been added to the HashMap:

   1. Take all its keys and put them in a vector
   2. Sort it by rule priority
   3. In the case that two rules have the same priority, sort them lexicographically by name

In the end, we should have a final deterministically ordered list of rules and a HashMap that maps them to their priorities. Now, we can proceed with rewriting.

Why all this weirdness?

Rule ordering

We want to always have a single deterministic ordering of Rules. This way, for a given set of rules, the select_rule strategy would always give the same result.

Think of it as a multiple choice quiz: if we want to know that the same numbers in the answer sheet actually correspond to the same set of answers, we must make sure that all students get the questions in the same order.

This is why we sort Rules by priority, and then use their name (which is guaranteed to be unique) as a tie breaker.

Normally, one would just construct a vector of Rules and use it as the final ordering, but we cannot do that, because rules are registered in a decentralised way across many files, and when we get them from the rule registry, they are not guaranteed to be in any specific order

RuleSet ordering

As part of resolving the list of rules to use, we need to take rules from multiple RuleSets and put these rules and their priorities in a HashMap. However, the RuleSets may overlap (i.e. contain the same rules but with different priorities), and we want to make sure that, for a given set of RuleSets, the final rule priorities will always be the same.

Normally, this would not be an issue - entries in the HashMap would be added and updated as needed as we loop over the RuleSets. However, since the RuleSets are stored in a decentralised registry and are not guaranteed to come in any particular order (i.e. this order may change every time we recompile the project), we need to ensure that the order in which the entries are added to the HashMap (and thus the final rule priorities) doesn’t change.

To achieve this, we use the following algorithm:

1. Loop over all given RuleSets
2. Loop over all the rules in a RuleSet
   • If the rule is not present in the HashMap, add it
   • If the rule is already there:
     • If this RuleSet has a higher order than the one that the rule came from, update its priority
     • Otherwise, don’t change anything

Note

The order of a RuleSet should not be thought of as a “priority” and does not affect the priorities of the rules in it. It only provides a consistent order of operations when resolving the final set of rules NOTE: The order of a RuleSet should not be thought of as a “priority” and does not affect the priorities of the rules in it. It only provides a consistent order of operations when resolving the final set of rules

Concrete Example: SAT Backend Pipeline

To see how rules and rulesets work in practice, let’s walk through the SAT backend transformation of a simple Essence model.

Note: The actual RuleSet names and groupings in the codebase may differ from this simplified explanation, but the general priority ordering and transformation pipeline described here is accurate.

Input Model

find x : int(1..3)
find y : int(2..5)
such that x > y

Transformation Pipeline

The SAT backend applies rules in three priority groups:

1. Integer Representation Rules (Highest Priority)

RuleSet: integer_repr

These rules convert integer variables into SATInt representations (boolean vectors):

#![allow(unused)]
fn main() {
#[register_rule(("integer_repr", 100))]
fn integer_decision_representation(expr: &Expression) -> Result<Expression, RuleApplicationError> {
    // Converts:  find x : int(1..3)
    // Into: SATInt([bool_0, bool_1, ... ])
}
}

2. Operation Transformation Rules

RuleSet: integer_operations

These rules convert operations on SATInts into boolean expressions:

#![allow(unused)]
fn main() {
#[register_rule(("integer_operations", 50))]
fn cnf_int_ineq(expr: &Expression) -> Result<Expression, RuleApplicationError> {
    // Converts: SATInt(x) > SATInt(y)
    // Into: complex boolean expression
}
}

3. Tseytin Transformation Rules (Lowest Priority)

RuleSet: boolean

These rules convert the resulting boolean expressions into Conjunctive Normal Form:

#![allow(unused)]
fn main() {
#[register_rule(("boolean", 10))]
fn tseitin_and(expr: &Expression) -> Result<Expression, RuleApplicationError> {
    // Converts: A AND B
    // Into: auxiliary variable C with clauses enforcing C <-> A AND B
}
}

Viewing the Transformations

You can see this pipeline in action using logging:

RUST_LOG=TRACE cargo run -- solve --solver sat my_problem.essence --verbose

This section had been taken from the ‘Expression rewriting, Rules and RuleSets’ page of the conjure-oxide wiki

Introductory notes on the use of “<-” in generators, and the logic behind and() and or() comprehensions. Followed by horizontal set rules. These are representation-independent rules in conjure that are used to rewrite models.

Notes:

• “<-” is called an expression projection

  • it creates a generator called GenInExpr
  • the left hand side has the type of a member of the right hand side
  • It is used to loop over elements of a set, primarily within and() and or() comprehensions
  • see Expression Projection for more information

• and() - for-all quantifier

  • essentially a series of conjunctions (a ∧ b ∧ .. ∧ z)
  • states that the body of the contained comprehension must hold for all elements specified by the generators and conditions.

• or() - existence quantifier

  • essentially a series of disjunctions (a ∨ b ∨ .. ∨ z)
  • states that the body of the contained comprehension must hold for at least one element specified by the generators and conditions.

• example combining these three concepts:

  • taken from the last section of this page (shown both before and after vertical rules are applied):

and([ or([ q5 = q4 | q5 <- A, or([ q6 = q5 | q6 <- B ]) ]) | q4 <- C ])
and([C_Occurrence[q4] -> or([A_Occurrence[q5] ∧ B_Occurrence[q5] ∧ q5 = q4 | q5 : int(0..6)]) | q4 : int(0..6)])

this translates to:

∀q4 ϵ C: ∃ q5 ϵ A∶(q5=q4) ∧ (∃ q6 ϵ B∶q6=q5 )

Horizontal Rules

Set-Comprehension-Literal

identifies set literal in model and converts to matrix literal containing the same elements of the same type as the set.

1. takes in Comprehension containing a “body” and generators or conditions “gensOrConds”
2. matches “gensOrConds” to a tuple containing the Generator “(pat,expr)”, between two generators or conditions, “gocBefore” and “gocAfter”
3. identifies generator containing pattern and expression, attempts to match expression to a set or multiset
4. stores elements of set literal in a list of relevant type “tau”
5. creates matrix literal of type “tau” containing same elements as set literal
6. returns original comprehension with same body, gocBefore, gocAfter, middle Generator with same pattern but matrix literal replaces set literal

Code:

     theRule (Comprehension body gensOrConds) = do
         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
             Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToSet, opToMSet] expr)
             Generator (GenInExpr pat@AbsPatSet{} expr) -> return (pat, matchDefs [opToSet, opToMSet] expr)
             _ -> na "rule_Comprehension_Literal"
         (TypeSet tau, elems) <- match setLiteral expr
         let outLiteral = make matrixLiteral
                             (TypeMatrix (TypeInt TagInt) tau)
                             (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength elems))])
                             elems
         return
             ( "Comprehension on set literals"
             , return $ Comprehension body
                      $  gocBefore
                      ++ [Generator (GenInExpr pat outLiteral)]
                      ++ gocAfter
             )

Example:

• set-comprehension-literal rule appears within model: “letting A be {1,5,3}, find B : set of int(0..6), such that B subsetEq A”
• here the body of the comprehension is “q3 = q2”, the gensOrConds is the single Generator “q3 <- {1,3,5}”
• the set literal expression {1,3,5} is replaced with the matrix literal [1,3,5; int(1..3)], the pattern “q3 <-” and the body are left unaffected.
• context:
  • q2 is a quantified variable in larger scope (Context #3) – using Occurrence representation here, used to iterate over elements in B
  • q3 is the quantified variable used to check that each q2 is an element from A = {1,3,5}

Picking the first option: Question 1: [q3 = q2 | q3 <- {1, 3, 5}]
                               Context #1: or([q3 = q2 | q3 <- {1, 3, 5}])
                               Context #3: and([or([q3 = q2 | q3 <- {1, 3, 5}]) | q2 : int(0..6), B_Occurrence[q2]])
     Answer 1: set-comprehension-literal: Comprehension on set literals
               [q3 = q2 | q3 <- {1, 3, 5}]
               ~~>
               [q3 = q2 | q3 <- [1, 3, 5; int(1..3)]]

Set-eq (boolean)

rule for set equality, checks if two sets are equal, i.e. they contain the same elements

1. identifies pattern: “x eq y”
2. checks that x and y are sets
3. translates equality into conjunction of two subset-equalities

• i.e. “x eq y” becomes “ “x subsetEq of y” AND “y subsetEq of x” “, using Set-subsetEq rule

Code:

     theRule p = do
         (x,y)     <- match opEq p
         TypeSet{} <- typeOf x
         TypeSet{} <- typeOf y
         return
             ( "Horizontal rule for set equality"
             , return $ make opAnd $ fromList
                 [ make opSubsetEq x y
                 , make opSubsetEq y x
                 ]
             )

Example:

Picking the first option: Question 1: A = B union C
     Answer 1: set-eq: Horizontal rule for set equality
               A = B union C ~~> A subsetEq B union C /\ B union C subsetEq A

Set-neq (boolean)

rule for set inequality

1. identifies pattern: “x != y”
2. checks that x and y are sets
3. translates inequality to existence of an element that is either in x but not in y, or that is in y but not in x

• i.e. “x != y” becomes “there exists i such that i in x and i not in y, or i in y and i not in x”

Code:

     theRule [essence| &x != &y |] = do
         TypeSet{} <- typeOf x
         TypeSet{} <- typeOf y
         return
             ( "Horizontal rule for set dis-equality"
             , do
                  (iPat, i) <- quantifiedVar
                  return [essence|
                          (exists &iPat in &x . !(&i in &y))
                          \/
                          (exists &iPat in &y . !(&i in &x))
                      |]
             )

Example:

• checking that the set A is not equal to set B
• here q4 is the quantified variable, referred to as “i” above.
• “exists” statement is translated using the existence quantifier or(), quantifying over q4 members of A.
• The expression projection “<-” creates a generator, in which the lhs has the type of a member of the rhs. This means the body of the or() comprehension must apply to at least one member (q4) of A (see Notes).

Picking the first option: Question 1: A != B union C
     Answer 1: set-neq: Horizontal rule for set dis-equality
               A != B union C
               ~~>
               or([!(q4 in B union C) | q4 <- A]) \/
               or([!(q4 in A) | q4 <- B union C])

Set-subsetEq (boolean)

rule for subsetEq, checks if one set is contained in another, they may be equal

1. identifies pattern: “x subsetEq y”
2. checks that x and y are sets
3. translates x is subsetEq of y to all elements in x are in y

• i.e. “x subsetEq y” becomes “for all i in x, i in y”

Code:

     theRule p = do
         (x,y)     <- match opSubsetEq p
         TypeSet{} <- typeOf x
         TypeSet{} <- typeOf y
         return
             ( "Horizontal rule for set subsetEq"
             , do
                  (iPat, i) <- quantifiedVar
                  return [essence| forAll &iPat in &x . &i in &y |]
             )

Example:

• here q3 is the quantified variable, referred to as “i” above.
• and() is the universal quantifier, quantifying over q3. and([q3 in B | q3 <- A]) translates to “for all q3 in A, q3 is in B”
• The expression projection “<-” creates a generator, in which the lhs has the type of a member of the rhs. This means the body of the and() comprehension must apply to all members (q3) of A. (see Notes).

Picking the first option: Question 1: A subsetEq B
     Answer 1: set-subsetEq: Horizontal rule for set subsetEq
               A subsetEq B ~~> and([q3 in B | q3 <- A])

Set-subset (boolean)

rule for subset, checks if one set is strictly contained in another, they cannot be equal

1. identifies pattern: “a subset b”
2. checks that a and b are sets
3. translates a is subset of b to a is subsetEq of b, and a is not equal to b

• i.e. “a subset b” becomes “ “a subsetEq b” AND “a neq b” “, using rules Set-subsetEq and Set-neq

Code:

     theRule [essence| &a subset &b |] = do
         TypeSet{} <- typeOf a
         TypeSet{} <- typeOf b
         return
             ( "Horizontal rule for set subset"
             , return [essence| &a subsetEq &b /\ &a != &b |]
             )
     theRule _ = na "rule_Subset"

Example:

Picking the first option: Question 1: A subset B
     Answer 1: set-subset: Horizontal rule for set subset
               A subset B ~~> A subsetEq B /\ A != B

Set-supset (boolean)

rule for superset, checks if one set strictly contains another, they cannot be equal

1. identifies pattern: “a supset b”
2. checks that a and b are sets
3. translates a is superset of b to b is subset of a, and applies subset rule.

Code:

     theRule [essence| &a supset &b |] = do
         TypeSet{} <- typeOf a
         TypeSet{} <- typeOf b
         return
             ( "Horizontal rule for set supset"
             , return [essence| &b subset &a |]
             )
     theRule _ = na "rule_Supset"

Example:

Picking the first option: Question 1: A supset B
     Answer 1: set-supset: Horizontal rule for set supset
               A supset B ~~> B subset A

Set-supsetEq (boolean)

rule for supsetEq, checks if one set contains another, they may be equal

1. identifies pattern: “x supsetEq y”
2. checks that x and y are sets
3. translates x is supsetEq of y to y is subsetEq of x, and applies subsetEq rule.

Code:

     theRule [essence| &a supsetEq &b |] = do
         TypeSet{} <- typeOf a
         TypeSet{} <- typeOf b
         return
             ( "Horizontal rule for set supsetEq"
             , return [essence| &b subsetEq &a |]
             )
     theRule _ = na "rule_SupsetEq"

Example:

Picking the first option: Question 1: A supsetEq B
     Answer 1: set-subsetEq: Horizontal rule for set supsetEq
               A supsetEq B ~~> B subsetEq A

Set-intersect (describes a new set)

rule for set intersection. defines that an element is in the intersection of two sets when it is in both sets. similar structure as comprehension literal rule, only used within generators or conditions

1. attempts to match generator to pattern and expression: pattern “quantified variable <-” and expression with a modifier operator (if present) applied to a set/multiset/relation “s”
2. attempts to match s to “x intersect y”
3. checks x is a set, multiset, function, or relation
4. replaces generator with same pattern and modifier (if present) applied to x, and adds the condition that the relevant quantified variable must be in y.

• i.e. “i <- x intersect y” becomes “i <- x, i in y”

Code:

theRule (Comprehension body gensOrConds) = do
         (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
             Generator (GenInExpr pat@(Single iPat) expr) ->
                 return (pat, iPat, matchDefs [opToSet,opToMSet,opToRelation] expr)
             _ -> na "rule_Intersect"
         (mkModifier, s)    <- match opModifier expr
         (x, y)             <- match opIntersect s
         tx                 <- typeOf x
         case tx of
             TypeSet{}      -> return ()
             TypeMSet{}     -> return ()
             TypeFunction{} -> return ()
             TypeRelation{} -> return ()
             _              -> failDoc "type incompatibility in intersect operator"
         let i = Reference iPat Nothing
         return
             ( "Horizontal rule for set intersection"
             , return $
                 Comprehension body
                     $  gocBefore
                     ++ [ Generator (GenInExpr pat (mkModifier x))
                        , Condition [essence| &i in &y |]
                        ]
                     ++ gocAfter
             )

Example:

• set-intersect rule appears within model C = A intersect B, after applying set-equals, set-subsetEq, set-in
• q4 is quantified in a former step, it is an element in C
• see Context #1, q5 is quantified by or() - existence quantifier, translates to “there exists a q5 in A intersect B such that q5 equals q4”
• translates “q5 <- A intersect B” to “q5 <- A, q5 in B”, i.e. body of or() comprehension must apply to at least one member (q5) of A, with the additional condition that q5 must be in B.

Picking the first option: Question 1: [q5 = q4 | q5 <- A intersect B]
                               Context #1: or([q5 = q4 | q5 <- A intersect B])
                               ...
     Answer 1: set-intersect: Horizontal rule for set intersection
               [q5 = q4 | q5 <- A intersect B] ~~> [q5 = q4 | q5 <- A, q5 in B]

Set-union (describes a new set)

rule for set union. defines that an element is in the union of two sets when it is in at least one of the sets. similar structure as comprehension literal rule, only used within generators or conditions

1. attempts to match generator to pattern and expression: pattern “quantified variable <-” and expression with a modifier operator (if present) applied to a set/multiset/relation “s”
2. attempts to match s to “x union y”
3. checks x is a set, multiset, function, or relation
4. creates abstract matrix containing two comprehensions:

• both comprehensions have body from original comprehension
• both comprehensions have a generator with same pattern on same quantified variable.
• expressions in generators consist of same modifier operator (if present) applied to only set x and only set y respectively
• for set y, the additional condition “i not in x” is added to prevent double counting (relevant for sums)

Code:

     theRule (Comprehension body gensOrConds) = do
         (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
             Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, matchDef opToSet expr)
             _ -> na "rule_Union"
         (mkModifier, s)    <- match opModifier expr
         (x, y)             <- match opUnion s
         tx                 <- typeOf x
         case tx of
             TypeSet{}      -> return ()
             TypeMSet{}     -> return ()
             TypeFunction{} -> return ()
             TypeRelation{} -> return ()
             _              -> failDoc "type incompatibility in union operator"
         let i = Reference iPat Nothing
         return
             ( "Horizontal rule for set union"
             , return $ make opFlatten $ AbstractLiteral $ AbsLitMatrix
                 (DomainInt TagInt [RangeBounded 1 2])
                 [ Comprehension body
                     $  gocBefore
                     ++ [ Generator (GenInExpr pat (mkModifier x)) ]
                     ++ gocAfter
                 , Comprehension body
                     $  gocBefore
                     ++ [ Generator (GenInExpr pat (mkModifier y))
                        , Condition [essence| !(&i in &x) |]
                        ]
                     ++ gocAfter
                 ]
             )

Example:

• set-union rule appears within model C = A union B, after applying set-equals, set-subsetEq, set-in
• q4 is quantified in a former step, it is an element in C (Context #3)
• see Context #1, q5 is quantified by or() - existence quantifier, translates to “there exists a q5 in A union B such that q5 equals q4”
• translates “[q5 = q4 | q5 <- A union B]” to return the matrix “flatten([[q5 = q4 | q5 <- A], [q5 = q4 | q5 <- B, !(q5 in A)]; int(1..2)])”
• “q5 = q4” is the body of the comprehension, the pattern “q5 <-” is applied to both A and B in the respective entries of the matrix
• additional condition “!(q5 in A)” for the second comprehension, to prevent double counting
  • i.e. check that the body “q5 = q4”, applies to at least one member (q5) in A or in B.

Picking the first option: Question 1: [q5 = q4 | q5 <- A union B]
                               Context #1: or([q5 = q4 | q5 <- A union B])
                               Context #3: and([or([q5 = q4 | q5 <- A union B]) | q4 : int(0..6), C_Occurrence[q4]])
     Answer 1: set-union: Horizontal rule for set union
               [q5 = q4 | q5 <- A union B]
               ~~>
               flatten([[q5 = q4 | q5 <- A], [q5 = q4 | q5 <- B, !(q5 in A)];
                            int(1..2)])

Set-difference (describes a new set)

rule for set difference. defines that an element is in the difference of two sets when it is in the former but not in the latter. similar structure as comprehension literal rule, only used within generators or conditions

1. attempts to match generator to pattern and expression: pattern “quantified variable <-” and expression with a modifier operator (if present) applied to a set/multiset/relation “s”
2. attempts to match s to “x - y”
3. checks x is a set, multiset, function, or relation
4. returns comprehension with same body as original, same gocBefore, gocAfter. Generator is replaced by original generator applied only to x, with additional condition “i not in y”

Code:

     theRule (Comprehension body gensOrConds) = do
         (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
             Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, expr)
             _ -> na "rule_Difference"
         (mkModifier, s)    <- match opModifier expr
         (x, y)             <- match opMinus s
         tx                 <- typeOf x
         case tx of
             TypeSet{}      -> return ()
             TypeMSet{}     -> return ()
             TypeFunction{} -> return ()
             TypeRelation{} -> return ()
             _              -> failDoc "type incompatibility in difference operator"
         let i = Reference iPat Nothing
         return
             ( "Horizontal rule for set difference"
             , return $
                 Comprehension body
                     $  gocBefore
                     ++ [ Generator (GenInExpr pat (mkModifier x))
                        , Condition [essence| !(&i in &y) |]
                        ]
                     ++ gocAfter
             )

Example:

• set-difference rule appears within model C = A - B, after applying set-equals, set-subsetEq, set-in
• q4 is quantified in a former step, it is an element in C (Context #3)
• see Context #1, q5 is quantified by or() - existence quantifier, translates to “there exists a q5 in A - B such that q5 equals q4”
• translates “q5 <- A - B” to “q5 <- A, !(q5 in B)”

Picking the first option: Question 1: [q5 = q4 | q5 <- A - B]
                               Context #1: or([q5 = q4 | q5 <- A - B])
                               Context #3: and([or([q5 = q4 | q5 <- A - B]) | q4 : int(0..6), C_Occurrence[q4]])
     Answer 1: set-difference: Horizontal rule for set difference
               [q5 = q4 | q5 <- A - B] ~~> [q5 = q4 | q5 <- A, !(q5 in B)]

Set-max-min (int)

rule for finding maximum and minimum of a set of integers

• contains two sub-rules, one for max, one for min.
• if set is literal, converts to list and finds max.
• otherwise creates quantified variable and uses max() operation in Essence.
• minimum rule works analogously

Code:

     theRule [essence| max(&s) |] = do
         TypeSet (TypeInt _) <- typeOf s
         return             
             ( "Horizontal rule for set max"
             , case () of
                 _ | Just (_, xs) <- match setLiteral s, length xs > 0 -> return $ make opMax $ fromList xs
                 _ -> do
                     (iPat, i) <- quantifiedVar
                     return [essence| max([&i | &iPat <- &s]) |]
             )
     theRule [essence| min(&s) |] = do
         TypeSet (TypeInt _) <- typeOf s
         return
             ( "Horizontal rule for set min"
             , case () of
                 _ | Just (_, xs) <- match setLiteral s, length xs > 0 -> return $ make opMin $ fromList xs
                 _ -> do
                     (iPat, i) <- quantifiedVar
                     return [essence| min([&i | &iPat <- &s]) |]
             )
     theRule _ = na "rule_MaxMin"

Example:

Picking the first option: Question 1: max(A)
                               Context #1: max(A) = max(B)
     Answer 1: set-max-min: Horizontal rule for set max
               max(A) ~~> max([q3 | q3 <- A])

Set-literal example:

        letting A be {5, 6, 3}
        find i: int(0..10)
        such that i = min(A)
        branching on [i]
        such that
        such that true(i)
        
Picking the first option: Question 1: min(A)
                               Context #1: i = min(A)
     Answer 1: full-evaluate: Full evaluator
               min(A) ~~> 3

Set-in (boolean)

rule for set membership, checks whether something is an element of a set

1. identifies pattern: “x in s”
2. checks s is a set
3. introduces quantified variable to go through set s and check whether any of its elements equal x

• i.e. “x in s” becomes “there exists i in s such that i = x”

Code:

     theRule p = do
         (x,s)     <- match opIn p
         TypeSet{} <- typeOf s
         -- do not apply this rule to quantified variables
         -- or else we might miss the opportunity to apply a more specific vertical rule
         if referenceToComprehensionVar s
             then na "rule_In"
             else return ()
         return
             ( "Horizontal rule for set-in."
             , do
                  (iPat, i) <- quantifiedVar
                  return [essence| exists &iPat in &s . &i = &x |]
             )

Example:

• here we are checking for membership of q4 in B union C
• q4 is a quantified variable in larger context
• q5 is the quantified variable introduced by the set-in rule.

Picking the first option: Question 1: q4 in B union C
     Answer 1: set-in: Horizontal rule for set-in.
               q4 in B union C ~~> or([q5 = q4 | q5 <- B union C])

Set-card (int)

rule for set cardinality, counts number of elements in a set

1. identifies pattern: |s|
2. checks s is a set
3. if it exists, returns the set’s domain’s size attribute
4. otherwise introduces quantified variable “iPat” to iterate through set, incrementing the sum for each new element, returns sum.

Code:

rule_Card = "set-card" `namedRule` theRule where
     theRule p = do
         s         <- match opTwoBars p
         case s of
             Domain{} -> na "rule_Card"
             _        -> return ()
         TypeSet{} <- typeOf s
         return
             ( "Horizontal rule for set cardinality."
             , do
                 mdom <- runMaybeT $ domainOf s
                 case mdom of
                     Just (DomainSet _ (SetAttr (SizeAttr_Size n)) _) -> return n
                     _ -> do
                         (iPat, _) <- quantifiedVar
                         return [essence| sum &iPat in &s . 1 |]
             )

Example:

• set-card rule appears within model |A| = |B|
• here q3 is the quantified variable called “iPat” above

Picking the first option: Question 1: |A|
                               Context #1: |A| = |B|
     Answer 1: set-card: Horizontal rule for set cardinality.
               |A| ~~> sum([1 | q3 <- A])

Vertical rules for Occurrence, which are applied once all possible horizontal rules have been applied at a given stage. Followed by an example of rewriting a model in Occurrence representation, using both horizontal and vertical rules.

• see Conjure Horizontal Set Rules for representation-independent horizontal set rules.

Vertical rules for Occurrence-representation of sets

• Occurrence representation creates a matrix that has the length of the maximum integer value contained in the sets. E.g. a set {1,5,11} will be represented by a matrix of length 11. Each entry in the matrix is a boolean, representing whether that integer is contained in the set. in the matrix for the set {1,5,11}, the first, fifth and eleventh entry will all be True, all others will be False.

Set-comprehension

Comprehension rule for Occurrence. Uses the “<-” expression projection (see Horizontal Rules - Notes).

1. identifies a comprehension consisting of a “body” followed by “generators or conditions”
2. matches the generator to an expression of the form “iPat <- s”, iPat, later called “i” is a quantified variable
3. checks that s is a set, and that it has Occurrence representation
4. retrieves matrix m representing this set, and its domain
5. returns Comprehension with same body, original generator is replaced by a generator specifying the domain of the quantified variable, followed by a condition that the i-th entry of the Occurrence matrix is true.

• i.e. it loops over the given domain and checks that element “i” is present in the set.

Code:

    theRule (Comprehension body gensOrConds) = do
        (gocBefore, (pat, iPat, s), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
            Generator (GenInExpr pat@(Single iPat) s) -> return (pat, iPat, matchDefs [opToSet,opToMSet] s)
            _ -> na "rule_Comprehension"
        TypeSet{}            <- typeOf s
        Set_Occurrence       <- representationOf s
        [m]                  <- downX1 s
        DomainMatrix index _ <- domainOf m
        let i = Reference iPat Nothing
        return
            ( "Vertical rule for set-comprehension, Occurrence representation"
            , return $
                Comprehension body
                    $  gocBefore
                    ++ [ Generator (GenDomainNoRepr pat index)
                       , Condition [essence| &m[&i] |]
                       ]
                    ++ gocAfter
            )
    theRule _ = na "rule_Comprehension"

Example:

• here the quantified variable is q3, the set is A, the domain of the matrix is int(0..6). the GenInExpr “q3 <- A” is rewritten using the domain and the Occurrence matrix.
• the larger context is an and() comprehension representing the statement “for all q3 in A: q3 in B”, where “for all q3 in A” comes from the GenInExpr (see Horizontal Rules - Notes)
• this is rewritten as “for all q3 in the domain int(0..6), for which the q3th index of A_Occurrence is true: q3 in B”

Picking the first option: Question 1: [q3 in B | q3 <- A]
                              Context #1: and([q3 in B | q3 <- A])
    Answer 1: set-comprehension{Occurrence}: Vertical rule for set-comprehension, Occurrence representation
              [q3 in B | q3 <- A]
              ~~>
              [q3 in B | q3 : int(0..6), A_Occurrence[q3]]

Set-in

Set-in rule for Occurrence representation. In Occurrence representation, an element “i” is in a set if and only if the “i-th” entry of the Occurrence matrix is true.

• This rule is not necessary, “in” can be implemented using the comprehension rule above.

1. identifies a pattern “x in s”
2. checks s is a set of type Occurrence and retrieves its Occurrence representation matrix, m.
3. returns the value of m at x.

Code:

    theRule p = do
        (x, s)         <- match opIn p
        TypeSet{}      <- typeOf s
        Set_Occurrence <- representationOf s
        [m]            <- downX1 s
        return
            ( "Vertical rule for set-in, Occurrence representation"
            , return $ make opIndexing m x
            )

Example:

• here we are checking for containment of a quantified variable q3 in a set B
• the statement “q3 in B” is replaced with the value of B_Occurrence at index q3.

Picking the first option: Question 1: q3 in B
                              Context #1: [q3 in B | q3 : int(0..6), A_Occurrence[q3]]
    Answer 1: set-in{Occurrence}: Vertical rule for set-in, Occurrence representation
              q3 in B ~~> B_Occurrence[q3]

General Example: Rewriting the generalised model “C = A intersect B”

Original Essence Model:

find A,B,C : set of int(0..6)  
such that C = A intersect B

Conjure rewriting the problem, step by step:

1. first set equals is converted to conjunction of subsetEq, applying horizontal Set-eq rule

    Answer 1: set-eq: Horizontal rule for set equality
              C = A intersect B
              ~~>
              C subsetEq A intersect B /\ A intersect B subsetEq C

2. dealing with the left hand side first, subsetEq is converted into a comprehension, applying horizontal Set-subsetEq rule. The expression projection “<-” (see Horizontal Rules - Notes) means the body of the and() comprehension must apply to all members (q4) of C

Picking the first option: Question 1: C subsetEq A intersect B
                              Context #1: [C subsetEq A intersect B, A intersect B subsetEq C; int(1..2)]
    Answer 1: set-subsetEq: Horizontal rule for set subsetEq
              C subsetEq A intersect B ~~> and([q4 in A intersect B | q4 <- C])

3. the inside of the comprehension is simplified, using the definition of the “<-” expression projection in Occurrence representation. (see previous section “Set-comprehension{Occurrence}”) “q4 <- C” is converted to: all q4 in the length of the matrix (0 to 6) for which the q4th entry in the Occurrence matrix is true.

Picking the first option: Question 1: [q4 in A intersect B | q4 <- C]
                              Context #1: and([q4 in A intersect B | q4 <- C])
                              Context #3: and([q4 in A intersect B | q4 <- C]) /\ A intersect B subsetEq C
    Answer 1: set-comprehension{Occurrence}: Vertical rule for set-comprehension, Occurrence representation
              [q4 in A intersect B | q4 <- C]
              ~~>
              [q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]] 

4. turning “q4 in A intersect B” into a comprehension, applying horizontal Set-in rule. again using the expression projection “<-”, to signify that the body of the or() comprehension must apply to at least one member (q5) of A intersect B

Picking the first option: Question 1: q4 in A intersect B
                              Context #1: [q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]]
                              Context #3: [and([q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]]), A intersect B subsetEq C; int(1..2)]
    Answer 1: set-in: Horizontal rule for set-in.
              q4 in A intersect B ~~> or([q5 = q4 | q5 <- A intersect B])

5. replacing “q5 <- A intersect B” generator with “q5 <- A, q5 in B”, applying horizontal Set-intersect rule

Picking the first option: Question 1: [q5 = q4 | q5 <- A intersect B]
                              Context #1: or([q5 = q4 | q5 <- A intersect B])
                              Context #3: and([or([q5 = q4 | q5 <- A intersect B]) | q4 : int(0..6), C_Occurrence[q4]])
                              Context #5: and([or([q5 = q4 | q5 <- A intersect B]) | q4 : int(0..6), C_Occurrence[q4]]) /\ A intersect B subsetEq C
    Answer 1: set-intersect: Horizontal rule for set intersection
              [q5 = q4 | q5 <- A intersect B] ~~> [q5 = q4 | q5 <- A, q5 in B]

6. as in step 3., “<-” is replaced with its definition in Occurrence representation. (see previous section “Set-comprehension{Occurrence}”)

Picking the first option: Question 1: [q5 = q4 | q5 <- A, q5 in B]
                              Context #1: or([q5 = q4 | q5 <- A, q5 in B])
                              Context #3: and([or([q5 = q4 | q5 <- A, q5 in B]) | q4 : int(0..6), C_Occurrence[q4]])
                              Context #5: and([or([q5 = q4 | q5 <- A, q5 in B]) | q4 : int(0..6), C_Occurrence[q4]]) /\ A intersect B subsetEq C
    Answer 1: set-comprehension{Occurrence}: Vertical rule for set-comprehension, Occurrence representation
              [q5 = q4 | q5 <- A, q5 in B]
              ~~>
              [q5 = q4 | q5 : int(0..6), A_Occurrence[q5], q5 in B]

7. “q5 in B” is replaces with vertical, Occurrence-specific rule for set-in. simply checks the boolean value of the q5th entry in the occurrence matrix.

Picking the first option: Question 1: q5 in B
                              Context #1: [q5 = q4 | q5 : int(0..6), A_Occurrence[q5], q5 in B]
                              Context #3: [or([q5 = q4 | q5 : int(0..6), A_Occurrence[q5], q5 in B]) | q4 : int(0..6), C_Occurrence[q4]]
                              Context #5: [and([or([q5 = q4 | q5 : int(0..6), A_Occurrence[q5], q5 in B]) | q4 : int(0..6), C_Occurrence[q4]]),
                                           A intersect B subsetEq C;
                                               int(1..2)]
    Answer 1: set-in{Occurrence}: Vertical rule for set-in, Occurrence representation
              q5 in B ~~> B_Occurrence[q5]

8. restructuring (“inlining conditions”) inside or and and statements in turn:

Picking the first option: Question 1: [q5 = q4 | q5 : int(0..6), A_Occurrence[q5], B_Occurrence[q5]]
                              Context #1: or([q5 = q4 | q5 : int(0..6), A_Occurrence[q5], B_Occurrence[q5]])
                              Context #3: and([or([q5 = q4 | q5 : int(0..6), A_Occurrence[q5], B_Occurrence[q5]]) | q4 : int(0..6), C_Occurrence[q4]])
                              Context #5: and([or([q5 = q4 | q5 : int(0..6), A_Occurrence[q5], B_Occurrence[q5]]) | q4 : int(0..6), C_Occurrence[q4]]) /\
                                          A intersect B subsetEq C
    Answer 1: inline-conditions: Inlining conditions, inside or
              [q5 = q4 | q5 : int(0..6), A_Occurrence[q5], B_Occurrence[q5]]
              ~~>
              [A_Occurrence[q5] /\ B_Occurrence[q5] /\ q5 = q4 | q5 : int(0..6)] 

Picking the first option: Question 1: [or([A_Occurrence[q5] /\ B_Occurrence[q5] /\ q5 = q4 | q5 : int(0..6)])
                                           | q4 : int(0..6), C_Occurrence[q4]]
                              Context #1: and([or([A_Occurrence[q5] /\ B_Occurrence[q5] /\ q5 = q4 | q5 : int(0..6)]) | q4 : int(0..6), C_Occurrence[q4]])
                              Context #3: and([or([A_Occurrence[q5] /\ B_Occurrence[q5] /\ q5 = q4 | q5 : int(0..6)]) | q4 : int(0..6), C_Occurrence[q4]]) /\
                                          A intersect B subsetEq C
    Answer 1: inline-conditions: Inlining conditions, inside and
              [or([A_Occurrence[q5] /\ B_Occurrence[q5] /\ q5 = q4
                       | q5 : int(0..6)])
                   | q4 : int(0..6), C_Occurrence[q4]]
              ~~>
              [C_Occurrence[q4] ->
               or([A_Occurrence[q5] /\ B_Occurrence[q5] /\ q5 = q4
                       | q5 : int(0..6)])
                   | q4 : int(0..6)] 

9. the process is repeated for the right hand side of the conjunction in step 1, leading to a similar but simpler expression due to the order of operations.

Final Rewritten Model:

find A_Occurrence: matrix indexed by [int(0..6)] of bool
    find B_Occurrence: matrix indexed by [int(0..6)] of bool
    find C_Occurrence: matrix indexed by [int(0..6)] of bool
    branching on [A_Occurrence, B_Occurrence, C_Occurrence]
    such that
        and([C_Occurrence[q4] -> or([A_Occurrence[q5] /\ B_Occurrence[q5] /\ q5 = q4 | q5 : int(0..6)]) | q4 : int(0..6)]),
        and([A_Occurrence[q6] /\ B_Occurrence[q6] -> C_Occurrence[q6] | q6 : int(0..6)])

Syntax Errors

(Will produce an invalid CST)

1. Missing Token (e.g variable, Domain, Expression)

Description: expected token is absent Detection: Empty node or a missing child node. (MISSING node is inserted) Example: missing variable name

find: bool

Example: missing Expression

letting x be 

2. Missing Keyword

Description: a token appears where a different token/keyword is expected Detection: ERROR node containing all the tokens where that failed to match the grammar

Example: missing colon, int is unexpected (here x and int will be children of the ERROR node)

find x int

3. Unexpected Token

Description: a token appearing after a valid construct is complete Detection: ERROR node containing the extra token (ERROR node will likely be the last child of a valid construct) Example: second ) is extra

find x: int(1..2))

4. Invalid Token

Description: token is malformed or not part of the grammar Detection: look for an ERROR node with the invalid token Example: @int is not a valid token (ERROR node with @)

find x: @int

Conjure does not identify int at all, just says “Skipped token”, “Missing Domain” Tree-Sitter in conjure-oxide sees int as a valid token but has an ERROR node with @ before. So in Conjure the same error as Missing Token but might make sense to separate due to different CST structures.

5. Unclosed Delimiter

Description: unmatched or missing closing bracket, parenthesis, brace Detection: MISSING node “)” Example: missing )

find x: int(1..2

Conjure allows it but since out grammar enforces it Tree-Sitter produces an error.

6. Unsupported Statements

Description: statement not recognised by Essence grammar Detection: ERROR node with the unrecognised statement Example:

find x: int(1..5)
print x 

Conjure doesn’t recognise print x as a separate invalid statement.

7. General Syntax Error

All the other cases that cause an ERROR node in the CST tree.

Semantic Errors

(Will produce a valid CST and AST, now can only detected at runtime, e.g type checking)

1. Keywords as Identifiers

Description: token’s name is not allowed
Detection: compare the variable names against the set of keywords Example: Keyword “bool” used as a variable name

find bool: bool

find x: letting

Conjure doesn’t allow it but Tree-Sitter does so we will have to check as part of semantic checks.

2. Omitted Declaration

Description: variable not declared Detection: save the declared variables and check if the ones used in expressions are in the declared set Example: x was not declared before

find y: int (1..4)
such that x = 5

3. Invalid Domain

Description: logically or mathematically invalid bounds/domain + infinite domain

Example: a bigger value before smaller

find x: int(10..5)

Conjure doesn’t flag as error just says no solutions found.

Example: infinite domain

find x: int(1..) 

Might want to restrict infinite domain with the grammar so it could be a syntax error.

4. Type Mismatch

Description: attempt to do an operation on illegal types

Example: cannot add integer and boolean

letting y be true 
find x: int (5..10)
such that 5 + y = 6

5. Unsafe division

Description: cannot divide/modulo by zero

Example: cannot divide by zero

find x: int(5..10)
such that x/0 = 3

Conjure allows, proceeds to run the solver but just outputs no solutions. We should disallow.

6. Invalid indexing in tuples and matrices

Description: Tuples and matrices are indexed from . Negative, zero or index out of bounds is invalid

Example: s tuple index of out bounds

letting s be tuple(0,1,1,0)
letting t be tuple(0,0,0,1)
find a : bool such that a = (s[5] = t[1]) $ true

Possible semantic errors per statement type

(All syntactic errors are relevant for each)

Declarations

Find Statement

(Declaring decision variables)

Format: “find” Name “:” Domain

Semantic Errors: Keyword as Token, Invalid Domain

Letting Statement

(Declaring aliases)

Formats: “letting” Name “be” Expression | “letting” Name “be” “domain” Domain

Semantic Errors: All except Omitted Declaration

Constraints

Format: “such that” list(Expression, “,”)

Semantic Errors: All except for Invalid Domain

Ideal Scenario of Testing for Conjure-Oxide

Introduction

What is the goal of this document?

The goal of this document is to provide an ideal testing outline for Conjure-Oxide, a project in development. To do so, this document will be split into definitions (of Conjure-Oxide and other relevant components, as well as key testing terms), current Conjure-Oxide testing, and idealised (to an extent) Conjure-Oxide testing. When discussing idealised testing, any key limitations will also be discussed. Further, this document will address the use of GitHub actions in this project, including code coverage.

What is Conjure-Oxide

Conjure-Oxide is a constraint modelling tool which is implemented in Rust. Of note, it is a reimplementation of the Conjure automated constraint modelling tool and the Savile Row Modelling Assistant, functionally merged and rewritten in Rust - largely because Rust is an efficient high-performance language. Conjure-Oxide takes in a problem written in a high level constraint language, which is called Essence, and creates a model from this. This model is then transformed into a solver-friendly form, and solved using one of the available back-ends. At the moment, these solver back-ends include Minion (a Constraint Satisfiability Problem (CSP) solver) and in-development translation and bindings to a SAT (Propositional Satisfiability Problem) solver. To put it simply, Conjure-Oxide is a compiler to different modelling languages, the result of which is passed into the respective solver. These solvers act as back-ends and must be given bindings to Conjure-Oxide, but are not actually part of it themselves.

How is the model made ‘solver-friendly’?

Conjure-Oxide has a rule engine, which applies rules onto the model passed in as Essence, to lower the level of the language into one which can be parsed and solved by the back-end solvers. This engine applies rewriting rules, such as (x = - y) to (x + y = 0), to transform the model. As Essence is a fairly high-level language, with compatibility for sets and matrices and a number of keywords, there are a lot of rewrite rules which may be needed before the model can be passed into a solver. This translation is one of the key roles of Conjure-Oxide, and this rule application refines the language from a higher level to a lower level. The exact rules applied and the degree of simplification varies on the language requirement of the solver: for example, Minion has higher-level language compatibility than a SAT solver¹.

Conjure and Savile Row

Also relevant to the testing of Conjure-Oxide is Conjure and Savile Row ². This is because as Conjure-Oxide is a merge and reimplementation of these programs, the testing can be performed comparatively against Conjure and Savile Row. When this document uses the term “Conjure suite”, it refers to both Conjure and Savile Row, being used in combination, generally using the Minion solver. Where there is deviation from this, it will be explicitly clarified.

What is Conjure?

Conjure is a constraint modelling tool, implemented in Haskell. It uses a rule engine similarly to Conjure-Oxide to simplify from Essence to Essence’ (a subset of Essence which is slightly lower-level), and this “refinement” produces the lower-level model to pass to Savile Row.

What is Savile Row?

Savile Row is a constraint modelling assistant which translates from Essence’ to a solver-friendly language. Alongside translating the model to the target language, it can reformat the model with an additional set of rules. This provides a performance increase by improving the model itself. Functionally, the better a model is, the faster a solver will solve it.

What is Minion?

Minion is a Constraint Satisfiability Problem solver, which has bindings to both Conjure suite and Conjure-Oxide. Minion is a fast, scalable, CSP solver, designed to be capable of solving difficult models while still being time optimised. This is the main solver in use by both the Conjure suite and by Conjure-Oxide, due to its flexibility and efficiency.

Definitions for Testing

Two main forms of testing will be addressed within this document: correctness testing and performance testing. Fuzz testing (inputting malformed instances to see the program response) is not currently intended as part of testing Conjure-Oxide, and so will not be outlined or addressed. Metamorphic testing may have applications to this project, and so will be defined, but will not be considered as part of the ideal implementation at present as it is not possible to implement at this point in time.

What is correctness testing?

In the field of computer science, correctness can be formally defined as a program which behaves as expected by it’s formal specification, in all cases. As such, testing for correctness essentially consists of testing that the program produced the correct result for all given test cases. Correctness testing does not require exhaustiveness (checking all inputs on all states), but instead requires testing that all (or most) states function with varied inputs, which can then be used as a proof of correctness.

What is performance testing?

Performance testing refers to a range of methodologies designed to measure or evaluate a software’s performance. By performance, this generally refers to time taken to complete a process and the stability under load. The time taken for processes will vary not only by system, but also by device depending on factors such as background processes. As not all performance testing methodologies are relevant to Conjure-Oxide, they will not be outlined in this document. The two most common forms of performance testing are load testing and stress testing. Load testing examines the performance of a program to support its expected usage, and is used to identify bottlenecks in software, as well as possibly identify a relationship of usage to time. Stress testing places the program under extremely high load to see the ability of the software to function under exceptional load. This is generally used to find the functional upper load of a program before it breaks.

What is metamorphic testing?

Most tests use oracles, where the answer is known and is explicitly checked against. This is what is done in correctness testing, as laid out above. Metamorphic testing, instead, uses Metamorphic relations to generate new test cases from existing previous ones. A metamorphic relation is the relation between the test (the inputs) and the result (the outputs). An example of this is (sin(x) = sin( \pi -x)), where, regardless of x, there is a consistent relation between the input and output. As such, test cases can be generated to test the correctness of this output.

Test Scenario for Conjure-Oxide

As Conjure-Oxide is a reimplementation, it is possible to perform a large amount of the testing comparatively. By this, it means that testing can be done independently on Conjure-Oxide, and the results can be directly compared against the results of the same test being ran in the Conjure suite. This is true not only for the correctness testing, but also for the performance testing. Tests run in the Conjure suite are run by Conjure, which uses Savile Row and the required solvers to produce the correct output.

Correctness Testing

There are several areas which should be tested for correctness in Conjure-Oxide: that the Essence is correctly parsed; that the correct Essence translation is generated; that the correct rules are applied in the correct order; and finally that the correct solution is reached by Minion. For something to be ‘correct’ in Conjure-Oxide, it means it must behave as expected. As Conjure-Oxide reimplements Conjure and Savile Row, the expected behaviour is that of the Conjure suite. As such, correctness testing is performed exclusively comparative to the results produced by this suite. Correctness testing as implemented is looking to ensure that all expected files match the files which are actually produced. Where there is a difference, the initial assumption is that Conjure-Oxide has the mistake. This is not necessarily always correct - the Conjure suite may have bugs or areas where it is not producing the expected outcome - but usually is.

Current Correctness Testing

Correctness testing is the main form of testing performed in Conjure-Oxide at present, mainly through integration testing. Integration testing tests how the whole application works together as a whole, and as such is the most applicable to test all areas of testing needing to be done in Conjure-Oxide. In the current testing implementation, a test model is produced, and then the parse, rule-based transformation and result file are compared against those produced by calling the same test case on Conjure. In this, we assume that the result produced by the Conjure suite is always going to be correct. Theoretically, this is completely functional - as Conjure-Oxide is a reimplementation, any bugs which exist in Conjure or Savile Row could also exist in Conjure-Oxide without causing Conjure-Oxide to violate it’s correctness. However, this defeats the point of an evolving project, so assuming the complete correctness of the Conjure suite is not sufficient for testing.

Comparative Correctness Testing

As it is possible to perform the testing comparatively, the current implementation forms a functional basis for any ideal implementation, because it is built on this comparison. The current implementation functions well (although with limitations, as addressed below) in showing a degree of correctness, however it is not necessarily holistic enough to show the full correctness of the project. The primary solution for this issue is simply increasing the test coverage through developing a broader repository of models to be tested. Conjure has a very broad set of translation rules, meaning that there is a large number of rules which can be reimplemented in Conjure-Oxide. This enables a demonstration of the functionality of Conjure-Oxide in more scenarios, by ensuring not only are all rules tested individually, but rules in combination, with specific priority, are also tested and return results as expected. There may be some benefit to having tests that are not solved and compared against results from the Conjure suite, but rather solved independently (e.g., by mathematicians) and then compared to the results of the same model produced by Conjure-Oxide. By proving these results as correct, it is possible to go beyond simply assuming Conjure and Savile Row are always right. However, this is not particularly feasible in a broader implementation and would be fairly limited in scale due to this, especially as Conjure-Oxide is not a large project. Solver Testing Part of the larger Conjure-Oxide project is the implementation of a Satisfiability (SAT) solver. This implementation will require integration testing alongside the rest of the Conjure-Oxide project. As Conjure has a SAT solver, this is possible to be done comparatively, although would require the implementation of the ability to select a specific solver to solve a model. The comparative testing would simply compare the translated essence to SAT, and the output of the Conjure suite’s SAT solver to that of the Conjure-Oxide SAT solver, and debug where the tests do not pass.

Limitations of Correctness Testing

Conjure-Oxide is, in part, a refinement based program. A large part of it’s function is to refine from Essence down to a solver-friendly language. One part of the way that this is done in Conjure-Oxide is through a rule engine. This rule engine applies modifications to the constraints problems given to the project. At current, we just assume the rules applied are true. For example, (x = -y + z) becoming (x + y - z = 0) is a simple transformation which could be made by the rule engine. We do not formally prove that this transformation is correct, we just assume that it is the correct transformation. In simpler transformations such as this one, that is a valid assumption - it is possible to confirm that the modification is correct with minimal effort. In cases where more complex rules may be applied, the lack of a proof poses a limitation on the project. In an ideal scenario, this limitation could be removed by having proofs for every single rule applied in the rule engine, therefore not having to rely on an assumed correctness. Another of the primary limitations in correctness testing as implemented is that it assumes that the output being produced by Minion (or the SAT solver in development) is correct. As there are no known bugs in Minion, this is an acceptable assumption to make. That said, it is not necessarily accurate that all output from Minion is correct. Other mature (having existed, and been used and updated, over a protracted period of time), state of the art solvers can produce incorrect results³.

If Minion has similar unknown bugs, it may fail to fulfil the correctness element of correctness testing. The SAT solver which is being implemented is in it’s infancy and as such is much less reliable. It is likely that it will have a number of bugs and logical errors which will be gradually harder to find as time goes on (operating under the assumption that easy-to find and solve bugs will be removed earlier, leaving only more hidden or complex bugs).

Performance Testing

It is of note that a large motivation behind the reimplementation of the Conjure suite into a single Rust program is to improve the performance of the compilation from Essence to a solver-friendly language, without compromising on the time taken to solve a model. Currently, Conjure translates Essence into Essence’, and then Savile Row refines and reformats the resultant Essence’ into a solver-friendly language. Conjure-Oxide translates directly from Essence into a solver-friendly language, which should cut down on the amount of steps necessary and as such result in a shorter translation time. When testing for overall performance of Conjure-Oxide, the primary metrics that we are are concerned with is the total time taken for a model to be parsed, translated, and solved through the solver back-end. This total time can be split into two components: the translation time and the time taken by the solver. We can also use solver nodes as a measure of performance of the solver, as the time the solver takes may vary depending on background processes. In the performance testing addressed in this document, though there will be consideration for the solver time, the primary measurement of value is translation time.

Current Performance Testing

At present, there is no formal performance testing implemented in Conjure-Oxide. While stats files are generated on each test run, tracking a number of fields (rewrite time, solver time, solver nodes, total time, etc.), nothing is done with this information. As such, while there is some measure of ‘performance’, it lacks context, is not reliable (since data is produced from a single run) and overall does not create a measure of Conjure-Oxide’s performance. Performance testing, both load and stress based, can be performed both comparatively (as in checking speed or efficiency of one program directly against another (or several other) programs), but also individually on the given program. As such, both ‘methods’ of Performance testing will be discussed.

Performance Testing of just Conjure-Oxide

Sole examination of the performance of Conjure-Oxide cannot show whether there is a performance improvement as desired. However, the goal of individual performance testing is rather to enable the development of a relationship between complexity (of translation) and time (to translate). In addition, this will allow for the identification of any notable bottlenecks in the program, allowing these specific problem areas to be targeted for improvement. To performance test a program, a number of things need to be established. Firstly, what the metric(s) are being considered - as established above, for Conjure-Oxide this is the translation-, and to some degree solver-, time. Secondly, what is the independent variable - as in, what is being varied to result in different outputs. In Conjure-Oxide, this will be size or complexity of a given Essence file. Size and complexity will be defined contextually below.

Distinction between Size and Complexity

Size and complexity of a given Essence file are separate, although certainly correlated. Put simply, size refers more directly to the number of components that make up an Essence input problem, whereas complexity refers to specific aspects which complicate translation, rather than directly increase its size. When applying rules to a model, the rules are applied by priority. The implementation of this is essentially that each rule is checked against the model, and if it applies, it is applied to transform the model in order of priority (e.g., two rules are valid, the higher priority rule is the one selected). Use of a dirty-clean (this will not try to apply rules to a finished model) or naive (this will try and apply all rules until they have all been checked, applied, checked again, etc.) rewriter will also result in variance on translation time, so when experiments are being defined it is best to account that all models are using the same version of the rewriter. Size refers to the number of variables, constraints, or size of input data (for example, a larger set or array) given as part of an input file. A ‘larger’ problem has more constraints and variables than a ‘smaller’ one. This will impact translation time (the relationship of this change should be examined by the performance testing) because there is more to parse and translate, even if the actual rule application is simple. On the other hand, in this context, complexity can be loosely defined as elements of the model which make it difficult to translate, without regard for the size. Features which could increase complexity include nesting, conditional constraints, dynamic constraints, etc. When testing for size, it is best to use very simple, repeated rules, and when testing complexity it is best to try to ensure that this is not also linked into increasing size, although these two features are tied together and therefore difficult to isolate from one another.

Performance Experiments to run

There are two main types of experiment to be considered in the performance testing of Conjure-Oxide. \textbf{Load testing}, where the size or complexity is varied in order to measure translation time under different conditions; and \textbf{stress testing}, specifically to see whether higher complexity or larger files disproportionately increase translation time. As stress testing requires some measure of what is proportional and what is not, load testing is addressed first.

Load testing for Conjure-Oxide

When designing performance testing for a system, there are several considerations to be made. Primarily, it is of importance that data gathered and aggregated is suitable to be used for graphing and building relationships. To do this, data must be reliable, consistent and accurate. Single runs of data cannot provide this, as many factors may influence the results. In order to fulfil these needs, substantial amounts of data should be gathered. Anomalies should be removed (for example, using interquartile range or using Z-Scores) or simply averaged over (this is less accurate but more achievable). As size or complexity varies, these averaged results should be plotted into a graph. This is the most effective way of providing understanding of the relationship between size/complexity and translation time.

Stress testing for Conjure-Oxide

Once a relationship has been established by load testing, stress testing can occur. Although it is possible to see the point at which a program fails without prior load testing, having determined the relationship between size/complexity and time allows for a consideration of what is disproportionate. Implementing this in Conjure-Oxide would simply involve the program under abnormally high load to find it’s breaking point, using repeated results to ensure reliability and accuracy of the data.

Additional Performance Profiling

Many parts of Conjure-Oxide (such as specific rules, string manipulations, memory allocation to solvers, etc.) are also not capable of being directly examined for their complexity, and the complexity of these things cannot be manipulated to perform experiments as outlined above. However, it is important that these are still being tested for their performance. This is because it is important to catch irregular memory allowances, excessive time spending, expensive Rust functions, etc., in order to ensure that Conjure-Oxide runs both as quickly and as smoothly as possible, One way to do this is to run profilers, such as Perf, which allow for the areas that time or memory is being spent to be analysed more specifically. Given this analysis, it is then possible to examine these areas for improvements, as was done in Issue #288⁴.

Comparative Performance Testing

As established, Conjure-Oxide is a reimplementation of a pre-existing set of programs, these being Conjure and Savile Row. One of the primary goals of this reimplementation is to improve the performance of Translation time, while also ensuring that the time taken to solve a given essence problem is not worsened. Considering that Minion is simply rebound to Conjure-Oxide, much as it was in the Conjure suite, it is unlikely that these bindings would be responsible for a slower solve time. As such, the primary impact on solve time is the model passed into the solver. A worse model will take substantially more time than a model which has been well translated and refined, and substantial increases in the time taken to solve should be avoided. Performance testing should be performed on the Conjure suite (primarily on Savile Row, since the time of Conjure is amortised over each instance) to establish the relationship of size/complexity to time, as in Conjure-Oxide. The results of both may then be plotted on one graph, to see at which point(s) Conjure-Oxide is faster than Savile Row at translation, and vice versa. Comparative testing also allows for the solver nodes (which represent, to some degree, solver time) from both the Conjure suite and Conjure-Oxide. As established, the goal of Conjure-Oxide is to improve translation performance without sacrificing solving performance. As such, it is vital to also consider at which size/complexity of translation the solver nodes start to vastly differ between Conjure suite and Conjure-Oxide, and to examine the rules to see why this is (and whether there is a requisite decrease in translation time which could possibly balance this increase). Though having a small number of nodes which differ (e.g., by 10) is not an issue, when there is a large disparity between number of solver nodes, this reflects poorer quality translation or (possibly) an issue with the binding to Rust.

Limitations of Performance Testing

One limitation of performance testing is the impact that other processes running on the computer or server when testing. Other processes running at the same time mean that less threads can be allocated to Conjure-Oxide or its solver backends when dealing with a model, and as such slow down the speed at which these models can be parsed, translated, and solved. However, this is mainly removed as an issue by a combination of repeated runs, and identifying and removing anomalies (using Z-Score). Another issue present in performance testing is that completely decoupling size and complexity is rather difficult, if not entirely impossible. This is because there is overlap in the definitions, and because as a model becomes more complex, it often becomes larger, and vice versa. Although fully separating these two metrics is the aim in an ideal scenario, an actual implementation would struggle to follow through with this requirement.

GitHub Actions and Testing

GitHub Actions allow for integration of the CI’/CD pipeline to GitHub and the automation of the software development cycle. Automated workflows can be used to build, test and deploy code into a GitHub VM, allowing for flexibility in the development of a project.

What is a workflow?

In GitHub Actions, a workflow is an automated process which is set up within a GitHub repository with the aim to accomplish a specific task. They are triggered by an Event, such as pushing or pulling code. Workflows are made up of the combination of a trigger (the Event) and a set of processes (made up of Jobs, which are sets of steps in a workflow).

Test Rerun

This involves the automated rerunning of tests when a push or pull request is made on the GitHub repository. This is already implemented in Conjure-Oxide, through “test.yml”. Test.yml runs tests every push request made to the main branch, and on all pull requests. This allows for correctness testing to be performed on all pushes made to the main, to ensure that no additional tests fail.

Code Coverage

When pushes are made to the main branch of Conjure-Oxide on GitHub, a code coverage automated workflow is run. This workflow generates a documentation coverage report which outlines what percentage of the code in the repository is being executed when tests are run. The higher the percentage, the more of the code can be relied upon as working under test conditions. This is also already implemented in the GitHub repository, through “code-coverage.yml”, “code-coverage-main.yml” and “code-coverage-deploy.yml”. One of the goals of correctness testing is to increase the code coverage percentage, because this would show that more of the code is functioning correctly.

Automated Performance Testing

GitHub workflows can be used to create further custom processed to be automated. Automating performance testing in GitHub allows for them to be run routinely (e.g., every X pushes, or every X days) to ensure consistent performance of the project. As they occur automatically, this means that benchmarks can be set, and failure on any of these benchmarks can result in a flag, allowing for early detection when performance of the program begins to regress, or fall far behind that of the Conjure suite. GitHub Actions allow for the results to be placed into files, and from here an interactive dashboard could be generated (as in PR #291. ⁵

Brief Outline of Possible Future Sub-Projects

Having outlined at least a portion of the ideal testing scenario above, as well as some limitations of this scenario, it is now possible to outline to some degree future sub-projects which could be added to the overall Conjure-Oxide project.

Improving Code Coverage

One method of improving the code coverage is by creating a broader repository of integration tests. This project focuses on the correctness aspect of the testing, and in itself can be split into several sub-projects or subsumed into other projects (e.g., if someone is writing a parser, they may decide to write the tests for this parser). The code coverage report is updated every-time a PR is made, and by examining the coverage report (see: {Code Coverage Report}), it is possible to see which areas would benefit from additional testing. Although code coverage testing itself is not concerned with correctness, increasing the amount of correctness testing increases code coverage, and so they are related. It may be beneficial to target areas of the code which have a very low line or function coverage, as this is likely easier to increase.

Producing Proofs for Correctness

As established, one of the limitations of the current correctness testing is that there is an assumption of correctness, that being that we either assume the Conjure suite is correct, or we assume that the rules we are applying are correct. These assumptions are largely valid, but do limit the factual correctness of the project. One possible sub-project, which would have a heavy reliance on mathematical knowledge, is to produce these proofs. This does not necessarily have to be exhaustive: in the case of the correctness testing exhausting the proofs would be extremely time consuming, but having proofs to additionally prove correctness overcomes one of the project limitations. In the case of proving the existing rules, though there are a currently increasing set of rules, they are finite, so this may be more manageable as a project.

Measuring Performance Through Load Testing

The outline of this subproject is to fulfil, at least in part, the requirement for performance testing on this project. There are several ways that this could be approached, all of which vary somewhat, so this project is flexible in its details. One method which may be effective regarding performance testing is to use GitHub Actions to automate the performance testing, as outlined in GitHub Actions and Testing. This is because this would allow flexibility and repeated performance testing, as well as the ability to flag early on when there is a performance decrease. To outline this, it would be necessary to make a directory of tests to be run for their performance, and then create the GitHub workflow to repeatedly run tests on that directory and aggregate the translation time. This can then be plotted graphically and statistically analysed.

Comparative Load Testing

This is an extension of the above project, in that it cannot be created until there is a basis of load performance testing. The essential outline of this project is to repeat the above, except aggregating the data from the results of Savile Row’s rewriter, and then graph both Conjure-Oxide and Conjure suite together. This will allow for a direct visual comparison, as well as help with statistical analysis. Furthermore, if GitHub Actions are used, it is possible to flag where there is a large degree of difference in rewriter or solver between Conjure suite and Conjure-Oxide.

Benchmark Testing for Performance

Another sub-project which is possible to derive from this document is to benchmark test elements of the project which cannot be done by varied-load testing, as outlined in the Performance Testing section. Tools, such as Perf, can measure benchmarks and find specific problem areas. When problem areas have been found, these can be raised as an issue, and either fixed as part of this sub-project, or given to another member of the project to complete. This kind of benchmark testing will ensure that the entirety of the Conjure-Oxide is running as efficiently as possible.

Possible Stress Testing

There is also the possibility of adding stress testing to see at which point the rewrite engine fails to be able to parse through an extremely long or especially complex model. This can be done following much the same outline as that of \textit{Measuring Performance Through Load Testing}, however rather than gradually changing the load (dictated by size or complexity) on the system, the change is rapid, in order to find the system’s point of failure. As with load testing, this may also be automated by GitHub Actions, though this is a lower priority, as the failure point is less likely to change than the overall system performance.

Conclusion

This document outlines definitions relevant for understanding both the project and the types of testing most applicable. A scenario of testing is then produced, which outlines what testing exists and what testing can be added, as well as any large limitations on an implementation of this ideal state. This allows for any individuals working on testing in the future to have a holistic overview of the state of testing on this project. Finally, a number of smaller sub-projects are outlined as a product of this document, aiming to improve the tested-ness of Conjure-Oxide and compare its success as a reimplementation to Conjure and Savile Row. In the future, it may also be worth examining the possibility and likelihood of being able to apply Metamorphic testing to Conjure-Oxide, to ensure consistency in it’s results by developing metamorphic relations between input and output. At present, this is not feasible, and although this document is idealised, it is not intended to be entirely unreasonable or detached from the current reality of the project.

This section had been taken from the ‘Ideal Scenario of Testing (Dec 2024)’ page of the conjure-oxide wiki

1. Ian P. Gent, Chris Jefferson, and Ian Miguel. 2006. MINION: A Fast, Scalable, Constraint Solver. In Proceedings of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 – September 1, 2006, Riva del Garda, Italy. IOS Press, NLD, 98–102. ↩

2. Hussain, B. S. 2017. Model Selection and Testing for an Automated Constraint Modelling Toolchain; Thesis ↩

3. {Berg, J., Bogaerts, B., Nordström, J., Oertel, A., & Vandesande, D. 2023. Certified Core-Guided MaxSAT Solving. \textit{Lecture Notes in Computer Science}, 1–22. https://doi.org/10.1007/978-3-031-38499-8_1 ↩

4. conjure-cp. 2024, April 3. Possible optimisation: Intern the UserName in Name · Issue #288 · conjure-cp/conjure-oxide. \textit{GitHub}. https://github.com/conjure-cp/conjure-oxide/issues/288 ↩

5. conjure-cp. 2024, April 3. Benchmark Visualizer: Conjure Native vs Oxide · Pull Request #291 · conjure-cp/conjure-oxide. GitHub. https://github.com/conjure-cp/conjure-oxide/pull/291 ↩

Overview

Custom tests were created as a solution to the problem that integration tests do not allow for testing of error messages, which automatically return from the integration test method and therefore cannot be analyzed. The custom tests, however, work for both erroneous and non-erroneous code. Each test contains an input, a run.sh file to execute the test, and an expected standard output/error (or both) to compare against. Conjure Oxide is set up to automatically create and execute a test for each test folder in the tests/custom directory when cargo test is ran so to add a test case, all one must do is add a folder in the directory which contains the necessary components.

How to add a test case

Adding a test case is simple. First add a folder with the test case name to the tests/custom directory. Tests can be organized within folders in the directory–only folders with a run.sh file will be treated as a test case. Within the test folder, add these components:

1. run.sh file: This will typically be in the format conjure_oxide <options> <command> with the command being solve model.eprime (assuming the input file is named model.eprime). The conjure_oxide executable path is added to the PATH environment variable, so the script can invoke conjure_oxide as a command (i.e., just by name, without the full path).

   ex) conjure_oxide --solver Minion --enable-native-parser solve model.eprime

2. input file: This file will be the Essence code that is inputted into Conjure Oxide. It can be named anything but be sure to reference it correctly in the run.sh file.

   ex) find x : bool

3. stdout.expected/stderr.expected: These files will be what the output is compared against. They will also be what is overwritten if the test is run with ACCEPT=true. Avoid creating empty files: if there is no expected error from the input, do not create a stderr.expected file and if there is no output, do not create a stdout.expected file.

The custom tests are run automatically when cargo test is run. You can run just the custom tests with cargo test custom and a specific test with cargo test custom_<test_path>. To overwrite the expected output/error with the actual output/error, run the tests with ACCEPT=true.

Code structure

The code to run the custom tests is integrated into the build.rs file. Much like for the integration tests, the custom tests directory is traversed and a test is dynamically written at compile time for any folder containing a run.sh file. Tests are based on a custom test template (shown below) which calls the custom_test function (passing in the test folder path). They are written into a generated file, which is included at the bottom of the custom_tests.rs file (which contains the custom_test function).

#[test]
fn {test_name}() -> Result<(), Box<dyn Error>> {{
    custom_test("{test_dir}")
}}

The custom_test function takes the test directory as a parameter. It adds the conjure_oxide executable to the PATH environment variable and runs the commands from the run.sh file, saving the produced output. It then overwrites the expected output and error if accept was set to true and compares the actual and expected outputs/errors if not. If either does not match, the expected and actual output are printed and the test fails. Otherwise, the test passes.

Introduction

Comments and discussion about this document can be found in issue #261.

In #180 and #259 we implemented the basic Uniplate interface and a derive macro to automatically implement it for enum types. However, our current implementation is incorrect and problematic: we have defined children wrong; and our children list does not preserve structure, making more complex nested structures hard to recreate in the context function.

Recap: Uniplates and Biplates

A quick recap of what we are trying to do - for details, see the Uniplate Haskell docs, our Github Issues, and the paper.

Uniplates are an easy way to perform recursion over complex recursive data types.

It is typically used with enums containing multiple variants, many of which may be different types.

data T = A T [Integer]
       | B T T
       | C T U
       | D [T]

With Uniplate, one can perform a map over this with very little or no boilerplate.

This is implemented with a single function uniplate that returns a list of children of the current object and a context function to rebuild the object from a list of children.

Biplates provide recursion over instances of type T within some other type U. They are implemented with a single function biplate of similar type to uniplate (returning children and a context function).

These functions are able to be implemented on any data type through macros making Uniplate operations boilerplate free.

Definition of Children

We currently take children of T to mean direct descendants of T inside T. However, the correct definition of children is maximal substructures of type T.

For example, consider these Haskell types:

data T = A T [Integer]
       | B T T
       | C T U
       | D [T]

data U = E T T
       | F Integer
       | G [T] T

Our current implementation would define children as the following:

children (A t1 _) = [t1]
children (B t1 t2) = [t1, t2]
children (C t1 u) = [t1]
children (D ts) = ts

However, the proper definition should support transitive children - i.e. T contains a U which contains a T:

children (A t1 _) = [t1]
children (B t1 t2) = [t1, t2]
children (C t1 (E t2 t3)) = [t1,t2,t3]
children (C t1 (F _)) = [t1]
children (C t1 (G ts t3)) = [t1] ++ ts ++ [t3]
children (D ts) = ts

While a seemingly small difference, this complicates how we reconstruct a node from its children: we now need to create a context that takes a list of children and creates an arbitrarily deeply nested data structure containing multiple different types. In particular, the challenge is keeping track of which elements of the children list go into which fields of the enum we are creating.

We already had this problem dealing with children from lists, but a more general approach is needed.

Storing The Structure of Children

How do we know which children go into which fields of the enum variant?

For example, consider this complicated instance of T:

data T = A T [Integer]
       | B T T
       | C T U 
       | D [T]

data U = E T T
       | F Integer
       | G [T] T

myT = C(D([t0,...,t5]),G([t6,...,t12],t13))

Its list of children is: [t0,...,t13].

Try creating a function to recreate myT based on a new list of children. Hint: it is difficult, and even more so in full generality!

If we instead consider children to be a tree, where each field in the original enum variant is its own branch, we get:

data Tree A = Zero | One A | Many [(Tree A)]

myTChildren = 
  Many [(Many [One(t0),...,One(t5)]),      -- C([XXX], _) field 1 of C
        (Many [                            -- C([_],XXX)  field 2 of C
          (Many [One(t6),...,One(t12)]),   -- G([XXX],_)  field 2.1 of C
          (One  t13))]                     -- G([_],XXX)) field 2.2 of C

This captures, in a type-independent way, the following structural information:

1. myT has two fields.
2. The first field is a container of Ts.
3. The second field contains two inner fields: one is a container of Ts, one is a single T.

Representing non-recursive and primitive types

Often primitive and non-recursive types are found in the middle of enum variants. How do we say “we don’t care about this field, it does not contain a T” with our Tree type? Zero can be used for this.

For example:

data V = V1 V Integer W
       | V2 Integer

data W = W1 V V

myV = (V1 
        (V2 1) 
        1 
        (W1 
          (V2 2) 
          (V2 3)))

myVChildren = 
  (Many [
    (One v1),  -- V1(XXX,_,_)
    Zero,      -- V1(_,XXX,_) 
    (Many [    -- V1(_,_,XXX)
      (One v2),
      (One v3)
   ]))

This additionally encodes the information that the second field of myV has no Ts at all.

While this information isn’t too useful for finding or traversing over the target type, it means that the tree structure defines the structure of the target type completely: there are always the same number of tree branches as there are fields in the enum variant.

Uniplates and Biplates Using Structure Preserving Trees

Recall that the uniplate function returns all children of a data structure alongside a context function that rebuilds the data structure using some new children.

To implement this, for each field in an enum variant, we need to ask the questions: “how do we get the type Ts in the type U”, and how can we rebuild this U based on some new children of type T?.

This is just a Biplate<U,T>, which gives us the type T children within a type U as well as a context function to reconstruct the U from the T.

Therefore:

• We build the children tree by combining the children trees of all fields of the enum (such that each field’s children is a branch on the tree).

• We build the context function by calling each fields context function on each branch of the input tree.

This is effectively a recursive invocation of Biplate.

What happens when we reach a T? Under the normal definition, Biplate<T,T> would return its children. This is wrong - we want to return T here, not its children!

When T == U we need to change the definition of a Biplate: Biplate<T,T> operates over the input structure, not its children.

For our example AST:

data T = A T [Integer]
       | B T T
       | C T U 
       | D [T]

data U = E T T
       | F Integer
       | G [T] T

Here are some Biplate and Uniplates and their resultant children trees:

• Biplate<Integer,T> 1 is Zero.

• Uniplate<T> (A t [1,2,3]) is (Many [Biplate<T,T> t ,Zero]).

  This evaluates to (Many [(One t),Zero])

• Biplate<T,T> t is One t.

• Biplate<T,U> (G ts t1) is (Many [Biplate<T,[T]> ts , Biplate<T,T> t ]).

  This evaluates to (Many [(Many [(One t0),...(One tn)]),(One t)])

• Uniplate<T,T> (C t (G ts t1)) is (Many [Biplate<T,T> t, Biplate<U,T> (G ts t1))

  This evaluates to (Many [(One t), (Many [(Many [(One t0),...,(One tn)]), (One t)]))

SAT Encoding Types

Types of SAT Encodings

There are three different types of SAT Encodings planned in conjure oxide. Of these, only Logarithmic Encodings have been implemented thus far. The three types are these:

• Direct Encodings
• Logarithmic Encodings
• Order Encodings

Each type of encoding has pros and cons, and a different one may be selected based on the type of constraint problem.

SATInt Expression

All encodings are stored using the same SATInt expression type. This expression type holds: an enum specifying the encoding, a bitvector of boolean expressions (these can be literals, variables, or complex operations), and the domain of the integer. This expression cannot be created through parsing and should only be created by SAT rules.

Logarithmic Encoding

The base principle is quite simple: encode an integer as a bitvector. This allows us to represent integers as a series of boolean constraints – one for each bit.

For example, the integer ‘6’ can be represented in binary as ‘0110’. We can then represent this as (P = 0 ∨ 1, Q = 0 ∨ 1, R = 0 ∨ 1, S = 0 ∨ 1). The connection that is missing, however, is that this isn’t actually a representation of a constraint problem, but of a solution to a problem.

Direct Encoding

Direct encodings are the most straightforward type of encoding - it involves creating a vector of boolean variables, one corresponding to each member of the domain. Only one of these variables can be true at a time, and it is the one corresponding to the value of the integer.

Order Encoding

Order follows the same principle as direct encoding, but instead of each boolean variable ‘specifying’ a value in the way that direct encodings do, each bit specifies whether the integer corresponding to it is less than or equal to the integer variable’s value.

Why have multiple types of encoding?

Only logarithmic encodings are currently implemented in conjure-oxide. We’re planning to include other encodings such as direct and order encodings. This is motivated by their potential advantages over the log encoding in some cases.

Direct encodings should perform well for equality-heavy constraints but may scale poorly with larger domains or inequalities. Logarithmic encodings are expected to handle inequalities more efficiently. Order encodings are often viewed as a compromise, potentially balancing these trade-offs.

Performance Comparison

The choice of encoding significantly impacts performance depending on the constraint types used.

Direct Encoding: Better for Equality and Disequality

Direct encoding excels in models dominated by = and != constraints, such as graph coloring. It enables immediate unit propagation in the SAT solver, pruning values faster than bitwise reasoning.

Example: Graph Coloring

find c1, c2, c3, c4, c5 : int(1..3)
such that
    c1 != c2, c1 != c3, c2 != c3, c2 != c4,
    c3 != c4, c3 != c5, c4 != c5

• Direct: ~0.55s Rewriting / 0.001s Solving
• Log: ~1.61s Rewriting / 0.002s Solving

Logarithmic Encoding: Better for Inequalities

Logarithmic encoding is superior for arithmetic and inequalities (<, >, <=, >=) over large or sparse domains. Binary bit-vectors result in a more compact representation and reduced overhead.

Example: Sparse Domain with Inequalities

find x : int(1, 10, 20, 30, 40, 50)
such that x > 10

• Direct: ~1.24s Rewriting / 0.005s Solving
• Log: ~0.07s Rewriting / 0.000s Solving

Rule Types

Rule Sets

While developing rule-based transformations for conjure oxide, it is useful to understand the structure of the rulesets and the types of rules that can be used in conjure oxide. Let us first look at how rules actually function, not programmatically, but in an abstract sense. An understanding of (and some experience of) functional programming is incredibly helpful¹. Also useful is an understanding of the idea behind graph machines² and an understanding of the difference between function results and side effects³.

In conjure oxide, the rules are functions that take in the expression tree and the symbol table as arguments and return a function result⁴, meaning that the original expression tree and symbol table are only modified through side effects of rule functions⁵.

There are quite a few advantages to this system, including a few small quality-of-life things such as the ability to write more descriptive errors and to pattern match on function results. The most significant benefit, however, is the ability to express rules as functions that can do whatever they need to do as long as they return a failure or a success. This means that an application failure can be treated as a recoverable result rather than a crash.

Each function is self-contained⁶, meaning that the only things preserved are the initial symbol table and the expression, along with the result being passed along the call stack. The most significant benefit, however, is that this allows for code to be written in a way that enforces that errors are handled. This is quite useful in general because it means that the codebase can leverage Rust’s type system to eliminate edge cases everywhere.

The rule application is able to use this to avoid a situation where the rule engine fails unexpectedly and loses a large amount of work, or worse, a situation where a rule seems to have been applied and is visible in the trace but has not actually affected the tree because it failed⁷.

Now that we know how rules are called, we can move on to how the rules themselves are designed. Broadly, there are two categories that we can divide the rules into: Representation Rules and Transformation Rules. This is because, despite being applied in the same step in the process, they have different purposes from each other, but all rules of either type share a common goal.

Representation Rules

Essence (which is the input language of conjure oxide) defines domains that are not present in the type systems of the different solvers’ input languages, meaning they need to be encoded in some way into the input languages. The encoding is done using representation rules.

Representation rules implement shared behaviour using a trait⁸. The representation rules must change Essence variables into the target solver’s input language while preserving all of the relevant information. To actually do this, write a struct that implements the relevant trait. The rule engine can then use this to encode unsupported decision variable types.

Transformation Rules

After all of the variables in the symbol table have been encoded into the relevant types, the next thing to do is to convert all of the constraints in the conjure oxide AST into a form that has a one-to-one parallel with the input language of the target solver.

This done is using transformation rules, each of which is registered with a ‘priority’ and can then be used by the rule engine to convert the AST into a format that can be used by the solver adaptor.

1. Take a look at Graham Hutton’s Programming in Haskell (2nd Ed), and Miran Lipovača’s Learn You a Haskell for Great Good! for a lighter read ↩

2. https://amelia.how/posts/the-gmachine-in-detail.html ↩

3. Read the section of this text on ‘Functional Rust’ ↩

4. In Rust, this is std::Result<T, E> ↩

5. Particularly nice in Rust due to the way it does ownership and error handling ↩

6. Extra memory is freed when the function exits ↩

7. Unless unwrap is used ↩

8. See project documentation ↩

Useful Links

API Documentation

• conjure-cp

• tree-morph

• minion-sys

Internal crates

The following crates are internal, and are re-exported by conjure-cp:

• conjure-cp-cli
• conjure-cp-core
• conjure-cp-essence-macros
• conjure-cp-essence-parser
• conjure-cp-rule-macros
• conjure-cp-enum-compatibility-macro

Code Coverage

Code coverage reports can be found here.

Miscellaneous

• Essence feature usage stats
• Conjure blocks

Testing

Types of Tests

Conjure-Oxide currently has four forms of tests:

• Integration tests
• Custom tests
• Roundtrip tests
• A small number of unit tests

Test generation

The test generation occurs in the file ./tests_integration/build.rs. This generates the integration, custom and roundtrip tests all in a similar manner.

For each test framework we define a base directory for all these tests:

• ./tests_integration/tests/integration
• ./tests_integration/tests/custom
• ./tests_integration/tests/roundtrip

Any sub-directory of these defined directories containing the necessary files to make a test, will be considered a test.

• For integration and roundtrip tests this is containing a singular file with a .essence or .eprime extension.
• For custom tests this is containing a run.sh script file.

Once these tests are identified a Rust #[test] is created using the defined templates (<test type>_test_template). This test is within the pre-generated file gen_tests_<test type>.rs within the specified output directory (OUT_DIR).

This template contains the code to call a new function which carries out the test. The values passed to the template determines its test name, through sanitation of the path, and determine the arguments to this test function.

Finally, the test function itself includes the line include!(concat!(env!("OUT_DIR"), "/gen_tests_<test type>.rs"));, such that it is accessible during the test through insertion using the include macro.

This format improves scalability and allows new tests to be created by just creating the input file.

Roundtrip Testing

Overview

Roundtrip tests check that parsing is valid and that there is no unexpected behaviour during a full roundtrip of an Essence file. Roundtrip tests do not consider rewriting or solving.

Full Test Structure

The structure of a roundtrip test is shown in the following diagram:

The first phase tests that the parser is still performing as expected. As with the other tests in the suite, if the expected should have changed the suite can be run with ACCEPT=true to overwrite these expected files with whatever is generated.

• The test parses a provided Essence or Essence’ file.
• If this parse is valid, it saves the generated AST model JSON and generated Essence representation and compare these to the expected versions.
• Otherwise, is the parse fails; it saves the generated error outputs and compares this to the expected version.

The second phase tests that the structure of the input does not change during parsing without applying any rules to it, ensuring validity.

• If the initial parse was successful the roundtrip phase of the test occurs.
• The newly generated Essence is then parsed back into Conjure-Oxide and used to generate a new AST and output Essence file
• This new Essence file is then compared with the previously generated one and asserted equal.

Multiple Parsers

Roundtrip tests support both the ‘legacy’ and ‘native’ parser. The parser used for the test can be specified in a config.TOML in the test directory using the form parsers = [<string list of parsers>] Both parsers will be used by default for each test unless specified and will use separate generated and expected files as this may be different per parser.

Creating a New Roundtrip Test

To create a new roundtrip test you must create a new directory under ./tests-integration/tests/roundtrip/. Any directories within here than contain a singular .essence or .eprime file will be treated as a test. After creating the Essence or Essence’ file for your test you should run the test suite with ACCEPT=true to generate the expected files.

Creating Types Guide

Currently Conjure-Oxide does not have any support for Essence’s sequences, relations, partitions or variants. This guide outlines the process of creating support for those types to the AST. This does not currently cover rewriting rules or solving.

Creating the Type

• The domains of these types can contain pointers and so must be able to be both ground and unresolved. Hence you must add to the GroundDomain and UnresolvedDomain Enums
• Adding a new domain will require adding implementations for it, for a lot of related functions. To use the roundtrip tests the Display function fmt() must be implemented to match the Essence of the type.
• Next to complete some of these implementation you will need to add to the ReturnType Enum. This is the returned value from a specific element of the abstract type.
• Finally these functions will also require you to add to the AbstractLiteral Enum. This defines the values of a literal of that type. This will be required for defining the type explicitly. You should also note that we implement Uniplate for AbstractLiteral, and so this implementation will be required.

Adding to the Legacy Parser

Once the type can be stored in Conjure-Oxide’s AST, you will need to add parsing support.

• For the legacy parser this involves adding to parse_model.rs to parse the JSON output of Conjure’s parser.

Functions

What Are Functions

A function is a binary relation on two sets, from elements of a domain to elements of a codomain.

Functions have attributes and two domains for the domain and codomain of its results. They are defined for both GroundDomain and UnresolvedDomain as Function(FuncAttr, Moo<GroundDomain>, Moo<GroundDomain>).

The result of a function is a list of tuples defined by the mappings. As such the AbstractLiteral for functions is defined Function(Vec<(T, T)>). This AbstractLiteral type also means that functions can also be represented explicitly.

Attributes

Functions contain three types of attributes: size, partiality and jectivity.

Size attributes determine how many mappings the function is true for. Size attributes are converted to a Range<A> type in Conjure-Oxide. This size can be defined as:

• A single size size(x)
• A minimum size minSize(x)
• A maximum size maxSize(x)
• A range of sizes minSize(x) maxSize(x)
• Or unbounded by not specifying any attribute

Partiality determines whether the function is total or partial. A total function is one which is defined for every possible input in the domain set. A function will have partial partiality unless specified otherwise. Partiality is stored as an Enum inside Conjure-Oxide.

Jectivity refers to whether a function is injective, surjective, or bijective. These determine whether elements in the domain and codomain must have only one corresponding mapping. A function can also have no specified jectivity, which is the default. Jectivity is also stored as an Enum inside Conjure-Oxide.

Operators

There are seven operators which are defined on functions. These are represented as Expressions in Conjure-Oxide.

• Defined(f) - Returns the set of values in the domain for which a function f is defined.
• Image(f, x) - Returns the element of the codomain which is mapped to domain element x, in function f.
• ImageSet(f, x) - Returns the set of elements of the codomain which is mapped to domain element x, in function f.
• Inverse (f1, f2) - Returns a boolean representing if functions f1 and f2 are inverses of each other.
• PreImage(f, x) - Returns the set of elements of the domain which map to codomain element x, in function f.
• Range(f) - Returns the set of values in the domain for which a function f is defined.
• Restrict(f, D) - Returns a sub-function of f which has its mapping restricted to values in the domain D.

Note on Implementation

Currently functions are defined within the AST of Conjure-Oxide and can be parsed with the ‘legacy’ parser. However, there is no support as of Dec-2025 for rewriting rules or solving.

Multisets

What Are Multisets

A multiset is a datatype for storing a set of objects where objects can occur more than once, but the ordering of objects does not matter. Multisets have attributes and a single domain. A multiset can be defined for both GroundDomain and UnresolvedDomain.

Attributes

Three cardinality attributes; size, minSize, maxSize. Two occurrence attributes; minOccur, maxOccur.

In the original conjure implementation, a multiset was infinite without size, maxSize, or maxOccur. In the new conjure-oxide implementation, a variable’s domain is ground if it is fully-bounded (i.e. has a minSize and maxSize).

Operators

There are four operators which are defined on functions. These are represented as Expressions in Conjure-Oxide.

• hist(m) - histogram of multi-set m
• max(m) - largest element in ordered multiset m
• min(m) - largest element in ordered multiset m
• freq(m,e) - counts occurrences of element e in multiset m

Essence Parser

The parser converts incoming Essence programs in Conjure Oxide to the Model Object that the rule engine takes in. The relevant parts of the Model object are the SymbolTable and Expression objects. The symbol table is essentially a list of the variables and their corresponding domains. The Expression object is a recursive object that holds all the constraints of the problem, nested into one object. The parser has two main parts. The first is the tree-sitter-essence crate, which is a general Essence parser using the library tree-sitter. The second part is the conjure-cp-essence-parser crate which is Rust code that uses the grammar to parse Essence programs and convert them into the above-mentioned Model object.

Tree Sitter Grammar

Tree-sitter is a parsing library that creates concrete syntax trees from programs in various languages. It contains many languages already, but Essence is unfortunately not one of them. Therefore, the tree-sitter-essence crate contains a JavaScript grammar for Essence, which tree-sitter uses to create a parser. The parser is not specific to Conjure Oxide as the grammar merely describes the general Essence language, but it is used in and developed for Conjure Oxide so currently covers only parts of the Essence language that Conjure Oxide deals with and has tests written for. The grammar is based on this Essence documentation.

General Structure

At the top level, there can be either find statements, letting statements, or constraint statements. Find statements consist of the keyword find, one or more variables, and then a domain. Letting statements have the keyword letting, one or more variables, and an expression or domain to assign to those variables. Constraints contain the keyword such that and one or more logical or numerical expressions which include variables and constants.

Domains

Domains in Essence specify the set of possible values that a variable can take. The grammar currently supports the following types of domains:

• bool_domain: Boolean values (bool)
• int_domain: Integer values, which can be unbounded (int) or bounded by ranges (int(1..10), int(1..5, 10..15))
• tuple_domain: Tuples of multiple domains ((int(1..5), bool))
• matrix_domain: Multi-dimensional arrays indexed by domains (matrix indexed by [int(1..5)] of int(0..9))
• record_domain: Named records with typed fields (record {x: int, y: bool})
• set_domain: Sets with optional size constraints (set of int(1..10), set (minSize 2, maxSize 5) of bool)
• variable_domain: Domain references using identifiers, allowing domains to be parameterized or defined elsewhere

Expression Hierarchy

Expressions in the grammar are broken down into boolean expressions, comparison expressions, arithmetic expressions, and atoms. This separation helps enforce semantic constraints inherent to the language. For example, expressions like x + 3 = y are allowed because an arithmetic expression is permitted on either side of a comparison, but chained comparisons like x = y = 3 are disallowed, since a comparison expression cannot itself contain another comparison expression as an operand. This also helps ensure the top-most expression in a constraint evaluates to a boolean (so such that x + 3 wouldn’t be valid).

Atoms are the fundamental building blocks and represent constants, identifiers, and structured values (tuples, matrices, records, comprehensions, or slices). Atoms are separate from boolean and arithmetic expressions in the grammar hierarchy, though they can be used as operands in most expression contexts. This means a constraint like such that y would be valid syntactically even though y might be an integer - type checking happens at a later stage. List combining expressions are also separated into boolean and arithmetic variants for this reason (so such that allDiff([a, b]) is valid but such that min([a,b]) isn’t).

The precedence levels throughout the grammar are based on the Essence Prime operator precedence table found in Appendix B of the Savile Row Manual. This is important to ensure that nested or complicated expressions such as (2*x) + (3*y) = 12 are parsed in the correct order, as this will determine the structure of the Expression object in the Model.

Limitations of the Tree-sitter Grammar

Keyword Exclusion

Currently, the grammar allows for any combination of letters, numbers, and underscores to be parsed as variable identifiers. This includes reserved keywords of the Essence language such as ‘find’ or ‘letting’. This is incorrect and such keywords shouldn’t be allowed as variables. Tree-sitter doesn’t support lookahead assertions or negative matches, so grammar rules cannot exclude specific patterns or words from identifier rules. Checking for keywords as variables happens during semantic checking (see Diagnostics section).

Error Detection

Error detection from tree-sitter is unpredictable and can be confusing, as it simply creates ERROR nodes in the parse tree without detailed information about what was invalid. Similar errors will produce ERROR nodes in different places and impact the surrounding tree structure in varying ways, depending on the context. More sophisticated error detection and messaging has been implemented through Diagnostics.

Rust Parser

This is the second part of the parser and is contained in the conjure-cp-essence-parser crate. The primary function is parse_essence_file_native, shown below, which takes in the path to the input and the context and returns the Model or an error.

pub fn parse_essence_file_native(
    path: &str,
    context: Arc<RwLock<Context<'static>>>,
) -> Result<Model, EssenceParseError> {...}

Within that function, the source code is read from the input and the tree-sitter grammar is used to parse that code and produce a parse tree. From there, a Model object is created and the SymbolTable and Expression fields are populated by traversing and extracting information from the parse tree.

General Structure

The top level nodes (children of the root node), are either extras (comments or language labels), find statements, letting statements, or constraints. Find and letting statements provide info that is added to the SymbolTable while constraints are added to the Expression.

The parser crate is organized into multiple modules, each handling a specific aspect of Essence parsing:

• parse_model.rs: Entry point containing parse_essence_file_native. Handles top-level statement parsing (find, letting, constraints) and orchestrates the overall parsing process.
• expression.rs: Core expression parsing logic. Handles boolean expressions, comparisons, arithmetic operations, and dispatches to specialized parsers.
• atom.rs: Parses atomic expressions - constants, identifiers, tuples, matrices, records, set literals, and indexing/slicing operations.
• domain.rs: Domain parsing including integer domains (ranges), boolean domains, and matrix domains. Handles both ground domains (fully specified) and unresolved domains (containing references).
• find.rs: Parses find statements, extracting variable names and their domains for the symbol table.
• letting.rs: Parses letting statements, which can bind variables to either domains or expressions.
• comprehension.rs: Parses comprehensions, quantifiers (forAll, exists), and aggregate expressions (sum, product, min, max, etc.). This is a complex module handling generator expressions and nested quantification.
• abstract_literal.rs: Parses abstract literal structures like matrices, tuples, and records.

Layered Dispatch Pattern

The parser is designed with a hierarchical dispatch architecture where each module has a main entry point function that delegates to more specific functions based on the tree-sitter node type. This creates layers of abstraction:

1. Top-level dispatcher: Examines the node’s kind() to determine which category of parser to call (e.g., expression, domain, statement)
2. Category-level parsers: Further dispatch to specialized functions based on the specific variant (e.g., parse_binary_expression, parse_atom, parse_int_domain)
3. Specialized parsers: Handle the actual parsing logic for specific node types

This layered approach mirrors the structure of the tree-sitter grammar itself, where rules contain choices of subrules. This pattern keeps the codebase maintainable by separating concerns and making additions straightforward.

General utils

kind() is used to determine which rule a node represents and the corresponding function or logic is then applied to that node. Child nodes are found using their field names or indexes and the named_children() function is used to iterate over the named child nodes of a node. The function child_expr returns the Expression parsed from the first named child of the given node.

Extracting from the source code (identifiers and constants)

The tree-sitter nodes have a start and end byte indicating where the node corresponds to in the source code. For variable identifiers, constants, and operators, these bytes are necessary to extract the actual values from the source code.

For example, the following code appears in the parse_find_statement function and is used to extract the specific variable name from the source code, which is represented simply by a tree-sitter node (named variable in this case).

let variable_name = &source_code[variable.start_byte()..variable.end_byte()];

Another example is when parsing expressions, the node representing the operator is not always ‘named’, meaning it is not its own rule in the grammar and rather specified directly in the rule (ex. exponent: $ => seq($.arithmetic_expr, "**", $.arithmetic_expr) (simplified)), or the operator one of multiple choices in a rule (ex. mulitcative_op: $ => choice("*", "/", "%")). In this situation, the same method as for the variable identifiers is used:

let op = constraint.child_by_field_name("operator").ok_or(format!(
        "Missing operator in expression {}",
        constraint.kind()
    ))?;
let op_type = &source_code[op.start_byte()..op.end_byte()];

Find and Letting Statements

Find and letting statements are parsed relatively intuitively. For find statements, the list of variables is iterated over and each is added to a hash map as the key. Then, the domain is parsed and added as the value for each variable it applies to. Once all variables and domains are parsed, the hash map is returned and the caller function iterates over it and adds each pair to the SymbolTable. For letting statements, a new SymbolTable is created. The variables are again iterated over and added to the table. Letting statements can either specify a domain or an expression for the variables so the type of node is checked and either parsed as an expression or domain before being added to the table. The SymbolTable is returned and the caller function adds it to the existing SymbolTable of the Model.

Ground vs Unresolved Domains

The parser supports both ground domains (fully specified, e.g., int(1..10)) and unresolved domains (containing variable references, e.g., int(1..n)). For unresolved domains, the variable pointer must be retrieved from the existing SymbolTable, which was described in the previous section. Unresolved domains are resolved during later stages of processing once all variables are known.

Constraints

Adding constraints to the overall constraints Expression requires nesting Expression objects. Each constraint is parsed and then added to the model using the add_constraints function.

Following the layered dispatch pattern, expressions are organized into types (again mirroring the grammar):

• parse_expression in expression.rs: The main entry point that dispatches to specialized parsers based on node type
• parse_binary_expression: Handles binary operations
• parse_arithmetic_expression: Handles arithmetic operations
• parse_comparison_expression: Handles comparison operations
• parse_atom in atom.rs: Handles atomic expressions
• parse_comprehension in comprehension.rs: Handles comprehensions, quantifiers, and aggregates

Comprehensions, Quantifiers, and Aggregates

Comprehensions are a significant feature in Essence that require special parsing logic beyond the standard node-to-expression pattern. They are parsed by the comprehension.rs module using the specialized ComprehensionBuilder type that manages the complex scoping rules inherent to comprehensions.

Comprehensions create their own scope with local variables (generators). The parsing process involves:

1. Creating a ComprehensionBuilder: Initialized with the parent symbol table
2. Setting up scoped symbol tables: The builder creates two child symbol tables:
   • Generator symbol table: Contains generator variables as regular variables (for parsing conditions)
   • Return expression symbol table: Contains generator variables as “givens” (for parsing the return expression)
3. Parsing generators: Each generator (var : domain or var <- collection) is parsed and added to both symbol tables
4. Parsing conditions: Conditions are parsed using the generator symbol table, allowing them to reference generator variables
5. Parsing the return expression: Parsed using the return expression symbol table where generators appear as givens
6. Building the comprehension: The builder combines all components into a Comprehension object

Example: For [x + 1 | x : int(1..5), x > 2]:

• Generator x : int(1..5) is added to both symbol tables
• Condition x > 2 is parsed with x in scope as a variable
• Return expression x + 1 is parsed with x in scope as a given
• The result is wrapped in a Comprehension expression

Quantifiers and Aggregates

Quantifier expressions (forAll, exists) and aggregate expressions (sum, min, max) follow the same comprehension-based parsing approach through parse_quantifier_or_aggregate_expr. They:

1. Use ComprehensionBuilder to set up scoped symbol tables
2. Parse generators to add variables to the scope
3. Parse the body expression using the return expression symbol table
4. Build a comprehension with an appropriate AC operator kind (And for forAll, Sum for sum, etc.)
5. Wrap the comprehension in the corresponding expression type (Expression::And, Expression::Sum, etc.)

This unified approach ensures consistent scoping behavior across all comprehension-style constructs in Essence.

Testing

Integration Testing

The native parser (parse_essence_file_native) is used by default for all integration tests in the tests-integration crate, which include a range of tests for every feature currently supported. Also included in the integration testing suite is roundtrip testing. Some of the roundtrip tests test the parser’s error messages.

To explicitly disable the native parser for a specific test, add a config.toml file in the test directory with:

enable_native_parser = false

This will cause the test to fall back to the legacy parser instead.

Parser-Specific Tests

The conjure-cp-essence-parser crate contains its own unit tests that specifically test parser functionality. These tests can be run with:

cargo test -p conjure-cp-essence-parser

For more details on parser testing, see the parser testing documentation.

CST - Concrete Syntax Tree. Generated by the tree-sitter parser when parsing an essence file.

AST - Abstract Syntax Tree. Generated when the CST is parsed and Model struct is created.

Syntax Errors

Surface level mistakes in the Essence format. Lead to an invalid CST. They are caught by the tree-sitter when an Essence expression does not match any rules in the current grammar and cause the CST to have ERROR nodes.

Detected by inspecting and contextualising the CST.

1. Missing Token

Description

Expected token is absent.

Detection

MISSING node inserted or zero range node in the CST.

Example 1: Missing identifier(s)

find: bool

Example 2: Missing right operand

find x: int
such that x /

Example 3: Missing domain in tuple

find x: tuple()

2. Unexpected Token

Description

Symbol(s) that are not supposed to be there according to the grammar rule tree-sitter is matching. Can be tokens belonging to the grammar or any foreign symbols.

Detection

ERROR node wrapping the unexpected symbol(s).

Example 1: Extra ) at the end

find x: int(1..2))

Example 2: Unexpected % in implication

find x: int(1..3)
such that x -> %9

Example 3: Unexpected & inside matrix domain

find x: matrix indexed by [int, &] of int

3. Malformed Top Level Statement

Description

A line that cannot be parsed by the tree-sitter using any of the grammar rules.

Detection

ERROR node that is a direct child of the root node program and precedes the nodes if the parsed line.

Example 1: Invalid print x

find x: int(1..5)
print x 

Example 2: Malformed find statement

More of an edge case. Even though the keyword find is present, tree-sitter does not parse the line using the find_statement rule since the first symbol after find cannot be parsed an identifier.

find +,a,b: int(1..3)

4. General Syntax Error

Cases that cause an error in the CST but did not fall into any of the previous categories.

Semantic Errors

These errors concern the logical context of an expression rather than its surface-level formatting. As a result, the expression may conform to the grammar and produce a valid CST, but still fail to parse into a valid AST. Such errors are detected during the phase that converts the CST into a Model struct.

1. Keywords as Identifiers

Description

Using grammar keywords (e.g find, bool) as a variable name.

Detection

Compare the variable names against the set of keywords that should not be allowed.

Example 1: Keyword bool as an identifier

find bool: bool

Example 2: Keyword letting used as an identifier

find letting,b,c: int(1..3)

2. Omitted Declaration

Description

Variable used but not declared.

Detection

Checking that the identifier used in a constraint was previously declared in a find or letting_statement.

Example: x was not declared before

find y: int (1..4)
such that x = 5

3. Invalid Domain

(not yet supported)

Description

Logically or mathematically invalid bounds.

Example: a bigger value before smaller

find x: int(10..5)

4. Type Mismatch

Description

Attempt to do an operation on illegal types.

Detection

Enforcing types on operations and catching a mismatch between expected types and node kind that is being parsed.

Example: Adding an integer and boolean

letting y be true 
find x: int (5..10)
such that 5 + y = 6

5. Unsafe division

(not yet implemented)

Description

Attempt to divide/modulo by zero.

Example: Divide by zero

find x: int(5..10)
such that x/0 = 3

At the moment says no solutions found. Would want to explicitly disallow it.

6. Invalid indexing

Description

Tuples and matrices are indexed from 1. Negative, zero or index out of bounds is invalid.

Example: s tuple index of out bounds

letting s be tuple(0,1,1,0)
letting t be tuple(0,0,0,1)
find a : bool such that a = (s[5] = t[1]) $ true

Conjure Blocks

Conjure blocks is an online block editor for Essence. This tool allows you to write constraint programs in blocks, which are then translated into Essence. Conjure-aaS is used to solve these problems. Conjure blocks is an ongoing project.

See the the Conjure Blocks repository, the Conjure Blocks Documentation and the live site for more information.

For Interested Students

This project is developed as part of the “Artificial Intelligence for Decision Making” Vertically Integrated Project module. For more information on the VIP, click here.

Contributors