Grcov report - operations.rs

1

use conjure_cp::ast::Expression as Expr;

2

use conjure_cp::ast::{SATIntEncoding, SymbolTable};

3

use conjure_cp::rule_engine::{

4

    ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect, register_rule,

5

};

6

7

use conjure_cp::ast::AbstractLiteral::Matrix;

8

use conjure_cp::ast::Metadata;

9

use conjure_cp::ast::Moo;

10

use conjure_cp::into_matrix_expr;

11

12

use itertools::Itertools;

13

14

use super::materialise::{bit_magnitude, match_bits_length, validate_log_int_operands};

15

use crate::backends::sat::boolean::{

16

    tseytin_and, tseytin_iff, tseytin_imply, tseytin_mux, tseytin_not, tseytin_or, tseytin_xor,

17

};

18

19

use conjure_cp::ast::SatEncodingDecision;

20

21

use std::cmp;

22

23

// Creates a boolean expression for > or >=

24

// a > b or a >= b

25

// This can also be used for < and <= by reversing the order of the inputs

26

// Returns result, new symbol table, new decisions

27

10780

fn inequality_boolean(

28

10780

    a: Vec<Expr>,

29

10780

    b: Vec<Expr>,

30

10780

    strict: bool,

31

10780

    decisions: &mut Vec<SatEncodingDecision>,

32

10780

    symbols: &mut SymbolTable,

33

10780

) -> Expr {

34

    let mut notb;

35

    let mut output;

36

37

10780

    if strict {

38

10780

        notb = tseytin_not(b[0].clone(), decisions, symbols);

39

10780

        output = tseytin_and(&[a[0].clone(), notb], decisions, symbols);

40

    } else {

41

        output = tseytin_imply(b[0].clone(), a[0].clone(), decisions, symbols);

42

43

44

    //TODO: There may be room for simplification, and constant optimisation

45

46

10780

    let bit_count = a.len();

47

48

    let mut lhs;

49

    let mut rhs;

50

    let mut iff;

51

10780

    for n in 1..(bit_count - 1) {

52

17640

        notb = tseytin_not(b[n].clone(), decisions, symbols);

53

17640

        lhs = tseytin_and(&[a[n].clone(), notb.clone()], decisions, symbols);

54

17640

        iff = tseytin_iff(a[n].clone(), b[n].clone(), decisions, symbols);

55

17640

        rhs = tseytin_and(&[iff.clone(), output.clone()], decisions, symbols);

56

17640

        output = tseytin_or(&[lhs.clone(), rhs.clone()], decisions, symbols);

57

58

59

    // final bool is the sign bit and should be handled inversely

60

10780

    let nota = tseytin_not(a[bit_count - 1].clone(), decisions, symbols);

61

10780

    lhs = tseytin_and(&[nota, b[bit_count - 1].clone()], decisions, symbols);

62

10780

    iff = tseytin_iff(

63

10780

        a[bit_count - 1].clone(),

64

10780

        b[bit_count - 1].clone(),

65

10780

        decisions,

66

10780

        symbols,

67

10780

);

68

10780

    rhs = tseytin_and(&[iff, output.clone()], decisions, symbols);

69

10780

    output = tseytin_or(&[lhs, rhs], decisions, symbols);

70

71

10780

    output

72

10780

73

74

/// Returns result, new symbol table, new decisions

75

/// This function expects bits to match the lengths of x and y

76

1604358

fn tseytin_int_adder(

77

1604358

    x: &[Expr],

78

1604358

    y: &[Expr],

79

1604358

    bits: usize,

80

1604358

    decisions: &mut Vec<SatEncodingDecision>,

81

1604358

    symbols: &mut SymbolTable,

82

1604358

) -> Vec<Expr> {

83

    //TODO: Optimizing for constants

84

    let (mut result, mut carry) =

85

1604358

        tseytin_half_adder(x[0].clone(), y[0].clone(), decisions, symbols);

86

87

1604358

    let mut output = vec![result];

88

1604358

    for i in 1..bits {

89

16361520

        (result, carry) = tseytin_full_adder(

90

16361520

            x[i].clone(),

91

16361520

            y[i].clone(),

92

16361520

            carry.clone(),

93

16361520

            decisions,

94

16361520

            symbols,

95

16361520

);

96

16361520

        output.push(result);

97

98

99

1604358

    output

100

1604358

101

102

/// This function adds two booleans and a carry boolean using the full-adder logic circuit, it is intended for use in a binary adder.

103

16361520

fn tseytin_full_adder(

104

16361520

    a: Expr,

105

16361520

    b: Expr,

106

16361520

    carry: Expr,

107

16361520

    decisions: &mut Vec<SatEncodingDecision>,

108

16361520

    symbols: &mut SymbolTable,

109

16361520

) -> (Expr, Expr) {

110

16361520

    let axorb = tseytin_xor(a.clone(), b.clone(), decisions, symbols);

111

16361520

    let result = tseytin_xor(axorb.clone(), carry.clone(), decisions, symbols);

112

16361520

    let aandb = tseytin_and(&[a, b], decisions, symbols);

113

16361520

    let carryandaxorb = tseytin_and(&[carry, axorb], decisions, symbols);

114

16361520

    let carryout = tseytin_or(&[aandb, carryandaxorb], decisions, symbols);

115

116

16361520

    (result, carryout)

117

16361520

118

119

/// This function adds two booleans using the half-adder logic circuit, it is intended for use in a binary adder.

120

1604358

fn tseytin_half_adder(

121

1604358

    a: Expr,

122

1604358

    b: Expr,

123

1604358

    decisions: &mut Vec<SatEncodingDecision>,

124

1604358

    symbols: &mut SymbolTable,

125

1604358

) -> (Expr, Expr) {

126

1604358

    let result = tseytin_xor(a.clone(), b.clone(), decisions, symbols);

127

1604358

    let carry = tseytin_and(&[a, b], decisions, symbols);

128

129

1604358

    (result, carry)

130

1604358

131

132

/// this function is for specifically adding a power of two constant to a cnf int.

133

981904

fn tseytin_add_two_power(

134

981904

    expr: &[Expr],

135

981904

    exponent: usize,

136

981904

    bits: usize,

137

981904

    decisions: &mut Vec<SatEncodingDecision>,

138

981904

    symbols: &mut SymbolTable,

139

981904

) -> Vec<Expr> {

140

981904

    let mut result = vec![];

141

981904

    let mut product = expr[exponent].clone();

142

143

981904

    for item in expr.iter().take(exponent) {

144

        result.push(item.clone());

145

146

147

981904

    result.push(tseytin_not(expr[exponent].clone(), decisions, symbols));

148

149

981904

    for item in expr.iter().take(bits).skip(exponent + 1) {

150

5038068

        result.push(tseytin_xor(

151

5038068

            product.clone(),

152

5038068

            item.clone(),

153

5038068

            decisions,

154

5038068

            symbols,

155

5038068

));

156

5038068

        product = tseytin_and(&[product, item.clone()], decisions, symbols);

157

158

159

981904

    result

160

981904

161

162

/// This function multiplies two binary values using the shift-add multiplication algorithm.

163

36162

fn cnf_shift_add_multiply(

164

36162

    x: &[Expr],

165

36162

    y: &[Expr],

166

36162

    bits: usize,

167

36162

    decisions: &mut Vec<SatEncodingDecision>,

168

36162

    symbols: &mut SymbolTable,

169

36162

) -> Vec<Expr> {

170

36162

    let mut x = x.to_owned();

171

36162

    let mut y = y.to_owned();

172

173

    //TODO Optimizing for constants

174

    //TODO Optimize addition for i left shifted values - skip first i bits

175

176

    // extend sign bits of operands to 2*`bits`

177

36162

    x.extend(std::iter::repeat_n(x[bits - 1].clone(), bits));

178

36162

    y.extend(std::iter::repeat_n(y[bits - 1].clone(), bits));

179

180

36162

    let mut s: Vec<Expr> = vec![];

181

    let mut x_0andy_i;

182

183

36162

    for bit in &y {

184

383964

        x_0andy_i = tseytin_and(&[x[0].clone(), bit.clone()], decisions, symbols);

185

383964

        s.push(x_0andy_i);

186

187

188

    let mut sum;

189

    let mut if_true;

190

    let mut not_x_n;

191

    let mut if_false;

192

193

    // Include the extended sign bits in the full-width modular product.

194

36162

    for item in x.iter().take(bits * 2).skip(1) {

195

        // y << 1

196

347802

        for i in (1..bits * 2).rev() {

197

5418938

            y[i] = y[i - 1].clone();

198

199

347802

        y[0] = false.into();

200

201

        // TODO switch to multiplexer

202

347802

        sum = tseytin_int_adder(&s, &y, bits * 2, decisions, symbols);

203

347802

        not_x_n = tseytin_not(item.clone(), decisions, symbols);

204

205

347802

        for i in 0..(bits * 2) {

206

5766740

            if_true = tseytin_and(&[item.clone(), sum[i].clone()], decisions, symbols);

207

5766740

            if_false = tseytin_and(&[not_x_n.clone(), s[i].clone()], decisions, symbols);

208

5766740

            s[i] = tseytin_or(&[if_true.clone(), if_false.clone()], decisions, symbols);

209

210

211

212

36162

213

36162

214

215

/// This function calculates the range of the product of multiple integers.

216

/// E.g.

217

/// a : [2, 5], b : [-1, 2], c : [-10, -6], d : [0, 3]

218

/// a * b * c *d : [-300, 150]

219

53228

fn product_of_ranges(ranges: Vec<&(i32, i32)>) -> (i32, i32) {

220

53228

    if ranges.is_empty() {

221

        return (1, 1); // product of zero numbers = 1

222

53228

223

224

53228

    let &(mut min_prod, mut max_prod) = ranges[0];

225

226

53228

    for &(a, b) in &ranges[1..] {

227

55118

        let candidates = [min_prod * a, min_prod * b, max_prod * a, max_prod * b];

228

55118

        min_prod = *candidates.iter().min().unwrap();

229

55118

        max_prod = *candidates.iter().max().unwrap();

230

231

232

53228

    (min_prod, max_prod)

233

53228

234

235

/// Converts product of SATInts to a single SATInt

236

///

237

/// ```text

238

/// Product(SATInt(a), SATInt(b), ...) ~> SATInt(c)

239

///

240

/// ```

241

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

242

151053

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

243

    // Constant scaling belongs to the selected linear encoder, not multiplication circuits.

244

151053

    if crate::backends::sat::pseudo_boolean::integer_view(expr).is_some() {

245

33929

        return Err(RuleNotApplicable);

246

117124

247

117124

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

248

21

        return Err(RuleNotApplicable);

249

};

250

251

117103

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

252

7

        return Err(RuleNotApplicable);

253

};

254

255

117096

    let ranges: Result<Vec<_>, _> = exprs_list

256

117096

        .iter()

257

211659

        .map(|e| match e {

258

147791

            Expr::SATInt(_, _, _, x) => Ok(x),

259

63868

            _ => Err(RuleNotApplicable),

260

211659

})

261

        .collect();

262

263

117096

    let ranges = ranges?; // propagate error if any

264

265

53228

    let (min, max) = product_of_ranges(ranges.clone());

266

267

53228

    let exprs_bits = validate_log_int_operands(exprs_list.clone(), None)?;

268

269

23436

    let mut new_symbols = symbols.clone();

270

23436

    let mut new_sat_decisions = vec![];

271

272

23436

    let (result, _) = exprs_bits

273

23436

        .iter()

274

23436

        .cloned()

275

23436

        .zip(ranges.into_iter().copied())

276

24430

        .reduce(|lhs, rhs| {

277

            // Make both bit vectors the same length

278

24430

            let (lhs_bits, rhs_bits) = match_bits_length(lhs.0.clone(), rhs.0.clone());

279

280

            // Multiply operands

281

24430

            let mut values = cnf_shift_add_multiply(

282

24430

                &lhs_bits,

283

24430

                &rhs_bits,

284

24430

                lhs_bits.len(),

285

24430

                &mut new_sat_decisions,

286

24430

                &mut new_symbols,

287

24430

);

288

289

            // Determine new range of result

290

24430

            let (mut cum_min, mut cum_max) = lhs.1;

291

24430

            let candidates = [

292

24430

                cum_min * rhs.1.0,

293

24430

                cum_min * rhs.1.1,

294

24430

                cum_max * rhs.1.0,

295

24430

                cum_max * rhs.1.1,

296

24430

];

297

24430

            cum_min = *candidates.iter().min().unwrap();

298

24430

            cum_max = *candidates.iter().max().unwrap();

299

300

24430

            let new_bit_count = bit_magnitude(cum_min).max(bit_magnitude(cum_max));

301

24430

            values.truncate(new_bit_count);

302

303

24430

            (values, (cum_min, cum_max))

304

24430

})

305

        .unwrap();

306

307

23436

    Ok(RuleEffect::sat(

308

23436

        Expr::SATInt(

309

23436

            Metadata::new(),

310

23436

            SATIntEncoding::Log,

311

23436

            Moo::new(into_matrix_expr!(result)),

312

23436

            (min, max),

313

23436

),

314

23436

        new_sat_decisions,

315

23436

        new_symbols,

316

23436

))

317

151053

318

319

979447

fn tseytin_negate(

320

979447

    expr: &Vec<Expr>,

321

979447

    bits: usize,

322

979447

    decisions: &mut Vec<SatEncodingDecision>,

323

979447

    symbols: &mut SymbolTable,

324

979447

) -> Vec<Expr> {

325

979447

    let mut result = vec![];

326

    // invert bits

327

979447

    for bit in expr {

328

6010270

        result.push(tseytin_not(bit.clone(), decisions, symbols));

329

330

331

    // add one

332

979447

    result = tseytin_add_two_power(&result, 0, bits, decisions, symbols);

333

334

979447

    result

335

979447

336

337

/// Converts min of SATInts to a single SATInt

338

///

339

/// ```text

340

/// Min(SATInt(a), SATInt(b), ...) ~> SATInt(c)

341

///

342

/// ```

343

#[register_rule("SAT", 4100, [Min])]

344

10871

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

345

10871

    let Expr::Min(_, exprs) = expr else {

346

21

        return Err(RuleNotApplicable);

347

};

348

349

10850

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

350

        return Err(RuleNotApplicable);

351

};

352

353

10850

    let ranges: Result<Vec<_>, _> = exprs_list

354

10850

        .iter()

355

23100

        .map(|e| match e {

356

23100

            Expr::SATInt(_, _, _, x) => Ok(x),

357

            _ => Err(RuleNotApplicable),

358

23100

})

359

        .collect();

360

361

10850

    let ranges = ranges?; // propagate error if any

362

363

    // Is this optimal?

364

23100

    let min = ranges.iter().map(|(a, _)| *a).min().unwrap();

365

23100

    let max = ranges.iter().map(|(_, b)| *b).min().unwrap();

366

367

10850

    let mut exprs_bits = validate_log_int_operands(exprs_list.clone(), None)?;

368

369

5390

    let mut new_symbols = symbols.clone();

370

    let mut values;

371

5390

    let mut new_sat_decisions = vec![];

372

373

11270

    while exprs_bits.len() > 1 {

374

5880

        let mut next = Vec::with_capacity(exprs_bits.len().div_ceil(2));

375

5880

        let mut iter = exprs_bits.into_iter();

376

377

12250

        while let Some(a) = iter.next() {

378

6370

            if let Some(b) = iter.next() {

379

5880

                values =

380

5880

                    tseytin_binary_min_max(&a, &b, true, &mut new_sat_decisions, &mut new_symbols);

381

5880

                next.push(values);

382

            } else {

383

490

                next.push(a);

384

385

386

387

5880

        exprs_bits = next;

388

389

390

5390

    let result = exprs_bits.pop().unwrap();

391

392

5390

    Ok(RuleEffect::sat(

393

5390

        Expr::SATInt(

394

5390

            Metadata::new(),

395

5390

            SATIntEncoding::Log,

396

5390

            Moo::new(into_matrix_expr!(result)),

397

5390

            (min, max),

398

5390

),

399

5390

        new_sat_decisions,

400

5390

        new_symbols,

401

5390

))

402

10871

403

404

/// General function for getting the min or max of two log integers.

405

10780

fn tseytin_binary_min_max(

406

10780

    x: &[Expr],

407

10780

    y: &[Expr],

408

10780

    min: bool,

409

10780

    decisions: &mut Vec<SatEncodingDecision>,

410

10780

    symbols: &mut SymbolTable,

411

10780

) -> Vec<Expr> {

412

10780

    let mask = if min {

413

        // mask is 1 if x > y

414

5880

        inequality_boolean(x.to_owned(), y.to_owned(), true, decisions, symbols)

415

    } else {

416

        // flip the args if getting maximum x < y -> 1

417

4900

        inequality_boolean(y.to_owned(), x.to_owned(), true, decisions, symbols)

418

};

419

420

10780

    tseytin_select_array(mask, x, y, decisions, symbols)

421

10780

422

423

// Selects between two boolean vectors depending on a condition (both vectors must be the same length)

424

/// cond ? b : a

425

///

426

/// cond = 1 => b

427

/// cond = 0 => a

428

990227

fn tseytin_select_array(

429

990227

    cond: Expr,

430

990227

    a: &[Expr],

431

990227

    b: &[Expr],

432

990227

    decisions: &mut Vec<SatEncodingDecision>,

433

990227

    symbols: &mut SymbolTable,

434

990227

) -> Vec<Expr> {

435

990227

    assert_eq!(

436

990227

        a.len(),

437

990227

        b.len(),

438

        "Input vectors 'a' and 'b' must have the same length"

439

);

440

441

990227

    let mut out = vec![];

442

443

990227

    let bit_count = a.len();

444

445

990227

    for i in 0..bit_count {

446

5000044

        out.push(tseytin_mux(

447

5000044

            cond.clone(),

448

5000044

            a[i].clone(),

449

5000044

            b[i].clone(),

450

5000044

            decisions,

451

5000044

            symbols,

452

5000044

));

453

454

455

990227

out

456

990227

457

458

/// Converts max of SATInts to a single SATInt

459

///

460

/// ```text

461

/// Max(SATInt(a), SATInt(b), ...) ~> SATInt(c)

462

///

463

/// ```

464

#[register_rule("SAT", 4100, [Max])]

465

9436

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

466

9436

    let Expr::Max(_, exprs) = expr else {

467

21

        return Err(RuleNotApplicable);

468

};

469

470

9415

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

471

        return Err(RuleNotApplicable);

472

};

473

474

9415

    let ranges: Result<Vec<_>, _> = exprs_list

475

9415

        .iter()

476

19775

        .map(|e| match e {

477

19775

            Expr::SATInt(_, _, _, x) => Ok(x),

478

            _ => Err(RuleNotApplicable),

479

19775

})

480

        .collect();

481

482

9415

    let ranges = ranges?; // propagate error if any

483

484

    // Is this optimal?

485

19775

    let min = ranges.iter().map(|(a, _)| *a).max().unwrap();

486

19775

    let max = ranges.iter().map(|(_, b)| *b).max().unwrap();

487

488

9415

    let mut exprs_bits = validate_log_int_operands(exprs_list.clone(), None)?;

489

490

4410

    let mut new_symbols = symbols.clone();

491

    let mut values;

492

4410

    let mut new_sat_decisions = vec![];

493

494

9310

    while exprs_bits.len() > 1 {

495

4900

        let mut next = Vec::with_capacity(exprs_bits.len().div_ceil(2));

496

4900

        let mut iter = exprs_bits.into_iter();

497

498

10290

        while let Some(a) = iter.next() {

499

5390

            if let Some(b) = iter.next() {

500

4900

                values =

501

4900

                    tseytin_binary_min_max(&a, &b, false, &mut new_sat_decisions, &mut new_symbols);

502

4900

                next.push(values);

503

            } else {

504

490

                next.push(a);

505

506

507

508

4900

        exprs_bits = next;

509

510

511

4410

    let result = exprs_bits.pop().unwrap();

512

513

4410

    Ok(RuleEffect::sat(

514

4410

        Expr::SATInt(

515

4410

            Metadata::new(),

516

4410

            SATIntEncoding::Log,

517

4410

            Moo::new(into_matrix_expr!(result)),

518

4410

            (min, max),

519

4410

),

520

4410

        new_sat_decisions,

521

4410

        new_symbols,

522

4410

))

523

9436

524

525

/// Converts Abs of a SATInt to a SATInt

526

///

527

/// ```text

528

/// |SATInt(a)| ~> SATInt(b)

529

///

530

/// ```

531

#[register_rule("SAT", 4100, [Abs])]

532

5775

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

533

5775

    let Expr::Abs(_, expr) = expr else {

534

21

        return Err(RuleNotApplicable);

535

};

536

537

5754

    let Expr::SATInt(_, _, _, (min, max)) = expr.as_ref() else {

538

630

        return Err(RuleNotApplicable);

539

};

540

541

5124

    let range = (

542

5124

        cmp::max(0, cmp::max(*min, -*max)),

543

5124

        cmp::max(min.abs(), max.abs()),

544

5124

);

545

546

5124

    let binding = validate_log_int_operands(vec![expr.as_ref().clone()], None)?;

547

2457

    let [bits] = binding.as_slice() else {

548

        return Err(RuleNotApplicable);

549

};

550

551

2457

    let mut new_sat_decisions = vec![];

552

2457

    let mut new_symbols = symbols.clone();

553

554

2457

    let mut result = vec![];

555

556

    // How does this handle negatives edge cases: -(-8) = 8, an extra bit is needed

557

558

    // invert bits

559

2457

    for bit in bits {

560

9702

        result.push(tseytin_not(

561

9702

            bit.clone(),

562

9702

            &mut new_sat_decisions,

563

9702

            &mut new_symbols,

564

9702

));

565

566

567

2457

    let bit_count = result.len();

568

569

    // add one

570

2457

    result = tseytin_add_two_power(

571

2457

        &result,

572

2457

0,

573

2457

        bit_count,

574

2457

        &mut new_sat_decisions,

575

2457

        &mut new_symbols,

576

2457

);

577

578

2457

    for i in 0..bit_count {

579

9702

        result[i] = tseytin_mux(

580

9702

            bits[bit_count - 1].clone(),

581

9702

            bits[i].clone(),

582

9702

            result[i].clone(),

583

9702

            &mut new_sat_decisions,

584

9702

            &mut new_symbols,

585

9702

586

587

588

2457

    Ok(RuleEffect::sat(

589

2457

        Expr::SATInt(

590

2457

            Metadata::new(),

591

2457

            SATIntEncoding::Log,

592

2457

            Moo::new(into_matrix_expr!(result)),

593

2457

            range,

594

2457

),

595

2457

        new_sat_decisions,

596

2457

        new_symbols,

597

2457

))

598

5775

599

600

/// Converts SafeDiv of SATInts to a single SATInt

601

///

602

/// ```text

603

/// SafeDiv(SATInt(a), SATInt(b)) ~> SATInt(c)

604

///

605

/// ```

606

#[register_rule("SAT", 4100, [SafeDiv])]

607

151564

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

608

151564

    let Expr::SafeDiv(_, numer, denom) = expr else {

609

21

        return Err(RuleNotApplicable);

610

};

611

151543

    encode_div_mod(numer, denom, symbols, false)

612

151564

613

614

/// Reuses restoring division's remainder, with Essence's floor-modulo semantics.

615

#[register_rule("SAT", 4100, [SafeMod])]

616

501515

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

617

501515

    let Expr::SafeMod(_, numer, denom) = expr else {

618

21

        return Err(RuleNotApplicable);

619

};

620

501494

    encode_div_mod(numer, denom, symbols, true)

621

501515

622

623

653037

fn encode_div_mod(

624

653037

    numer: &Expr,

625

653037

    denom: &Expr,

626

653037

    symbols: &SymbolTable,

627

653037

    modulo: bool,

628

653037

) -> ApplicationResult {

629

    // Restoring division computes both quotient and remainder magnitudes.

630

631

653037

    let Expr::SATInt(_, _, _, (numer_min, numer_max)) = numer else {

632

126735

        return Err(RuleNotApplicable);

633

};

634

635

526302

    let Expr::SATInt(_, _, _, (denom_min, denom_max)) = denom else {

636

1260

        return Err(RuleNotApplicable);

637

};

638

639

525042

    let (min, max) = if modulo {

640

        // Remainders have the divisor's sign; include the safe zero-divisor dummy.

641

642

375844

            if *denom_min < 0 { denom_min + 1 } else { 0 },

643

375844

            if *denom_max > 0 { denom_max - 1 } else { 0 },

644

645

    } else {

646

149198

        division_bounds((*numer_min, *numer_max), (*denom_min, *denom_max))

647

149198

            .ok_or(RuleNotApplicable)?

648

};

649

650

525042

    let binding = validate_log_int_operands(vec![numer.clone(), denom.clone()], None)?;

651

207130

    let [numer_bits, denom_bits] = binding.as_slice() else {

652

        return Err(RuleNotApplicable);

653

};

654

655

    // Widen before taking absolute values: abs(MIN) needs an additional sign bit.

656

207130

    let mut numer_bits = numer_bits.clone();

657

207130

    let mut denom_bits = denom_bits.clone();

658

207130

    numer_bits.push(numer_bits.last().unwrap().clone());

659

207130

    denom_bits.push(denom_bits.last().unwrap().clone());

660

207130

    let bit_count = numer_bits.len();

661

662

207130

    let mut new_symbols = symbols.clone();

663

207130

    let mut new_sat_decisions = vec![];

664

207130

    let mut quotient = vec![false.into(); bit_count];

665

666

207130

    let minus_numer = tseytin_negate(

667

207130

        &numer_bits.clone(),

668

207130

        bit_count,

669

207130

        &mut new_sat_decisions,

670

207130

        &mut new_symbols,

671

207130

);

672

207130

    let minus_denom = tseytin_negate(

673

207130

        &denom_bits.clone(),

674

207130

        bit_count,

675

207130

        &mut new_sat_decisions,

676

207130

        &mut new_symbols,

677

207130

);

678

679

207130

    let denom_sign = denom_bits[bit_count - 1].clone();

680

207130

    let sign_bit = tseytin_xor(

681

207130

        numer_bits[bit_count - 1].clone(),

682

207130

        denom_bits[bit_count - 1].clone(),

683

207130

        &mut new_sat_decisions,

684

207130

        &mut new_symbols,

685

207130

);

686

687

207130

    let numer_bits = tseytin_select_array(

688

207130

        numer_bits[bit_count - 1].clone(),

689

207130

        &numer_bits.clone(),

690

207130

        &minus_numer,

691

207130

        &mut new_sat_decisions,

692

207130

        &mut new_symbols,

693

207130

);

694

207130

    let denom_bits = tseytin_select_array(

695

207130

        denom_bits[bit_count - 1].clone(),

696

207130

        &denom_bits.clone(),

697

207130

        &minus_denom,

698

207130

        &mut new_sat_decisions,

699

207130

        &mut new_symbols,

700

207130

);

701

702

207130

    let mut r = numer_bits;

703

207130

    r.extend(std::iter::repeat_n(r[bit_count - 1].clone(), bit_count));

704

207130

    let mut d = std::iter::repeat_n(false.into(), bit_count).collect_vec();

705

207130

    d.extend(denom_bits.clone());

706

707

207130

    let minus_d = tseytin_negate(

708

207130

        &d.clone(),

709

207130

        2 * bit_count,

710

207130

        &mut new_sat_decisions,

711

207130

        &mut new_symbols,

712

207130

);

713

    let mut rminusd;

714

715

207130

    for i in (0..bit_count).rev() {

716

        // r << 1

717

1049426

        for j in (1..bit_count * 2).rev() {

718

10100286

            r[j] = r[j - 1].clone();

719

720

1049426

        r[0] = false.into();

721

722

1049426

        rminusd = tseytin_int_adder(

723

1049426

            &r.clone(),

724

1049426

            &minus_d.clone(),

725

1049426

            2 * bit_count,

726

1049426

            &mut new_sat_decisions,

727

1049426

            &mut new_symbols,

728

1049426

);

729

730

1049426

        quotient[i] = tseytin_not(

731

            // q[i] = inverse of sign bit - 1 if positive, 0 if negative

732

1049426

            rminusd[2 * bit_count - 1].clone(),

733

1049426

            &mut new_sat_decisions,

734

1049426

            &mut new_symbols,

735

1049426

);

736

737

1049426

        for j in 0..(2 * bit_count) {

738

11149712

            r[j] = tseytin_mux(

739

11149712

                quotient[i].clone(),

740

11149712

                r[j].clone(),       // use r if negative

741

11149712

                rminusd[j].clone(), // use r-d if positive

742

11149712

                &mut new_sat_decisions,

743

11149712

                &mut new_symbols,

744

11149712

);

745

746

747

748

    // Opposite signs and a nonzero remainder require one more unit of magnitude

749

    // before negation to obtain floor division rather than truncating division.

750

207130

    let remainder_nonzero = tseytin_or(&r, &mut new_sat_decisions, &mut new_symbols);

751

207130

    let round_down = tseytin_and(

752

207130

        &[sign_bit.clone(), remainder_nonzero],

753

207130

        &mut new_sat_decisions,

754

207130

        &mut new_symbols,

755

207130

);

756

207130

    let out = if modulo {

757

150927

        let remainder = r[bit_count..].to_vec();

758

150927

        let minus_remainder = tseytin_negate(

759

150927

            &remainder,

760

150927

            bit_count,

761

150927

            &mut new_sat_decisions,

762

150927

            &mut new_symbols,

763

150927

);

764

150927

        let complement = tseytin_int_adder(

765

150927

            &denom_bits,

766

150927

            &minus_remainder,

767

150927

            bit_count,

768

150927

            &mut new_sat_decisions,

769

150927

            &mut new_symbols,

770

150927

);

771

150927

        let magnitude = tseytin_select_array(

772

150927

            round_down,

773

150927

            &remainder,

774

150927

            &complement,

775

150927

            &mut new_sat_decisions,

776

150927

            &mut new_symbols,

777

150927

);

778

150927

        let negative = tseytin_negate(

779

150927

            &magnitude,

780

150927

            bit_count,

781

150927

            &mut new_sat_decisions,

782

150927

            &mut new_symbols,

783

150927

);

784

150927

        tseytin_select_array(

785

150927

            denom_sign,

786

150927

            &magnitude,

787

150927

            &negative,

788

150927

            &mut new_sat_decisions,

789

150927

            &mut new_symbols,

790

150927

791

    } else {

792

56203

        let mut correction = vec![false.into(); bit_count];

793

56203

        correction[0] = round_down;

794

56203

        quotient = tseytin_int_adder(

795

56203

            &quotient,

796

56203

            &correction,

797

56203

            bit_count,

798

56203

            &mut new_sat_decisions,

799

56203

            &mut new_symbols,

800

56203

);

801

802

56203

        let minus_quotient = tseytin_negate(

803

56203

            &quotient.clone(),

804

56203

            bit_count,

805

56203

            &mut new_sat_decisions,

806

56203

            &mut new_symbols,

807

56203

);

808

809

56203

        tseytin_select_array(

810

56203

            sign_bit,

811

56203

            &quotient,

812

56203

            &minus_quotient,

813

56203

            &mut new_sat_decisions,

814

56203

            &mut new_symbols,

815

56203

816

};

817

818

    // Safe division and modulo must keep zero-divisor dummy values within their bounds.

819

    // Definedness is handled separately by the bubble rules, including under negation.

820

207130

    let nonzero = tseytin_or(&denom_bits, &mut new_sat_decisions, &mut new_symbols);

821

207130

    let out = tseytin_select_array(

822

207130

        nonzero,

823

207130

        &vec![false.into(); bit_count],

824

207130

        &out,

825

207130

        &mut new_sat_decisions,

826

207130

        &mut new_symbols,

827

207130

);

828

829

207130

    Ok(RuleEffect::sat(

830

207130

        Expr::SATInt(

831

207130

            Metadata::new(),

832

207130

            SATIntEncoding::Log,

833

207130

            Moo::new(into_matrix_expr!(out)),

834

207130

            (min, max),

835

207130

),

836

207130

        new_sat_decisions,

837

207130

        new_symbols,

838

207130

))

839

653037

840

841

// Quotient extrema can occur at the nonzero denominators closest to zero.

842

149198

fn division_bounds(numerator: (i32, i32), denominator: (i32, i32)) -> Option<(i32, i32)> {

843

149198

    let mut values = Vec::new();

844

149198

    for divisor in [denominator.0, denominator.1, -1, 1] {

845

596792

        if divisor == 0 || divisor < denominator.0 || divisor > denominator.1 {

846

240961

            continue;

847

355831

848

355831

        for dividend in [numerator.0, numerator.1] {

849

711662

            values.push(super::super::floor_div(dividend, divisor)?);

850

851

852

149198

    if denominator.0 <= 0 && denominator.1 >= 0 {

853

6755

        values.push(0);

854

142443

855

149198

    Some((*values.iter().min()?, *values.iter().max()?))

856

149198

857

858

/// Lower power using exponentiation by squaring and the existing Boolean circuit decisions.

859

/// Undefined inputs retain a harmless value; their definedness is handled by the bubble rules.

860

#[register_rule("SAT", 4100, [SafePow])]

861

13153

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

862

13153

    let Expr::SafePow(_, base, exponent) = expr else {

863

21

        return Err(RuleNotApplicable);

864

};

865

    let (

866

        Expr::SATInt(_, SATIntEncoding::Log, _, base_bounds),

867

        Expr::SATInt(_, SATIntEncoding::Log, exponent_bits, exponent_bounds),

868

13132

    ) = (base.as_ref(), exponent.as_ref())

869

    else {

870

8701

        return Err(RuleNotApplicable);

871

};

872

    // Endpoints bound both parities; include zero and the unspecified values 0/1.

873

    // Decline machine-overflowing ranges instead of silently wrapping their mathematical powers.

874

4431

    let mut bounds = (0, 1);

875

4431

    if exponent_bounds.1 > 31 && (base_bounds.0 < -1 || base_bounds.1 > 1) {

876

        return Err(RuleNotApplicable);

877

4431

878

4431

    for power in 0..=exponent_bounds.1.clamp(0, 31) {

879

19173

        for value in [base_bounds.0, base_bounds.1] {

880

38346

            let result = value.checked_pow(power as u32).ok_or(RuleNotApplicable)?;

881

38346

            bounds.0 = bounds.0.min(result);

882

38346

            bounds.1 = bounds.1.max(result);

883

884

885

4431

    let width = bit_magnitude(bounds.0).max(bit_magnitude(bounds.1)).max(2);

886

    let mut factor =

887

4431

        validate_log_int_operands(vec![(**base).clone()], Some(width as u32))?.remove(0);

888

4431

    let exponent_bits = exponent_bits.unwrap_list_cow().ok_or(RuleNotApplicable)?;

889

4431

    let mut result = vec![Expr::from(false); width];

890

4431

    result[0] = true.into();

891

4431

    let mut decisions = vec![];

892

4431

    let mut symbols = symbols.clone();

893

4431

    let mut result_is_one = true;

894

    // Only non-sign bits can participate in a defined, non-negative exponent.

895

4431

    for (index, selected) in exponent_bits[..exponent_bits.len() - 1].iter().enumerate() {

896

10682

        let selected_constant = conjure_cp::ast::eval_constant(selected);

897

10682

        if selected_constant != Some(false.into()) {

898

9912

            let mut product = if result_is_one {

899

4431

                factor.clone()

900

            } else {

901

5481

                cnf_shift_add_multiply(&result, &factor, width, &mut decisions, &mut symbols)

902

};

903

9912

            product.truncate(width);

904

9912

            result = if selected_constant == Some(true.into()) {

905

770

                product

906

            } else {

907

9142

                result

908

9142

                    .iter()

909

9142

                    .zip(product)

910

86506

                    .map(|(old, new)| {

911

86506

                        tseytin_mux(

912

86506

                            selected.clone(),

913

86506

                            old.clone(),

914

86506

                            new,

915

86506

                            &mut decisions,

916

86506

                            &mut symbols,

917

86506

918

86506

})

919

                    .collect()

920

};

921

9912

            result_is_one = false;

922

770

923

10682

        if index + 1 < exponent_bits.len() - 1 {

924

6251

            factor = cnf_shift_add_multiply(&factor, &factor, width, &mut decisions, &mut symbols);

925

6251

            factor.truncate(width);

926

4431

927

928

4431

    let negative = exponent_bits.last().ok_or(RuleNotApplicable)?;

929

4431

    if conjure_cp::ast::eval_constant(negative) != Some(false.into()) {

930

2296

        for bit in &mut result {

931

18298

            *bit = tseytin_mux(

932

18298

                negative.clone(),

933

18298

                bit.clone(),

934

18298

                false.into(),

935

18298

                &mut decisions,

936

18298

                &mut symbols,

937

18298

);

938

939

2135

940

4431

    Ok(RuleEffect::sat(

941

4431

        Expr::SATInt(

942

4431

            Metadata::new(),

943

4431

            SATIntEncoding::Log,

944

4431

            Moo::new(into_matrix_expr!(result)),

945

4431

            bounds,

946

4431

),

947

4431

        decisions,

948

4431

        symbols,

949

4431

))

950

13153