Grcov report - pseudo

1

//! Preserve linear constraints and numeric relations as semantic library decisions.

2

use conjure_cp::ast::sat_decision::{CardinalityRelation, PbTermGroup, PbTermStructure};

3

use conjure_cp::ast::{

4

    AbstractLiteral::Matrix, Atom, Expression as Expr, Literal, Metadata, SATIntEncoding,

5

    SatEncodingDecision, SymbolTable,

6

};

7

use conjure_cp::rule_engine::{

8

    ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect, register_rule,

9

};

10

11

#[derive(Default)]

12

struct Linear {

13

    constant: i128,

14

    terms: Vec<(i128, Expr)>,

15

    groups: Vec<PbTermGroup>,

16

17

impl Linear {

18

49209704

    fn add(&mut self, expression: &Expr, scale: i128) -> Option<()> {

19

49209704

        match expression {

20

            Expr::Atomic(_, Atom::Literal(Literal::Int(value))) => {

21

3097098

                self.constant = self

22

3097098

                    .constant

23

3097098

                    .checked_add(scale.checked_mul(i128::from(*value))?)?

24

25

            Expr::Atomic(_, Atom::Reference(reference)) => {

26

                use crate::types::int::{

27

                    IntBinaryOffset, IntBinaryRank, IntBinarySignMagnitude,

28

                    IntBinaryTwosComplement, IntDirect, IntOrder,

29

};

30

6574788

                let represented = if let Some(state) = reference.get_repr_as::<IntDirect>() {

31

1523732

                    state.sat_int_expr()

32

5051056

                } else if let Some(state) = reference.get_repr_as::<IntOrder>() {

33

268791

                    state.sat_int_expr()

34

4782265

                } else if let Some(state) = reference.get_repr_as::<IntBinaryOffset>() {

35

405019

                    state.sat_int_expr()

36

4377246

                } else if let Some(state) = reference.get_repr_as::<IntBinaryRank>() {

37

177237

                    state.sat_int_expr()

38

4200009

                } else if let Some(state) = reference.get_repr_as::<IntBinarySignMagnitude>() {

39

217749

                    state.sat_int_expr()

40

                } else {

41

3982260

                    reference

42

3982260

                        .get_repr_as::<IntBinaryTwosComplement>()?

43

                        .sat_int_expr()

44

};

45

2771798

                self.add(&represented, scale)?;

46

47

            Expr::Minus(_, left, right) => {

48

251209

                self.add(left, scale)?;

49

52346

                self.add(right, scale.checked_neg()?)?;

50

51

127239

            Expr::Neg(_, input) => self.add(input, scale.checked_neg()?)?,

52

            Expr::Sum(_, inputs) => {

53

7313722

                let Expr::AbstractLiteral(_, Matrix(inputs, _)) = inputs.as_ref() else {

54

366695

                    return None;

55

};

56

6947027

                for input in inputs {

57

17003951

                    self.add(input, scale)?;

58

59

60

            Expr::Product(_, inputs) => {

61

1354346

                let Expr::AbstractLiteral(_, Matrix(inputs, _)) = inputs.as_ref() else {

62

14

                    return None;

63

};

64

1354332

                let mut multiplier = scale;

65

1354332

                let mut variable = None;

66

1354332

                for input in inputs {

67

2718086

                    if let Some(value) = constant_int(input) {

68

692230

                        multiplier = multiplier.checked_mul(i128::from(value))?;

69

2025856

                    } else if variable.replace(input).is_some() {

70

671524

                        return None;

71

1354332

72

73

682808

                if let Some(variable) = variable {

74

682808

                    self.add(variable, multiplier)?;

75

                } else {

76

                    self.constant = self.constant.checked_add(multiplier)?;

77

78

79

            Expr::ToInt(_, input)

80

4008181

                if crate::shared::utils::is_literal(input)

81

1246415

                    && input.domain_of().is_some_and(|domain| domain.is_bool()) =>

82

83

1246415

                self.terms.push((scale, input.as_ref().clone()))

84

85

            Expr::SATInt(_, encoding, inner, (low, high)) => {

86

14526701

                let bits = inner.unwrap_list_cow()?;

87

14526701

                let start = self.terms.len();

88

14526701

                let structure = match encoding {

89

                    SATIntEncoding::Direct => {

90

2596013

                        if bits.len() as i128 != i128::from(*high) - i128::from(*low) + 1 {

91

                            return None;

92

2596013

93

                        // Direct and Order retain the domain span; separate structural

94

                        // constraints exclude sparse-domain gaps.

95

2596013

                        for (index, bit) in bits.iter().enumerate() {

96

14512141

                            self.terms.push((

97

14512141

                                scale.checked_mul(i128::from(*low) + index as i128)?,

98

14512141

                                bit.clone(),

99

));

100

101

2596013

                        Some(PbTermStructure::Choice)

102

103

                    SATIntEncoding::Order => {

104

543598

                        if bits.len() as i128 != i128::from(*high) - i128::from(*low) + 1 {

105

                            return None;

106

543598

107

543598

                        self.constant = self

108

543598

                            .constant

109

543598

                            .checked_add(scale.checked_mul(i128::from(*low))?)?;

110

543598

                        for bit in bits.iter().skip(1) {

111

3622727

                            self.terms.push((scale, bit.clone()));

112

113

543598

                        Some(PbTermStructure::Chain)

114

115

                    SATIntEncoding::Offset | SATIntEncoding::Rank(_) => {

116

1276506

                        if let SATIntEncoding::Rank(ranges) = encoding

117

543121

                            && ranges.as_slice() != [(*low, *high)]

118

119

241106

                            return None;

120

1035400

121

1035400

                        if bits.is_empty() || bits.len() > 32 {

122

                            return None;

123

1035400

124

1035400

                        self.constant = self

125

1035400

                            .constant

126

1035400

                            .checked_add(scale.checked_mul(i128::from(*low))?)?;

127

1035400

                        for (index, bit) in bits.iter().enumerate() {

128

2472659

                            self.terms

129

2472659

                                .push((scale.checked_mul(1i128 << index)?, bit.clone()));

130

131

1035400

                        binary_structure(scale, 0, i128::from(*high) - i128::from(*low))

132

133

                    SATIntEncoding::SignMagnitude => {

134

483798

                        if bits.len() < 2 || bits.len() > 33 {

135

                            return None;

136

483798

137

483798

                        let sign = bits.last()?;

138

483798

                        for (index, magnitude) in bits[..bits.len() - 1].iter().enumerate() {

139

1185576

                            let weight = scale.checked_mul(1i128 << index)?;

140

1185576

                            self.terms.push((weight, magnitude.clone()));

141

                            // x = magnitude - 2*(sign AND magnitude). The compiler

142

                            // reuses RustSAT gates and the selected library PB encoder.

143

1185576

                            let negative = match (sign, magnitude) {

144

                                (Expr::Atomic(_, Atom::Literal(Literal::Bool(false))), _)

145

                                | (_, Expr::Atomic(_, Atom::Literal(Literal::Bool(false)))) => {

146

4900

                                    false.into()

147

148

                                (Expr::Atomic(_, Atom::Literal(Literal::Bool(true))), _) => {

149

420

                                    magnitude.clone()

150

151

                                (_, Expr::Atomic(_, Atom::Literal(Literal::Bool(true)))) => {

152

                                    sign.clone()

153

154

1180256

                                _ => Expr::And(

155

1180256

                                    Metadata::new(),

156

1180256

                                    conjure_cp::ast::Moo::new(conjure_cp::into_matrix_expr!(vec![

157

1180256

                                        sign.clone(),

158

1180256

                                        magnitude.clone()

159

1180256

                                    ])),

160

1180256

),

161

};

162

1185576

                            self.terms.push((weight.checked_mul(-2)?, negative));

163

164

                        // The conjunctions depend on the magnitude bits: this is

165

                        // not an independent bounded-binary input group.

166

483798

                        None

167

168

                    SATIntEncoding::Log => {

169

9626786

                        if bits.is_empty() || bits.len() > 32 {

170

                            return None;

171

9626786

172

9626786

                        for (index, bit) in bits.iter().enumerate() {

173

23218947

                            let weight = scale.checked_mul(1i128 << index)?;

174

23218947

                            self.terms.push((

175

23218947

                                if index + 1 == bits.len() {

176

9626786

                                    weight.checked_neg()?

177

                                } else {

178

13592161

                                    weight

179

},

180

23218947

                                bit.clone(),

181

));

182

183

9626786

                        binary_structure(scale, i128::from(*low), i128::from(*high))

184

185

};

186

14285595

                if self.terms.len() > start

187

14277755

                    && let Some(structure) = structure

188

189

13793957

                    self.groups.push(PbTermGroup {

190

13793957

                        start,

191

13793957

                        end: self.terms.len(),

192

13793957

                        structure,

193

13793957

});

194

491638

195

196

14718186

            _ => return None,

197

198

22059402

        Some(())

199

49209704

200

201

/// Extract an actual-value view without folding representation bounds to constants.

202

3466175

pub(super) fn integer_view(

203

3466175

    expression: &Expr,

204

3466175

) -> Option<conjure_cp::ast::sat_decision::SatIntegerView> {

205

    use conjure_cp::ast::{Moo, sat_decision::SatIntegerView};

206

3466175

    if expression

207

3466175

        .domain_of()

208

3466161

        .is_some_and(|domain| domain.is_bool())

209

91175

        && crate::shared::utils::is_literal(expression)

210

211

91154

        return Some(SatIntegerView {

212

91154

            constant: 0,

213

91154

            terms: vec![(1, expression.clone())],

214

91154

            groups: vec![],

215

91154

            choices: Some(vec![

216

91154

                (0, Expr::Not(Metadata::new(), Moo::new(expression.clone()))),

217

91154

                (1, expression.clone()),

218

91154

]),

219

91154

});

220

3375021

221

3375021

    let mut linear = Linear::default();

222

3375021

    linear.add(expression, 1)?;

223

2072451

    let constant = i64::try_from(linear.constant).ok()?;

224

2072451

    let terms = linear

225

2072451

        .terms

226

2072451

        .into_iter()

227

8036334

        .map(|(weight, input)| i64::try_from(weight).ok().map(|weight| (weight, input)))

228

        .collect::<Option<Vec<_>>>()?;

229

    // Literal code bits establish the actual value; singleton bounds alone do not.

230

2072451

    if terms

231

2072451

        .iter()

232

1732258

        .all(|(_, input)| matches!(input, Expr::Atomic(_, Atom::Literal(Literal::Bool(_)))))

233

234

456344

        let value = terms

235

456344

            .iter()

236

456344

            .try_fold(i128::from(constant), |value, (weight, input)| {

237

116151

                let Expr::Atomic(_, Atom::Literal(Literal::Bool(bit))) = input else {

238

                    unreachable!()

239

};

240

116151

                value.checked_add(i128::from(*weight) * i128::from(*bit))

241

116151

})

242

456344

            .and_then(|value| i64::try_from(value).ok())?;

243

456344

        return Some(SatIntegerView {

244

456344

            constant: value,

245

456344

            terms: vec![],

246

456344

            groups: vec![],

247

456344

            choices: Some(vec![(value, true.into())]),

248

456344

});

249

1616107

250

1616107

    let choices = if terms.is_empty() {

251

        Some(vec![(constant, true.into())])

252

1616107

    } else if linear.groups.len() == 1

253

1458299

        && linear.groups[0].start == 0

254

1458299

        && linear.groups[0].end == terms.len()

255

1458299

        && linear.groups[0].structure == PbTermStructure::Choice

256

257

        Some(

258

818685

            terms

259

818685

                .iter()

260

5069295

                .map(|(weight, input)| {

261

5069295

                    constant

262

5069295

                        .checked_add(*weight)

263

5069295

                        .map(|value| (value, input.clone()))

264

5069295

})

265

                .collect::<Option<Vec<_>>>()?,

266

267

    } else {

268

797422

        None

269

};

270

1616107

    Some(SatIntegerView {

271

1616107

        constant,

272

1616107

        terms,

273

1616107

        groups: linear.groups,

274

1616107

        choices,

275

1616107

})

276

3466175

277

278

10662186

fn binary_structure(scale: i128, low: i128, high: i128) -> Option<PbTermStructure> {

279

10662186

    let a = scale.checked_mul(low)?;

280

10662186

    let b = scale.checked_mul(high)?;

281

    Some(PbTermStructure::BoundedBinary {

282

10662186

        lower: i64::try_from(a.min(b)).ok()?,

283

10662186

        upper: i64::try_from(a.max(b)).ok()?,

284

})

285

10662186

286

3717868

fn constant_int(expression: &Expr) -> Option<i32> {

287

3717868

    match expression {

288

1462517

        Expr::Atomic(_, Atom::Literal(Literal::Int(value))) => Some(*value),

289

        Expr::SATInt(..) => {

290

            // Inspect literal code bits: singleton bounds alone do not make a value constant.

291

731101

            let view = integer_view(expression)?;

292

642166

            view.terms

293

642166

                .is_empty()

294

98021

                .then(|| i32::try_from(view.constant).ok())

295

                .flatten()

296

297

1524250

        _ => None,

298

299

3717868

300

13663601

fn has_linear_operation(expression: &Expr) -> bool {

301

13663601

    matches!(

302

13663601

        expression,

303

        Expr::Sum(..) | Expr::Product(..) | Expr::Minus(..) | Expr::Neg(..) | Expr::ToInt(..)

304

305

13663601

306

307

/// Preserve products of Boolean indicators as an indicator of their conjunction.

308

#[register_rule("SAT", 18900, [Product])]

309

966323

fn product_boolean_indicators(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

310

966323

    let Expr::Product(_, factors) = expr else {

311

21

        return Err(RuleNotApplicable);

312

};

313

966302

    let inputs = super::boolean::count_inputs(factors).ok_or(RuleNotApplicable)?;

314

15344

    Ok(RuleEffect::pure(Expr::ToInt(

315

15344

        Metadata::new(),

316

15344

        conjure_cp::ast::Moo::new(Expr::And(

317

15344

            Metadata::new(),

318

15344

            conjure_cp::ast::Moo::new(conjure_cp::into_matrix_expr!(inputs)),

319

15344

)),

320

15344

)))

321

966323

322

323

/// Extract ready, asserted linear comparisons before integer circuits consume them.

324

#[register_rule("SAT", 19000, [Root])]

325

7134034

fn select_pseudo_boolean(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

326

71683978

    super::asserted::select_asserted(expr, symbols, |child| {

327

71683978

        let (left, right, relation, strict) = match child {

328

2306912

            Expr::Leq(_, left, right) => (left, right, CardinalityRelation::AtMost, false),

329

115983

            Expr::Lt(_, left, right) => (left, right, CardinalityRelation::AtMost, true),

330

824939

            Expr::Geq(_, left, right) => (left, right, CardinalityRelation::AtLeast, false),

331

13825

            Expr::Gt(_, left, right) => (left, right, CardinalityRelation::AtLeast, true),

332

5597248

            Expr::Eq(_, left, right) => (left, right, CardinalityRelation::Exactly, false),

333

62825071

            _ => return None,

334

};

335

8858907

        if !has_linear_operation(left) && !has_linear_operation(right) {

336

4258351

            return None;

337

4600556

338

4600556

        let mut linear = Linear::default();

339

4600556

        linear.add(left, 1)?;

340

505465

        linear.add(right, -1)?;

341

55120

        let mut bound = linear.constant.checked_neg()?;

342

55120

        if strict {

343

987

            bound = bound.checked_add(if relation == CardinalityRelation::AtMost {

344

980

-1

345

            } else {

346

7

347

            })?;

348

54133

349

55120

        let bound = i64::try_from(bound).ok()?;

350

55120

        let terms = linear

351

55120

            .terms

352

55120

            .into_iter()

353

617392

            .map(|(weight, input)| i64::try_from(weight).map(|weight| (weight, input)))

354

            .collect::<Result<Vec<_>, _>>()

355

            .ok()?;

356

55120

        Some(SatEncodingDecision::PseudoBoolean {

357

55120

            terms,

358

55120

            groups: linear.groups,

359

55120

            relation,

360

55120

            bound,

361

55120

            encoding: None,

362

55120

})

363

71683978

})

364

7134034

365

257164140

fn ready_count_comparison(expr: &Expr) -> bool {

366

257164140

    let (left, right) = match expr {

367

        Expr::Eq(_, left, right)

368

        | Expr::Neq(_, left, right)

369

        | Expr::Lt(_, left, right)

370

        | Expr::Leq(_, left, right)

371

        | Expr::Gt(_, left, right)

372

57261590

        | Expr::Geq(_, left, right) => (left, right),

373

199902550

        _ => return false,

374

};

375

113833463

    let count = |expression: &Expr| {

376

113833463

        matches!(expression, Expr::Sum(_, inputs)

377

6742517

        if super::boolean::count_inputs(inputs).is_some())

378

113833463

};

379

57261590

    (count(left) && constant_int(right).is_some()) || (count(right) && constant_int(left).is_some())

380

257164140

381

382

/// Reify Boolean counts within ready Boolean contexts using cardinality and AMO providers.

383

#[register_rule("SAT", 18600, [Root])]

384

7078389

fn select_guarded_count(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

385

7078389

    if !matches!(expr, Expr::Root(..)) {

386

21

        return Err(RuleNotApplicable);

387

7078368

388

7078368

    guarded_count(expr, true, symbols).ok_or(RuleNotApplicable)

389

7078389

390

391

300647446

fn guarded_count(expr: &Expr, asserted: bool, symbols: &SymbolTable) -> Option<RuleEffect> {

392

300647446

    if !asserted && ready_count_comparison(expr) {

393

108136

        return count_relation(expr, symbols).ok();

394

300539310

395

    // Only traverse Boolean contexts and literal matrices, never a binder or undefined value.

396

300539310

    match expr {

397

7078368

        Expr::Root(_, entries) => guarded_children(expr, entries.iter(), true, symbols),

398

        Expr::AbstractLiteral(_, Matrix(entries, _)) => {

399

44264966

            guarded_children(expr, entries.iter(), asserted, symbols)

400

401

        Expr::And(_, entries)

402

14023577

            if matches!(entries.as_ref(), Expr::AbstractLiteral(_, Matrix(..))) =>

403

404

13087887

            guarded_children(expr, std::iter::once(entries.as_ref()), asserted, symbols)

405

406

        Expr::Or(_, entries)

407

31383033

            if matches!(entries.as_ref(), Expr::AbstractLiteral(_, Matrix(..))) =>

408

409

31177079

            guarded_children(expr, std::iter::once(entries.as_ref()), false, symbols)

410

411

        Expr::Not(_, child) | Expr::ToInt(_, child) => {

412

16362764

            guarded_children(expr, std::iter::once(child.as_ref()), false, symbols)

413

414

        Expr::Imply(_, left, right)

415

        | Expr::Iff(_, left, right)

416

        | Expr::Eq(_, left, right)

417

        | Expr::Neq(_, left, right)

418

        | Expr::Lt(_, left, right)

419

        | Expr::Leq(_, left, right)

420

        | Expr::Gt(_, left, right)

421

34417155

        | Expr::Geq(_, left, right) => guarded_children(

422

34417155

            expr,

423

34417155

            [left.as_ref(), right.as_ref()].into_iter(),

424

34417155

            false,

425

34417155

            symbols,

426

34417155

),

427

154151091

        _ => None,

428

429

300647446

430

431

146388219

fn guarded_children<'a>(

432

146388219

    expr: &Expr,

433

146388219

    children: impl Iterator<Item = &'a Expr>,

434

146388219

    asserted: bool,

435

146388219

    symbols: &SymbolTable,

436

146388219

) -> Option<RuleEffect> {

437

    use uniplate::Uniplate;

438

146388219

    for (index, child) in children.enumerate() {

439

293569078

        if let Some(mut effect) = guarded_count(child, asserted, symbols) {

440

415324

            let mut replacements = expr.children();

441

415324

            replacements[index] = effect.new_expression;

442

415324

            effect.new_expression = expr.with_children(replacements);

443

415324

            return Some(effect);

444

293153754

445

446

145972895

    None

447

146388219

448

449

/// Preserve numeric equality and comparison, including nested Boolean uses, for library encoding.

450

#[register_rule("SAT", 18500, [Eq, Neq, Lt, Leq, Gt, Geq])]

451

18696890

fn select_integer_relation(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

452

    // Root chooses asserted bounds; disequality and guarded counts require equivalence decisions.

453

18696890

    if ready_count_comparison(expr) && !matches!(expr, Expr::Neq(..)) {

454

634816

        return Err(RuleNotApplicable);

455

18062074

456

18062074

    if ready_count_comparison(expr) {

457

5740

        return count_relation(expr, symbols);

458

18056334

459

18056334

    integer_relation(expr, symbols)

460

18696890

461

462

113876

fn count_relation(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

463

    use conjure_cp::ast::sat_decision::IntegerRelation;

464

113876

    let (left, right, mut relation) = match expr {

465

11648

        Expr::Eq(_, left, right) => (left, right, IntegerRelation::Equal),

466

9646

        Expr::Neq(_, left, right) => (left, right, IntegerRelation::NotEqual),

467

33894

        Expr::Lt(_, left, right) => (left, right, IntegerRelation::Less),

468

46970

        Expr::Leq(_, left, right) => (left, right, IntegerRelation::LessEqual),

469

3906

        Expr::Gt(_, left, right) => (left, right, IntegerRelation::Greater),

470

7812

        Expr::Geq(_, left, right) => (left, right, IntegerRelation::GreaterEqual),

471

        _ => return Err(RuleNotApplicable),

472

};

473

113876

    let (sum, bound) = if let Expr::Sum(_, sum) = left.as_ref() {

474

49994

        (sum, constant_int(right).ok_or(RuleNotApplicable)?)

475

63882

    } else if let Expr::Sum(_, sum) = right.as_ref() {

476

63882

        relation = match relation {

477

29988

            IntegerRelation::Less => IntegerRelation::Greater,

478

29988

            IntegerRelation::LessEqual => IntegerRelation::GreaterEqual,

479

            IntegerRelation::Greater => IntegerRelation::Less,

480

3906

            IntegerRelation::GreaterEqual => IntegerRelation::LessEqual,

481

            other => other,

482

};

483

63882

        (sum, constant_int(left).ok_or(RuleNotApplicable)?)

484

    } else {

485

        return Err(RuleNotApplicable);

486

};

487

113876

    let inputs = super::boolean::count_inputs(sum).ok_or(RuleNotApplicable)?;

488

113876

    let bound = i64::from(bound);

489

113876

    let mut symbols = symbols.clone();

490

113876

    let output = super::boolean::create_bool_aux(&mut symbols);

491

113876

    Ok(RuleEffect::sat(

492

113876

        output.clone(),

493

113876

        vec![SatEncodingDecision::CountRelation {

494

113876

            output,

495

113876

            inputs,

496

113876

            relation,

497

113876

            bound,

498

113876

            encoding: None,

499

113876

            amo_encoding: None,

500

113876

}],

501

113876

        symbols,

502

113876

))

503

113876

504

505

18056334

fn integer_relation(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

506

    use conjure_cp::ast::sat_decision::IntegerRelation;

507

18056334

    let (left, right, relation) = match expr {

508

11161778

        Expr::Eq(_, left, right) => (left, right, IntegerRelation::Equal),

509

903457

        Expr::Neq(_, left, right) => (left, right, IntegerRelation::NotEqual),

510

2116333

        Expr::Lt(_, left, right) => (left, right, IntegerRelation::Less),

511

2751038

        Expr::Leq(_, left, right) => (left, right, IntegerRelation::LessEqual),

512

230888

        Expr::Gt(_, left, right) => (left, right, IntegerRelation::Greater),

513

892819

        Expr::Geq(_, left, right) => (left, right, IntegerRelation::GreaterEqual),

514

21

        _ => return Err(RuleNotApplicable),

515

};

516

    // Boolean equality stays in the Boolean family. Ready SATInt views are already numeric.

517

18056313

    if !matches!(left.as_ref(), Expr::SATInt(..))

518

16692095

        && !left.domain_of().is_some_and(|domain| domain.is_int())

519

520

1961672

        return Err(RuleNotApplicable);

521

16094641

522

16094641

    let mut linear = Linear::default();

523

16094641

    linear.add(left, 1).ok_or(RuleNotApplicable)?;

524

3744670

    linear.add(right, -1).ok_or(RuleNotApplicable)?;

525

2142132

    let bound = linear

526

2142132

        .constant

527

2142132

        .checked_neg()

528

2142132

        .and_then(|n| i64::try_from(n).ok())

529

2142132

        .ok_or(RuleNotApplicable)?;

530

2142132

    let terms = linear

531

2142132

        .terms

532

2142132

        .into_iter()

533

12203594

        .map(|(weight, input)| i64::try_from(weight).map(|weight| (weight, input)))

534

        .collect::<Result<Vec<_>, _>>()

535

        .map_err(|_| RuleNotApplicable)?;

536

2142132

    let mut symbols = symbols.clone();

537

2142132

    let output = super::boolean::create_bool_aux(&mut symbols);

538

2142132

    Ok(RuleEffect::sat(

539

2142132

        output.clone(),

540

2142132

        vec![SatEncodingDecision::IntegerRelation {

541

2142132

            output,

542

2142132

            terms,

543

2142132

            groups: linear.groups,

544

2142132

            relation,

545

2142132

            bound,

546

2142132

            encoding: None,

547

2142132

}],

548

2142132

        symbols,

549

2142132

))

550

18056334

551

552

/// Preserve the objective's actual-value view and shared PB choice for solve-time tightening.

553

#[register_rule("SAT", 18400, [SatObjective])]

554

23806

fn select_sat_objective(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

555

23806

    let Expr::SatObjective(_, minimise, value) = expr else {

556

21

        return Err(RuleNotApplicable);

557

};

558

23785

    let value = integer_view(value).ok_or(RuleNotApplicable)?;

559

4980

    Ok(RuleEffect::sat(

560

4980

        true.into(),

561

4980

        vec![SatEncodingDecision::Objective {

562

4980

            minimise: *minimise,

563

4980

            value,

564

4980

            encoding: None,

565

4980

}],

566

4980

        symbols.clone(),

567

4980

))

568

23806