this repo has no description
dekker.one
1#include <minizinc/hash.hh>
2#include <minizinc/solvers/nl/nl_file.hh>
3
4/**
5 * A NL File reprensentation.
6 * The purpose of this file is mainly to be a writer.
7 * Most of the information come from 'nlwrite.pdf'
8 * Note:
9 * * a character '#' starts a comment until the end of line.
10 * * A new line is '\n'
11 */
12
13namespace MiniZinc {
14
15/** *** *** *** Helpers *** *** *** **/
16
17/** Create a string representing the name (and unique identifier) from an identifier. */
18string NLFile::get_vname(const Id* id) {
19 stringstream os;
20 if (id->idn() != -1) {
21 os << "X_INTRODUCED_" << id->idn() << "_";
22 } else if (id->v().size() != 0) {
23 os << id->v();
24 }
25 string name = os.str();
26 return name;
27}
28
29/** Create a string representing the name (and unique identifier) of a variable from a variable
30 * declaration. */
31string NLFile::get_vname(const VarDecl& vd) { return get_vname(vd.id()); }
32
33/** Create a string representing the name (and unique identifier) of a constraint from a specific
34 * call expression. */
35string NLFile::get_cname(const Call& c) {
36 stringstream os;
37 os << c.id() << "_" << static_cast<const void*>(&c); // use the memory address as unique ID.
38 string name = os.str();
39 return name;
40}
41
42/** Obtain the vector of an array, either from an identifier or an array litteral */
43const ArrayLit& NLFile::get_arraylit(const Expression* e) {
44 switch (e->eid()) {
45 case Expression::E_ID: {
46 return get_arraylit(
47 e->cast<Id>()->decl()->e()); // Follow the pointer to the expression of the declaration
48 }
49
50 case Expression::E_ARRAYLIT: {
51 const ArrayLit& al = *e->cast<ArrayLit>();
52 return al;
53 }
54 }
55 should_not_happen("Could not read array from expression.");
56}
57
58/** Create a vector of double from a vector containing Expression being IntLit. */
59vector<double> NLFile::from_vec_int(const ArrayLit& v_int) {
60 vector<double> v = {};
61 for (unsigned int i = 0; i < v_int.size(); ++i) {
62 double d = v_int[i]->cast<IntLit>()->v().toInt();
63 v.push_back(d);
64 }
65 return v;
66}
67
68/** Create a vector of double from a vector containing Expression being FloatLit. */
69vector<double> NLFile::from_vec_fp(const ArrayLit& v_fp) {
70 vector<double> v = {};
71 for (unsigned int i = 0; i < v_fp.size(); ++i) {
72 double d = v_fp[i]->cast<FloatLit>()->v().toDouble();
73 v.push_back(d);
74 }
75 return v;
76}
77
78/** Create a vector of variable names from a vector containing Expression being identifier Id. */
79vector<string> NLFile::from_vec_id(const ArrayLit& v_id) {
80 vector<string> v = {};
81 for (unsigned int i = 0; i < v_id.size(); ++i) {
82 string s = get_vname(*(v_id[i]->cast<Id>()->decl()));
83 v.push_back(s);
84 }
85 return v;
86}
87
88/** *** *** *** Phase 1: collecting data from MZN *** *** *** **/
89
90/** Add a variable declaration in the NL File.
91 * This function pre-analyse the declaration VarDecl, then delegate to add_vdecl_integer or
92 * add_vdecl_fp. In flatzinc, arrays always have a rhs: the can always be replaced by their
93 * definition (following the pointer starting at the ID) Hence, we do not reproduce arrays in the NL
94 * file.
95 */
96void NLFile::add_vdecl(const VarDecl& vd, const TypeInst& ti, const Expression& rhs) {
97 // Get the name
98 string name = get_vname(vd);
99 // Discriminate according to the type:
100 if (ti.isEnum()) {
101 should_not_happen("Enum type in the flatzinc");
102 } else if (ti.isarray()) {
103 DEBUG_MSG(" Definition of array " << name << " is not reproduced in nl.");
104
105 // Look for the annotation "output_array"
106 for (ExpressionSetIter it = vd.ann().begin(); it != vd.ann().end(); ++it) {
107 Call* c = (*it)->dyn_cast<Call>();
108 if (c != NULL && c->id() == (constants().ann.output_array)) {
109 NLArray array;
110 array.name = name;
111 array.is_integer = ti.type().bt() == Type::BT_INT;
112
113 // Search the 'annotation' array
114 const ArrayLit& aa = get_arraylit(c->arg(0));
115 for (int i = 0; i < aa.size(); ++i) {
116 IntSetVal* r = aa[i]->cast<SetLit>()->isv();
117 stringstream ss;
118 ss << r->min().toInt() << ".." << r->max().toInt();
119 array.dimensions.push_back(ss.str());
120 }
121
122 // Search the 'real' array. Items can be an identifier or a litteral.
123 const ArrayLit& ra = get_arraylit(&rhs);
124 for (int i = 0; i < ra.size(); ++i) {
125 NLArray::Item item;
126
127 if (ra[i]->isa<Id>()) {
128 item.variable = get_vname(ra[i]->cast<Id>());
129 } else if (ra[i]->isa<IntLit>()) {
130 assert(array.is_integer);
131 item.value = ra[i]->cast<IntLit>()->v().toInt();
132 } else {
133 assert(!array.is_integer); // Floating point
134 item.value = ra[i]->cast<FloatLit>()->v().toDouble();
135 }
136
137 array.items.push_back(item);
138 }
139
140 output_arrays.push_back(array);
141
142 break;
143 }
144 }
145 } else {
146 // Check if the variable needs to be reported
147 bool to_report = vd.ann().contains(constants().ann.output_var);
148 DEBUG_MSG(" '" << name << "' to be reported? " << to_report);
149
150 // variable declaration
151 const Type& type = ti.type();
152 const Expression* domain = ti.domain();
153
154 // Check the type: integer or floatin point
155 assert(type.isvarint() || type.isvarfloat());
156 bool isvarint = type.isvarint();
157
158 // Call the declaration function according to the type
159 // Check the domain and convert if not null.
160 // Note: we directly jump to the specialized Int/Float set, going through the set literal
161 if (isvarint) {
162 // Integer
163 IntSetVal* isv = NULL;
164 if (domain != NULL) {
165 isv = domain->cast<SetLit>()->isv();
166 }
167 add_vdecl_integer(name, isv, to_report);
168 } else {
169 // Floating point
170 FloatSetVal* fsv = NULL;
171 if (domain != NULL) {
172 fsv = domain->cast<SetLit>()->fsv();
173 }
174 add_vdecl_fp(name, fsv, to_report);
175 }
176 }
177}
178
179/** Add an integer variable declaration to the NL File. */
180void NLFile::add_vdecl_integer(const string& name, const IntSetVal* isv, bool to_report) {
181 // Check that we do not have naming conflict
182 assert(variables.find(name) == variables.end());
183
184 // Check the domain.
185 NLBound bound;
186 if (isv == NULL) {
187 bound = NLBound::make_nobound();
188 } else if (isv->size() == 1) {
189 long long lb = isv->min(0).toInt();
190 long long ub = isv->max(0).toInt();
191 bound = NLBound::make_bounded(lb, ub);
192 } else {
193 should_not_happen("Range: switch on mzn_opt_only_range_domains" << endl);
194 }
195 // Create the variable and update the NLFile
196 NLVar v = NLVar(name, true, to_report, bound);
197 variables[name] = v;
198}
199
200/** Add a floating point variable declaration to the NL File. */
201void NLFile::add_vdecl_fp(const string& name, const FloatSetVal* fsv, bool to_report) {
202 // Check that we do not have naming conflict
203 assert(variables.find(name) == variables.end());
204 // Check the domain.
205 NLBound bound;
206 if (fsv == NULL) {
207 bound = NLBound::make_nobound();
208 } else if (fsv->size() == 1) {
209 double lb = fsv->min(0).toDouble();
210 double ub = fsv->max(0).toDouble();
211 bound = NLBound::make_bounded(lb, ub);
212 } else {
213 should_not_happen("Range: switch on mzn_opt_only_range_domains" << std::endl);
214 }
215 // Create the variable and update the NLFile
216 NLVar v = NLVar(name, false, to_report, bound);
217 variables[name] = v;
218}
219
220// --- --- --- Constraints analysis
221
222/** Dispatcher for constraint analysis. */
223void NLFile::analyse_constraint(const Call& c) {
224 // ID of the call
225 auto id = c.id();
226 // Constants for integer builtins
227 auto consint = constants().ids.int_;
228 // Constants for floating point builtins
229 auto consfp = constants().ids.float_;
230
231 // Integer linear predicates
232 if (id == consint.lin_eq) {
233 consint_lin_eq(c);
234 } else if (id == consint.lin_le) {
235 consint_lin_le(c);
236 } else if (id == consint.lin_ne) {
237 consint_lin_ne(c);
238 }
239
240 // Integer predicates
241 else if (id == consint.le) {
242 consint_le(c);
243 } else if (id == consint.eq) {
244 consint_eq(c);
245 } else if (id == consint.ne) {
246 consint_ne(c);
247 }
248
249 // Integer binary operators
250 else if (id == consint.times) {
251 consint_times(c);
252 } else if (id == consint.div) {
253 consint_div(c);
254 } else if (id == consint.mod) {
255 consint_mod(c);
256 } else if (id == consint.plus) {
257 consint_plus(c);
258 } else if (id == "int_pow") {
259 int_pow(c);
260 } else if (id == "int_max") {
261 int_max(c);
262 } else if (id == "int_min") {
263 int_min(c);
264 }
265
266 // Integer unary operators
267 else if (id == "int_abs") {
268 int_abs(c);
269 }
270
271 // Floating point linear predicates
272 else if (id == consfp.lin_eq) {
273 consfp_lin_eq(c);
274 } else if (id == consfp.lin_le) {
275 consfp_lin_le(c);
276 } else if (id == consfp.lin_lt) {
277 consfp_lin_lt(c);
278 } else if (id == consfp.lin_ne) {
279 consfp_lin_ne(c);
280 }
281
282 // Floating point predicates
283 else if (id == consfp.lt) {
284 consfp_lt(c);
285 } else if (id == consfp.le) {
286 consfp_le(c);
287 } else if (id == consfp.eq) {
288 consfp_eq(c);
289 } else if (id == consfp.ne) {
290 consfp_ne(c);
291 }
292
293 // Floating point binary operators
294 else if (id == consfp.plus) {
295 consfp_plus(c);
296 } else if (id == consfp.minus) {
297 consfp_minus(c);
298 } else if (id == consfp.div) {
299 consfp_div(c);
300 } else if (id == consfp.times) {
301 consfp_times(c);
302 } else if (id == "float_pow") {
303 float_pow(c);
304 } else if (id == "float_max") {
305 float_max(c);
306 } else if (id == "float_min") {
307 float_min(c);
308 }
309
310 // Floating point unary operators
311 else if (id == "float_abs") {
312 float_abs(c);
313 } else if (id == "float_acos") {
314 float_acos(c);
315 } else if (id == "float_acosh") {
316 float_acosh(c);
317 } else if (id == "float_asin") {
318 float_asin(c);
319 } else if (id == "float_asinh") {
320 float_asinh(c);
321 } else if (id == "float_atan") {
322 float_atan(c);
323 } else if (id == "float_atanh") {
324 float_atanh(c);
325 } else if (id == "float_cos") {
326 float_cos(c);
327 } else if (id == "float_cosh") {
328 float_cosh(c);
329 } else if (id == "float_exp") {
330 float_exp(c);
331 } else if (id == "float_ln") {
332 float_ln(c);
333 } else if (id == "float_log10") {
334 float_log10(c);
335 } else if (id == "float_log2") {
336 float_log2(c);
337 } else if (id == "float_sqrt") {
338 float_sqrt(c);
339 } else if (id == "float_sin") {
340 float_sin(c);
341 } else if (id == "float_sinh") {
342 float_sinh(c);
343 } else if (id == "float_tan") {
344 float_tan(c);
345 } else if (id == "float_tanh") {
346 float_tanh(c);
347 }
348
349 // Other
350 else if (id == "int2float") {
351 int2float(c);
352 }
353
354 // Domain
355 else if (id == consfp.in) {
356 should_not_happen("Ignore for now: constraint 'float in ' not implemented");
357 } else if (id == consfp.dom) {
358 should_not_happen("Ignore for now: constraint 'float dom ' not implemented");
359 }
360
361 // Grey area
362 else if (id == consint.lt) {
363 should_not_happen("'int lt'");
364 } else if (id == consint.gt) {
365 should_not_happen("'int gt'");
366 } else if (id == consint.ge) {
367 should_not_happen("'int ge'");
368 } else if (id == consint.minus) {
369 should_not_happen("'int minus'");
370 } else if (id == consfp.gt) {
371 should_not_happen("float gt'");
372 } else if (id == consfp.ge) {
373 should_not_happen("float ge'");
374 }
375
376 // Not implemented
377 else {
378 should_not_happen("Builtins " << c.id() << " not implemented or not recognized.");
379 }
380}
381
382// --- --- --- Helpers
383
384/** Create a token from an expression representing a variable */
385NLToken NLFile::get_tok_var_int(const Expression* e) {
386 if (e->type().ispar()) {
387 // Constant
388 long long value = e->cast<IntLit>()->v().toInt();
389 return NLToken::n(value);
390 } else {
391 // Variable
392 VarDecl& vd = *(e->cast<Id>()->decl());
393 string n = get_vname(vd);
394 return NLToken::v(n);
395 }
396}
397
398/** Create a token from an expression representing either a variable or a floating point numeric
399 * value. */
400NLToken NLFile::get_tok_var_fp(const Expression* e) {
401 if (e->type().ispar()) {
402 // Constant
403 double value = e->cast<FloatLit>()->v().toDouble();
404 return NLToken::n(value);
405 } else {
406 // Variable
407 VarDecl& vd = *(e->cast<Id>()->decl());
408 string n = get_vname(vd);
409 return NLToken::v(n);
410 }
411}
412
413/** Create a token from an expression representing either a variable. */
414NLToken NLFile::get_tok_var(const Expression* e) {
415 assert(!e->type().ispar());
416 // Variable
417 VarDecl& vd = *(e->cast<Id>()->decl());
418 string n = get_vname(vd);
419 return NLToken::v(n);
420}
421
422/** Update an expression graph (only by appending token) with a linear combination
423 * of coefficients and variables. Count as "non linear" for the variables occuring here.
424 */
425void NLFile::make_SigmaMult(vector<NLToken>& expression_graph, const vector<double>& coeffs,
426 const vector<string>& vars) {
427 assert(coeffs.size() == vars.size());
428 assert(coeffs.size() >= 2);
429
430 // Create a sum of products.
431 // WARNING: OPSUMLIST needs at least 3 operands! We need a special case for the sum of 2.
432 if (coeffs.size() == 2) {
433 expression_graph.push_back(NLToken::o(NLToken::OpCode::OPPLUS));
434 } else {
435 expression_graph.push_back(NLToken::mo(NLToken::MOpCode::OPSUMLIST, coeffs.size()));
436 }
437
438 // Component of the sum. Simplify multiplication by one.
439 for (unsigned int i = 0; i < coeffs.size(); ++i) {
440 // Product if coeff !=1
441 if (coeffs[i] != 1) {
442 expression_graph.push_back(NLToken::o(NLToken::OpCode::OPMULT));
443 expression_graph.push_back(NLToken::n(coeffs[i]));
444 }
445 // Set the variable as "non linear"
446 expression_graph.push_back(NLToken::v(vars[i]));
447 }
448}
449
450// --- --- --- Linear Builders
451
452/** Create a linear constraint [coeffs] *+ [vars] = value. */
453void NLFile::lincons_eq(const Call& c, const vector<double>& coeffs, const vector<string>& vars,
454 NLToken value) {
455 // Create the Algebraic Constraint and set the data
456 NLAlgCons cons;
457
458 // Get the name of the constraint
459 string cname = get_cname(c);
460 cons.name = cname;
461
462 if (value.is_constant()) {
463 // Create the bound of the constraint
464 NLBound bound = NLBound::make_equal(value.numeric_value);
465 cons.range = bound;
466 // No non linear part: leave the expression graph empty.
467 // Linear part: set the jacobian
468 cons.set_jacobian(vars, coeffs, this);
469 } else {
470 // Create the bound of the constraint = 0 and change the Jacobian to incorporate a -1 on the
471 // variable in 'value'
472 NLBound bound = NLBound::make_equal(0);
473 cons.range = bound;
474 // No non linear part: leave the expression graph empty.
475 // Linear part: set the jacobian
476 vector<double> coeffs_(coeffs);
477 coeffs_.push_back(-1);
478 vector<string> vars_(vars);
479 vars_.push_back(value.str);
480 cons.set_jacobian(vars_, coeffs_, this);
481 }
482
483 // Add the constraint in our mapping
484 constraints[cname] = cons;
485}
486
487/** Create a linear constraint [coeffs] *+ [vars] <= value. */
488void NLFile::lincons_le(const Call& c, const vector<double>& coeffs, const vector<string>& vars,
489 NLToken value) {
490 // Create the Algebraic Constraint and set the data
491 NLAlgCons cons;
492
493 // Get the name of the constraint
494 string cname = get_cname(c);
495 cons.name = cname;
496
497 if (value.is_constant()) {
498 // Create the bound of the constraint
499 NLBound bound = NLBound::make_ub_bounded(value.numeric_value);
500 cons.range = bound;
501 // No non linear part: leave the expression graph empty.
502 // Linear part: set the jacobian
503 cons.set_jacobian(vars, coeffs, this);
504 } else {
505 // Create the bound of the constraint = 0 and change the Jacobian to incorporate a -1 on the
506 // variable in 'value'
507 NLBound bound = NLBound::make_ub_bounded(0);
508 cons.range = bound;
509 // No non linear part: leave the expression graph empty.
510 // Linear part: set the jacobian
511 vector<double> coeffs_(coeffs);
512 coeffs_.push_back(-1);
513 vector<string> vars_(vars);
514 vars_.push_back(value.str);
515 cons.set_jacobian(vars_, coeffs_, this);
516 }
517
518 // Add the constraint in our mapping
519 constraints[cname] = cons;
520}
521
522/** Create a linear logical constraint [coeffs] *+ [vars] PREDICATE value.
523 * Use a generic comparison operator.
524 * Warnings: - Creates a logical constraint
525 * - Only use for conmparisons that cannot be expressed with '=' xor '<='.
526 */
527void NLFile::lincons_predicate(const Call& c, NLToken::OpCode oc, const vector<double>& coeffs,
528 const vector<string>& vars, NLToken value) {
529 // Create the Logical Constraint and set the data
530 NLLogicalCons cons(logical_constraints.size());
531
532 // Get the name of the constraint
533 string cname = get_cname(c);
534 cons.name = cname;
535
536 // Create the expression graph (Note: no Jacobian associated with a logical constraint).
537 // 1) Push the comparison operator, e.g. "!= operand1 operand2"
538 cons.expression_graph.push_back(NLToken::o(oc));
539
540 // 2) Operand1 := sum of product
541 make_SigmaMult(cons.expression_graph, coeffs, vars);
542
543 // 3) Operand 2 := value.
544 cons.expression_graph.push_back(value);
545
546 // Store the constraint
547 logical_constraints.push_back(cons);
548}
549
550// --- --- --- Non Linear Builders
551// For predicates, uses 2 variables or literals: x := c.arg(0), y := c.arg(1)
552// x PREDICATE y
553
554// For operations, uses 3 variables or literals: x := c.arg(0), y := c.arg(1), and z := c.arg(2).
555// x OPERATOR y = z
556
557/** Create a non linear constraint x = y
558 * Use the jacobian and the bound on constraint to translate into x - y = 0
559 * Simply update the bound if one is a constant.
560 */
561void NLFile::nlcons_eq(const Call& c, NLToken x, NLToken y) {
562 if (x.kind != y.kind) {
563 if (x.is_constant()) {
564 // Update bound on y
565 double value = x.numeric_value;
566 NLVar& v = variables.at(y.str);
567 v.bound.update_eq(value);
568 } else {
569 // Update bound on x
570 double value = y.numeric_value;
571 NLVar& v = variables.at(x.str);
572 v.bound.update_eq(value);
573 }
574 } else if (x.str != y.str) { // both must be variables anyway.
575 assert(x.is_variable() && y.is_variable());
576 // Create the Algebraic Constraint and set the data
577 NLAlgCons cons;
578
579 // Get the name of the constraint
580 string cname = get_cname(c);
581 cons.name = cname;
582
583 // Create the bound of the constraint: equal 0
584 NLBound bound = NLBound::make_equal(0);
585 cons.range = bound;
586
587 // Create the jacobian
588 vector<double> coeffs = {1, -1};
589 vector<string> vars = {x.str, y.str};
590 cons.set_jacobian(vars, coeffs, this);
591
592 // Store the constraint
593 constraints[cname] = cons;
594 }
595}
596
597/** Create a non linear constraint x <= y
598 * Use the jacobian and the bound on constraint to translate into x - y <= 0
599 * Simply update the bound if one is a constant.
600 */
601void NLFile::nlcons_le(const Call& c, NLToken x, NLToken y) {
602 if (x.kind != y.kind) {
603 if (x.is_constant()) {
604 // Update lower bound on y
605 double value = x.numeric_value;
606 NLVar& v = variables.at(y.str);
607 v.bound.update_lb(value);
608 } else {
609 // Update upper bound on x
610 double value = y.numeric_value;
611 NLVar& v = variables.at(x.str);
612 v.bound.update_ub(value);
613 }
614 } else if (x.str != y.str) { // both must be variables anyway.
615 assert(x.is_variable() && y.is_variable());
616
617 // Create the Algebraic Constraint and set the data
618 NLAlgCons cons;
619
620 // Get the name of the constraint
621 string cname = get_cname(c);
622 cons.name = cname;
623
624 // Create the bound of the constraint: <= 0
625 NLBound bound = NLBound::make_ub_bounded(0);
626 cons.range = bound;
627
628 // Create the jacobian
629 vector<double> coeffs = {1, -1};
630 vector<string> vars = {x.str, y.str};
631 cons.set_jacobian(vars, coeffs, this);
632
633 // Store the constraint
634 constraints[cname] = cons;
635 }
636}
637
638/** Create a non linear constraint with a predicate: x PREDICATE y
639 * Use a generic comparison operator.
640 * Warnings: - Creates a logical constraint
641 * - Only use for conmparisons that cannot be expressed with '=' xor '<='.
642 */
643void NLFile::nlcons_predicate(const Call& c, NLToken::OpCode oc, NLToken x, NLToken y) {
644 // Create the Logical Constraint and set the data
645 NLLogicalCons cons(logical_constraints.size());
646
647 // Get the name of the constraint
648 string cname = get_cname(c);
649 cons.name = cname;
650
651 // Create the expression graph
652 cons.expression_graph.push_back(NLToken::o(oc));
653 cons.expression_graph.push_back(x);
654 cons.expression_graph.push_back(y);
655
656 // Store the constraint
657 logical_constraints.push_back(cons);
658}
659
660/** Create a non linear constraint with a binary operator: x OPERATOR y = z */
661void NLFile::nlcons_operator_binary(const Call& c, NLToken::OpCode oc, NLToken x, NLToken y,
662 NLToken z) {
663 // Create the Algebraic Constraint and set the data
664 NLAlgCons cons;
665
666 // Get the name of the constraint
667 string cname = get_cname(c);
668 cons.name = cname;
669
670 // If z is a constant, use the bound, else use the jacobian
671 if (z.is_constant()) {
672 // Create the bound of the constraint with the numeric value of z
673 NLBound bound = NLBound::make_equal(z.numeric_value);
674 cons.range = bound;
675 } else {
676 // Else, use a constraint bound = 0 and use the jacobian to substract z from the result.
677 // Create the bound of the constraint to 0
678 NLBound bound = NLBound::make_equal(0);
679 cons.range = bound;
680
681 vector<double> coeffs = {};
682 vector<string> vars = {};
683
684 // If x is a variable different from y (and must be different from z), give it 0 for the linear
685 // part
686 if (x.is_variable() && x.str != y.str) {
687 assert(x.str != z.str);
688 coeffs.push_back(0);
689 vars.push_back(x.str);
690 }
691 // Same as above for y.
692 if (y.is_variable()) {
693 assert(y.str != z.str);
694 coeffs.push_back(0);
695 vars.push_back(y.str);
696 }
697 // z is a variable whose value is substracted from the result
698 coeffs.push_back(-1);
699 vars.push_back(z.str);
700
701 // Finish jacobian
702 cons.set_jacobian(vars, coeffs, this);
703 }
704
705 // Create the expression graph using the operand code 'oc'
706 cons.expression_graph.push_back(NLToken::o(oc));
707 cons.expression_graph.push_back(x);
708 cons.expression_graph.push_back(y);
709
710 // Store the constraint
711 constraints[cname] = cons;
712}
713
714/** Create a non linear constraint with a binary operator: x OPERATOR y = z.
715 * OPERATOR is now a Multiop, with a count of 2 (so the choice of the method to use depends on the
716 * LN implementation) */
717void NLFile::nlcons_operator_binary(const Call& c, NLToken::MOpCode moc, NLToken x, NLToken y,
718 NLToken z) {
719 // Create the Algebraic Constraint and set the data
720 NLAlgCons cons;
721
722 // Get the name of the constraint
723 string cname = get_cname(c);
724 cons.name = cname;
725
726 // If z is a constant, use the bound, else use the jacobian
727 if (z.is_constant()) {
728 // Create the bound of the constraint with the numeric value of z
729 NLBound bound = NLBound::make_equal(z.numeric_value);
730 cons.range = bound;
731 } else {
732 // Else, use a constraint bound = 0 and use the jacobian to substract vres from the result.
733 // Create the bound of the constraint to 0
734 NLBound bound = NLBound::make_equal(0);
735 cons.range = bound;
736
737 vector<double> coeffs = {};
738 vector<string> vars = {};
739
740 // If x is a variable different from y (and must be different from z), give it 0 for the linear
741 // part
742 if (x.is_variable() && x.str != y.str) {
743 assert(x.str != z.str);
744 coeffs.push_back(0);
745 vars.push_back(x.str);
746 }
747 // Same as above for y.
748 if (y.is_variable()) {
749 assert(y.str != z.str);
750 coeffs.push_back(0);
751 vars.push_back(y.str);
752 }
753 // z is a variable whose value is substracted from the result
754 coeffs.push_back(-1);
755 vars.push_back(z.str);
756
757 // Finish jacobian
758 cons.set_jacobian(vars, coeffs, this);
759 }
760
761 // Create the expression graph using the operand code 'oc'
762 cons.expression_graph.push_back(NLToken::mo(moc, 2));
763 cons.expression_graph.push_back(x);
764 cons.expression_graph.push_back(y);
765
766 // Store the constraint
767 constraints[cname] = cons;
768}
769
770/** Create a non linear constraint with an unary operator: OPERATOR x = y */
771void NLFile::nlcons_operator_unary(const Call& c, NLToken::OpCode oc, NLToken x, NLToken y) {
772 // Create the Algebraic Constraint and set the data
773 NLAlgCons cons;
774
775 // Get the name of the constraint
776 string cname = get_cname(c);
777 cons.name = cname;
778
779 // If y is a constant, use the bound, else use the jacobian
780 if (y.is_constant()) {
781 // Create the bound of the constraint with the numeric value of y
782 NLBound bound = NLBound::make_equal(y.numeric_value);
783 cons.range = bound;
784 } else {
785 // Else, use a constraint bound = 0 and use the jacobian to substract y from the result.
786 // Create the bound of the constraint to 0
787 NLBound bound = NLBound::make_equal(0);
788 cons.range = bound;
789
790 vector<double> coeffs = {};
791 vector<string> vars = {};
792
793 // If x is a variable (must be different from y), give it '0' for the linear part
794 if (x.is_variable()) {
795 assert(x.str != y.str);
796 coeffs.push_back(0);
797 vars.push_back(x.str);
798 }
799
800 // z is a variable whose value is substracted from the result
801 coeffs.push_back(-1);
802 vars.push_back(y.str);
803
804 // Finish jacobian
805 cons.set_jacobian(vars, coeffs, this);
806 }
807
808 // Create the expression graph using the operand code 'oc'
809 cons.expression_graph.push_back(NLToken::o(oc));
810 cons.expression_graph.push_back(x);
811
812 // Store the constraint
813 constraints[cname] = cons;
814}
815
816/** Create a non linear constraint, specialized for log2 unary operator: Log2(x) = y */
817void NLFile::nlcons_operator_unary_log2(const Call& c, NLToken x, NLToken y) {
818 // Create the Algebraic Constraint and set the data
819 NLAlgCons cons;
820
821 // Get the name of the constraint
822 string cname = get_cname(c);
823 cons.name = cname;
824
825 // If y is a constant, use the bound, else use the jacobian
826 if (y.is_constant()) {
827 // Create the bound of the constraint with the numeric value of y
828 NLBound bound = NLBound::make_equal(y.numeric_value);
829 cons.range = bound;
830 } else {
831 // Else, use a constraint bound = 0 and use the jacobian to substract vres from the result.
832 // Create the bound of the constraint to 0
833 NLBound bound = NLBound::make_equal(0);
834 cons.range = bound;
835
836 vector<double> coeffs = {};
837 vector<string> vars = {};
838
839 // If x is a variable (must be different from y), give it '0' for the linear part
840 if (x.is_variable()) {
841 assert(x.str != y.str);
842 coeffs.push_back(0);
843 vars.push_back(x.str);
844 }
845 // z is a variable whose value is substracted from the result
846 coeffs.push_back(-1);
847 vars.push_back(y.str);
848
849 // Finish jacobian
850 cons.set_jacobian(vars, coeffs, this);
851 }
852
853 // Create the expression graph with log2(x) = ln(x)/ln(2)
854 cons.expression_graph.push_back(NLToken::o(NLToken::OpCode::OPDIV));
855 cons.expression_graph.push_back(NLToken::o(NLToken::OpCode::OP_log));
856 cons.expression_graph.push_back(x);
857 cons.expression_graph.push_back(NLToken::o(NLToken::OpCode::OP_log));
858 cons.expression_graph.push_back(NLToken::n(2));
859
860 // Store the constraint
861 constraints[cname] = cons;
862}
863
864// --- --- --- Integer Linear Constraints
865
866/** Linar constraint: [coeffs] *+ [vars] = value */
867void NLFile::consint_lin_eq(const Call& c) {
868 // Get the arguments arg0 (array0 = coeffs), arg1 (array = variables) and arg2 (value)
869 vector<double> coeffs = from_vec_int(get_arraylit(c.arg(0)));
870 vector<string> vars = from_vec_id(get_arraylit(c.arg(1)));
871 NLToken value = get_tok_var_int(c.arg(2));
872 // Create the constraint
873 lincons_eq(c, coeffs, vars, value);
874}
875
876/** Linar constraint: [coeffs] *+ [vars] =< value */
877void NLFile::consint_lin_le(const Call& c) {
878 // Get the arguments arg0 (array0 = coeffs), arg1 (array = variables) and arg2 (value)
879 vector<double> coeffs = from_vec_int(get_arraylit(c.arg(0)));
880 vector<string> vars = from_vec_id(get_arraylit(c.arg(1)));
881 NLToken value = get_tok_var_int(c.arg(2));
882 // Create the constraint
883 lincons_le(c, coeffs, vars, value);
884}
885
886/** Linar constraint: [coeffs] *+ [vars] != value */
887void NLFile::consint_lin_ne(const Call& c) {
888 // Get the arguments arg0 (array0 = coeffs), arg1 (array = variables) and arg2 (value)
889 vector<double> coeffs = from_vec_int(get_arraylit(c.arg(0)));
890 vector<string> vars = from_vec_id(get_arraylit(c.arg(1)));
891 NLToken value = get_tok_var_int(c.arg(2));
892 // Create the constraint
893 lincons_predicate(c, NLToken::OpCode::NE, coeffs, vars, value);
894}
895
896// --- --- --- Integer Non Linear Predicate Constraints
897
898/** Non linear constraint x = y */
899void NLFile::consint_eq(const Call& c) {
900 nlcons_eq(c, get_tok_var_int(c.arg(0)), get_tok_var_int(c.arg(1)));
901}
902
903/** Non linear constraint x <= y */
904void NLFile::consint_le(const Call& c) {
905 nlcons_le(c, get_tok_var_int(c.arg(0)), get_tok_var_int(c.arg(1)));
906}
907
908/** Non linear constraint x != y */
909void NLFile::consint_ne(const Call& c) {
910 nlcons_predicate(c, NLToken::OpCode::NE, get_tok_var_int(c.arg(0)), get_tok_var_int(c.arg(1)));
911}
912
913// --- --- --- Integer Non Linear Binary Operator Constraints
914
915/** Non linear constraint x + y = z */
916void NLFile::consint_plus(const Call& c) {
917 nlcons_operator_binary(c, NLToken::OpCode::OPPLUS, get_tok_var_int(c.arg(0)),
918 get_tok_var_int(c.arg(1)), get_tok_var_int(c.arg(2)));
919}
920
921/** Non linear constraint x * y = z */
922void NLFile::consint_times(const Call& c) {
923 nlcons_operator_binary(c, NLToken::OpCode::OPMULT, get_tok_var_int(c.arg(0)),
924 get_tok_var_int(c.arg(1)), get_tok_var_int(c.arg(2)));
925}
926
927/** Non linear constraint x / y = z */
928void NLFile::consint_div(const Call& c) {
929 nlcons_operator_binary(c, NLToken::OpCode::OPDIV, get_tok_var_int(c.arg(0)),
930 get_tok_var_int(c.arg(1)), get_tok_var_int(c.arg(2)));
931}
932
933/** Non linear constraint x mod y = z */
934void NLFile::consint_mod(const Call& c) {
935 nlcons_operator_binary(c, NLToken::OpCode::OPREM, get_tok_var_int(c.arg(0)),
936 get_tok_var_int(c.arg(1)), get_tok_var_int(c.arg(2)));
937}
938
939/** Non linear constraint x pow y = z */
940void NLFile::int_pow(const Call& c) {
941 nlcons_operator_binary(c, NLToken::OpCode::OPPOW, get_tok_var_int(c.arg(0)),
942 get_tok_var_int(c.arg(1)), get_tok_var_int(c.arg(2)));
943}
944
945/** Non linear constraint max(x, y) = z */
946void NLFile::int_max(const Call& c) {
947 nlcons_operator_binary(c, NLToken::MOpCode::MAXLIST, get_tok_var_int(c.arg(0)),
948 get_tok_var_int(c.arg(1)), get_tok_var_int(c.arg(2)));
949}
950
951/** Non linear constraint min(x, y) = z */
952void NLFile::int_min(const Call& c) {
953 nlcons_operator_binary(c, NLToken::MOpCode::MINLIST, get_tok_var_int(c.arg(0)),
954 get_tok_var_int(c.arg(1)), get_tok_var_int(c.arg(2)));
955}
956
957// --- --- --- Integer Non Linear Unary Operator Constraints
958
959/** Non linear constraint abs x = y */
960void NLFile::int_abs(const Call& c) {
961 nlcons_operator_unary(c, NLToken::OpCode::ABS, get_tok_var_int(c.arg(0)),
962 get_tok_var_int(c.arg(1)));
963}
964
965// --- --- --- Floating Point Linear Constraints
966
967/** Linar constraint: [coeffs] *+ [vars] = value */
968void NLFile::consfp_lin_eq(const Call& c) {
969 // Get the arguments arg0 (array0 = coeffs), arg1 (array = variables) and arg2 (value)
970 vector<double> coeffs = from_vec_fp(get_arraylit(c.arg(0)));
971 vector<string> vars = from_vec_id(get_arraylit(c.arg(1)));
972 NLToken value = get_tok_var_fp(c.arg(2));
973 // Create the constraint
974 lincons_eq(c, coeffs, vars, value);
975}
976
977/** Linar constraint: [coeffs] *+ [vars] = value */
978void NLFile::consfp_lin_le(const Call& c) {
979 // Get the arguments arg0 (array0 = coeffs), arg1 (array = variables) and arg2 (value)
980 vector<double> coeffs = from_vec_fp(get_arraylit(c.arg(0)));
981 vector<string> vars = from_vec_id(get_arraylit(c.arg(1)));
982 NLToken value = get_tok_var_fp(c.arg(2));
983 // Create the constraint
984 lincons_le(c, coeffs, vars, value);
985}
986
987/** Linar constraint: [coeffs] *+ [vars] != value */
988void NLFile::consfp_lin_ne(const Call& c) {
989 // Get the arguments arg0 (array0 = coeffs), arg1 (array = variables) and arg2 (value)
990 vector<double> coeffs = from_vec_fp(get_arraylit(c.arg(0)));
991 vector<string> vars = from_vec_id(get_arraylit(c.arg(1)));
992 NLToken value = get_tok_var_fp(c.arg(2));
993 // Create the constraint
994 lincons_predicate(c, NLToken::OpCode::NE, coeffs, vars, value);
995}
996
997/** Linar constraint: [coeffs] *+ [vars] < value */
998void NLFile::consfp_lin_lt(const Call& c) {
999 // Get the arguments arg0 (array0 = coeffs), arg1 (array = variables) and arg2 (value)
1000 vector<double> coeffs = from_vec_fp(get_arraylit(c.arg(0)));
1001 vector<string> vars = from_vec_id(get_arraylit(c.arg(1)));
1002 NLToken value = get_tok_var_fp(c.arg(2));
1003 // Create the constraint
1004 lincons_predicate(c, NLToken::OpCode::LT, coeffs, vars, value);
1005}
1006
1007// --- --- --- Floating Point Non Linear Predicate Constraints
1008
1009/** Non linear constraint x = y */
1010void NLFile::consfp_eq(const Call& c) {
1011 nlcons_eq(c, get_tok_var_fp(c.arg(0)), get_tok_var_fp(c.arg(1)));
1012}
1013
1014/** Non linear constraint x <= y */
1015void NLFile::consfp_le(const Call& c) {
1016 nlcons_le(c, get_tok_var_fp(c.arg(0)), get_tok_var_fp(c.arg(1)));
1017}
1018
1019/** Non linear constraint x != y */
1020void NLFile::consfp_ne(const Call& c) {
1021 nlcons_predicate(c, NLToken::OpCode::NE, get_tok_var_fp(c.arg(0)), get_tok_var_fp(c.arg(1)));
1022}
1023
1024/** Non linear constraint x < y */
1025void NLFile::consfp_lt(const Call& c) {
1026 nlcons_predicate(c, NLToken::OpCode::LT, get_tok_var_fp(c.arg(0)), get_tok_var_fp(c.arg(1)));
1027}
1028
1029// --- --- --- Floating Point Non Linear Binary Operator Constraints
1030
1031/** Non linear constraint x + y = z */
1032void NLFile::consfp_plus(const Call& c) {
1033 nlcons_operator_binary(c, NLToken::OpCode::OPPLUS, get_tok_var_fp(c.arg(0)),
1034 get_tok_var_fp(c.arg(1)), get_tok_var_fp(c.arg(2)));
1035}
1036
1037/** Non linear constraint x - y = z */
1038void NLFile::consfp_minus(const Call& c) {
1039 nlcons_operator_binary(c, NLToken::OpCode::OPMINUS, get_tok_var_fp(c.arg(0)),
1040 get_tok_var_fp(c.arg(1)), get_tok_var_fp(c.arg(2)));
1041}
1042
1043/** Non linear constraint x * y = z */
1044void NLFile::consfp_times(const Call& c) {
1045 nlcons_operator_binary(c, NLToken::OpCode::OPMULT, get_tok_var_fp(c.arg(0)),
1046 get_tok_var_fp(c.arg(1)), get_tok_var_fp(c.arg(2)));
1047}
1048
1049/** Non linear constraint x / y = z */
1050void NLFile::consfp_div(const Call& c) {
1051 nlcons_operator_binary(c, NLToken::OpCode::OPDIV, get_tok_var_fp(c.arg(0)),
1052 get_tok_var_fp(c.arg(1)), get_tok_var_fp(c.arg(2)));
1053}
1054
1055/** Non linear constraint x mod y = z */
1056void NLFile::consfp_mod(const Call& c) {
1057 nlcons_operator_binary(c, NLToken::OpCode::OPREM, get_tok_var_fp(c.arg(0)),
1058 get_tok_var_fp(c.arg(1)), get_tok_var_fp(c.arg(2)));
1059}
1060
1061/** Non linear constraint x pow y = z */
1062void NLFile::float_pow(const Call& c) {
1063 nlcons_operator_binary(c, NLToken::OpCode::OPPOW, get_tok_var_fp(c.arg(0)),
1064 get_tok_var_fp(c.arg(1)), get_tok_var_fp(c.arg(2)));
1065}
1066
1067/** Non linear constraint max(x, y) = z */
1068void NLFile::float_max(const Call& c) {
1069 nlcons_operator_binary(c, NLToken::MOpCode::MAXLIST, get_tok_var_fp(c.arg(0)),
1070 get_tok_var_fp(c.arg(1)), get_tok_var_fp(c.arg(2)));
1071}
1072
1073/** Non linear constraint min(x, y) = z */
1074void NLFile::float_min(const Call& c) {
1075 nlcons_operator_binary(c, NLToken::MOpCode::MINLIST, get_tok_var_fp(c.arg(0)),
1076 get_tok_var_fp(c.arg(1)), get_tok_var_fp(c.arg(2)));
1077}
1078
1079// --- --- --- Floating Point Non Linear Unary operator Constraints
1080
1081/** Non linear constraint abs x = y */
1082void NLFile::float_abs(const Call& c) {
1083 nlcons_operator_unary(c, NLToken::OpCode::ABS, get_tok_var_fp(c.arg(0)),
1084 get_tok_var_fp(c.arg(1)));
1085}
1086
1087/** Non linear constraint acos x = y */
1088void NLFile::float_acos(const Call& c) {
1089 nlcons_operator_unary(c, NLToken::OpCode::OP_acos, get_tok_var_fp(c.arg(0)),
1090 get_tok_var_fp(c.arg(1)));
1091}
1092
1093/** Non linear constraint acosh x = y */
1094void NLFile::float_acosh(const Call& c) {
1095 nlcons_operator_unary(c, NLToken::OpCode::OP_acosh, get_tok_var_fp(c.arg(0)),
1096 get_tok_var_fp(c.arg(1)));
1097}
1098
1099/** Non linear constraint asin x = y */
1100void NLFile::float_asin(const Call& c) {
1101 nlcons_operator_unary(c, NLToken::OpCode::OP_asin, get_tok_var_fp(c.arg(0)),
1102 get_tok_var_fp(c.arg(1)));
1103}
1104
1105/** Non linear constraint asinh x = y */
1106void NLFile::float_asinh(const Call& c) {
1107 nlcons_operator_unary(c, NLToken::OpCode::OP_asinh, get_tok_var_fp(c.arg(0)),
1108 get_tok_var_fp(c.arg(1)));
1109}
1110
1111/** Non linear constraint atan x = y */
1112void NLFile::float_atan(const Call& c) {
1113 nlcons_operator_unary(c, NLToken::OpCode::OP_atan, get_tok_var_fp(c.arg(0)),
1114 get_tok_var_fp(c.arg(1)));
1115}
1116
1117/** Non linear constraint atanh x = y */
1118void NLFile::float_atanh(const Call& c) {
1119 nlcons_operator_unary(c, NLToken::OpCode::OP_atanh, get_tok_var_fp(c.arg(0)),
1120 get_tok_var_fp(c.arg(1)));
1121}
1122
1123/** Non linear constraint cos x = y */
1124void NLFile::float_cos(const Call& c) {
1125 nlcons_operator_unary(c, NLToken::OpCode::OP_cos, get_tok_var_fp(c.arg(0)),
1126 get_tok_var_fp(c.arg(1)));
1127}
1128
1129/** Non linear constraint cosh x = y */
1130void NLFile::float_cosh(const Call& c) {
1131 nlcons_operator_unary(c, NLToken::OpCode::OP_cosh, get_tok_var_fp(c.arg(0)),
1132 get_tok_var_fp(c.arg(1)));
1133}
1134
1135/** Non linear constraint exp x = y */
1136void NLFile::float_exp(const Call& c) {
1137 nlcons_operator_unary(c, NLToken::OpCode::OP_exp, get_tok_var_fp(c.arg(0)),
1138 get_tok_var_fp(c.arg(1)));
1139}
1140
1141/** Non linear constraint ln x = y */
1142void NLFile::float_ln(const Call& c) {
1143 nlcons_operator_unary(c, NLToken::OpCode::OP_log, get_tok_var_fp(c.arg(0)),
1144 get_tok_var_fp(c.arg(1)));
1145}
1146
1147/** Non linear constraint log10 x = y */
1148void NLFile::float_log10(const Call& c) {
1149 nlcons_operator_unary(c, NLToken::OpCode::OP_log10, get_tok_var_fp(c.arg(0)),
1150 get_tok_var_fp(c.arg(1)));
1151}
1152
1153/** Non linear constraint log2 x = y */
1154void NLFile::float_log2(const Call& c) {
1155 nlcons_operator_unary_log2(c, get_tok_var_fp(c.arg(0)), get_tok_var_fp(c.arg(1)));
1156}
1157
1158/** Non linear constraint sqrt x = y */
1159void NLFile::float_sqrt(const Call& c) {
1160 nlcons_operator_unary(c, NLToken::OpCode::OP_sqrt, get_tok_var_fp(c.arg(0)),
1161 get_tok_var_fp(c.arg(1)));
1162}
1163
1164/** Non linear constraint sin x = y */
1165void NLFile::float_sin(const Call& c) {
1166 nlcons_operator_unary(c, NLToken::OpCode::OP_sin, get_tok_var_fp(c.arg(0)),
1167 get_tok_var_fp(c.arg(1)));
1168}
1169
1170/** Non linear constraint sinh x = y */
1171void NLFile::float_sinh(const Call& c) {
1172 nlcons_operator_unary(c, NLToken::OpCode::OP_sinh, get_tok_var_fp(c.arg(0)),
1173 get_tok_var_fp(c.arg(1)));
1174}
1175
1176/** Non linear constraint tan x = y */
1177void NLFile::float_tan(const Call& c) {
1178 nlcons_operator_unary(c, NLToken::OpCode::OP_tan, get_tok_var_fp(c.arg(0)),
1179 get_tok_var_fp(c.arg(1)));
1180}
1181
1182/** Non linear constraint tanh x = y */
1183void NLFile::float_tanh(const Call& c) {
1184 nlcons_operator_unary(c, NLToken::OpCode::OP_tanh, get_tok_var_fp(c.arg(0)),
1185 get_tok_var_fp(c.arg(1)));
1186}
1187
1188// --- --- --- Other
1189
1190/** Integer x to floating point y. Constraint x = y translated into x - y = 0.
1191 * Simulate a linear constraint [1, -1]+*[x, y] = 0
1192 */
1193void NLFile::int2float(const Call& c) {
1194 vector<double> coeffs = {1, -1};
1195 vector<string> vars = {};
1196 vars.push_back(get_tok_var(c.arg(0)).str);
1197 vars.push_back(get_tok_var(c.arg(1)).str);
1198 // Create the constraint
1199 lincons_eq(c, coeffs, vars, NLToken::n(0));
1200}
1201
1202// --- --- --- Objective
1203
1204/** Add a solve goal in the NL File. In our case, we can only have one and only one solve goal. */
1205void NLFile::add_solve(SolveI::SolveType st, const Expression* e) {
1206 // We can only have one objective. Prevent override.
1207 assert(!objective.is_defined());
1208
1209 switch (st) {
1210 case SolveI::SolveType::ST_SAT: {
1211 // Satisfy: implemented by minimizing 0 (print n0 for an empty expression graph)
1212 objective.minmax = objective.SATISFY;
1213 break;
1214 }
1215 case SolveI::SolveType::ST_MIN: {
1216 // Maximize an objective represented by a variable
1217 objective.minmax = objective.MINIMIZE;
1218 string v = get_tok_var(e).str;
1219 // Use the gradient
1220 vector<double> coeffs = {1};
1221 vector<string> vars = {v};
1222 objective.set_gradient(vars, coeffs);
1223 break;
1224 }
1225 case SolveI::SolveType::ST_MAX: {
1226 // Maximize an objective represented by a variable
1227 objective.minmax = objective.MAXIMIZE;
1228 string v = get_tok_var(e).str;
1229 // Use the gradient
1230 vector<double> coeffs = {1};
1231 vector<string> vars = {v};
1232 objective.set_gradient(vars, coeffs);
1233 break;
1234 }
1235 }
1236
1237 // Ensure that the obejctive is now defined.
1238 assert(objective.is_defined());
1239}
1240
1241/* *** *** *** Phase 2: processing *** *** *** */
1242
1243void NLFile::phase_2() {
1244 // --- --- --- Go over all constraint (algebraic AND logical) and mark non linear variables
1245 for (auto const& n_c : constraints) {
1246 for (auto const& tok : n_c.second.expression_graph) {
1247 if (tok.is_variable()) {
1248 variables.at(tok.str).is_in_nl_constraint = true;
1249 }
1250 }
1251 }
1252
1253 for (auto const& c : logical_constraints) {
1254 for (auto const& tok : c.expression_graph) {
1255 if (tok.is_variable()) {
1256 variables.at(tok.str).is_in_nl_constraint = true;
1257 }
1258 }
1259 }
1260
1261 // --- --- --- Go over the objective and mark non linear variables
1262 for (auto const& tok : objective.expression_graph) {
1263 if (tok.is_variable()) {
1264 variables.at(tok.str).is_in_nl_objective = true;
1265 }
1266 }
1267
1268 // --- --- --- Variables ordering and indexing
1269 for (auto const& name_var : variables) {
1270 const NLVar& v = name_var.second;
1271
1272 // Accumulate jacobian count
1273 _jacobian_count += v.jacobian_count;
1274
1275 // First check non linear variables in BOTH objective and constraint.
1276 if (v.is_in_nl_objective && v.is_in_nl_constraint) {
1277 if (v.is_integer) {
1278 vname_nliv_both.push_back(v.name);
1279 } else {
1280 vname_nlcv_both.push_back(v.name);
1281 }
1282 }
1283 // Variables in non linear constraint ONLY
1284 else if (!v.is_in_nl_objective && v.is_in_nl_constraint) {
1285 if (v.is_integer) {
1286 vname_nliv_cons.push_back(v.name);
1287 } else {
1288 vname_nlcv_cons.push_back(v.name);
1289 }
1290 }
1291 // Variables in non linear objective ONLY
1292 else if (v.is_in_nl_objective && !v.is_in_nl_constraint) {
1293 if (v.is_integer) {
1294 vname_nliv_obj.push_back(v.name);
1295 } else {
1296 vname_nlcv_obj.push_back(v.name);
1297 }
1298 }
1299 // Variables not appearing nonlinearly
1300 else if (!v.is_in_nl_objective && !v.is_in_nl_constraint) {
1301 if (v.is_integer) {
1302 vname_liv_all.push_back(v.name);
1303 } else {
1304 vname_lcv_all.push_back(v.name);
1305 }
1306 }
1307 // Should not happen
1308 else {
1309 should_not_happen("Dispatching variables in phase2");
1310 }
1311 }
1312
1313 // Note: In the above, we dealt with all 'vname_*' vectors BUT 'vname_larc_all' and
1314 // 'vname_bv_all'
1315 // networks and boolean are not implemented. Nevertheless, we keep the vectors and deal
1316 // with them below to ease further implementations.
1317
1318 vnames.reserve(variables.size());
1319
1320 vnames.insert(vnames.end(), vname_nlcv_both.begin(), vname_nlcv_both.end());
1321 vnames.insert(vnames.end(), vname_nliv_both.begin(), vname_nliv_both.end());
1322 vnames.insert(vnames.end(), vname_nlcv_cons.begin(), vname_nlcv_cons.end());
1323 vnames.insert(vnames.end(), vname_nliv_cons.begin(), vname_nliv_cons.end());
1324 vnames.insert(vnames.end(), vname_nlcv_obj.begin(), vname_nlcv_obj.end());
1325 vnames.insert(vnames.end(), vname_nliv_obj.begin(), vname_nliv_obj.end());
1326 vnames.insert(vnames.end(), vname_larc_all.begin(), vname_larc_all.end());
1327 vnames.insert(vnames.end(), vname_lcv_all.begin(), vname_lcv_all.end());
1328 vnames.insert(vnames.end(), vname_bv_all.begin(), vname_bv_all.end());
1329 vnames.insert(vnames.end(), vname_liv_all.begin(), vname_liv_all.end());
1330
1331 // Create the mapping name->index
1332 for (int i = 0; i < vnames.size(); ++i) {
1333 variable_indexes[vnames[i]] = i;
1334 }
1335
1336 // --- --- --- Constraint ordering, couting, and indexing
1337 for (auto const& name_cons : constraints) {
1338 const NLAlgCons& c = name_cons.second;
1339
1340 // Sort by linearity. We do not have network constraint.
1341 if (c.is_linear()) {
1342 cnames_lin_general.push_back(c.name);
1343 } else {
1344 cnames_nl_general.push_back(c.name);
1345 }
1346
1347 // Count the number of ranges and eqns constraints
1348 switch (c.range.tag) {
1349 case NLBound::LB_UB: {
1350 ++nb_alg_cons_range;
1351 }
1352 case NLBound::EQ: {
1353 ++nb_alg_cons_eq;
1354 }
1355 }
1356 }
1357
1358 cnames.reserve(constraints.size());
1359 cnames.insert(cnames.end(), cnames_nl_general.begin(), cnames_nl_general.end());
1360 cnames.insert(cnames.end(), cnames_nl_network.begin(), cnames_nl_network.end());
1361 cnames.insert(cnames.end(), cnames_lin_network.begin(), cnames_lin_network.end());
1362 cnames.insert(cnames.end(), cnames_lin_general.begin(), cnames_lin_general.end());
1363
1364 // Create the mapping name->index
1365 for (int i = 0; i < cnames.size(); ++i) {
1366 constraint_indexes[cnames[i]] = i;
1367 }
1368}
1369
1370// --- --- --- Simple tests
1371
1372bool NLFile::has_integer_vars() const { return (nlvbi() + nlvci() + nlvoi() + niv()) > 0; }
1373
1374bool NLFile::has_continous_vars() const { return !has_integer_vars(); }
1375
1376// --- --- --- Counts
1377
1378/** Jacobian count. */
1379int NLFile::jacobian_count() const { return _jacobian_count; }
1380
1381/** Total number of variables. */
1382int NLFile::n_var() const { return variables.size(); }
1383
1384/** Number of variables appearing nonlinearly in constraints. */
1385int NLFile::nlvc() const {
1386 // Variables in both + variables in constraint only (integer+continuous)
1387 return nlvb() + vname_nliv_cons.size() + vname_nlcv_cons.size();
1388}
1389
1390/** Number of variables appearing nonlinearly in objectives. */
1391int NLFile::nlvo() const {
1392 // Variables in both + variables in objective only (integer+continuous)
1393 return nlvb() + vname_nliv_obj.size() + vname_nlcv_obj.size();
1394}
1395
1396/** Number of variables appearing nonlinearly in both constraints and objectives.*/
1397int NLFile::nlvb() const { return vname_nlcv_both.size() + vname_nliv_both.size(); }
1398
1399/** Number of integer variables appearing nonlinearly in both constraints and objectives.*/
1400int NLFile::nlvbi() const { return vname_nliv_both.size(); }
1401
1402/** Number of integer variables appearing nonlinearly in constraints **only**.*/
1403int NLFile::nlvci() const { return vname_nliv_cons.size(); }
1404
1405/** Number of integer variables appearing nonlinearly in objectives **only**.*/
1406int NLFile::nlvoi() const { return vname_nliv_obj.size(); }
1407
1408/** Number of linear arcs. Network nor implemented, so always 0.*/
1409int NLFile::nwv() const { return vname_larc_all.size(); }
1410
1411/** Number of "other" integer variables.*/
1412int NLFile::niv() const { return vname_liv_all.size(); }
1413
1414/** Number of binary variables.*/
1415int NLFile::nbv() const { return vname_bv_all.size(); }
1416
1417/** *** *** *** Printable *** *** *** **/
1418// Note: * empty line not allowed
1419// * comment only not allowed
1420ostream& NLFile::print_on(ostream& os) const {
1421 // Print the header
1422 {
1423 NLHeader header;
1424 header.print_on(os, *this);
1425 }
1426 os << endl;
1427
1428 // Print the unique segments about the variables
1429 if (n_var() > 1) {
1430 // Print the 'k' segment Maybe to adjust with the presence of 'J' segments
1431 os << "k" << (n_var() - 1)
1432 << " # Cumulative Sum of non-zero in the jacobian matrix's (nbvar-1) columns." << endl;
1433 int acc = 0;
1434 // Note stop before the last var. Total jacobian count is in the header.
1435 for (int i = 0; i < n_var() - 1; ++i) {
1436 string name = vnames[i];
1437 acc += variables.at(name).jacobian_count;
1438 os << acc << " # " << name << endl;
1439 }
1440
1441 // Print the 'b' segment
1442 os << "b # Bounds on variables (" << n_var() << ")" << endl;
1443 for (auto n : vnames) {
1444 NLVar v = variables.at(n);
1445 v.bound.print_on(os, n);
1446 os << endl;
1447 }
1448 }
1449
1450 // Print the unique segments about the constraints
1451 if (!cnames.empty()) {
1452 // Create the 'r' range segment per constraint
1453 // For now, it is NOT clear if the network constraint should appear in the range constraint or
1454 // not. To be determine if later implemented.
1455 os << "r # Bounds on algebraic constraint bodies (" << cnames.size() << ")" << endl;
1456 for (auto n : cnames) {
1457 NLAlgCons c = constraints.at(n);
1458 c.range.print_on(os, n);
1459 os << endl;
1460 }
1461 }
1462
1463 // Print the Algebraic Constraints
1464 for (auto n : cnames) {
1465 NLAlgCons c = constraints.at(n);
1466 c.print_on(os, *this);
1467 }
1468
1469 // Print the Logical constraint
1470 for (auto& lc : logical_constraints) {
1471 lc.print_on(os, *this);
1472 }
1473
1474 // Print the objective
1475 objective.print_on(os, *this);
1476 return os;
1477}
1478
1479} // namespace MiniZinc