diff --git a/makefiles/Makefile.cpp.mk b/makefiles/Makefile.cpp.mk index ed59242744..f50a591298 100644 --- a/makefiles/Makefile.cpp.mk +++ b/makefiles/Makefile.cpp.mk @@ -547,16 +547,17 @@ FLATZINC_LIB_OBJS=\ $(SRC_DIR)/flatzinc/lexer.yy.cc: $(SRC_DIR)/flatzinc/lexer.lxx $(SRC_DIR)/flatzinc/parser.tab.h flex -o$(SRC_DIR)/flatzinc/lexer.yy.cc $(SRC_DIR)/flatzinc/lexer.lxx -$(SRC_DIR)/flatzinc/parser.tab.h $(SRC_DIR)/flatzinc/parser.tab.cc: $(SRC_DIR)/flatzinc/parser.yxx +$(SRC_DIR)/flatzinc/parser.tab.cc: $(SRC_DIR)/flatzinc/parser.yxx bison -t -o $(SRC_DIR)/flatzinc/parser.tab.cc -d $< mv $(SRC_DIR)/flatzinc/parser.tab.hh $(SRC_DIR)/flatzinc/parser.tab.h +$(SRC_DIR)/flatzinc/parser.tab.h: $(SRC_DIR)/flatzinc/parser.tab.cc $(OBJ_DIR)/flatzinc.$O:$(SRC_DIR)/flatzinc/flatzinc.cc $(SRC_DIR)/flatzinc/flatzinc.h $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sflatzinc.cc $(OBJ_OUT)flatzinc.$O $(OBJ_DIR)/lexer.yy.$O:$(SRC_DIR)/flatzinc/lexer.yy.cc $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Slexer.yy.cc $(OBJ_OUT)lexer.yy.$O -$(OBJ_DIR)/parser.tab.$O:$(SRC_DIR)/flatzinc/parser.tab.cc +$(OBJ_DIR)/parser.tab.$O:$(SRC_DIR)/flatzinc/parser.tab.cc $(SRC_DIR)/flatzinc/flatzinc.h $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sparser.tab.cc $(OBJ_OUT)parser.tab.$O $(OBJ_DIR)/registry.$O:$(SRC_DIR)/flatzinc/registry.cc $(SRC_DIR)/flatzinc/registry.h $(SRC_DIR)/flatzinc/flatzinc.h $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sregistry.cc $(OBJ_OUT)registry.$O diff --git a/src/flatzinc/flatzinc.cc b/src/flatzinc/flatzinc.cc index f7799ff710..0c8967cba2 100644 --- a/src/flatzinc/flatzinc.cc +++ b/src/flatzinc/flatzinc.cc @@ -55,7 +55,7 @@ FlatZincModel::FlatZincModel(void) collector_(NULL), objective_(NULL) {} -void FlatZincModel::init(int intVars, int boolVars, int setVars) { +void FlatZincModel::Init(int intVars, int boolVars, int setVars) { int_var_count = 0; integer_variables_ = std::vector(intVars); integer_variables_introduced = std::vector(intVars); @@ -68,7 +68,7 @@ void FlatZincModel::init(int intVars, int boolVars, int setVars) { sv_introduced = std::vector(setVars); } -void FlatZincModel::newIntVar(const std::string& name, IntVarSpec* vs) { +void FlatZincModel::NewIntVar(const std::string& name, IntVarSpec* vs) { if (vs->alias) { integer_variables_[int_var_count++] = integer_variables_[vs->i]; } else { @@ -97,7 +97,7 @@ int FlatZincModel::aliasBool2Int(int iv) { return integer_variables_boolalias[iv]; } -void FlatZincModel::newBoolVar(const std::string& name, BoolVarSpec* vs) { +void FlatZincModel::NewBoolVar(const std::string& name, BoolVarSpec* vs) { if (vs->alias) { boolean_variables_[bool_var_count++] = boolean_variables_[vs->i]; } else { @@ -118,7 +118,7 @@ void FlatZincModel::newSetVar(SetVarSpec* vs) { sv_introduced[set_var_count-1] = vs->introduced; } -void FlatZincModel::postConstraint(const ConExpr& ce, AST::Node* ann) { +void FlatZincModel::PostConstraint(const ConExpr& ce, AST::Node* ann) { try { registry().post(*this, ce, ann); } catch (AST::TypeError& e) { @@ -140,9 +140,9 @@ void flattenAnnotations(AST::Array* ann, std::vector& out) { } } -void FlatZincModel::createBranchers(AST::Node* ann, - bool ignoreUnknown, - std::ostream& err) { +void FlatZincModel::CreateDecisionBuilders(AST::Node* ann, + bool ignoreUnknown, + std::ostream& err) { if (ann) { std::vector flatAnn; if (ann->isArray()) { @@ -212,16 +212,16 @@ void FlatZincModel::createBranchers(AST::Node* ann, } } -AST::Array* FlatZincModel::solveAnnotations(void) const { +AST::Array* FlatZincModel::SolveAnnotations(void) const { return _solveAnnotations; } -void FlatZincModel::solve(AST::Array* ann) { +void FlatZincModel::Solve(AST::Array* ann) { method_ = SAT; _solveAnnotations = ann; } -void FlatZincModel::minimize(int var, AST::Array* ann) { +void FlatZincModel::Minimize(int var, AST::Array* ann) { method_ = MIN; objective_variable_ = var; _solveAnnotations = ann; @@ -239,7 +239,7 @@ void FlatZincModel::minimize(int var, AST::Array* ann) { objective_ = solver_.MakeMinimize(integer_variables_[objective_variable_], 1); } -void FlatZincModel::maximize(int var, AST::Array* ann) { +void FlatZincModel::Maximize(int var, AST::Array* ann) { method_ = MAX; objective_variable_ = var; _solveAnnotations = ann; @@ -261,12 +261,13 @@ FlatZincModel::~FlatZincModel(void) { delete _solveAnnotations; } -void FlatZincModel::run(std::ostream& out, const FzPrinter& p) { +void FlatZincModel::Run(const FzPrinter& p, bool log) { switch (method_) { case MIN: case MAX: { - std::cerr << "start optimization search\n"; - SearchMonitor* const log = solver_.MakeSearchLog(100000, objective_); + SearchMonitor* const log = log ? + solver_.MakeSearchLog(100000, objective_) : + NULL; collector_ = solver_.MakeLastSolutionCollector(); collector_->Add(integer_variables_); collector_->Add(boolean_variables_); @@ -275,7 +276,7 @@ void FlatZincModel::run(std::ostream& out, const FzPrinter& p) { break; } case SAT: { - SearchMonitor* const log = solver_.MakeSearchLog(100000); + SearchMonitor* const log = log ? solver_.MakeSearchLog(100000) : NULL; collector_ = solver_.MakeFirstSolutionCollector(); collector_->Add(integer_variables_); collector_->Add(boolean_variables_); @@ -285,15 +286,15 @@ void FlatZincModel::run(std::ostream& out, const FzPrinter& p) { } } -FlatZincModel::Meth FlatZincModel::method(void) const { +FlatZincModel::Meth FlatZincModel::Method(void) const { return method_; } -int FlatZincModel::optVar(void) const { +int FlatZincModel::optimize_var(void) const { return objective_variable_; } -void FlatZincModel::print(std::ostream& out, const FzPrinter& p) const { +void FlatZincModel::Print(std::ostream& out, const FzPrinter& p) const { p.print(out, *this); } diff --git a/src/flatzinc/flatzinc.h b/src/flatzinc/flatzinc.h index 405b19de7e..648f270058 100644 --- a/src/flatzinc/flatzinc.h +++ b/src/flatzinc/flatzinc.h @@ -126,40 +126,42 @@ class FlatZincModel { ~FlatZincModel(void); /// Initialize space with given number of variables - void init(int intVars, int boolVars, int setVars); + void Init(int num_int_variables, + int num_bool_variables, + int num_set_variables); /// Create new integer variable from specification - void newIntVar(const std::string& name, IntVarSpec* vs); + void NewIntVar(const std::string& name, IntVarSpec* vs); /// Link integer variable \a iv to Boolean variable \a bv void aliasBool2Int(int iv, int bv); /// Return linked Boolean variable for integer variable \a iv int aliasBool2Int(int iv); /// Create new Boolean variable from specification - void newBoolVar(const std::string& name, BoolVarSpec* vs); + void NewBoolVar(const std::string& name, BoolVarSpec* vs); /// Create new set variable from specification void newSetVar(SetVarSpec* vs); /// Post a constraint specified by \a ce - void postConstraint(const ConExpr& ce, AST::Node* annotation); + void PostConstraint(const ConExpr& ce, AST::Node* annotation); /// Post the solve item - void solve(AST::Array* annotation); + void Solve(AST::Array* annotation); /// Post that integer variable \a var should be minimized - void minimize(int var, AST::Array* annotation); + void Minimize(int var, AST::Array* annotation); /// Post that integer variable \a var should be maximized - void maximize(int var, AST::Array* annotation); + void Maximize(int var, AST::Array* annotation); /// Run the search - void run(std::ostream& out, const FzPrinter& p); + void Run(const FzPrinter& p, bool log); /// Produce output on \a out using \a p - void print(std::ostream& out, const FzPrinter& p) const; + void Print(std::ostream& out, const FzPrinter& p) const; /// Return whether to solve a satisfaction or optimization problem - Meth method(void) const; + Meth Method(void) const; /// Return index of variable used for optimization - int optVar(void) const; + int optimize_var(void) const; /** * \brief Create branchers corresponding to the solve item annotations @@ -167,11 +169,12 @@ class FlatZincModel { * If \a ignoreUnknown is true, unknown solve item annotations will be * ignored, otherwise a warning is written to \a err. */ - void createBranchers(AST::Node* ann, bool ignoreUnknown, - std::ostream& err = std::cerr); + void CreateDecisionBuilders(AST::Node* ann, + bool ignoreUnknown, + std::ostream& err = std::cerr); /// Return the solve item annotations - AST::Array* solveAnnotations(void) const; + AST::Array* SolveAnnotations(void) const; }; diff --git a/src/flatzinc/fz.cc b/src/flatzinc/fz.cc index d152e76820..197913fca0 100644 --- a/src/flatzinc/fz.cc +++ b/src/flatzinc/fz.cc @@ -48,6 +48,7 @@ using namespace std; DEFINE_string(file, "", "file name"); +DEFINE_bool(log, false, "Show search log"); namespace operations_research { void Run() { @@ -57,9 +58,11 @@ void Run() { parse(FLAGS_file.c_str(), p)); if (fz_model.get()) { - fz_model->createBranchers(fz_model->solveAnnotations(), false, std::cerr); - fz_model->run(std::cout, p); - fz_model->print(std::cout, p); + fz_model->CreateDecisionBuilders(fz_model->SolveAnnotations(), + false, + std::cerr); + fz_model->Run(p, FLAGS_log); + fz_model->Print(std::cout, p); } else { exit(EXIT_FAILURE); } diff --git a/src/flatzinc/parser.tab.cc b/src/flatzinc/parser.tab.cc index cdceaee227..92df49151a 100644 --- a/src/flatzinc/parser.tab.cc +++ b/src/flatzinc/parser.tab.cc @@ -277,7 +277,7 @@ void addDomainConstraint(ParserState* pp, std::string id, AST::Node* var, void initfg(ParserState* pp) { if (!pp->hadError) - pp->fg->init(pp->intvars.size(), + pp->fg->Init(pp->intvars.size(), pp->boolvars.size(), pp->setvars.size()); @@ -297,7 +297,7 @@ void initfg(ParserState* pp) { array_index = 0; } } - pp->fg->newIntVar(name, + pp->fg->NewIntVar(name, static_cast(pp->intvars[i].second)); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); @@ -324,7 +324,7 @@ void initfg(ParserState* pp) { array_index = 0; } } - pp->fg->newBoolVar(name, + pp->fg->NewBoolVar(name, static_cast(pp->boolvars[i].second)); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); @@ -352,7 +352,7 @@ void initfg(ParserState* pp) { if (!pp->hadError) { try { assert(pp->domainConstraints[i]->args->a.size() == 2); - pp->fg->postConstraint(*pp->domainConstraints[i], NULL); + pp->fg->PostConstraint(*pp->domainConstraints[i], NULL); delete pp->domainConstraints[i]; } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); @@ -2766,7 +2766,7 @@ yyreduce: ParserState *pp = static_cast(parm); if (!pp->hadError) { try { - pp->fg->postConstraint(c, (yyvsp[(6) - (6)].argVec)); + pp->fg->PostConstraint(c, (yyvsp[(6) - (6)].argVec)); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); } @@ -2781,7 +2781,7 @@ yyreduce: ParserState *pp = static_cast(parm); if (!pp->hadError) { try { - pp->fg->solve((yyvsp[(2) - (3)].argVec)); + pp->fg->Solve((yyvsp[(2) - (3)].argVec)); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); } @@ -2798,9 +2798,9 @@ yyreduce: if (!pp->hadError) { try { if ((yyvsp[(3) - (4)].bValue)) - pp->fg->minimize((yyvsp[(4) - (4)].iValue),(yyvsp[(2) - (4)].argVec)); + pp->fg->Minimize((yyvsp[(4) - (4)].iValue),(yyvsp[(2) - (4)].argVec)); else - pp->fg->maximize((yyvsp[(4) - (4)].iValue),(yyvsp[(2) - (4)].argVec)); + pp->fg->Maximize((yyvsp[(4) - (4)].iValue),(yyvsp[(2) - (4)].argVec)); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); } diff --git a/src/flatzinc/parser.yxx b/src/flatzinc/parser.yxx index fee065e477..ef0d69e031 100644 --- a/src/flatzinc/parser.yxx +++ b/src/flatzinc/parser.yxx @@ -149,7 +149,7 @@ void addDomainConstraint(ParserState* pp, std::string id, AST::Node* var, void initfg(ParserState* pp) { if (!pp->hadError) - pp->fg->init(pp->intvars.size(), + pp->fg->Init(pp->intvars.size(), pp->boolvars.size(), pp->setvars.size()); @@ -169,7 +169,7 @@ void initfg(ParserState* pp) { array_index = 0; } } - pp->fg->newIntVar(name, + pp->fg->NewIntVar(name, static_cast(pp->intvars[i].second)); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); @@ -196,7 +196,7 @@ void initfg(ParserState* pp) { array_index = 0; } } - pp->fg->newBoolVar(name, + pp->fg->NewBoolVar(name, static_cast(pp->boolvars[i].second)); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); @@ -224,7 +224,7 @@ void initfg(ParserState* pp) { if (!pp->hadError) { try { assert(pp->domainConstraints[i]->args->a.size() == 2); - pp->fg->postConstraint(*pp->domainConstraints[i], NULL); + pp->fg->PostConstraint(*pp->domainConstraints[i], NULL); delete pp->domainConstraints[i]; } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); @@ -1119,7 +1119,7 @@ constraint_item : ParserState *pp = static_cast(parm); if (!pp->hadError) { try { - pp->fg->postConstraint(c, $6); + pp->fg->PostConstraint(c, $6); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); } @@ -1132,7 +1132,7 @@ solve_item : ParserState *pp = static_cast(parm); if (!pp->hadError) { try { - pp->fg->solve($2); + pp->fg->Solve($2); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); } @@ -1146,9 +1146,9 @@ solve_item : if (!pp->hadError) { try { if ($3) - pp->fg->minimize($4,$2); + pp->fg->Minimize($4,$2); else - pp->fg->maximize($4,$2); + pp->fg->Maximize($4,$2); } catch (operations_research::Error& e) { yyerror(pp, e.toString().c_str()); } diff --git a/src/flatzinc/registry.cc b/src/flatzinc/registry.cc index 272fbd5b2c..a15049e089 100644 --- a/src/flatzinc/registry.cc +++ b/src/flatzinc/registry.cc @@ -903,10 +903,12 @@ void p_int_in(FlatZincModel& s, const ConExpr& ce, AST::Node *ann) { IntVar* const var = s.integer_variables_[var_node->getIntVar()]; AST::SetLit* const domain = domain_node->getSet(); if (domain->interval) { - Constraint* const ct = - solver->MakeBetweenCt(var, domain->min, domain->max); - VLOG(1) << "Posted " << ct->DebugString(); - solver->AddConstraint(ct); + if (var->Min() < domain->min || var->Max() > domain->max) { + Constraint* const ct = + solver->MakeBetweenCt(var, domain->min, domain->max); + VLOG(1) << "Posted " << ct->DebugString(); + solver->AddConstraint(ct); + } } else { Constraint* const ct = solver->MakeMemberCt(var, domain->s); VLOG(1) << "Posted " << ct->DebugString();