chage all ==, >=... API to use IntExpr, except the last term of IsXXX which is always an IntVar

This commit is contained in:
lperron@google.com
2012-07-05 16:27:57 +00:00
parent 1d2dfae7ac
commit 40dbb60d23
6 changed files with 258 additions and 343 deletions

View File

@@ -1327,97 +1327,97 @@ class Solver {
Constraint* MakeFalseConstraint(const string& explanation);
// b == (v == c)
Constraint* MakeIsEqualCstCt(IntVar* const v, int64 c, IntVar* const b);
Constraint* MakeIsEqualCstCt(IntExpr* const v, int64 c, IntVar* const b);
// status var of (v == c)
IntVar* MakeIsEqualCstVar(IntVar* const var, int64 value);
IntVar* MakeIsEqualCstVar(IntExpr* const var, int64 value);
// b == (v1 == v2)
Constraint* MakeIsEqualCt(IntExpr* const v1, IntExpr* v2, IntVar* const b);
// status var of (v1 == v2)
IntVar* MakeIsEqualVar(IntExpr* const var, IntExpr* v2);
// left == right
Constraint* MakeEquality(IntVar* const left, IntVar* const right);
Constraint* MakeEquality(IntExpr* const left, IntExpr* const right);
// expr == value
Constraint* MakeEquality(IntExpr* const expr, int64 value);
// expr == value
Constraint* MakeEquality(IntExpr* const expr, int value);
// b == (v != c)
Constraint* MakeIsDifferentCstCt(IntVar* const v, int64 c, IntVar* const b);
Constraint* MakeIsDifferentCstCt(IntExpr* const v, int64 c, IntVar* const b);
// status var of (v != c)
IntVar* MakeIsDifferentCstVar(IntVar* const v, int64 c);
IntVar* MakeIsDifferentCstVar(IntExpr* const v, int64 c);
// status var of (v1 != v2)
IntVar* MakeIsDifferentVar(IntExpr* const v1, IntExpr* const v2);
// b == (v1 != v2)
Constraint* MakeIsDifferentCt(IntExpr* const v1, IntExpr* const v2,
IntVar* const b);
// left != right
Constraint* MakeNonEquality(IntVar* const left, IntVar* const right);
Constraint* MakeNonEquality(IntExpr* const left, IntExpr* const right);
// expr != value
Constraint* MakeNonEquality(IntVar* const expr, int64 value);
Constraint* MakeNonEquality(IntExpr* const expr, int64 value);
// expr != value
Constraint* MakeNonEquality(IntVar* const expr, int value);
Constraint* MakeNonEquality(IntExpr* const expr, int value);
// b == (v <= c)
Constraint* MakeIsLessOrEqualCstCt(IntVar* const v, int64 c,
Constraint* MakeIsLessOrEqualCstCt(IntExpr* const v, int64 c,
IntVar* const b);
// status var of (v <= c)
IntVar* MakeIsLessOrEqualCstVar(IntVar* const v, int64 c);
IntVar* MakeIsLessOrEqualCstVar(IntExpr* const v, int64 c);
// status var of (left <= right)
IntVar* MakeIsLessOrEqualVar(IntExpr* const left, IntExpr* const right);
// b == (left <= right)
Constraint* MakeIsLessOrEqualCt(IntExpr* const left, IntExpr* const right,
IntVar* const b);
// left <= right
Constraint* MakeLessOrEqual(IntVar* const left, IntVar* const right);
Constraint* MakeLessOrEqual(IntExpr* const left, IntExpr* const right);
// expr <= value
Constraint* MakeLessOrEqual(IntExpr* const expr, int64 value);
// expr <= value
Constraint* MakeLessOrEqual(IntExpr* const expr, int value);
// b == (v >= c)
Constraint* MakeIsGreaterOrEqualCstCt(IntVar* const v, int64 c,
Constraint* MakeIsGreaterOrEqualCstCt(IntExpr* const v, int64 c,
IntVar* const b);
// status var of (v >= c)
IntVar* MakeIsGreaterOrEqualCstVar(IntVar* const v, int64 c);
IntVar* MakeIsGreaterOrEqualCstVar(IntExpr* const v, int64 c);
// status var of (left >= right)
IntVar* MakeIsGreaterOrEqualVar(IntExpr* const left, IntExpr* const right);
// b == (left >= right)
Constraint* MakeIsGreaterOrEqualCt(IntExpr* const left, IntExpr* const right,
IntVar* const b);
// left >= right
Constraint* MakeGreaterOrEqual(IntVar* const left, IntVar* const right);
Constraint* MakeGreaterOrEqual(IntExpr* const left, IntExpr* const right);
// expr >= value
Constraint* MakeGreaterOrEqual(IntExpr* const expr, int64 value);
// expr >= value
Constraint* MakeGreaterOrEqual(IntExpr* const expr, int value);
// b == (v > c)
Constraint* MakeIsGreaterCstCt(IntVar* const v, int64 c, IntVar* const b);
Constraint* MakeIsGreaterCstCt(IntExpr* const v, int64 c, IntVar* const b);
// status var of (v > c)
IntVar* MakeIsGreaterCstVar(IntVar* const v, int64 c);
IntVar* MakeIsGreaterCstVar(IntExpr* const v, int64 c);
// status var of (left > right)
IntVar* MakeIsGreaterVar(IntExpr* const left, IntExpr* const right);
// b == (left > right)
Constraint* MakeIsGreaterCt(IntExpr* const left, IntExpr* const right,
IntVar* const b);
// left > right
Constraint* MakeGreater(IntVar* const left, IntVar* const right);
Constraint* MakeGreater(IntExpr* const left, IntExpr* const right);
// expr > value
Constraint* MakeGreater(IntExpr* const expr, int64 value);
// expr > value
Constraint* MakeGreater(IntExpr* const expr, int value);
// b == (v < c)
Constraint* MakeIsLessCstCt(IntVar* const v, int64 c, IntVar* const b);
Constraint* MakeIsLessCstCt(IntExpr* const v, int64 c, IntVar* const b);
// status var of (v < c)
IntVar* MakeIsLessCstVar(IntVar* const v, int64 c);
IntVar* MakeIsLessCstVar(IntExpr* const v, int64 c);
// status var of (left < right)
IntVar* MakeIsLessVar(IntExpr* const left, IntExpr* const right);
// b == (left < right)
Constraint* MakeIsLessCt(IntExpr* const left, IntExpr* const right,
IntVar* const b);
// left < right
Constraint* MakeLess(IntVar* const left, IntVar* const right);
Constraint* MakeLess(IntExpr* const left, IntExpr* const right);
// expr < value
Constraint* MakeLess(IntExpr* const expr, int64 value);
// expr < value

View File

@@ -1408,14 +1408,14 @@ class ModelCache {
VAR_CONSTANT_CONSTANT_CONSTRAINT_MAX,
};
enum VarVarConstraintType {
VAR_VAR_EQUALITY = 0,
VAR_VAR_GREATER,
VAR_VAR_GREATER_OR_EQUAL,
VAR_VAR_LESS,
VAR_VAR_LESS_OR_EQUAL,
VAR_VAR_NON_EQUALITY,
VAR_VAR_CONSTRAINT_MAX,
enum ExprExprConstraintType {
EXPR_EXPR_EQUALITY = 0,
EXPR_EXPR_GREATER,
EXPR_EXPR_GREATER_OR_EQUAL,
EXPR_EXPR_LESS,
EXPR_EXPR_LESS_OR_EQUAL,
EXPR_EXPR_NON_EQUALITY,
EXPR_EXPR_CONSTRAINT_MAX,
};
enum ExprExpressionType {
@@ -1425,28 +1425,16 @@ class ModelCache {
EXPR_EXPRESSION_MAX,
};
enum VarConstantExpressionType {
VAR_CONSTANT_IS_EQUAL = 0,
VAR_CONSTANT_IS_NOT_EQUAL,
VAR_CONSTANT_IS_GREATER_OR_EQUAL,
VAR_CONSTANT_IS_LESS_OR_EQUAL,
VAR_CONSTANT_EXPRESSION_MAX,
};
enum VarVarExpressionType {
VAR_VAR_IS_EQUAL = 0,
VAR_VAR_IS_NOT_EQUAL,
VAR_VAR_IS_LESS,
VAR_VAR_IS_LESS_OR_EQUAL,
VAR_VAR_EXPRESSION_MAX,
};
enum ExprExprExpressionType {
EXPR_EXPR_DIFFERENCE = 0,
EXPR_EXPR_PROD,
EXPR_EXPR_MAX,
EXPR_EXPR_MIN,
EXPR_EXPR_SUM,
EXPR_EXPR_IS_LESS,
EXPR_EXPR_IS_LESS_OR_EQUAL,
EXPR_EXPR_IS_EQUAL,
EXPR_EXPR_IS_NOT_EQUAL,
EXPR_EXPR_EXPRESSION_MAX,
};
@@ -1457,6 +1445,10 @@ class ModelCache {
EXPR_CONSTANT_MAX,
EXPR_CONSTANT_MIN,
EXPR_CONSTANT_SUM,
EXPR_CONSTANT_IS_EQUAL,
EXPR_CONSTANT_IS_NOT_EQUAL,
EXPR_CONSTANT_IS_GREATER_OR_EQUAL,
EXPR_CONSTANT_IS_LESS_OR_EQUAL,
EXPR_CONSTANT_EXPRESSION_MAX,
};
enum VarConstantConstantExpressionType {
@@ -1525,15 +1517,15 @@ class ModelCache {
// Var Var Constraints.
virtual Constraint* FindVarVarConstraint(
IntVar* const var1,
IntVar* const var2,
VarVarConstraintType type) const = 0;
virtual Constraint* FindExprExprConstraint(
IntExpr* const expr1,
IntExpr* const expr2,
ExprExprConstraintType type) const = 0;
virtual void InsertVarVarConstraint(Constraint* const ct,
IntVar* const var1,
IntVar* const var2,
VarVarConstraintType type) = 0;
virtual void InsertExprExprConstraint(Constraint* const ct,
IntExpr* const expr1,
IntExpr* const expr2,
ExprExprConstraintType type) = 0;
// Var Expressions.
@@ -1545,32 +1537,6 @@ class ModelCache {
IntExpr* const expr,
ExprExpressionType type) = 0;
// Var Constant Expressions .
virtual IntExpr* FindVarConstantExpression(
IntVar* const var,
int64 value,
VarConstantExpressionType type) const = 0;
virtual void InsertVarConstantExpression(
IntExpr* const expression,
IntVar* const var,
int64 value,
VarConstantExpressionType type) = 0;
// Var Var Expressions.
virtual IntExpr* FindVarVarExpression(
IntVar* const var1,
IntVar* const var2,
VarVarExpressionType type) const = 0;
virtual void InsertVarVarExpression(
IntExpr* const expression,
IntVar* const var1,
IntVar* const var2,
VarVarExpressionType type) = 0;
// Expr Constant Expressions.
virtual IntExpr* FindExprConstantExpression(

View File

@@ -307,33 +307,33 @@ string DiffCst::DebugString() const {
}
} // namespace
Constraint* Solver::MakeNonEquality(IntVar* const e, int64 v) {
Constraint* Solver::MakeNonEquality(IntExpr* const e, int64 v) {
CHECK_EQ(this, e->solver());
IntExpr* left = NULL;
IntExpr* right = NULL;
if (v == 0 && IsADifference(e, &left, &right)) {
return MakeNonEquality(left->Var(), right->Var());
} else if (!e->Contains(v)) {
return MakeNonEquality(left, right);
} else if (e->IsVar() && !e->Var()->Contains(v)) {
return MakeTrueConstraint();
} else if (e->Bound() && e->Min() == v) {
return MakeFalseConstraint();
} else {
return RevAlloc(new DiffCst(this, e, v));
return RevAlloc(new DiffCst(this, e->Var(), v));
}
}
Constraint* Solver::MakeNonEquality(IntVar* const e, int v) {
Constraint* Solver::MakeNonEquality(IntExpr* const e, int v) {
CHECK_EQ(this, e->solver());
IntExpr* left = NULL;
IntExpr* right = NULL;
if (v == 0 && IsADifference(e, &left, &right)) {
return MakeNonEquality(left->Var(), right->Var());
} else if (!e->Contains(v)) {
} else if (e->IsVar() && !e->Var()->Contains(v)) {
return MakeTrueConstraint();
} else if (e->Bound() && e->Min() == v) {
return MakeFalseConstraint();
} else {
return RevAlloc(new DiffCst(this, e, v));
return RevAlloc(new DiffCst(this, e->Var(), v));
}
}
// ----- is_equal_cst Constraint -----
@@ -389,7 +389,7 @@ class IsEqualCstCt : public CastConstraint {
};
} // namespace
IntVar* Solver::MakeIsEqualCstVar(IntVar* const var, int64 value) {
IntVar* Solver::MakeIsEqualCstVar(IntExpr* const var, int64 value) {
IntExpr* left = NULL;
IntExpr* right = NULL;
if (value == 0 && IsADifference(var, &left, &right)) {
@@ -404,10 +404,19 @@ IntVar* Solver::MakeIsEqualCstVar(IntVar* const var, int64 value) {
return MakeIntConst(0);
}
}
return var->IsEqual(value);
if (var->IsVar()) {
return var->Var()->IsEqual(value);
} else {
IntVar* const boolvar =
MakeBoolVar(StringPrintf("Is(%s == %" GG_LL_FORMAT "d",
var->DebugString().c_str(),
value));
AddConstraint(MakeIsEqualCstCt(var, value, boolvar));
return boolvar;
}
}
Constraint* Solver::MakeIsEqualCstCt(IntVar* const var,
Constraint* Solver::MakeIsEqualCstCt(IntExpr* const var,
int64 value,
IntVar* const boolvar) {
CHECK_EQ(this, var->solver());
@@ -427,17 +436,17 @@ Constraint* Solver::MakeIsEqualCstCt(IntVar* const var,
}
// TODO(user) : what happens if the constraint is not posted?
// The cache becomes tainted.
model_cache_->InsertVarConstantExpression(
model_cache_->InsertExprConstantExpression(
boolvar,
var,
value,
ModelCache::VAR_CONSTANT_IS_EQUAL);
ModelCache::EXPR_CONSTANT_IS_EQUAL);
IntExpr* left = NULL;
IntExpr* right = NULL;
if (value == 0 && IsADifference(var, &left, &right)) {
return MakeIsEqualCt(left, right, boolvar);
} else {
return RevAlloc(new IsEqualCstCt(this, var, value, boolvar));
return RevAlloc(new IsEqualCstCt(this, var->Var(), value, boolvar));
}
}
@@ -497,16 +506,16 @@ class IsDiffCstCt : public CastConstraint {
};
} // namespace
IntVar* Solver::MakeIsDifferentCstVar(IntVar* const var, int64 value) {
IntVar* Solver::MakeIsDifferentCstVar(IntExpr* const var, int64 value) {
IntExpr* left = NULL;
IntExpr* right = NULL;
if (value == 0 && IsADifference(var, &left, &right)) {
return MakeIsDifferentVar(left, right);
}
return var->IsDifferent(value);
return var->Var()->IsDifferent(value);
}
Constraint* Solver::MakeIsDifferentCstCt(IntVar* const var,
Constraint* Solver::MakeIsDifferentCstCt(IntExpr* const var,
int64 value,
IntVar* const boolvar) {
CHECK_EQ(this, var->solver());
@@ -517,10 +526,10 @@ Constraint* Solver::MakeIsDifferentCstCt(IntVar* const var,
if (value == var->Max()) {
return MakeIsLessOrEqualCstCt(var, value - 1, boolvar);
}
if (!var->Contains(value)) {
if (var->IsVar() && !var->Var()->Contains(value)) {
return MakeEquality(boolvar, 1LL);
}
if (var->Bound() && var->Value() == value) {
if (var->Bound() && var->Min() == value) {
return MakeEquality(boolvar, Zero());
}
if (boolvar->Bound()) {
@@ -530,17 +539,17 @@ Constraint* Solver::MakeIsDifferentCstCt(IntVar* const var,
return MakeNonEquality(var, value);
}
}
model_cache_->InsertVarConstantExpression(
model_cache_->InsertExprConstantExpression(
boolvar,
var,
value,
ModelCache::VAR_CONSTANT_IS_NOT_EQUAL);
ModelCache::EXPR_CONSTANT_IS_NOT_EQUAL);
IntExpr* left = NULL;
IntExpr* right = NULL;
if (value == 0 && IsADifference(var, &left, &right)) {
return MakeIsDifferentCt(left, right, boolvar);
} else {
return RevAlloc(new IsDiffCstCt(this, var, value, boolvar));
return RevAlloc(new IsDiffCstCt(this, var->Var(), value, boolvar));
}
}
@@ -549,7 +558,7 @@ Constraint* Solver::MakeIsDifferentCstCt(IntVar* const var,
namespace {
class IsGreaterEqualCstCt : public CastConstraint {
public:
IsGreaterEqualCstCt(Solver* const s, IntVar* const v, int64 c,
IsGreaterEqualCstCt(Solver* const s, IntExpr* const v, int64 c,
IntVar* const b)
: CastConstraint(s, b), var_(v), cst_(c), demon_(NULL) {}
virtual void Post() {
@@ -592,27 +601,36 @@ class IsGreaterEqualCstCt : public CastConstraint {
}
private:
IntVar* const var_;
IntExpr* const var_;
int64 cst_;
Demon* demon_;
};
} // namespace
IntVar* Solver::MakeIsGreaterOrEqualCstVar(IntVar* const var, int64 value) {
IntVar* Solver::MakeIsGreaterOrEqualCstVar(IntExpr* const var, int64 value) {
if (var->Min() >= value) {
return MakeIntConst(1LL);
}
if (var->Max() < value) {
return MakeIntConst(0LL);
}
return var->IsGreaterOrEqual(value);
if (var->IsVar()) {
return var->Var()->IsGreaterOrEqual(value);
} else {
IntVar* const boolvar =
MakeBoolVar(StringPrintf("Is(%s >= %" GG_LL_FORMAT "d",
var->DebugString().c_str(),
value));
AddConstraint(MakeIsGreaterOrEqualCstCt(var, value, boolvar));
return boolvar;
}
}
IntVar* Solver::MakeIsGreaterCstVar(IntVar* const var, int64 value) {
IntVar* Solver::MakeIsGreaterCstVar(IntExpr* const var, int64 value) {
return MakeIsGreaterOrEqualCstVar(var, value + 1);
}
Constraint* Solver::MakeIsGreaterOrEqualCstCt(IntVar* const var,
Constraint* Solver::MakeIsGreaterOrEqualCstCt(IntExpr* const var,
int64 value,
IntVar* const boolvar) {
if (boolvar->Bound()) {
@@ -624,15 +642,15 @@ Constraint* Solver::MakeIsGreaterOrEqualCstCt(IntVar* const var,
}
CHECK_EQ(this, var->solver());
CHECK_EQ(this, boolvar->solver());
model_cache_->InsertVarConstantExpression(
model_cache_->InsertExprConstantExpression(
boolvar,
var,
value,
ModelCache::VAR_CONSTANT_IS_GREATER_OR_EQUAL);
ModelCache::EXPR_CONSTANT_IS_GREATER_OR_EQUAL);
return RevAlloc(new IsGreaterEqualCstCt(this, var, value, boolvar));
}
Constraint* Solver::MakeIsGreaterCstCt(IntVar* const v, int64 c,
Constraint* Solver::MakeIsGreaterCstCt(IntExpr* const v, int64 c,
IntVar* const b) {
return MakeIsGreaterOrEqualCstCt(v, c + 1, b);
}
@@ -642,7 +660,7 @@ Constraint* Solver::MakeIsGreaterCstCt(IntVar* const v, int64 c,
namespace {
class IsLessEqualCstCt : public CastConstraint {
public:
IsLessEqualCstCt(Solver* const s, IntVar* const v, int64 c, IntVar* const b)
IsLessEqualCstCt(Solver* const s, IntExpr* const v, int64 c, IntVar* const b)
: CastConstraint(s, b), var_(v), cst_(c), demon_(NULL) {}
virtual void Post() {
@@ -687,28 +705,37 @@ class IsLessEqualCstCt : public CastConstraint {
}
private:
IntVar* const var_;
IntExpr* const var_;
int64 cst_;
Demon* demon_;
};
} // namespace
IntVar* Solver::MakeIsLessOrEqualCstVar(IntVar* const var, int64 value) {
IntVar* Solver::MakeIsLessOrEqualCstVar(IntExpr* const var, int64 value) {
if (var->Max() <= value) {
return MakeIntConst(1LL);
}
if (var->Min() > value) {
return MakeIntConst(0LL);
}
return var->IsLessOrEqual(value);
if (var->IsVar()) {
return var->Var()->IsLessOrEqual(value);
} else {
IntVar* const boolvar =
MakeBoolVar(StringPrintf("Is(%s <= %" GG_LL_FORMAT "d",
var->DebugString().c_str(),
value));
AddConstraint(MakeIsLessOrEqualCstCt(var, value, boolvar));
return boolvar;
}
}
IntVar* Solver::MakeIsLessCstVar(IntVar* const var, int64 value) {
IntVar* Solver::MakeIsLessCstVar(IntExpr* const var, int64 value) {
return MakeIsLessOrEqualCstVar(var, value - 1);
}
Constraint* Solver::MakeIsLessOrEqualCstCt(IntVar* const var,
Constraint* Solver::MakeIsLessOrEqualCstCt(IntExpr* const var,
int64 value,
IntVar* const boolvar) {
if (boolvar->Bound()) {
@@ -720,15 +747,15 @@ Constraint* Solver::MakeIsLessOrEqualCstCt(IntVar* const var,
}
CHECK_EQ(this, var->solver());
CHECK_EQ(this, boolvar->solver());
model_cache_->InsertVarConstantExpression(
model_cache_->InsertExprConstantExpression(
boolvar,
var,
value,
ModelCache::VAR_CONSTANT_IS_LESS_OR_EQUAL);
ModelCache::EXPR_CONSTANT_IS_LESS_OR_EQUAL);
return RevAlloc(new IsLessEqualCstCt(this, var, value, boolvar));
}
Constraint* Solver::MakeIsLessCstCt(IntVar* const v, int64 c,
Constraint* Solver::MakeIsLessCstCt(IntExpr* const v, int64 c,
IntVar* const b) {
return MakeIsLessOrEqualCstCt(v, c - 1, b);
}

View File

@@ -357,10 +357,9 @@ class NonReversibleCache : public ModelCache {
typedef Cache1<IntExpr, std::vector<IntVar*> > VarArrayIntExprCache;
typedef Cache2<Constraint, IntVar*, int64> VarConstantConstraintCache;
typedef Cache2<Constraint, IntVar*, IntVar*> VarVarConstraintCache;
typedef Cache2<Constraint, IntExpr*, IntExpr*> ExprExprConstraintCache;
typedef Cache2<IntExpr, IntVar*, int64> VarConstantIntExprCache;
typedef Cache2<IntExpr, IntExpr*, int64> ExprConstantIntExprCache;
typedef Cache2<IntExpr, IntVar*, IntVar*> VarVarIntExprCache;
typedef Cache2<IntExpr, IntExpr*, IntExpr*> ExprExprIntExprCache;
typedef Cache2<IntExpr, IntVar*, ConstIntArray*> VarConstantArrayIntExprCache;
typedef Cache2<IntExpr, std::vector<IntVar*>, ConstIntArray*> VarArrayConstantArrayIntExprCache;
@@ -377,8 +376,8 @@ class NonReversibleCache : public ModelCache {
for (int i = 0; i < VAR_CONSTANT_CONSTRAINT_MAX; ++i) {
var_constant_constraints_.push_back(new VarConstantConstraintCache);
}
for (int i = 0; i < VAR_VAR_CONSTRAINT_MAX; ++i) {
var_var_constraints_.push_back(new VarVarConstraintCache);
for (int i = 0; i < EXPR_EXPR_CONSTRAINT_MAX; ++i) {
expr_expr_constraints_.push_back(new ExprExprConstraintCache);
}
for (int i = 0; i < VAR_CONSTANT_CONSTANT_CONSTRAINT_MAX; ++i) {
var_constant_constant_constraints_.push_back(
@@ -387,15 +386,9 @@ class NonReversibleCache : public ModelCache {
for (int i = 0; i < EXPR_EXPRESSION_MAX; ++i) {
expr_expressions_.push_back(new ExprIntExprCache);
}
for (int i = 0; i < VAR_CONSTANT_EXPRESSION_MAX; ++i) {
var_constant_expressions_.push_back(new VarConstantIntExprCache);
}
for (int i = 0; i < EXPR_CONSTANT_EXPRESSION_MAX; ++i) {
expr_constant_expressions_.push_back(new ExprConstantIntExprCache);
}
for (int i = 0; i < VAR_VAR_EXPRESSION_MAX; ++i) {
var_var_expressions_.push_back(new VarVarIntExprCache);
}
for (int i = 0; i < EXPR_EXPR_EXPRESSION_MAX; ++i) {
expr_expr_expressions_.push_back(new ExprExprIntExprCache);
}
@@ -422,11 +415,9 @@ class NonReversibleCache : public ModelCache {
virtual ~NonReversibleCache() {
STLDeleteElements(&var_constant_constraints_);
STLDeleteElements(&var_var_constraints_);
STLDeleteElements(&expr_expr_constraints_);
STLDeleteElements(&var_constant_constant_constraints_);
STLDeleteElements(&expr_expressions_);
STLDeleteElements(&var_constant_expressions_);
STLDeleteElements(&var_var_expressions_);
STLDeleteElements(&expr_constant_expressions_);
STLDeleteElements(&expr_expr_expressions_);
STLDeleteElements(&var_constant_constant_expressions_);
@@ -517,29 +508,29 @@ class NonReversibleCache : public ModelCache {
// Var Var Constraint.
virtual Constraint* FindVarVarConstraint(
IntVar* const var1,
IntVar* const var2,
VarVarConstraintType type) const {
virtual Constraint* FindExprExprConstraint(
IntExpr* const var1,
IntExpr* const var2,
ExprExprConstraintType type) const {
DCHECK(var1 != NULL);
DCHECK(var2 != NULL);
DCHECK_GE(type, 0);
DCHECK_LT(type, VAR_VAR_CONSTRAINT_MAX);
return var_var_constraints_[type]->Find(var1, var2);
DCHECK_LT(type, EXPR_EXPR_CONSTRAINT_MAX);
return expr_expr_constraints_[type]->Find(var1, var2);
}
virtual void InsertVarVarConstraint(Constraint* const ct,
IntVar* const var1,
IntVar* const var2,
VarVarConstraintType type) {
virtual void InsertExprExprConstraint(Constraint* const ct,
IntExpr* const var1,
IntExpr* const var2,
ExprExprConstraintType type) {
DCHECK(ct != NULL);
DCHECK(var1 != NULL);
DCHECK(var2 != NULL);
DCHECK_GE(type, 0);
DCHECK_LT(type, VAR_VAR_CONSTRAINT_MAX);
DCHECK_LT(type, EXPR_EXPR_CONSTRAINT_MAX);
if (solver()->state() != Solver::IN_SEARCH &&
var_var_constraints_[type]->Find(var1, var2) == NULL) {
var_var_constraints_[type]->UnsafeInsert(var1, var2, ct);
expr_expr_constraints_[type]->Find(var1, var2) == NULL) {
expr_expr_constraints_[type]->UnsafeInsert(var1, var2, ct);
}
}
@@ -566,62 +557,6 @@ class NonReversibleCache : public ModelCache {
}
}
// Var Constant Expression.
virtual IntExpr* FindVarConstantExpression(
IntVar* const var,
int64 value,
VarConstantExpressionType type) const {
DCHECK(var != NULL);
DCHECK_GE(type, 0);
DCHECK_LT(type, VAR_CONSTANT_EXPRESSION_MAX);
return var_constant_expressions_[type]->Find(var, value);
}
virtual void InsertVarConstantExpression(
IntExpr* const expression,
IntVar* const var,
int64 value,
VarConstantExpressionType type) {
DCHECK(expression != NULL);
DCHECK(var != NULL);
DCHECK_GE(type, 0);
DCHECK_LT(type, VAR_CONSTANT_EXPRESSION_MAX);
if (solver()->state() != Solver::IN_SEARCH &&
var_constant_expressions_[type]->Find(var, value) == NULL) {
var_constant_expressions_[type]->UnsafeInsert(var, value, expression);
}
}
// Var Var Expression.
virtual IntExpr* FindVarVarExpression(
IntVar* const var1,
IntVar* const var2,
VarVarExpressionType type) const {
DCHECK(var1 != NULL);
DCHECK(var2 != NULL);
DCHECK_GE(type, 0);
DCHECK_LT(type, VAR_VAR_EXPRESSION_MAX);
return var_var_expressions_[type]->Find(var1, var2);
}
virtual void InsertVarVarExpression(
IntExpr* const expression,
IntVar* const var1,
IntVar* const var2,
VarVarExpressionType type) {
DCHECK(expression != NULL);
DCHECK(var1 != NULL);
DCHECK(var2 != NULL);
DCHECK_GE(type, 0);
DCHECK_LT(type, VAR_VAR_EXPRESSION_MAX);
if (solver()->state() != Solver::IN_SEARCH &&
var_var_expressions_[type]->Find(var1, var2) == NULL) {
var_var_expressions_[type]->UnsafeInsert(var1, var2, expression);
}
}
// Expr Constant Expressions.
virtual IntExpr* FindExprConstantExpression(
@@ -821,12 +756,10 @@ class NonReversibleCache : public ModelCache {
private:
std::vector<Constraint*> void_constraints_;
std::vector<VarConstantConstraintCache*> var_constant_constraints_;
std::vector<VarVarConstraintCache*> var_var_constraints_;
std::vector<ExprExprConstraintCache*> expr_expr_constraints_;
std::vector<VarConstantConstantConstraintCache*>
var_constant_constant_constraints_;
std::vector<ExprIntExprCache*> expr_expressions_;
std::vector<VarConstantIntExprCache*> var_constant_expressions_;
std::vector<VarVarIntExprCache*> var_var_expressions_;
std::vector<ExprConstantIntExprCache*> expr_constant_expressions_;
std::vector<ExprExprIntExprCache*> expr_expr_expressions_;
std::vector<VarConstantConstantIntExprCache*> var_constant_constant_expressions_;

View File

@@ -28,7 +28,7 @@ namespace operations_research {
namespace {
class RangeEquality : public Constraint {
public:
RangeEquality(Solver* const s, IntVar* const l, IntVar* const r)
RangeEquality(Solver* const s, IntExpr* const l, IntExpr* const r)
: Constraint(s), left_(l), right_(r) {}
virtual ~RangeEquality() {}
@@ -61,8 +61,8 @@ class RangeEquality : public Constraint {
}
private:
IntVar* const left_;
IntVar* const right_;
IntExpr* const left_;
IntExpr* const right_;
};
//-----------------------------------------------------------------------------
@@ -70,7 +70,7 @@ class RangeEquality : public Constraint {
class RangeLessOrEqual : public Constraint {
public:
RangeLessOrEqual(Solver* const s, IntVar* const l, IntVar* const r);
RangeLessOrEqual(Solver* const s, IntExpr* const l, IntExpr* const r);
virtual ~RangeLessOrEqual() {}
virtual void Post();
virtual void InitialPropagate();
@@ -87,12 +87,12 @@ class RangeLessOrEqual : public Constraint {
}
private:
IntVar* const left_;
IntVar* const right_;
IntExpr* const left_;
IntExpr* const right_;
};
RangeLessOrEqual::RangeLessOrEqual(Solver* const s, IntVar* const l,
IntVar* const r)
RangeLessOrEqual::RangeLessOrEqual(Solver* const s, IntExpr* const l,
IntExpr* const r)
: Constraint(s), left_(l), right_(r) {}
void RangeLessOrEqual::Post() {
@@ -115,7 +115,7 @@ string RangeLessOrEqual::DebugString() const {
class RangeGreaterOrEqual : public Constraint {
public:
RangeGreaterOrEqual(Solver* const s, IntVar* const l, IntVar* const r);
RangeGreaterOrEqual(Solver* const s, IntExpr* const l, IntExpr* const r);
virtual ~RangeGreaterOrEqual() {}
virtual void Post();
virtual void InitialPropagate();
@@ -132,12 +132,12 @@ class RangeGreaterOrEqual : public Constraint {
}
private:
IntVar* const left_;
IntVar* const right_;
IntExpr* const left_;
IntExpr* const right_;
};
RangeGreaterOrEqual::RangeGreaterOrEqual(Solver* const s, IntVar* const l,
IntVar* const r)
RangeGreaterOrEqual::RangeGreaterOrEqual(Solver* const s, IntExpr* const l,
IntExpr* const r)
: Constraint(s), left_(l), right_(r) {}
void RangeGreaterOrEqual::Post() {
@@ -160,7 +160,7 @@ string RangeGreaterOrEqual::DebugString() const {
class RangeLess : public Constraint {
public:
RangeLess(Solver* const s, IntVar* const l, IntVar* const r);
RangeLess(Solver* const s, IntExpr* const l, IntExpr* const r);
virtual ~RangeLess() {}
virtual void Post();
virtual void InitialPropagate();
@@ -177,11 +177,11 @@ class RangeLess : public Constraint {
}
private:
IntVar* const left_;
IntVar* const right_;
IntExpr* const left_;
IntExpr* const right_;
};
RangeLess::RangeLess(Solver* const s, IntVar* const l, IntVar* const r)
RangeLess::RangeLess(Solver* const s, IntExpr* const l, IntExpr* const r)
: Constraint(s), left_(l), right_(r) {}
void RangeLess::Post() {
@@ -204,7 +204,7 @@ string RangeLess::DebugString() const {
class RangeGreater : public Constraint {
public:
RangeGreater(Solver* const s, IntVar* const l, IntVar* const r);
RangeGreater(Solver* const s, IntExpr* const l, IntExpr* const r);
virtual ~RangeGreater() {}
virtual void Post();
virtual void InitialPropagate();
@@ -221,11 +221,11 @@ class RangeGreater : public Constraint {
}
private:
IntVar* const left_;
IntVar* const right_;
IntExpr* const left_;
IntExpr* const right_;
};
RangeGreater::RangeGreater(Solver* const s, IntVar* const l, IntVar* const r)
RangeGreater::RangeGreater(Solver* const s, IntExpr* const l, IntExpr* const r)
: Constraint(s), left_(l), right_(r) {}
void RangeGreater::Post() {
@@ -634,8 +634,8 @@ class IsDifferentCt : public CastConstraint {
class IsLessOrEqualCt : public CastConstraint {
public:
IsLessOrEqualCt(Solver* const s,
IntVar* const l,
IntVar* const r,
IntExpr* const l,
IntExpr* const r,
IntVar* const b)
: CastConstraint(s, b),
left_(l),
@@ -687,16 +687,16 @@ class IsLessOrEqualCt : public CastConstraint {
}
private:
IntVar* const left_;
IntVar* const right_;
IntExpr* const left_;
IntExpr* const right_;
Demon* demon_;
};
class IsLessCt : public CastConstraint {
public:
IsLessCt(Solver* const s,
IntVar* const l,
IntVar* const r,
IntExpr* const l,
IntExpr* const r,
IntVar* const b)
: CastConstraint(s, b),
left_(l),
@@ -748,13 +748,13 @@ class IsLessCt : public CastConstraint {
}
private:
IntVar* const left_;
IntVar* const right_;
IntExpr* const left_;
IntExpr* const right_;
Demon* demon_;
};
} // namespace
Constraint* Solver::MakeEquality(IntVar* const l, IntVar* const r) {
Constraint* Solver::MakeEquality(IntExpr* const l, IntExpr* const r) {
CHECK(l != NULL) << "left expression NULL, maybe a bad cast";
CHECK(r != NULL) << "left expression NULL, maybe a bad cast";
CHECK_EQ(this, l->solver());
@@ -768,7 +768,7 @@ Constraint* Solver::MakeEquality(IntVar* const l, IntVar* const r) {
}
}
Constraint* Solver::MakeLessOrEqual(IntVar* const l, IntVar* const r) {
Constraint* Solver::MakeLessOrEqual(IntExpr* const l, IntExpr* const r) {
CHECK(l != NULL) << "left expression NULL, maybe a bad cast";
CHECK(r != NULL) << "left expression NULL, maybe a bad cast";
CHECK_EQ(this, l->solver());
@@ -782,7 +782,7 @@ Constraint* Solver::MakeLessOrEqual(IntVar* const l, IntVar* const r) {
}
}
Constraint* Solver::MakeGreaterOrEqual(IntVar* const l, IntVar* const r) {
Constraint* Solver::MakeGreaterOrEqual(IntExpr* const l, IntExpr* const r) {
CHECK(l != NULL) << "left expression NULL, maybe a bad cast";
CHECK(r != NULL) << "left expression NULL, maybe a bad cast";
CHECK_EQ(this, l->solver());
@@ -796,7 +796,7 @@ Constraint* Solver::MakeGreaterOrEqual(IntVar* const l, IntVar* const r) {
}
}
Constraint* Solver::MakeLess(IntVar* const l, IntVar* const r) {
Constraint* Solver::MakeLess(IntExpr* const l, IntExpr* const r) {
CHECK(l != NULL) << "left expression NULL, maybe a bad cast";
CHECK(r != NULL) << "left expression NULL, maybe a bad cast";
CHECK_EQ(this, l->solver());
@@ -810,7 +810,7 @@ Constraint* Solver::MakeLess(IntVar* const l, IntVar* const r) {
}
}
Constraint* Solver::MakeGreater(IntVar* const l, IntVar* const r) {
Constraint* Solver::MakeGreater(IntExpr* const l, IntExpr* const r) {
CHECK(l != NULL) << "left expression NULL, maybe a bad cast";
CHECK(r != NULL) << "left expression NULL, maybe a bad cast";
CHECK_EQ(this, l->solver());
@@ -824,7 +824,7 @@ Constraint* Solver::MakeGreater(IntVar* const l, IntVar* const r) {
}
}
Constraint* Solver::MakeNonEquality(IntVar* const l, IntVar* const r) {
Constraint* Solver::MakeNonEquality(IntExpr* const l, IntExpr* const r) {
CHECK(l != NULL) << "left expression NULL, maybe a bad cast";
CHECK(r != NULL) << "left expression NULL, maybe a bad cast";
CHECK_EQ(this, l->solver());
@@ -834,7 +834,7 @@ Constraint* Solver::MakeNonEquality(IntVar* const l, IntVar* const r) {
} else if (r->Bound()) {
return MakeNonEquality(l, r->Min());
}
return RevAlloc(new DiffVar(this, l, r));
return RevAlloc(new DiffVar(this, l->Var(), r->Var()));
}
IntVar* Solver::MakeIsEqualVar(IntExpr* const v1, IntExpr* const v2) {
@@ -847,10 +847,10 @@ IntVar* Solver::MakeIsEqualVar(IntExpr* const v1, IntExpr* const v2) {
}
IntVar* const var1 = v1->Var();
IntVar* const var2 = v2->Var();
IntExpr* const cache = model_cache_->FindVarVarExpression(
IntExpr* const cache = model_cache_->FindExprExprExpression(
var1,
var2,
ModelCache::VAR_VAR_IS_EQUAL);
ModelCache::EXPR_EXPR_IS_EQUAL);
if (cache != NULL) {
return cache->Var();
} else {
@@ -865,11 +865,11 @@ IntVar* Solver::MakeIsEqualVar(IntExpr* const v1, IntExpr* const v2) {
IntVar* const boolvar = MakeBoolVar(
StringPrintf("IsEqualVar(%s, %s)", name1.c_str(), name2.c_str()));
AddConstraint(MakeIsEqualCt(v1, v2, boolvar));
model_cache_->InsertVarVarExpression(
model_cache_->InsertExprExprExpression(
boolvar,
var1,
var2,
ModelCache::VAR_VAR_IS_EQUAL);
ModelCache::EXPR_EXPR_IS_EQUAL);
return boolvar;
}
}
@@ -904,10 +904,10 @@ IntVar* Solver::MakeIsDifferentVar(IntExpr* const v1, IntExpr* const v2) {
}
IntVar* const var1 = v1->Var();
IntVar* const var2 = v2->Var();
IntExpr* const cache = model_cache_->FindVarVarExpression(
IntExpr* const cache = model_cache_->FindExprExprExpression(
var1,
var2,
ModelCache::VAR_VAR_IS_NOT_EQUAL);
ModelCache::EXPR_EXPR_IS_NOT_EQUAL);
if (cache != NULL) {
return cache->Var();
} else {
@@ -922,11 +922,11 @@ IntVar* Solver::MakeIsDifferentVar(IntExpr* const v1, IntExpr* const v2) {
IntVar* const boolvar = MakeBoolVar(
StringPrintf("IsDifferentVar(%s, %s)", name1.c_str(), name2.c_str()));
AddConstraint(MakeIsDifferentCt(v1, v2, boolvar));
model_cache_->InsertVarVarExpression(
model_cache_->InsertExprExprExpression(
boolvar,
var1,
var2,
ModelCache::VAR_VAR_IS_NOT_EQUAL);
ModelCache::EXPR_EXPR_IS_NOT_EQUAL);
return boolvar;
}
}
@@ -944,8 +944,8 @@ Constraint* Solver::MakeIsDifferentCt(IntExpr* const v1,
return RevAlloc(new IsDifferentCt(this, v1->Var(), v2->Var(), b));
}
IntVar* Solver::MakeIsLessOrEqualVar(
IntExpr* const left, IntExpr* const right) {
IntVar* Solver::MakeIsLessOrEqualVar(IntExpr* const left,
IntExpr* const right) {
CHECK_EQ(this, left->solver());
CHECK_EQ(this, right->solver());
if (left->Bound()) {
@@ -953,33 +953,31 @@ IntVar* Solver::MakeIsLessOrEqualVar(
} else if (right->Bound()) {
return MakeIsLessOrEqualCstVar(left->Var(), right->Min());
}
IntVar* const var1 = left->Var();
IntVar* const var2 = right->Var();
IntExpr* const cache = model_cache_->FindVarVarExpression(
var1,
var2,
ModelCache::VAR_VAR_IS_LESS_OR_EQUAL);
IntExpr* const cache = model_cache_->FindExprExprExpression(
left,
right,
ModelCache::EXPR_EXPR_IS_LESS_OR_EQUAL);
if (cache != NULL) {
return cache->Var();
} else {
string name1 = var1->name();
string name1 = left->name();
if (name1.empty()) {
name1 = var1->DebugString();
name1 = left->DebugString();
}
string name2 = var2->name();
string name2 = right->name();
if (name2.empty()) {
name2 = var2->DebugString();
name2 = right->DebugString();
}
IntVar* const boolvar = MakeBoolVar(
StringPrintf("IsLessOrEqual(%s, %s)", name1.c_str(), name2.c_str()));
AddConstraint(RevAlloc(
new IsLessOrEqualCt(this, left->Var(), right->Var(), boolvar)));
model_cache_->InsertVarVarExpression(
model_cache_->InsertExprExprExpression(
boolvar,
var1,
var2,
ModelCache::VAR_VAR_IS_LESS_OR_EQUAL);
left,
right,
ModelCache::EXPR_EXPR_IS_LESS_OR_EQUAL);
return boolvar;
}
}
@@ -1005,33 +1003,31 @@ IntVar* Solver::MakeIsLessVar(
} else if (right->Bound()) {
return MakeIsLessCstVar(left->Var(), right->Min());
}
IntVar* const var1 = left->Var();
IntVar* const var2 = right->Var();
IntExpr* const cache = model_cache_->FindVarVarExpression(
var1,
var2,
ModelCache::VAR_VAR_IS_LESS);
IntExpr* const cache = model_cache_->FindExprExprExpression(
left,
right,
ModelCache::EXPR_EXPR_IS_LESS);
if (cache != NULL) {
return cache->Var();
} else {
string name1 = var1->name();
string name1 = left->name();
if (name1.empty()) {
name1 = var1->DebugString();
name1 = left->DebugString();
}
string name2 = var2->name();
string name2 = right->name();
if (name2.empty()) {
name2 = var2->DebugString();
name2 = right->DebugString();
}
IntVar* const boolvar = MakeBoolVar(
StringPrintf("IsLessOrEqual(%s, %s)", name1.c_str(), name2.c_str()));
AddConstraint(RevAlloc(
new IsLessCt(this, left->Var(), right->Var(), boolvar)));
model_cache_->InsertVarVarExpression(
model_cache_->InsertExprExprExpression(
boolvar,
var1,
var2,
ModelCache::VAR_VAR_IS_LESS);
left,
right,
ModelCache::EXPR_EXPR_IS_LESS);
return boolvar;
}
}

View File

@@ -132,7 +132,7 @@ void p_int_eq(FlatZincModel* const model, CtSpec* const spec) {
} else {
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeEquality(left->Var(), right->Var());
Constraint* const ct = solver->MakeEquality(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -142,7 +142,7 @@ void p_int_ne(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeNonEquality(left->Var(), right->Var());
Constraint* const ct = solver->MakeNonEquality(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -151,7 +151,7 @@ void p_int_ge(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeGreaterOrEqual(left->Var(), right->Var());
Constraint* const ct = solver->MakeGreaterOrEqual(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -160,7 +160,7 @@ void p_int_gt(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeGreater(left->Var(), right->Var());
Constraint* const ct = solver->MakeGreater(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -169,7 +169,7 @@ void p_int_le(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeLessOrEqual(left->Var(), right->Var());
Constraint* const ct = solver->MakeLessOrEqual(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -178,7 +178,7 @@ void p_int_lt(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeLess(left->Var(), right->Var());
Constraint* const ct = solver->MakeLess(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -192,7 +192,7 @@ void p_int_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
if (spec->IsDefined(node_boolvar)) {
IntVar* const boolvar =
node_right->isInt() ?
solver->MakeIsEqualCstVar(left->Var(), node_right->getInt()) :
solver->MakeIsEqualCstVar(left, node_right->getInt()) :
solver->MakeIsEqualVar(left, model->GetIntExpr(node_right));
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
@@ -210,20 +210,21 @@ void p_int_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
void p_int_ne_reif(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntVar* const left = model->GetIntExpr(spec->Arg(0))->Var();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
AST::Node* const node_right = spec->Arg(1);
AST::Node* const node_boolvar = spec->Arg(2);
if (spec->IsDefined(node_boolvar)) {
IntVar* const boolvar = node_right->isInt() ?
IntVar* const boolvar =
node_right->isInt() ?
solver->MakeIsDifferentCstVar(left, node_right->getInt()) :
solver->MakeIsDifferentVar(left, model->GetIntExpr(node_right)->Var());
solver->MakeIsDifferentVar(left, model->GetIntExpr(node_right));
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
model->CheckIntegerVariableIsNull(node_boolvar);
model->SetIntegerExpression(node_boolvar, boolvar);
CHECK_NOTNULL(boolvar);
} else {
IntVar* const right = model->GetIntExpr(spec->Arg(1))->Var();
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
Constraint* const ct = solver->MakeIsDifferentCt(left, right, boolvar);
VLOG(1) << " - posted " << ct->DebugString();
@@ -233,21 +234,21 @@ void p_int_ne_reif(FlatZincModel* const model, CtSpec* const spec) {
void p_int_ge_reif(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntVar* const left = model->GetIntExpr(spec->Arg(0))->Var();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
AST::Node* const node_right = spec->Arg(1);
AST::Node* const node_boolvar = spec->Arg(2);
if (spec->IsDefined(node_boolvar)) {
IntVar* const boolvar = node_right->isInt() ?
IntVar* const boolvar =
node_right->isInt() ?
solver->MakeIsGreaterOrEqualCstVar(left, node_right->getInt()) :
solver->MakeIsGreaterOrEqualVar(left,
model->GetIntExpr(node_right)->Var());
solver->MakeIsGreaterOrEqualVar(left, model->GetIntExpr(node_right));
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
model->CheckIntegerVariableIsNull(node_boolvar);
model->SetIntegerExpression(node_boolvar, boolvar);
CHECK_NOTNULL(boolvar);
} else {
IntVar* const right = model->GetIntExpr(spec->Arg(1))->Var();
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
Constraint* const ct = solver->MakeIsGreaterOrEqualCt(left, right, boolvar);
VLOG(1) << " - posted " << ct->DebugString();
@@ -257,8 +258,8 @@ void p_int_ge_reif(FlatZincModel* const model, CtSpec* const spec) {
void p_int_gt_reif(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntVar* const left = model->GetIntExpr(spec->Arg(0))->Var();
IntVar* const right = model->GetIntExpr(spec->Arg(1))->Var();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
IntVar* const boolvar = model->GetIntExpr(spec->Arg(2))->Var();
Constraint* const ct = solver->MakeIsGreaterCt(left, right, boolvar);
VLOG(1) << " - posted " << ct->DebugString();
@@ -272,8 +273,8 @@ void p_int_le_reif(FlatZincModel* const model, CtSpec* const spec) {
AST::Node* const node_boolvar = spec->Arg(2);
if (spec->IsDefined(node_boolvar)) {
IntVar* const boolvar = node_right->isInt() ?
solver->MakeIsLessOrEqualCstVar(left->Var(), node_right->getInt()) :
solver->MakeIsLessOrEqualVar(left, model->GetIntExpr(node_right));
solver->MakeIsLessOrEqualCstVar(left, node_right->getInt()) :
solver->MakeIsLessOrEqualVar(left, model->GetIntExpr(node_right));
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
model->CheckIntegerVariableIsNull(node_boolvar);
@@ -334,8 +335,8 @@ void p_int_lin_eq(FlatZincModel* const model, CtSpec* const spec) {
coefficients.push_back(constant - rhs);
variables.push_back(solver->MakeIntConst(1));
}
IntVar* const target =
solver->MakeScalProd(variables, coefficients)->Var();
IntExpr* const target =
solver->MakeScalProd(variables, coefficients);
VLOG(1) << " - creating " << defined->DebugString() << " := "
<< target->DebugString();
model->CheckIntegerVariableIsNull(defined);
@@ -351,7 +352,7 @@ void p_int_lin_eq(FlatZincModel* const model, CtSpec* const spec) {
}
Constraint* const ct =
strong_propagation ?
MakeStrongScalProdEquality(solver, variables, coefficients, rhs) :
MakeStrongScalProdEquality(solver, variables, coefficients, rhs) :
(ones == size ?
solver->MakeSumEquality(variables, rhs) :
solver->MakeScalProdEquality(variables, coefficients, rhs));
@@ -562,9 +563,9 @@ void p_int_lin_le_reif(FlatZincModel* const model, CtSpec* const spec) {
coefficients[i] = array_coefficients->a[i]->getInt();
variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
}
IntVar* const var = solver->MakeScalProd(variables, coefficients)->Var();
IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
Constraint* const ct = solver->MakeIsLessOrEqualCstCt(var, rhs, boolvar);
Constraint* const ct = solver->MakeIsLessOrEqualCstCt(expr, rhs, boolvar);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -606,10 +607,10 @@ void p_int_lin_lt_reif(FlatZincModel* const model, CtSpec* const spec) {
coefficients[i] = array_coefficients->a[i]->getInt();
variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
}
IntVar* const var =
solver->MakeScalProd(variables, coefficients)->Var();
IntExpr* const expr =
solver->MakeScalProd(variables, coefficients);
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
Constraint* const ct = solver->MakeIsLessOrEqualCstCt(var, rhs - 1, boolvar);
Constraint* const ct = solver->MakeIsLessCstCt(expr, rhs, boolvar);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -651,9 +652,9 @@ void p_int_lin_ge_reif(FlatZincModel* const model, CtSpec* const spec) {
coefficients[i] = array_coefficients->a[i]->getInt();
variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
}
IntVar* const var = solver->MakeScalProd(variables, coefficients)->Var();
IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
Constraint* const ct = solver->MakeIsGreaterOrEqualCstCt(var, rhs, boolvar);
Constraint* const ct = solver->MakeIsGreaterOrEqualCstCt(expr, rhs, boolvar);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -695,10 +696,9 @@ void p_int_lin_gt_reif(FlatZincModel* const model, CtSpec* const spec) {
coefficients[i] = array_coefficients->a[i]->getInt();
variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
}
IntVar* const var = solver->MakeScalProd(variables, coefficients)->Var();
IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
Constraint* const ct =
solver->MakeIsGreaterOrEqualCstCt(var, rhs + 1, boolvar);
Constraint* const ct = solver->MakeIsGreaterCstCt(expr, rhs, boolvar);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -736,8 +736,7 @@ void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
IntExpr* const target = model->GetIntExpr(spec->Arg(2));
Constraint* const ct =
solver->MakeEquality(solver->MakeSum(left, right)->Var(),
target->Var());
solver->MakeEquality(solver->MakeSum(left, right), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -754,10 +753,9 @@ void p_int_minus(FlatZincModel* const model, CtSpec* const spec) {
model->CheckIntegerVariableIsNull(spec->Arg(2));
model->SetIntegerExpression(spec->Arg(2), target);
} else {
IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
IntExpr* const target = model->GetIntExpr(spec->Arg(2));
Constraint* const ct =
solver->MakeEquality(solver->MakeDifference(left, right)->Var(),
target);
solver->MakeEquality(solver->MakeDifference(left, right), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -774,9 +772,9 @@ void p_int_times(FlatZincModel* const model, CtSpec* const spec) {
model->CheckIntegerVariableIsNull(spec->Arg(2));
model->SetIntegerExpression(spec->Arg(2), target);
} else {
IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
IntExpr* const target = model->GetIntExpr(spec->Arg(2));
Constraint* const ct =
solver->MakeEquality(solver->MakeProd(left, right)->Var(), target);
solver->MakeEquality(solver->MakeProd(left, right), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -785,18 +783,17 @@ void p_int_times(FlatZincModel* const model, CtSpec* const spec) {
void p_int_div(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
IntExpr* const target = model->GetIntExpr(spec->Arg(2));
if (spec->Arg(1)->isIntVar()) {
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct =
solver->MakeEquality(solver->MakeDiv(left, right)->Var(), target);
solver->MakeEquality(solver->MakeDiv(left, right), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
} else {
Constraint* const ct =
solver->MakeEquality(
solver->MakeDiv(left, spec->Arg(1)->getInt())->Var(),
target);
solver->MakeDiv(left, spec->Arg(1)->getInt()), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -830,9 +827,9 @@ void p_int_min(FlatZincModel* const model, CtSpec* const spec) {
model->CheckIntegerVariableIsNull(spec->Arg(2));
model->SetIntegerExpression(spec->Arg(2), target);
} else {
IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
IntExpr* const target = model->GetIntExpr(spec->Arg(2));
Constraint* const ct =
solver->MakeEquality(solver->MakeMin(left, right)->Var(), target);
solver->MakeEquality(solver->MakeMin(left, right), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -849,9 +846,9 @@ void p_int_max(FlatZincModel* const model, CtSpec* const spec) {
model->CheckIntegerVariableIsNull(spec->Arg(2));
model->SetIntegerExpression(spec->Arg(2), target);
} else {
IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
IntExpr* const target = model->GetIntExpr(spec->Arg(2));
Constraint* const ct =
solver->MakeEquality(solver->MakeMax(left, right)->Var(), target);
solver->MakeEquality(solver->MakeMax(left, right), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -860,9 +857,9 @@ void p_int_max(FlatZincModel* const model, CtSpec* const spec) {
void p_int_negate(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
IntExpr* const target = model->GetIntExpr(spec->Arg(2));
Constraint* const ct =
solver->MakeEquality(solver->MakeOpposite(left)->Var(), target);
solver->MakeEquality(solver->MakeOpposite(left), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -883,7 +880,7 @@ void p_array_bool_and(FlatZincModel* const model, CtSpec* const spec) {
}
}
if (spec->IsDefined(node_boolvar)) {
IntVar* const boolvar = solver->MakeMin(variables)->Var();
IntExpr* const boolvar = solver->MakeMin(variables);
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
model->CheckIntegerVariableIsNull(node_boolvar);
@@ -930,8 +927,7 @@ void p_array_bool_or(FlatZincModel* const model, CtSpec* const spec) {
}
} else {
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
Constraint* const ct =
solver->MakeMaxEquality(variables, boolvar);
Constraint* const ct = solver->MakeMaxEquality(variables, boolvar);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -956,9 +952,7 @@ void p_bool_xor(FlatZincModel* const model, CtSpec* const spec) {
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
Constraint* const ct =
solver->MakeIsEqualCstCt(solver->MakeSum(left, right)->Var(),
1,
target);
solver->MakeIsEqualCstCt(solver->MakeSum(left, right), 1, target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -980,9 +974,9 @@ void p_bool_r_imp(FlatZincModel* const model, CtSpec* const spec) {
void p_bool_not(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
IntExpr* const left = model->GetIntExpr(spec->Arg(0));
IntVar* const target = model->GetIntExpr(spec->Arg(1))->Var();
IntExpr* const target = model->GetIntExpr(spec->Arg(1));
Constraint* const ct =
solver->MakeEquality(solver->MakeDifference(1, left)->Var(), target);
solver->MakeEquality(solver->MakeDifference(1, left), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -1118,8 +1112,8 @@ void p_bool2int(FlatZincModel* const model, CtSpec* const spec) {
model->CheckIntegerVariableIsNull(spec->Arg(1));
model->SetIntegerExpression(spec->Arg(1), left);
} else {
IntVar* const right = model->GetIntExpr(spec->Arg(1))->Var();
Constraint* const ct = solver->MakeEquality(left->Var(), right);
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeEquality(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -1135,8 +1129,8 @@ void p_bool2bool(FlatZincModel* const model, CtSpec* const spec) {
model->CheckIntegerVariableIsNull(spec->Arg(1));
model->SetIntegerExpression(spec->Arg(1), left);
} else {
IntVar* const right = model->GetIntExpr(spec->Arg(1))->Var();
Constraint* const ct = solver->MakeEquality(left->Var(), right);
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeEquality(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -1151,8 +1145,8 @@ void p_int2int(FlatZincModel* const model, CtSpec* const spec) {
model->CheckIntegerVariableIsNull(spec->Arg(1));
model->SetIntegerExpression(spec->Arg(1), left);
} else {
IntVar* const right = model->GetIntExpr(spec->Arg(1))->Var();
Constraint* const ct = solver->MakeEquality(left->Var(), right);
IntExpr* const right = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeEquality(left, right);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}
@@ -1190,9 +1184,8 @@ void p_abs(FlatZincModel* const model, CtSpec* const spec) {
<< target->DebugString();
model->SetIntegerExpression(spec->Arg(1), target);
} else {
IntVar* const target = model->GetIntExpr(spec->Arg(1))->Var();
Constraint* const ct =
solver->MakeEquality(solver->MakeAbs(left)->Var(), target);
IntExpr* const target = model->GetIntExpr(spec->Arg(1));
Constraint* const ct = solver->MakeEquality(solver->MakeAbs(left), target);
VLOG(1) << " - posted " << ct->DebugString();
solver->AddConstraint(ct);
}