feat(SAT): implement negation -a for order encoding

[Andrew-Mullan]

Description

This PR implements the negation rule for order encoding in SAT and adds integration tests for the new rule. The new neg_sat_order function reverses the old bit vector, then pads with false at the front, then negates the bits.

Example

Say we have domain D = [-3..2], $x = 1$, so we want to find $y = -x = -1$. Start with [1, 1, 1, 1, 1, 0]

New domain D' = [-2..3] and our target bitvector for y is [1, 1, 0, 0, 0, 0]

1. Reverse bits: [0, 1, 1, 1, 1, 1]
2. Insert false at front: [0, 0, 1, 1, 1, 1]
3. NOT each bit: [1, 1, 0, 0, 0, 0]

We now have an order representation for -1 as desired.

Related issues

Closes #1253

Key changes

• Add new function neg_sat_order in order_int_ops.rs as above.
• Add test files in cnf/int_order/03-neg

How to test/review

Checkout branch feat/sat/order_negation, run tests and/or solve with Essence model in directory shown above.

@ozgurakgun fyi as requested

[conjure-bot]

RustDoc Coverage

Report: https://conjure-cp.github.io/conjure-oxide-reports/pr/1536/coverage-docs/index.html

This PR: 43.24% documented, 3.43% with examples (35/441/1020)
Main: 43.24% documented, 3.43% with examples (35/441/1020)
Delta: docs +0.00 pp, examples +0.00 pp

[conjure-bot]

Code Coverage

Report: https://conjure-cp.github.io/conjure-oxide-reports/pr/1536/coverage-code/index.html
Diff report: https://conjure-cp.github.io/conjure-oxide-reports/pr/1536/coverage-code/diff-coverage.html

This PR: 74.72% lines (16924/22649)
Diff: 100.00% lines (30/30 measured; 16224 changed)
Main: 74.70% lines (16896/22619)
Delta vs main: +0.02 pp

[YehorBoiar]

add // consider covered and LGTM!

[ozgurakgun]

I wonder if we should add Err(RuleNotApplicable) to the list of stuff we exclude from code coverage.

[ozgurakgun]

just to confirm these are commented out on purpose?

[Andrew-Mullan]

I may not be fully understanding: I was under the impression that since this is a test for int_order, that it should only use sat-order to solve. I suppose this is a side effect of the old tests naming, and we now aim to have each and every test pass with as many solvers as possible?

I have added log and direct with output as expected.

[ozgurakgun]

we may be adding a test specifically to test a certain configuration, but want to also enable that test for all other configurations (unless there is a reason not to).

[Andrew-Mullan]

That makes sense, thanks for clarifying

[YehorBoiar]

lgtm!