Grcov report - settings.rs

1

use std::{

2

    cell::{Cell, RefCell},

3

    collections::VecDeque,

4

    fmt::Display,

5

    io::{self, BufRead, Write},

6

    str::FromStr,

7

};

8

9

use schemars::JsonSchema;

10

use serde::{Deserialize, Serialize};

11

use strum_macros::{Display as StrumDisplay, EnumIter};

12

13

use crate::bug;

14

use crate::bug_assert;

15

16

/// Strategy used when a modelling decision has more than one applicable answer.

17

#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]

18

pub enum Heuristic {

19

    First,

20

    Random,

21

    #[default]

22

    Compact,

23

    /// Prompt on stdin, or consume values from [`set_heuristic_responses`].

24

    Interactive,

25

    /// Enumerate every applicable choice. This is supported by the exhaustive model generator,

26

    /// but is not accepted by the command-line interface yet.

27

    All,

28

29

30

impl Display for Heuristic {

31

2475645

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

32

2475645

        f.write_str(match self {

33

2204

            Self::First => "f",

34

            Self::Random => "r",

35

22999

            Self::Compact => "c",

36

            Self::Interactive => "i",

37

2450442

            Self::All => "x",

38

})

39

2475645

40

41

42

impl FromStr for Heuristic {

43

    type Err = String;

44

45

47430

    fn from_str(value: &str) -> Result<Self, Self::Err> {

46

47430

        match value.trim().to_ascii_lowercase().as_str() {

47

552

            "f" | "first" => Ok(Self::First),

48

1

            "r" | "random" => Ok(Self::Random),

49

7666

            "c" | "compact" => Ok(Self::Compact),

50

2

            "i" | "interactive" => Ok(Self::Interactive),

51

39209

            "x" | "all" => Ok(Self::All),

52

            other => Err(format!(

53

                "unknown heuristic '{other}'; expected one of: f, r, c, i, x"

54

)),

55

56

47430

57

58

59

/// Whether a declaration may have more than one channelled representation.

60

#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]

61

pub enum Channelling {

62

    #[default]

63

No,

64

    Yes,

65

    /// One representation kind per type family throughout a model, without channelling.

66

    Uniform,

67

68

69

impl Display for Channelling {

70

2502442

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

71

2502442

        f.write_str(match self {

72

94513

            Self::No => "no",

73

            Self::Yes => "yes",

74

2407929

            Self::Uniform => "uniform",

75

})

76

2502442

77

78

79

impl FromStr for Channelling {

80

    type Err = String;

81

82

47079

    fn from_str(value: &str) -> Result<Self, Self::Err> {

83

47079

        match value.trim().to_ascii_lowercase().as_str() {

84

14183

            "no" => Ok(Self::No),

85

5

            "yes" => Ok(Self::Yes),

86

32891

            "uniform" => Ok(Self::Uniform),

87

            other => Err(format!(

88

                "unknown channelling setting '{other}'; expected yes, no, or uniform"

89

)),

90

91

47079

92

93

94

pub const DEFAULT_HEURISTIC_SEED: u64 = 0;

95

96

thread_local! {

97

    static ELEMENT_ENCODING: Cell<Option<crate::ast::sat_decision::ElementEncoding>> = const { Cell::new(None) };

98

    static TABLE_ENCODING: Cell<Option<crate::ast::sat_decision::TableEncoding>> = const { Cell::new(None) };

99

    static ALLDIFFERENT_ENCODING: Cell<Option<crate::ast::sat_decision::AllDifferentEncoding>> = const { Cell::new(None) };

100

    static PB_ENCODING: Cell<Option<crate::ast::sat_decision::PbEncoding>> = const { Cell::new(None) };

101

    static CARDINALITY_ENCODING: Cell<Option<crate::ast::sat_decision::CardinalityEncoding>> = const { Cell::new(None) };

102

    static AMO_ENCODING: Cell<Option<crate::ast::sat_decision::AmoEncoding>> = const { Cell::new(None) };

103

    static HEURISTIC: Cell<Heuristic> = const { Cell::new(Heuristic::Compact) };

104

    static CHANNELLING: Cell<Channelling> = const { Cell::new(Channelling::No) };

105

    static HEURISTIC_RANDOM_STATE: Cell<u64> = const { Cell::new(DEFAULT_HEURISTIC_SEED) };

106

    static HEURISTIC_ALL_CHOICES: RefCell<AllChoicesState> =

107

        const { RefCell::new(AllChoicesState::new()) };

108

    /// 1-based answers for the interactive heuristic, matching Conjure's `--responses`.

109

    static HEURISTIC_RESPONSES: RefCell<VecDeque<usize>> = const { RefCell::new(VecDeque::new()) };

110

111

112

#[derive(Clone, Debug, PartialEq, Eq)]

113

pub struct HeuristicChoice {

114

    pub selected: usize,

115

    pub options: Vec<String>,

116

117

118

#[derive(Debug)]

119

struct AllChoicesState {

120

    requested: Vec<usize>,

121

    decisions: Vec<HeuristicChoice>,

122

123

124

impl AllChoicesState {

125

    const fn new() -> Self {

126

        Self {

127

            requested: Vec::new(),

128

            decisions: Vec::new(),

129

130

131

132

133

2430240

pub fn set_heuristic(heuristic: Heuristic) {

134

2430240

    HEURISTIC.with(|current| current.set(heuristic));

135

2430240

136

137

6981123

pub fn heuristic() -> Heuristic {

138

6981123

    HEURISTIC.with(Cell::get)

139

6981123

140

141

1212007

pub fn set_channelling(channelling: Channelling) {

142

1212007

    CHANNELLING.with(|current| current.set(channelling));

143

1212007

    crate::representation::uniform::reset();

144

1212007

145

146

3996723354

pub fn channelling() -> Channelling {

147

3996723354

    CHANNELLING.with(Cell::get)

148

3996723354

149

150

1212009

pub fn set_heuristic_seed(seed: u64) {

151

1212009

    HEURISTIC_RANDOM_STATE.with(|state| state.set(seed));

152

1212009

153

154

/// Sets the 1-based answers consumed by the interactive heuristic (`i`).

155

///

156

/// When provided (e.g. via `--responses`), these are used instead of prompting on stdin.

157

/// Values must be in `1..=n` for a decision with `n` options, matching Conjure.

158

302

pub fn set_heuristic_responses(responses: Vec<usize>) {

159

302

    HEURISTIC_RESPONSES.with(|state| {

160

302

        *state.borrow_mut() = VecDeque::from(responses);

161

302

});

162

302

163

164

/// Clears any remaining interactive responses.

165

1

pub fn clear_heuristic_responses() {

166

1

    HEURISTIC_RESPONSES.with(|state| state.borrow_mut().clear());

167

1

168

169

/// Returns a deterministic pseudo-random index and advances the per-thread heuristic RNG.

170

16

pub fn next_heuristic_random_index(upper_bound: usize) -> usize {

171

    bug_assert!(

172

16

        upper_bound > 0,

173

        "random choice requires at least one candidate"

174

);

175

16

    HEURISTIC_RANDOM_STATE.with(|state| {

176

        // SplitMix64: small, reproducible, and sufficient for choice ordering.

177

16

        let next = state.get().wrapping_add(0x9e37_79b9_7f4a_7c15);

178

16

        state.set(next);

179

16

        let mut mixed = next;

180

16

        mixed = (mixed ^ (mixed >> 30)).wrapping_mul(0xbf58_476d_1ce4_e5b9);

181

16

        mixed = (mixed ^ (mixed >> 27)).wrapping_mul(0x94d0_49bb_1331_11eb);

182

16

        mixed ^= mixed >> 31;

183

16

        (mixed as usize) % upper_bound

184

16

})

185

16

186

187

/// Starts one replay of the `x` heuristic using the requested branch indices.

188

1205619

pub fn begin_heuristic_all_choices(requested: Vec<usize>) {

189

1205619

    HEURISTIC_ALL_CHOICES.with(|state| {

190

1205619

        *state.borrow_mut() = AllChoicesState {

191

1205619

            requested,

192

1205619

            decisions: Vec::new(),

193

1205619

};

194

1205619

});

195

1205619

196

197

/// Restores the previous heuristic when a scoped override ends.

198

struct HeuristicGuard(Heuristic);

199

200

impl Drop for HeuristicGuard {

201

6276

    fn drop(&mut self) {

202

6276

        set_heuristic(self.0);

203

6276

204

205

206

/// Runs `f` with the compact heuristic in force, whatever the configured one is.

207

///

208

/// Rewriting a temporary model -- a comprehension generator submodel, say -- picks representations

209

/// too, but those are not modelling choices about the user's problem: a representation is

210

/// semantics-preserving, so whichever one a submodel gets, it enumerates the same values. Compact

211

/// takes the smallest and moves on, leaving the configured heuristic's state for the decisions that

212

/// do matter: `x` keeps enumerating combinations of the real model only, the random stream is not

213

/// advanced, and the interactive heuristic does not ask the user about throwaway variables.

214

///

215

/// A representation named on the domain itself (`set (representation packed)`) still wins -- representation

216

/// selection honours that before it consults the heuristic at all.

217

1518

pub fn with_compact_heuristic<T>(f: impl FnOnce() -> T) -> T {

218

1518

    let previous = heuristic();

219

1518

    set_heuristic(Heuristic::Compact);

220

1518

    let _guard = HeuristicGuard(previous);

221

1518

f()

222

1518

223

224

/// Selects the requested branch at the next `x` decision and records all available options.

225

3995477

pub fn next_heuristic_all_index(options: &[&str]) -> usize {

226

    bug_assert!(

227

3995477

        !options.is_empty(),

228

        "all-choice requires at least one candidate"

229

);

230

3995477

    HEURISTIC_ALL_CHOICES.with(|state| {

231

3995477

        let mut state = state.borrow_mut();

232

3995477

        let decision_index = state.decisions.len();

233

3995477

        let selected = state.requested.get(decision_index).copied().unwrap_or(0);

234

3995477

        assert!(

235

3995477

            selected < options.len(),

236

            "requested heuristic branch {selected} but only {} options exist",

237

            options.len()

238

);

239

3995477

        state.decisions.push(HeuristicChoice {

240

3995477

            selected,

241

21862031

            options: options.iter().map(|option| (*option).to_string()).collect(),

242

});

243

3995477

        selected

244

3995477

})

245

3995477

246

247

2411236

pub fn heuristic_all_choices() -> Vec<HeuristicChoice> {

248

2411236

    HEURISTIC_ALL_CHOICES.with(|state| state.borrow().decisions.clone())

249

2411236

250

251

/// Selects an option for the interactive heuristic (`i`).

252

///

253

/// Options are printed 1-based. Prefers the next value from [`set_heuristic_responses`]; otherwise

254

/// prompts on stdin (empty input picks option 1), matching Conjure.

255

3

pub fn next_heuristic_interactive_index(options: &[&str]) -> usize {

256

    bug_assert!(

257

3

        !options.is_empty(),

258

        "interactive choice requires at least one candidate"

259

);

260

261

3

    for (index, option) in options.iter().enumerate() {

262

7

        eprintln!("{}. {}", index + 1, option);

263

264

265

3

    let recorded = HEURISTIC_RESPONSES.with(|state| state.borrow_mut().pop_front());

266

3

    let one_based = match recorded {

267

        Some(recorded) => {

268

3

            eprintln!("Response: {recorded}");

269

3

            assert!(

270

3

                recorded >= 1 && recorded <= options.len(),

271

                "recorded response {recorded} out of range; expected a value between 1 and {}",

272

                options.len()

273

);

274

3

            recorded

275

276

        None => prompt_heuristic_interactive_choice(options.len()),

277

};

278

3

    one_based - 1

279

3

280

281

fn prompt_heuristic_interactive_choice(option_count: usize) -> usize {

282

    let stdin = io::stdin();

283

    let mut stdout = io::stderr();

284

    loop {

285

        eprint!("Pick option: ");

286

        let _ = stdout.flush();

287

        let mut line = String::new();

288

        if stdin.lock().read_line(&mut line).is_err() {

289

            eprintln!("Failed to read interactive heuristic response; defaulting to 1");

290

            return 1;

291

292

        let trimmed = line.trim();

293

        if trimmed.is_empty() {

294

            return 1;

295

296

        match trimmed.parse::<usize>() {

297

            Ok(value) if value >= 1 && value <= option_count => return value,

298

            Ok(_) => {

299

                eprintln!("Enter a value between 1 and {option_count}");

300

301

            Err(_) => {

302

                eprintln!("Enter an integer value.");

303

304

305

306

307

308

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default)]

309

pub enum Parser {

310

    #[default]

311

    TreeSitter,

312

    ViaConjure,

313

314

315

impl Display for Parser {

316

2522360

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

317

2522360

        match self {

318

2517285

            Parser::TreeSitter => write!(f, "tree-sitter"),

319

5075

            Parser::ViaConjure => write!(f, "via-conjure"),

320

321

2522360

322

323

324

impl FromStr for Parser {

325

    type Err = String;

326

327

26805

    fn from_str(s: &str) -> Result<Self, Self::Err> {

328

26805

        match s.trim().to_ascii_lowercase().as_str() {

329

21881

            "tree-sitter" => Ok(Parser::TreeSitter),

330

4924

            "via-conjure" => Ok(Parser::ViaConjure),

331

            other => Err(format!(

332

                "unknown parser: {other}; expected one of: tree-sitter, via-conjure"

333

)),

334

335

26805

336

337

338

thread_local! {

339

    /// Thread-local setting for which parser is currently active.

340

///

341

    /// Must be explicitly set before use.

342

    static CURRENT_PARSER: Cell<Option<Parser>> = const { Cell::new(None) };

343

344

345

1212335

pub fn set_current_parser(parser: Parser) {

346

1212335

    CURRENT_PARSER.with(|current| current.set(Some(parser)));

347

1212335

348

349

pub fn current_parser() -> Parser {

350

    CURRENT_PARSER.with(|current| {

351

        current.get().unwrap_or_else(|| {

352

            // loud failure on purpose, so we don't end up using the default

353

            bug!("current parser not set for this thread; call set_current_parser first")

354

})

355

})

356

357

358

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]

359

pub struct RewriteConfig {

360

    /// Skip rules whose declared expression discriminants cannot match.

361

    pub prefilter: bool,

362

    /// Drive rewriting from persistent dirty node queues instead of repeated full scans.

363

    pub worklist: bool,

364

365

366

impl RewriteConfig {

367

60

    pub const fn baseline() -> Self {

368

60

        Self {

369

60

            prefilter: false,

370

60

            worklist: false,

371

60

372

60

373

374

20173

    pub const fn optimised() -> Self {

375

20173

        Self {

376

20173

            prefilter: true,

377

20173

            worklist: true,

378

20173

379

20173

380

381

1351542

    pub const fn is_baseline(self) -> bool {

382

1351542

        !self.prefilter && !self.worklist

383

1351542

384

385

2469568

    pub const fn is_optimised(self) -> bool {

386

2469568

        self.prefilter && self.worklist

387

2469568

388

389

390

impl Default for RewriteConfig {

391

    fn default() -> Self {

392

        Self::optimised()

393

394

395

396

impl Display for RewriteConfig {

397

2469568

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

398

2469568

        if self.is_optimised() {

399

2469565

            write!(f, "optimised")

400

3

        } else if self.is_baseline() {

401

1

            write!(f, "baseline")

402

        } else {

403

2

            let mut options = vec!["baseline"];

404

2

            if self.prefilter {

405

1

                options.push("prefilter");

406

1

407

2

            if self.worklist {

408

1

                options.push("worklist");

409

1

410

2

            write!(f, "{}", options.join("+"))

411

412

2469568

413

414

415

impl FromStr for RewriteConfig {

416

    type Err = String;

417

418

19285

    fn from_str(s: &str) -> Result<Self, Self::Err> {

419

19285

        let trimmed = s.trim().to_ascii_lowercase();

420

19285

        match trimmed.as_str() {

421

13

            "baseline" => return Ok(Self::baseline()),

422

19254

            "optimised" => return Ok(Self::optimised()),

423

18

            _ => {}

424

425

426

18

        if !trimmed.starts_with("baseline+") {

427

2

            return Err(format!(

428

2

                "unknown rewrite config: {trimmed}; expected baseline, optimised, or baseline plus '+' separated prefilter/worklist options"

429

2

));

430

16

431

432

16

        let mut config = Self::baseline();

433

16

        let mut baseline_seen = false;

434

16

        let mut prefilter_seen = false;

435

16

        let mut worklist_seen = false;

436

16

        let mut option_seen = false;

437

438

16

        for token in trimmed.split('+') {

439

35

            match token {

440

                "" => {}

441

                "baseline" => {

442

16

                    if baseline_seen {

443

                        return Err("duplicate rewrite option 'baseline'".to_string());

444

16

445

16

                    baseline_seen = true;

446

447

                "prefilter" => {

448

5

                    if prefilter_seen {

449

                        return Err("duplicate rewrite option 'prefilter'".to_string());

450

5

451

5

                    config.prefilter = true;

452

5

                    prefilter_seen = true;

453

5

                    option_seen = true;

454

455

                "worklist" => {

456

4

                    if worklist_seen {

457

                        return Err("duplicate rewrite option 'worklist'".to_string());

458

4

459

4

                    config.worklist = true;

460

4

                    worklist_seen = true;

461

4

                    option_seen = true;

462

463

                other => {

464

10

                    return Err(format!(

465

10

                        "unknown rewrite option '{other}'; expected baseline, optimised, or a '+' separated combination of: prefilter, worklist"

466

10

));

467

468

469

470

471

6

        if !option_seen {

472

            return Err(

473

                "rewrite config 'baseline+' must include at least one of: prefilter, worklist"

474

                    .to_string(),

475

);

476

6

477

478

6

        Ok(config)

479

19285

480

481

482

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]

483

pub enum Rewriter {

484

    Rewrite(RewriteConfig),

485

486

487

impl Default for Rewriter {

488

839

    fn default() -> Self {

489

839

        Self::Rewrite(RewriteConfig::optimised())

490

839

491

492

493

thread_local! {

494

    /// Thread-local setting for which rewriter is currently active.

495

///

496

    /// Must be explicitly set before use.

497

    static CURRENT_REWRITER: Cell<Option<Rewriter>> = const { Cell::new(None) };

498

499

500

impl Display for Rewriter {

501

2469551

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

502

2469551

        match self {

503

2469551

            Rewriter::Rewrite(config) => write!(f, "{config}"),

504

2469551

505

2469551

506

507

508

impl FromStr for Rewriter {

509

    type Err = String;

510

511

19270

    fn from_str(s: &str) -> Result<Self, Self::Err> {

512

19270

        let trimmed = s.trim().to_ascii_lowercase();

513

19270

        match trimmed.as_str() {

514

19265

            "baseline" | "optimised" => Ok(Rewriter::Rewrite(trimmed.parse()?)),

515

            other => {

516

5

                if other.contains('+') {

517

4

                    return Ok(Rewriter::Rewrite(other.parse()?));

518

1

519

520

1

                Err(format!(

521

1

                    "unknown rewriter: {other}; expected baseline, optimised, or baseline plus '+' separated prefilter/worklist options"

522

1

))

523

524

525

19270

526

527

528

2564175

pub fn set_current_rewriter(rewriter: Rewriter) {

529

2564175

    CURRENT_REWRITER.with(|current| current.set(Some(rewriter)));

530

2564175

531

532

139474

pub fn current_rewriter() -> Rewriter {

533

139474

    CURRENT_REWRITER.with(|current| {

534

139474

        current.get().unwrap_or_else(|| {

535

            // loud failure on purpose, so we don't end up using the default

536

            bug!("current rewriter not set for this thread; call set_current_rewriter first")

537

})

538

139474

})

539

139474

540

541

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]

542

pub enum QuantifiedExpander {

543

    Auto,

544

    Native,

545

    ViaSolver,

546

    ViaSolverAc,

547

548

549

impl Display for QuantifiedExpander {

550

2514854

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

551

2514854

        match self {

552

2514854

            QuantifiedExpander::Auto => write!(f, "auto"),

553

            QuantifiedExpander::Native => write!(f, "native"),

554

            QuantifiedExpander::ViaSolver => write!(f, "via-solver"),

555

            QuantifiedExpander::ViaSolverAc => write!(f, "via-solver-ac"),

556

557

2514854

558

559

560

impl FromStr for QuantifiedExpander {

561

    type Err = String;

562

563

19266

    fn from_str(s: &str) -> Result<Self, Self::Err> {

564

19266

        match s.trim().to_ascii_lowercase().as_str() {

565

19254

            "auto" => Ok(QuantifiedExpander::Auto),

566

            "native" => Ok(QuantifiedExpander::Native),

567

            "via-solver" => Ok(QuantifiedExpander::ViaSolver),

568

12

            "via-solver-ac" => Ok(QuantifiedExpander::ViaSolverAc),

569

            _ => Err(format!(

570

                "unknown comprehension expander: {s}; expected one of: \

571

                 auto, native, via-solver, via-solver-ac"

572

)),

573

574

19266

575

576

577

thread_local! {

578

    /// Thread-local setting for which comprehension expansion strategy is currently active.

579

///

580

    /// Must be explicitly set before use.

581

    static COMPREHENSION_EXPANDER: Cell<Option<QuantifiedExpander>> = const { Cell::new(None) };

582

583

584

1212693

pub fn set_comprehension_expander(expander: QuantifiedExpander) {

585

1212693

    COMPREHENSION_EXPANDER.with(|current| current.set(Some(expander)));

586

1212693

587

588

924825

pub fn comprehension_expander() -> QuantifiedExpander {

589

924825

    COMPREHENSION_EXPANDER.with(|current| {

590

924825

        current.get().unwrap_or_else(|| {

591

            // loud failure on purpose, so we don't end up using the default

592

            bug!(

593

                "comprehension expander not set for this thread; call set_comprehension_expander first"

594

595

})

596

924825

})

597

924825

598

599

#[derive(

600

    Debug,

601

    EnumIter,

602

    StrumDisplay,

603

    PartialEq,

604

Eq,

605

    Hash,

606

    Clone,

607

    Copy,

608

    Serialize,

609

    Deserialize,

610

    JsonSchema,

611

)]

612

pub enum SolverFamily {

613

    Minion,

614

    Sat,

615

Z3,

616

617

618

thread_local! {

619

    /// Thread-local setting for which solver family is currently active.

620

///

621

    /// Must be explicitly set before use.

622

    static CURRENT_SOLVER_FAMILY: Cell<Option<SolverFamily>> = const { Cell::new(None) };

623

624

625

pub const DEFAULT_MINION_DISCRETE_THRESHOLD: usize = 10;

626

627

thread_local! {

628

    /// Thread-local setting controlling when Minion int domains are emitted as `DISCRETE`.

629

///

630

    /// If an int domain size is <= this threshold, the Minion adaptor uses `DISCRETE`; otherwise

631

    /// it uses `BOUND`, unless another constraint requires `DISCRETE`.

632

    static MINION_DISCRETE_THRESHOLD: Cell<Option<usize>> = const { Cell::new(None) };

633

634

    /// Thread-local setting controlling whether rule-trace outputs are active in this phase.

635

///

636

    /// This is intentionally off by default and can be disabled before solver-time rewrites so

637

    /// follow-up dominance-blocking rewrites do not pollute the initial rewrite trace.

638

    static RULE_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };

639

640

    /// Thread-local setting controlling whether default rule traces are configured.

641

    static DEFAULT_RULE_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };

642

643

    /// Thread-local setting controlling whether verbose rule-attempt traces are configured.

644

    static RULE_ATTEMPT_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };

645

646

    /// Thread-local setting controlling whether aggregate rule-application traces are configured.

647

    static RULE_TRACE_AGGREGATES_ENABLED: Cell<bool> = const { Cell::new(false) };

648

649

650

1212336

pub fn set_current_solver_family(solver_family: SolverFamily) {

651

1212336

    CURRENT_SOLVER_FAMILY.with(|current| current.set(Some(solver_family)));

652

1212336

653

654

/// Restores the previous solver family when a scoped override ends.

655

struct SolverFamilyGuard(Option<SolverFamily>);

656

657

impl Drop for SolverFamilyGuard {

658

6277

    fn drop(&mut self) {

659

6277

        CURRENT_SOLVER_FAMILY.with(|current| current.set(self.0));

660

6277

661

662

663

/// Runs `f` as a rewrite for `solver_family`, then restores the surrounding solver context.

664

///

665

/// Some rewrites build and solve a temporary model with a different backend from the outer model.

666

/// Representation applicability must follow the backend that will actually consume that temporary

667

/// model, not the user's outer solver setting.

668

1519

pub fn with_solver_family<T>(solver_family: SolverFamily, f: impl FnOnce() -> T) -> T {

669

1519

    let previous = CURRENT_SOLVER_FAMILY.with(|current| current.replace(Some(solver_family)));

670

1519

    let _guard = SolverFamilyGuard(previous);

671

1519

f()

672

1519

673

674

/// The active solver family, or `None` if this thread has not set one.

675

///

676

/// Unlike [`current_solver_family`] this does not panic. Solver-family gating asks with this so

677

/// that unit tests exercising a single component do not have to stand up a solver context.

678

324422152

pub fn try_current_solver_family() -> Option<SolverFamily> {

679

324422152

    CURRENT_SOLVER_FAMILY.with(|current| current.get())

680

324422152

681

682

pub fn current_solver_family() -> SolverFamily {

683

    CURRENT_SOLVER_FAMILY.with(|current| {

684

        current.get().unwrap_or_else(|| {

685

            // loud failure on purpose, so we don't end up using the default

686

            bug!(

687

                "current solver family not set for this thread; call set_current_solver_family first"

688

689

})

690

})

691

692

693

/// Whether integers carry a representation choice for the solver being targeted.

694

///

695

/// SAT has no integers at all: an int variable is encoded as a vector of Booleans, and which

696

/// encoding it gets is a representation choice like any other. The SMT backend does have integers,

697

/// but has two ways to express them -- linear arithmetic and bit-vectors -- so the choice is a

698

/// representation there too. Minion has one native integer and needs none of this. With no solver

699

/// family set -- a unit test exercising one component, say -- integers stay concrete.

700

58970512

pub fn ints_need_representation() -> bool {

701

58970512

    matches!(

702

58970512

        try_current_solver_family(),

703

        Some(SolverFamily::Sat | SolverFamily::Z3)

704

705

58970512

706

707

/// Pins Minion's domain threshold, or leaves it to the modelling heuristic.

708

1212335

pub fn set_minion_discrete_threshold(threshold: Option<usize>) {

709

1212335

    MINION_DISCRETE_THRESHOLD.with(|current| current.set(threshold));

710

1212335

711

712

/// Selects one threshold for a Minion model: the default, all bound, or all discrete.

713

/// Constraints requiring discrete variables still override the threshold.

714

28488

pub fn select_minion_discrete_threshold() -> usize {

715

28488

    if let Some(threshold) = MINION_DISCRETE_THRESHOLD.with(Cell::get) {

716

28362

        return threshold;

717

126

718

126

    let thresholds = [DEFAULT_MINION_DISCRETE_THRESHOLD, 0, usize::MAX];

719

126

    let labels = [

720

126

        "minion-discrete-threshold=10",

721

126

        "minion-discrete-threshold=0",

722

126

        "minion-discrete-threshold=unlimited",

723

126

];

724

126

    let index = match heuristic() {

725

126

        Heuristic::First | Heuristic::Compact => 0,

726

        Heuristic::Random => next_heuristic_random_index(thresholds.len()),

727

        Heuristic::Interactive => next_heuristic_interactive_index(&labels),

728

        Heuristic::All => next_heuristic_all_index(&labels),

729

};

730

126

    thresholds[index]

731

28488

732

733

2424055

pub fn set_rule_trace_enabled(enabled: bool) {

734

2424055

    RULE_TRACE_ENABLED.with(|current| current.set(enabled));

735

2424055

736

737

149323720

pub fn rule_trace_enabled() -> bool {

738

149323720

    RULE_TRACE_ENABLED.with(|current| current.get())

739

149323720

740

741

1212339

pub fn set_default_rule_trace_enabled(enabled: bool) {

742

1212339

    DEFAULT_RULE_TRACE_ENABLED.with(|current| current.set(enabled));

743

1212339

744

745

72277224

pub fn default_rule_trace_enabled() -> bool {

746

72277224

    DEFAULT_RULE_TRACE_ENABLED.with(|current| current.get())

747

72277224

748

749

1212335

pub fn set_rule_attempt_trace_enabled(enabled: bool) {

750

1212335

    RULE_ATTEMPT_TRACE_ENABLED.with(|current| current.set(enabled));

751

1212335

752

753

2414782

pub fn rule_attempt_trace_enabled() -> bool {

754

2414782

    RULE_ATTEMPT_TRACE_ENABLED.with(|current| current.get())

755

2414782

756

757

1212335

pub fn set_rule_trace_aggregates_enabled(enabled: bool) {

758

1212335

    RULE_TRACE_AGGREGATES_ENABLED.with(|current| current.set(enabled));

759

1212335

760

761

55878379

pub fn rule_trace_aggregates_enabled() -> bool {

762

55878379

    RULE_TRACE_AGGREGATES_ENABLED.with(|current| current.get())

763

55878379

764

765

pub fn configured_rule_trace_enabled() -> bool {

766

    default_rule_trace_enabled() || rule_attempt_trace_enabled() || rule_trace_aggregates_enabled()

767

768

769

impl FromStr for SolverFamily {

770

    type Err = String;

771

772

63983

    fn from_str(s: &str) -> Result<Self, Self::Err> {

773

63983

        match s.trim().to_ascii_lowercase().as_str() {

774

18627

            "minion" => Ok(SolverFamily::Minion),

775

33956

            "sat" => Ok(SolverFamily::Sat),

776

11400

            "z3" => Ok(SolverFamily::Z3),

777

            other => Err(format!(

778

                "unknown solver '{other}', expected one of: minion, sat, z3"

779

)),

780

781

63983

782

783

784

impl SolverFamily {

785

8784651

    pub fn as_str(&self) -> String {

786

8784651

        match self {

787

306762

            SolverFamily::Minion => "minion".to_owned(),

788

8187135

            SolverFamily::Sat => "sat".to_owned(),

789

290754

            SolverFamily::Z3 => "z3".to_owned(),

790

791

8784651

792

793

794

#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]

795

pub struct SolverArgs {

796

    pub timeout_ms: Option<u64>,

797

798

799

#[cfg(test)]

800

mod tests {

801

    use super::{

802

        Channelling, Heuristic, QuantifiedExpander, RewriteConfig, Rewriter, SolverFamily,

803

        begin_heuristic_all_choices, clear_heuristic_responses, heuristic_all_choices,

804

        next_heuristic_all_index, next_heuristic_interactive_index, next_heuristic_random_index,

805

        set_current_solver_family, set_heuristic_responses, set_heuristic_seed,

806

        try_current_solver_family, with_solver_family,

807

};

808

    use std::str::FromStr;

809

810

    #[test]

811

1

    fn compact_is_the_default_heuristic() {

812

1

        assert_eq!(Heuristic::default(), Heuristic::Compact);

813

1

814

815

    #[test]

816

1

    fn scoped_solver_family_restores_the_outer_solver() {

817

1

        set_current_solver_family(SolverFamily::Z3);

818

819

1

        with_solver_family(SolverFamily::Minion, || {

820

1

            assert_eq!(try_current_solver_family(), Some(SolverFamily::Minion));

821

1

});

822

823

1

        assert_eq!(try_current_solver_family(), Some(SolverFamily::Z3));

824

1

825

826

    #[test]

827

1

    fn parses_answer_heuristics_and_channelling() {

828

1

        assert_eq!(Heuristic::from_str("f"), Ok(Heuristic::First));

829

1

        assert_eq!(Heuristic::from_str("random"), Ok(Heuristic::Random));

830

1

        assert_eq!(Heuristic::from_str("c"), Ok(Heuristic::Compact));

831

1

        assert_eq!(Heuristic::from_str("i"), Ok(Heuristic::Interactive));

832

1

        assert_eq!(

833

1

            Heuristic::from_str("interactive"),

834

1

            Ok(Heuristic::Interactive)

835

);

836

1

        assert_eq!(Heuristic::from_str("x"), Ok(Heuristic::All));

837

1

        assert_eq!(Channelling::from_str("no"), Ok(Channelling::No));

838

1

        assert_eq!(Channelling::from_str("yes"), Ok(Channelling::Yes));

839

1

        assert_eq!(Channelling::from_str("uniform"), Ok(Channelling::Uniform));

840

1

        assert_eq!(Channelling::Uniform.to_string(), "uniform");

841

1

842

843

    #[test]

844

1

    fn parses_auto_comprehension_expander() {

845

1

        assert_eq!(

846

1

            QuantifiedExpander::from_str("auto"),

847

1

            Ok(QuantifiedExpander::Auto)

848

);

849

1

        assert_eq!(QuantifiedExpander::Auto.to_string(), "auto");

850

1

851

852

    #[test]

853

1

    fn interactive_heuristic_consumes_one_based_responses() {

854

1

        set_heuristic_responses(vec![2, 1]);

855

1

        assert_eq!(next_heuristic_interactive_index(&["left", "right"]), 1);

856

1

        assert_eq!(next_heuristic_interactive_index(&["a", "b", "c"]), 0);

857

1

        clear_heuristic_responses();

858

1

859

860

    #[test]

861

1

    fn random_heuristic_is_reproducible_from_seed() {

862

1

        set_heuristic_seed(42);

863

8

        let first: Vec<_> = (0..8).map(|_| next_heuristic_random_index(7)).collect();

864

1

        set_heuristic_seed(42);

865

8

        let second: Vec<_> = (0..8).map(|_| next_heuristic_random_index(7)).collect();

866

1

        assert_eq!(first, second);

867

1

868

869

    #[test]

870

1

    fn all_heuristic_replays_and_records_choices() {

871

1

        begin_heuristic_all_choices(vec![1]);

872

1

        assert_eq!(next_heuristic_all_index(&["left", "right"]), 1);

873

1

        assert_eq!(

874

1

            heuristic_all_choices()[0].options,

875

1

            vec!["left".to_string(), "right".to_string()]

876

);

877

1

878

879

    #[test]

880

1

    fn parses_rewrite_option_combinations() {

881

1

        assert_eq!(

882

1

            RewriteConfig::from_str("baseline").unwrap(),

883

1

            RewriteConfig {

884

1

                prefilter: false,

885

1

                worklist: false,

886

1

887

);

888

1

        assert_eq!(

889

1

            RewriteConfig::from_str("baseline+prefilter").unwrap(),

890

1

            RewriteConfig {

891

1

                prefilter: true,

892

1

                worklist: false,

893

1

894

);

895

1

        assert_eq!(

896

1

            RewriteConfig::from_str("baseline+worklist").unwrap(),

897

1

            RewriteConfig {

898

1

                prefilter: false,

899

1

                worklist: true,

900

1

901

);

902

1

        assert_eq!(

903

1

            RewriteConfig::from_str("baseline+prefilter+worklist").unwrap(),

904

1

            RewriteConfig::optimised()

905

);

906

1

        assert!(RewriteConfig::from_str("+dirty").is_err());

907

1

        assert!(RewriteConfig::from_str("baseline+dirty").is_err());

908

1

        assert!(RewriteConfig::from_str("baseline+cache").is_err());

909

1

        assert!(RewriteConfig::from_str("baseline+rulememo").is_err());

910

1

        assert!(RewriteConfig::from_str("baseline+candidateindex").is_err());

911

1

        assert!(RewriteConfig::from_str("baseline+dirtyqueues").is_err());

912

1

        assert!(RewriteConfig::from_str("baseline+rule-memo").is_err());

913

1

        assert!(RewriteConfig::from_str("baseline+candidate-index").is_err());

914

1

        assert!(RewriteConfig::from_str("baseline+candidate-node-index").is_err());

915

1

        assert!(RewriteConfig::from_str("baseline+dirty-node-queues").is_err());

916

1

917

918

    #[test]

919

1

    fn optimised_rewrite_config_enables_fast_default_options() {

920

1

        assert_eq!(

921

1

            RewriteConfig::from_str("optimised").unwrap(),

922

1

            RewriteConfig {

923

1

                prefilter: true,

924

1

                worklist: true,

925

1

926

);

927

1

928

929

    #[test]

930

1

    fn displays_rewrite_option_combinations() {

931

1

        assert_eq!(RewriteConfig::baseline().to_string(), "baseline");

932

1

        assert_eq!(

933

1

            RewriteConfig {

934

1

                prefilter: true,

935

1

                worklist: false,

936

1

937

1

            .to_string(),

938

1

            "baseline+prefilter"

939

);

940

1

        assert_eq!(

941

1

            RewriteConfig {

942

1

                prefilter: false,

943

1

                worklist: true,

944

1

945

1

            .to_string(),

946

1

            "baseline+worklist"

947

);

948

1

        assert_eq!(RewriteConfig::optimised().to_string(), "optimised");

949

1

        assert_eq!(

950

1

            RewriteConfig::from_str("baseline+prefilter+worklist")

951

1

                .unwrap()

952

1

                .to_string(),

953

1

            "optimised"

954

);

955

1

956

957

    #[test]

958

1

    fn parses_rewriter_option_combinations() {

959

1

        assert_eq!(

960

1

            Rewriter::from_str("baseline+prefilter").unwrap(),

961

1

            Rewriter::Rewrite(RewriteConfig {

962

1

                prefilter: true,

963

1

                worklist: false,

964

1

})

965

);

966

1

        assert_eq!(

967

1

            Rewriter::from_str("baseline+prefilter+worklist").unwrap(),

968

1

            Rewriter::Rewrite(RewriteConfig::optimised())

969

);

970

1

        assert!(Rewriter::from_str("+dirty").is_err());

971

1

        assert!(Rewriter::from_str("dirty").is_err());

972

1

        assert!(Rewriter::from_str("baseline+dirty").is_err());

973

1

974

975

976

/// Pin the AMO algorithm, or allow the modelling heuristic to choose.

977

300

pub fn set_amo_encoding(encoding: Option<crate::ast::sat_decision::AmoEncoding>) {

978

300

    AMO_ENCODING.with(|current| current.set(encoding));

979

300

980

/// Explicit AMO algorithm override for this compilation thread.

981

2165134

pub fn amo_encoding() -> Option<crate::ast::sat_decision::AmoEncoding> {

982

2165134

    AMO_ENCODING.with(Cell::get)

983

2165134

984

985

/// Pin a cardinality provider/algorithm, or let the heuristic select it.

986

300

pub fn set_cardinality_encoding(encoding: Option<crate::ast::sat_decision::CardinalityEncoding>) {

987

300

    CARDINALITY_ENCODING.with(|current| current.set(encoding));

988

300

989

/// Explicit cardinality encoder override for this compilation thread.

990

216166

pub fn cardinality_encoding() -> Option<crate::ast::sat_decision::CardinalityEncoding> {

991

216166

    CARDINALITY_ENCODING.with(Cell::get)

992

216166

993

994

/// Pin a pseudo-Boolean provider/algorithm, or let the heuristic select it.

995

300

pub fn set_pb_encoding(encoding: Option<crate::ast::sat_decision::PbEncoding>) {

996

300

    PB_ENCODING.with(|current| current.set(encoding));

997

300

998

/// Explicit pseudo-Boolean encoder override for this compilation thread.

999

1206107

pub fn pb_encoding() -> Option<crate::ast::sat_decision::PbEncoding> {

1000

1206107

    PB_ENCODING.with(Cell::get)

1001

1206107

1002

1003

/// Pin the allDifferent strategy, or let the heuristic choose an applicable composition.

1004

300

pub fn set_alldifferent_encoding(encoding: Option<crate::ast::sat_decision::AllDifferentEncoding>) {

1005

300

    ALLDIFFERENT_ENCODING.with(|current| current.set(encoding));

1006

300

1007

/// Explicit allDifferent strategy override for this compilation thread.

1008

63394

pub fn alldifferent_encoding() -> Option<crate::ast::sat_decision::AllDifferentEncoding> {

1009

63394

    ALLDIFFERENT_ENCODING.with(Cell::get)

1010

63394

1011

1012

/// Pin the table composition, or let the modelling heuristic select it.

1013

300

pub fn set_table_encoding(encoding: Option<crate::ast::sat_decision::TableEncoding>) {

1014

300

    TABLE_ENCODING.with(|current| current.set(encoding));

1015

300

1016

/// Explicit table strategy override for this compilation thread.

1017

1432739

pub fn table_encoding() -> Option<crate::ast::sat_decision::TableEncoding> {

1018

1432739

    TABLE_ENCODING.with(Cell::get)

1019

1432739

1020

1021

/// Pin the element composition, or let the modelling heuristic select it.

1022

300

pub fn set_element_encoding(encoding: Option<crate::ast::sat_decision::ElementEncoding>) {

1023

300

    ELEMENT_ENCODING.with(|current| current.set(encoding));

1024

300

1025

/// Explicit element strategy override for this compilation thread.

1026

143202

pub fn element_encoding() -> Option<crate::ast::sat_decision::ElementEncoding> {

1027

143202

    ELEMENT_ENCODING.with(Cell::get)

1028

143202