Grcov report - partial

1

use std::collections::HashSet;

2

3

use crate::ast::Typeable;

4

use crate::{

5

    ast::{

6

        AbstractLiteral, Atom, DomainPtr, Expression as Expr, GroundDomain, Literal as Lit,

7

        Metadata, Moo, Range, ReturnType,

8

},

9

    into_matrix_expr,

10

    rule_engine::{ApplicationError::RuleNotApplicable, ApplicationResult, Reduction},

11

};

12

use itertools::iproduct;

13

use uniplate::Uniplate;

14

15

/// Normalises integer ranges so equivalent domains compare structurally equal.

16

55392

fn normalise_int_domain(domain: &GroundDomain) -> GroundDomain {

17

55392

    match domain {

18

55392

        GroundDomain::Int(ranges) => GroundDomain::Int(Range::squeeze(

19

55392

            &ranges

20

55392

                .iter()

21

76332

                .map(|range| Range::new(range.low().copied(), range.high().copied()))

22

55392

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

23

)),

24

        _ => domain.clone(),

25

26

55392

27

28

/// Returns whether `expr` is safe after resolving any referenced expressions.

29

5225032

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

30

5237460

    fn helper(expr: &Expr, resolving: &mut HashSet<crate::ast::serde::ObjId>) -> bool {

31

5237460

        if !expr.is_safe() {

32

826716

            return false;

33

4410744

34

35

40500472

        for subexpr in expr.universe() {

36

26032492

            let Expr::Atomic(_, Atom::Reference(reference)) = subexpr else {

37

22051132

                continue;

38

};

39

40

18449340

            let Some(resolved) = reference.resolve_expression() else {

41

18436912

                continue;

42

};

43

44

12428

            let id = reference.id();

45

12428

            if !resolving.insert(id.clone()) {

46

                return false;

47

12428

48

49

12428

            let is_safe = helper(&resolved, resolving);

50

12428

            resolving.remove(&id);

51

52

12428

            if !is_safe {

53

                return false;

54

12428

55

56

57

4410744

        true

58

5237460

59

60

5225032

    helper(expr, &mut HashSet::new())

61

5225032

62

63

/// Tries to decide `expr in domain` from resolved domains alone.

64

31040

fn simplify_in_domain(expr: &Expr, domain: &DomainPtr) -> Option<bool> {

65

31040

    if !is_semantically_safe(expr) {

66

212

        return None;

67

30828

68

69

30828

    let expr_domain = resolved_ground_domain_of_for_partial_eval(expr)?;

70

30388

    let domain = domain.resolve().ok()?;

71

30388

    let intersection = expr_domain.intersect(&domain).ok()?;

72

73

27696

    if normalise_int_domain(&intersection) == normalise_int_domain(expr_domain.as_ref()) {

74

52

        return Some(true);

75

27644

76

77

27644

    if let Ok(values_in_domain) = intersection.values_i32()

78

27644

        && values_in_domain.is_empty()

79

80

        return Some(false);

81

27644

82

83

27644

    None

84

31040

85

86

/// Extracts an integer when `expr` is known to be a singleton integer value.

87

989260

fn singleton_int_value(expr: &Expr) -> Option<i32> {

88

989260

    if let Ok(value) = expr.try_into() {

89

1320

        return Some(value);

90

987940

91

92

987940

    let domain = resolved_ground_domain_of_for_partial_eval(expr)?;

93

987940

    let GroundDomain::Int(ranges) = domain.as_ref() else {

94

        return None;

95

};

96

987940

    let [range] = ranges.as_slice() else {

97

        return None;

98

};

99

987940

    let (Some(low), Some(high)) = (range.low(), range.high()) else {

100

        return None;

101

};

102

103

987940

    if low == high { Some(*low) } else { None }

104

989260

105

106

/// Resolves a matrix literal subject, including constant references to matrix literals.

107

2832372

fn resolve_matrix_subject(subject: &Expr) -> Option<(Vec<Expr>, DomainPtr)> {

108

2832372

    subject.clone().unwrap_matrix_unchecked().or_else(|| {

109

1866812

        let Expr::Atomic(_, Atom::Reference(reference)) = subject else {

110

            return None;

111

};

112

113

23700

        let Lit::AbstractLiteral(AbstractLiteral::Matrix(elems, index_domain)) =

114

1866812

            reference.resolve_constant()?

115

        else {

116

            return None;

117

};

118

119

        Some((

120

23700

            elems

121

23700

                .into_iter()

122

258180

                .map(|elem| Expr::Atomic(Metadata::new(), Atom::Literal(elem)))

123

23700

                .collect(),

124

23700

            index_domain.into(),

125

))

126

1866812

})

127

2832372

128

129

/// Resolves domains for partial evaluation while avoiding malformed indexing panics.

130

1919892

fn resolved_ground_domain_of_for_partial_eval(expr: &Expr) -> Option<Moo<GroundDomain>> {

131

1919892

    match expr {

132

121624

        Expr::SafeIndex(_, subject, _) => {

133

121624

            let subject_domain = resolved_ground_domain_of_for_partial_eval(subject)?;

134

121624

            let GroundDomain::Matrix(elem_domain, _) = subject_domain.as_ref() else {

135

3440

                return None;

136

};

137

138

118184

            Some(elem_domain.clone())

139

140

        Expr::SafeSlice(_, subject, indices) => {

141

            let subject_domain = resolved_ground_domain_of_for_partial_eval(subject)?;

142

            let GroundDomain::Matrix(elem_domain, index_domains) = subject_domain.as_ref() else {

143

                return None;

144

};

145

            let sliced_dimension = indices.iter().position(Option::is_none);

146

147

            match sliced_dimension {

148

                Some(dimension) => Some(Moo::new(GroundDomain::Matrix(

149

                    elem_domain.clone(),

150

                    vec![index_domains[dimension].clone()],

151

                ))),

152

                None => Some(elem_domain.clone()),

153

154

155

        Expr::UnsafeIndex(_, _, _) | Expr::UnsafeSlice(_, _, _) => None,

156

1798268

        _ => expr.domain_of()?.resolve().ok(),

157

158

1919892

159

160

/// Tries to decide `expr = lit` and `expr != lit` from the resolved domain of `expr`.

161

947652

fn simplify_comparison_with_literal(expr: &Expr, lit: &Lit) -> Option<(bool, bool)> {

162

947652

    if !is_semantically_safe(expr) {

163

168152

        return None;

164

779500

165

166

779500

    let expr_domain = resolved_ground_domain_of_for_partial_eval(expr)?;

167

168

760808

    if !expr_domain.contains(lit).ok()? {

169

3324

        return Some((false, true));

170

757484

171

172

757484

    match (expr_domain.as_ref(), lit) {

173

579596

        (GroundDomain::Int(ranges), Lit::Int(value)) => {

174

579596

            let [range] = ranges.as_slice() else {

175

4128

                return None;

176

};

177

575468

            let (Some(low), Some(high)) = (range.low(), range.high()) else {

178

                return None;

179

};

180

181

575468

            if low == high && low == value {

182

500

                Some((true, false))

183

            } else {

184

574968

                None

185

186

187

174368

        (GroundDomain::Bool, Lit::Bool(_)) => None,

188

3520

        _ => None,

189

190

947652

191

192

/// Tries to decide reflexive equality and inequality when both sides are semantically safe.

193

2422320

fn simplify_reflexive_comparison(x: &Expr, y: &Expr) -> Option<(bool, bool)> {

194

2422320

    if x.identical_atom_to(y) && is_semantically_safe(x) && is_semantically_safe(y) {

195

80

        return Some((true, false));

196

2422240

197

198

2422240

    if is_semantically_safe(x) && is_semantically_safe(y) && x == y {

199

24120

        return Some((true, false));

200

2398120

201

202

2398120

    None

203

2422320

204

205

40130204

pub fn run_partial_evaluator(expr: &Expr) -> ApplicationResult {

206

    // NOTE: If nothing changes, we must return RuleNotApplicable, or the rewriter will try this

207

    // rule infinitely!

208

    // This is why we always check whether we found a constant or not.

209

40130204

    match expr {

210

216

        Expr::Union(_, _, _) => Err(RuleNotApplicable),

211

4668

        Expr::In(_, _, _) => Err(RuleNotApplicable),

212

560

        Expr::Intersect(_, _, _) => Err(RuleNotApplicable),

213

320

        Expr::Supset(_, _, _) => Err(RuleNotApplicable),

214

320

        Expr::SupsetEq(_, _, _) => Err(RuleNotApplicable),

215

800

        Expr::Subset(_, _, _) => Err(RuleNotApplicable),

216

404

        Expr::SubsetEq(_, _, _) => Err(RuleNotApplicable),

217

4643796

        Expr::AbstractLiteral(_, _) => Err(RuleNotApplicable),

218

279140

        Expr::Comprehension(_, _) => Err(RuleNotApplicable),

219

        Expr::AbstractComprehension(_, _) => Err(RuleNotApplicable),

220

        Expr::DominanceRelation(_, _) => Err(RuleNotApplicable),

221

        Expr::FromSolution(_, _) => Err(RuleNotApplicable),

222

        Expr::Metavar(_, _) => Err(RuleNotApplicable),

223

1127912

        Expr::UnsafeIndex(_, _, _) => Err(RuleNotApplicable),

224

61640

        Expr::UnsafeSlice(_, _, _) => Err(RuleNotApplicable),

225

1920

        Expr::Table(_, _, _) => Err(RuleNotApplicable),

226

320

        Expr::NegativeTable(_, _, _) => Err(RuleNotApplicable),

227

8560

        Expr::RecordField(_, _, _) => Err(RuleNotApplicable),

228

2832372

        Expr::SafeIndex(_, subject, indices) => {

229

            // partially evaluate matrix literals indexed by a constant.

230

231

            // subject must be a matrix literal

232

2832372

            let (es, index_domain) = resolve_matrix_subject(subject).ok_or(RuleNotApplicable)?;

233

234

989260

            if indices.is_empty() {

235

                return Err(RuleNotApplicable);

236

989260

237

238

            // the leading index must be fixed to a single value

239

989260

            let index = singleton_int_value(&indices[0]).ok_or(RuleNotApplicable)?;

240

241

            // index domain must be a single integer range with a lower bound

242

1320

            if let Some(ranges) = index_domain.as_int_ground()

243

1320

                && ranges.len() == 1

244

1320

                && let Some(from) = ranges[0].low()

245

246

1320

                let zero_indexed_index = index - from;

247

1320

                let selected = es

248

1320

                    .get(zero_indexed_index as usize)

249

1320

                    .ok_or(RuleNotApplicable)?

250

1320

                    .clone();

251

252

1320

                if indices.len() == 1 {

253

                    Ok(Reduction::pure(selected))

254

                } else {

255

1320

                    Ok(Reduction::pure(Expr::SafeIndex(

256

1320

                        Metadata::new(),

257

1320

                        Moo::new(selected),

258

1320

                        indices[1..].to_vec(),

259

1320

)))

260

261

            } else {

262

                Err(RuleNotApplicable)

263

264

265

79920

        Expr::SafeSlice(_, _, _) => Err(RuleNotApplicable),

266

31040

        Expr::InDomain(_, x, domain) => {

267

31040

            if let Some(result) = simplify_in_domain(x, domain) {

268

52

                Ok(Reduction::pure(Expr::Atomic(

269

52

                    Metadata::new(),

270

52

                    result.into(),

271

52

)))

272

30988

            } else if let Expr::Atomic(_, Atom::Reference(decl)) = x.as_ref() {

273

4240

                let decl_domain = decl

274

4240

                    .domain()

275

4240

                    .ok_or(RuleNotApplicable)?

276

4240

                    .resolve()

277

4240

                    .map_err(|_| RuleNotApplicable)?;

278

4240

                let domain = domain.resolve().map_err(|_| RuleNotApplicable)?;

279

280

4240

                let intersection = decl_domain

281

4240

                    .intersect(&domain)

282

4240

                    .map_err(|_| RuleNotApplicable)?;

283

284

                // if the declaration's domain is a subset of domain, expr is always true.

285

4240

                if &intersection == decl_domain.as_ref() {

286

                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))

287

288

                // if no elements of declaration's domain are in the domain (i.e. they have no

289

                // intersection), expr is always false.

290

//

291

                // Only check this when the intersection is a finite integer domain, as we

292

                // currently don't have a way to check whether other domain kinds are empty or not.

293

//

294

                // we should expand this to cover more domain types in the future.

295

4240

                else if let Ok(values_in_domain) = intersection.values_i32()

296

4240

                    && values_in_domain.is_empty()

297

298

                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), false.into())))

299

                } else {

300

4240

                    Err(RuleNotApplicable)

301

302

26748

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref() {

303

                if domain

304

                    .resolve()

305

                    .and_then(|gd| gd.contains(lit))

306

                    .map_err(|_| RuleNotApplicable)?

307

308

                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))

309

                } else {

310

                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), false.into())))

311

312

            } else {

313

26748

                Err(RuleNotApplicable)

314

315

316

35588

        Expr::Bubble(_, expr, cond) => {

317

            // definition of bubble is "expr is valid as long as cond is true"

318

//

319

            // check if cond is true and pop the bubble!

320

35588

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(true))) = cond.as_ref() {

321

2276

                Ok(Reduction::pure(Moo::unwrap_or_clone(expr.clone())))

322

            } else {

323

33312

                Err(RuleNotApplicable)

324

325

326

15389056

        Expr::Atomic(_, _) => Err(RuleNotApplicable),

327

33532

        Expr::ToInt(_, expression) => {

328

33532

            if expression.return_type() == ReturnType::Int {

329

                Ok(Reduction::pure(Moo::unwrap_or_clone(expression.clone())))

330

            } else {

331

33532

                Err(RuleNotApplicable)

332

333

334

19240

        Expr::Abs(m, e) => match e.as_ref() {

335

160

            Expr::Neg(_, inner) => Ok(Reduction::pure(Expr::Abs(m.clone(), inner.clone()))),

336

19080

            _ => Err(RuleNotApplicable),

337

},

338

2066640

        Expr::Sum(m, vec) => {

339

2066640

            let vec = Moo::unwrap_or_clone(vec.clone())

340

2066640

                .unwrap_list()

341

2066640

                .ok_or(RuleNotApplicable)?;

342

1687720

            let mut acc = 0;

343

1687720

            let mut n_consts = 0;

344

1687720

            let mut new_vec: Vec<Expr> = Vec::new();

345

3670956

            for expr in vec {

346

1336368

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {

347

1336368

                    acc += x;

348

1336368

                    n_consts += 1;

349

2334588

                } else {

350

2334588

                    new_vec.push(expr);

351

2334588

352

353

1687720

            if acc != 0 {

354

1278256

                new_vec.push(Expr::Atomic(

355

1278256

                    Default::default(),

356

1278256

                    Atom::Literal(Lit::Int(acc)),

357

1278256

));

358

1279344

359

360

1687720

            if n_consts <= 1 {

361

1680072

                Err(RuleNotApplicable)

362

            } else {

363

7648

                Ok(Reduction::pure(Expr::Sum(

364

7648

                    m.clone(),

365

7648

                    Moo::new(into_matrix_expr![new_vec]),

366

7648

)))

367

368

369

370

666268

        Expr::Product(m, vec) => {

371

666268

            let mut acc = 1;

372

666268

            let mut n_consts = 0;

373

666268

            let mut new_vec: Vec<Expr> = Vec::new();

374

666268

            let vec = Moo::unwrap_or_clone(vec.clone())

375

666268

                .unwrap_list()

376

666268

                .ok_or(RuleNotApplicable)?;

377

1140804

            for expr in vec {

378

449736

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {

379

449736

                    acc *= x;

380

449736

                    n_consts += 1;

381

691068

                } else {

382

691068

                    new_vec.push(expr);

383

691068

384

385

386

575308

            if n_consts == 0 {

387

125692

                return Err(RuleNotApplicable);

388

449616

389

390

449616

            new_vec.push(Expr::Atomic(

391

449616

                Default::default(),

392

449616

                Atom::Literal(Lit::Int(acc)),

393

449616

));

394

449616

            let new_product = Expr::Product(m.clone(), Moo::new(into_matrix_expr![new_vec]));

395

396

449616

            if acc == 0 {

397

                // if safe, 0 * exprs ~> 0

398

                // otherwise, just return 0* exprs

399

                if is_semantically_safe(&new_product) {

400

                    Ok(Reduction::pure(Expr::Atomic(

401

                        Default::default(),

402

                        Atom::Literal(Lit::Int(0)),

403

)))

404

                } else {

405

                    Ok(Reduction::pure(new_product))

406

407

449616

            } else if n_consts == 1 {

408

                // acc !=0, only one constant

409

449536

                Err(RuleNotApplicable)

410

            } else {

411

                // acc !=0, multiple constants found

412

80

                Ok(Reduction::pure(new_product))

413

414

415

416

41880

        Expr::Min(m, e) => {

417

41880

            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {

418

36360

                return Err(RuleNotApplicable);

419

};

420

5520

            let mut acc: Option<i32> = None;

421

5520

            let mut n_consts = 0;

422

5520

            let mut new_vec: Vec<Expr> = Vec::new();

423

11760

            for expr in vec {

424

480

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {

425

480

                    n_consts += 1;

426

480

                    acc = match acc {

427

                        Some(i) => {

428

                            if i > x {

429

                                Some(x)

430

                            } else {

431

                                Some(i)

432

433

434

480

                        None => Some(x),

435

};

436

11280

                } else {

437

11280

                    new_vec.push(expr);

438

11280

439

440

441

5520

            if let Some(i) = acc {

442

480

                new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));

443

5040

444

445

5520

            if n_consts <= 1 {

446

5520

                Err(RuleNotApplicable)

447

            } else {

448

                Ok(Reduction::pure(Expr::Min(

449

                    m.clone(),

450

                    Moo::new(into_matrix_expr![new_vec]),

451

)))

452

453

454

455

44000

        Expr::Max(m, e) => {

456

44000

            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {

457

38960

                return Err(RuleNotApplicable);

458

};

459

460

5040

            let mut acc: Option<i32> = None;

461

5040

            let mut n_consts = 0;

462

5040

            let mut new_vec: Vec<Expr> = Vec::new();

463

10320

            for expr in vec {

464

240

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {

465

240

                    n_consts += 1;

466

240

                    acc = match acc {

467

                        Some(i) => {

468

                            if i < x {

469

                                Some(x)

470

                            } else {

471

                                Some(i)

472

473

474

240

                        None => Some(x),

475

};

476

10080

                } else {

477

10080

                    new_vec.push(expr);

478

10080

479

480

481

5040

            if let Some(i) = acc {

482

240

                new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));

483

4800

484

485

5040

            if n_consts <= 1 {

486

5040

                Err(RuleNotApplicable)

487

            } else {

488

                Ok(Reduction::pure(Expr::Max(

489

                    m.clone(),

490

                    Moo::new(into_matrix_expr![new_vec]),

491

)))

492

493

494

293968

        Expr::Not(_, e1) => {

495

293968

            let Expr::Imply(_, p, q) = e1.as_ref() else {

496

293728

                return Err(RuleNotApplicable);

497

};

498

499

240

            if !is_semantically_safe(e1) {

500

                return Err(RuleNotApplicable);

501

240

502

503

240

            match (p.as_ref(), q.as_ref()) {

504

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

505

                    Ok(Reduction::pure(Expr::from(false)))

506

507

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

508

                    Ok(Reduction::pure(Moo::unwrap_or_clone(p.clone())))

509

510

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

511

                    Ok(Reduction::pure(Expr::Not(Metadata::new(), q.clone())))

512

513

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

514

                    Ok(Reduction::pure(Expr::from(false)))

515

516

240

                _ => Err(RuleNotApplicable),

517

518

519

1006448

        Expr::Or(m, e) => {

520

1006448

            let Some(terms) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {

521

222100

                return Err(RuleNotApplicable);

522

};

523

524

784348

            let mut has_changed = false;

525

526

            // 2. boolean literals

527

784348

            let mut new_terms = vec![];

528

1637832

            for expr in terms {

529

620

                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {

530

620

                    has_changed = true;

531

532

                    // true ~~> entire or is true

533

                    // false ~~> remove false from the or

534

620

                    if x {

535

                        return Ok(Reduction::pure(true.into()));

536

620

537

1637212

                } else {

538

1637212

                    new_terms.push(expr);

539

1637212

540

541

542

            // 2. check pairwise tautologies.

543

784348

            if check_pairwise_or_tautologies(&new_terms) {

544

80

                return Ok(Reduction::pure(true.into()));

545

784268

546

547

            // 3. empty or ~~> false

548

784268

            if new_terms.is_empty() {

549

                return Ok(Reduction::pure(false.into()));

550

784268

551

552

784268

            if !has_changed {

553

783664

                return Err(RuleNotApplicable);

554

604

555

556

604

            Ok(Reduction::pure(Expr::Or(

557

604

                m.clone(),

558

604

                Moo::new(into_matrix_expr![new_terms]),

559

604

)))

560

561

856388

        Expr::And(_, e) => {

562

856388

            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {

563

395096

                return Err(RuleNotApplicable);

564

};

565

461292

            let mut new_vec: Vec<Expr> = Vec::new();

566

461292

            let mut has_const: bool = false;

567

1249060

            for expr in vec {

568

165680

                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {

569

165680

                    has_const = true;

570

165680

                    if !x {

571

1032

                        return Ok(Reduction::pure(Expr::Atomic(

572

1032

                            Default::default(),

573

1032

                            Atom::Literal(Lit::Bool(false)),

574

1032

                        )));

575

164648

576

1083380

                } else {

577

1083380

                    new_vec.push(expr);

578

1083380

579

580

581

460260

            if !has_const {

582

457924

                Err(RuleNotApplicable)

583

            } else {

584

2336

                Ok(Reduction::pure(Expr::And(

585

2336

                    Metadata::new(),

586

2336

                    Moo::new(into_matrix_expr![new_vec]),

587

2336

)))

588

589

590

591

        // similar to And, but booleans are returned wrapped in Root.

592

917988

        Expr::Root(_, es) => {

593

917988

            match es.as_slice() {

594

917988

                [] => Err(RuleNotApplicable),

595

                // want to unwrap nested ands

596

913108

                [Expr::And(_, _)] => Ok(()),

597

                // root([true]) / root([false]) are already evaluated

598

276588

                [_] => Err(RuleNotApplicable),

599

615060

                [_, _, ..] => Ok(()),

600

281468

}?;

601

602

636520

            let mut new_vec: Vec<Expr> = Vec::new();

603

636520

            let mut has_changed: bool = false;

604

4217536

            for expr in es {

605

3548

                match expr {

606

3548

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

607

3548

                        has_changed = true;

608

3548

                        if !x {

609

                            // false

610

316

                            return Ok(Reduction::pure(Expr::Root(

611

316

                                Metadata::new(),

612

316

                                vec![Expr::Atomic(

613

316

                                    Default::default(),

614

316

                                    Atom::Literal(Lit::Bool(false)),

615

316

)],

616

316

                            )));

617

3232

618

                        // remove trues

619

620

621

                    // flatten ands in root

622

236780

                    Expr::And(_, vecs) => match Moo::unwrap_or_clone(vecs.clone()).unwrap_list() {

623

51320

                        Some(mut list) => {

624

51320

                            has_changed = true;

625

51320

                            new_vec.append(&mut list);

626

51320

627

185460

                        None => new_vec.push(expr.clone()),

628

},

629

3977208

                    _ => new_vec.push(expr.clone()),

630

631

632

633

636204

            if !has_changed {

634

584832

                Err(RuleNotApplicable)

635

            } else {

636

51372

                if new_vec.is_empty() {

637

200

                    new_vec.push(true.into());

638

51172

639

51372

                Ok(Reduction::pure(Expr::Root(Metadata::new(), new_vec)))

640

641

642

315472

        Expr::Imply(_m, x, y) => {

643

315472

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {

644

161976

                return if *x {

645

                    // (true) -> y ~~> y

646

1576

                    Ok(Reduction::pure(Moo::unwrap_or_clone(y.clone())))

647

                } else {

648

                    // (false) -> y ~~> true

649

160400

                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))

650

};

651

153496

};

652

653

153496

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {

654

232

                return if *y {

655

                    // x -> (true) ~~> true

656

160

                    Ok(Reduction::pure(Expr::from(true)))

657

                } else {

658

                    // x -> (false) ~~> !x

659

72

                    Ok(Reduction::pure(Expr::Not(Metadata::new(), x.clone())))

660

};

661

153264

};

662

663

            // reflexivity: p -> p ~> true

664

665

            // instead of checking syntactic equivalence of a possibly deep expression,

666

            // let identical-CSE turn them into identical variables first. Then, check if they are

667

            // identical variables.

668

669

153264

            if x.identical_atom_to(y.as_ref()) && is_semantically_safe(x) && is_semantically_safe(y)

670

671

84

                return Ok(Reduction::pure(true.into()));

672

153180

673

674

153180

            Err(RuleNotApplicable)

675

676

18568

        Expr::Iff(_m, x, y) => {

677

18568

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {

678

80

                return if *x {

679

                    // (true) <-> y ~~> y

680

                    Ok(Reduction::pure(Moo::unwrap_or_clone(y.clone())))

681

                } else {

682

                    // (false) <-> y ~~> !y

683

80

                    Ok(Reduction::pure(Expr::Not(Metadata::new(), y.clone())))

684

};

685

18488

};

686

18488

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {

687

                return if *y {

688

                    // x <-> (true) ~~> x

689

                    Ok(Reduction::pure(Moo::unwrap_or_clone(x.clone())))

690

                } else {

691

                    // x <-> (false) ~~> !x

692

                    Ok(Reduction::pure(Expr::Not(Metadata::new(), x.clone())))

693

};

694

18488

};

695

696

            // reflexivity: p <-> p ~> true

697

698

            // instead of checking syntactic equivalence of a possibly deep expression,

699

            // let identical-CSE turn them into identical variables first. Then, check if they are

700

            // identical variables.

701

702

18488

            if x.identical_atom_to(y.as_ref()) && is_semantically_safe(x) && is_semantically_safe(y)

703

704

80

                return Ok(Reduction::pure(true.into()));

705

18408

706

707

18408

            Err(RuleNotApplicable)

708

709

1506352

        Expr::Eq(_, x, y) => {

710

1506352

            if let Some((eq_result, _)) = simplify_reflexive_comparison(x, y) {

711

200

                Ok(Reduction::pure(Expr::Atomic(

712

200

                    Metadata::new(),

713

200

                    Atom::Literal(Lit::Bool(eq_result)),

714

200

)))

715

1506152

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref()

716

24588

                && let Some((eq_result, _)) = simplify_comparison_with_literal(y, lit)

717

718

160

                Ok(Reduction::pure(Expr::Atomic(

719

160

                    Metadata::new(),

720

160

                    Atom::Literal(Lit::Bool(eq_result)),

721

160

)))

722

1505992

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = y.as_ref()

723

624612

                && let Some((eq_result, _)) = simplify_comparison_with_literal(x, lit)

724

725

932

                Ok(Reduction::pure(Expr::Atomic(

726

932

                    Metadata::new(),

727

932

                    Atom::Literal(Lit::Bool(eq_result)),

728

932

)))

729

            } else {

730

1505060

                Err(RuleNotApplicable)

731

732

733

915968

        Expr::Neq(_, x, y) => {

734

915968

            if let Some((_, neq_result)) = simplify_reflexive_comparison(x, y) {

735

24000

                Ok(Reduction::pure(Expr::Atomic(

736

24000

                    Metadata::new(),

737

24000

                    Atom::Literal(Lit::Bool(neq_result)),

738

24000

)))

739

891968

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref()

740

227804

                && let Some((_, neq_result)) = simplify_comparison_with_literal(y, lit)

741

742

484

                Ok(Reduction::pure(Expr::Atomic(

743

484

                    Metadata::new(),

744

484

                    Atom::Literal(Lit::Bool(neq_result)),

745

484

)))

746

891484

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = y.as_ref()

747

70648

                && let Some((_, neq_result)) = simplify_comparison_with_literal(x, lit)

748

749

2248

                Ok(Reduction::pure(Expr::Atomic(

750

2248

                    Metadata::new(),

751

2248

                    Atom::Literal(Lit::Bool(neq_result)),

752

2248

)))

753

            } else {

754

889236

                Err(RuleNotApplicable)

755

756

757

341236

        Expr::Geq(_, _, _) => Err(RuleNotApplicable),

758

922924

        Expr::Leq(_, _, _) => Err(RuleNotApplicable),

759

14996

        Expr::Gt(_, _, _) => Err(RuleNotApplicable),

760

148444

        Expr::Lt(_, _, _) => Err(RuleNotApplicable),

761

56600

        Expr::SafeDiv(_, _, _) => Err(RuleNotApplicable),

762

60120

        Expr::UnsafeDiv(_, _, _) => Err(RuleNotApplicable),

763

13596

        Expr::Flatten(_, _, _) => Err(RuleNotApplicable), // TODO: check if anything can be done here

764

140760

        Expr::AllDiff(m, e) => {

765

140760

            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {

766

125204

                return Err(RuleNotApplicable);

767

};

768

769

15556

            let mut consts: HashSet<i32> = HashSet::new();

770

771

            // check for duplicate constant values which would fail the constraint

772

57408

            for expr in vec {

773

2760

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr

774

2760

                    && !consts.insert(x)

775

776

                    return Ok(Reduction::pure(Expr::Atomic(

777

                        m.clone(),

778

                        Atom::Literal(Lit::Bool(false)),

779

                    )));

780

57408

781

782

783

            // nothing has changed

784

15556

            Err(RuleNotApplicable)

785

786

98820

        Expr::Neg(_, _) => Err(RuleNotApplicable),

787

        Expr::Factorial(_, _) => Err(RuleNotApplicable),

788

293240

        Expr::AuxDeclaration(_, _, _) => Err(RuleNotApplicable),

789

6400

        Expr::UnsafeMod(_, _, _) => Err(RuleNotApplicable),

790

17520

        Expr::SafeMod(_, _, _) => Err(RuleNotApplicable),

791

12140

        Expr::UnsafePow(_, _, _) => Err(RuleNotApplicable),

792

23688

        Expr::SafePow(_, _, _) => Err(RuleNotApplicable),

793

409532

        Expr::Minus(_, _, _) => Err(RuleNotApplicable),

794

        Expr::Card(_, _) => todo!(),

795

796

        // As these are in a low level solver form, I'm assuming that these have already been

797

        // simplified and partially evaluated.

798

70320

        Expr::FlatAllDiff(_, _) => Err(RuleNotApplicable),

799

5600

        Expr::FlatAbsEq(_, _, _) => Err(RuleNotApplicable),

800

222784

        Expr::FlatIneq(_, _, _, _) => Err(RuleNotApplicable),

801

2160

        Expr::FlatMinusEq(_, _, _) => Err(RuleNotApplicable),

802

9480

        Expr::FlatProductEq(_, _, _, _) => Err(RuleNotApplicable),

803

537792

        Expr::FlatSumLeq(_, _, _) => Err(RuleNotApplicable),

804

559952

        Expr::FlatSumGeq(_, _, _) => Err(RuleNotApplicable),

805

72380

        Expr::FlatWatchedLiteral(_, _, _) => Err(RuleNotApplicable),

806

213920

        Expr::FlatWeightedSumLeq(_, _, _, _) => Err(RuleNotApplicable),

807

214600

        Expr::FlatWeightedSumGeq(_, _, _, _) => Err(RuleNotApplicable),

808

16040

        Expr::MinionDivEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),

809

3600

        Expr::MinionModuloEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),

810

5844

        Expr::MinionPow(_, _, _, _) => Err(RuleNotApplicable),

811

244968

        Expr::MinionReify(_, _, _) => Err(RuleNotApplicable),

812

85960

        Expr::MinionReifyImply(_, _, _) => Err(RuleNotApplicable),

813

2920

        Expr::MinionWInIntervalSet(_, _, _) => Err(RuleNotApplicable),

814

960

        Expr::MinionWInSet(_, _, _) => Err(RuleNotApplicable),

815

299460

        Expr::MinionElementOne(_, _, _, _) => Err(RuleNotApplicable),

816

1755220

        Expr::SATInt(_, _, _, _) => Err(RuleNotApplicable),

817

        Expr::PairwiseSum(_, _, _) => Err(RuleNotApplicable),

818

        Expr::PairwiseProduct(_, _, _) => Err(RuleNotApplicable),

819

        Expr::Active(_, _, _) => todo!(),

820

        Expr::Defined(_, _) => todo!(),

821

        Expr::Range(_, _) => todo!(),

822

        Expr::Image(_, _, _) => todo!(),

823

        Expr::ImageSet(_, _, _) => todo!(),

824

        Expr::PreImage(_, _, _) => todo!(),

825

        Expr::Inverse(_, _, _) => todo!(),

826

        Expr::Restrict(_, _, _) => todo!(),

827

        Expr::ToSet(_, _) => todo!(),

828

        Expr::ToMSet(_, _) => todo!(),

829

        Expr::ToRelation(_, _) => todo!(),

830

        Expr::RelationProj(_, _, _) => todo!(),

831

        Expr::Apart(_, _, _) => todo!(),

832

        Expr::Together(_, _, _) => todo!(),

833

        Expr::Participants(_, _) => todo!(),

834

        Expr::Party(_, _, _) => todo!(),

835

        Expr::Parts(_, _) => todo!(),

836

        Expr::Subsequence(_, _, _) => todo!(),

837

        Expr::Substring(_, _, _) => todo!(),

838

2404

        Expr::LexLt(_, _, _) => Err(RuleNotApplicable),

839

41000

        Expr::LexLeq(_, _, _) => Err(RuleNotApplicable),

840

120

        Expr::LexGt(_, _, _) => Err(RuleNotApplicable),

841

240

        Expr::LexGeq(_, _, _) => Err(RuleNotApplicable),

842

480

        Expr::FlatLexLt(_, _, _) => Err(RuleNotApplicable),

843

720

        Expr::FlatLexLeq(_, _, _) => Err(RuleNotApplicable),

844

845

40130204

846

847

/// Checks for tautologies involving pairs of terms inside an or, returning true if one is found.

848

///

849

/// This applies the following rules:

850

///

851

/// ```text

852

/// (p->q) \/ (q->p) ~> true    [totality of implication]

853

/// (p->q) \/ (p-> !q) ~> true  [conditional excluded middle]

854

/// ```

855

///

856

784348

fn check_pairwise_or_tautologies(or_terms: &[Expr]) -> bool {

857

    // Collect terms that are structurally identical to the rule input.

858

    // Then, try the rules on these terms, also checking the other conditions of the rules.

859

860

    // stores (p,q) in p -> q

861

784348

    let mut p_implies_q: Vec<(&Expr, &Expr)> = vec![];

862

863

    // stores (p,q) in p -> !q

864

784348

    let mut p_implies_not_q: Vec<(&Expr, &Expr)> = vec![];

865

866

1637212

    for term in or_terms.iter() {

867

1637212

        if let Expr::Imply(_, p, q) = term {

868

            // we use identical_atom_to for equality later on, so these sets are mutually exclusive.

869

//

870

            // in general however, p -> !q would be in p_implies_q as (p,!q)

871

1000

            if let Expr::Not(_, q_1) = q.as_ref() {

872

40

                p_implies_not_q.push((p.as_ref(), q_1.as_ref()));

873

960

            } else {

874

960

                p_implies_q.push((p.as_ref(), q.as_ref()));

875

960

876

1636212

877

878

879

    // `(p->q) \/ (q->p) ~> true    [totality of implication]`

880

784348

    for ((p1, q1), (q2, p2)) in iproduct!(p_implies_q.iter(), p_implies_q.iter()) {

881

1440

        if p1.identical_atom_to(p2) && q1.identical_atom_to(q2) {

882

40

            return true;

883

1400

884

885

886

    // `(p->q) \/ (p-> !q) ~> true`    [conditional excluded middle]

887

784308

    for ((p1, q1), (p2, q2)) in iproduct!(p_implies_q.iter(), p_implies_not_q.iter()) {

888

40

        if p1.identical_atom_to(p2) && q1.identical_atom_to(q2) {

889

40

            return true;

890

891

892

893

784268

    false

894

784348