always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

stable version before submission to challenge

Browse Source
This commit is contained in:
lperron@google.com
2013-08-02 22:21:12 +00:00
parent 0516749029
commit fbca77b812
9 changed files with 266 additions and 65 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
makefiles/Makefile.cpp.mk
View File

@@ -814,6 +814,12 @@ fz: $(BIN_DIR)/fz$E
$(BIN_DIR)/fz$E: $(OBJ_DIR)/fz.$O $(STATIC_FLATZINC_DEPS)
$(CCC) $(CFLAGS) $(OBJ_DIR)/fz.$O $(STATIC_FZ) $(STATIC_FLATZINC_LNK) $(FZ_STATIC) $(STATIC_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sfz$E
ifeq ($(PLATFORM),LINUX)
$(BIN_DIR)/fzn_or_tools: $(OBJ_DIR)/fz.$O $(STATIC_FLATZINC_DEPS)
$(CCC) -static -static-libgcc $(CFLAGS) $(OBJ_DIR)/fz.$O $(STATIC_FZ) $(STATIC_FLATZINC_LNK) $(FZ_STATIC) $(STATIC_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sfzn_or_tools
endif
# Flow and linear assignment cpp
$(OBJ_DIR)/linear_assignment_api.$O:$(EX_DIR)/cpp/linear_assignment_api.cc

6
src/flatzinc/booleans.cc
View File

@@ -661,6 +661,12 @@ bool AddSumBoolArrayGreaterEqVar(SatPropagator* const sat,
return true;
}
bool AddSumBoolArrayLessEqKVar(SatPropagator* const sat,
const std::vector<IntVar*>& vars,
IntExpr* const target) {
return false;
}
bool AddBoolOrEqVar(SatPropagator* const sat, IntExpr* const left,
IntExpr* const right, IntExpr* const target) {
if (!sat->Check(left) || !sat->Check(right) || !sat->Check(target)) {

4
src/flatzinc/flatzinc_constraints.h
View File

@@ -41,6 +41,10 @@ bool AddSumBoolArrayGreaterEqVar(SatPropagator* const sat,
const std::vector<IntVar*>& vars,
IntExpr* const target);
bool AddSumBoolArrayLessEqKVar(SatPropagator* const sat,
const std::vector<IntVar*>& vars,
IntExpr* const target);
bool AddBoolAndEqVar(SatPropagator* const sat, IntExpr* const left,
IntExpr* const right, IntExpr* const target);

6
src/flatzinc/mznlib/count_geq.mzn
View File

@@ -3,11 +3,7 @@
% occurrences of % 'y' in 'x'.
%-----------------------------------------------------------------------------%
include "count_eq.mzn";
predicate count_geq(array[int] of var int: x, var int: y, var int: c) =
let { var 0..length(x) : card }
in count_eq(x, y, card) /\ c >= card;
predicate count_geq(array[int] of var int: x, var int: y, var int: c);
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

6
src/flatzinc/mznlib/count_gt.mzn
View File

@@ -3,11 +3,7 @@
% 'y' in 'x'.
%-----------------------------------------------------------------------------%
include "count_eq.mzn";
predicate count_gt(array[int] of var int: x, var int: y, var int: c) =
let { var 0..length(x) : card }
in count_eq(x, y, card) /\ c > card;
predicate count_gt(array[int] of var int: x, var int: y, var int: c);
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

6
src/flatzinc/mznlib/count_leq.mzn
View File

@@ -3,11 +3,7 @@
% 'y' in 'x'.
%-----------------------------------------------------------------------------%
include "count_eq.mzn";
predicate count_leq(array[int] of var int: x, var int: y, var int: c) =
let { var 0..length(x) : card }
in count_eq(x, y, card) /\ c <= card;
predicate count_leq(array[int] of var int: x, var int: y, var int: c);
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

6
src/flatzinc/mznlib/count_lt.mzn
View File

@@ -2,11 +2,7 @@
% Constrains 'c' to be less than to the number of occurrences of 'y' in 'x'.
%-----------------------------------------------------------------------------%
include "count_eq.mzn";
predicate count_lt(array[int] of var int: x, var int: y, var int: c) =
let { var 0..length(x) : card }
in count_eq(x, y, card) /\ c < card;
predicate count_lt(array[int] of var int: x, var int: y, var int: c);
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

6
src/flatzinc/mznlib/count_neq.mzn
View File

@@ -2,11 +2,7 @@
% Constrains 'c' to be different to the number of occurrences of 'y' in 'x'.
%-----------------------------------------------------------------------------%
include "count_eq.mzn";
predicate count_neq(array[int] of var int: x, var int: y, var int: c) =
let { var 0..length(x) : card }
in count_eq(x, y, card) /\ card != c;
predicate count_neq(array[int] of var int: x, var int: y, var int: c);
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

285
src/flatzinc/registry.cc
View File

@@ -902,7 +902,7 @@ bool PostHiddenOr(FlatZincModel* const model, CtSpec* const spec,
for (int i = 1; i < vars.size(); ++i) {
others[i - 1] = vars[i];
}
return AddBoolOrArrayEqVar(model->Sat(), others, vars[0]);
return AddSumBoolArrayLessEqKVar(model->Sat(), others, vars[0]);
}
bool PostSumGreaterVar(FlatZincModel* const model, CtSpec* const spec,
@@ -2340,13 +2340,13 @@ void p_alldifferent_except_0(FlatZincModel* const model, CtSpec* const spec) {
model->AddConstraint(spec, ct);
}
void p_count(FlatZincModel* const model, CtSpec* const spec) {
void p_count_eq(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
std::vector<IntVar*> tmp_sum;
if (spec->Arg(1)->isInt()) {
const int64 value = spec->Arg(1)->getInt();
std::vector<IntVar*> tmp_sum;
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualCstVar(
model->GetIntExpr(array_variables->a[i]), value);
@@ -2354,27 +2354,25 @@ void p_count(FlatZincModel* const model, CtSpec* const spec) {
tmp_sum.push_back(var);
}
}
if (spec->Arg(2)->isInt()) {
const int64 count = spec->Arg(2)->getInt();
PostBooleanSumInRange(model, spec, tmp_sum, count, count);
} else {
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
Constraint* const ct = solver->MakeSumEquality(tmp_sum, count);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
} else {
IntVar* const value = model->GetIntExpr(spec->Arg(1))->Var();
std::vector<IntVar*> tmp_sum;
for (int i = 0; i < size; ++i) {
tmp_sum.push_back(solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value));
IntVar* const var = solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
if (spec->Arg(2)->isInt()) {
const int64 count = spec->Arg(2)->getInt();
PostBooleanSumInRange(model, spec, tmp_sum, count, count);
}
if (spec->Arg(2)->isInt()) {
const int64 count = spec->Arg(2)->getInt();
PostBooleanSumInRange(model, spec, tmp_sum, count, count);
} else {
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
if (count->Bound()) {
const int64 fcount = count->Min();
PostBooleanSumInRange(model, spec, tmp_sum, fcount, fcount);
} else {
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
Constraint* const ct = solver->MakeSumEquality(tmp_sum, count);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
@@ -2382,14 +2380,13 @@ void p_count(FlatZincModel* const model, CtSpec* const spec) {
}
}
void p_count_reif(FlatZincModel* const model, CtSpec* const spec) {
void p_count_leq(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
AstNode* const node_boolvar = spec->Arg(3);
std::vector<IntVar*> tmp_sum;
if (spec->Arg(1)->isInt()) {
const int64 value = spec->Arg(1)->getInt();
std::vector<IntVar*> tmp_sum;
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualCstVar(
model->GetIntExpr(array_variables->a[i]), value);
@@ -2397,32 +2394,236 @@ void p_count_reif(FlatZincModel* const model, CtSpec* const spec) {
tmp_sum.push_back(var);
}
}
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
if (spec->Arg(2)->isInt()) {
const int64 value = spec->Arg(2)->getInt();
PostIsBooleanSumInRange(model, spec, tmp_sum, value, value, boolvar);
} else {
IntVar* const value = model->GetIntExpr(spec->Arg(1))->Var();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
}
if (spec->Arg(2)->isInt()) {
const int64 count = spec->Arg(2)->getInt();
PostBooleanSumInRange(model, spec, tmp_sum, 0, count);
} else {
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
if (count->Bound()) {
const int64 fcount = count->Min();
PostBooleanSumInRange(model, spec, tmp_sum, 0, fcount);
} else {
Constraint* const ct =
solver->MakeIsEqualCt(solver->MakeSum(tmp_sum),
model->GetIntExpr(spec->Arg(2)), boolvar);
solver->MakeLessOrEqual(solver->MakeSum(tmp_sum), count);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
}
}
void p_count_lt(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
std::vector<IntVar*> tmp_sum;
if (spec->Arg(1)->isInt()) {
const int64 value = spec->Arg(1)->getInt();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualCstVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
} else {
IntVar* const value = model->GetIntExpr(spec->Arg(1))->Var();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
}
if (spec->Arg(2)->isInt()) {
const int64 count = spec->Arg(2)->getInt();
PostBooleanSumInRange(model, spec, tmp_sum, 0, count - 1);
} else {
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
if (count->Bound()) {
const int64 fcount = count->Min();
PostBooleanSumInRange(model, spec, tmp_sum, 0, fcount - 1);
} else {
Constraint* const ct = solver->MakeLess(solver->MakeSum(tmp_sum), count);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
}
}
void p_count_geq(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
std::vector<IntVar*> tmp_sum;
if (spec->Arg(1)->isInt()) {
const int64 value = spec->Arg(1)->getInt();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualCstVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
} else {
IntVar* const value = model->GetIntExpr(spec->Arg(1))->Var();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
}
if (spec->Arg(2)->isInt()) {
const int64 count = spec->Arg(2)->getInt();
PostBooleanSumInRange(model, spec, tmp_sum, count, tmp_sum.size());
} else {
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
if (count->Bound()) {
const int64 fcount = count->Min();
PostBooleanSumInRange(model, spec, tmp_sum, fcount, tmp_sum.size());
} else {
Constraint* const ct =
solver->MakeGreaterOrEqual(solver->MakeSum(tmp_sum), count);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
}
}
void p_count_gt(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
std::vector<IntVar*> tmp_sum;
if (spec->Arg(1)->isInt()) {
const int64 value = spec->Arg(1)->getInt();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualCstVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
} else {
IntVar* const value = model->GetIntExpr(spec->Arg(1))->Var();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
}
if (spec->Arg(2)->isInt()) {
const int64 count = spec->Arg(2)->getInt();
PostBooleanSumInRange(model, spec, tmp_sum, count + 1, tmp_sum.size());
} else {
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
if (count->Bound()) {
const int64 fcount = count->Min();
PostBooleanSumInRange(model, spec, tmp_sum, fcount + 1, tmp_sum.size());
} else {
Constraint* const ct =
solver->MakeGreater(solver->MakeSum(tmp_sum), count);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
}
}
void p_count_neq(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
std::vector<IntVar*> tmp_sum;
if (spec->Arg(1)->isInt()) {
const int64 value = spec->Arg(1)->getInt();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualCstVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
} else {
IntVar* const value = model->GetIntExpr(spec->Arg(1))->Var();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
}
if (spec->Arg(2)->isInt()) {
const int64 count = spec->Arg(2)->getInt();
if (count == 0) {
PostBooleanSumInRange(model, spec, tmp_sum, 1, tmp_sum.size());
} else if (count == tmp_sum.size()) {
PostBooleanSumInRange(model, spec, tmp_sum, 0, tmp_sum.size() - 1);
} else {
Constraint* const ct =
solver->MakeNonEquality(solver->MakeSum(tmp_sum), count);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
} else {
IntVar* const value = model->GetIntExpr(spec->Arg(1))->Var();
std::vector<IntVar*> tmp_sum;
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
Constraint* const ct =
solver->MakeNonEquality(solver->MakeSum(tmp_sum), count);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
}
void p_count_reif(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
std::vector<IntVar*> tmp_sum;
if (spec->Arg(1)->isInt()) {
const int64 value = spec->Arg(1)->getInt();
for (int i = 0; i < size; ++i) {
tmp_sum.push_back(solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value));
IntVar* const var = solver->MakeIsEqualCstVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
if (spec->Arg(2)->isInt()) {
const int64 value = spec->Arg(2)->getInt();
PostIsBooleanSumInRange(model, spec, tmp_sum, value, value, boolvar);
} else {
IntVar* const value = model->GetIntExpr(spec->Arg(1))->Var();
for (int i = 0; i < size; ++i) {
IntVar* const var = solver->MakeIsEqualVar(
model->GetIntExpr(array_variables->a[i]), value);
if (var->Max() == 1) {
tmp_sum.push_back(var);
}
}
}
IntVar* const boolvar = model->GetIntExpr(spec->Arg(3))->Var();
if (spec->Arg(2)->isInt()) {
const int64 fcount = spec->Arg(2)->getInt();
PostIsBooleanSumInRange(model, spec, tmp_sum, fcount, fcount, boolvar);
} else {
IntVar* const count = model->GetIntExpr(spec->Arg(2))->Var();
if (count->Bound()) {
const int64 fcount = count->Min();
PostIsBooleanSumInRange(model, spec, tmp_sum, fcount, fcount, boolvar);
} else {
Constraint* const ct =
solver->MakeIsEqualCt(solver->MakeSum(tmp_sum),
model->GetIntExpr(spec->Arg(2)), boolvar);
solver->MakeIsEqualCt(solver->MakeSum(tmp_sum), count, boolvar);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
@@ -3122,8 +3323,12 @@ class IntBuilder {
global_model_builder.Register("all_different_int", &p_all_different_int);
global_model_builder.Register("alldifferent_except_0",
&p_alldifferent_except_0);
global_model_builder.Register("count", &p_count);
global_model_builder.Register("count_eq", &p_count);
global_model_builder.Register("count_eq", &p_count_eq);
global_model_builder.Register("count_leq", &p_count_leq);
global_model_builder.Register("count_lt", &p_count_lt);
global_model_builder.Register("count_geq", &p_count_geq);
global_model_builder.Register("count_gt", &p_count_gt);
global_model_builder.Register("count_neq", &p_count_neq);
global_model_builder.Register("count_reif", &p_count_reif);
global_model_builder.Register("global_cardinality", &p_global_cardinality);
global_model_builder.Register("global_cardinality_closed",