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

extract array_bool_or, fix obsolete count predicate

Browse Source
This commit is contained in:
laurent.perron@gmail.com
2014-05-02 21:05:16 +00:00
parent 1504206d18
commit 33c62d6027
3 changed files with 59 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
examples/flatzinc/warehouses.fzn
View File

@@ -99,11 +99,11 @@ constraint bool2int(open[2], INT____00076) :: defines_var(INT____00076);
constraint bool2int(open[3], INT____00077) :: defines_var(INT____00077);
constraint bool2int(open[4], INT____00078) :: defines_var(INT____00078);
constraint bool2int(open[5], INT____00079) :: defines_var(INT____00079);
constraint count(supplier, 1, use____00081);
constraint count(supplier, 2, use____00082);
constraint count(supplier, 3, use____00083);
constraint count(supplier, 4, use____00084);
constraint count(supplier, 5, use____00085);
constraint count_eq(supplier, 1, use____00081);
constraint count_eq(supplier, 2, use____00082);
constraint count_eq(supplier, 3, use____00083);
constraint count_eq(supplier, 4, use____00084);
constraint count_eq(supplier, 5, use____00085);
constraint int_eq_reif(1, supplier[1], BOOL____00001) :: defines_var(BOOL____00001);
constraint int_eq_reif(1, supplier[2], BOOL____00002) :: defines_var(BOOL____00002);
constraint int_eq_reif(1, supplier[3], BOOL____00003) :: defines_var(BOOL____00003);

1
src/flatzinc/registry.cc
View File

@@ -3424,6 +3424,7 @@ 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_eq);
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);

55
src/flatzinc2/constraints.cc
View File

@@ -44,7 +44,58 @@ void ExtractArrayBoolAnd(FzSolver* fzsolver, FzConstraint* ct) {
}
void ExtractArrayBoolOr(FzSolver* fzsolver, FzConstraint* ct) {
LOG(FATAL) << "Not implemented: Extract " << ct->DebugString();
Solver* const solver = fzsolver->solver();
const std::vector<FzIntegerVariable*>& vars = ct->Arg(0).variables;
const int size = vars.size();
std::vector<IntVar*> variables;
hash_set<IntExpr*> added;
for (FzIntegerVariable* var : vars) {
IntVar* const to_add = fzsolver->Extract(var)->Var();
if (!ContainsKey(added, to_add) && to_add->Max() != 0) {
variables.push_back(to_add);
added.insert(to_add);
}
}
if (ct->target_variable != nullptr) {
IntVar* const boolvar = solver->MakeMax(variables)->Var();
FZVLOG << " - creating " << ct->target_variable->DebugString()
<< " := " << boolvar->DebugString() << FZENDL;
fzsolver->SetExtracted(ct->target_variable, boolvar);
} else if (ct->Arg(1).HasOneValue() && ct->Arg(1).Value() == 0) {
FZVLOG << " - forcing array_bool_or to 0" << FZENDL;
for (int i = 0; i < variables.size(); ++i) {
variables[i]->SetValue(0);
}
} else {
if (ct->Arg(1).HasOneValue()) {
if (ct->Arg(1).Value() == 1) {
// if (FLAGS_use_sat && AddBoolOrArrayEqualTrue(fzsolver->Sat(), variables)) {
// VLOG(2) << " - posted to sat";
// } else {
Constraint* const constraint =
solver->MakeSumGreaterOrEqual(variables, 1);
FZVLOG << " - posted " << constraint->DebugString() << FZENDL;
solver->AddConstraint(constraint);
// }
} else {
Constraint* const constraint =
solver->MakeSumEquality(variables, Zero());
FZVLOG << " - posted " << constraint->DebugString() << FZENDL;
solver->AddConstraint(constraint);
}
} else {
IntVar* const boolvar = fzsolver->GetExpression(ct->Arg(1))->Var();
// if (FLAGS_use_sat &&
// AddBoolOrArrayEqVar(fzsolver->Sat(), variables, boolvar)) {
// FZVLOG << " - posted to sat" << FZENDL;
// } else {
Constraint* const constraint =
solver->MakeMaxEquality(variables, boolvar);
FZVLOG << " - posted " << constraint->DebugString() << FZENDL;
solver->AddConstraint(constraint);
// }
}
}
}
void ExtractArrayBoolXor(FzSolver* fzsolver, FzConstraint* ct) {
@@ -821,7 +872,7 @@ void FzSolver::ExtractConstraint(FzConstraint* ct) {
ExtractBoolXor(this, ct);
} else if (type == "circuit") {
ExtractCircuit(this, ct);
} else if (type == "count_eq") {
} else if (type == "count_eq" || type == "count") {
ExtractCountEq(this, ct);
} else if (type == "count_geq") {
ExtractCountGeq(this, ct);