Grcov report - run.rs

1

#![allow(unreachable_patterns)]

2

#![allow(unsafe_op_in_unsafe_fn)]

3

4

use std::{

5

    cell::Cell,

6

    collections::HashMap,

7

    ffi::{CStr, CString, c_char, c_void},

8

    ptr,

9

    sync::{

10

        LazyLock, Mutex,

11

        atomic::{AtomicPtr, Ordering},

12

},

13

};

14

15

use anyhow::anyhow;

16

17

use crate::{

18

    ast::Tuple,

19

    ffi::{self},

20

};

21

use crate::{

22

    ast::{Constant, Constraint, Model, Var, VarDomain, VarName},

23

    error::{MinionError, check_minion_result},

24

    scoped_ptr::Scoped,

25

};

26

27

/// The callback type used by [`run_minion`].

28

///

29

/// Called by Minion whenever a solution is found. The input is

30

/// a `HashMap` of all named variables along with their value.

31

///

32

/// Return `true` to continue searching, `false` to stop.

33

///

34

/// Since this is a boxed closure, it can capture state from its environment,

35

/// eliminating the need for global or thread-local state in callers.

36

///

37

/// # Examples

38

///

39

/// ```

40

///   use minion_sys::ast::*;

41

///   use minion_sys::run_minion;

42

///   use std::collections::HashMap;

43

///

44

///   let mut all_solutions: Vec<HashMap<VarName,Constant>> = vec![];

45

///

46

///   let callback = Box::new(|solutions: HashMap<VarName,Constant>| -> bool {

47

///       all_solutions.push(solutions);

48

///       true

49

///   });

50

///

51

///   // Build and run the model.

52

///   let mut model = Model::new();

53

///

54

///   // ... omitted for brevity ...

55

/// # model

56

/// #     .named_variables

57

/// #     .add_var("x".to_owned(), VarDomain::Bound(1, 3));

58

/// # model

59

/// #     .named_variables

60

/// #     .add_var("y".to_owned(), VarDomain::Bound(2, 4));

61

/// # model

62

/// #     .named_variables

63

/// #     .add_var("z".to_owned(), VarDomain::Bound(1, 5));

64

/// #

65

/// # let leq = Constraint::SumLeq(

66

/// #     vec![

67

/// #         Var::NameRef("x".to_owned()),

68

/// #         Var::NameRef("y".to_owned()),

69

/// #         Var::NameRef("z".to_owned()),

70

/// #     ],

71

/// #     Var::ConstantAsVar(4),

72

/// # );

73

/// #

74

/// # let geq = Constraint::SumGeq(

75

/// #     vec![

76

/// #         Var::NameRef("x".to_owned()),

77

/// #         Var::NameRef("y".to_owned()),

78

/// #         Var::NameRef("z".to_owned()),

79

/// #     ],

80

/// #     Var::ConstantAsVar(4),

81

/// # );

82

/// #

83

/// # let ineq = Constraint::Ineq(

84

/// #     Var::NameRef("x".to_owned()),

85

/// #     Var::NameRef("y".to_owned()),

86

/// #     Constant::Integer(-1),

87

/// # );

88

/// #

89

/// # model.constraints.push(leq);

90

/// # model.constraints.push(geq);

91

/// # model.constraints.push(ineq);

92

///

93

///   let _solver_ctx = run_minion(model, callback).expect("Error occurred");

94

///

95

///   let solution_set_1 = &all_solutions[0];

96

///   let x1 = solution_set_1.get("x").unwrap();

97

///   let y1 = solution_set_1.get("y").unwrap();

98

///   let z1 = solution_set_1.get("z").unwrap();

99

/// #

100

/// # assert_eq!(all_solutions.len(),1);

101

/// # assert_eq!(*x1,Constant::Integer(1));

102

/// # assert_eq!(*y1,Constant::Integer(2));

103

/// # assert_eq!(*z1,Constant::Integer(1));

104

/// ```

105

pub type Callback<'a> = Box<dyn FnMut(HashMap<VarName, Constant>) -> bool + 'a>;

106

107

/// Value-order strategy for Minion branching.

108

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

109

pub enum ValueOrder {

110

    Ascend,

111

    Descend,

112

    Random,

113

114

115

/// Optional runtime controls for [`run_minion_with_options`].

116

#[derive(Debug, Clone, Copy, Default)]

117

pub struct RunOptions {

118

    /// Override Minion value ordering.

119

///

120

    /// When unset, Minion keeps its default behaviour (or whatever was encoded

121

    /// in the input model).

122

    pub value_order: Option<ValueOrder>,

123

124

125

/// State passed through the C callback's `void* userdata` pointer.

126

///

127

/// This replaces the old thread-local approach — all callback state is now

128

/// passed explicitly through the FFI userdata mechanism.

129

struct CallbackState<'a> {

130

    callback: Callback<'a>,

131

    print_vars: Vec<VarName>,

132

133

134

static CURRENT_INSTANCE: AtomicPtr<ffi::ProbSpec_CSPInstance> = AtomicPtr::new(ptr::null_mut());

135

static CURRENT_CTX: AtomicPtr<ffi::MinionContext> = AtomicPtr::new(ptr::null_mut());

136

304

static MINION_RUN_LOCK: LazyLock<Mutex<()>> = LazyLock::new(|| Mutex::new(()));

137

thread_local! {

138

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

139

140

141

/// Opaque handle to a Minion solver context.

142

///

143

/// Holds solver state (including run statistics) after a solve completes.

144

/// Query results (e.g. via [`SolverContext::get_from_table`]) before dropping.

145

pub struct SolverContext {

146

    ctx: *mut ffi::MinionContext,

147

148

149

// Safety: MinionContext is an independent solver instance. It is safe to send

150

// between threads as long as it is not used concurrently (which we ensure by

151

// only accessing it through &mut self or after the solve completes).

152

unsafe impl Send for SolverContext {}

153

154

impl SolverContext {

155

    /// Gets a value from Minion's TableOut (where it stores run statistics).

156

36704

    pub fn get_from_table(&self, key: String) -> Option<String> {

157

        unsafe {

158

            #[allow(clippy::expect_used)]

159

36704

            let c_string = CString::new(key).expect("");

160

36704

            let key_ptr = c_string.into_raw();

161

36704

            let val_ptr: *mut c_char = ffi::TableOut_get(self.ctx, key_ptr);

162

163

36704

            drop(CString::from_raw(key_ptr));

164

165

36704

            if val_ptr.is_null() {

166

                None

167

            } else {

168

                #[allow(clippy::unwrap_used)]

169

36704

                let res = CStr::from_ptr(val_ptr).to_str().unwrap().to_owned();

170

36704

                libc::free(val_ptr as _);

171

36704

                Some(res)

172

173

174

36704

175

176

177

impl Drop for SolverContext {

178

36760

    fn drop(&mut self) {

179

36760

        unsafe {

180

36760

            ffi::minion_freeContext(self.ctx);

181

36760

182

36760

183

184

185

/// The C callback passed to `runMinion`. Receives the active context and our

186

/// `CallbackState` via the userdata pointer.

187

992514

unsafe extern "C" fn run_callback(ctx: *mut ffi::MinionContext, userdata: *mut c_void) -> bool {

188

    // Safety: userdata is a pointer to our CallbackState, set by run_minion

189

    // and valid for the duration of the runMinion call.

190

992514

    let state = unsafe { &mut *(userdata as *mut CallbackState<'_>) };

191

192

992514

    if state.print_vars.is_empty() {

193

908

        return true;

194

991606

195

196

    // Build solutions HashMap by reading variable values from Minion.

197

991606

    let mut solutions: HashMap<VarName, Constant> = HashMap::new();

198

7381976

    for (i, var) in state.print_vars.iter().enumerate() {

199

7381976

        let solution_int: i32 = unsafe { ffi::printMatrix_getValue(ctx, i as _) };

200

7381976

        let solution: Constant = Constant::Integer(solution_int);

201

7381976

        solutions.insert(var.to_string(), solution);

202

7381976

203

204

991606

    INSIDE_MINION_CALLBACK.with(|flag| flag.set(true));

205

991606

    let continue_search = (state.callback)(solutions);

206

991606

    INSIDE_MINION_CALLBACK.with(|flag| flag.set(false));

207

991606

    continue_search

208

992514

209

210

/// Run Minion on the given [Model].

211

///

212

/// The given [callback](Callback) is ran whenever a new solution set is found.

213

///

214

/// Returns a [`SolverContext`] on success, which can be used to query run

215

/// statistics via [`SolverContext::get_from_table`].

216

#[allow(clippy::unwrap_used)]

217

140

pub fn run_minion(model: Model, callback: Callback<'_>) -> Result<SolverContext, MinionError> {

218

140

    run_minion_with_options(model, callback, RunOptions::default())

219

140

220

221

/// Like [`run_minion`], but allows configuring selected Minion runtime options.

222

#[allow(clippy::unwrap_used)]

223

36760

pub fn run_minion_with_options(

224

36760

    model: Model,

225

36760

    callback: Callback<'_>,

226

36760

    options: RunOptions,

227

36760

) -> Result<SolverContext, MinionError> {

228

36760

    let _run_guard = MINION_RUN_LOCK.lock().unwrap();

229

36760

    let mut state = CallbackState {

230

36760

        callback,

231

36760

        print_vars: vec![],

232

36760

};

233

234

    unsafe {

235

36760

        let ctx = ffi::minion_newContext();

236

36760

        let search_opts = ffi::searchOptions_new();

237

36760

        let search_method = ffi::searchMethod_new();

238

36760

        let search_instance = ffi::instance_new();

239

36760

        CURRENT_INSTANCE.store(search_instance, Ordering::SeqCst);

240

36760

        CURRENT_CTX.store(ctx, Ordering::SeqCst);

241

242

        // Use Minion as a quiet library by default. Low-level FFI callers that

243

        // want native solver output can opt out by configuring SearchOptions

244

        // themselves instead of going through this wrapper.

245

36760

        (*search_opts).silent = true;

246

36760

        (*search_opts).print_solution = false;

247

36760

        if let Some(value_order) = options.value_order {

248

            let value_order = match value_order {

249

                ValueOrder::Ascend => ffi::ValOrderEnum_VALORDER_ASCEND,

250

                ValueOrder::Descend => ffi::ValOrderEnum_VALORDER_DESCEND,

251

                ValueOrder::Random => ffi::ValOrderEnum_VALORDER_RANDOM,

252

};

253

            (*search_method).valorder = ffi::ValOrder {

254

                type_: value_order,

255

                bias: 0,

256

};

257

36760

258

259

36760

        convert_model_to_raw(search_instance, &model, &mut state.print_vars)?;

260

261

36760

        let userdata = &mut state as *mut CallbackState<'_> as *mut c_void;

262

36760

        let res = ffi::runMinion(

263

36760

            ctx,

264

36760

            search_opts,

265

36760

            search_method,

266

36760

            search_instance,

267

36760

            Some(run_callback),

268

36760

            userdata,

269

);

270

271

36760

        ffi::searchMethod_free(search_method);

272

36760

        ffi::searchOptions_free(search_opts);

273

36760

        CURRENT_INSTANCE.store(ptr::null_mut(), Ordering::SeqCst);

274

36760

        CURRENT_CTX.store(ptr::null_mut(), Ordering::SeqCst);

275

36760

        ffi::instance_free(search_instance);

276

277

36760

        match check_minion_result(res) {

278

36760

            Ok(()) => Ok(SolverContext { ctx }),

279

            Err(e) => {

280

                ffi::minion_freeContext(ctx);

281

                Err(MinionError::from(e))

282

283

284

285

36760

286

287

/// Adds a new auxiliary variable to the currently-running Minion instance.

288

///

289

/// This is intended for use from a solver callback while `run_minion` is active.

290

8232

pub fn add_aux_var_during_search(name: VarName, domain: VarDomain) -> Result<(), MinionError> {

291

8232

    let instance = CURRENT_INSTANCE.load(Ordering::SeqCst);

292

8232

    let ctx = CURRENT_CTX.load(Ordering::SeqCst);

293

8232

    let inside_callback = INSIDE_MINION_CALLBACK.with(|flag| flag.get());

294

8232

    if instance.is_null() || ctx.is_null() || !inside_callback {

295

        return Err(MinionError::Other(anyhow!(

296

            "cannot add a Minion variable outside an active callback"

297

        )));

298

8232

299

300

8232

    let c_str = CString::new(name.clone())

301

8232

        .map_err(|_| anyhow!("variable name {:?} contains a null character", name))?;

302

303

8232

    let (vartype_raw, domain_low, domain_high) = match domain {

304

        VarDomain::Bound(a, b) => Ok((ffi::VariableType_VAR_BOUND, a, b)),

305

3024

        VarDomain::Discrete(a, b) => Ok((ffi::VariableType_VAR_DISCRETE, a, b)),

306

5208

        VarDomain::Bool => Ok((ffi::VariableType_VAR_BOOL, 0, 1)),

307

        x => Err(MinionError::NotImplemented(format!("{x:?}"))),

308

}?;

309

310

    unsafe {

311

8232

        check_minion_result(ffi::minion_newVarMidsearch(

312

8232

            ctx,

313

8232

            instance,

314

8232

            c_str.as_ptr() as *mut c_char,

315

8232

            vartype_raw,

316

8232

            domain_low,

317

8232

            domain_high,

318

        ))?;

319

320

321

8232

    Ok(())

322

8232

323

324

/// Adds a constraint to the currently-running Minion instance.

325

///

326

/// This is intended for use from a solver callback while `run_minion` is active.

327

7224

pub fn add_constraint_during_search(constraint: Constraint) -> Result<(), MinionError> {

328

7224

    let instance = CURRENT_INSTANCE.load(Ordering::SeqCst);

329

7224

    let ctx = CURRENT_CTX.load(Ordering::SeqCst);

330

7224

    let inside_callback = INSIDE_MINION_CALLBACK.with(|flag| flag.get());

331

7224

    if instance.is_null() || ctx.is_null() || !inside_callback {

332

        return Err(MinionError::Other(anyhow!(

333

            "cannot add a Minion constraint outside an active callback"

334

        )));

335

7224

336

337

    unsafe {

338

7224

        let constraint_type = get_constraint_type(&constraint)?;

339

7224

        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {

340

7224

            ffi::constraint_free(x as _)

341

7224

});

342

343

7224

        constraint_add_args(instance, raw_constraint.ptr, &constraint)?;

344

7224

        check_minion_result(ffi::minion_addConstraintMidsearch(

345

7224

            ctx,

346

7224

            instance,

347

7224

            raw_constraint.ptr,

348

        ))?;

349

350

351

7224

    Ok(())

352

7224

353

354

36760

unsafe fn convert_model_to_raw(

355

36760

    instance: *mut ffi::ProbSpec_CSPInstance,

356

36760

    model: &Model,

357

36760

    print_vars: &mut Vec<VarName>,

358

36760

) -> Result<(), MinionError> {

359

    /*******************************/

360

    /*        Add variables        */

361

    /*******************************/

362

363

/*

364

     * Add variables to:

365

     * 1. symbol table

366

     * 2. print matrix

367

     * 3. search vars

368

369

     * These are all done in the order saved in the SymbolTable.

370

*/

371

372

36760

    let search_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));

373

374

    // initialise all variables, and add all variables to the print order

375

221420

    for var_name in model.named_variables.get_variable_order() {

376

221420

        let c_str = CString::new(var_name.clone()).map_err(|_| {

377

            anyhow!(

378

                "Variable name {:?} contains a null character.",

379

                var_name.clone()

380

381

        })?;

382

383

221420

        let vartype = model

384

221420

            .named_variables

385

221420

            .get_vartype(var_name.clone())

386

221420

            .ok_or(anyhow!("Could not get var type for {:?}", var_name.clone()))?;

387

388

221420

        let (vartype_raw, domain_low, domain_high) = match vartype {

389

19130

            VarDomain::Bound(a, b) => Ok((ffi::VariableType_VAR_BOUND, a, b)),

390

179260

            VarDomain::Discrete(a, b) => Ok((ffi::VariableType_VAR_DISCRETE, a, b)),

391

23030

            VarDomain::Bool => Ok((ffi::VariableType_VAR_BOOL, 0, 1)), // TODO: will this work?

392

            x => Err(MinionError::NotImplemented(format!("{x:?}"))),

393

}?;

394

395

221420

        check_minion_result(ffi::minion_newVar(

396

221420

            instance,

397

221420

            c_str.as_ptr() as *mut c_char,

398

221420

            vartype_raw,

399

221420

            domain_low,

400

221420

            domain_high,

401

        ))?;

402

403

221420

        let var_result = ffi::minion_getVarByName(instance, c_str.as_ptr() as _);

404

221420

        check_minion_result(var_result.result)?;

405

221420

        let var = var_result.var;

406

407

221420

        ffi::printMatrix_addVar(instance, var);

408

409

        // Remember the order for the callback function.

410

221420

        print_vars.push(var_name.clone());

411

412

413

    // only add search variables to search order

414

90358

    for search_var_name in model.named_variables.get_search_variable_order() {

415

90358

        let c_str = CString::new(search_var_name.clone()).map_err(|_| {

416

            anyhow!(

417

                "Variable name {:?} contains a null character.",

418

                search_var_name.clone()

419

420

        })?;

421

90358

        let var_result = ffi::minion_getVarByName(instance, c_str.as_ptr() as _);

422

90358

        check_minion_result(var_result.result)?;

423

90358

        ffi::vec_var_push_back(search_vars.ptr, var_result.var);

424

425

426

36760

    let search_order = Scoped::new(

427

36760

        ffi::searchOrder_new(search_vars.ptr, ffi::VarOrderEnum_ORDER_STATIC, false),

428

36760

        |x| ffi::searchOrder_free(x as _),

429

);

430

431

36760

    ffi::instance_addSearchOrder(instance, search_order.ptr);

432

433

    /*********************************/

434

    /*        Add constraints        */

435

    /*********************************/

436

437

139208

    for constraint in &model.constraints {

438

        // 1. get constraint type and create C++ constraint object

439

        // 2. run through arguments and add them to the constraint

440

        // 3. add constraint to instance

441

442

139208

        let constraint_type = get_constraint_type(constraint)?;

443

139208

        let raw_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {

444

139208

            ffi::constraint_free(x as _)

445

139208

});

446

447

139208

        constraint_add_args(instance, raw_constraint.ptr, constraint)?;

448

139208

        ffi::instance_addConstraint(instance, raw_constraint.ptr);

449

450

451

36760

    Ok(())

452

36760

453

454

229308

unsafe fn get_constraint_type(constraint: &Constraint) -> Result<u32, MinionError> {

455

229308

    match constraint {

456

24158

        Constraint::SumGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQSUM),

457

21194

        Constraint::SumLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQSUM),

458

31826

        Constraint::Ineq(_, _, _) => Ok(ffi::ConstraintType_CT_INEQ),

459

20002

        Constraint::Eq(_, _) => Ok(ffi::ConstraintType_CT_EQ),

460

        Constraint::Difference(_, _) => Ok(ffi::ConstraintType_CT_DIFFERENCE),

461

        Constraint::Div(_, _) => Ok(ffi::ConstraintType_CT_DIV),

462

3752

        Constraint::DivUndefZero(_, _) => Ok(ffi::ConstraintType_CT_DIV_UNDEFZERO),

463

        Constraint::Modulo(_, _) => Ok(ffi::ConstraintType_CT_MODULO),

464

1232

        Constraint::ModuloUndefZero(_, _) => Ok(ffi::ConstraintType_CT_MODULO_UNDEFZERO),

465

950

        Constraint::Pow(_, _) => Ok(ffi::ConstraintType_CT_POW),

466

1624

        Constraint::Product(_, _) => Ok(ffi::ConstraintType_CT_PRODUCT2),

467

6048

        Constraint::WeightedSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTGEQSUM),

468

6720

        Constraint::WeightedSumLeq(_, _, _) => Ok(ffi::ConstraintType_CT_WEIGHTLEQSUM),

469

        Constraint::CheckAssign(_) => Ok(ffi::ConstraintType_CT_CHECK_ASSIGN),

470

        Constraint::CheckGsa(_) => Ok(ffi::ConstraintType_CT_CHECK_GSA),

471

        Constraint::ForwardChecking(_) => Ok(ffi::ConstraintType_CT_FORWARD_CHECKING),

472

13248

        Constraint::Reify(_, _) => Ok(ffi::ConstraintType_CT_REIFY),

473

3684

        Constraint::ReifyImply(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY),

474

        Constraint::ReifyImplyQuick(_, _) => Ok(ffi::ConstraintType_CT_REIFYIMPLY_QUICK),

475

16688

        Constraint::WatchedAnd(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_AND),

476

14630

        Constraint::WatchedOr(_) => Ok(ffi::ConstraintType_CT_WATCHED_NEW_OR),

477

        Constraint::GacAllDiff(_) => Ok(ffi::ConstraintType_CT_GACALLDIFF),

478

2482

        Constraint::AllDiff(_) => Ok(ffi::ConstraintType_CT_ALLDIFF),

479

        Constraint::AllDiffMatrix(_, _) => Ok(ffi::ConstraintType_CT_ALLDIFFMATRIX),

480

        Constraint::WatchSumGeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_GEQSUM),

481

        Constraint::WatchSumLeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LEQSUM),

482

        Constraint::OccurrenceGeq(_, _, _) => Ok(ffi::ConstraintType_CT_GEQ_OCCURRENCE),

483

        Constraint::OccurrenceLeq(_, _, _) => Ok(ffi::ConstraintType_CT_LEQ_OCCURRENCE),

484

        Constraint::Occurrence(_, _, _) => Ok(ffi::ConstraintType_CT_OCCURRENCE),

485

        Constraint::LitSumGeq(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_LITSUM),

486

        Constraint::Gcc(_, _, _) => Ok(ffi::ConstraintType_CT_GCC),

487

        Constraint::GccWeak(_, _, _) => Ok(ffi::ConstraintType_CT_GCCWEAK),

488

        Constraint::LexLeqRv(_, _) => Ok(ffi::ConstraintType_CT_GACLEXLEQ),

489

336

        Constraint::LexLeq(_, _) => Ok(ffi::ConstraintType_CT_LEXLEQ),

490

224

        Constraint::LexLess(_, _) => Ok(ffi::ConstraintType_CT_LEXLESS),

491

        Constraint::LexLeqQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),

492

        Constraint::LexLessQuick(_, _) => Ok(ffi::ConstraintType_CT_QUICK_LEXLEQ),

493

        Constraint::WatchVecNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VECNEQ),

494

        Constraint::WatchVecExistsLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_VEC_OR_LESS),

495

        Constraint::Hamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_HAMMING),

496

        Constraint::NotHamming(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_HAMMING),

497

        Constraint::FrameUpdate(_, _, _, _, _) => Ok(ffi::ConstraintType_CT_FRAMEUPDATE),

498

84

        Constraint::NegativeTable(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEGATIVE_TABLE),

499

364

        Constraint::Table(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_TABLE),

500

        Constraint::GacSchema(_, _) => Ok(ffi::ConstraintType_CT_GACSCHEMA),

501

        Constraint::LightTable(_, _) => Ok(ffi::ConstraintType_CT_LIGHTTABLE),

502

        Constraint::Mddc(_, _) => Ok(ffi::ConstraintType_CT_MDDC),

503

        Constraint::NegativeMddc(_, _) => Ok(ffi::ConstraintType_CT_NEGATIVEMDDC),

504

        Constraint::Str2Plus(_, _) => Ok(ffi::ConstraintType_CT_STR),

505

        Constraint::Max(_, _) => Ok(ffi::ConstraintType_CT_MAX),

506

        Constraint::Min(_, _) => Ok(ffi::ConstraintType_CT_MIN),

507

        Constraint::NvalueGeq(_, _) => Ok(ffi::ConstraintType_CT_GEQNVALUE),

508

        Constraint::NvalueLeq(_, _) => Ok(ffi::ConstraintType_CT_LEQNVALUE),

509

        Constraint::Element(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT),

510

10474

        Constraint::ElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_ONE),

511

        Constraint::ElementUndefZero(_, _, _) => Ok(ffi::ConstraintType_CT_ELEMENT_UNDEFZERO),

512

        Constraint::WatchElement(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT),

513

        Constraint::WatchElementOne(_, _, _) => Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE),

514

        Constraint::WatchElementOneUndefZero(_, _, _) => {

515

            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_ONE_UNDEFZERO)

516

517

        Constraint::WatchElementUndefZero(_, _, _) => {

518

            Ok(ffi::ConstraintType_CT_WATCHED_ELEMENT_UNDEFZERO)

519

520

22914

        Constraint::WLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LIT),

521

        Constraint::WNotLiteral(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOTLIT),

522

448

        Constraint::WInIntervalSet(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_ININTERVALSET),

523

        Constraint::WInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INRANGE),

524

2014

        Constraint::WInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_INSET),

525

        Constraint::WNotInRange(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INRANGE),

526

        Constraint::WNotInset(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NOT_INSET),

527

1344

        Constraint::Abs(_, _) => Ok(ffi::ConstraintType_CT_ABS),

528

10600

        Constraint::DisEq(_, _) => Ok(ffi::ConstraintType_CT_DISEQ),

529

672

        Constraint::MinusEq(_, _) => Ok(ffi::ConstraintType_CT_MINUSEQ),

530

        Constraint::GacEq(_, _) => Ok(ffi::ConstraintType_CT_GACEQ),

531

        Constraint::WatchLess(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_LESS),

532

        Constraint::WatchNeq(_, _) => Ok(ffi::ConstraintType_CT_WATCHED_NEQ),

533

8348

        Constraint::True => Ok(ffi::ConstraintType_CT_TRUE),

534

3248

        Constraint::False => Ok(ffi::ConstraintType_CT_FALSE),

535

536

        #[allow(unreachable_patterns)]

537

        x => Err(MinionError::NotImplemented(format!(

538

            "Constraint not implemented {x:?}",

539

        ))),

540

541

229308

542

543

229308

unsafe fn constraint_add_args(

544

229308

    i: *mut ffi::ProbSpec_CSPInstance,

545

229308

    r_constr: *mut ffi::ProbSpec_ConstraintBlob,

546

229308

    constr: &Constraint,

547

229308

) -> Result<(), MinionError> {

548

229308

    match constr {

549

24158

        Constraint::SumGeq(lhs_vars, rhs_var) => {

550

24158

            read_list(i, r_constr, lhs_vars)?;

551

24158

            read_var(i, r_constr, rhs_var)?;

552

24158

            Ok(())

553

554

21194

        Constraint::SumLeq(lhs_vars, rhs_var) => {

555

21194

            read_list(i, r_constr, lhs_vars)?;

556

21194

            read_var(i, r_constr, rhs_var)?;

557

21194

            Ok(())

558

559

31826

        Constraint::Ineq(var1, var2, c) => {

560

31826

            read_var(i, r_constr, var1)?;

561

31826

            read_var(i, r_constr, var2)?;

562

31826

            read_constant(r_constr, c)?;

563

31826

            Ok(())

564

565

20002

        Constraint::Eq(var1, var2) => {

566

20002

            read_var(i, r_constr, var1)?;

567

20002

            read_var(i, r_constr, var2)?;

568

20002

            Ok(())

569

570

        Constraint::Difference((a, b), c) => {

571

            read_2_vars(i, r_constr, a, b)?;

572

            read_var(i, r_constr, c)?;

573

            Ok(())

574

575

        Constraint::Div((a, b), c) => {

576

            read_2_vars(i, r_constr, a, b)?;

577

            read_var(i, r_constr, c)?;

578

            Ok(())

579

580

3752

        Constraint::DivUndefZero((a, b), c) => {

581

3752

            read_2_vars(i, r_constr, a, b)?;

582

3752

            read_var(i, r_constr, c)?;

583

3752

            Ok(())

584

585

        Constraint::Modulo((a, b), c) => {

586

            read_2_vars(i, r_constr, a, b)?;

587

            read_var(i, r_constr, c)?;

588

            Ok(())

589

590

1232

        Constraint::ModuloUndefZero((a, b), c) => {

591

1232

            read_2_vars(i, r_constr, a, b)?;

592

1232

            read_var(i, r_constr, c)?;

593

1232

            Ok(())

594

595

950

        Constraint::Pow((a, b), c) => {

596

950

            read_2_vars(i, r_constr, a, b)?;

597

950

            read_var(i, r_constr, c)?;

598

950

            Ok(())

599

600

1624

        Constraint::Product((a, b), c) => {

601

1624

            read_2_vars(i, r_constr, a, b)?;

602

1624

            read_var(i, r_constr, c)?;

603

1624

            Ok(())

604

605

6048

        Constraint::WeightedSumGeq(a, b, c) => {

606

6048

            read_constant_list(r_constr, a)?;

607

6048

            read_list(i, r_constr, b)?;

608

6048

            read_var(i, r_constr, c)?;

609

6048

            Ok(())

610

611

6720

        Constraint::WeightedSumLeq(a, b, c) => {

612

6720

            read_constant_list(r_constr, a)?;

613

6720

            read_list(i, r_constr, b)?;

614

6720

            read_var(i, r_constr, c)?;

615

6720

            Ok(())

616

617

        Constraint::CheckAssign(a) => {

618

            read_constraint(i, r_constr, (**a).clone())?;

619

            Ok(())

620

621

        Constraint::CheckGsa(a) => {

622

            read_constraint(i, r_constr, (**a).clone())?;

623

            Ok(())

624

625

        Constraint::ForwardChecking(a) => {

626

            read_constraint(i, r_constr, (**a).clone())?;

627

            Ok(())

628

629

13248

        Constraint::Reify(a, b) => {

630

13248

            read_constraint(i, r_constr, (**a).clone())?;

631

13248

            read_var(i, r_constr, b)?;

632

13248

            Ok(())

633

634

3684

        Constraint::ReifyImply(a, b) => {

635

3684

            read_constraint(i, r_constr, (**a).clone())?;

636

3684

            read_var(i, r_constr, b)?;

637

3684

            Ok(())

638

639

        Constraint::ReifyImplyQuick(a, b) => {

640

            read_constraint(i, r_constr, (**a).clone())?;

641

            read_var(i, r_constr, b)?;

642

            Ok(())

643

644

16688

        Constraint::WatchedAnd(a) => {

645

16688

            read_constraint_list(i, r_constr, a)?;

646

16688

            Ok(())

647

648

14630

        Constraint::WatchedOr(a) => {

649

14630

            read_constraint_list(i, r_constr, a)?;

650

14630

            Ok(())

651

652

        Constraint::GacAllDiff(a) => {

653

            read_list(i, r_constr, a)?;

654

            Ok(())

655

656

2482

        Constraint::AllDiff(a) => {

657

2482

            read_list(i, r_constr, a)?;

658

2482

            Ok(())

659

660

        Constraint::AllDiffMatrix(a, b) => {

661

            read_list(i, r_constr, a)?;

662

            read_constant(r_constr, b)?;

663

            Ok(())

664

665

        Constraint::WatchSumGeq(a, b) => {

666

            read_list(i, r_constr, a)?;

667

            read_constant(r_constr, b)?;

668

            Ok(())

669

670

        Constraint::WatchSumLeq(a, b) => {

671

            read_list(i, r_constr, a)?;

672

            read_constant(r_constr, b)?;

673

            Ok(())

674

675

        Constraint::OccurrenceGeq(a, b, c) => {

676

            read_list(i, r_constr, a)?;

677

            read_constant(r_constr, b)?;

678

            read_constant(r_constr, c)?;

679

            Ok(())

680

681

        Constraint::OccurrenceLeq(a, b, c) => {

682

            read_list(i, r_constr, a)?;

683

            read_constant(r_constr, b)?;

684

            read_constant(r_constr, c)?;

685

            Ok(())

686

687

        Constraint::Occurrence(a, b, c) => {

688

            read_list(i, r_constr, a)?;

689

            read_constant(r_constr, b)?;

690

            read_var(i, r_constr, c)?;

691

            Ok(())

692

693

224

        Constraint::LexLess(a, b) => {

694

224

            read_list(i, r_constr, a)?;

695

224

            read_list(i, r_constr, b)?;

696

224

            Ok(())

697

698

336

        Constraint::LexLeq(a, b) => {

699

336

            read_list(i, r_constr, a)?;

700

336

            read_list(i, r_constr, b)?;

701

336

            Ok(())

702

703

        Constraint::WatchVecNeq(a, b) => {

704

            read_list(i, r_constr, a)?;

705

            read_list(i, r_constr, b)?;

706

            Ok(())

707

708

        //Constraint::LitSumGeq(_, _, _) => todo!(),

709

        //Constraint::Gcc(_, _, _) => todo!(),

710

        //Constraint::GccWeak(_, _, _) => todo!(),

711

        //Constraint::LexLeqRv(_, _) => todo!(),

712

        //Constraint::LexLeqQuick(_, _) => todo!(),

713

        //Constraint::LexLessQuick(_, _) => todo!(),

714

        //Constraint::WatchVecExistsLess(_, _) => todo!(),

715

        //Constraint::Hamming(_, _, _) => todo!(),

716

        //Constraint::NotHamming(_, _, _) => todo!(),

717

        //Constraint::FrameUpdate(_, _, _, _, _) => todo!(),

718

364

        Constraint::NegativeTable(vars, tuple_list) | Constraint::Table(vars, tuple_list) => {

719

448

            read_list(i, r_constr, vars)?;

720

448

            read_tuple_list(r_constr, tuple_list)?;

721

448

            Ok(())

722

723

        //Constraint::GacSchema(_, _) => todo!(),

724

        //Constraint::LightTable(_, _) => todo!(),

725

        //Constraint::Mddc(_, _) => todo!(),

726

        //Constraint::NegativeMddc(_, _) => todo!(),

727

        //Constraint::Str2Plus(_, _) => todo!(),

728

        //Constraint::Max(_, _) => todo!(),

729

        //Constraint::Min(_, _) => todo!(),

730

        //Constraint::NvalueGeq(_, _) => todo!(),

731

        //Constraint::NvalueLeq(_, _) => todo!(),

732

        //Constraint::Element(_, _, _) => todo!(),

733

        //Constraint::ElementUndefZero(_, _, _) => todo!(),

734

        //Constraint::WatchElement(_, _, _) => todo!(),

735

        //Constraint::WatchElementOne(_, _, _) => todo!(),

736

10474

        Constraint::ElementOne(vec, j, e) => {

737

10474

            read_list(i, r_constr, vec)?;

738

10474

            read_var(i, r_constr, j)?;

739

10474

            read_var(i, r_constr, e)?;

740

10474

            Ok(())

741

742

        //Constraint::WatchElementOneUndefZero(_, _, _) => todo!(),

743

        //Constraint::WatchElementUndefZero(_, _, _) => todo!(),

744

22914

        Constraint::WLiteral(a, b) => {

745

22914

            read_var(i, r_constr, a)?;

746

22914

            read_constant(r_constr, b)?;

747

22914

            Ok(())

748

749

        //Constraint::WNotLiteral(_, _) => todo!(),

750

448

        Constraint::WInIntervalSet(var, consts) => {

751

448

            read_var(i, r_constr, var)?;

752

448

            read_constant_list(r_constr, consts)?;

753

448

            Ok(())

754

755

        //Constraint::WInRange(_, _) => todo!(),

756

2014

        Constraint::WInset(a, b) => {

757

2014

            read_var(i, r_constr, a)?;

758

2014

            read_constant_list(r_constr, b)?;

759

2014

            Ok(())

760

761

        //Constraint::WNotInRange(_, _) => todo!(),

762

        //Constraint::WNotInset(_, _) => todo!(),

763

1344

        Constraint::Abs(a, b) => {

764

1344

            read_var(i, r_constr, a)?;

765

1344

            read_var(i, r_constr, b)?;

766

1344

            Ok(())

767

768

10600

        Constraint::DisEq(a, b) => {

769

10600

            read_var(i, r_constr, a)?;

770

10600

            read_var(i, r_constr, b)?;

771

10600

            Ok(())

772

773

672

        Constraint::MinusEq(a, b) => {

774

672

            read_var(i, r_constr, a)?;

775

672

            read_var(i, r_constr, b)?;

776

672

            Ok(())

777

778

        //Constraint::GacEq(_, _) => todo!(),

779

        //Constraint::WatchLess(_, _) => todo!(),

780

        // TODO: ensure that this is a bool?

781

        Constraint::WatchNeq(a, b) => {

782

            read_var(i, r_constr, a)?;

783

            read_var(i, r_constr, b)?;

784

            Ok(())

785

786

787

8348

        Constraint::True => Ok(()),

788

3248

        Constraint::False => Ok(()),

789

        #[allow(unreachable_patterns)]

790

        x => Err(MinionError::NotImplemented(format!("{x:?}"))),

791

792

229308

793

794

// DO NOT call manually - this assumes that all needed vars are already in the symbol table.

795

// TODO not happy with this just assuming the name is in the symbol table

796

/// Resolve an AST Var to a raw FFI Var.

797

482562

unsafe fn resolve_var(

798

482562

    instance: *mut ffi::ProbSpec_CSPInstance,

799

482562

    var: &Var,

800

482562

) -> Result<ffi::ProbSpec_Var, MinionError> {

801

482562

    match var {

802

377454

        Var::NameRef(name) => {

803

377454

            let c_str = CString::new(name.clone()).map_err(|_| {

804

                anyhow!(

805

                    "Variable name {:?} contains a null character.",

806

                    name.clone()

807

808

            })?;

809

377454

            let var_result = ffi::minion_getVarByName(instance, c_str.as_ptr() as _);

810

377454

            check_minion_result(var_result.result)?;

811

377454

            Ok(var_result.var)

812

813

105108

        Var::ConstantAsVar(n) => Ok(ffi::constantAsVar(*n)),

814

815

482562

816

817

72644

unsafe fn read_list(

818

72644

    instance: *mut ffi::ProbSpec_CSPInstance,

819

72644

    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,

820

72644

    vars: &Vec<Var>,

821

72644

) -> Result<(), MinionError> {

822

72644

    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));

823

209624

    for var in vars {

824

209624

        let raw_var = resolve_var(instance, var)?;

825

209624

        ffi::vec_var_push_back(raw_vars.ptr, raw_var);

826

827

828

72644

    ffi::constraint_addList(raw_constraint, raw_vars.ptr);

829

830

72644

    Ok(())

831

72644

832

833

257822

unsafe fn read_var(

834

257822

    instance: *mut ffi::ProbSpec_CSPInstance,

835

257822

    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,

836

257822

    var: &Var,

837

257822

) -> Result<(), MinionError> {

838

257822

    let raw_vars = Scoped::new(ffi::vec_var_new(), |x| ffi::vec_var_free(x as _));

839

257822

    let raw_var = resolve_var(instance, var)?;

840

257822

    ffi::vec_var_push_back(raw_vars.ptr, raw_var);

841

257822

    ffi::constraint_addList(raw_constraint, raw_vars.ptr);

842

843

257822

    Ok(())

844

257822

845

846

7558

unsafe fn read_2_vars(

847

7558

    instance: *mut ffi::ProbSpec_CSPInstance,

848

7558

    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,

849

7558

    var1: &Var,

850

7558

    var2: &Var,

851

7558

) -> Result<(), MinionError> {

852

7558

    let mut raw_var = resolve_var(instance, var1)?;

853

7558

    let mut raw_var2 = resolve_var(instance, var2)?;

854

    // todo: does this move or copy? I am confus!

855

    // TODO need to mkae the semantics of move vs copy / ownership clear in libminion!!

856

    // This shouldve leaked everywhere by now but i think libminion copies stuff??

857

7558

    ffi::constraint_addTwoVars(raw_constraint, &mut raw_var, &mut raw_var2);

858

7558

    Ok(())

859

7558

860

861

54740

unsafe fn read_constant(

862

54740

    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,

863

54740

    constant: &Constant,

864

54740

) -> Result<(), MinionError> {

865

54740

    let val: i32 = match constant {

866

54740

        Constant::Integer(n) => Ok(*n),

867

        Constant::Bool(true) => Ok(1),

868

        Constant::Bool(false) => Ok(0),

869

        x => Err(MinionError::NotImplemented(format!("{x:?}"))),

870

}?;

871

872

54740

    ffi::constraint_addConstant(raw_constraint, val);

873

874

54740

    Ok(())

875

54740

876

877

15230

unsafe fn read_constant_list(

878

15230

    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,

879

15230

    constants: &[Constant],

880

15230

) -> Result<(), MinionError> {

881

15230

    let raw_consts = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_int_free(x as _));

882

883

57088

    for constant in constants.iter() {

884

57088

        let val = match constant {

885

57032

            Constant::Integer(n) => Ok(*n),

886

28

            Constant::Bool(true) => Ok(1),

887

28

            Constant::Bool(false) => Ok(0),

888

            #[allow(unreachable_patterns)] // TODO: can there be other types?

889

            x => Err(MinionError::NotImplemented(format!("{x:?}"))),

890

}?;

891

892

57088

        ffi::vec_int_push_back(raw_consts.ptr, val);

893

894

895

15230

    ffi::constraint_addConstantList(raw_constraint, raw_consts.ptr);

896

15230

    Ok(())

897

15230

898

899

//TODO: check if the inner constraint is listed in the model or not?

900

//Does this matter?

901

// TODO: type-check inner constraints vars and tuples and so on?

902

16932

unsafe fn read_constraint(

903

16932

    instance: *mut ffi::ProbSpec_CSPInstance,

904

16932

    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,

905

16932

    inner_constraint: Constraint,

906

16932

) -> Result<(), MinionError> {

907

16932

    let constraint_type = get_constraint_type(&inner_constraint)?;

908

16932

    let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {

909

16932

        ffi::constraint_free(x as _)

910

16932

});

911

912

16932

    constraint_add_args(instance, raw_inner_constraint.ptr, &inner_constraint)?;

913

914

16932

    ffi::constraint_addConstraint(raw_constraint, raw_inner_constraint.ptr);

915

16932

    Ok(())

916

16932

917

918

31318

unsafe fn read_constraint_list(

919

31318

    instance: *mut ffi::ProbSpec_CSPInstance,

920

31318

    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,

921

31318

    inner_constraints: &[Constraint],

922

31318

) -> Result<(), MinionError> {

923

31318

    let raw_inners = Scoped::new(ffi::vec_constraints_new(), |x| {

924

31318

        ffi::vec_constraints_free(x as _)

925

31318

});

926

65944

    for inner_constraint in inner_constraints.iter() {

927

65944

        let constraint_type = get_constraint_type(inner_constraint)?;

928

65944

        let raw_inner_constraint = Scoped::new(ffi::constraint_new(constraint_type), |x| {

929

65944

            ffi::constraint_free(x as _)

930

65944

});

931

932

65944

        constraint_add_args(instance, raw_inner_constraint.ptr, inner_constraint)?;

933

65944

        ffi::vec_constraints_push_back(raw_inners.ptr, raw_inner_constraint.ptr);

934

935

936

31318

    ffi::constraint_addConstraintList(raw_constraint, raw_inners.ptr);

937

31318

    Ok(())

938

31318

939

940

448

unsafe fn read_tuple_list(

941

448

    raw_constraint: *mut ffi::ProbSpec_ConstraintBlob,

942

448

    tuples: &Vec<Tuple>,

943

448

) -> Result<(), MinionError> {

944

    // a tuple list is just a vec<vec<int>>, where each inner vec is a tuple

945

448

    let raw_tuples = Scoped::new(ffi::vec_vec_int_new(), |x| ffi::vec_vec_int_free(x as _));

946

1148

    for tuple in tuples {

947

1148

        let raw_tuple = Scoped::new(ffi::vec_int_new(), |x| ffi::vec_int_free(x as _));

948

2996

        for constant in tuple.iter() {

949

2996

            let val = match constant {

950

2996

                Constant::Integer(n) => Ok(*n),

951

                Constant::Bool(true) => Ok(1),

952

                Constant::Bool(false) => Ok(0),

953

                #[allow(unreachable_patterns)] // TODO: can there be other types?

954

                x => Err(MinionError::NotImplemented(format!("{:?}", x))),

955

}?;

956

957

2996

            ffi::vec_int_push_back(raw_tuple.ptr, val);

958

959

960

1148

        ffi::vec_vec_int_push_back_ptr(raw_tuples.ptr, raw_tuple.ptr);

961

962

963

    // `constraint_setTuples` transfers ownership of `TupleList` into Minion via shared_ptr.

964

    // Do not wrap this pointer in `Scoped` or it will be freed too early.

965

448

    let raw_tuple_list = ffi::tupleList_new(raw_tuples.ptr);

966

448

    ffi::constraint_setTuples(raw_constraint, raw_tuple_list);

967

968

448

    Ok(())

969

448