#547 Decouple Solver Component into Standalone Crate#25
#547 Decouple Solver Component into Standalone Crate#25tareknaser wants to merge 1 commit intomainfrom
Conversation
momvart
left a comment
momvart
left a comment
There was a problem hiding this comment.
Thanks for the effort.
An important missing piece:
As I mentioned before, except sanity checking, we will negate some constraints to derive a new input. Currently, we don't have any mechanism for that. Although implementing it will be done by supporting a view on the query, for now we can have an option to negate the last constraint as a minimum.
Beside that, things look fine for now. I'll rebase to your branch and use your binary for actual solving.
| match output.result.as_str() { | ||
| "sat" => println!( | ||
| "✓ SAT - Solution found and written to {}", | ||
| args.output.display() | ||
| ), | ||
| "unsat" => println!("✗ UNSAT - No solution exists"), | ||
| "unknown" => println!("? UNKNOWN - Could not determine satisfiability"), | ||
| _ => unreachable!("Unexpected result: {}", output.result), | ||
| } |
There was a problem hiding this comment.
Use macros in common:logging for logging.
|
|
||
| let constraint_value = json_value | ||
| .as_object_mut() | ||
| .and_then(|obj| obj.remove("constraint")) |
There was a problem hiding this comment.
Make sure you use consts for these stuff.
| /// Input format for JSONL constraint files | ||
| #[derive(Debug, Serialize, Deserialize)] | ||
| pub struct ConstraintEntry { | ||
| pub step: StepInfo, |
|
|
||
| // Serialization support for binary interface | ||
| #[cfg(feature = "serde")] | ||
| pub mod format { |
There was a problem hiding this comment.
As this format only concerns the binary, I'd like it out of the library but in the binary's module
| } | ||
|
|
||
| #[test] | ||
| fn test_constraint_kind_operations() { |
There was a problem hiding this comment.
Thanks for writing the tests. I see some of them are focused on common's data structures. Why not moving them there next to their definitions?
momvart
changed the title
2 participants
This PR extracts the SMT solving functionality from the codebase into a standalone
leafsolvercrate. The new crate provides both a library interface and a CLI binary