Implement global context

[niklasdewally]

Problems

User settings

There is information given by the user at the start of the program that we will need to use all the way through the program.
For example:

1. What solver type (Minion vs SAT)
2. What solver implementation (eg for SAT, lingling or kissat.)
3. For SAT, what type of encoding to use?

This information is useful both during rewriting, and to decide what solver to use / what parameters to give it.
See: #199 #103

Solver stats

Solvers can produce different metadata / stats, such as CPU time or node count.
Conjure now can capture this and store a s a JSON file. We need to be able to extract this information and use it in our CI (for performance testing) - see #247 #248

Having a general way to pass information between layers is useful in general

Proposal

TODO

Questions

1. What options do we need?
2. How will we store solver specific information?

[niklasdewally]

RFC @ozgurakgun @Kieranoski702 @lixitrixi @PedroGGBM @gskorokhod

[niklasdewally]

For clarification, solver type vs implementation is an important distinction because we do not care in most places that we are using Lingling, Caddical, etc, just that we are solving for SAT. Solver type will be used to determine which rules apply, and the Solver Implementation will be used to determine what solver adaptor to use.

[niklasdewally]

(FYI @gskorokhod @lixitrixi)

Some additional requirements discussed in yesterdays meeting:

Configuration needs to be thread-safe - i.e. usable across threads. We also may want multiple configurations at once - for example, so that cargo test can run multiple runs of the rewriter in parallel using different settings. Therefore, configuration can not be a global variable.

Some other (optional) thoughts:

• A nice pattern to avoid having pass-through variables in every function is to have the main data-structure in each layer of abstraction hold a pointer to its "context" (Ousterhout, Software Design). In our case, this could mean that the "rewriting" layer could access global context through a pointer in the Model struct and the "solving" layer could access global context through a pointer in the Solver struct. This would mean basically no refactoring apart from at the boundaries between the parse and rewriting and rewriting and solver layers. In Rust this pointer would probably be an Arc<Context>.

• The Context could be immutable with us allowing the mutation of specific inner values only through a Mutex<>.

• To ensure backwards compatibility as we add stuff to it, contexts could be unable to be constructed manually, using a builder and/or ::new().

[niklasdewally]

Happy for you to take this @gskorokhod if you are still interested :)

[gskorokhod]

Happy for you to take this @gskorokhod if you are still interested :)

Hmm, I could! I will take a few days to get my midterm report submited and start working on the next C practical though

[gskorokhod]

I think i'm interested in working on uniplate and learning more about that though. But I'm still happy to take this if need be!

[niklasdewally]

I think i'm interested in working on uniplate and learning more about that though. But I'm still happy to take this if need be!

Just brought it up because you mentioned it earlier :) It's marked as help wanted so someone might pick it up at some point. Otherwise I imagine Felix or me may end up doing this as we need it for SAT.

[gskorokhod]

Reanimating this issue because we need it for performance testing :)

[gskorokhod]

From Friday meeting:

• Our system is multi-threaded, so every thread should have its own global context (hence it can't be a static object)
• Context should be a part of the object that gets passed around between layers (e.g. Model). not a separate parameter
• Every layer should be self contained. In the future, it should be possible to support different use cases, such as:
  • Importing conjure as a library and running each layer individually from within a user's Rust program
  • Running conjure as a server, taking new problems as they come, and saving something / doing some computation in between (e.g. caching parts of the rewrite to speed things up)

[niklasdewally]

@ozgurakgun @gskorokhod what's the current status of this? I think this issue has been completed.

[niklasdewally]

@ozgurakgun closing this as completed.