move flatzinc -> old_flatzinc; flatzin2 -> flatzinc; start working on doxygen
This commit is contained in:
@@ -22,12 +22,12 @@ DYNAMIC_GRAPH_LIBS = \
|
||||
DYNAMIC_ROUTING_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)routing.$(DYNAMIC_LIB_SUFFIX)
|
||||
|
||||
DYNAMIC_OLD_FLATZINC_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)old_fz.$(DYNAMIC_LIB_SUFFIX)
|
||||
|
||||
DYNAMIC_FLATZINC_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)fz.$(DYNAMIC_LIB_SUFFIX)
|
||||
|
||||
DYNAMIC_FLATZINC2_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)fz2.$(DYNAMIC_LIB_SUFFIX)
|
||||
|
||||
DYNAMIC_DIMACS_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)dimacs.$(DYNAMIC_LIB_SUFFIX)
|
||||
|
||||
@@ -67,10 +67,10 @@ DYNAMIC_ROUTING_DEPS = $(DYNAMIC_ROUTING_LIBS) \
|
||||
$(DYNAMIC_CP_DEPS) \
|
||||
$(DYNAMIC_GRAPH_DEPS)
|
||||
|
||||
DYNAMIC_FLATZINC_DEPS = $(DYNAMIC_FLATZINC_LIBS) \
|
||||
DYNAMIC_OLD_FLATZINC_DEPS = $(DYNAMIC_OLD_FLATZINC_LIBS) \
|
||||
$(DYNAMIC_CP_DEPS)
|
||||
|
||||
DYNAMIC_FLATZINC2_DEPS = $(DYNAMIC_FLATZINC2_LIBS) \
|
||||
DYNAMIC_FLATZINC_DEPS = $(DYNAMIC_FLATZINC_LIBS) \
|
||||
$(DYNAMIC_CP_DEPS)
|
||||
|
||||
DYNAMIC_DIMACS_DEPS = $(DYNAMIC_DIMACS_LIBS) \
|
||||
@@ -121,12 +121,12 @@ DYNAMIC_ROUTING_LNK = \
|
||||
$(DYNAMIC_PRE_LIB)shortestpaths$(DYNAMIC_POST_LIB) \
|
||||
$(DYNAMIC_CP_LNK)
|
||||
|
||||
DYNAMIC_FLATZINC_LNK = \
|
||||
$(DYNAMIC_PRE_LIB)fz$(DYNAMIC_POST_LIB)\
|
||||
DYNAMIC_OLD_FLATZINC_LNK = \
|
||||
$(DYNAMIC_PRE_LIB)old_fz$(DYNAMIC_POST_LIB)\
|
||||
$(DYNAMIC_CP_LNK)
|
||||
|
||||
DYNAMIC_FLATZINC2_LNK = \
|
||||
$(DYNAMIC_PRE_LIB)fz2$(DYNAMIC_POST_LIB)\
|
||||
DYNAMIC_FLATZINC_LNK = \
|
||||
$(DYNAMIC_PRE_LIB)fz$(DYNAMIC_POST_LIB)\
|
||||
$(DYNAMIC_CP_LNK)
|
||||
|
||||
DYNAMIC_DIMACS_LNK = \
|
||||
@@ -171,12 +171,12 @@ STATIC_GRAPH_LIBS = \
|
||||
STATIC_ROUTING_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)routing.$(STATIC_LIB_SUFFIX)
|
||||
|
||||
STATIC_OLD_FLATZINC_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)old_fz.$(STATIC_LIB_SUFFIX)
|
||||
|
||||
STATIC_FLATZINC_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)fz.$(STATIC_LIB_SUFFIX)
|
||||
|
||||
STATIC_FLATZINC2_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)fz2.$(STATIC_LIB_SUFFIX)
|
||||
|
||||
STATIC_SAT_LIBS = \
|
||||
$(LIB_DIR)/$(LIBPREFIX)sat.$(STATIC_LIB_SUFFIX)
|
||||
|
||||
@@ -206,11 +206,11 @@ STATIC_ROUTING_DEPS = $(STATIC_ROUTING_LIBS) \
|
||||
$(STATIC_CP_DEPS) \
|
||||
$(STATIC_GRAPH_DEPS)
|
||||
|
||||
STATIC_FLATZINC_DEPS = $(STATIC_FLATZINC_LIBS) \
|
||||
STATIC_OLD_FLATZINC_DEPS = $(STATIC_OLD_FLATZINC_LIBS) \
|
||||
$(STATIC_BASE_DEPS) \
|
||||
$(STATIC_CP_DEPS)
|
||||
|
||||
STATIC_FLATZINC2_DEPS = $(STATIC_FLATZINC2_LIBS) \
|
||||
STATIC_FLATZINC_DEPS = $(STATIC_FLATZINC_LIBS) \
|
||||
$(STATIC_BASE_DEPS) \
|
||||
$(STATIC_CP_DEPS)
|
||||
|
||||
@@ -257,12 +257,12 @@ STATIC_ROUTING_LNK = \
|
||||
$(STATIC_PRE_LIB)shortestpaths$(STATIC_POST_LIB) \
|
||||
$(STATIC_CP_LNK)
|
||||
|
||||
STATIC_FLATZINC_LNK = \
|
||||
$(STATIC_PRE_LIB)fz$(STATIC_POST_LIB)\
|
||||
STATIC_OLD_FLATZINC_LNK = \
|
||||
$(STATIC_PRE_LIB)old_fz$(STATIC_POST_LIB)\
|
||||
$(STATIC_CP_LNK)
|
||||
|
||||
STATIC_FLATZINC2_LNK = \
|
||||
$(STATIC_PRE_LIB)fz2$(STATIC_POST_LIB)\
|
||||
STATIC_FLATZINC_LNK = \
|
||||
$(STATIC_PRE_LIB)fz$(STATIC_POST_LIB)\
|
||||
$(STATIC_CP_LNK)
|
||||
|
||||
# TODO(lperron): update to include FZ.
|
||||
@@ -324,6 +324,7 @@ clean_cc:
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)routing.$(DYNAMIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)algorithms.$(DYNAMIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)dimacs.$(DYNAMIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)old_fz.$(DYNAMIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)fz.$(DYNAMIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)sat.$(DYNAMIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)shortestpaths.$(DYNAMIC_LIB_SUFFIX)
|
||||
@@ -336,13 +337,14 @@ clean_cc:
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)routing.$(STATIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)algorithms.$(STATIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)shortestpaths.$(STATIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)old_fz.$(STATIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)fz.$(STATIC_LIB_SUFFIX)
|
||||
-$(DEL) $(LIB_DIR)$S$(LIBPREFIX)sat.$(STATIC_LIB_SUFFIX)
|
||||
-$(DEL) $(OBJ_DIR)$S*.$O
|
||||
-$(DEL) $(OBJ_DIR)$Salgorithms$S*.$O
|
||||
-$(DEL) $(OBJ_DIR)$Sbase$S*.$O
|
||||
-$(DEL) $(OBJ_DIR)$Sold_flatzinc$S*.$O
|
||||
-$(DEL) $(OBJ_DIR)$Sflatzinc$S*.$O
|
||||
-$(DEL) $(OBJ_DIR)$Sflatzinc2$S*.$O
|
||||
-$(DEL) $(OBJ_DIR)$Sglop$S*.$O
|
||||
-$(DEL) $(OBJ_DIR)$Sgraph$S*.$O
|
||||
-$(DEL) $(OBJ_DIR)$Ssat$S*.$O
|
||||
@@ -356,13 +358,13 @@ clean_cc:
|
||||
-$(DEL) $(GEN_DIR)$Sconstraint_solver$S*.pb.*
|
||||
-$(DEL) $(GEN_DIR)$Slinear_solver$S*.pb.*
|
||||
-$(DEL) $(GEN_DIR)$Sglop$S*.pb.*
|
||||
-$(DEL) $(GEN_DIR)$Sflatzinc$Sflatzinc*
|
||||
-$(DEL) $(GEN_DIR)$Sflatzinc2$Sparser*
|
||||
-$(DEL) $(GEN_DIR)$Sold_flatzinc$Sflatzinc*
|
||||
-$(DEL) $(GEN_DIR)$Sflatzinc$Sparser*
|
||||
-$(DEL) $(GEN_DIR)$Ssat$S*.pb.*
|
||||
-$(DEL) $(BIN_DIR)$S*.exp
|
||||
-$(DEL) $(BIN_DIR)$S*.lib
|
||||
-$(DEL) $(SRC_DIR)$Sflatzinc$Slexer*
|
||||
-$(DEL) $(SRC_DIR)$Sflatzinc$Sparser.tab.*
|
||||
-$(DEL) $(SRC_DIR)$Sold_flatzinc$Slexer*
|
||||
-$(DEL) $(SRC_DIR)$Sold_flatzinc$Sparser.tab.*
|
||||
|
||||
clean_compat:
|
||||
-$(DELREC) $(OR_ROOT)constraint_solver
|
||||
@@ -1062,58 +1064,58 @@ $(OBJ_DIR)/fap_utilities.$O:$(EX_DIR)/cpp/fap_utilities.cc
|
||||
$(LIB_DIR)/$(LIBPREFIX)fap.$(DYNAMIC_LIB_SUFFIX): $(FAP_LIB_OBJS)
|
||||
$(DYNAMIC_LINK_CMD) $(DYNAMIC_LINK_PREFIX)$(LIB_DIR)$S$(LIBPREFIX)fap.$(DYNAMIC_LIB_SUFFIX) $(FAP_LIB_OBJS)
|
||||
|
||||
# Flatzinc Support
|
||||
# old Flatzinc Support
|
||||
|
||||
FLATZINC_LIB_OBJS=\
|
||||
$(OBJ_DIR)/flatzinc/booleans.$O\
|
||||
$(OBJ_DIR)/flatzinc/flatzinc.$O\
|
||||
$(OBJ_DIR)/flatzinc/flatzinc_constraints.$O\
|
||||
$(OBJ_DIR)/flatzinc/fz_search.$O\
|
||||
$(OBJ_DIR)/flatzinc/flatzinc.yy.$O\
|
||||
$(OBJ_DIR)/flatzinc/flatzinc.tab.$O\
|
||||
$(OBJ_DIR)/flatzinc/parser.$O\
|
||||
$(OBJ_DIR)/flatzinc/registry.$O
|
||||
OLD_FLATZINC_LIB_OBJS=\
|
||||
$(OBJ_DIR)/old_flatzinc/booleans.$O\
|
||||
$(OBJ_DIR)/old_flatzinc/flatzinc.$O\
|
||||
$(OBJ_DIR)/old_flatzinc/flatzinc_constraints.$O\
|
||||
$(OBJ_DIR)/old_flatzinc/fz_search.$O\
|
||||
$(OBJ_DIR)/old_flatzinc/flatzinc.yy.$O\
|
||||
$(OBJ_DIR)/old_flatzinc/flatzinc.tab.$O\
|
||||
$(OBJ_DIR)/old_flatzinc/parser.$O\
|
||||
$(OBJ_DIR)/old_flatzinc/registry.$O
|
||||
|
||||
$(GEN_DIR)/flatzinc/flatzinc.yy.cc: $(SRC_DIR)/flatzinc/flatzinc.lex $(FLEX)
|
||||
$(FLEX) -o$(GEN_DIR)/flatzinc/flatzinc.yy.cc $(SRC_DIR)/flatzinc/flatzinc.lex
|
||||
$(GEN_DIR)/old_flatzinc/flatzinc.yy.cc: $(SRC_DIR)/old_flatzinc/flatzinc.lex $(FLEX)
|
||||
$(FLEX) -o$(GEN_DIR)/old_flatzinc/flatzinc.yy.cc $(SRC_DIR)/old_flatzinc/flatzinc.lex
|
||||
|
||||
$(GEN_DIR)/flatzinc/flatzinc.tab.cc: $(SRC_DIR)/flatzinc/flatzinc.yy $(BISON)
|
||||
$(BISON) -t -o $(GEN_DIR)/flatzinc/flatzinc.tab.cc -d $<
|
||||
$(GEN_DIR)/old_flatzinc/flatzinc.tab.cc: $(SRC_DIR)/old_flatzinc/flatzinc.yy $(BISON)
|
||||
$(BISON) -t -o $(GEN_DIR)/old_flatzinc/flatzinc.tab.cc -d $<
|
||||
|
||||
$(GEN_DIR)/flatzinc/flatzinc.tab.hh: $(GEN_DIR)/flatzinc/flatzinc.tab.cc
|
||||
$(GEN_DIR)/old_flatzinc/flatzinc.tab.hh: $(GEN_DIR)/old_flatzinc/flatzinc.tab.cc
|
||||
|
||||
$(OBJ_DIR)/flatzinc/booleans.$O:$(SRC_DIR)/flatzinc/booleans.cc $(SRC_DIR)/flatzinc/flatzinc.h $(SRC_DIR)/flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sbooleans.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sbooleans.$O
|
||||
$(OBJ_DIR)/flatzinc/flatzinc.$O:$(SRC_DIR)/flatzinc/flatzinc.cc $(SRC_DIR)/flatzinc/flatzinc.h $(SRC_DIR)/flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sflatzinc.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sflatzinc.$O
|
||||
$(OBJ_DIR)/flatzinc/flatzinc_constraints.$O:$(SRC_DIR)/flatzinc/flatzinc_constraints.cc $(SRC_DIR)/flatzinc/flatzinc.h $(SRC_DIR)/flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sflatzinc_constraints.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sflatzinc_constraints.$O
|
||||
$(OBJ_DIR)/flatzinc/fz_search.$O:$(SRC_DIR)/flatzinc/fz_search.cc $(SRC_DIR)/flatzinc/flatzinc.h $(SRC_DIR)/flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sfz_search.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sfz_search.$O
|
||||
$(OBJ_DIR)/flatzinc/flatzinc.yy.$O:$(GEN_DIR)/flatzinc/flatzinc.yy.cc $(GEN_DIR)/flatzinc/flatzinc.tab.hh $(SRC_DIR)/flatzinc/parser.h $(SRC_DIR)/flatzinc/flatzinc.h
|
||||
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sflatzinc$Sflatzinc.yy.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sflatzinc.yy.$O
|
||||
$(OBJ_DIR)/flatzinc/parser.$O:$(SRC_DIR)/flatzinc/parser.cc $(SRC_DIR)/flatzinc/flatzinc.h $(SRC_DIR)/flatzinc/parser.h $(GEN_DIR)/flatzinc/flatzinc.tab.hh
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sparser.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sparser.$O
|
||||
$(OBJ_DIR)/flatzinc/flatzinc.tab.$O:$(GEN_DIR)/flatzinc/flatzinc.tab.cc $(SRC_DIR)/flatzinc/flatzinc.h
|
||||
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sflatzinc$Sflatzinc.tab.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sflatzinc.tab.$O
|
||||
$(OBJ_DIR)/flatzinc/registry.$O:$(SRC_DIR)/flatzinc/registry.cc $(SRC_DIR)/flatzinc/flatzinc.h $(SRC_DIR)/flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sregistry.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sregistry.$O
|
||||
$(OBJ_DIR)/old_flatzinc/booleans.$O:$(SRC_DIR)/old_flatzinc/booleans.cc $(SRC_DIR)/old_flatzinc/flatzinc.h $(SRC_DIR)/old_flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sold_flatzinc$Sbooleans.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sbooleans.$O
|
||||
$(OBJ_DIR)/old_flatzinc/flatzinc.$O:$(SRC_DIR)/old_flatzinc/flatzinc.cc $(SRC_DIR)/old_flatzinc/flatzinc.h $(SRC_DIR)/old_flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sold_flatzinc$Sflatzinc.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sflatzinc.$O
|
||||
$(OBJ_DIR)/old_flatzinc/flatzinc_constraints.$O:$(SRC_DIR)/old_flatzinc/flatzinc_constraints.cc $(SRC_DIR)/old_flatzinc/flatzinc.h $(SRC_DIR)/old_flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sold_flatzinc$Sflatzinc_constraints.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sflatzinc_constraints.$O
|
||||
$(OBJ_DIR)/old_flatzinc/fz_search.$O:$(SRC_DIR)/old_flatzinc/fz_search.cc $(SRC_DIR)/old_flatzinc/flatzinc.h $(SRC_DIR)/old_flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sold_flatzinc$Sfz_search.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sfz_search.$O
|
||||
$(OBJ_DIR)/old_flatzinc/flatzinc.yy.$O:$(GEN_DIR)/old_flatzinc/flatzinc.yy.cc $(GEN_DIR)/old_flatzinc/flatzinc.tab.hh $(SRC_DIR)/old_flatzinc/parser.h $(SRC_DIR)/old_flatzinc/flatzinc.h
|
||||
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sold_flatzinc$Sflatzinc.yy.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sflatzinc.yy.$O
|
||||
$(OBJ_DIR)/old_flatzinc/parser.$O:$(SRC_DIR)/old_flatzinc/parser.cc $(SRC_DIR)/old_flatzinc/flatzinc.h $(SRC_DIR)/old_flatzinc/parser.h $(GEN_DIR)/old_flatzinc/flatzinc.tab.hh
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sold_flatzinc$Sparser.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sparser.$O
|
||||
$(OBJ_DIR)/old_flatzinc/flatzinc.tab.$O:$(GEN_DIR)/old_flatzinc/flatzinc.tab.cc $(SRC_DIR)/old_flatzinc/flatzinc.h
|
||||
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sold_flatzinc$Sflatzinc.tab.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sflatzinc.tab.$O
|
||||
$(OBJ_DIR)/old_flatzinc/registry.$O:$(SRC_DIR)/old_flatzinc/registry.cc $(SRC_DIR)/old_flatzinc/flatzinc.h $(SRC_DIR)/old_flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sold_flatzinc$Sregistry.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sregistry.$O
|
||||
|
||||
$(LIB_DIR)/$(LIBPREFIX)fz.$(DYNAMIC_LIB_SUFFIX): $(FLATZINC_LIB_OBJS)
|
||||
$(DYNAMIC_LINK_CMD) $(DYNAMIC_LINK_PREFIX)$(LIB_DIR)$S$(LIBPREFIX)fz.$(DYNAMIC_LIB_SUFFIX) $(FLATZINC_LIB_OBJS)
|
||||
$(LIB_DIR)/$(LIBPREFIX)old_fz.$(DYNAMIC_LIB_SUFFIX): $(OLD_FLATZINC_LIB_OBJS)
|
||||
$(DYNAMIC_LINK_CMD) $(DYNAMIC_LINK_PREFIX)$(LIB_DIR)$S$(LIBPREFIX)old_fz.$(DYNAMIC_LIB_SUFFIX) $(OLD_FLATZINC_LIB_OBJS)
|
||||
|
||||
ifneq ($(SYSTEM),win)
|
||||
$(LIB_DIR)/$(LIBPREFIX)fz.$(STATIC_LIB_SUFFIX): $(FLATZINC_LIB_OBJS)
|
||||
$(STATIC_LINK_CMD) $(STATIC_LINK_PREFIX)$(LIB_DIR)$S$(LIBPREFIX)fz.$(STATIC_LIB_SUFFIX) $(FLATZINC_LIB_OBJS)
|
||||
$(LIB_DIR)/$(LIBPREFIX)old_fz.$(STATIC_LIB_SUFFIX): $(OLD_FLATZINC_LIB_OBJS)
|
||||
$(STATIC_LINK_CMD) $(STATIC_LINK_PREFIX)$(LIB_DIR)$S$(LIBPREFIX)old_fz.$(STATIC_LIB_SUFFIX) $(OLD_FLATZINC_LIB_OBJS)
|
||||
endif
|
||||
|
||||
$(OBJ_DIR)/flatzinc/fz.$O:$(SRC_DIR)/flatzinc/fz.cc $(SRC_DIR)/flatzinc/flatzinc.h $(SRC_DIR)/flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sfz.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sfz.$O
|
||||
$(OBJ_DIR)/old_flatzinc/fz.$O:$(SRC_DIR)/old_flatzinc/fz.cc $(SRC_DIR)/old_flatzinc/flatzinc.h $(SRC_DIR)/old_flatzinc/parser.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sold_flatzinc$Sfz.cc $(OBJ_OUT)$(OBJ_DIR)$Sold_flatzinc$Sfz.$O
|
||||
|
||||
fz: $(BIN_DIR)/fz$E
|
||||
old_fz: $(BIN_DIR)/old_fz$E
|
||||
|
||||
$(BIN_DIR)/fz$E: $(OBJ_DIR)/flatzinc/fz.$O $(STATIC_FLATZINC_DEPS)
|
||||
$(CCC) $(CFLAGS) $(OBJ_DIR)/flatzinc/fz.$O $(STATIC_FZ) $(STATIC_FLATZINC_LNK) $(STATIC_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sfz$E
|
||||
$(BIN_DIR)/old_fz$E: $(OBJ_DIR)/old_flatzinc/fz.$O $(STATIC_OLD_FLATZINC_DEPS)
|
||||
$(CCC) $(CFLAGS) $(OBJ_DIR)/old_flatzinc/fz.$O $(STATIC_FZ) $(STATIC_OLD_FLATZINC_LNK) $(STATIC_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sold_fz$E
|
||||
|
||||
# Static archive for minizinc challenge
|
||||
|
||||
@@ -1122,82 +1124,82 @@ $(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
|
||||
|
||||
# Flatzinc2 experimental code
|
||||
# Flatzinc experimental code
|
||||
|
||||
FLATZINC2_LIB_OBJS=\
|
||||
$(OBJ_DIR)/flatzinc2/constraints.$O\
|
||||
$(OBJ_DIR)/flatzinc2/flatzinc_constraints.$O\
|
||||
$(OBJ_DIR)/flatzinc2/model.$O\
|
||||
$(OBJ_DIR)/flatzinc2/parallel_support.$O\
|
||||
$(OBJ_DIR)/flatzinc2/parser.$O\
|
||||
$(OBJ_DIR)/flatzinc2/parser.tab.$O\
|
||||
$(OBJ_DIR)/flatzinc2/parser.yy.$O\
|
||||
$(OBJ_DIR)/flatzinc2/presolve.$O\
|
||||
$(OBJ_DIR)/flatzinc2/sat_constraint.$O\
|
||||
$(OBJ_DIR)/flatzinc2/search.$O\
|
||||
$(OBJ_DIR)/flatzinc2/sequential_support.$O\
|
||||
$(OBJ_DIR)/flatzinc2/solver.$O
|
||||
FLATZINC_LIB_OBJS=\
|
||||
$(OBJ_DIR)/flatzinc/constraints.$O\
|
||||
$(OBJ_DIR)/flatzinc/flatzinc_constraints.$O\
|
||||
$(OBJ_DIR)/flatzinc/model.$O\
|
||||
$(OBJ_DIR)/flatzinc/parallel_support.$O\
|
||||
$(OBJ_DIR)/flatzinc/parser.$O\
|
||||
$(OBJ_DIR)/flatzinc/parser.tab.$O\
|
||||
$(OBJ_DIR)/flatzinc/parser.yy.$O\
|
||||
$(OBJ_DIR)/flatzinc/presolve.$O\
|
||||
$(OBJ_DIR)/flatzinc/sat_constraint.$O\
|
||||
$(OBJ_DIR)/flatzinc/search.$O\
|
||||
$(OBJ_DIR)/flatzinc/sequential_support.$O\
|
||||
$(OBJ_DIR)/flatzinc/solver.$O
|
||||
|
||||
$(GEN_DIR)/flatzinc2/parser.yy.cc: $(SRC_DIR)/flatzinc2/parser.lex $(FLEX)
|
||||
$(FLEX) -o$(GEN_DIR)/flatzinc2/parser.yy.cc $(SRC_DIR)/flatzinc2/parser.lex
|
||||
$(GEN_DIR)/flatzinc/parser.yy.cc: $(SRC_DIR)/flatzinc/parser.lex $(FLEX)
|
||||
$(FLEX) -o$(GEN_DIR)/flatzinc/parser.yy.cc $(SRC_DIR)/flatzinc/parser.lex
|
||||
|
||||
$(GEN_DIR)/flatzinc2/parser.tab.cc: $(SRC_DIR)/flatzinc2/parser.yy $(BISON)
|
||||
$(BISON) -t -o $(GEN_DIR)/flatzinc2/parser.tab.cc -d $<
|
||||
$(GEN_DIR)/flatzinc/parser.tab.cc: $(SRC_DIR)/flatzinc/parser.yy $(BISON)
|
||||
$(BISON) -t -o $(GEN_DIR)/flatzinc/parser.tab.cc -d $<
|
||||
|
||||
$(GEN_DIR)/flatzinc2/parser.tab.hh: $(GEN_DIR)/flatzinc2/parser.tab.cc
|
||||
$(GEN_DIR)/flatzinc/parser.tab.hh: $(GEN_DIR)/flatzinc/parser.tab.cc
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/constraints.$O:$(SRC_DIR)/flatzinc2/constraints.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Sconstraints.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Sconstraints.$O
|
||||
$(OBJ_DIR)/flatzinc/constraints.$O:$(SRC_DIR)/flatzinc/constraints.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sconstraints.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sconstraints.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/flatzinc_constraints.$O:$(SRC_DIR)/flatzinc2/flatzinc_constraints.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Sflatzinc_constraints.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Sflatzinc_constraints.$O
|
||||
$(OBJ_DIR)/flatzinc/flatzinc_constraints.$O:$(SRC_DIR)/flatzinc/flatzinc_constraints.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sflatzinc_constraints.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sflatzinc_constraints.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/model.$O:$(SRC_DIR)/flatzinc2/model.cc $(SRC_DIR)/flatzinc2/model.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Smodel.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Smodel.$O
|
||||
$(OBJ_DIR)/flatzinc/model.$O:$(SRC_DIR)/flatzinc/model.cc $(SRC_DIR)/flatzinc/model.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Smodel.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Smodel.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/parallel_support.$O:$(SRC_DIR)/flatzinc2/parallel_support.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Sparallel_support.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Sparallel_support.$O
|
||||
$(OBJ_DIR)/flatzinc/parallel_support.$O:$(SRC_DIR)/flatzinc/parallel_support.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sparallel_support.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sparallel_support.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/parser.$O:$(SRC_DIR)/flatzinc2/parser.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/parser.h $(GEN_DIR)/flatzinc2/parser.tab.hh
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Sparser.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Sparser.$O
|
||||
$(OBJ_DIR)/flatzinc/parser.$O:$(SRC_DIR)/flatzinc/parser.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/parser.h $(GEN_DIR)/flatzinc/parser.tab.hh
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sparser.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sparser.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/parser.tab.$O:$(GEN_DIR)/flatzinc2/parser.tab.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/parser.h $(GEN_DIR)/flatzinc2/parser.tab.hh
|
||||
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sflatzinc2$Sparser.tab.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Sparser.tab.$O
|
||||
$(OBJ_DIR)/flatzinc/parser.tab.$O:$(GEN_DIR)/flatzinc/parser.tab.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/parser.h $(GEN_DIR)/flatzinc/parser.tab.hh
|
||||
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sflatzinc$Sparser.tab.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sparser.tab.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/parser.yy.$O:$(GEN_DIR)/flatzinc2/parser.yy.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/parser.h $(GEN_DIR)/flatzinc2/parser.tab.hh
|
||||
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sflatzinc2$Sparser.yy.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Sparser.yy.$O
|
||||
$(OBJ_DIR)/flatzinc/parser.yy.$O:$(GEN_DIR)/flatzinc/parser.yy.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/parser.h $(GEN_DIR)/flatzinc/parser.tab.hh
|
||||
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sflatzinc$Sparser.yy.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sparser.yy.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/presolve.$O:$(SRC_DIR)/flatzinc2/presolve.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/presolve.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Spresolve.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Spresolve.$O
|
||||
$(OBJ_DIR)/flatzinc/presolve.$O:$(SRC_DIR)/flatzinc/presolve.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/presolve.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Spresolve.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Spresolve.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/sat_constraint.$O:$(SRC_DIR)/flatzinc2/sat_constraint.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h $(GEN_DIR)/sat/sat_parameters.pb.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Ssat_constraint.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Ssat_constraint.$O
|
||||
$(OBJ_DIR)/flatzinc/sat_constraint.$O:$(SRC_DIR)/flatzinc/sat_constraint.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h $(GEN_DIR)/sat/sat_parameters.pb.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Ssat_constraint.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Ssat_constraint.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/search.$O:$(SRC_DIR)/flatzinc2/search.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Ssearch.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Ssearch.$O
|
||||
$(OBJ_DIR)/flatzinc/search.$O:$(SRC_DIR)/flatzinc/search.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Ssearch.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Ssearch.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/sequential_support.$O:$(SRC_DIR)/flatzinc2/sequential_support.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Ssequential_support.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Ssequential_support.$O
|
||||
$(OBJ_DIR)/flatzinc/sequential_support.$O:$(SRC_DIR)/flatzinc/sequential_support.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Ssequential_support.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Ssequential_support.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/solver.$O:$(SRC_DIR)/flatzinc2/solver.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Ssolver.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Ssolver.$O
|
||||
$(OBJ_DIR)/flatzinc/solver.$O:$(SRC_DIR)/flatzinc/solver.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Ssolver.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Ssolver.$O
|
||||
|
||||
$(LIB_DIR)/$(LIBPREFIX)fz2.$(STATIC_LIB_SUFFIX): $(FLATZINC2_LIB_OBJS)
|
||||
$(STATIC_LINK_CMD) $(STATIC_LINK_PREFIX)$(LIB_DIR)$S$(LIBPREFIX)fz2.$(STATIC_LIB_SUFFIX) $(FLATZINC2_LIB_OBJS)
|
||||
$(LIB_DIR)/$(LIBPREFIX)fz.$(STATIC_LIB_SUFFIX): $(FLATZINC_LIB_OBJS)
|
||||
$(STATIC_LINK_CMD) $(STATIC_LINK_PREFIX)$(LIB_DIR)$S$(LIBPREFIX)fz.$(STATIC_LIB_SUFFIX) $(FLATZINC_LIB_OBJS)
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/fz.$O:$(SRC_DIR)/flatzinc2/fz.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Sfz.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Sfz.$O
|
||||
$(OBJ_DIR)/flatzinc/fz.$O:$(SRC_DIR)/flatzinc/fz.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sfz.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sfz.$O
|
||||
|
||||
$(OBJ_DIR)/flatzinc2/parser_main.$O:$(SRC_DIR)/flatzinc2/parser_main.cc $(SRC_DIR)/flatzinc2/model.h $(SRC_DIR)/flatzinc2/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc2$Sparser_main.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc2$Sparser_main.$O
|
||||
$(OBJ_DIR)/flatzinc/parser_main.$O:$(SRC_DIR)/flatzinc/parser_main.cc $(SRC_DIR)/flatzinc/model.h $(SRC_DIR)/flatzinc/solver.h
|
||||
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sflatzinc$Sparser_main.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Sparser_main.$O
|
||||
|
||||
fz2 : $(BIN_DIR)/fz2$E $(BIN_DIR)/parser_main$E
|
||||
fz : $(BIN_DIR)/fz$E $(BIN_DIR)/parser_main$E
|
||||
|
||||
$(BIN_DIR)/fz2$E: $(OBJ_DIR)/flatzinc2/fz.$O $(STATIC_FLATZINC2_DEPS)
|
||||
$(CCC) $(CFLAGS) $(OBJ_DIR)$Sflatzinc2$Sfz.$O $(STATIC_FZ) $(STATIC_FLATZINC2_LNK) $(STATIC_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sfz2$E
|
||||
$(BIN_DIR)/fz$E: $(OBJ_DIR)/flatzinc/fz.$O $(STATIC_FLATZINC_DEPS)
|
||||
$(CCC) $(CFLAGS) $(OBJ_DIR)$Sflatzinc$Sfz.$O $(STATIC_FZ) $(STATIC_FLATZINC_LNK) $(STATIC_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sfz$E
|
||||
|
||||
$(BIN_DIR)/parser_main$E: $(OBJ_DIR)/flatzinc2/parser_main.$O $(STATIC_FLATZINC2_DEPS)
|
||||
$(CCC) $(CFLAGS) $(OBJ_DIR)$Sflatzinc2$Sparser_main.$O $(STATIC_FZ) $(STATIC_FLATZINC2_LNK) $(STATIC_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sparser_main$E
|
||||
$(BIN_DIR)/parser_main$E: $(OBJ_DIR)/flatzinc/parser_main.$O $(STATIC_FLATZINC_DEPS)
|
||||
$(CCC) $(CFLAGS) $(OBJ_DIR)$Sflatzinc$Sparser_main.$O $(STATIC_FZ) $(STATIC_FLATZINC_LNK) $(STATIC_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sparser_main$E
|
||||
|
||||
# Flow and linear assignment cpp
|
||||
|
||||
|
||||
@@ -5,6 +5,24 @@ ifeq ($(PLATFORM), MACOSX)
|
||||
DOXYGEN = /Applications/Doxygen.app/Contents/Resources/doxygen
|
||||
endif
|
||||
|
||||
clean_refman:
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Sbase
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Sutil
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Sgraph
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Salgorithms
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Slp_data
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Sglop
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Slinear_solver
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Sconstraint_solver
|
||||
-$(DELREC) $(OR_ROOT)documentation$Sgenerated$Sor-tools$Sfz
|
||||
|
||||
refman:
|
||||
cd documentations/doxygen
|
||||
$(DOXYGEN) or-tools.doxy
|
||||
$(DOXYGEN) tools/base.doxy
|
||||
$(DOXYGEN) tools/util.doxy
|
||||
$(DOXYGEN) tools/graph.doxy
|
||||
$(DOXYGEN) tools/algorithms.doxy
|
||||
$(DOXYGEN) tools/lp_data.doxy
|
||||
$(DOXYGEN) tools/glop.doxy
|
||||
$(DOXYGEN) tools/linear_solver.doxy
|
||||
$(DOXYGEN) tools/constraint_solver.doxy
|
||||
$(DOXYGEN) tools/fz.doxy
|
||||
|
||||
@@ -14,11 +14,11 @@
|
||||
#include "base/integral_types.h"
|
||||
#include "base/logging.h"
|
||||
#include "base/hash.h"
|
||||
#include "flatzinc2/flatzinc_constraints.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/sat_constraint.h"
|
||||
#include "flatzinc2/search.h"
|
||||
#include "flatzinc2/solver.h"
|
||||
#include "flatzinc/flatzinc_constraints.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/sat_constraint.h"
|
||||
#include "flatzinc/search.h"
|
||||
#include "flatzinc/solver.h"
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
#include "constraint_solver/constraint_solveri.h"
|
||||
|
||||
@@ -10,17 +10,18 @@
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
|
||||
#include "flatzinc/flatzinc_constraints.h"
|
||||
|
||||
#include "base/commandlineflags.h"
|
||||
#include "flatzinc/flatzinc.h"
|
||||
#include "constraint_solver/constraint_solveri.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/sat_constraint.h"
|
||||
#include "util/string_array.h"
|
||||
|
||||
DECLARE_bool(cp_trace_search);
|
||||
DECLARE_bool(cp_trace_propagation);
|
||||
DECLARE_bool(use_sat);
|
||||
DECLARE_bool(fz_verbose);
|
||||
|
||||
namespace operations_research {
|
||||
namespace {
|
||||
@@ -121,6 +122,47 @@ class BooleanSumOdd : public Constraint {
|
||||
NumericalRev<int> num_always_true_vars_;
|
||||
};
|
||||
|
||||
class BoundModulo : public Constraint {
|
||||
public:
|
||||
BoundModulo(Solver* const s, IntVar* x, IntVar* const m, int64 r)
|
||||
: Constraint(s), var_(x), mod_(m), residual_(r) {}
|
||||
|
||||
virtual ~BoundModulo() {}
|
||||
|
||||
virtual void Post() {
|
||||
Demon* const d = solver()->MakeConstraintInitialPropagateCallback(this);
|
||||
var_->WhenRange(d);
|
||||
mod_->WhenBound(d);
|
||||
}
|
||||
|
||||
virtual void InitialPropagate() {
|
||||
if (mod_->Bound()) {
|
||||
const int64 d = std::abs(mod_->Min());
|
||||
if (d == 0) {
|
||||
solver()->Fail();
|
||||
} else {
|
||||
const int64 emin = var_->Min();
|
||||
const int64 emax = var_->Max();
|
||||
const int64 new_min = PosIntDivUp(emin - residual_, d) * d + residual_;
|
||||
const int64 new_max =
|
||||
PosIntDivDown(emax - residual_, d) * d + residual_;
|
||||
var_->SetRange(new_min, new_max);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("(%s %% %s == %" GG_LL_FORMAT "d)",
|
||||
var_->DebugString().c_str(),
|
||||
mod_->DebugString().c_str(), residual_);
|
||||
}
|
||||
|
||||
private:
|
||||
IntVar* const var_;
|
||||
IntVar* const mod_;
|
||||
const int64 residual_;
|
||||
};
|
||||
|
||||
class VariableParity : public Constraint {
|
||||
public:
|
||||
VariableParity(Solver* const s, IntVar* const var, bool odd)
|
||||
@@ -207,7 +249,6 @@ class IsBooleanSumInRange : public Constraint {
|
||||
virtual void InitialPropagate() {
|
||||
int num_always_true = 0;
|
||||
int num_possible_true = 0;
|
||||
int possible_true_index = -1;
|
||||
for (int i = 0; i < vars_.size(); ++i) {
|
||||
const IntVar* const var = vars_[i];
|
||||
if (var->Min() == 1) {
|
||||
@@ -215,7 +256,6 @@ class IsBooleanSumInRange : public Constraint {
|
||||
num_possible_true++;
|
||||
} else if (var->Max() == 1) {
|
||||
num_possible_true++;
|
||||
possible_true_index = i;
|
||||
}
|
||||
}
|
||||
num_possible_true_vars_.SetValue(solver(), num_possible_true);
|
||||
@@ -264,10 +304,10 @@ class IsBooleanSumInRange : public Constraint {
|
||||
}
|
||||
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("Sum([%s]) in [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT
|
||||
"d] == %s",
|
||||
JoinDebugStringPtr(vars_, ", ").c_str(), range_min_,
|
||||
range_max_, target_->DebugString().c_str());
|
||||
return StringPrintf(
|
||||
"Sum([%s]) in [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d] == %s",
|
||||
JoinDebugStringPtr(vars_, ", ").c_str(), range_min_, range_max_,
|
||||
target_->DebugString().c_str());
|
||||
}
|
||||
|
||||
virtual void Accept(ModelVisitor* const visitor) const {
|
||||
@@ -420,360 +460,185 @@ class BooleanSumInRange : public Constraint {
|
||||
NumericalRev<int> num_always_true_vars_;
|
||||
};
|
||||
|
||||
// ----- Inverse constraint -----
|
||||
// ----- Variable duration interval var -----
|
||||
|
||||
// This constraints maintains: left[i] == j <=> right_[j] == i.
|
||||
// It assumes array are 0 based.
|
||||
class Inverse : public Constraint {
|
||||
class StartVarDurationVarPerformedIntervalVar : public IntervalVar {
|
||||
public:
|
||||
Inverse(Solver* const s, const std::vector<IntVar*>& left,
|
||||
const std::vector<IntVar*>& right)
|
||||
: Constraint(s),
|
||||
left_(left),
|
||||
right_(right),
|
||||
left_holes_(left.size()),
|
||||
left_iterators_(left_.size()),
|
||||
right_holes_(right_.size()),
|
||||
right_iterators_(right_.size()) {
|
||||
CHECK_EQ(left_.size(), right_.size());
|
||||
for (int i = 0; i < left_.size(); ++i) {
|
||||
left_holes_[i] = left_[i]->MakeHoleIterator(true);
|
||||
left_iterators_[i] = left_[i]->MakeDomainIterator(true);
|
||||
right_holes_[i] = right_[i]->MakeHoleIterator(true);
|
||||
right_iterators_[i] = right_[i]->MakeDomainIterator(true);
|
||||
}
|
||||
StartVarDurationVarPerformedIntervalVar(Solver* const s,
|
||||
IntVar* const start,
|
||||
IntVar* const duration,
|
||||
const std::string& name);
|
||||
virtual ~StartVarDurationVarPerformedIntervalVar() {}
|
||||
|
||||
virtual int64 StartMin() const;
|
||||
virtual int64 StartMax() const;
|
||||
virtual void SetStartMin(int64 m);
|
||||
virtual void SetStartMax(int64 m);
|
||||
virtual void SetStartRange(int64 mi, int64 ma);
|
||||
virtual int64 OldStartMin() const { return start_->OldMin(); }
|
||||
virtual int64 OldStartMax() const { return start_->OldMax(); }
|
||||
virtual void WhenStartRange(Demon* const d) { start_->WhenRange(d); }
|
||||
virtual void WhenStartBound(Demon* const d) { start_->WhenBound(d); }
|
||||
|
||||
virtual int64 DurationMin() const;
|
||||
virtual int64 DurationMax() const;
|
||||
virtual void SetDurationMin(int64 m);
|
||||
virtual void SetDurationMax(int64 m);
|
||||
virtual void SetDurationRange(int64 mi, int64 ma);
|
||||
virtual int64 OldDurationMin() const { return duration_->Min(); }
|
||||
virtual int64 OldDurationMax() const { return duration_->Max(); }
|
||||
virtual void WhenDurationRange(Demon* const d) { duration_->WhenRange(d); }
|
||||
virtual void WhenDurationBound(Demon* const d) { duration_->WhenBound(d); }
|
||||
|
||||
virtual int64 EndMin() const;
|
||||
virtual int64 EndMax() const;
|
||||
virtual void SetEndMin(int64 m);
|
||||
virtual void SetEndMax(int64 m);
|
||||
virtual void SetEndRange(int64 mi, int64 ma);
|
||||
virtual int64 OldEndMin() const {
|
||||
return start_->OldMin() + duration_->OldMin();
|
||||
}
|
||||
virtual int64 OldEndMax() const {
|
||||
return start_->OldMax() + duration_->OldMax();
|
||||
}
|
||||
virtual void WhenEndRange(Demon* const d) {
|
||||
start_->WhenRange(d);
|
||||
duration_->WhenRange(d);
|
||||
}
|
||||
virtual void WhenEndBound(Demon* const d) {
|
||||
start_->WhenBound(d);
|
||||
duration_->WhenBound(d);
|
||||
}
|
||||
|
||||
virtual ~Inverse() {}
|
||||
virtual bool MustBePerformed() const;
|
||||
virtual bool MayBePerformed() const;
|
||||
virtual void SetPerformed(bool val);
|
||||
virtual bool WasPerformedBound() const { return true; }
|
||||
virtual void WhenPerformedBound(Demon* const d) {}
|
||||
virtual std::string DebugString() const;
|
||||
|
||||
virtual void Post() {
|
||||
for (int i = 0; i < left_.size(); ++i) {
|
||||
Demon* const left_demon = MakeConstraintDemon2(
|
||||
solver(), this, &Inverse::Propagate, "Propagate", i, true);
|
||||
left_[i]->WhenDomain(left_demon);
|
||||
Demon* const right_demon = MakeConstraintDemon2(
|
||||
solver(), this, &Inverse::Propagate, "Propagate", i, false);
|
||||
right_[i]->WhenDomain(right_demon);
|
||||
}
|
||||
solver()->AddConstraint(solver()->MakeAllDifferent(left_, false));
|
||||
solver()->AddConstraint(solver()->MakeAllDifferent(right_, false));
|
||||
virtual IntExpr* StartExpr() { return start_; }
|
||||
virtual IntExpr* DurationExpr() { return duration_; }
|
||||
virtual IntExpr* EndExpr() {
|
||||
return solver()->MakeSum(start_, duration_);
|
||||
}
|
||||
|
||||
virtual void InitialPropagate() {
|
||||
const int size = left_.size();
|
||||
for (int i = 0; i < size; ++i) {
|
||||
left_[i]->SetRange(0, size - 1);
|
||||
right_[i]->SetRange(0, size - 1);
|
||||
}
|
||||
for (int i = 0; i < size; ++i) {
|
||||
PropagateDomain(i, left_[i], left_iterators_[i], right_, &remove_left_);
|
||||
PropagateDomain(i, right_[i], right_iterators_[i], left_, &remove_right_);
|
||||
}
|
||||
virtual IntExpr* PerformedExpr() { return solver()->MakeIntConst(1); }
|
||||
virtual IntExpr* SafeStartExpr(int64 unperformed_value) {
|
||||
return StartExpr();
|
||||
}
|
||||
|
||||
void Propagate(int index, bool left_to_right) {
|
||||
if (left_to_right) {
|
||||
PropagateHoles(index, left_[index], left_holes_[index], right_);
|
||||
} else {
|
||||
PropagateHoles(index, right_[index], right_holes_[index], left_);
|
||||
}
|
||||
}
|
||||
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("Inverse([%s], [%s])",
|
||||
JoinDebugStringPtr(left_, ", ").c_str(),
|
||||
JoinDebugStringPtr(right_, ", ").c_str());
|
||||
virtual IntExpr* SafeDurationExpr(int64 unperformed_value) {
|
||||
return DurationExpr();
|
||||
}
|
||||
virtual IntExpr* SafeEndExpr(int64 unperformed_value) { return EndExpr(); }
|
||||
|
||||
virtual void Accept(ModelVisitor* const visitor) const {
|
||||
visitor->BeginVisitConstraint("Inverse", this);
|
||||
visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kLeftArgument,
|
||||
left_);
|
||||
visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kRightArgument,
|
||||
right_);
|
||||
visitor->EndVisitConstraint("Inverse", this);
|
||||
}
|
||||
|
||||
private:
|
||||
void PropagateHoles(int index, IntVar* const var, IntVarIterator* const holes,
|
||||
const std::vector<IntVar*>& inverse) {
|
||||
const int64 oldmax =
|
||||
std::min(var->OldMax(), static_cast<int64>(left_.size() - 1));
|
||||
const int64 vmin = var->Min();
|
||||
const int64 vmax = var->Max();
|
||||
for (int64 value = std::max(var->OldMin(), 0LL); value < vmin; ++value) {
|
||||
inverse[value]->RemoveValue(index);
|
||||
}
|
||||
for (holes->Init(); holes->Ok(); holes->Next()) {
|
||||
inverse[holes->Value()]->RemoveValue(index);
|
||||
}
|
||||
for (int64 value = vmax + 1; value <= oldmax; ++value) {
|
||||
inverse[value]->RemoveValue(index);
|
||||
}
|
||||
}
|
||||
|
||||
void PropagateDomain(int index, IntVar* const var,
|
||||
IntVarIterator* const domain,
|
||||
const std::vector<IntVar*>& inverse,
|
||||
std::vector<int64>* const remove) {
|
||||
remove->clear();
|
||||
for (domain->Init(); domain->Ok(); domain->Next()) {
|
||||
const int64 value = domain->Value();
|
||||
if (!inverse[value]->Contains(index)) {
|
||||
remove->push_back(value);
|
||||
}
|
||||
}
|
||||
if (!remove->empty()) {
|
||||
var->RemoveValues(*remove);
|
||||
}
|
||||
}
|
||||
|
||||
std::vector<IntVar*> left_;
|
||||
std::vector<IntVar*> right_;
|
||||
std::vector<IntVarIterator*> left_holes_;
|
||||
std::vector<IntVarIterator*> left_iterators_;
|
||||
std::vector<IntVarIterator*> right_holes_;
|
||||
std::vector<IntVarIterator*> right_iterators_;
|
||||
std::vector<int64> remove_left_;
|
||||
std::vector<int64> remove_right_;
|
||||
};
|
||||
|
||||
// Variable demand cumulative time table
|
||||
|
||||
class VariableCumulativeTask : public BaseObject {
|
||||
public:
|
||||
VariableCumulativeTask(IntVar* const start, IntVar* const duration,
|
||||
IntVar* const demand)
|
||||
: start_(start), duration_(duration), demand_(demand) {}
|
||||
// Copy constructor. Cannot be explicit, because we want to pass instances of
|
||||
// VariableCumulativeTask by copy.
|
||||
VariableCumulativeTask(const VariableCumulativeTask& task)
|
||||
: start_(task.start_), duration_(task.duration_), demand_(task.demand_) {}
|
||||
|
||||
IntVar* start() const { return start_; }
|
||||
IntVar* duration() const { return duration_; }
|
||||
IntVar* demand() const { return demand_; }
|
||||
int64 StartMin() const { return start_->Min(); }
|
||||
int64 StartMax() const { return start_->Max(); }
|
||||
int64 EndMin() const { return start_->Min() + duration_->Min(); }
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("Task{ start: %s, duration: %s, demand: %s }",
|
||||
start_->DebugString().c_str(),
|
||||
duration_->DebugString().c_str(),
|
||||
demand_->DebugString().c_str());
|
||||
visitor->VisitIntervalVariable(this, "", 0, nullptr);
|
||||
}
|
||||
|
||||
private:
|
||||
IntVar* const start_;
|
||||
IntVar* const duration_;
|
||||
IntVar* const demand_;
|
||||
};
|
||||
|
||||
struct ProfileDelta {
|
||||
ProfileDelta(int64 _time, int64 _delta) : time(_time), delta(_delta) {}
|
||||
int64 time;
|
||||
int64 delta;
|
||||
};
|
||||
// TODO(user): Take care of overflows.
|
||||
StartVarDurationVarPerformedIntervalVar::
|
||||
StartVarDurationVarPerformedIntervalVar(Solver* const s,
|
||||
IntVar* const var,
|
||||
IntVar* const duration,
|
||||
const std::string& name)
|
||||
: IntervalVar(s, name), start_(var), duration_(duration) {}
|
||||
|
||||
bool TimeLessThan(const ProfileDelta& delta1, const ProfileDelta& delta2) {
|
||||
return delta1.time < delta2.time;
|
||||
int64 StartVarDurationVarPerformedIntervalVar::StartMin() const {
|
||||
return start_->Min();
|
||||
}
|
||||
|
||||
bool TaskStartMinLessThan(const VariableCumulativeTask* const task1,
|
||||
const VariableCumulativeTask* const task2) {
|
||||
return (task1->StartMin() < task2->StartMin());
|
||||
int64 StartVarDurationVarPerformedIntervalVar::StartMax() const {
|
||||
return start_->Max();
|
||||
}
|
||||
|
||||
class VariableCumulativeTimeTable : public Constraint {
|
||||
public:
|
||||
VariableCumulativeTimeTable(Solver* const solver,
|
||||
const std::vector<VariableCumulativeTask*>& tasks,
|
||||
IntVar* const capacity)
|
||||
: Constraint(solver), by_start_min_(tasks), capacity_(capacity) {
|
||||
// There may be up to 2 delta's per interval (one on each side),
|
||||
// plus two sentinels
|
||||
const int profile_max_size = 2 * NumTasks() + 2;
|
||||
profile_non_unique_time_.reserve(profile_max_size);
|
||||
profile_unique_time_.reserve(profile_max_size);
|
||||
void StartVarDurationVarPerformedIntervalVar::SetStartMin(int64 m) {
|
||||
start_->SetMin(m);
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetStartMax(int64 m) {
|
||||
start_->SetMax(m);
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetStartRange(int64 mi, int64 ma) {
|
||||
start_->SetRange(mi, ma);
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::DurationMin() const {
|
||||
return duration_->Min();
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::DurationMax() const {
|
||||
return duration_->Max();
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetDurationMin(int64 m) {
|
||||
duration_->SetMin(m);
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetDurationMax(int64 m) {
|
||||
duration_->SetMax(m);
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetDurationRange(
|
||||
int64 mi, int64 ma) {
|
||||
duration_->SetRange(mi, ma);
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::EndMin() const {
|
||||
return start_->Min() + duration_->Min();
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::EndMax() const {
|
||||
return start_->Max() + duration_->Max();
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetEndMin(int64 m) {
|
||||
start_->SetMin(m - duration_->Max());
|
||||
duration_->SetMin(m - start_->Max());
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetEndMax(int64 m) {
|
||||
start_->SetMax(m - duration_->Min());
|
||||
duration_->SetMax(m - start_->Min());
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetEndRange(int64 mi, int64 ma) {
|
||||
start_->SetRange(mi - duration_->Max(), ma - duration_->Min());
|
||||
duration_->SetRange(mi - start_->Max(), ma - start_->Min());
|
||||
}
|
||||
|
||||
bool StartVarDurationVarPerformedIntervalVar::MustBePerformed() const {
|
||||
return true;
|
||||
}
|
||||
|
||||
bool StartVarDurationVarPerformedIntervalVar::MayBePerformed() const {
|
||||
return true;
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetPerformed(bool val) {
|
||||
if (!val) {
|
||||
solver()->Fail();
|
||||
}
|
||||
}
|
||||
|
||||
virtual void InitialPropagate() {
|
||||
BuildProfile();
|
||||
PushTasks();
|
||||
std::string StartVarDurationVarPerformedIntervalVar::DebugString() const {
|
||||
std::string out;
|
||||
const std::string& var_name = name();
|
||||
if (!var_name.empty()) {
|
||||
out = var_name + "(start = ";
|
||||
} else {
|
||||
out = "IntervalVar(start = ";
|
||||
}
|
||||
|
||||
virtual void Post() {
|
||||
Demon* const demon =
|
||||
solver()->MakeDelayedConstraintInitialPropagateCallback(this);
|
||||
for (int i = 0; i < NumTasks(); ++i) {
|
||||
by_start_min_[i]->start()->WhenRange(demon);
|
||||
by_start_min_[i]->duration()->WhenRange(demon);
|
||||
by_start_min_[i]->demand()->WhenRange(demon);
|
||||
}
|
||||
capacity_->WhenRange(demon);
|
||||
}
|
||||
|
||||
int NumTasks() const { return by_start_min_.size(); }
|
||||
|
||||
void Accept(ModelVisitor* const visitor) const {
|
||||
LOG(FATAL) << "Should not be visited";
|
||||
}
|
||||
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("VariableCumulativeTimeTable([%s], capacity = %s)",
|
||||
JoinDebugStringPtr(by_start_min_, ", ").c_str(),
|
||||
capacity_->DebugString().c_str());
|
||||
}
|
||||
|
||||
private:
|
||||
// Build the usage profile. Runs in O(n log n).
|
||||
void BuildProfile() {
|
||||
// Build profile with non unique time
|
||||
profile_non_unique_time_.clear();
|
||||
for (int i = 0; i < NumTasks(); ++i) {
|
||||
const VariableCumulativeTask* task = by_start_min_[i];
|
||||
const int64 start_max = task->StartMax();
|
||||
const int64 end_min = task->EndMin();
|
||||
const int64 demand_min = task->demand()->Min();
|
||||
if (start_max < end_min && demand_min > 0) {
|
||||
profile_non_unique_time_.push_back(
|
||||
ProfileDelta(start_max, +demand_min));
|
||||
profile_non_unique_time_.push_back(ProfileDelta(end_min, -demand_min));
|
||||
}
|
||||
}
|
||||
// Sort
|
||||
std::sort(profile_non_unique_time_.begin(), profile_non_unique_time_.end(),
|
||||
TimeLessThan);
|
||||
// Build profile with unique times
|
||||
profile_unique_time_.clear();
|
||||
profile_unique_time_.push_back(ProfileDelta(kint64min, 0));
|
||||
for (int i = 0; i < profile_non_unique_time_.size(); ++i) {
|
||||
const ProfileDelta& profile_delta = profile_non_unique_time_[i];
|
||||
if (profile_delta.time == profile_unique_time_.back().time) {
|
||||
profile_unique_time_.back().delta += profile_delta.delta;
|
||||
} else {
|
||||
profile_unique_time_.push_back(profile_delta);
|
||||
}
|
||||
}
|
||||
// Re-scan profile to compute min usage, max usage, and check
|
||||
// final usage to be 0.
|
||||
int64 usage = 0;
|
||||
int64 max_required_usage = 0;
|
||||
const int64 max_capacity = capacity_->Max();
|
||||
for (int i = 0; i < profile_unique_time_.size(); ++i) {
|
||||
const ProfileDelta& profile_delta = profile_unique_time_[i];
|
||||
usage += profile_delta.delta;
|
||||
max_required_usage = std::max(max_required_usage, usage);
|
||||
if (usage > max_capacity) {
|
||||
solver()->Fail();
|
||||
}
|
||||
}
|
||||
DCHECK_EQ(0, usage);
|
||||
profile_unique_time_.push_back(ProfileDelta(kint64max, 0));
|
||||
|
||||
// Propagate on capacity.
|
||||
capacity_->SetMin(max_required_usage);
|
||||
}
|
||||
|
||||
// Update the start min for all tasks. Runs in O(n^2) and Omega(n).
|
||||
void PushTasks() {
|
||||
std::sort(by_start_min_.begin(), by_start_min_.end(), TaskStartMinLessThan);
|
||||
int64 usage = 0;
|
||||
int profile_index = 0;
|
||||
for (int task_index = 0; task_index < NumTasks(); ++task_index) {
|
||||
VariableCumulativeTask* const task = by_start_min_[task_index];
|
||||
if (task->duration()->Min() > 0) {
|
||||
while (task->StartMin() > profile_unique_time_[profile_index].time) {
|
||||
DCHECK(profile_index < profile_unique_time_.size());
|
||||
++profile_index;
|
||||
usage += profile_unique_time_[profile_index].delta;
|
||||
}
|
||||
PushTask(task, profile_index, usage);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Push the given task to new_start_min, defined as the smallest integer such
|
||||
// that the profile usage for all tasks, excluding the current one, does not
|
||||
// exceed capacity_ - task->demand()->Min() on the interval
|
||||
// [new_start_min, new_start_min + task->interval()->DurationMin() ).
|
||||
void PushTask(VariableCumulativeTask* const task, int profile_index,
|
||||
int64 usage) {
|
||||
// Init
|
||||
const int64 demand_min = task->demand()->Min();
|
||||
const int64 adjusted_demand = demand_min == 0 ? 1 : demand_min;
|
||||
const bool is_adjusted = demand_min == 0;
|
||||
const int64 residual_capacity = capacity_->Max() - adjusted_demand;
|
||||
const int64 duration_min = task->duration()->Min();
|
||||
const ProfileDelta& first_prof_delta = profile_unique_time_[profile_index];
|
||||
|
||||
int64 new_start_min = task->StartMin();
|
||||
|
||||
DCHECK_GE(first_prof_delta.time, task->StartMin());
|
||||
// The check above is with a '>='. Let's first treat the '>' case
|
||||
if (first_prof_delta.time > task->StartMin()) {
|
||||
// There was no profile delta at a time between interval->StartMin()
|
||||
// (included) and the current one.
|
||||
// As we don't delete delta's of 0 value, this means the current task
|
||||
// does not contribute to the usage before:
|
||||
DCHECK((task->StartMax() >= first_prof_delta.time) ||
|
||||
(task->StartMax() >= task->EndMin()));
|
||||
// The 'usage' given in argument is valid at first_prof_delta.time. To
|
||||
// compute the usage at the start min, we need to remove the last delta.
|
||||
const int64 usage_at_start_min = usage - first_prof_delta.delta;
|
||||
if (usage_at_start_min > residual_capacity) {
|
||||
new_start_min = profile_unique_time_[profile_index].time;
|
||||
}
|
||||
}
|
||||
|
||||
// Influence of current task
|
||||
const int64 start_max = task->StartMax();
|
||||
const int64 end_min = task->EndMin();
|
||||
// TODO(user): remove delta_start and delta_end.
|
||||
ProfileDelta delta_start(start_max, 0);
|
||||
ProfileDelta delta_end(end_min, 0);
|
||||
if (start_max < end_min) {
|
||||
delta_start.delta = +demand_min;
|
||||
delta_end.delta = -demand_min;
|
||||
}
|
||||
while (profile_unique_time_[profile_index].time <
|
||||
duration_min + new_start_min) {
|
||||
const ProfileDelta& profile_delta = profile_unique_time_[profile_index];
|
||||
DCHECK(profile_index < profile_unique_time_.size());
|
||||
// Compensate for current task
|
||||
if (profile_delta.time == delta_start.time) {
|
||||
usage -= delta_start.delta;
|
||||
}
|
||||
if (profile_delta.time == delta_end.time) {
|
||||
usage -= delta_end.delta;
|
||||
}
|
||||
// Increment time
|
||||
++profile_index;
|
||||
DCHECK(profile_index < profile_unique_time_.size());
|
||||
// Does it fit?
|
||||
if (usage > residual_capacity) {
|
||||
new_start_min = profile_unique_time_[profile_index].time;
|
||||
}
|
||||
usage += profile_unique_time_[profile_index].delta;
|
||||
}
|
||||
if (is_adjusted) {
|
||||
if (new_start_min > task->StartMax()) {
|
||||
task->demand()->SetMax(0);
|
||||
}
|
||||
} else {
|
||||
task->start()->SetMin(new_start_min);
|
||||
}
|
||||
}
|
||||
|
||||
typedef std::vector<ProfileDelta> Profile;
|
||||
|
||||
Profile profile_unique_time_;
|
||||
Profile profile_non_unique_time_;
|
||||
std::vector<VariableCumulativeTask*> by_start_min_;
|
||||
IntVar* const capacity_;
|
||||
|
||||
DISALLOW_COPY_AND_ASSIGN(VariableCumulativeTimeTable);
|
||||
};
|
||||
StringAppendF(&out, "%s, duration = %s, performed = true)",
|
||||
start_->DebugString().c_str(),
|
||||
duration_->DebugString().c_str());
|
||||
return out;
|
||||
}
|
||||
} // namespace
|
||||
|
||||
Constraint* MakeIsBooleanSumInRange(Solver* const solver,
|
||||
@@ -784,99 +649,12 @@ Constraint* MakeIsBooleanSumInRange(Solver* const solver,
|
||||
new IsBooleanSumInRange(solver, variables, range_min, range_max, target));
|
||||
}
|
||||
|
||||
void PostIsBooleanSumInRange(FlatZincModel* const model, CtSpec* const spec,
|
||||
const std::vector<IntVar*>& variables, int64 range_min,
|
||||
int64 range_max, IntVar* const target) {
|
||||
Solver* const solver = model->solver();
|
||||
const int64 size = variables.size();
|
||||
range_min = std::max(0LL, range_min);
|
||||
range_max = std::min(size, range_max);
|
||||
int true_vars = 0;
|
||||
int possible_vars = 0;
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (variables[i]->Max() == 1) {
|
||||
possible_vars++;
|
||||
if (variables[i]->Min() == 1) {
|
||||
true_vars++;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (true_vars > range_max || possible_vars < range_min) {
|
||||
target->SetValue(0);
|
||||
VLOG(2) << " - set target to 0";
|
||||
} else if (true_vars >= range_min && possible_vars <= range_max) {
|
||||
target->SetValue(1);
|
||||
VLOG(2) << " - set target to 1";
|
||||
} else if (FLAGS_use_sat && range_min == size &&
|
||||
AddBoolAndArrayEqVar(model->Sat(), variables, target)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else if (FLAGS_use_sat && range_max == 0 &&
|
||||
AddBoolOrArrayEqVar(model->Sat(), variables,
|
||||
solver->MakeDifference(1, target)->Var())) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == size &&
|
||||
AddBoolOrArrayEqVar(model->Sat(), variables, target)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else {
|
||||
Constraint* const ct = MakeIsBooleanSumInRange(solver, variables, range_min,
|
||||
range_max, target);
|
||||
VLOG(2) << " - posted " << ct->DebugString();
|
||||
model->AddConstraint(spec, ct);
|
||||
}
|
||||
}
|
||||
|
||||
Constraint* MakeBooleanSumInRange(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max) {
|
||||
return solver->RevAlloc(
|
||||
new BooleanSumInRange(solver, variables, range_min, range_max));
|
||||
}
|
||||
void PostBooleanSumInRange(FlatZincModel* const model, CtSpec* const spec,
|
||||
const std::vector<IntVar*>& variables, int64 range_min,
|
||||
int64 range_max) {
|
||||
Solver* const solver = model->solver();
|
||||
const int64 size = variables.size();
|
||||
range_min = std::max(0LL, range_min);
|
||||
range_max = std::min(size, range_max);
|
||||
int true_vars = 0;
|
||||
std::vector<IntVar*> alt;
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (!variables[i]->Bound()) {
|
||||
alt.push_back(variables[i]);
|
||||
} else if (variables[i]->Min() == 1) {
|
||||
true_vars++;
|
||||
}
|
||||
}
|
||||
const int possible_vars = alt.size();
|
||||
range_min -= true_vars;
|
||||
range_max -= true_vars;
|
||||
|
||||
if (range_max < 0 || range_min > possible_vars) {
|
||||
Constraint* const ct = solver->MakeFalseConstraint();
|
||||
VLOG(2) << " - posted " << ct->DebugString();
|
||||
model->AddConstraint(spec, ct);
|
||||
} else if (range_min <= 0 && range_max >= possible_vars) {
|
||||
Constraint* const ct = solver->MakeTrueConstraint();
|
||||
VLOG(2) << " - posted " << ct->DebugString();
|
||||
model->AddConstraint(spec, ct);
|
||||
} else if (FLAGS_use_sat && range_min == 0 && range_max == 1 &&
|
||||
AddAtMostOne(model->Sat(), alt)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else if (FLAGS_use_sat && range_min == 0 && range_max == size - 1 &&
|
||||
AddAtMostNMinusOne(model->Sat(), alt)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == 1 &&
|
||||
AddBoolOrArrayEqualTrue(model->Sat(), alt) &&
|
||||
AddAtMostOne(model->Sat(), alt)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else {
|
||||
Constraint* const ct =
|
||||
MakeBooleanSumInRange(solver, alt, range_min, range_max);
|
||||
VLOG(2) << " - posted " << ct->DebugString();
|
||||
model->AddConstraint(spec, ct);
|
||||
}
|
||||
}
|
||||
|
||||
Constraint* MakeBooleanSumOdd(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables) {
|
||||
return solver->RevAlloc(new BooleanSumOdd(solver, variables));
|
||||
@@ -913,25 +691,6 @@ Constraint* MakeStrongScalProdEquality(Solver* const solver,
|
||||
return solver->MakeAllowedAssignments(variables, tuples);
|
||||
}
|
||||
|
||||
Constraint* MakeInverse(Solver* const solver, const std::vector<IntVar*>& left,
|
||||
const std::vector<IntVar*>& right) {
|
||||
return solver->RevAlloc(new Inverse(solver, left, right));
|
||||
}
|
||||
|
||||
Constraint* MakeVariableCumulative(Solver* const solver,
|
||||
const std::vector<IntVar*>& starts,
|
||||
const std::vector<IntVar*>& durations,
|
||||
const std::vector<IntVar*>& usages,
|
||||
IntVar* const capacity) {
|
||||
std::vector<VariableCumulativeTask*> tasks(starts.size());
|
||||
for (int i = 0; i < starts.size(); ++i) {
|
||||
tasks[i] = solver->RevAlloc(
|
||||
new VariableCumulativeTask(starts[i], durations[i], usages[i]));
|
||||
}
|
||||
return solver->RevAlloc(
|
||||
new VariableCumulativeTimeTable(solver, tasks, capacity));
|
||||
}
|
||||
|
||||
Constraint* MakeVariableOdd(Solver* const s, IntVar* const var) {
|
||||
return s->RevAlloc(new VariableParity(s, var, true));
|
||||
}
|
||||
@@ -939,4 +698,123 @@ Constraint* MakeVariableOdd(Solver* const s, IntVar* const var) {
|
||||
Constraint* MakeVariableEven(Solver* const s, IntVar* const var) {
|
||||
return s->RevAlloc(new VariableParity(s, var, false));
|
||||
}
|
||||
|
||||
Constraint* MakeBoundModulo(Solver* const s, IntVar* const var,
|
||||
IntVar* const mod, int64 residual) {
|
||||
return s->RevAlloc(new BoundModulo(s, var, mod, residual));
|
||||
}
|
||||
|
||||
void PostBooleanSumInRange(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max) {
|
||||
const int64 size = variables.size();
|
||||
range_min = std::max(0LL, range_min);
|
||||
range_max = std::min(size, range_max);
|
||||
int true_vars = 0;
|
||||
std::vector<IntVar*> alt;
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (!variables[i]->Bound()) {
|
||||
alt.push_back(variables[i]);
|
||||
} else if (variables[i]->Min() == 1) {
|
||||
true_vars++;
|
||||
}
|
||||
}
|
||||
const int possible_vars = alt.size();
|
||||
range_min -= true_vars;
|
||||
range_max -= true_vars;
|
||||
|
||||
if (range_max < 0 || range_min > possible_vars) {
|
||||
Constraint* const ct = solver->MakeFalseConstraint();
|
||||
FZVLOG << " - posted " << ct->DebugString() << FZENDL;
|
||||
solver->AddConstraint(ct);
|
||||
} else if (range_min <= 0 && range_max >= possible_vars) {
|
||||
FZVLOG << " - ignore true constraint" << FZENDL;
|
||||
} else if (FLAGS_use_sat && AddSumInRange(sat, alt, range_min, range_max)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 0 && range_max == 1 &&
|
||||
AddAtMostOne(sat, alt)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 0 && range_max == size - 1 &&
|
||||
AddAtMostNMinusOne(sat, alt)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == 1 &&
|
||||
AddBoolOrArrayEqualTrue(sat, alt) && AddAtMostOne(sat, alt)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == possible_vars &&
|
||||
AddBoolOrArrayEqualTrue(sat, alt)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else {
|
||||
Constraint* const ct =
|
||||
MakeBooleanSumInRange(solver, alt, range_min, range_max);
|
||||
FZVLOG << " - posted " << ct->DebugString() << FZENDL;
|
||||
solver->AddConstraint(ct);
|
||||
}
|
||||
}
|
||||
|
||||
void PostIsBooleanSumInRange(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max, IntVar* target) {
|
||||
const int64 size = variables.size();
|
||||
range_min = std::max(0LL, range_min);
|
||||
range_max = std::min(size, range_max);
|
||||
int true_vars = 0;
|
||||
int possible_vars = 0;
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (variables[i]->Max() == 1) {
|
||||
possible_vars++;
|
||||
if (variables[i]->Min() == 1) {
|
||||
true_vars++;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (true_vars > range_max || possible_vars < range_min) {
|
||||
target->SetValue(0);
|
||||
FZVLOG << " - set target to 0" << FZENDL;
|
||||
} else if (true_vars >= range_min && possible_vars <= range_max) {
|
||||
target->SetValue(1);
|
||||
FZVLOG << " - set target to 1" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == size &&
|
||||
AddBoolAndArrayEqVar(sat, variables, target)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_max == 0 &&
|
||||
AddBoolOrArrayEqVar(sat, variables,
|
||||
solver->MakeDifference(1, target)->Var())) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == size &&
|
||||
AddBoolOrArrayEqVar(sat, variables, target)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else {
|
||||
Constraint* const ct = MakeIsBooleanSumInRange(solver, variables, range_min,
|
||||
range_max, target);
|
||||
FZVLOG << " - posted " << ct->DebugString() << FZENDL;
|
||||
solver->AddConstraint(ct);
|
||||
}
|
||||
}
|
||||
|
||||
void PostIsBooleanSumDifferent(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 value, IntVar* target) {
|
||||
const int64 size = variables.size();
|
||||
if (value == 0) {
|
||||
PostIsBooleanSumInRange(sat, solver, variables, 1, size, target);
|
||||
} else if (value == size) {
|
||||
PostIsBooleanSumInRange(sat, solver, variables, 0, size - 1, target);
|
||||
} else {
|
||||
Constraint* const ct =
|
||||
solver->MakeIsDifferentCstCt(solver->MakeSum(variables), value, target);
|
||||
FZVLOG << " - posted " << ct->DebugString() << FZENDL;
|
||||
solver->AddConstraint(ct);
|
||||
}
|
||||
}
|
||||
|
||||
IntervalVar* MakePerformedIntervalVar(Solver* const solver,
|
||||
IntVar* const start,
|
||||
IntVar* const duration,
|
||||
const std::string& n) {
|
||||
CHECK(start != nullptr);
|
||||
CHECK(duration != nullptr);
|
||||
return solver->RegisterIntervalVar(solver->RevAlloc(
|
||||
new StartVarDurationVarPerformedIntervalVar(solver, start, duration, n)));
|
||||
}
|
||||
|
||||
} // namespace operations_research
|
||||
|
||||
@@ -11,68 +11,13 @@
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
|
||||
#ifndef OR_TOOLS_FLATZINC_FLATZINC_CONSTRAINTS_H_
|
||||
#define OR_TOOLS_FLATZINC_FLATZINC_CONSTRAINTS_H_
|
||||
#ifndef OR_TOOLS_FLATZINC2_FLATZINC_CONSTRAINTS_H_
|
||||
#define OR_TOOLS_FLATZINC2_FLATZINC_CONSTRAINTS_H_
|
||||
|
||||
#include <map>
|
||||
#include <cassert>
|
||||
|
||||
#include "flatzinc/parser.h"
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
|
||||
namespace operations_research {
|
||||
class SatPropagator;
|
||||
bool AddBoolEq(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right);
|
||||
|
||||
bool AddBoolLe(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right);
|
||||
|
||||
bool AddBoolNot(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right);
|
||||
|
||||
bool AddBoolAndArrayEqVar(SatPropagator* const sat, const std::vector<IntVar*>& vars,
|
||||
IntExpr* const target);
|
||||
|
||||
bool AddBoolOrArrayEqVar(SatPropagator* const sat, const std::vector<IntVar*>& vars,
|
||||
IntExpr* const target);
|
||||
|
||||
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);
|
||||
|
||||
bool AddBoolIsNEqVar(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right, IntExpr* const target);
|
||||
|
||||
bool AddBoolIsLeVar(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right, IntExpr* const target);
|
||||
|
||||
bool AddBoolOrEqVar(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right, IntExpr* const target);
|
||||
|
||||
bool AddBoolIsEqVar(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right, IntExpr* const target);
|
||||
|
||||
bool AddBoolOrArrayEqualTrue(SatPropagator* const sat,
|
||||
const std::vector<IntVar*>& vars);
|
||||
|
||||
bool AddBoolAndArrayEqualFalse(SatPropagator* const sat,
|
||||
const std::vector<IntVar*>& vars);
|
||||
|
||||
bool AddAtMostOne(SatPropagator* const sat, const std::vector<IntVar*>& vars);
|
||||
|
||||
bool AddAtMostNMinusOne(SatPropagator* const sat, const std::vector<IntVar*>& vars);
|
||||
|
||||
bool AddArrayXor(SatPropagator* const sat, const std::vector<IntVar*>& vars);
|
||||
|
||||
bool DeclareVariable(SatPropagator* const sat, IntVar* const var);
|
||||
|
||||
Constraint* MakeStrongScalProdEquality(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
@@ -91,21 +36,26 @@ Constraint* MakeBooleanSumInRange(Solver* const solver,
|
||||
Constraint* MakeBooleanSumOdd(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables);
|
||||
|
||||
Constraint* MakeVariableCumulative(Solver* const solver,
|
||||
const std::vector<IntVar*>& starts,
|
||||
const std::vector<IntVar*>& durations,
|
||||
const std::vector<IntVar*>& usages,
|
||||
IntVar* const capacity);
|
||||
|
||||
Constraint* MakeVariableOdd(Solver* const s, IntVar* const var);
|
||||
Constraint* MakeVariableEven(Solver* const s, IntVar* const var);
|
||||
Constraint* MakeBoundModulo(Solver* const s, IntVar* const var,
|
||||
IntVar* const mod, int64 residual);
|
||||
|
||||
void PostIsBooleanSumInRange(FlatZincModel* const model, CtSpec* const spec,
|
||||
const std::vector<IntVar*>& variables, int64 range_min,
|
||||
int64 range_max, IntVar* const target);
|
||||
void PostIsBooleanSumInRange(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max, IntVar* target);
|
||||
|
||||
void PostBooleanSumInRange(FlatZincModel* const model, CtSpec* const spec,
|
||||
const std::vector<IntVar*>& variables, int64 range_min,
|
||||
int64 range_max);
|
||||
void PostIsBooleanSumDifferent(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 value, IntVar* target);
|
||||
|
||||
void PostBooleanSumInRange(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max);
|
||||
|
||||
IntervalVar* MakePerformedIntervalVar(Solver* const solver,
|
||||
IntVar* const start,
|
||||
IntVar* const duration,
|
||||
const std::string& n);
|
||||
} // namespace operations_research
|
||||
#endif // OR_TOOLS_FLATZINC_FLATZINC_CONSTRAINTS_H_
|
||||
#endif // OR_TOOLS_FLATZINC2_FLATZINC_CONSTRAINTS_H_
|
||||
|
||||
@@ -1,14 +1,38 @@
|
||||
// Copyright 2010-2014 Google
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
// This is the skeleton for the official flatzinc interpreter. Much
|
||||
// of the funcionnalities are fixed (name of parameters, format of the
|
||||
// input): see http://www.minizinc.org/downloads/doc-1.6/flatzinc-spec.pdf
|
||||
|
||||
#if defined(__GNUC__) // Linux or Mac OS X.
|
||||
#include <signal.h>
|
||||
#endif // __GNUC__
|
||||
|
||||
#include <iostream> // NOLINT
|
||||
#include <fstream> // NOLINT
|
||||
#include <cstring>
|
||||
#include "base/unique_ptr.h"
|
||||
#include "base/commandlineflags.h"
|
||||
#include <string>
|
||||
#include <vector>
|
||||
|
||||
#include "base/commandlineflags.h"
|
||||
#include "base/stringprintf.h"
|
||||
#include "base/integral_types.h"
|
||||
#include "base/logging.h"
|
||||
#include "base/stringprintf.h"
|
||||
#include "base/threadpool.h"
|
||||
#include "flatzinc/flatzinc.h"
|
||||
#include "base/timer.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/parser.h"
|
||||
#include "flatzinc/presolve.h"
|
||||
#include "flatzinc/search.h"
|
||||
#include "flatzinc/solver.h"
|
||||
|
||||
DEFINE_int32(log_period, 10000000, "Search log period");
|
||||
DEFINE_bool(all, false, "Search for all solutions");
|
||||
@@ -16,43 +40,55 @@ DEFINE_bool(free, false, "Ignore search annotations");
|
||||
DEFINE_int32(num_solutions, 0, "Number of solution to search for");
|
||||
DEFINE_int32(time_limit, 0, "time limit in ms");
|
||||
DEFINE_int32(workers, 0, "Number of workers");
|
||||
DEFINE_int32(simplex_frequency, 0, "Simplex frequency, 0 = no simplex");
|
||||
DEFINE_bool(use_impact, false, "Use impact based search");
|
||||
DEFINE_double(restart_log_size, -1, "Restart log size for impact search");
|
||||
DEFINE_int32(luby_restart, -1, "Luby restart factor, <= 0 = no luby");
|
||||
DEFINE_int32(heuristic_period, 100, "Period to call heuristics in free search");
|
||||
DEFINE_bool(verbose_impact, false, "Verbose impact");
|
||||
DEFINE_bool(verbose_mt, false, "Verbose Multi-Thread");
|
||||
DEFINE_bool(presolve, true, "Use presolve.");
|
||||
|
||||
DECLARE_bool(fz_logging);
|
||||
DECLARE_bool(log_prefix);
|
||||
DECLARE_bool(logging);
|
||||
DECLARE_bool(use_sat);
|
||||
|
||||
using operations_research::ThreadPool;
|
||||
extern void interrupt_handler(int s);
|
||||
|
||||
namespace operations_research {
|
||||
int Run(const std::string& file, const FlatZincSearchParameters& parameters,
|
||||
FzParallelSupport* const parallel_support) {
|
||||
FlatZincModel fz_model;
|
||||
if (file == "-") {
|
||||
if (!fz_model.Parse(std::cin)) {
|
||||
return -1;
|
||||
}
|
||||
} else {
|
||||
parallel_support->Init(
|
||||
parameters.worker_id,
|
||||
StringPrintf("%%%% model: %s", file.c_str()));
|
||||
if (!fz_model.Parse(file)) {
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
|
||||
fz_model.Solve(parameters, parallel_support);
|
||||
return 0;
|
||||
void Solve(const FzModel* const model, const FzSolverParameters& parameters,
|
||||
FzParallelSupportInterface* parallel_support) {
|
||||
FzSolver solver(*model);
|
||||
CHECK(solver.Extract());
|
||||
solver.Solve(parameters, parallel_support);
|
||||
}
|
||||
|
||||
void ParallelRun(char* const file, int worker_id,
|
||||
FzParallelSupport* const parallel_support) {
|
||||
operations_research::FlatZincSearchParameters parameters;
|
||||
void SequentialRun(const FzModel* model) {
|
||||
FzSolverParameters parameters;
|
||||
parameters.all_solutions = FLAGS_all;
|
||||
parameters.free_search = FLAGS_free;
|
||||
parameters.heuristic_period = FLAGS_heuristic_period;
|
||||
parameters.ignore_unknown = false;
|
||||
parameters.log_period = FLAGS_log_period;
|
||||
parameters.luby_restart = FLAGS_luby_restart;
|
||||
parameters.num_solutions = FLAGS_num_solutions;
|
||||
parameters.restart_log_size = FLAGS_restart_log_size;
|
||||
parameters.threads = FLAGS_workers;
|
||||
parameters.time_limit_in_ms = FLAGS_time_limit;
|
||||
parameters.use_log = FLAGS_fz_logging;
|
||||
parameters.verbose_impact = FLAGS_verbose_impact;
|
||||
parameters.worker_id = -1;
|
||||
parameters.search_type =
|
||||
FLAGS_use_impact ? FzSolverParameters::IBS : FzSolverParameters::DEFAULT;
|
||||
|
||||
std::unique_ptr<FzParallelSupportInterface> parallel_support(
|
||||
MakeSequentialSupport(FLAGS_all, FLAGS_num_solutions));
|
||||
Solve(model, parameters, parallel_support.get());
|
||||
}
|
||||
|
||||
void ParallelRun(const FzModel* const model, int worker_id,
|
||||
FzParallelSupportInterface* parallel_support) {
|
||||
FzSolverParameters parameters;
|
||||
parameters.all_solutions = FLAGS_all;
|
||||
parameters.heuristic_period = FLAGS_heuristic_period;
|
||||
parameters.ignore_unknown = false;
|
||||
@@ -60,7 +96,6 @@ void ParallelRun(char* const file, int worker_id,
|
||||
parameters.luby_restart = -1;
|
||||
parameters.num_solutions = FLAGS_num_solutions;
|
||||
parameters.random_seed = worker_id * 10;
|
||||
parameters.simplex_frequency = FLAGS_simplex_frequency;
|
||||
parameters.threads = FLAGS_workers;
|
||||
parameters.time_limit_in_ms = FLAGS_time_limit;
|
||||
parameters.use_log = false;
|
||||
@@ -69,37 +104,34 @@ void ParallelRun(char* const file, int worker_id,
|
||||
switch (worker_id) {
|
||||
case 0: {
|
||||
parameters.free_search = false;
|
||||
parameters.search_type =
|
||||
operations_research::FlatZincSearchParameters::DEFAULT;
|
||||
parameters.search_type = operations_research::FzSolverParameters::DEFAULT;
|
||||
parameters.restart_log_size = -1.0;
|
||||
break;
|
||||
}
|
||||
case 1: {
|
||||
parameters.free_search = true;
|
||||
parameters.search_type =
|
||||
operations_research::FlatZincSearchParameters::MIN_SIZE;
|
||||
operations_research::FzSolverParameters::MIN_SIZE;
|
||||
parameters.restart_log_size = -1.0;
|
||||
break;
|
||||
}
|
||||
case 2: {
|
||||
parameters.free_search = true;
|
||||
parameters.search_type =
|
||||
operations_research::FlatZincSearchParameters::IBS;
|
||||
parameters.search_type = operations_research::FzSolverParameters::IBS;
|
||||
parameters.restart_log_size = FLAGS_restart_log_size;
|
||||
break;
|
||||
}
|
||||
case 3: {
|
||||
parameters.free_search = true;
|
||||
parameters.search_type =
|
||||
operations_research::FlatZincSearchParameters::FIRST_UNBOUND;
|
||||
operations_research::FzSolverParameters::FIRST_UNBOUND;
|
||||
parameters.restart_log_size = -1.0;
|
||||
parameters.heuristic_period = 10000000;
|
||||
break;
|
||||
}
|
||||
case 4: {
|
||||
parameters.free_search = true;
|
||||
parameters.search_type =
|
||||
operations_research::FlatZincSearchParameters::DEFAULT;
|
||||
parameters.search_type = operations_research::FzSolverParameters::DEFAULT;
|
||||
parameters.restart_log_size = -1.0;
|
||||
parameters.heuristic_period = 30;
|
||||
parameters.run_all_heuristics = true;
|
||||
@@ -109,40 +141,13 @@ void ParallelRun(char* const file, int worker_id,
|
||||
parameters.free_search = true;
|
||||
parameters.search_type =
|
||||
worker_id % 2 == 0
|
||||
? operations_research::FlatZincSearchParameters::RANDOM_MIN
|
||||
: operations_research::FlatZincSearchParameters::RANDOM_MAX;
|
||||
? operations_research::FzSolverParameters::RANDOM_MIN
|
||||
: operations_research::FzSolverParameters::RANDOM_MAX;
|
||||
parameters.restart_log_size = -1.0;
|
||||
parameters.luby_restart = 250;
|
||||
}
|
||||
}
|
||||
Run(file, parameters, parallel_support);
|
||||
}
|
||||
|
||||
void SequentialRun(char* const file) {
|
||||
FlatZincSearchParameters parameters;
|
||||
parameters.all_solutions = FLAGS_all;
|
||||
parameters.free_search = FLAGS_free;
|
||||
parameters.heuristic_period = FLAGS_heuristic_period;
|
||||
parameters.ignore_unknown = false;
|
||||
parameters.log_period = FLAGS_log_period;
|
||||
parameters.luby_restart = FLAGS_luby_restart;
|
||||
parameters.num_solutions = FLAGS_num_solutions;
|
||||
parameters.restart_log_size = FLAGS_restart_log_size;
|
||||
parameters.simplex_frequency = FLAGS_simplex_frequency;
|
||||
parameters.threads = FLAGS_workers;
|
||||
parameters.time_limit_in_ms = FLAGS_time_limit;
|
||||
parameters.use_log = FLAGS_logging;
|
||||
parameters.verbose_impact = FLAGS_verbose_impact;
|
||||
parameters.worker_id = -1;
|
||||
parameters.search_type =
|
||||
FLAGS_use_impact ? FlatZincSearchParameters::IBS
|
||||
: FlatZincSearchParameters::DEFAULT;
|
||||
|
||||
std::unique_ptr<FzParallelSupport> parallel_support(
|
||||
operations_research::MakeSequentialSupport(parameters.all_solutions,
|
||||
parameters.num_solutions,
|
||||
FLAGS_verbose_mt));
|
||||
Run(file, parameters, parallel_support.get());
|
||||
Solve(model, parameters, parallel_support);
|
||||
}
|
||||
|
||||
void FixAndParseParameters(int* argc, char*** argv) {
|
||||
@@ -151,7 +156,9 @@ void FixAndParseParameters(int* argc, char*** argv) {
|
||||
char free_param[] = "--free";
|
||||
char workers_param[] = "--workers";
|
||||
char solutions_param[] = "--num_solutions";
|
||||
char logging_param[] = "--logging";
|
||||
char logging_param[] = "--fz_logging";
|
||||
char verbose_param[] = "--fz_verbose";
|
||||
char debug_param[] = "--fz_debug";
|
||||
for (int i = 1; i < *argc; ++i) {
|
||||
if (strcmp((*argv)[i], "-a") == 0) {
|
||||
(*argv)[i] = all_param;
|
||||
@@ -168,8 +175,63 @@ void FixAndParseParameters(int* argc, char*** argv) {
|
||||
if (strcmp((*argv)[i], "-l") == 0) {
|
||||
(*argv)[i] = logging_param;
|
||||
}
|
||||
if (strcmp((*argv)[i], "-v") == 0) {
|
||||
(*argv)[i] = verbose_param;
|
||||
}
|
||||
if (strcmp((*argv)[i], "-d") == 0) {
|
||||
(*argv)[i] = debug_param;
|
||||
}
|
||||
}
|
||||
google::ParseCommandLineFlags(argc, argv, true);
|
||||
// Fix the number of solutions.
|
||||
if (FLAGS_num_solutions == 0) { // not specified
|
||||
FLAGS_num_solutions = FLAGS_all ? kint32max : 1;
|
||||
}
|
||||
}
|
||||
|
||||
void ParseAndRun(const std::string& filename, int num_workers) {
|
||||
WallTimer timer;
|
||||
timer.Start();
|
||||
std::string problem_name(filename);
|
||||
problem_name.resize(problem_name.size() - 4);
|
||||
size_t found = problem_name.find_last_of("/\\");
|
||||
if (found != std::string::npos) {
|
||||
problem_name = problem_name.substr(found + 1);
|
||||
}
|
||||
FzModel model(problem_name);
|
||||
CHECK(ParseFlatzincFile(filename, &model));
|
||||
FZLOG << "File " << filename << " parsed in " << timer.GetInMs() << " ms"
|
||||
<< FZENDL;
|
||||
FzPresolver presolve;
|
||||
presolve.CleanUpModelForTheCpSolver(&model, FLAGS_use_sat);
|
||||
if (FLAGS_presolve) {
|
||||
FZLOG << "Presolve model" << FZENDL;
|
||||
timer.Reset();
|
||||
timer.Start();
|
||||
presolve.Run(&model);
|
||||
FZLOG << " - done in " << timer.GetInMs() << " ms" << FZENDL;
|
||||
}
|
||||
FzModelStatistics stats(model);
|
||||
stats.PrintStatistics();
|
||||
|
||||
#if defined(__GNUC__)
|
||||
signal (SIGINT, &interrupt_handler);
|
||||
#endif
|
||||
|
||||
if (num_workers == 0) {
|
||||
operations_research::SequentialRun(&model);
|
||||
} else {
|
||||
std::unique_ptr<operations_research::FzParallelSupportInterface>
|
||||
parallel_support(operations_research::MakeMtSupport(
|
||||
FLAGS_all, FLAGS_num_solutions, FLAGS_verbose_mt));
|
||||
{
|
||||
ThreadPool pool("Parallel FlatZinc", num_workers);
|
||||
for (int w = 0; w < num_workers; ++w) {
|
||||
pool.Add(NewCallback(ParallelRun, &model, w, parallel_support.get()));
|
||||
}
|
||||
pool.StartWorkers();
|
||||
}
|
||||
}
|
||||
google::ParseCommandLineFlags( argc, argv, true);
|
||||
}
|
||||
} // namespace operations_research
|
||||
|
||||
@@ -179,25 +241,6 @@ int main(int argc, char** argv) {
|
||||
LOG(ERROR) << "Usage: " << argv[0] << " <file>";
|
||||
exit(EXIT_FAILURE);
|
||||
}
|
||||
// Fix the number of solutions.
|
||||
if (FLAGS_num_solutions == 0) { // not specified
|
||||
FLAGS_num_solutions = FLAGS_all ? kint32max : 1;
|
||||
}
|
||||
|
||||
if (FLAGS_workers == 0) {
|
||||
operations_research::SequentialRun(argv[1]);
|
||||
} else {
|
||||
std::unique_ptr<operations_research::FzParallelSupport> parallel_support(
|
||||
operations_research::MakeMtSupport(
|
||||
FLAGS_all, FLAGS_num_solutions, FLAGS_verbose_mt));
|
||||
{
|
||||
ThreadPool pool("Parallel FlatZinc", FLAGS_workers);
|
||||
pool.StartWorkers();
|
||||
for (int w = 0; w < FLAGS_workers; ++w) {
|
||||
pool.Add(NewCallback(&operations_research::ParallelRun, argv[1], w,
|
||||
parallel_support.get()));
|
||||
}
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
operations_research::ParseAndRun(argv[1], FLAGS_workers);
|
||||
return 0;
|
||||
}
|
||||
|
||||
@@ -18,7 +18,7 @@
|
||||
#include "base/join.h"
|
||||
#include "base/map_util.h"
|
||||
#include "base/stl_util.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc/model.h"
|
||||
|
||||
DEFINE_bool(fz_logging, false,
|
||||
"Print logging information from the flatzinc interpreter.");
|
||||
@@ -5,35 +5,8 @@
|
||||
% Assumptions:
|
||||
% - forall i, d[i] >= 0 and r[i] >= 0
|
||||
%-----------------------------------------------------------------------------%
|
||||
predicate fixed_cumulative(array[int] of var int: s,
|
||||
array[int] of int: d,
|
||||
array[int] of int: r,
|
||||
int: b);
|
||||
|
||||
predicate var_cumulative(array[int] of var int: s,
|
||||
array[int] of int: d,
|
||||
array[int] of int: r,
|
||||
var int: b);
|
||||
|
||||
predicate variable_cumulative(array[int] of var int: s,
|
||||
array[int] of var int: d,
|
||||
array[int] of var int: r,
|
||||
var int: b);
|
||||
|
||||
predicate cumulative(array[int] of var int: s,
|
||||
array[int] of int: d,
|
||||
array[int] of int: r,
|
||||
int: b) =
|
||||
fixed_cumulative(s, d, r, b);
|
||||
|
||||
predicate cumulative(array[int] of var int: s,
|
||||
array[int] of int: d,
|
||||
array[int] of int: r,
|
||||
var int: b) =
|
||||
var_cumulative(s, d, r, b);
|
||||
|
||||
predicate cumulative(array[int] of var int: s,
|
||||
array[int] of var int: d,
|
||||
array[int] of var int: r,
|
||||
var int: b) =
|
||||
variable_cumulative(s, d, r, b);
|
||||
var int: b);
|
||||
|
||||
|
||||
@@ -18,8 +18,8 @@
|
||||
#include "base/stringprintf.h"
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
#include "constraint_solver/constraint_solveri.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/search.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/search.h"
|
||||
|
||||
DECLARE_bool(fz_logging);
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -11,7 +11,7 @@
|
||||
#include <string>
|
||||
#include "base/integral_types.h"
|
||||
#include "base/strtoint.h"
|
||||
#include "flatzinc2/parser.tab.hh"
|
||||
#include "flatzinc/parser.tab.hh"
|
||||
using operations_research::atoi64;
|
||||
#if defined(_MSC_VER)
|
||||
#define YY_NO_UNISTD_H
|
||||
@@ -21,7 +21,7 @@
|
||||
#if !defined(OR_TOOLS_FLATZINC_FLATZINC_TAB_HH_)
|
||||
#define OR_TOOLS_FLATZINC_FLATZINC_TAB_HH_
|
||||
#include "base/map_util.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc/model.h"
|
||||
|
||||
namespace operations_research {
|
||||
// This is the context used during parsing.
|
||||
@@ -113,8 +113,8 @@ typedef operations_research::LexerInfo YYSTYPE;
|
||||
#include "base/integral_types.h"
|
||||
#include "base/logging.h"
|
||||
#include "base/stl_util.h"
|
||||
#include "flatzinc2/parser.tab.hh"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc/parser.tab.hh"
|
||||
#include "flatzinc/model.h"
|
||||
#include "util/string_array.h"
|
||||
|
||||
extern int orfz_lex(YYSTYPE*, void* scanner);
|
||||
@@ -18,9 +18,9 @@
|
||||
|
||||
#include "base/commandlineflags.h"
|
||||
#include "base/commandlineflags.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/parser.h"
|
||||
#include "flatzinc2/presolve.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/parser.h"
|
||||
#include "flatzinc/presolve.h"
|
||||
|
||||
DEFINE_string(file, "", "Input file in the flatzinc format.");
|
||||
DEFINE_bool(print, false, "Print model.");
|
||||
@@ -10,7 +10,7 @@
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
#include "flatzinc2/presolve.h"
|
||||
#include "flatzinc/presolve.h"
|
||||
|
||||
#include <algorithm>
|
||||
#include "base/hash.h"
|
||||
@@ -18,7 +18,7 @@
|
||||
#include "base/integral_types.h"
|
||||
#include "base/logging.h"
|
||||
#include "base/hash.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc/model.h"
|
||||
|
||||
namespace operations_research {
|
||||
// The FzPresolver "pre-solves" a FzModel by applying some iterative
|
||||
@@ -10,7 +10,7 @@
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
#include "flatzinc2/sat_constraint.h"
|
||||
#include "flatzinc/sat_constraint.h"
|
||||
|
||||
#include <algorithm>
|
||||
#include <string>
|
||||
@@ -22,9 +22,9 @@
|
||||
#include "base/hash.h"
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
#include "constraint_solver/constraint_solveri.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/search.h"
|
||||
#include "flatzinc2/solver.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/search.h"
|
||||
#include "flatzinc/solver.h"
|
||||
|
||||
DECLARE_bool(fz_logging);
|
||||
DECLARE_bool(fz_verbose);
|
||||
@@ -14,7 +14,7 @@
|
||||
#define OR_TOOLS_FLATZINC_SEARCH_H_
|
||||
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc/model.h"
|
||||
|
||||
namespace operations_research {
|
||||
struct FzSolverParameters {
|
||||
@@ -17,8 +17,8 @@
|
||||
#include "base/stringprintf.h"
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
#include "constraint_solver/constraint_solveri.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/search.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/search.h"
|
||||
|
||||
DECLARE_bool(fz_logging);
|
||||
|
||||
@@ -15,9 +15,9 @@
|
||||
#include "base/logging.h"
|
||||
#include "base/hash.h"
|
||||
#include "base/map_util.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/sat_constraint.h"
|
||||
#include "flatzinc2/solver.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/sat_constraint.h"
|
||||
#include "flatzinc/solver.h"
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
#include "util/string_array.h"
|
||||
|
||||
@@ -14,8 +14,8 @@
|
||||
#define OR_TOOLS_FLATZINC_SOLVER_H_
|
||||
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/search.h"
|
||||
#include "flatzinc/model.h"
|
||||
#include "flatzinc/search.h"
|
||||
|
||||
namespace operations_research {
|
||||
class SatPropagator;
|
||||
@@ -1,61 +0,0 @@
|
||||
// Copyright 2010-2014 Google
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
|
||||
#ifndef OR_TOOLS_FLATZINC2_FLATZINC_CONSTRAINTS_H_
|
||||
#define OR_TOOLS_FLATZINC2_FLATZINC_CONSTRAINTS_H_
|
||||
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
|
||||
namespace operations_research {
|
||||
class SatPropagator;
|
||||
|
||||
Constraint* MakeStrongScalProdEquality(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
const std::vector<int64>& coefficients,
|
||||
int64 rhs);
|
||||
|
||||
Constraint* MakeIsBooleanSumInRange(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max,
|
||||
IntVar* const target);
|
||||
|
||||
Constraint* MakeBooleanSumInRange(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max);
|
||||
|
||||
Constraint* MakeBooleanSumOdd(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables);
|
||||
|
||||
Constraint* MakeVariableOdd(Solver* const s, IntVar* const var);
|
||||
Constraint* MakeVariableEven(Solver* const s, IntVar* const var);
|
||||
Constraint* MakeBoundModulo(Solver* const s, IntVar* const var,
|
||||
IntVar* const mod, int64 residual);
|
||||
|
||||
void PostIsBooleanSumInRange(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max, IntVar* target);
|
||||
|
||||
void PostIsBooleanSumDifferent(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 value, IntVar* target);
|
||||
|
||||
void PostBooleanSumInRange(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max);
|
||||
|
||||
IntervalVar* MakePerformedIntervalVar(Solver* const solver,
|
||||
IntVar* const start,
|
||||
IntVar* const duration,
|
||||
const std::string& n);
|
||||
} // namespace operations_research
|
||||
#endif // OR_TOOLS_FLATZINC2_FLATZINC_CONSTRAINTS_H_
|
||||
@@ -1,12 +0,0 @@
|
||||
%-----------------------------------------------------------------------------%
|
||||
% Requires that a set of tasks given by start times 's', durations 'd', and
|
||||
% resource requirements 'r', never require more than a global resource bound
|
||||
% 'b' at any one time.
|
||||
% Assumptions:
|
||||
% - forall i, d[i] >= 0 and r[i] >= 0
|
||||
%-----------------------------------------------------------------------------%
|
||||
predicate cumulative(array[int] of var int: s,
|
||||
array[int] of var int: d,
|
||||
array[int] of var int: r,
|
||||
var int: b);
|
||||
|
||||
@@ -1,76 +0,0 @@
|
||||
// Copyright 2010-2014 Google
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
#include <cstdio>
|
||||
#include "base/file.h"
|
||||
#include "flatzinc2/parser.h"
|
||||
#include "flatzinc2/parser.tab.hh"
|
||||
|
||||
// Declare external functions in the flatzinc.tab.cc generated file.
|
||||
extern int orfz_parse(operations_research::FzParserContext* parser,
|
||||
operations_research::FzModel* model, bool* ok,
|
||||
void* scanner);
|
||||
extern int orfz_lex_init(void** scanner);
|
||||
extern int orfz_lex_destroy(void* scanner);
|
||||
extern void orfz_set_in(FILE* in_str, void* yyscanner);
|
||||
// Declare external functions and structures in the flatzinc.yy.cc
|
||||
// generated file.
|
||||
struct yy_buffer_state;
|
||||
extern yy_buffer_state* orfz__scan_bytes(const char* input, size_t size,
|
||||
void* scanner);
|
||||
extern void orfz__delete_buffer(yy_buffer_state* b, void* scanner);
|
||||
|
||||
namespace operations_research {
|
||||
// ----- public parsing API -----
|
||||
|
||||
bool ParseFlatzincFile(const std::string& filename, FzModel* const model) {
|
||||
// Init.
|
||||
FILE* const input = fopen(filename.c_str(), "r");
|
||||
if (input == nullptr) {
|
||||
LOG(INFO) << "Could not open file '" << filename << "'";
|
||||
return false;
|
||||
}
|
||||
FzParserContext context;
|
||||
bool ok = true;
|
||||
void* scanner = nullptr;
|
||||
orfz_lex_init(&scanner);
|
||||
orfz_set_in(input, scanner);
|
||||
// Parse.
|
||||
orfz_parse(&context, model, &ok, scanner);
|
||||
// Clean up.
|
||||
if (scanner != nullptr) {
|
||||
orfz_lex_destroy(scanner);
|
||||
}
|
||||
fclose(input);
|
||||
return ok;
|
||||
}
|
||||
|
||||
bool ParseFlatzincString(const std::string& input, FzModel* const model) {
|
||||
// Init.
|
||||
FzParserContext context;
|
||||
bool ok = true;
|
||||
void* scanner = nullptr;
|
||||
orfz_lex_init(&scanner);
|
||||
yy_buffer_state* const string_buffer =
|
||||
orfz__scan_bytes(input.data(), input.size(), scanner);
|
||||
// Parse.
|
||||
orfz_parse(&context, model, &ok, scanner);
|
||||
// Clean up.
|
||||
if (string_buffer != nullptr) {
|
||||
orfz__delete_buffer(string_buffer, scanner);
|
||||
}
|
||||
if (scanner != nullptr) {
|
||||
orfz_lex_destroy(scanner);
|
||||
}
|
||||
return ok;
|
||||
}
|
||||
} // namespace operations_research
|
||||
@@ -1,25 +0,0 @@
|
||||
// Copyright 2010-2014 Google
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
#ifndef OR_TOOLS_FLATZINC_PARSER_H_
|
||||
#define OR_TOOLS_FLATZINC_PARSER_H_
|
||||
|
||||
#include <string>
|
||||
|
||||
#include "flatzinc2/model.h"
|
||||
|
||||
namespace operations_research {
|
||||
// Public parsing API.
|
||||
bool ParseFlatzincFile(const std::string& filename, FzModel* const model);
|
||||
bool ParseFlatzincString(const std::string& input, FzModel* const model);
|
||||
} // namespace operations_research
|
||||
#endif // OR_TOOLS_FLATZINC_PARSER_H_
|
||||
@@ -36,7 +36,7 @@
|
||||
#include <string>
|
||||
|
||||
#include "base/stringprintf.h"
|
||||
#include "flatzinc/flatzinc.h"
|
||||
#include "old_flatzinc/flatzinc.h"
|
||||
#include "base/hash.h"
|
||||
|
||||
DECLARE_bool(use_sat);
|
||||
@@ -39,7 +39,7 @@
|
||||
#include <cassert>
|
||||
#include "base/unique_ptr.h"
|
||||
|
||||
#include "flatzinc/parser.h"
|
||||
#include "old_flatzinc/parser.h"
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
|
||||
/*
|
||||
@@ -55,8 +55,8 @@ void orfz_error(operations_research::ParserState*, void*, const char*);
|
||||
yyscanner, s)
|
||||
|
||||
#include "base/strtoint.h"
|
||||
#include "flatzinc/parser.h"
|
||||
#include "flatzinc/flatzinc.tab.hh"
|
||||
#include "old_flatzinc/parser.h"
|
||||
#include "old_flatzinc/flatzinc.tab.hh"
|
||||
|
||||
using operations_research::atoi64;
|
||||
|
||||
@@ -43,9 +43,9 @@
|
||||
#define YYPARSE_PARAM parm
|
||||
#define YYLEX_PARAM yyscanner
|
||||
|
||||
#include "flatzinc/flatzinc.h"
|
||||
#include "flatzinc/parser.h"
|
||||
#include "flatzinc/flatzinc.tab.hh"
|
||||
#include "old_flatzinc/flatzinc.h"
|
||||
#include "old_flatzinc/parser.h"
|
||||
#include "old_flatzinc/flatzinc.tab.hh"
|
||||
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
@@ -10,18 +10,17 @@
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
#include "flatzinc2/flatzinc_constraints.h"
|
||||
|
||||
#include "old_flatzinc/flatzinc_constraints.h"
|
||||
|
||||
#include "base/commandlineflags.h"
|
||||
#include "old_flatzinc/flatzinc.h"
|
||||
#include "constraint_solver/constraint_solveri.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/sat_constraint.h"
|
||||
#include "util/string_array.h"
|
||||
|
||||
DECLARE_bool(cp_trace_search);
|
||||
DECLARE_bool(cp_trace_propagation);
|
||||
DECLARE_bool(use_sat);
|
||||
DECLARE_bool(fz_verbose);
|
||||
|
||||
namespace operations_research {
|
||||
namespace {
|
||||
@@ -122,47 +121,6 @@ class BooleanSumOdd : public Constraint {
|
||||
NumericalRev<int> num_always_true_vars_;
|
||||
};
|
||||
|
||||
class BoundModulo : public Constraint {
|
||||
public:
|
||||
BoundModulo(Solver* const s, IntVar* x, IntVar* const m, int64 r)
|
||||
: Constraint(s), var_(x), mod_(m), residual_(r) {}
|
||||
|
||||
virtual ~BoundModulo() {}
|
||||
|
||||
virtual void Post() {
|
||||
Demon* const d = solver()->MakeConstraintInitialPropagateCallback(this);
|
||||
var_->WhenRange(d);
|
||||
mod_->WhenBound(d);
|
||||
}
|
||||
|
||||
virtual void InitialPropagate() {
|
||||
if (mod_->Bound()) {
|
||||
const int64 d = std::abs(mod_->Min());
|
||||
if (d == 0) {
|
||||
solver()->Fail();
|
||||
} else {
|
||||
const int64 emin = var_->Min();
|
||||
const int64 emax = var_->Max();
|
||||
const int64 new_min = PosIntDivUp(emin - residual_, d) * d + residual_;
|
||||
const int64 new_max =
|
||||
PosIntDivDown(emax - residual_, d) * d + residual_;
|
||||
var_->SetRange(new_min, new_max);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("(%s %% %s == %" GG_LL_FORMAT "d)",
|
||||
var_->DebugString().c_str(),
|
||||
mod_->DebugString().c_str(), residual_);
|
||||
}
|
||||
|
||||
private:
|
||||
IntVar* const var_;
|
||||
IntVar* const mod_;
|
||||
const int64 residual_;
|
||||
};
|
||||
|
||||
class VariableParity : public Constraint {
|
||||
public:
|
||||
VariableParity(Solver* const s, IntVar* const var, bool odd)
|
||||
@@ -249,6 +207,7 @@ class IsBooleanSumInRange : public Constraint {
|
||||
virtual void InitialPropagate() {
|
||||
int num_always_true = 0;
|
||||
int num_possible_true = 0;
|
||||
int possible_true_index = -1;
|
||||
for (int i = 0; i < vars_.size(); ++i) {
|
||||
const IntVar* const var = vars_[i];
|
||||
if (var->Min() == 1) {
|
||||
@@ -256,6 +215,7 @@ class IsBooleanSumInRange : public Constraint {
|
||||
num_possible_true++;
|
||||
} else if (var->Max() == 1) {
|
||||
num_possible_true++;
|
||||
possible_true_index = i;
|
||||
}
|
||||
}
|
||||
num_possible_true_vars_.SetValue(solver(), num_possible_true);
|
||||
@@ -304,10 +264,10 @@ class IsBooleanSumInRange : public Constraint {
|
||||
}
|
||||
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf(
|
||||
"Sum([%s]) in [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d] == %s",
|
||||
JoinDebugStringPtr(vars_, ", ").c_str(), range_min_, range_max_,
|
||||
target_->DebugString().c_str());
|
||||
return StringPrintf("Sum([%s]) in [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT
|
||||
"d] == %s",
|
||||
JoinDebugStringPtr(vars_, ", ").c_str(), range_min_,
|
||||
range_max_, target_->DebugString().c_str());
|
||||
}
|
||||
|
||||
virtual void Accept(ModelVisitor* const visitor) const {
|
||||
@@ -460,185 +420,360 @@ class BooleanSumInRange : public Constraint {
|
||||
NumericalRev<int> num_always_true_vars_;
|
||||
};
|
||||
|
||||
// ----- Variable duration interval var -----
|
||||
// ----- Inverse constraint -----
|
||||
|
||||
class StartVarDurationVarPerformedIntervalVar : public IntervalVar {
|
||||
// This constraints maintains: left[i] == j <=> right_[j] == i.
|
||||
// It assumes array are 0 based.
|
||||
class Inverse : public Constraint {
|
||||
public:
|
||||
StartVarDurationVarPerformedIntervalVar(Solver* const s,
|
||||
IntVar* const start,
|
||||
IntVar* const duration,
|
||||
const std::string& name);
|
||||
virtual ~StartVarDurationVarPerformedIntervalVar() {}
|
||||
|
||||
virtual int64 StartMin() const;
|
||||
virtual int64 StartMax() const;
|
||||
virtual void SetStartMin(int64 m);
|
||||
virtual void SetStartMax(int64 m);
|
||||
virtual void SetStartRange(int64 mi, int64 ma);
|
||||
virtual int64 OldStartMin() const { return start_->OldMin(); }
|
||||
virtual int64 OldStartMax() const { return start_->OldMax(); }
|
||||
virtual void WhenStartRange(Demon* const d) { start_->WhenRange(d); }
|
||||
virtual void WhenStartBound(Demon* const d) { start_->WhenBound(d); }
|
||||
|
||||
virtual int64 DurationMin() const;
|
||||
virtual int64 DurationMax() const;
|
||||
virtual void SetDurationMin(int64 m);
|
||||
virtual void SetDurationMax(int64 m);
|
||||
virtual void SetDurationRange(int64 mi, int64 ma);
|
||||
virtual int64 OldDurationMin() const { return duration_->Min(); }
|
||||
virtual int64 OldDurationMax() const { return duration_->Max(); }
|
||||
virtual void WhenDurationRange(Demon* const d) { duration_->WhenRange(d); }
|
||||
virtual void WhenDurationBound(Demon* const d) { duration_->WhenBound(d); }
|
||||
|
||||
virtual int64 EndMin() const;
|
||||
virtual int64 EndMax() const;
|
||||
virtual void SetEndMin(int64 m);
|
||||
virtual void SetEndMax(int64 m);
|
||||
virtual void SetEndRange(int64 mi, int64 ma);
|
||||
virtual int64 OldEndMin() const {
|
||||
return start_->OldMin() + duration_->OldMin();
|
||||
}
|
||||
virtual int64 OldEndMax() const {
|
||||
return start_->OldMax() + duration_->OldMax();
|
||||
}
|
||||
virtual void WhenEndRange(Demon* const d) {
|
||||
start_->WhenRange(d);
|
||||
duration_->WhenRange(d);
|
||||
}
|
||||
virtual void WhenEndBound(Demon* const d) {
|
||||
start_->WhenBound(d);
|
||||
duration_->WhenBound(d);
|
||||
Inverse(Solver* const s, const std::vector<IntVar*>& left,
|
||||
const std::vector<IntVar*>& right)
|
||||
: Constraint(s),
|
||||
left_(left),
|
||||
right_(right),
|
||||
left_holes_(left.size()),
|
||||
left_iterators_(left_.size()),
|
||||
right_holes_(right_.size()),
|
||||
right_iterators_(right_.size()) {
|
||||
CHECK_EQ(left_.size(), right_.size());
|
||||
for (int i = 0; i < left_.size(); ++i) {
|
||||
left_holes_[i] = left_[i]->MakeHoleIterator(true);
|
||||
left_iterators_[i] = left_[i]->MakeDomainIterator(true);
|
||||
right_holes_[i] = right_[i]->MakeHoleIterator(true);
|
||||
right_iterators_[i] = right_[i]->MakeDomainIterator(true);
|
||||
}
|
||||
}
|
||||
|
||||
virtual bool MustBePerformed() const;
|
||||
virtual bool MayBePerformed() const;
|
||||
virtual void SetPerformed(bool val);
|
||||
virtual bool WasPerformedBound() const { return true; }
|
||||
virtual void WhenPerformedBound(Demon* const d) {}
|
||||
virtual std::string DebugString() const;
|
||||
virtual ~Inverse() {}
|
||||
|
||||
virtual IntExpr* StartExpr() { return start_; }
|
||||
virtual IntExpr* DurationExpr() { return duration_; }
|
||||
virtual IntExpr* EndExpr() {
|
||||
return solver()->MakeSum(start_, duration_);
|
||||
virtual void Post() {
|
||||
for (int i = 0; i < left_.size(); ++i) {
|
||||
Demon* const left_demon = MakeConstraintDemon2(
|
||||
solver(), this, &Inverse::Propagate, "Propagate", i, true);
|
||||
left_[i]->WhenDomain(left_demon);
|
||||
Demon* const right_demon = MakeConstraintDemon2(
|
||||
solver(), this, &Inverse::Propagate, "Propagate", i, false);
|
||||
right_[i]->WhenDomain(right_demon);
|
||||
}
|
||||
solver()->AddConstraint(solver()->MakeAllDifferent(left_, false));
|
||||
solver()->AddConstraint(solver()->MakeAllDifferent(right_, false));
|
||||
}
|
||||
virtual IntExpr* PerformedExpr() { return solver()->MakeIntConst(1); }
|
||||
virtual IntExpr* SafeStartExpr(int64 unperformed_value) {
|
||||
return StartExpr();
|
||||
|
||||
virtual void InitialPropagate() {
|
||||
const int size = left_.size();
|
||||
for (int i = 0; i < size; ++i) {
|
||||
left_[i]->SetRange(0, size - 1);
|
||||
right_[i]->SetRange(0, size - 1);
|
||||
}
|
||||
for (int i = 0; i < size; ++i) {
|
||||
PropagateDomain(i, left_[i], left_iterators_[i], right_, &remove_left_);
|
||||
PropagateDomain(i, right_[i], right_iterators_[i], left_, &remove_right_);
|
||||
}
|
||||
}
|
||||
virtual IntExpr* SafeDurationExpr(int64 unperformed_value) {
|
||||
return DurationExpr();
|
||||
|
||||
void Propagate(int index, bool left_to_right) {
|
||||
if (left_to_right) {
|
||||
PropagateHoles(index, left_[index], left_holes_[index], right_);
|
||||
} else {
|
||||
PropagateHoles(index, right_[index], right_holes_[index], left_);
|
||||
}
|
||||
}
|
||||
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("Inverse([%s], [%s])",
|
||||
JoinDebugStringPtr(left_, ", ").c_str(),
|
||||
JoinDebugStringPtr(right_, ", ").c_str());
|
||||
}
|
||||
virtual IntExpr* SafeEndExpr(int64 unperformed_value) { return EndExpr(); }
|
||||
|
||||
virtual void Accept(ModelVisitor* const visitor) const {
|
||||
visitor->VisitIntervalVariable(this, "", 0, nullptr);
|
||||
visitor->BeginVisitConstraint("Inverse", this);
|
||||
visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kLeftArgument,
|
||||
left_);
|
||||
visitor->VisitIntegerVariableArrayArgument(ModelVisitor::kRightArgument,
|
||||
right_);
|
||||
visitor->EndVisitConstraint("Inverse", this);
|
||||
}
|
||||
|
||||
private:
|
||||
void PropagateHoles(int index, IntVar* const var, IntVarIterator* const holes,
|
||||
const std::vector<IntVar*>& inverse) {
|
||||
const int64 oldmax =
|
||||
std::min(var->OldMax(), static_cast<int64>(left_.size() - 1));
|
||||
const int64 vmin = var->Min();
|
||||
const int64 vmax = var->Max();
|
||||
for (int64 value = std::max(var->OldMin(), 0LL); value < vmin; ++value) {
|
||||
inverse[value]->RemoveValue(index);
|
||||
}
|
||||
for (holes->Init(); holes->Ok(); holes->Next()) {
|
||||
inverse[holes->Value()]->RemoveValue(index);
|
||||
}
|
||||
for (int64 value = vmax + 1; value <= oldmax; ++value) {
|
||||
inverse[value]->RemoveValue(index);
|
||||
}
|
||||
}
|
||||
|
||||
void PropagateDomain(int index, IntVar* const var,
|
||||
IntVarIterator* const domain,
|
||||
const std::vector<IntVar*>& inverse,
|
||||
std::vector<int64>* const remove) {
|
||||
remove->clear();
|
||||
for (domain->Init(); domain->Ok(); domain->Next()) {
|
||||
const int64 value = domain->Value();
|
||||
if (!inverse[value]->Contains(index)) {
|
||||
remove->push_back(value);
|
||||
}
|
||||
}
|
||||
if (!remove->empty()) {
|
||||
var->RemoveValues(*remove);
|
||||
}
|
||||
}
|
||||
|
||||
std::vector<IntVar*> left_;
|
||||
std::vector<IntVar*> right_;
|
||||
std::vector<IntVarIterator*> left_holes_;
|
||||
std::vector<IntVarIterator*> left_iterators_;
|
||||
std::vector<IntVarIterator*> right_holes_;
|
||||
std::vector<IntVarIterator*> right_iterators_;
|
||||
std::vector<int64> remove_left_;
|
||||
std::vector<int64> remove_right_;
|
||||
};
|
||||
|
||||
// Variable demand cumulative time table
|
||||
|
||||
class VariableCumulativeTask : public BaseObject {
|
||||
public:
|
||||
VariableCumulativeTask(IntVar* const start, IntVar* const duration,
|
||||
IntVar* const demand)
|
||||
: start_(start), duration_(duration), demand_(demand) {}
|
||||
// Copy constructor. Cannot be explicit, because we want to pass instances of
|
||||
// VariableCumulativeTask by copy.
|
||||
VariableCumulativeTask(const VariableCumulativeTask& task)
|
||||
: start_(task.start_), duration_(task.duration_), demand_(task.demand_) {}
|
||||
|
||||
IntVar* start() const { return start_; }
|
||||
IntVar* duration() const { return duration_; }
|
||||
IntVar* demand() const { return demand_; }
|
||||
int64 StartMin() const { return start_->Min(); }
|
||||
int64 StartMax() const { return start_->Max(); }
|
||||
int64 EndMin() const { return start_->Min() + duration_->Min(); }
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("Task{ start: %s, duration: %s, demand: %s }",
|
||||
start_->DebugString().c_str(),
|
||||
duration_->DebugString().c_str(),
|
||||
demand_->DebugString().c_str());
|
||||
}
|
||||
|
||||
private:
|
||||
IntVar* const start_;
|
||||
IntVar* const duration_;
|
||||
IntVar* const demand_;
|
||||
};
|
||||
|
||||
// TODO(user): Take care of overflows.
|
||||
StartVarDurationVarPerformedIntervalVar::
|
||||
StartVarDurationVarPerformedIntervalVar(Solver* const s,
|
||||
IntVar* const var,
|
||||
IntVar* const duration,
|
||||
const std::string& name)
|
||||
: IntervalVar(s, name), start_(var), duration_(duration) {}
|
||||
struct ProfileDelta {
|
||||
ProfileDelta(int64 _time, int64 _delta) : time(_time), delta(_delta) {}
|
||||
int64 time;
|
||||
int64 delta;
|
||||
};
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::StartMin() const {
|
||||
return start_->Min();
|
||||
bool TimeLessThan(const ProfileDelta& delta1, const ProfileDelta& delta2) {
|
||||
return delta1.time < delta2.time;
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::StartMax() const {
|
||||
return start_->Max();
|
||||
bool TaskStartMinLessThan(const VariableCumulativeTask* const task1,
|
||||
const VariableCumulativeTask* const task2) {
|
||||
return (task1->StartMin() < task2->StartMin());
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetStartMin(int64 m) {
|
||||
start_->SetMin(m);
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetStartMax(int64 m) {
|
||||
start_->SetMax(m);
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetStartRange(int64 mi, int64 ma) {
|
||||
start_->SetRange(mi, ma);
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::DurationMin() const {
|
||||
return duration_->Min();
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::DurationMax() const {
|
||||
return duration_->Max();
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetDurationMin(int64 m) {
|
||||
duration_->SetMin(m);
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetDurationMax(int64 m) {
|
||||
duration_->SetMax(m);
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetDurationRange(
|
||||
int64 mi, int64 ma) {
|
||||
duration_->SetRange(mi, ma);
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::EndMin() const {
|
||||
return start_->Min() + duration_->Min();
|
||||
}
|
||||
|
||||
int64 StartVarDurationVarPerformedIntervalVar::EndMax() const {
|
||||
return start_->Max() + duration_->Max();
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetEndMin(int64 m) {
|
||||
start_->SetMin(m - duration_->Max());
|
||||
duration_->SetMin(m - start_->Max());
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetEndMax(int64 m) {
|
||||
start_->SetMax(m - duration_->Min());
|
||||
duration_->SetMax(m - start_->Min());
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetEndRange(int64 mi, int64 ma) {
|
||||
start_->SetRange(mi - duration_->Max(), ma - duration_->Min());
|
||||
duration_->SetRange(mi - start_->Max(), ma - start_->Min());
|
||||
}
|
||||
|
||||
bool StartVarDurationVarPerformedIntervalVar::MustBePerformed() const {
|
||||
return true;
|
||||
}
|
||||
|
||||
bool StartVarDurationVarPerformedIntervalVar::MayBePerformed() const {
|
||||
return true;
|
||||
}
|
||||
|
||||
void StartVarDurationVarPerformedIntervalVar::SetPerformed(bool val) {
|
||||
if (!val) {
|
||||
solver()->Fail();
|
||||
class VariableCumulativeTimeTable : public Constraint {
|
||||
public:
|
||||
VariableCumulativeTimeTable(Solver* const solver,
|
||||
const std::vector<VariableCumulativeTask*>& tasks,
|
||||
IntVar* const capacity)
|
||||
: Constraint(solver), by_start_min_(tasks), capacity_(capacity) {
|
||||
// There may be up to 2 delta's per interval (one on each side),
|
||||
// plus two sentinels
|
||||
const int profile_max_size = 2 * NumTasks() + 2;
|
||||
profile_non_unique_time_.reserve(profile_max_size);
|
||||
profile_unique_time_.reserve(profile_max_size);
|
||||
}
|
||||
}
|
||||
|
||||
std::string StartVarDurationVarPerformedIntervalVar::DebugString() const {
|
||||
std::string out;
|
||||
const std::string& var_name = name();
|
||||
if (!var_name.empty()) {
|
||||
out = var_name + "(start = ";
|
||||
} else {
|
||||
out = "IntervalVar(start = ";
|
||||
virtual void InitialPropagate() {
|
||||
BuildProfile();
|
||||
PushTasks();
|
||||
}
|
||||
StringAppendF(&out, "%s, duration = %s, performed = true)",
|
||||
start_->DebugString().c_str(),
|
||||
duration_->DebugString().c_str());
|
||||
return out;
|
||||
}
|
||||
|
||||
virtual void Post() {
|
||||
Demon* const demon =
|
||||
solver()->MakeDelayedConstraintInitialPropagateCallback(this);
|
||||
for (int i = 0; i < NumTasks(); ++i) {
|
||||
by_start_min_[i]->start()->WhenRange(demon);
|
||||
by_start_min_[i]->duration()->WhenRange(demon);
|
||||
by_start_min_[i]->demand()->WhenRange(demon);
|
||||
}
|
||||
capacity_->WhenRange(demon);
|
||||
}
|
||||
|
||||
int NumTasks() const { return by_start_min_.size(); }
|
||||
|
||||
void Accept(ModelVisitor* const visitor) const {
|
||||
LOG(FATAL) << "Should not be visited";
|
||||
}
|
||||
|
||||
virtual std::string DebugString() const {
|
||||
return StringPrintf("VariableCumulativeTimeTable([%s], capacity = %s)",
|
||||
JoinDebugStringPtr(by_start_min_, ", ").c_str(),
|
||||
capacity_->DebugString().c_str());
|
||||
}
|
||||
|
||||
private:
|
||||
// Build the usage profile. Runs in O(n log n).
|
||||
void BuildProfile() {
|
||||
// Build profile with non unique time
|
||||
profile_non_unique_time_.clear();
|
||||
for (int i = 0; i < NumTasks(); ++i) {
|
||||
const VariableCumulativeTask* task = by_start_min_[i];
|
||||
const int64 start_max = task->StartMax();
|
||||
const int64 end_min = task->EndMin();
|
||||
const int64 demand_min = task->demand()->Min();
|
||||
if (start_max < end_min && demand_min > 0) {
|
||||
profile_non_unique_time_.push_back(
|
||||
ProfileDelta(start_max, +demand_min));
|
||||
profile_non_unique_time_.push_back(ProfileDelta(end_min, -demand_min));
|
||||
}
|
||||
}
|
||||
// Sort
|
||||
std::sort(profile_non_unique_time_.begin(), profile_non_unique_time_.end(),
|
||||
TimeLessThan);
|
||||
// Build profile with unique times
|
||||
profile_unique_time_.clear();
|
||||
profile_unique_time_.push_back(ProfileDelta(kint64min, 0));
|
||||
for (int i = 0; i < profile_non_unique_time_.size(); ++i) {
|
||||
const ProfileDelta& profile_delta = profile_non_unique_time_[i];
|
||||
if (profile_delta.time == profile_unique_time_.back().time) {
|
||||
profile_unique_time_.back().delta += profile_delta.delta;
|
||||
} else {
|
||||
profile_unique_time_.push_back(profile_delta);
|
||||
}
|
||||
}
|
||||
// Re-scan profile to compute min usage, max usage, and check
|
||||
// final usage to be 0.
|
||||
int64 usage = 0;
|
||||
int64 max_required_usage = 0;
|
||||
const int64 max_capacity = capacity_->Max();
|
||||
for (int i = 0; i < profile_unique_time_.size(); ++i) {
|
||||
const ProfileDelta& profile_delta = profile_unique_time_[i];
|
||||
usage += profile_delta.delta;
|
||||
max_required_usage = std::max(max_required_usage, usage);
|
||||
if (usage > max_capacity) {
|
||||
solver()->Fail();
|
||||
}
|
||||
}
|
||||
DCHECK_EQ(0, usage);
|
||||
profile_unique_time_.push_back(ProfileDelta(kint64max, 0));
|
||||
|
||||
// Propagate on capacity.
|
||||
capacity_->SetMin(max_required_usage);
|
||||
}
|
||||
|
||||
// Update the start min for all tasks. Runs in O(n^2) and Omega(n).
|
||||
void PushTasks() {
|
||||
std::sort(by_start_min_.begin(), by_start_min_.end(), TaskStartMinLessThan);
|
||||
int64 usage = 0;
|
||||
int profile_index = 0;
|
||||
for (int task_index = 0; task_index < NumTasks(); ++task_index) {
|
||||
VariableCumulativeTask* const task = by_start_min_[task_index];
|
||||
if (task->duration()->Min() > 0) {
|
||||
while (task->StartMin() > profile_unique_time_[profile_index].time) {
|
||||
DCHECK(profile_index < profile_unique_time_.size());
|
||||
++profile_index;
|
||||
usage += profile_unique_time_[profile_index].delta;
|
||||
}
|
||||
PushTask(task, profile_index, usage);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Push the given task to new_start_min, defined as the smallest integer such
|
||||
// that the profile usage for all tasks, excluding the current one, does not
|
||||
// exceed capacity_ - task->demand()->Min() on the interval
|
||||
// [new_start_min, new_start_min + task->interval()->DurationMin() ).
|
||||
void PushTask(VariableCumulativeTask* const task, int profile_index,
|
||||
int64 usage) {
|
||||
// Init
|
||||
const int64 demand_min = task->demand()->Min();
|
||||
const int64 adjusted_demand = demand_min == 0 ? 1 : demand_min;
|
||||
const bool is_adjusted = demand_min == 0;
|
||||
const int64 residual_capacity = capacity_->Max() - adjusted_demand;
|
||||
const int64 duration_min = task->duration()->Min();
|
||||
const ProfileDelta& first_prof_delta = profile_unique_time_[profile_index];
|
||||
|
||||
int64 new_start_min = task->StartMin();
|
||||
|
||||
DCHECK_GE(first_prof_delta.time, task->StartMin());
|
||||
// The check above is with a '>='. Let's first treat the '>' case
|
||||
if (first_prof_delta.time > task->StartMin()) {
|
||||
// There was no profile delta at a time between interval->StartMin()
|
||||
// (included) and the current one.
|
||||
// As we don't delete delta's of 0 value, this means the current task
|
||||
// does not contribute to the usage before:
|
||||
DCHECK((task->StartMax() >= first_prof_delta.time) ||
|
||||
(task->StartMax() >= task->EndMin()));
|
||||
// The 'usage' given in argument is valid at first_prof_delta.time. To
|
||||
// compute the usage at the start min, we need to remove the last delta.
|
||||
const int64 usage_at_start_min = usage - first_prof_delta.delta;
|
||||
if (usage_at_start_min > residual_capacity) {
|
||||
new_start_min = profile_unique_time_[profile_index].time;
|
||||
}
|
||||
}
|
||||
|
||||
// Influence of current task
|
||||
const int64 start_max = task->StartMax();
|
||||
const int64 end_min = task->EndMin();
|
||||
// TODO(user): remove delta_start and delta_end.
|
||||
ProfileDelta delta_start(start_max, 0);
|
||||
ProfileDelta delta_end(end_min, 0);
|
||||
if (start_max < end_min) {
|
||||
delta_start.delta = +demand_min;
|
||||
delta_end.delta = -demand_min;
|
||||
}
|
||||
while (profile_unique_time_[profile_index].time <
|
||||
duration_min + new_start_min) {
|
||||
const ProfileDelta& profile_delta = profile_unique_time_[profile_index];
|
||||
DCHECK(profile_index < profile_unique_time_.size());
|
||||
// Compensate for current task
|
||||
if (profile_delta.time == delta_start.time) {
|
||||
usage -= delta_start.delta;
|
||||
}
|
||||
if (profile_delta.time == delta_end.time) {
|
||||
usage -= delta_end.delta;
|
||||
}
|
||||
// Increment time
|
||||
++profile_index;
|
||||
DCHECK(profile_index < profile_unique_time_.size());
|
||||
// Does it fit?
|
||||
if (usage > residual_capacity) {
|
||||
new_start_min = profile_unique_time_[profile_index].time;
|
||||
}
|
||||
usage += profile_unique_time_[profile_index].delta;
|
||||
}
|
||||
if (is_adjusted) {
|
||||
if (new_start_min > task->StartMax()) {
|
||||
task->demand()->SetMax(0);
|
||||
}
|
||||
} else {
|
||||
task->start()->SetMin(new_start_min);
|
||||
}
|
||||
}
|
||||
|
||||
typedef std::vector<ProfileDelta> Profile;
|
||||
|
||||
Profile profile_unique_time_;
|
||||
Profile profile_non_unique_time_;
|
||||
std::vector<VariableCumulativeTask*> by_start_min_;
|
||||
IntVar* const capacity_;
|
||||
|
||||
DISALLOW_COPY_AND_ASSIGN(VariableCumulativeTimeTable);
|
||||
};
|
||||
} // namespace
|
||||
|
||||
Constraint* MakeIsBooleanSumInRange(Solver* const solver,
|
||||
@@ -649,12 +784,99 @@ Constraint* MakeIsBooleanSumInRange(Solver* const solver,
|
||||
new IsBooleanSumInRange(solver, variables, range_min, range_max, target));
|
||||
}
|
||||
|
||||
void PostIsBooleanSumInRange(FlatZincModel* const model, CtSpec* const spec,
|
||||
const std::vector<IntVar*>& variables, int64 range_min,
|
||||
int64 range_max, IntVar* const target) {
|
||||
Solver* const solver = model->solver();
|
||||
const int64 size = variables.size();
|
||||
range_min = std::max(0LL, range_min);
|
||||
range_max = std::min(size, range_max);
|
||||
int true_vars = 0;
|
||||
int possible_vars = 0;
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (variables[i]->Max() == 1) {
|
||||
possible_vars++;
|
||||
if (variables[i]->Min() == 1) {
|
||||
true_vars++;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (true_vars > range_max || possible_vars < range_min) {
|
||||
target->SetValue(0);
|
||||
VLOG(2) << " - set target to 0";
|
||||
} else if (true_vars >= range_min && possible_vars <= range_max) {
|
||||
target->SetValue(1);
|
||||
VLOG(2) << " - set target to 1";
|
||||
} else if (FLAGS_use_sat && range_min == size &&
|
||||
AddBoolAndArrayEqVar(model->Sat(), variables, target)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else if (FLAGS_use_sat && range_max == 0 &&
|
||||
AddBoolOrArrayEqVar(model->Sat(), variables,
|
||||
solver->MakeDifference(1, target)->Var())) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == size &&
|
||||
AddBoolOrArrayEqVar(model->Sat(), variables, target)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else {
|
||||
Constraint* const ct = MakeIsBooleanSumInRange(solver, variables, range_min,
|
||||
range_max, target);
|
||||
VLOG(2) << " - posted " << ct->DebugString();
|
||||
model->AddConstraint(spec, ct);
|
||||
}
|
||||
}
|
||||
|
||||
Constraint* MakeBooleanSumInRange(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max) {
|
||||
return solver->RevAlloc(
|
||||
new BooleanSumInRange(solver, variables, range_min, range_max));
|
||||
}
|
||||
void PostBooleanSumInRange(FlatZincModel* const model, CtSpec* const spec,
|
||||
const std::vector<IntVar*>& variables, int64 range_min,
|
||||
int64 range_max) {
|
||||
Solver* const solver = model->solver();
|
||||
const int64 size = variables.size();
|
||||
range_min = std::max(0LL, range_min);
|
||||
range_max = std::min(size, range_max);
|
||||
int true_vars = 0;
|
||||
std::vector<IntVar*> alt;
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (!variables[i]->Bound()) {
|
||||
alt.push_back(variables[i]);
|
||||
} else if (variables[i]->Min() == 1) {
|
||||
true_vars++;
|
||||
}
|
||||
}
|
||||
const int possible_vars = alt.size();
|
||||
range_min -= true_vars;
|
||||
range_max -= true_vars;
|
||||
|
||||
if (range_max < 0 || range_min > possible_vars) {
|
||||
Constraint* const ct = solver->MakeFalseConstraint();
|
||||
VLOG(2) << " - posted " << ct->DebugString();
|
||||
model->AddConstraint(spec, ct);
|
||||
} else if (range_min <= 0 && range_max >= possible_vars) {
|
||||
Constraint* const ct = solver->MakeTrueConstraint();
|
||||
VLOG(2) << " - posted " << ct->DebugString();
|
||||
model->AddConstraint(spec, ct);
|
||||
} else if (FLAGS_use_sat && range_min == 0 && range_max == 1 &&
|
||||
AddAtMostOne(model->Sat(), alt)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else if (FLAGS_use_sat && range_min == 0 && range_max == size - 1 &&
|
||||
AddAtMostNMinusOne(model->Sat(), alt)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == 1 &&
|
||||
AddBoolOrArrayEqualTrue(model->Sat(), alt) &&
|
||||
AddAtMostOne(model->Sat(), alt)) {
|
||||
VLOG(2) << " - posted to sat";
|
||||
} else {
|
||||
Constraint* const ct =
|
||||
MakeBooleanSumInRange(solver, alt, range_min, range_max);
|
||||
VLOG(2) << " - posted " << ct->DebugString();
|
||||
model->AddConstraint(spec, ct);
|
||||
}
|
||||
}
|
||||
|
||||
Constraint* MakeBooleanSumOdd(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables) {
|
||||
return solver->RevAlloc(new BooleanSumOdd(solver, variables));
|
||||
@@ -691,6 +913,25 @@ Constraint* MakeStrongScalProdEquality(Solver* const solver,
|
||||
return solver->MakeAllowedAssignments(variables, tuples);
|
||||
}
|
||||
|
||||
Constraint* MakeInverse(Solver* const solver, const std::vector<IntVar*>& left,
|
||||
const std::vector<IntVar*>& right) {
|
||||
return solver->RevAlloc(new Inverse(solver, left, right));
|
||||
}
|
||||
|
||||
Constraint* MakeVariableCumulative(Solver* const solver,
|
||||
const std::vector<IntVar*>& starts,
|
||||
const std::vector<IntVar*>& durations,
|
||||
const std::vector<IntVar*>& usages,
|
||||
IntVar* const capacity) {
|
||||
std::vector<VariableCumulativeTask*> tasks(starts.size());
|
||||
for (int i = 0; i < starts.size(); ++i) {
|
||||
tasks[i] = solver->RevAlloc(
|
||||
new VariableCumulativeTask(starts[i], durations[i], usages[i]));
|
||||
}
|
||||
return solver->RevAlloc(
|
||||
new VariableCumulativeTimeTable(solver, tasks, capacity));
|
||||
}
|
||||
|
||||
Constraint* MakeVariableOdd(Solver* const s, IntVar* const var) {
|
||||
return s->RevAlloc(new VariableParity(s, var, true));
|
||||
}
|
||||
@@ -698,123 +939,4 @@ Constraint* MakeVariableOdd(Solver* const s, IntVar* const var) {
|
||||
Constraint* MakeVariableEven(Solver* const s, IntVar* const var) {
|
||||
return s->RevAlloc(new VariableParity(s, var, false));
|
||||
}
|
||||
|
||||
Constraint* MakeBoundModulo(Solver* const s, IntVar* const var,
|
||||
IntVar* const mod, int64 residual) {
|
||||
return s->RevAlloc(new BoundModulo(s, var, mod, residual));
|
||||
}
|
||||
|
||||
void PostBooleanSumInRange(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max) {
|
||||
const int64 size = variables.size();
|
||||
range_min = std::max(0LL, range_min);
|
||||
range_max = std::min(size, range_max);
|
||||
int true_vars = 0;
|
||||
std::vector<IntVar*> alt;
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (!variables[i]->Bound()) {
|
||||
alt.push_back(variables[i]);
|
||||
} else if (variables[i]->Min() == 1) {
|
||||
true_vars++;
|
||||
}
|
||||
}
|
||||
const int possible_vars = alt.size();
|
||||
range_min -= true_vars;
|
||||
range_max -= true_vars;
|
||||
|
||||
if (range_max < 0 || range_min > possible_vars) {
|
||||
Constraint* const ct = solver->MakeFalseConstraint();
|
||||
FZVLOG << " - posted " << ct->DebugString() << FZENDL;
|
||||
solver->AddConstraint(ct);
|
||||
} else if (range_min <= 0 && range_max >= possible_vars) {
|
||||
FZVLOG << " - ignore true constraint" << FZENDL;
|
||||
} else if (FLAGS_use_sat && AddSumInRange(sat, alt, range_min, range_max)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 0 && range_max == 1 &&
|
||||
AddAtMostOne(sat, alt)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 0 && range_max == size - 1 &&
|
||||
AddAtMostNMinusOne(sat, alt)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == 1 &&
|
||||
AddBoolOrArrayEqualTrue(sat, alt) && AddAtMostOne(sat, alt)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == possible_vars &&
|
||||
AddBoolOrArrayEqualTrue(sat, alt)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else {
|
||||
Constraint* const ct =
|
||||
MakeBooleanSumInRange(solver, alt, range_min, range_max);
|
||||
FZVLOG << " - posted " << ct->DebugString() << FZENDL;
|
||||
solver->AddConstraint(ct);
|
||||
}
|
||||
}
|
||||
|
||||
void PostIsBooleanSumInRange(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max, IntVar* target) {
|
||||
const int64 size = variables.size();
|
||||
range_min = std::max(0LL, range_min);
|
||||
range_max = std::min(size, range_max);
|
||||
int true_vars = 0;
|
||||
int possible_vars = 0;
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (variables[i]->Max() == 1) {
|
||||
possible_vars++;
|
||||
if (variables[i]->Min() == 1) {
|
||||
true_vars++;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (true_vars > range_max || possible_vars < range_min) {
|
||||
target->SetValue(0);
|
||||
FZVLOG << " - set target to 0" << FZENDL;
|
||||
} else if (true_vars >= range_min && possible_vars <= range_max) {
|
||||
target->SetValue(1);
|
||||
FZVLOG << " - set target to 1" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == size &&
|
||||
AddBoolAndArrayEqVar(sat, variables, target)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_max == 0 &&
|
||||
AddBoolOrArrayEqVar(sat, variables,
|
||||
solver->MakeDifference(1, target)->Var())) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else if (FLAGS_use_sat && range_min == 1 && range_max == size &&
|
||||
AddBoolOrArrayEqVar(sat, variables, target)) {
|
||||
FZVLOG << " - posted to sat" << FZENDL;
|
||||
} else {
|
||||
Constraint* const ct = MakeIsBooleanSumInRange(solver, variables, range_min,
|
||||
range_max, target);
|
||||
FZVLOG << " - posted " << ct->DebugString() << FZENDL;
|
||||
solver->AddConstraint(ct);
|
||||
}
|
||||
}
|
||||
|
||||
void PostIsBooleanSumDifferent(SatPropagator* sat, Solver* solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 value, IntVar* target) {
|
||||
const int64 size = variables.size();
|
||||
if (value == 0) {
|
||||
PostIsBooleanSumInRange(sat, solver, variables, 1, size, target);
|
||||
} else if (value == size) {
|
||||
PostIsBooleanSumInRange(sat, solver, variables, 0, size - 1, target);
|
||||
} else {
|
||||
Constraint* const ct =
|
||||
solver->MakeIsDifferentCstCt(solver->MakeSum(variables), value, target);
|
||||
FZVLOG << " - posted " << ct->DebugString() << FZENDL;
|
||||
solver->AddConstraint(ct);
|
||||
}
|
||||
}
|
||||
|
||||
IntervalVar* MakePerformedIntervalVar(Solver* const solver,
|
||||
IntVar* const start,
|
||||
IntVar* const duration,
|
||||
const std::string& n) {
|
||||
CHECK(start != nullptr);
|
||||
CHECK(duration != nullptr);
|
||||
return solver->RegisterIntervalVar(solver->RevAlloc(
|
||||
new StartVarDurationVarPerformedIntervalVar(solver, start, duration, n)));
|
||||
}
|
||||
|
||||
} // namespace operations_research
|
||||
111
src/old_flatzinc/flatzinc_constraints.h
Normal file
111
src/old_flatzinc/flatzinc_constraints.h
Normal file
@@ -0,0 +1,111 @@
|
||||
// Copyright 2010-2014 Google
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
|
||||
#ifndef OR_TOOLS_FLATZINC_FLATZINC_CONSTRAINTS_H_
|
||||
#define OR_TOOLS_FLATZINC_FLATZINC_CONSTRAINTS_H_
|
||||
|
||||
#include <map>
|
||||
#include <cassert>
|
||||
|
||||
#include "old_flatzinc/parser.h"
|
||||
#include "constraint_solver/constraint_solver.h"
|
||||
|
||||
namespace operations_research {
|
||||
class SatPropagator;
|
||||
bool AddBoolEq(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right);
|
||||
|
||||
bool AddBoolLe(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right);
|
||||
|
||||
bool AddBoolNot(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right);
|
||||
|
||||
bool AddBoolAndArrayEqVar(SatPropagator* const sat, const std::vector<IntVar*>& vars,
|
||||
IntExpr* const target);
|
||||
|
||||
bool AddBoolOrArrayEqVar(SatPropagator* const sat, const std::vector<IntVar*>& vars,
|
||||
IntExpr* const target);
|
||||
|
||||
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);
|
||||
|
||||
bool AddBoolIsNEqVar(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right, IntExpr* const target);
|
||||
|
||||
bool AddBoolIsLeVar(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right, IntExpr* const target);
|
||||
|
||||
bool AddBoolOrEqVar(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right, IntExpr* const target);
|
||||
|
||||
bool AddBoolIsEqVar(SatPropagator* const sat, IntExpr* const left,
|
||||
IntExpr* const right, IntExpr* const target);
|
||||
|
||||
bool AddBoolOrArrayEqualTrue(SatPropagator* const sat,
|
||||
const std::vector<IntVar*>& vars);
|
||||
|
||||
bool AddBoolAndArrayEqualFalse(SatPropagator* const sat,
|
||||
const std::vector<IntVar*>& vars);
|
||||
|
||||
bool AddAtMostOne(SatPropagator* const sat, const std::vector<IntVar*>& vars);
|
||||
|
||||
bool AddAtMostNMinusOne(SatPropagator* const sat, const std::vector<IntVar*>& vars);
|
||||
|
||||
bool AddArrayXor(SatPropagator* const sat, const std::vector<IntVar*>& vars);
|
||||
|
||||
bool DeclareVariable(SatPropagator* const sat, IntVar* const var);
|
||||
|
||||
Constraint* MakeStrongScalProdEquality(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
const std::vector<int64>& coefficients,
|
||||
int64 rhs);
|
||||
|
||||
Constraint* MakeIsBooleanSumInRange(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max,
|
||||
IntVar* const target);
|
||||
|
||||
Constraint* MakeBooleanSumInRange(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables,
|
||||
int64 range_min, int64 range_max);
|
||||
|
||||
Constraint* MakeBooleanSumOdd(Solver* const solver,
|
||||
const std::vector<IntVar*>& variables);
|
||||
|
||||
Constraint* MakeVariableCumulative(Solver* const solver,
|
||||
const std::vector<IntVar*>& starts,
|
||||
const std::vector<IntVar*>& durations,
|
||||
const std::vector<IntVar*>& usages,
|
||||
IntVar* const capacity);
|
||||
|
||||
Constraint* MakeVariableOdd(Solver* const s, IntVar* const var);
|
||||
Constraint* MakeVariableEven(Solver* const s, IntVar* const var);
|
||||
|
||||
void PostIsBooleanSumInRange(FlatZincModel* const model, CtSpec* const spec,
|
||||
const std::vector<IntVar*>& variables, int64 range_min,
|
||||
int64 range_max, IntVar* const target);
|
||||
|
||||
void PostBooleanSumInRange(FlatZincModel* const model, CtSpec* const spec,
|
||||
const std::vector<IntVar*>& variables, int64 range_min,
|
||||
int64 range_max);
|
||||
} // namespace operations_research
|
||||
#endif // OR_TOOLS_FLATZINC_FLATZINC_CONSTRAINTS_H_
|
||||
@@ -1,38 +1,14 @@
|
||||
// Copyright 2010-2014 Google
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
// This is the skeleton for the official flatzinc interpreter. Much
|
||||
// of the funcionnalities are fixed (name of parameters, format of the
|
||||
// input): see http://www.minizinc.org/downloads/doc-1.6/flatzinc-spec.pdf
|
||||
|
||||
#if defined(__GNUC__) // Linux or Mac OS X.
|
||||
#include <signal.h>
|
||||
#endif // __GNUC__
|
||||
|
||||
#include <iostream> // NOLINT
|
||||
#include <string>
|
||||
#include <vector>
|
||||
|
||||
#include <fstream> // NOLINT
|
||||
#include <cstring>
|
||||
#include "base/unique_ptr.h"
|
||||
#include "base/commandlineflags.h"
|
||||
#include "base/commandlineflags.h"
|
||||
#include "base/stringprintf.h"
|
||||
#include "base/integral_types.h"
|
||||
#include "base/logging.h"
|
||||
#include "base/stringprintf.h"
|
||||
#include "base/threadpool.h"
|
||||
#include "base/timer.h"
|
||||
#include "flatzinc2/model.h"
|
||||
#include "flatzinc2/parser.h"
|
||||
#include "flatzinc2/presolve.h"
|
||||
#include "flatzinc2/search.h"
|
||||
#include "flatzinc2/solver.h"
|
||||
#include "old_flatzinc/flatzinc.h"
|
||||
|
||||
DEFINE_int32(log_period, 10000000, "Search log period");
|
||||
DEFINE_bool(all, false, "Search for all solutions");
|
||||
@@ -40,55 +16,43 @@ DEFINE_bool(free, false, "Ignore search annotations");
|
||||
DEFINE_int32(num_solutions, 0, "Number of solution to search for");
|
||||
DEFINE_int32(time_limit, 0, "time limit in ms");
|
||||
DEFINE_int32(workers, 0, "Number of workers");
|
||||
DEFINE_int32(simplex_frequency, 0, "Simplex frequency, 0 = no simplex");
|
||||
DEFINE_bool(use_impact, false, "Use impact based search");
|
||||
DEFINE_double(restart_log_size, -1, "Restart log size for impact search");
|
||||
DEFINE_int32(luby_restart, -1, "Luby restart factor, <= 0 = no luby");
|
||||
DEFINE_int32(heuristic_period, 100, "Period to call heuristics in free search");
|
||||
DEFINE_bool(verbose_impact, false, "Verbose impact");
|
||||
DEFINE_bool(verbose_mt, false, "Verbose Multi-Thread");
|
||||
DEFINE_bool(presolve, true, "Use presolve.");
|
||||
|
||||
DECLARE_bool(fz_logging);
|
||||
DECLARE_bool(log_prefix);
|
||||
DECLARE_bool(use_sat);
|
||||
DECLARE_bool(logging);
|
||||
|
||||
using operations_research::ThreadPool;
|
||||
extern void interrupt_handler(int s);
|
||||
|
||||
namespace operations_research {
|
||||
void Solve(const FzModel* const model, const FzSolverParameters& parameters,
|
||||
FzParallelSupportInterface* parallel_support) {
|
||||
FzSolver solver(*model);
|
||||
CHECK(solver.Extract());
|
||||
solver.Solve(parameters, parallel_support);
|
||||
int Run(const std::string& file, const FlatZincSearchParameters& parameters,
|
||||
FzParallelSupport* const parallel_support) {
|
||||
FlatZincModel fz_model;
|
||||
if (file == "-") {
|
||||
if (!fz_model.Parse(std::cin)) {
|
||||
return -1;
|
||||
}
|
||||
} else {
|
||||
parallel_support->Init(
|
||||
parameters.worker_id,
|
||||
StringPrintf("%%%% model: %s", file.c_str()));
|
||||
if (!fz_model.Parse(file)) {
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
|
||||
fz_model.Solve(parameters, parallel_support);
|
||||
return 0;
|
||||
}
|
||||
|
||||
void SequentialRun(const FzModel* model) {
|
||||
FzSolverParameters parameters;
|
||||
parameters.all_solutions = FLAGS_all;
|
||||
parameters.free_search = FLAGS_free;
|
||||
parameters.heuristic_period = FLAGS_heuristic_period;
|
||||
parameters.ignore_unknown = false;
|
||||
parameters.log_period = FLAGS_log_period;
|
||||
parameters.luby_restart = FLAGS_luby_restart;
|
||||
parameters.num_solutions = FLAGS_num_solutions;
|
||||
parameters.restart_log_size = FLAGS_restart_log_size;
|
||||
parameters.threads = FLAGS_workers;
|
||||
parameters.time_limit_in_ms = FLAGS_time_limit;
|
||||
parameters.use_log = FLAGS_fz_logging;
|
||||
parameters.verbose_impact = FLAGS_verbose_impact;
|
||||
parameters.worker_id = -1;
|
||||
parameters.search_type =
|
||||
FLAGS_use_impact ? FzSolverParameters::IBS : FzSolverParameters::DEFAULT;
|
||||
|
||||
std::unique_ptr<FzParallelSupportInterface> parallel_support(
|
||||
MakeSequentialSupport(FLAGS_all, FLAGS_num_solutions));
|
||||
Solve(model, parameters, parallel_support.get());
|
||||
}
|
||||
|
||||
void ParallelRun(const FzModel* const model, int worker_id,
|
||||
FzParallelSupportInterface* parallel_support) {
|
||||
FzSolverParameters parameters;
|
||||
void ParallelRun(char* const file, int worker_id,
|
||||
FzParallelSupport* const parallel_support) {
|
||||
operations_research::FlatZincSearchParameters parameters;
|
||||
parameters.all_solutions = FLAGS_all;
|
||||
parameters.heuristic_period = FLAGS_heuristic_period;
|
||||
parameters.ignore_unknown = false;
|
||||
@@ -96,6 +60,7 @@ void ParallelRun(const FzModel* const model, int worker_id,
|
||||
parameters.luby_restart = -1;
|
||||
parameters.num_solutions = FLAGS_num_solutions;
|
||||
parameters.random_seed = worker_id * 10;
|
||||
parameters.simplex_frequency = FLAGS_simplex_frequency;
|
||||
parameters.threads = FLAGS_workers;
|
||||
parameters.time_limit_in_ms = FLAGS_time_limit;
|
||||
parameters.use_log = false;
|
||||
@@ -104,34 +69,37 @@ void ParallelRun(const FzModel* const model, int worker_id,
|
||||
switch (worker_id) {
|
||||
case 0: {
|
||||
parameters.free_search = false;
|
||||
parameters.search_type = operations_research::FzSolverParameters::DEFAULT;
|
||||
parameters.search_type =
|
||||
operations_research::FlatZincSearchParameters::DEFAULT;
|
||||
parameters.restart_log_size = -1.0;
|
||||
break;
|
||||
}
|
||||
case 1: {
|
||||
parameters.free_search = true;
|
||||
parameters.search_type =
|
||||
operations_research::FzSolverParameters::MIN_SIZE;
|
||||
operations_research::FlatZincSearchParameters::MIN_SIZE;
|
||||
parameters.restart_log_size = -1.0;
|
||||
break;
|
||||
}
|
||||
case 2: {
|
||||
parameters.free_search = true;
|
||||
parameters.search_type = operations_research::FzSolverParameters::IBS;
|
||||
parameters.search_type =
|
||||
operations_research::FlatZincSearchParameters::IBS;
|
||||
parameters.restart_log_size = FLAGS_restart_log_size;
|
||||
break;
|
||||
}
|
||||
case 3: {
|
||||
parameters.free_search = true;
|
||||
parameters.search_type =
|
||||
operations_research::FzSolverParameters::FIRST_UNBOUND;
|
||||
operations_research::FlatZincSearchParameters::FIRST_UNBOUND;
|
||||
parameters.restart_log_size = -1.0;
|
||||
parameters.heuristic_period = 10000000;
|
||||
break;
|
||||
}
|
||||
case 4: {
|
||||
parameters.free_search = true;
|
||||
parameters.search_type = operations_research::FzSolverParameters::DEFAULT;
|
||||
parameters.search_type =
|
||||
operations_research::FlatZincSearchParameters::DEFAULT;
|
||||
parameters.restart_log_size = -1.0;
|
||||
parameters.heuristic_period = 30;
|
||||
parameters.run_all_heuristics = true;
|
||||
@@ -141,13 +109,40 @@ void ParallelRun(const FzModel* const model, int worker_id,
|
||||
parameters.free_search = true;
|
||||
parameters.search_type =
|
||||
worker_id % 2 == 0
|
||||
? operations_research::FzSolverParameters::RANDOM_MIN
|
||||
: operations_research::FzSolverParameters::RANDOM_MAX;
|
||||
? operations_research::FlatZincSearchParameters::RANDOM_MIN
|
||||
: operations_research::FlatZincSearchParameters::RANDOM_MAX;
|
||||
parameters.restart_log_size = -1.0;
|
||||
parameters.luby_restart = 250;
|
||||
}
|
||||
}
|
||||
Solve(model, parameters, parallel_support);
|
||||
Run(file, parameters, parallel_support);
|
||||
}
|
||||
|
||||
void SequentialRun(char* const file) {
|
||||
FlatZincSearchParameters parameters;
|
||||
parameters.all_solutions = FLAGS_all;
|
||||
parameters.free_search = FLAGS_free;
|
||||
parameters.heuristic_period = FLAGS_heuristic_period;
|
||||
parameters.ignore_unknown = false;
|
||||
parameters.log_period = FLAGS_log_period;
|
||||
parameters.luby_restart = FLAGS_luby_restart;
|
||||
parameters.num_solutions = FLAGS_num_solutions;
|
||||
parameters.restart_log_size = FLAGS_restart_log_size;
|
||||
parameters.simplex_frequency = FLAGS_simplex_frequency;
|
||||
parameters.threads = FLAGS_workers;
|
||||
parameters.time_limit_in_ms = FLAGS_time_limit;
|
||||
parameters.use_log = FLAGS_logging;
|
||||
parameters.verbose_impact = FLAGS_verbose_impact;
|
||||
parameters.worker_id = -1;
|
||||
parameters.search_type =
|
||||
FLAGS_use_impact ? FlatZincSearchParameters::IBS
|
||||
: FlatZincSearchParameters::DEFAULT;
|
||||
|
||||
std::unique_ptr<FzParallelSupport> parallel_support(
|
||||
operations_research::MakeSequentialSupport(parameters.all_solutions,
|
||||
parameters.num_solutions,
|
||||
FLAGS_verbose_mt));
|
||||
Run(file, parameters, parallel_support.get());
|
||||
}
|
||||
|
||||
void FixAndParseParameters(int* argc, char*** argv) {
|
||||
@@ -156,9 +151,7 @@ void FixAndParseParameters(int* argc, char*** argv) {
|
||||
char free_param[] = "--free";
|
||||
char workers_param[] = "--workers";
|
||||
char solutions_param[] = "--num_solutions";
|
||||
char logging_param[] = "--fz_logging";
|
||||
char verbose_param[] = "--fz_verbose";
|
||||
char debug_param[] = "--fz_debug";
|
||||
char logging_param[] = "--logging";
|
||||
for (int i = 1; i < *argc; ++i) {
|
||||
if (strcmp((*argv)[i], "-a") == 0) {
|
||||
(*argv)[i] = all_param;
|
||||
@@ -175,63 +168,8 @@ void FixAndParseParameters(int* argc, char*** argv) {
|
||||
if (strcmp((*argv)[i], "-l") == 0) {
|
||||
(*argv)[i] = logging_param;
|
||||
}
|
||||
if (strcmp((*argv)[i], "-v") == 0) {
|
||||
(*argv)[i] = verbose_param;
|
||||
}
|
||||
if (strcmp((*argv)[i], "-d") == 0) {
|
||||
(*argv)[i] = debug_param;
|
||||
}
|
||||
}
|
||||
google::ParseCommandLineFlags(argc, argv, true);
|
||||
// Fix the number of solutions.
|
||||
if (FLAGS_num_solutions == 0) { // not specified
|
||||
FLAGS_num_solutions = FLAGS_all ? kint32max : 1;
|
||||
}
|
||||
}
|
||||
|
||||
void ParseAndRun(const std::string& filename, int num_workers) {
|
||||
WallTimer timer;
|
||||
timer.Start();
|
||||
std::string problem_name(filename);
|
||||
problem_name.resize(problem_name.size() - 4);
|
||||
size_t found = problem_name.find_last_of("/\\");
|
||||
if (found != std::string::npos) {
|
||||
problem_name = problem_name.substr(found + 1);
|
||||
}
|
||||
FzModel model(problem_name);
|
||||
CHECK(ParseFlatzincFile(filename, &model));
|
||||
FZLOG << "File " << filename << " parsed in " << timer.GetInMs() << " ms"
|
||||
<< FZENDL;
|
||||
FzPresolver presolve;
|
||||
presolve.CleanUpModelForTheCpSolver(&model, FLAGS_use_sat);
|
||||
if (FLAGS_presolve) {
|
||||
FZLOG << "Presolve model" << FZENDL;
|
||||
timer.Reset();
|
||||
timer.Start();
|
||||
presolve.Run(&model);
|
||||
FZLOG << " - done in " << timer.GetInMs() << " ms" << FZENDL;
|
||||
}
|
||||
FzModelStatistics stats(model);
|
||||
stats.PrintStatistics();
|
||||
|
||||
#if defined(__GNUC__)
|
||||
signal (SIGINT, &interrupt_handler);
|
||||
#endif
|
||||
|
||||
if (num_workers == 0) {
|
||||
operations_research::SequentialRun(&model);
|
||||
} else {
|
||||
std::unique_ptr<operations_research::FzParallelSupportInterface>
|
||||
parallel_support(operations_research::MakeMtSupport(
|
||||
FLAGS_all, FLAGS_num_solutions, FLAGS_verbose_mt));
|
||||
{
|
||||
ThreadPool pool("Parallel FlatZinc", num_workers);
|
||||
for (int w = 0; w < num_workers; ++w) {
|
||||
pool.Add(NewCallback(ParallelRun, &model, w, parallel_support.get()));
|
||||
}
|
||||
pool.StartWorkers();
|
||||
}
|
||||
}
|
||||
google::ParseCommandLineFlags( argc, argv, true);
|
||||
}
|
||||
} // namespace operations_research
|
||||
|
||||
@@ -241,6 +179,25 @@ int main(int argc, char** argv) {
|
||||
LOG(ERROR) << "Usage: " << argv[0] << " <file>";
|
||||
exit(EXIT_FAILURE);
|
||||
}
|
||||
operations_research::ParseAndRun(argv[1], FLAGS_workers);
|
||||
return 0;
|
||||
// Fix the number of solutions.
|
||||
if (FLAGS_num_solutions == 0) { // not specified
|
||||
FLAGS_num_solutions = FLAGS_all ? kint32max : 1;
|
||||
}
|
||||
|
||||
if (FLAGS_workers == 0) {
|
||||
operations_research::SequentialRun(argv[1]);
|
||||
} else {
|
||||
std::unique_ptr<operations_research::FzParallelSupport> parallel_support(
|
||||
operations_research::MakeMtSupport(
|
||||
FLAGS_all, FLAGS_num_solutions, FLAGS_verbose_mt));
|
||||
{
|
||||
ThreadPool pool("Parallel FlatZinc", FLAGS_workers);
|
||||
pool.StartWorkers();
|
||||
for (int w = 0; w < FLAGS_workers; ++w) {
|
||||
pool.Add(NewCallback(&operations_research::ParallelRun, argv[1], w,
|
||||
parallel_support.get()));
|
||||
}
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
@@ -21,7 +21,7 @@
|
||||
#include "base/mutex.h"
|
||||
#include "base/stringprintf.h"
|
||||
#include "base/synchronization.h"
|
||||
#include "flatzinc/flatzinc.h"
|
||||
#include "old_flatzinc/flatzinc.h"
|
||||
#include "constraint_solver/constraint_solveri.h"
|
||||
#include "constraint_solver/hybrid.h"
|
||||
|
||||
39
src/old_flatzinc/mznlib/cumulative.mzn
Normal file
39
src/old_flatzinc/mznlib/cumulative.mzn
Normal file
@@ -0,0 +1,39 @@
|
||||
%-----------------------------------------------------------------------------%
|
||||
% Requires that a set of tasks given by start times 's', durations 'd', and
|
||||
% resource requirements 'r', never require more than a global resource bound
|
||||
% 'b' at any one time.
|
||||
% Assumptions:
|
||||
% - forall i, d[i] >= 0 and r[i] >= 0
|
||||
%-----------------------------------------------------------------------------%
|
||||
predicate fixed_cumulative(array[int] of var int: s,
|
||||
array[int] of int: d,
|
||||
array[int] of int: r,
|
||||
int: b);
|
||||
|
||||
predicate var_cumulative(array[int] of var int: s,
|
||||
array[int] of int: d,
|
||||
array[int] of int: r,
|
||||
var int: b);
|
||||
|
||||
predicate variable_cumulative(array[int] of var int: s,
|
||||
array[int] of var int: d,
|
||||
array[int] of var int: r,
|
||||
var int: b);
|
||||
|
||||
predicate cumulative(array[int] of var int: s,
|
||||
array[int] of int: d,
|
||||
array[int] of int: r,
|
||||
int: b) =
|
||||
fixed_cumulative(s, d, r, b);
|
||||
|
||||
predicate cumulative(array[int] of var int: s,
|
||||
array[int] of int: d,
|
||||
array[int] of int: r,
|
||||
var int: b) =
|
||||
var_cumulative(s, d, r, b);
|
||||
|
||||
predicate cumulative(array[int] of var int: s,
|
||||
array[int] of var int: d,
|
||||
array[int] of var int: r,
|
||||
var int: b) =
|
||||
variable_cumulative(s, d, r, b);
|
||||
1978
src/old_flatzinc/parser.cc
Normal file
1978
src/old_flatzinc/parser.cc
Normal file
File diff suppressed because it is too large
Load Diff
1149
src/old_flatzinc/parser.h
Normal file
1149
src/old_flatzinc/parser.h
Normal file
File diff suppressed because it is too large
Load Diff
@@ -40,8 +40,8 @@
|
||||
*/
|
||||
|
||||
#include "base/commandlineflags.h"
|
||||
#include "flatzinc/flatzinc.h"
|
||||
#include "flatzinc/flatzinc_constraints.h"
|
||||
#include "old_flatzinc/flatzinc.h"
|
||||
#include "old_flatzinc/flatzinc_constraints.h"
|
||||
#include "base/mathutil.h"
|
||||
#include "constraint_solver/constraint_solveri.h"
|
||||
#include "util/string_array.h"
|
||||
1167
tools/algorithms.doxy
Normal file
1167
tools/algorithms.doxy
Normal file
File diff suppressed because it is too large
Load Diff
1163
tools/base.doxy
Normal file
1163
tools/base.doxy
Normal file
File diff suppressed because it is too large
Load Diff
1171
tools/constraint_solver.doxy
Normal file
1171
tools/constraint_solver.doxy
Normal file
File diff suppressed because it is too large
Load Diff
408
tools/doxygen_filter.py
Normal file
408
tools/doxygen_filter.py
Normal file
@@ -0,0 +1,408 @@
|
||||
#! /usr/bin/python2.4
|
||||
#
|
||||
# Copyright 2010-2014 Google
|
||||
# Licensed under the Apache License, Version 2.0 (the "License");
|
||||
# you may not use this file except in compliance with the License.
|
||||
# You may obtain a copy of the License at
|
||||
#
|
||||
# http://www.apache.org/licenses/LICENSE-2.0
|
||||
#
|
||||
# Unless required by applicable law or agreed to in writing, software
|
||||
# distributed under the License is distributed on an "AS IS" BASIS,
|
||||
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
# See the License for the specific language governing permissions and
|
||||
# limitations under the License.
|
||||
#
|
||||
# This here steaming pile of Python works as a Doxygen input filter which
|
||||
# automatically translates the C++ code with doxygen /// comments into
|
||||
# the format Doxygen wants, complete
|
||||
|
||||
import re
|
||||
import sys
|
||||
|
||||
# Class which reads from an input file one line at a time and allows you to
|
||||
# match that line against regexes.
|
||||
class Reader:
|
||||
def __init__(self, file):
|
||||
self.file = file
|
||||
self.line = file.readline()
|
||||
|
||||
def Eof(self):
|
||||
return self.line == ""
|
||||
|
||||
def LookingAt(self, pattern):
|
||||
return re.match(pattern, self.line) != None
|
||||
|
||||
def ConsumeAndWrite(self, out):
|
||||
out.write(self.line)
|
||||
self.line = self.file.readline()
|
||||
|
||||
def Consume(self):
|
||||
line = self.line
|
||||
self.line = self.file.readline()
|
||||
return line
|
||||
|
||||
def GetIndent(self):
|
||||
return re.match(" *", self.line).end()
|
||||
|
||||
# If we insert additional lines into the output, we will want to remove lines
|
||||
# somewhere else so that definitions generally appear on the line number they
|
||||
# were on originally. Otherwise, when Doxygen links into the orignial headers,
|
||||
# it links to the wrong line numbers. "offset" counts the number of lines we
|
||||
# need to make up.
|
||||
class OffsetTrackingFile:
|
||||
def __init__(self, file):
|
||||
self.file = file
|
||||
self.offset = 0
|
||||
def write(self, text):
|
||||
self.file.write(text)
|
||||
def writelines(self, lines):
|
||||
self.file.writelines(lines)
|
||||
|
||||
# This class keeps tracks of what member groups we've opened, so that we can
|
||||
# write their end tags later on. Doxygen does not allow nested groups, though
|
||||
# nested classes can have their own groups. Thus, we can keep track of groups
|
||||
# according to their indentation levels.
|
||||
class GroupTracker:
|
||||
def __init__(self):
|
||||
self.levels = []
|
||||
|
||||
# Start a new group indented by the given number of spaces.
|
||||
def StartGroup(self, indent, out):
|
||||
self.EndGroupsDeeperThan(indent - 1, out)
|
||||
out.write(" " * indent + "/// @{\n")
|
||||
out.offset += 1
|
||||
self.levels.append(indent)
|
||||
|
||||
# Write end tags for all open groups who are indented more than the given
|
||||
# number of spaces.
|
||||
def EndGroupsDeeperThan(self, indent, out):
|
||||
while self.levels and self.levels[-1] > indent:
|
||||
out.write(" " * self.levels[-1] + "/// @}\n")
|
||||
out.offset += 1
|
||||
self.levels.pop()
|
||||
|
||||
# Converts a regular comment block into a Doxygen-format comment block and
|
||||
# writes it to the output.
|
||||
#
|
||||
# Other than converting all the "//"s to "///"s, we also try to detect code
|
||||
# fragments embedded inside comments. Throughout the comments in net/proto2,
|
||||
# such fragments are always indented two spaces, e.g. like this:
|
||||
# // Here is a code fragment:
|
||||
# // int foo = Foo();
|
||||
# // // A comment within the code fragment.
|
||||
# // Bar(foo);
|
||||
# // That was a code fragment!
|
||||
# We try to detect this and put the fragment in a @code block so that Doxygen
|
||||
# will format it nicely. However, not everything which is indented is a code
|
||||
# block. Another common case is lists, which look like:
|
||||
# // Here is a list:
|
||||
# // * List item 1.
|
||||
# // This is still part of list item 1.
|
||||
# // Notice the indent.
|
||||
# // * List item 2.
|
||||
# // The list is over now.
|
||||
# So, we want to detect lists and *not* interpret them as code.
|
||||
def FormatDocComment(comment, out):
|
||||
min_indent_for_code = 3
|
||||
in_code = False
|
||||
empty_lines = []
|
||||
for line in comment:
|
||||
# Doxygen gets confused when it sees "*/" inside a // comment and silently
|
||||
# fails to parse anything in the file. Thanks, Doxygen.
|
||||
line = line.replace("*/", "* /")
|
||||
|
||||
# Separate the comment text from the pre-comment indent.
|
||||
(outer_indent, content) = line.split("//", 1)
|
||||
if content.strip() == "":
|
||||
# The line was empty. Buffer it for now.
|
||||
empty_lines.append(outer_indent + "///" + content)
|
||||
continue
|
||||
|
||||
# How many spaces is this line indented *after* the comment start? E.g.
|
||||
# the line " // foo" has a two-space outer indent and a one-space
|
||||
# inner_indent.
|
||||
inner_indent = re.match(" *", content).end()
|
||||
|
||||
if inner_indent >= min_indent_for_code:
|
||||
# Content is indented enough to be a code fragment.
|
||||
if not in_code:
|
||||
# Begin a code block.
|
||||
# Flush empty lines first.
|
||||
out.writelines(empty_lines)
|
||||
empty_lines = []
|
||||
out.write("%s///%s@code\n" %
|
||||
(outer_indent, " " * (min_indent_for_code - 2)))
|
||||
out.offset += 1
|
||||
in_code = True
|
||||
|
||||
# Doxygen takes all the raw bytes between @code and @encode and copies
|
||||
# them directly into the final web page. It does not look for newlines
|
||||
# in this range at all. So, if you have something reasonable like:
|
||||
# /// @code
|
||||
# /// int foo = 1;
|
||||
# /// @endcode
|
||||
# Your code fragment ends up being:
|
||||
# /// int foo = 1;
|
||||
# ///
|
||||
# That is, it includes the stupid "///"s, which obviously aren't supposed
|
||||
# to be part of the fragment. Instead, you have to do:
|
||||
# /// @code
|
||||
# int foo = 1;
|
||||
# @endcode
|
||||
# Which is, of course, totally invalid C++. But luckily we don't need
|
||||
# this to compile as C++. We just need Doxygen to read it.
|
||||
#
|
||||
# Before you ask, yes, I tried doing this:
|
||||
# /** @code
|
||||
# int foo = 1;
|
||||
# @endcode */
|
||||
# For whatever reason, Doxygen didn't like it.
|
||||
out.write("\n" * len(empty_lines))
|
||||
empty_lines = []
|
||||
out.write(content[min_indent_for_code:])
|
||||
else:
|
||||
if in_code:
|
||||
# End a code block. Do not flush empty lines; we don't want to
|
||||
# include them in the block.
|
||||
out.write("@endcode\n")
|
||||
out.offset += 1
|
||||
in_code = False
|
||||
|
||||
# Replace '*' bullet style with '-', since Doxygen only recognizes the
|
||||
# latter.
|
||||
content = re.sub("^( +)[*] ", "\\1- ", content)
|
||||
|
||||
if re.match(" +- ", content):
|
||||
# This line starts a bullet list. Subsequent lines will be indented,
|
||||
# but should not be code.
|
||||
min_indent_for_code = inner_indent + 4
|
||||
elif re.match(".*\\w.*:.*\\w.*$", content):
|
||||
# This line starts a note. Subsequent lines will be indented, but
|
||||
# should not be code.
|
||||
#
|
||||
# Note: "Note" comments look like this. They start with a word
|
||||
# followed by a colon (e.g. "Note:", "TODO(kenton):", etc.). A
|
||||
# line which merely ends with a colon, however, should *not* be
|
||||
# considered a note, because indented code blocks are often
|
||||
# preceeded by such lines.
|
||||
min_indent_for_code = inner_indent + 4
|
||||
else:
|
||||
# Nothing special here. If the next line is indented then we will
|
||||
# put it in a code block.
|
||||
min_indent_for_code = inner_indent + 2
|
||||
|
||||
out.writelines(empty_lines)
|
||||
empty_lines = []
|
||||
out.write(outer_indent + "///" + content)
|
||||
|
||||
if in_code:
|
||||
# End a code block. Do not flush empty lines; we don't want to
|
||||
# include them in the block.
|
||||
out.write("@endcode\n")
|
||||
out.offset += 1
|
||||
# Now flush empty lines.
|
||||
out.writelines(empty_lines)
|
||||
|
||||
# Reads a comment block. Returns a list of lines.
|
||||
def ReadComment(reader):
|
||||
assert reader.LookingAt(" *//")
|
||||
comment = []
|
||||
while (reader.LookingAt(" *//") or
|
||||
reader.LookingAt("#ifndef PROTO2_OPENSOURCE") or
|
||||
reader.LookingAt("#endif // !PROTO2_OPENSOURCE")):
|
||||
if reader.LookingAt(" *//"):
|
||||
comment.append(reader.Consume())
|
||||
else:
|
||||
# Replace PROTO2_OPENSOURCE ifdef with a blank comment line. These
|
||||
# ifdefs are used to hide google-internal parts of doc comments from
|
||||
# the open source release. The directives will actually be stripped
|
||||
# entirely from the released code, so if we're seeing them, then we
|
||||
# must be running against the internal code. This means we should
|
||||
# include the comments they are guarding. We replace it with a
|
||||
# blank comment that is indented equally to the previous comment line.
|
||||
comment.append(" " * comment[-1].index("//") + "//\n")
|
||||
reader.Consume()
|
||||
return comment
|
||||
|
||||
# Reads a comment block and writes it to the output. If the comment appears to
|
||||
# be documenting something, translates it to Doxygen format in the process.
|
||||
def HandleComment(reader, out, group_tracker):
|
||||
if reader.Eof(): return
|
||||
|
||||
comment = ReadComment(reader)
|
||||
|
||||
# Figure out what to do with it.
|
||||
if ((comment[0].count("----") > 0 or comment[0].count("====") > 0) and
|
||||
comment[0].startswith(" ")):
|
||||
# The comment is a divider. Put everything under it into a group.
|
||||
group_tracker.StartGroup(comment[0].index("//"), out)
|
||||
|
||||
# Remove the -'s and ='s.
|
||||
comment[0] = comment[0].rstrip(" -=\r\n") + "\n";
|
||||
if comment[0] == "//":
|
||||
# The first line is entirely composed of -'s or ='s. Remove it.
|
||||
comment = comment[1:]
|
||||
# We know the offset is at least 1 from the StartGroup() call, so we
|
||||
# should be able to decrement it.
|
||||
assert out.offset > 0
|
||||
out.offset -= 1
|
||||
else:
|
||||
comment[0] = comment[0].replace("//", "// @name")
|
||||
|
||||
# If the comment is non-empty, we want to write it even if it is not
|
||||
# followed by any content, since it documents the group.
|
||||
if comment:
|
||||
FormatDocComment(comment, out)
|
||||
# We need to ensure there is a blank line here so that the group's
|
||||
# doc comment doesn't run up against the doc comment for the first thing
|
||||
# in it.
|
||||
out.write("\n")
|
||||
out.offset += 1
|
||||
elif (# A line with alphanumeric characters is considered to be content.
|
||||
reader.LookingAt(".*\\w.*") and
|
||||
# Unless all the characters are in a comment.
|
||||
not reader.LookingAt("\\W*//") and
|
||||
# Also, class forward-declarations, namespace decls, and preprocessor
|
||||
# directives should not be documented.
|
||||
not reader.LookingAt(" *class +\\w+ *;") and
|
||||
not reader.LookingAt(" *namespace +\\w+ *{") and
|
||||
not reader.LookingAt(" *#") and
|
||||
# And neither should inline method definitions declared outside
|
||||
# the class definition.
|
||||
not reader.LookingAt("[^ ].*\w+::\w+ *\\(\\)")):
|
||||
# Line contains content. Transform the comment into a doc comment and
|
||||
# write it.
|
||||
if reader.LookingAt(".*typedef"):
|
||||
# If a group contains a typedef, Doxygen annoyingly places that group
|
||||
# above all other groups, rather than placing it in declaration order
|
||||
# like normal. So, don't let typedefs be in groups.
|
||||
group_tracker.EndGroupsDeeperThan(reader.GetIndent() - 1, out)
|
||||
FormatDocComment(comment, out)
|
||||
else:
|
||||
# No content. The comment is not a doc comment. Just write it. But try
|
||||
# to make up some offset lines while we're here.
|
||||
if out.offset >= len(comment):
|
||||
# The comment is shorter than the offset, so don't write it at all.
|
||||
out.offset -= len(comment)
|
||||
else:
|
||||
out.writelines(comment[out.offset:])
|
||||
out.offset = 0
|
||||
|
||||
# Skips code lines until a comment block is encountered.
|
||||
def FindNextComment(reader, out, group_tracker):
|
||||
while not reader.LookingAt(" *//") and not reader.Eof():
|
||||
if (reader.LookingAt(".*[^ \n].*$") and
|
||||
not reader.LookingAt(" *#")):
|
||||
# This line containts some sort of content. End any groups which had
|
||||
# deeper indentation levels than this line.
|
||||
group_tracker.EndGroupsDeeperThan(reader.GetIndent(), out)
|
||||
|
||||
# By default, Doxygen puts class members into implicit groups like
|
||||
# "Public Member Functions" and "Public Fields". This script sometimes
|
||||
# produces explicit groups as well, in order to improve organization.
|
||||
# Unfortunately, Doxygen does not handle things very well when some things
|
||||
# are explicitly grouped and some aren't. In particular:
|
||||
# * If the SUBGROUPING option is on, then the explicit groups will be
|
||||
# nested within the implicit ones, but *only if* all members of the group
|
||||
# belong in the same implicit group (e.g. they are all methods, or all
|
||||
# fields, etc.). If you make an explicit group that crosses multiple
|
||||
# implicit groups, the explicit group becomes a top-level group and
|
||||
# sits along side the implicit ones. This is really confusing, because
|
||||
# it makes it look like these groups are different from the ones that
|
||||
# are nested.
|
||||
# * If the SUBGROUPING option is off, then explicit groups always appear
|
||||
# as peers to the implicit ones. Unfortunately, the explicit groups
|
||||
# seem to appear *above* the implicit ones, even if the members in the
|
||||
# implicit group are all defined before the explicit group.
|
||||
# Unfortunately, methods which are not in any particular group are almost
|
||||
# always more important than methods that are in groups, and thus
|
||||
# should appear first.
|
||||
# The only way we can solve both of these problems without giving up on
|
||||
# groups altogether is to force *all* members to be in explicit groups.
|
||||
# So, we start a group called "General Members" immediately after the
|
||||
# "public:" line to pick up ungrouped stuff.
|
||||
is_public_line = False
|
||||
public_line_indent = 0
|
||||
if reader.LookingAt(" *public:"):
|
||||
is_public_line = True
|
||||
public_line_indent = reader.GetIndent() + 1
|
||||
|
||||
if (reader.LookingAt(".*\\w.*//") and
|
||||
not reader.LookingAt(" *namespace ") and
|
||||
not reader.LookingAt(" *class +\\w+ *;") and
|
||||
not reader.LookingAt(" *#")):
|
||||
# This line has some content followed by a line comment, e.g.:
|
||||
# FOO, // The FOO enum value.
|
||||
# We want to convert the comment into a post-declaration comment, like:
|
||||
# FOO, ///< The FOO enum value.
|
||||
line = reader.Consume()
|
||||
out.write(line.replace("//", "///<", 1))
|
||||
# If subsequent lines have comments that are lined up with this one
|
||||
# and only whitespace before those comments, they must be part of this
|
||||
# comment.
|
||||
indent = line.index("//")
|
||||
while reader.LookingAt(" " * indent + "//"):
|
||||
out.write(reader.Consume().replace("//", "///<", 1))
|
||||
elif reader.LookingAt(".*ATTRIBUTE_ALWAYS_INLINE"):
|
||||
# Hide this from Doxygen. Otherwise it actually documents its presence,
|
||||
# which looks confusing.
|
||||
out.write(reader.Consume().replace("ATTRIBUTE_ALWAYS_INLINE", ""))
|
||||
elif out.offset > 0 and reader.LookingAt(" *$"):
|
||||
# Skip empty line to make up an offset line.
|
||||
out.offset -= 1
|
||||
reader.Consume()
|
||||
else:
|
||||
# Normal line; just print it.
|
||||
reader.ConsumeAndWrite(out)
|
||||
|
||||
# See the monstrous comment earlier in this function.
|
||||
if is_public_line:
|
||||
group_tracker.StartGroup(public_line_indent, out)
|
||||
out.write(" " * public_line_indent + "/// @name General Members\n\n")
|
||||
out.offset += 2
|
||||
|
||||
# Read the entire file and convert it to Doxygen format.
|
||||
def HandleFile(reader, out):
|
||||
out = OffsetTrackingFile(out)
|
||||
|
||||
if reader.LookingAt(".*[cC]opyright.*"):
|
||||
# Skip copyright comment.
|
||||
while reader.LookingAt("//..+$"):
|
||||
reader.ConsumeAndWrite(out)
|
||||
# Skip blank lines after copyright.
|
||||
while reader.LookingAt("//$"):
|
||||
reader.ConsumeAndWrite(out)
|
||||
|
||||
# Read the file-level docs.
|
||||
file_comment = []
|
||||
if (reader.LookingAt("//")):
|
||||
file_comment = ReadComment(reader)
|
||||
|
||||
# Write the file-level docs as a Doxygen comment. Even if the file had no
|
||||
# top-level comment, we want to write an empty Doxygen file comment.
|
||||
# Otherwise, Doxygen will not generate a page listing the contents of this
|
||||
# file, even if the contents are themselves documented. Silly Doxygen.
|
||||
out.write("/// @file\n")
|
||||
out.offset += 1
|
||||
if file_comment:
|
||||
FormatDocComment(file_comment, out)
|
||||
|
||||
# Loop through the rest of the file.
|
||||
group_tracker = GroupTracker()
|
||||
while not reader.Eof():
|
||||
FindNextComment(reader, out, group_tracker)
|
||||
HandleComment(reader, out, group_tracker)
|
||||
|
||||
# Doxygen expects an input filter to take the source file name as a
|
||||
# command-line argument and write the filtered text to stdout.
|
||||
if len(sys.argv) == 1:
|
||||
# No arguments given. Read from stdin. Useful for debugging.
|
||||
HandleFile(Reader(sys.stdin), sys.stdout)
|
||||
else:
|
||||
for filename in sys.argv[1:]:
|
||||
f = file(filename, "r")
|
||||
try:
|
||||
HandleFile(Reader(f), sys.stdout)
|
||||
finally:
|
||||
f.close()
|
||||
1172
tools/fz.doxy
Normal file
1172
tools/fz.doxy
Normal file
File diff suppressed because it is too large
Load Diff
1167
tools/glop.doxy
Normal file
1167
tools/glop.doxy
Normal file
File diff suppressed because it is too large
Load Diff
1166
tools/graph.doxy
Normal file
1166
tools/graph.doxy
Normal file
File diff suppressed because it is too large
Load Diff
1170
tools/linear_solver.doxy
Normal file
1170
tools/linear_solver.doxy
Normal file
File diff suppressed because it is too large
Load Diff
1166
tools/lp_data.doxy
Normal file
1166
tools/lp_data.doxy
Normal file
File diff suppressed because it is too large
Load Diff
1163
tools/util.doxy
Normal file
1163
tools/util.doxy
Normal file
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user