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