1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 2 3 /* 4 * Main authors: 5 * Jip J. Dekker <jip.dekker@monash.edu> 6 */ 7 8 /* This Source Code Form is subject to the terms of the Mozilla Public 9 * License, v. 2.0. If a copy of the MPL was not distributed with this 10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ 11 12 #pragma once 13 14 #include <minizinc/model.hh> 15 16 #include <map> 17 18 namespace MiniZinc { 19 20 class ChainCompressor { 21 public: ChainCompressor(EnvI & env,Model & m,std::vector<VarDecl * > & deletedVarDecls)22 ChainCompressor(EnvI& env, Model& m, std::vector<VarDecl*>& deletedVarDecls) 23 : _env(env), _m(m), _deletedVarDecls(deletedVarDecls){}; 24 25 virtual bool trackItem(Item* i) = 0; 26 27 virtual void compress() = 0; 28 29 protected: 30 EnvI& _env; 31 Model& _m; 32 std::vector<VarDecl*>& _deletedVarDecls; 33 34 std::multimap<VarDecl*, Item*> _items; 35 typedef std::multimap<VarDecl*, Item*>::iterator iterator; 36 storeItem(VarDecl * v,Item * i)37 void storeItem(VarDecl* v, Item* i) { _items.emplace(v, i); } 38 39 void updateCount(); 40 count(VarDecl * v)41 unsigned long count(VarDecl* v) { return _items.count(v); } 42 find(VarDecl * v)43 std::pair<iterator, iterator> find(VarDecl* v) { return _items.equal_range(v); }; 44 45 void removeItem(Item* i); 46 int addItem(Item* i); 47 48 // Replaces the Nth argument of a Call c by Expression e, c must be located on Item i 49 void replaceCallArgument(Item* i, Call* c, unsigned int n, Expression* e); 50 }; 51 52 class ImpCompressor : public ChainCompressor { 53 public: ImpCompressor(EnvI & env,Model & m,std::vector<VarDecl * > & deletedVarDecls,std::vector<int> & boolConstraints0)54 ImpCompressor(EnvI& env, Model& m, std::vector<VarDecl*>& deletedVarDecls, 55 std::vector<int>& boolConstraints0) 56 : ChainCompressor(env, m, deletedVarDecls), _boolConstraints(boolConstraints0){}; 57 58 bool trackItem(Item* i) override; 59 60 void compress() override; 61 62 protected: 63 std::vector<int>& _boolConstraints; 64 65 // Compress two implications. e.g. (x -> y) /\ (y -> z) => x -> z 66 // In this case i: (y -> z), newLHS: x 67 // Function returns true if compression was successful (and the implication that contains newLHS 68 // can be removed) Side effect: Item i might be removed. 69 bool compressItem(Item* i, VarDecl* newLHS); 70 71 // Constructs a clause constraint item with pos and neg as parameters. 72 // if pos/neg are not ArrayLit then they will inserted into an ArrayLit. 73 ConstraintI* constructClause(Expression* pos, Expression* neg); 74 75 ConstraintI* constructHalfReif(Call* call, Id* control); 76 }; 77 78 class LECompressor : public ChainCompressor { 79 public: LECompressor(EnvI & env,Model & m,std::vector<VarDecl * > & deletedVarDecls)80 LECompressor(EnvI& env, Model& m, std::vector<VarDecl*>& deletedVarDecls) 81 : ChainCompressor(env, m, deletedVarDecls){}; 82 83 bool trackItem(Item* i) override; 84 85 void compress() override; 86 87 protected: 88 std::map<VarDecl*, VarDecl*> _aliasMap; 89 90 /// Replace the use a variable within an inequality 91 /// e.g. i: int_lin_le([1,2,3], [a,b,c], 10), oldVar: a, newVar d -> int_lin_le([1,2,3], [d,b,c], 92 /// 10) Occurrence count is updated for variables involved. 93 template <class Lit> 94 void leReplaceVar(Item* i, VarDecl* oldVar, VarDecl* newVar); 95 96 /// Check if the bounds of two Variables are equal 97 bool eqBounds(Expression* a, Expression* b); 98 }; 99 100 } // namespace MiniZinc 101