1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
* Main authors:
* Pierre WILKE (wilke.pierre@gmail.com)
* Andrea Rendl (andrea.rendl@nicta.com.au)
*/
/* This Source Code Form is subject to the terms of the Mozilla Public
* License, v. 2.0. If a copy of the MPL was not distributed with this
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
#pragma once
#include <minizinc/solvers/gecode_solverinstance.hh>
/**
* \brief Branching on the introduced variables
*
* This brancher makes sure that when a solution is found for the model
* variables, all introduced variables are either assigned, or the solution
* can be extended to a solution of the introduced variables.
*
* The advantage over simply branching over the introduced variables is that
* only one such extension will be searched for, instead of enumerating all
* possible (equivalent) extensions.
*
*/
namespace MiniZinc {
class AuxVarBrancher : public Gecode::Brancher {
protected:
/// Flag whether brancher is done
bool done;
/// Construct brancher
AuxVarBrancher(Gecode::Home home, const Gecode::TieBreak<Gecode::IntVarBranch>& int_varsel0,
const Gecode::IntValBranch& int_valsel0,
const Gecode::TieBreak<Gecode::BoolVarBranch>& bool_varsel0,
const Gecode::BoolValBranch& bool_valsel0
#ifdef GECODE_HAS_SET_VARS
,
const Gecode::SetVarBranch& set_varsel0, const Gecode::SetValBranch& set_valsel0
#endif
#ifdef GECODE_HAS_FLOAT_VARS
,
const Gecode::TieBreak<Gecode::FloatVarBranch>& float_varsel0,
const Gecode::FloatValBranch& float_valsel0
#endif
)
: Brancher(home),
done(false),
int_varsel(int_varsel0),
int_valsel(int_valsel0),
bool_varsel(bool_varsel0),
bool_valsel(bool_valsel0)
#ifdef GECODE_HAS_SET_VARS
,
set_varsel(set_varsel0),
set_valsel(set_valsel0)
#endif
#ifdef GECODE_HAS_FLOAT_VARS
,
float_varsel(float_varsel0),
float_valsel(float_valsel0)
#endif
{
}
/// Copy constructor
AuxVarBrancher(Gecode::Space& home, AuxVarBrancher& b) : Brancher(home, b), done(b.done) {}
/// %Choice that only signals failure or success
class Choice : public Gecode::Choice {
public:
/// Whether brancher should fail
bool fail;
/// Initialize choice for brancher \a b
Choice(const Brancher& b, bool fail0) : Gecode::Choice(b, 1), fail(fail0) {}
/// Report size occupied
virtual size_t size() const { return sizeof(Choice); }
/// Archive into \a e
virtual void archive(Gecode::Archive& e) const {
Gecode::Choice::archive(e);
e.put(fail);
}
};
Gecode::TieBreak<Gecode::IntVarBranch> int_varsel;
Gecode::IntValBranch int_valsel;
Gecode::TieBreak<Gecode::BoolVarBranch> bool_varsel;
Gecode::BoolValBranch bool_valsel;
#ifdef GECODE_HAS_SET_VARS
Gecode::SetVarBranch set_varsel;
Gecode::SetValBranch set_valsel;
#endif
#ifdef GECODE_HAS_FLOAT_VARS
Gecode::TieBreak<Gecode::FloatVarBranch> float_varsel;
Gecode::FloatValBranch float_valsel;
#endif
public:
/// Check status of brancher, return true if alternatives left.
virtual bool status(const Gecode::Space& _home) const {
if (done) return false;
const MiniZinc::FznSpace& home = static_cast<const MiniZinc::FznSpace&>(_home);
for (int i = 0; i < home.ivAux.size(); i++)
if (!home.ivAux[i].assigned()) return true;
for (int i = 0; i < home.bvAux.size(); i++)
if (!home.bvAux[i].assigned()) return true;
#ifdef GECODE_HAS_SET_VARS
for (int i = 0; i < home.svAux.size(); i++)
if (!home.svAux[i].assigned()) return true;
#endif
#ifdef GECODE_HAS_FLOAT_VARS
for (int i = 0; i < home.fvAux.size(); i++)
if (!home.fvAux[i].assigned()) return true;
#endif
// No non-assigned variables left
return false;
}
/// Return choice
virtual Choice* choice(Gecode::Space& home) {
done = true;
MiniZinc::FznSpace& fzs = static_cast<MiniZinc::FznSpace&>(*home.clone());
fzs.copyAuxVars = false;
Gecode::branch(fzs, fzs.ivAux, int_varsel, int_valsel);
Gecode::branch(fzs, fzs.bvAux, bool_varsel, bool_valsel);
#ifdef GECODE_HAS_SET_VARS
Gecode::branch(fzs, fzs.svAux, set_varsel, set_valsel);
#endif
#ifdef GECODE_HAS_FLOAT_VARS
Gecode::branch(fzs, fzs.fvAux, float_varsel, float_valsel);
#endif
Gecode::Search::Options opt;
opt.clone = false;
MiniZinc::FznSpace* sol = Gecode::dfs(&fzs, opt);
if (sol) {
delete sol;
return new Choice(*this, false);
} else {
return new Choice(*this, true);
}
}
/// Return choice
virtual Choice* choice(const Gecode::Space&, Gecode::Archive& e) {
bool fail;
e >> fail;
return new Choice(*this, fail);
}
/// Perform commit for choice \a c
virtual Gecode::ExecStatus commit(Gecode::Space&, const Gecode::Choice& c, unsigned int) {
return static_cast<const Choice&>(c).fail ? Gecode::ES_FAILED : Gecode::ES_OK;
}
/// Print explanation
virtual void print(const Gecode::Space&, const Gecode::Choice& c, unsigned int,
std::ostream& o) const {
o << "FlatZinc(" << (static_cast<const Choice&>(c).fail ? "fail" : "ok") << ")";
}
/// Copy brancher
virtual Actor* copy(Gecode::Space& home) { return new (home) AuxVarBrancher(home, *this); }
/// Post brancher
static void post(Gecode::Home home, const Gecode::TieBreak<Gecode::IntVarBranch>& int_varsel,
const Gecode::IntValBranch& int_valsel,
const Gecode::TieBreak<Gecode::BoolVarBranch>& bool_varsel,
const Gecode::BoolValBranch& bool_valsel
#ifdef GECODE_HAS_SET_VARS
,
const Gecode::SetVarBranch& set_varsel, const Gecode::SetValBranch& set_valsel
#endif
#ifdef GECODE_HAS_FLOAT_VARS
,
const Gecode::TieBreak<Gecode::FloatVarBranch>& float_varsel,
const Gecode::FloatValBranch& float_valsel
#endif
) {
(void)new (home) AuxVarBrancher(home, int_varsel, int_valsel, bool_varsel, bool_valsel
#ifdef GECODE_HAS_SET_VARS
,
set_varsel, set_valsel
#endif
#ifdef GECODE_HAS_FLOAT_VARS
,
float_varsel, float_valsel
#endif
);
}
/// Delete brancher and return its size
virtual size_t dispose(Gecode::Space&) { return sizeof(*this); }
};
} // namespace MiniZinc
|
