pull request for Sat backend #415

Shikhar-Srivastava-16 · 2024-11-05T15:44:31Z

Opened a PR for the sat backend, very basic implementation at the moment but as this point, the best approach is to work with the rest of the team. Please take a look at the code to see if there are any glaring problems

niklasdewally · 2024-11-05T15:51:07Z

solvers/sat_rs/src/main.rs

I'm not sure what your longer term intentions are, but if this just wraps rustsat, it might not need to be its own crate.

FYI: you won't be able to use any conjure_core types in here due to circular dependencies, so any conversion code from Conjure Oxide AST will have to go in conjure_core not a seperate crate.

It's not to create a wrapper for rustsat, I'm trying to pretty much replace the kissat_rs crate that we're using - mostly because this will provide the functionality for all or most sat solvers. I'm essentially just writing functions to create a tree and to solve that tree so that the larger conjure_core/conjure_oxide functions can call. I'm not planning on calling any of the conjure_core functions from this so, that's not something we need to worry about. Thanks

Sounds good. Note that we never actually used kissat_rs, so I wouldn't worry about trying to match that in any way. (more generally, as long as things still conform to the solver interface, you can gut and rework them as much as you want)

builds, runs but untested

github-actions · 2024-11-06T00:03:59Z

Code and Documentation Coverage Report

Documentation Coverage

Click to view documentation coverage for this PR

+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| crates/conjure_macros/src/lib.rs    |          2 |      66.7% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          2 |      66.7% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| ...m_compatability_macro/src/lib.rs |          2 |     100.0% |          1 |      50.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          2 |     100.0% |          1 |      50.0% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| solvers/sat_rs/src/main.rs          |          0 |       0.0% |          0 |       0.0% |
| solvers/sat_rs/src/sat_tree.rs      |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| solvers/minion/src/ast.rs           |         11 |      11.0% |          0 |       0.0% |
| solvers/minion/src/error.rs         |          8 |     100.0% |          0 |       0.0% |
| solvers/minion/src/lib.rs           |          1 |     100.0% |          1 |     100.0% |
| solvers/minion/src/run.rs           |          2 |     100.0% |          1 |     100.0% |
| solvers/minion/src/wrappers.rs      |          1 |     100.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |         23 |      20.5% |          2 |      11.8% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| ...onjure_core/src/ast/constants.rs |          0 |       0.0% |          0 |       0.0% |
| .../conjure_core/src/ast/domains.rs |          0 |       0.0% |          0 |       0.0% |
| ...jure_core/src/ast/expressions.rs |         26 |      96.3% |          0 |       0.0% |
| crates/conjure_core/src/ast/mod.rs  |          0 |       0.0% |          0 |       0.0% |
| ...ure_core/src/ast/symbol_table.rs |          0 |       0.0% |          0 |       0.0% |
| ...es/conjure_core/src/ast/types.rs |          0 |       0.0% |          0 |       0.0% |
| ...onjure_core/src/ast/variables.rs |          1 |      50.0% |          0 |       0.0% |
| crates/conjure_core/src/bug.rs      |          1 |      50.0% |          1 |      50.0% |
| crates/conjure_core/src/context.rs  |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/error.rs    |          1 |      14.3% |          0 |       0.0% |
| crates/conjure_core/src/lib.rs      |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/metadata.rs |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/model.rs    |          2 |      12.5% |          0 |       0.0% |
| ...core/src/parse/example_models.rs |          2 |     100.0% |          0 |       0.0% |
| ...es/conjure_core/src/parse/mod.rs |          0 |       0.0% |          0 |       0.0% |
| ...re_core/src/parse/parse_model.rs |          0 |       0.0% |          0 |       0.0% |
| ...jure_core/src/rule_engine/mod.rs |          5 |      71.4% |          5 |      71.4% |
| ...src/rule_engine/resolve_rules.rs |          3 |     100.0% |          0 |       0.0% |
| ..._core/src/rule_engine/rewrite.rs |          2 |      66.7% |          0 |       0.0% |
| ...ure_core/src/rule_engine/rule.rs |          3 |      25.0% |          1 |     100.0% |
| ...core/src/rule_engine/rule_set.rs |          4 |     100.0% |          0 |       0.0% |
| ...conjure_core/src/rules/checks.rs |          1 |      50.0% |          0 |       0.0% |
| ...njure_core/src/rules/constant.rs |          1 |     100.0% |          0 |       0.0% |
| ...es/conjure_core/src/rules/mod.rs |          1 |     100.0% |          0 |       0.0% |
| ...re/src/solver/adaptors/kissat.rs |          1 |     100.0% |          0 |       0.0% |
| ...re/src/solver/adaptors/minion.rs |          1 |     100.0% |          0 |       0.0% |
| ..._core/src/solver/adaptors/mod.rs |          1 |     100.0% |          0 |       0.0% |
| ...s/conjure_core/src/solver/mod.rs |         14 |      33.3% |          1 |       4.2% |
| ...ore/src/solver/model_modifier.rs |          7 |      70.0% |          0 |       0.0% |
| ...onjure_core/src/solver/states.rs |          7 |      63.6% |          0 |       0.0% |
| ...es/conjure_core/src/stats/mod.rs |          0 |       0.0% |          0 |       0.0% |
| ...core/src/stats/rewriter_stats.rs |          1 |      20.0% |          0 |       0.0% |
| ...e_core/src/stats/solver_stats.rs |          3 |      37.5% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |         88 |      41.5% |          8 |       9.6% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| conjure_oxide/src/defaults.rs       |          1 |      50.0% |          0 |       0.0% |
| conjure_oxide/src/find_conjure.rs   |          1 |      50.0% |          0 |       0.0% |
| conjure_oxide/src/lib.rs            |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/conjure.rs  |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/json.rs     |          2 |      66.7% |          0 |       0.0% |
| conjure_oxide/src/utils/misc.rs     |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/mod.rs      |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/testing.rs  |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          4 |      12.9% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+

Click to view documentation coverage for main

+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| crates/conjure_macros/src/lib.rs    |          2 |      66.7% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          2 |      66.7% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| ...m_compatability_macro/src/lib.rs |          2 |     100.0% |          1 |      50.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          2 |     100.0% |          1 |      50.0% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| solvers/kissat/src/lib.rs           |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| solvers/minion/src/ast.rs           |         11 |      11.0% |          0 |       0.0% |
| solvers/minion/src/error.rs         |          8 |     100.0% |          0 |       0.0% |
| solvers/minion/src/lib.rs           |          1 |     100.0% |          1 |     100.0% |
| solvers/minion/src/run.rs           |          2 |     100.0% |          1 |     100.0% |
| solvers/minion/src/wrappers.rs      |          1 |     100.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |         23 |      20.5% |          2 |      11.8% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| ...onjure_core/src/ast/constants.rs |          0 |       0.0% |          0 |       0.0% |
| .../conjure_core/src/ast/domains.rs |          0 |       0.0% |          0 |       0.0% |
| ...jure_core/src/ast/expressions.rs |         26 |      96.3% |          0 |       0.0% |
| crates/conjure_core/src/ast/mod.rs  |          0 |       0.0% |          0 |       0.0% |
| ...ure_core/src/ast/symbol_table.rs |          0 |       0.0% |          0 |       0.0% |
| ...es/conjure_core/src/ast/types.rs |          0 |       0.0% |          0 |       0.0% |
| ...onjure_core/src/ast/variables.rs |          1 |      50.0% |          0 |       0.0% |
| crates/conjure_core/src/bug.rs      |          1 |      50.0% |          1 |      50.0% |
| crates/conjure_core/src/context.rs  |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/error.rs    |          1 |      14.3% |          0 |       0.0% |
| crates/conjure_core/src/lib.rs      |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/metadata.rs |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/model.rs    |          2 |      12.5% |          0 |       0.0% |
| ...core/src/parse/example_models.rs |          2 |     100.0% |          0 |       0.0% |
| ...es/conjure_core/src/parse/mod.rs |          0 |       0.0% |          0 |       0.0% |
| ...re_core/src/parse/parse_model.rs |          0 |       0.0% |          0 |       0.0% |
| ...jure_core/src/rule_engine/mod.rs |          5 |      71.4% |          5 |      71.4% |
| ...src/rule_engine/resolve_rules.rs |          3 |     100.0% |          0 |       0.0% |
| ..._core/src/rule_engine/rewrite.rs |          2 |      66.7% |          0 |       0.0% |
| ...ure_core/src/rule_engine/rule.rs |          3 |      25.0% |          1 |     100.0% |
| ...core/src/rule_engine/rule_set.rs |          4 |     100.0% |          0 |       0.0% |
| ...conjure_core/src/rules/checks.rs |          1 |      50.0% |          0 |       0.0% |
| ...njure_core/src/rules/constant.rs |          1 |     100.0% |          0 |       0.0% |
| ...es/conjure_core/src/rules/mod.rs |          1 |     100.0% |          0 |       0.0% |
| ...re/src/solver/adaptors/kissat.rs |          1 |     100.0% |          0 |       0.0% |
| ...re/src/solver/adaptors/minion.rs |          1 |     100.0% |          0 |       0.0% |
| ..._core/src/solver/adaptors/mod.rs |          1 |     100.0% |          0 |       0.0% |
| ...s/conjure_core/src/solver/mod.rs |         14 |      33.3% |          1 |       4.2% |
| ...ore/src/solver/model_modifier.rs |          7 |      70.0% |          0 |       0.0% |
| ...onjure_core/src/solver/states.rs |          7 |      63.6% |          0 |       0.0% |
| ...es/conjure_core/src/stats/mod.rs |          0 |       0.0% |          0 |       0.0% |
| ...core/src/stats/rewriter_stats.rs |          1 |      20.0% |          0 |       0.0% |
| ...e_core/src/stats/solver_stats.rs |          3 |      37.5% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |         88 |      41.5% |          8 |       9.6% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| conjure_oxide/src/defaults.rs       |          1 |      50.0% |          0 |       0.0% |
| conjure_oxide/src/find_conjure.rs   |          1 |      50.0% |          0 |       0.0% |
| conjure_oxide/src/lib.rs            |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/conjure.rs  |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/json.rs     |          2 |      66.7% |          0 |       0.0% |
| conjure_oxide/src/utils/misc.rs     |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/mod.rs      |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/testing.rs  |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          4 |      12.9% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+

Code Coverage Summary

This PR: Detailed Report

  lines......: 72.6% (3189 of 4392 lines)
  functions..: 45.6% (369 of 809 functions)
  branches...: no data found

Main: Detailed Report

  lines......: 73.1% (3209 of 4389 lines)
  functions..: 45.8% (370 of 807 functions)
  branches...: no data found

Coverage Main & PR Coverage Change

Lines coverage changed by -0.50% and covered lines changed by -20
Functions coverage changed by -0.20% and covered lines changed by -1
Branches... coverage: No comparison data available

ozgurakgun · 2024-11-08T14:24:25Z

Not sure what the plan is here @Shikhar-Srivastava-16 - are you planning to update the PR to work with the solver adaptor interface or abandon this and work on a separate PR or soemthing else?

niklasdewally · 2024-11-08T14:38:55Z

I would be happy to run through my slides on the solver adaptor / do a bit of Q&A during Wednesdays meeting if it would be helpful @ozgurakgun @Shikhar-Srivastava-16 @ewilbert7

ozgurakgun · 2024-11-08T18:44:40Z

I would be happy to run through my slides on the solver adaptor / do a bit of Q&A during Wednesdays meeting if it would be helpful @ozgurakgun @Shikhar-Srivastava-16 @ewilbert7

great idea, thanks for the offer.

ewilbert7 · 2024-11-13T08:06:06Z

I would be happy to run through my slides on the solver adaptor / do a bit of Q&A during Wednesdays meeting if it would be helpful @ozgurakgun @Shikhar-Srivastava-16 @ewilbert7

That would very helpful! Thanks for the offer.

…re-oxide

Shikhar-Srivastava-16 · 2024-11-26T19:09:19Z

Added relevant functions for the loading step, the only remaining todo is to fix the error handling - at the moment the function uses the panic!() macro instead of CNFError.

The adaptor is set up to use a standard instance of the solve structs in rustsat, but will be able to use any type of the generic SatSolver.

…solve function rmoved kissat file **currently using MiniSat

ozgurakgun · 2024-12-01T15:18:20Z

crates/conjure_core/Cargo.toml

@@ -26,6 +26,9 @@ schemars = "0.8.21"
 clap = { version = "4.5.20", features = ["derive"] }
 itertools = "0.13.0"
 im = "15.1.0"
+sat_rs = { version = "0.1.0", path = "../../solvers/sat_rs" }


I thought we decided to remove the sat_rs crate, is it still needed?

still being used for some of the model loading step, so retaining it.

crates/conjure_core/src/solver/adaptors/sat_adaptor.rs

crates/conjure_core/src/solver/adaptors/common.rs.txt

Shikhar-Srivastava-16 added 2 commits November 4, 2024 21:39

basic framework

136d488

added basic functions

b44b2fb

niklasdewally reviewed Nov 5, 2024

View reviewed changes

Shikhar-Srivastava-16 added 5 commits November 5, 2024 21:53

refactored into separate module

5e03ea5

basic functions for populating SatInstance

fd58cbf

builds, runs but untested

removed kissat lib, not in use

1d02783

changes to Cargo.toml

a764a25

changes to building cargo.lock, auto-gen

ac6b5c4

Shikhar-Srivastava-16 added 4 commits November 6, 2024 10:10

added solver_instance with trait for solver and updated library script

0c662cc

removed unused file

ae9bc3b

basic structure for solver adaptor, may not function well

5f39b3b

more basics, see before

faada12

push for adaptor

42beb47

Devansh Chopra and others added 7 commits November 13, 2024 13:26

Updated the lib.rs and added solver_utils to it

1e34041

Updated main.rs to display the solver result

261dd47

Updated main.rs to display the solver result

5fcd6b6

Updated all sat_rs files by implementing a solver and mapping

5194683

minor change to main.rs, temp

9c6397f

Merge branch 'main' of https://github.com/Shikhar-Srivastava-16/conju…

d949cdf

…re-oxide

debugging

e29dcaf

ozgurakgun mentioned this pull request Nov 22, 2024

var_map in sat solvers #479

Open

Shikhar Srivastava added 3 commits November 23, 2024 02:03

changes

ea2ce69

final functions for model generation (must integrate into load)

615c76f

removed kissat.rs file, made relevant changes to other files

80e780f

Shikhar-Srivastava-16 self-assigned this Nov 26, 2024

Shikhar Srivastava and others added 5 commits November 27, 2024 02:45

function in SolverAdaptor trait called, partial implementation for …

6659fdd

…solve function rmoved kissat file **currently using MiniSat

housekeeping

b139de3

Implemented the solver and edited the coversion functions as well

d806a7e

Making changes

f62e008

housekeeping

b01b714

ozgurakgun reviewed Dec 1, 2024

View reviewed changes

crates/conjure_core/src/solver/adaptors/sat_adaptor.rs Outdated Show resolved Hide resolved

ozgurakgun reviewed Dec 1, 2024

View reviewed changes

crates/conjure_core/src/solver/adaptors/common.rs.txt Outdated Show resolved Hide resolved

Shikhar Srivastava and others added 2 commits December 1, 2024 18:13

adaptor changes

b222638

Fixed bugs and implemeneted a solver

55d0458

Shikhar-Srivastava-16 force-pushed the main branch from 3abe23a to 55d0458 Compare December 16, 2024 19:26

rename + auxiliary file deleted

c2b2d32

Shikhar-Srivastava-16 force-pushed the main branch from c7cf943 to c2b2d32 Compare December 17, 2024 03:33

Shikhar-Srivastava-16 and others added 4 commits December 19, 2024 11:39

rename, unneeded main deleted

731921b

rename WIP

25162e2

tests added

c9ca602

Cleaned up some code and removed coments from files I have worked on

f20119f

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

pull request for Sat backend #415

pull request for Sat backend #415

Shikhar-Srivastava-16 commented Nov 5, 2024

niklasdewally Nov 5, 2024 •

edited

Loading

niklasdewally Nov 5, 2024 •

edited

Loading

Shikhar-Srivastava-16 Nov 5, 2024

niklasdewally Nov 5, 2024

github-actions bot commented Nov 6, 2024

ozgurakgun commented Nov 8, 2024

niklasdewally commented Nov 8, 2024

ozgurakgun commented Nov 8, 2024

ewilbert7 commented Nov 13, 2024

Shikhar-Srivastava-16 commented Nov 26, 2024

ozgurakgun Dec 1, 2024

Shikhar-Srivastava-16 Dec 15, 2024

pull request for Sat backend #415

Are you sure you want to change the base?

pull request for Sat backend #415

Conversation

Shikhar-Srivastava-16 commented Nov 5, 2024

niklasdewally Nov 5, 2024 • edited Loading

Choose a reason for hiding this comment

niklasdewally Nov 5, 2024 • edited Loading

Choose a reason for hiding this comment

Shikhar-Srivastava-16 Nov 5, 2024

Choose a reason for hiding this comment

niklasdewally Nov 5, 2024

Choose a reason for hiding this comment

github-actions bot commented Nov 6, 2024

Code and Documentation Coverage Report

Documentation Coverage

Code Coverage Summary

Coverage Main & PR Coverage Change

ozgurakgun commented Nov 8, 2024

niklasdewally commented Nov 8, 2024

ozgurakgun commented Nov 8, 2024

ewilbert7 commented Nov 13, 2024

Shikhar-Srivastava-16 commented Nov 26, 2024

ozgurakgun Dec 1, 2024

Choose a reason for hiding this comment

Shikhar-Srivastava-16 Dec 15, 2024

Choose a reason for hiding this comment

niklasdewally Nov 5, 2024 •

edited

Loading

niklasdewally Nov 5, 2024 •

edited

Loading