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

misc improvements

Browse Source
This commit is contained in:
lperron@google.com
2012-06-26 15:40:19 +00:00
parent 59b313d1d0
commit 8a26929d55
9 changed files with 142 additions and 96 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
examples/flatzinc/calvin_puzzle.fzn
View File

@@ -1378,4 +1378,5 @@ constraint set_in(b____00584, {-3, -2, 0, 2, 3});
constraint set_in(b____00613, {-3, -2, 0, 2, 3});
constraint set_in(b____00642, {-3, -2, 0, 2, 3});
constraint set_in(b____00671, {-3, -2, 0, 2, 3});
constraint int_eq(x[1], 1);
solve :: int_search([x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25]], occurrence, indomain_median, complete) satisfy;

2
src/constraint_solver/element.cc
View File

@@ -1266,7 +1266,7 @@ class IntExprArrayElementCstCt : public Constraint {
std::vector<Demon*> demons_;
};
// This constraint implements vars[index] == constant.
// This constraint implements index == position(constant in vars).
class IntExprArrayPositionCt : public Constraint {
public:

2
src/constraint_solver/expr_array.cc
View File

@@ -2388,7 +2388,7 @@ Constraint* MakeScalProdGreaterOrEqualFct(Solver* solver,
for (int i = 0; i < size; ++i) {
terms.push_back(solver->MakeProd(vars[i], coefficients[i])->Var());
}
return solver->MakeGreaterOrEqual(solver->MakeSum(terms), cst);
return solver->MakeSumGreaterOrEqual(terms, cst);
}
} // namespace

6
src/constraint_solver/search.cc
View File

@@ -1287,12 +1287,12 @@ int64 CenterValueSelector::Select(const IntVar* const v, int64 id) {
}
const int64 diameter = vmax - mid; // always greater than mid - vmix.
for (int64 i = 1; i <= diameter; ++i) {
if (v->Contains(mid + i)) {
return mid + i;
}
if (v->Contains(mid - i)) {
return mid - i;
}
if (v->Contains(mid + i)) {
return mid + i;
}
}
return 0LL;
}

20
src/flatzinc/flatzinc.cc
View File

@@ -302,16 +302,16 @@ void FlatZincModel::CreateDecisionBuilders(bool ignore_unknown,
} else {
free_search_ = true;
}
builders_.push_back(solver_.MakePhase(active_variables_,
Solver::CHOOSE_FIRST_UNBOUND,
Solver::ASSIGN_MIN_VALUE));
VLOG(1) << "Decision builder = " << builders_.back()->DebugString();
if (!introduced_variables_.empty()) {
builders_.push_back(solver_.MakePhase(introduced_variables_,
Solver::CHOOSE_FIRST_UNBOUND,
Solver::ASSIGN_MIN_VALUE));
VLOG(1) << "Decision builder = " << builders_.back()->DebugString();
}
// builders_.push_back(solver_.MakePhase(active_variables_,
// Solver::CHOOSE_FIRST_UNBOUND,
// Solver::ASSIGN_MIN_VALUE));
// VLOG(1) << "Decision builder = " << builders_.back()->DebugString();
// if (!introduced_variables_.empty()) {
// builders_.push_back(solver_.MakePhase(introduced_variables_,
// Solver::CHOOSE_FIRST_UNBOUND,
// Solver::ASSIGN_MIN_VALUE));
// VLOG(1) << "Decision builder = " << builders_.back()->DebugString();
// }
}
void FlatZincModel::Satisfy(AST::Array* const annotations) {

113
src/flatzinc/parser.cc
View File

@@ -72,11 +72,7 @@ int ParserState::FindTarget(AST::Node* const annotations) const {
if (ann_array->a[0]->isCall("defines_var")) {
AST::Call* const call = ann_array->a[0]->getCall();
AST::Node* const args = call->args;
if (args->isIntVar()) {
return args->getIntVar();
} else if (args->isBoolVar()) {
return int_variables_.size() + args->getBoolVar();
}
return VarIndex(args);
}
}
}
@@ -97,13 +93,8 @@ void ParserState::CollectRequired(AST::Array* const args,
AST::Node* const node = args->a[i];
if (node->isArray()) {
CollectRequired(node->getArray(), candidates, require);
} else if (node->isIntVar()) {
const int req = node->getIntVar();
if (ContainsKey(candidates, req)) {
require->insert(req);
}
} else if (node->isBoolVar()) {
const int req = node->getBoolVar() + int_variables_.size();
} else if (node->isIntVar() || node->isBoolVar()) {
const int req = VarIndex(node);
if (ContainsKey(candidates, req)) {
require->insert(req);
}
@@ -142,15 +133,16 @@ void ParserState::ComputeViableTarget(
// Defines a bool var.
const int bool_define = FindTarget(spec->annotations());
if (bool_define != CtSpec::kNoDefinition) {
CHECK(bool_variables_[bool_define - int_variables_.size()]->introduced);
CHECK(bool_variables_[BoolFromVarIndex(bool_define)]->introduced);
candidates->insert(bool_define);
VLOG(2) << id << " -> insert " << bool_define;
}
} else if (id == "int2int") {
candidates->insert(spec->Arg(1)->getIntVar());
VLOG(2) << id << " -> insert " << spec->Arg(1)->getIntVar();
const int int_define = VarIndex(spec->Arg(1));
candidates->insert(int_define);
VLOG(2) << id << " -> insert " << int_define;
} else if (id == "bool2bool") {
const int bool_define = spec->Arg(1)->getBoolVar() + int_variables_.size();
const int bool_define = VarIndex(spec->Arg(1));
candidates->insert(bool_define);
VLOG(2) << id << " -> insert " << bool_define;
}
@@ -198,15 +190,28 @@ void MarkComputedVariables(CtSpec* const spec, hash_set<int>* const computed) {
}
}
void ParserState::Sanitize(CtSpec* const spec) {
if (spec->Id() == "int_lin_eq" && StrongPropagation(spec->annotations())) {
VLOG(1) << "## Presolve ## Remove defines part on " << spec->DebugString();
// Remove defines_var part.
spec->RemoveDefines();
}
}
void ParserState::CreateModel() {
hash_set<int> candidates;
hash_set<int> computed_variables;
// Find orphans (is_defined && not a target).
// Sanity.
for (int i = 0; i < constraints_.size(); ++i) {
Sanitize(constraints_[i]);
}
// Find orphans (is_defined && not a viable target).
hash_set<int> targets;
for (int i = 0; i < constraints_.size(); ++i) {
const int target = FindTarget(constraints_[i]->annotations());
if (target != CtSpec::kNoDefinition) {
VLOG(1) << "## Presolve ## Mark xi(" << target << ") as defined";
targets.insert(target);
}
}
@@ -214,6 +219,7 @@ void ParserState::CreateModel() {
IntVarSpec* const spec = int_variables_[i];
if (spec->introduced && !ContainsKey(targets, i)) {
orphans_.insert(i);
VLOG(1) << "## Presolve ## Mark xi(" << i << ") as orphan";
}
}
@@ -226,7 +232,7 @@ void ParserState::CreateModel() {
if (spec->Nullified()) {
continue;
}
if (Propagate(spec)) {
if (Presolve(spec)) {
repeat = true;
}
}
@@ -258,7 +264,7 @@ void ParserState::CreateModel() {
"bool2bool",
args,
NULL);
alias_ct->set_defines(i + int_variables_.size());
alias_ct->set_defines(VarIndex(args->a[1]));
constraints_.push_back(alias_ct);
}
}
@@ -452,13 +458,16 @@ void ParserState::CreateModel() {
for (unsigned int i = int_domain_constraints_.size(); i--;) {
if (!hadError) {
const int var_id = int_domain_constraints_[i].first;
IntVar* const var = model_->IntegerVariable(var_id);
AST::SetLit* const dom = int_domain_constraints_[i].second;
VLOG(1) << "Reduce integer variable " << var_id
<< " to " << dom->DebugString();
if (dom->interval) {
model_->IntegerVariable(var_id)->SetRange(dom->min, dom->max);
} else {
model_->IntegerVariable(var_id)->SetValues(dom->s);
if (dom->interval && (dom->min > var->Min() || dom->max < var->Max())) {
VLOG(1) << "Reduce integer variable " << var_id
<< " to " << dom->DebugString();
var->SetRange(dom->min, dom->max);
} else if (!dom->interval) {
VLOG(1) << "Reduce integer variable " << var_id
<< " to " << dom->DebugString();
var->SetValues(dom->s);
}
}
}
@@ -553,21 +562,11 @@ int ParserState::FindEndIntegerVariable(int index) {
return index;
}
bool ParserState::IsReifTrue(CtSpec* const spec) const {
AST::Node* const node = spec->LastArg();
if (node->isBool() && node->getBool() == 1) {
return true;
}
if (node->isBoolVar()) {
const int boolvar = node->getBoolVar();
return bool_variables_[boolvar]->IsTrue();
}
return false;
}
bool ParserState::IsBound(AST::Node* const node) const {
return node->isInt() ||
(node->isIntVar() && int_variables_[node->getIntVar()]->IsBound());
(node->isIntVar() && int_variables_[node->getIntVar()]->IsBound()) ||
node->isBool() ||
(node->isBoolVar() && bool_variables_[node->getBoolVar()]->IsBound());
}
int ParserState::GetBound(AST::Node* const node) const {
@@ -577,10 +576,16 @@ int ParserState::GetBound(AST::Node* const node) const {
if (node->isIntVar()) {
return int_variables_[node->getIntVar()]->GetBound();
}
if (node->isBool()) {
return node->getBool();
}
if (node->isBoolVar()) {
return bool_variables_[node->getBoolVar()]->GetBound();
}
return 0;
}
bool ParserState::AllDifferent(AST::Node* const node) const {
bool ParserState::IsAllDifferent(AST::Node* const node) const {
AST::Array* const array_variables = node->getArray();
const int size = array_variables->a.size();
std::vector<int> variables(size);
@@ -614,10 +619,10 @@ bool ParserState::AllDifferent(AST::Node* const node) const {
return false;
}
bool ParserState::Propagate(CtSpec* const spec) {
bool ParserState::Presolve(CtSpec* const spec) {
const string& id = spec->Id();
const int index = spec->Index();
if (id == "int_le" || (id == "int_le_reif" && IsReifTrue(spec))) {
if (id == "int_le") {
if (spec->Arg(0)->isIntVar() && IsBound(spec->Arg(1))) {
IntVarSpec* const var_spec =
int_variables_[FindEndIntegerVariable(spec->Arg(0)->getIntVar())];
@@ -642,7 +647,7 @@ bool ParserState::Propagate(CtSpec* const spec) {
return ok;
}
}
if (id == "int_eq" || (id == "int_eq_reif" && IsReifTrue(spec))) {
if (id == "int_eq") {
if (spec->Arg(0)->isIntVar() && IsBound(spec->Arg(1))) {
IntVarSpec* const var_spec =
int_variables_[FindEndIntegerVariable(spec->Arg(0)->getIntVar())];
@@ -668,30 +673,34 @@ bool ParserState::Propagate(CtSpec* const spec) {
} else if (spec->Arg(0)->isIntVar() &&
spec->Arg(1)->isIntVar() &&
spec->annotations() == NULL &&
!ContainsKey(stored_constraints_, index) &&
(ContainsKey(orphans_, spec->Arg(0)->getIntVar()) ||
ContainsKey(orphans_, spec->Arg(1)->getIntVar()))) {
stored_constraints_.insert(index);
const int var0 = spec->Arg(0)->getIntVar();
const int var1 = spec->Arg(1)->getIntVar();
if (ContainsKey(orphans_, var0) && !ContainsKey(orphans_, var1)) {
if (ContainsKey(orphans_, var0)) {
IntVarSpec* const spec0 = int_variables_[FindEndIntegerVariable(var0)];
AST::Call* const call =
new AST::Call("defines_var", new AST::IntVar(var0));
spec->AddAnnotation(call);
VLOG(1) << "## Presolve ## Aliasing xi(" << var0 << ") to xi("
<< var1 << ")";
orphans_.erase(var0);
return true;
} else if (!ContainsKey(orphans_, var0) && ContainsKey(orphans_, var1)) {
} else if (ContainsKey(orphans_, var1)) {
IntVarSpec* const spec1 = int_variables_[FindEndIntegerVariable(var1)];
AST::Call* const call =
new AST::Call("defines_var", new AST::IntVar(var1));
spec->AddAnnotation(call);
VLOG(1) << "## Presolve ## Aliasing xi(" << var1 << ") to xi("
<< var0 << ")";
orphans_.erase(var1);
return true;
}
}
}
if (id == "set_in" || (id == "set_in_reif" && IsReifTrue(spec))) {
if (id == "set_in") {
if (spec->Arg(0)->isIntVar() && spec->Arg(1)->isSet()) {
IntVarSpec* const var_spec =
int_variables_[FindEndIntegerVariable(spec->Arg(0)->getIntVar())];
@@ -710,7 +719,9 @@ bool ParserState::Propagate(CtSpec* const spec) {
return ok;
}
}
if (id == "array_bool_and" && IsReifTrue(spec)) {
if (id == "array_bool_and" &&
IsBound(spec->Arg(1)) &&
GetBound(spec->Arg(1)) == 1) {
VLOG(1) << "## Presolve ## Forcing array_bool_and to 1 on "
<< spec->DebugString();
AST::Array* const array_variables = spec->Arg(0)->getArray();
@@ -724,7 +735,9 @@ bool ParserState::Propagate(CtSpec* const spec) {
spec->Nullify();
return true;
}
if (id.find("_reif") != string::npos && IsReifTrue(spec)) {
if (id.find("_reif") != string::npos &&
IsBound(spec->LastArg()) &&
GetBound(spec->LastArg()) == 1) {
VLOG(1) << "## Presolve ## Unreify " << spec->DebugString();
spec->Unreify();
return true;
@@ -749,7 +762,7 @@ bool ParserState::Propagate(CtSpec* const spec) {
}
if (id == "array_var_int_element" &&
IsBound(spec->Arg(2)) &&
AllDifferent(spec->Arg(1))) {
IsAllDifferent(spec->Arg(1))) {
VLOG(1) << "## Presolve ## Reinforce " << spec->DebugString()
<< " to array_var_int_position";
spec->SetId("array_var_int_position");
@@ -757,10 +770,6 @@ bool ParserState::Propagate(CtSpec* const spec) {
spec->ReplaceArg(2, new AST::IntLit(bound));
return true;
}
if (id == "array_var_int_position" &&
!ContainsKey(stored_constraints_, index)) {
}
return false;
}

20
src/flatzinc/parser.h
View File

@@ -161,16 +161,29 @@ class ParserState {
AST::Node* const annotations);
void InitModel();
void FillOutput(operations_research::FlatZincModel& m);
bool Propagate(CtSpec* const spec);
bool IsReifTrue(CtSpec* const spec) const;
bool Presolve(CtSpec* const spec);
bool IsBound(AST::Node* const node) const;
int GetBound(AST::Node* const node) const;
bool AllDifferent(AST::Node* const node) const;
bool IsAllDifferent(AST::Node* const node) const;
FlatZincModel* model() const {
return model_;
}
int VarIndex(AST::Node* const node) const {
if (node->isIntVar()) {
return node->getIntVar();
} else if (node->isBoolVar()) {
return node->getBoolVar() + int_variables_.size();
} else {
return -1;
}
}
int BoolFromVarIndex(int index) const {
return index - int_variables_.size();
}
private:
int FindEndIntegerVariable(int index);
@@ -182,6 +195,7 @@ class ParserState {
CtSpec* const spec) const;
void ComputeViableTarget(CtSpec* const spec,
hash_set<int>* const candidates) const;
void Sanitize(CtSpec* const spec);
operations_research::FlatZincModel* model_;
std::vector<std::pair<std::string,AST::Node*> > output_;

52
src/flatzinc/registry.cc
View File

@@ -116,14 +116,14 @@ void p_int_eq(FlatZincModel* const model, CtSpec* const spec) {
if (spec->Arg(0)->isIntVar() &&
spec->defines() == spec->Arg(0)->getIntVar()) {
IntVar* const right = model->GetIntVar(spec->Arg(1));
VLOG(1) << " - creating " << spec->Arg(0)->DebugString() << " == "
VLOG(1) << " - creating " << spec->Arg(0)->DebugString() << " := "
<< right->DebugString();
CHECK(model->IntegerVariable(spec->Arg(0)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(0)->getIntVar(), right);
} else if (spec->Arg(1)->isIntVar() &&
spec->defines() == spec->Arg(1)->getIntVar()) {
IntVar* const left = model->GetIntVar(spec->Arg(0));
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " == "
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " := "
<< left->DebugString();
CHECK(model->IntegerVariable(spec->Arg(1)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(1)->getIntVar(), left);
@@ -193,8 +193,8 @@ void p_int_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
node_right->isInt() ?
solver->MakeIsEqualCstVar(left, node_right->getInt()) :
solver->MakeIsEqualVar(left, model->GetIntVar(node_right));
VLOG(1) << " - creating " << node_boolvar->DebugString() << " -> "
<< boolvar->DebugString();;
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
CHECK_NOTNULL(boolvar);
@@ -215,8 +215,8 @@ void p_int_ne_reif(FlatZincModel* const model, CtSpec* const spec) {
if (node_boolvar->isBoolVar() &&
node_boolvar->getBoolVar() + model->IntVarCount() == spec->defines()) {
IntVar* const boolvar = solver->MakeIsDifferentVar(left, right);
VLOG(1) << " - creating " << node_boolvar->DebugString() << " -> "
<< boolvar->DebugString();;
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
CHECK_NOTNULL(boolvar);
@@ -308,7 +308,7 @@ void p_int_lin_eq(FlatZincModel* const model, CtSpec* const spec) {
}
IntVar* const target =
solver->MakeScalProd(variables, coefficients)->Var();
VLOG(1) << " - creating xi(" << spec->defines() << ") -> "
VLOG(1) << " - creating xi(" << spec->defines() << ") := "
<< target->DebugString();
CHECK(model->IntegerVariable(spec->defines()) == NULL);
model->SetIntegerVariable(spec->defines(), target);
@@ -348,8 +348,8 @@ void p_int_lin_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
if (node_boolvar->isBoolVar() &&
node_boolvar->getBoolVar() + model->IntVarCount() == spec->defines()) {
IntVar* const boolvar = solver->MakeIsEqualCstVar(var, rhs);
VLOG(1) << " - creating " << node_boolvar->DebugString() << " -> "
<< boolvar->DebugString();;
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
} else {
@@ -610,7 +610,7 @@ void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
IntVar* const right = model->GetIntVar(spec->Arg(1));
IntVar* const target = model->GetIntVar(spec->Arg(2));
IntVar* const left = solver->MakeDifference(target, right)->Var();
VLOG(1) << " - creating " << spec->Arg(0)->DebugString() << " == "
VLOG(1) << " - creating " << spec->Arg(0)->DebugString() << " := "
<< left->DebugString();
CHECK(model->IntegerVariable(spec->Arg(0)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(0)->getIntVar(), left);
@@ -619,7 +619,7 @@ void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
IntVar* const left = model->GetIntVar(spec->Arg(0));
IntVar* const target = model->GetIntVar(spec->Arg(2));
IntVar* const right = solver->MakeDifference(target, left)->Var();
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " == "
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " := "
<< right->DebugString();
CHECK(model->IntegerVariable(spec->Arg(1)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(1)->getIntVar(), right);
@@ -628,7 +628,7 @@ void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
IntVar* const left = model->GetIntVar(spec->Arg(0));
IntVar* const right = model->GetIntVar(spec->Arg(1));
IntVar* const target = solver->MakeSum(left, right)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " == "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -650,7 +650,7 @@ void p_int_minus(FlatZincModel* const model, CtSpec* const spec) {
if (spec->Arg(2)->isIntVar() &&
spec->defines() == spec->Arg(2)->getIntVar()) {
IntVar* const target = solver->MakeDifference(left, right)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -671,7 +671,7 @@ void p_int_times(FlatZincModel* const model, CtSpec* const spec) {
if (spec->Arg(2)->isIntVar() &&
spec->defines() == spec->Arg(2)->getIntVar()) {
IntVar* const target = solver->MakeProd(left, right)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -728,7 +728,7 @@ void p_int_min(FlatZincModel* const model, CtSpec* const spec) {
if (spec->Arg(2)->isIntVar() &&
spec->defines() == spec->Arg(2)->getIntVar()) {
IntVar* const target = solver->MakeMin(left, right)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -748,7 +748,7 @@ void p_int_max(FlatZincModel* const model, CtSpec* const spec) {
if (spec->Arg(2)->isIntVar() &&
spec->defines() == spec->Arg(2)->getIntVar()) {
IntVar* const target = solver->MakeMax(left, right)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -784,7 +784,7 @@ void p_array_bool_and(FlatZincModel* const model, CtSpec* const spec) {
if (node_boolvar->isBoolVar() &&
node_boolvar->getBoolVar() + model->IntVarCount() == spec->defines()) {
IntVar* const boolvar = solver->MakeMin(variables)->Var();
VLOG(1) << " - creating " << node_boolvar->DebugString() << " -> "
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
@@ -815,7 +815,7 @@ void p_array_bool_or(FlatZincModel* const model, CtSpec* const spec) {
if (node_boolvar->isBoolVar() &&
node_boolvar->getBoolVar() + model->IntVarCount() == spec->defines()) {
IntVar* const boolvar = solver->MakeMax(variables)->Var();
VLOG(1) << " - creating " << node_boolvar->DebugString() << " -> "
VLOG(1) << " - creating " << node_boolvar->DebugString() << " := "
<< boolvar->DebugString();
CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
@@ -904,7 +904,7 @@ void p_array_int_element(FlatZincModel* const model, CtSpec* const spec) {
spec->defines() == spec->Arg(2)->getIntVar()) {
IntVar* const target =
solver->MakeElement(coefficients, shifted_index)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -930,7 +930,7 @@ void p_array_var_int_element(FlatZincModel* const model, CtSpec* const spec) {
if (spec->Arg(2)->isIntVar() &&
spec->defines() == spec->Arg(2)->getIntVar()) {
IntVar* const target = solver->MakeElement(variables, shifted_index)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -975,7 +975,7 @@ void p_array_bool_element(FlatZincModel* const model, CtSpec* const spec) {
spec->defines() == spec->Arg(2)->getBoolVar() + model->IntVarCount()) {
IntVar* const target =
solver->MakeElement(coefficients, shifted_index)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->BooleanVariable(spec->Arg(2)->getBoolVar()) == NULL);
model->SetBooleanVariable(spec->Arg(2)->getBoolVar(), target);
@@ -1001,7 +1001,7 @@ void p_array_var_bool_element(FlatZincModel* const model, CtSpec* const spec) {
if (spec->Arg(2)->isBoolVar() &&
spec->defines() == spec->Arg(2)->getBoolVar() + model->IntVarCount()) {
IntVar* const target = solver->MakeElement(variables, shifted_index)->Var();
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(2)->DebugString() << " := "
<< target->DebugString();
CHECK(model->BooleanVariable(spec->Arg(2)->getBoolVar()) == NULL);
model->SetBooleanVariable(spec->Arg(2)->getBoolVar(), target);
@@ -1022,7 +1022,7 @@ void p_bool2int(FlatZincModel* const model, CtSpec* const spec) {
IntVar* const left = model->GetIntVar(spec->Arg(0));
if (spec->Arg(1)->isIntVar() &&
spec->defines() == spec->Arg(1)->getIntVar()) {
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " := "
<< left->DebugString();
CHECK(model->IntegerVariable(spec->defines()) == NULL);
model->SetIntegerVariable(spec->defines(), left);
@@ -1040,7 +1040,7 @@ void p_bool2bool(FlatZincModel* const model, CtSpec* const spec) {
CHECK_NOTNULL(left);
if (spec->Arg(1)->isBoolVar() &&
spec->defines() == spec->Arg(1)->getBoolVar() + model->IntVarCount()) {
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " := "
<< left->DebugString();
CHECK(model->BooleanVariable(spec->Arg(1)->getBoolVar()) == NULL);
model->SetBooleanVariable(spec->Arg(1)->getBoolVar(), left);
@@ -1057,7 +1057,7 @@ void p_int2int(FlatZincModel* const model, CtSpec* const spec) {
IntVar* const left = model->GetIntVar(spec->Arg(0));
if (spec->Arg(1)->isIntVar() &&
spec->defines() == spec->Arg(1)->getIntVar()) {
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " := "
<< left->DebugString();
CHECK(model->IntegerVariable(spec->defines()) == NULL);
model->SetIntegerVariable(spec->defines(), left);
@@ -1098,7 +1098,7 @@ void p_abs(FlatZincModel* const model, CtSpec* const spec) {
spec->defines() == spec->Arg(1)->getIntVar()) {
CHECK(model->IntegerVariable(spec->defines()) == NULL);
IntVar* const target = solver->MakeAbs(left)->Var();
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " -> "
VLOG(1) << " - creating " << spec->Arg(1)->DebugString() << " := "
<< target->DebugString();
model->SetIntegerVariable(spec->defines(), target);
} else {

22
src/flatzinc/spec.h
View File

@@ -281,6 +281,15 @@ class BoolVarSpec : public VarSpec {
return (assigned && i == false);
}
bool IsBound() const {
return IsTrue() || IsFalse();
}
int GetBound() const {
CHECK(IsBound());
return IsTrue();
}
virtual string DebugString() const {
if (alias) {
return StringPrintf(
@@ -517,6 +526,19 @@ class CtSpec {
}
}
void RemoveDefines() {
if (annotations_ != NULL) {
AST::Array* const ann_array = annotations_->getArray();
if (ann_array->a[0]->isCall("defines_var")) {
delete ann_array->a[0];
for (int i = 0; i < ann_array->a.size() - 1; ++i) {
ann_array->a[i] = ann_array->a[i + 1];
}
ann_array->a.pop_back();
}
}
}
private:
const int index_;
std::string id_;