Something went wrong. Try again.
This repository has no description
Something went wrong. Try again.
71 kB · 1750 lines
C++
at develop
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373137413751376137713781379138013811382138313841385138613871388138913901391139213931394139513961397139813991400140114021403140414051406140714081409141014111412141314141415141614171418141914201421142214231424142514261427142814291430143114321433143414351436143714381439144014411442144314441445144614471448144914501451145214531454145514561457145814591460146114621463146414651466146714681469147014711472147314741475147614771478147914801481148214831484148514861487148814891490149114921493149414951496149714981499150015011502150315041505150615071508150915101511151215131514151515161517151815191520152115221523152415251526152715281529153015311532153315341535153615371538153915401541154215431544154515461547154815491550155115521553155415551556155715581559156015611562156315641565156615671568156915701571157215731574157515761577157815791580158115821583158415851586158715881589159015911592159315941595159615971598159916001601160216031604160516061607160816091610161116121613161416151616161716181619162016211622162316241625162616271628162916301631163216331634163516361637163816391640164116421643164416451646164716481649165016511652165316541655165616571658165916601661166216631664166516661667166816691670167116721673167416751676167716781679168016811682168316841685168616871688168916901691169216931694169516961697169816991700170117021703170417051706170717081709171017111712171317141715171617171718171917201721172217231724172517261727172817291730173117321733173417351736173717381739174017411742174317441745174617471748174917501751/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/* * Main authors: * Guido Tack <guido.tack@monash.edu> */
/* This Source Code Form is subject to the terms of the Mozilla Public * License, v. 2.0. If a copy of the MPL was not distributed with this * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
#include <minizinc/astiterator.hh>#include <minizinc/chain_compressor.hh>#include <minizinc/eval_par.hh>#include <minizinc/flatten.hh>#include <minizinc/flatten_internal.hh>#include <minizinc/hash.hh>#include <minizinc/optimize.hh>#include <minizinc/optimize_constraints.hh>#include <minizinc/prettyprinter.hh>
#include <deque>#include <vector>
namespace MiniZinc {
void VarOccurrences::addIndex(VarDeclI* i, int idx_i) { idx.insert(i->e()->id(), idx_i); }void VarOccurrences::addIndex(VarDecl* e, int idx_i) { assert(find(e) == -1); idx.insert(e->id(), idx_i);}int VarOccurrences::find(VarDecl* vd) { auto it = idx.find(vd->id()); return it == idx.end() ? -1 : it->second;}void VarOccurrences::remove(VarDecl* vd) { idx.remove(vd->id()); }
void VarOccurrences::add(VarDecl* v, Item* i) { auto vi = itemMap.find(v->id()->decl()->id()); if (vi == itemMap.end()) { Items items; items.insert(i); itemMap.insert(v->id()->decl()->id(), items); } else { vi->second.insert(i); }}
int VarOccurrences::remove(VarDecl* v, Item* i) { auto vi = itemMap.find(v->id()->decl()->id()); assert(vi != itemMap.end()); vi->second.erase(i); return static_cast<int>(vi->second.size());}
void VarOccurrences::removeAllOccurrences(VarDecl* v) { auto vi = itemMap.find(v->id()->decl()->id()); assert(vi != itemMap.end()); vi->second.clear();}
void VarOccurrences::unify(EnvI& env, Model* m, Id* id0_0, Id* id1_0) { Id* id0 = id0_0->decl()->id(); Id* id1 = id1_0->decl()->id();
VarDecl* v0 = id0->decl(); VarDecl* v1 = id1->decl();
if (v0 == v1) { return; }
int v0idx = find(v0); assert(v0idx != -1); (*env.flat())[v0idx]->remove();
auto vi0 = itemMap.find(v0->id()); if (vi0 != itemMap.end()) { auto vi1 = itemMap.find(v1->id()); if (vi1 == itemMap.end()) { itemMap.insert(v1->id(), vi0->second); } else { vi1->second.insert(vi0->second.begin(), vi0->second.end()); } itemMap.remove(v0->id()); }
remove(v0); id0->redirect(id1);}
void VarOccurrences::clear() { itemMap.clear(); idx.clear();}
int VarOccurrences::occurrences(VarDecl* v) { auto vi = itemMap.find(v->id()->decl()->id()); return (vi == itemMap.end() ? 0 : static_cast<int>(vi->second.size()));}
std::pair<int, bool> VarOccurrences::usages(VarDecl* v) { bool is_output = v->ann().contains(constants().ann.output_var) || v->ann().containsCall(constants().ann.output_array); auto vi = itemMap.find(v->id()->decl()->id()); if (vi == itemMap.end()) { return std::make_pair(0, is_output); } int count = 0; for (Item* i : vi->second) { auto* vd = i->dynamicCast<VarDeclI>(); if ((vd != nullptr) && (vd->e() != nullptr) && (vd->e()->e() != nullptr) && (vd->e()->e()->isa<ArrayLit>() || vd->e()->e()->isa<SetLit>())) { auto u = usages(vd->e()); is_output = is_output || u.second; count += u.first; } else { count++; } } return std::make_pair(count, is_output);}
void CollectOccurrencesI::vVarDeclI(VarDeclI* v) { CollectOccurrencesE ce(vo, v); top_down(ce, v->e());}void CollectOccurrencesI::vConstraintI(ConstraintI* ci) { CollectOccurrencesE ce(vo, ci); top_down(ce, ci->e()); for (ExpressionSetIter it = ci->e()->ann().begin(); it != ci->e()->ann().end(); ++it) { top_down(ce, *it); }}void CollectOccurrencesI::vSolveI(SolveI* si) { CollectOccurrencesE ce(vo, si); top_down(ce, si->e()); for (ExpressionSetIter it = si->ann().begin(); it != si->ann().end(); ++si) { top_down(ce, *it); }}
bool is_output(VarDecl* vd) { for (ExpressionSetIter it = vd->ann().begin(); it != vd->ann().end(); ++it) { if (*it != nullptr) { if (*it == constants().ann.output_var) { return true; } if (Call* c = (*it)->dynamicCast<Call>()) { if (c->id() == constants().ann.output_array) { return true; } } } } return false;}
void unify(EnvI& env, std::vector<VarDecl*>& deletedVarDecls, Id* id0, Id* id1) { if (id0->decl() != id1->decl()) { if (is_output(id0->decl())) { std::swap(id0, id1); }
if (id0->decl()->e() != nullptr && !Expression::equal(id0->decl()->e(), id1->decl()->id())) { Expression* rhs = id0->decl()->e();
auto* vdi1 = (*env.flat())[env.varOccurrences.find(id1->decl())]->cast<VarDeclI>(); CollectOccurrencesE ce(env.varOccurrences, vdi1); top_down(ce, rhs);
id1->decl()->e(rhs); id0->decl()->e(nullptr);
auto* vdi0 = (*env.flat())[env.varOccurrences.find(id0->decl())]->cast<VarDeclI>(); CollectDecls cd(env.varOccurrences, deletedVarDecls, vdi0); top_down(cd, rhs); } if (Expression::equal(id1->decl()->e(), id0->decl()->id())) { auto* vdi1 = (*env.flat())[env.varOccurrences.find(id1->decl())]->cast<VarDeclI>(); CollectDecls cd(env.varOccurrences, deletedVarDecls, vdi1); Expression* rhs = id1->decl()->e(); top_down(cd, rhs); id1->decl()->e(nullptr); } // Compute intersection of domains if (id0->decl()->ti()->domain() != nullptr) { if (id1->decl()->ti()->domain() != nullptr) { if (id0->type().isint() || id0->type().isIntSet()) { IntSetVal* isv0 = eval_intset(env, id0->decl()->ti()->domain()); IntSetVal* isv1 = eval_intset(env, id1->decl()->ti()->domain()); IntSetRanges isv0r(isv0); IntSetRanges isv1r(isv1); Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> inter(isv0r, isv1r); IntSetVal* nd = IntSetVal::ai(inter); if (nd->size() == 0) { env.fail(); } else if (nd->card() != isv1->card()) { id1->decl()->ti()->domain(new SetLit(Location(), nd)); if (nd->card() == isv0->card()) { id1->decl()->ti()->setComputedDomain(id0->decl()->ti()->computedDomain()); } else { id1->decl()->ti()->setComputedDomain(false); } } } else if (id0->type().isbool()) { if (eval_bool(env, id0->decl()->ti()->domain()) != eval_bool(env, id1->decl()->ti()->domain())) { env.fail(); } } else { // float FloatSetVal* isv0 = eval_floatset(env, id0->decl()->ti()->domain()); FloatSetVal* isv1 = eval_floatset(env, id1->decl()->ti()->domain()); FloatSetRanges isv0r(isv0); FloatSetRanges isv1r(isv1); Ranges::Inter<FloatVal, FloatSetRanges, FloatSetRanges> inter(isv0r, isv1r); FloatSetVal* nd = FloatSetVal::ai(inter);
FloatSetRanges nd_r(nd); FloatSetRanges isv1r_2(isv1);
if (nd->size() == 0) { env.fail(); } else if (!Ranges::equal(nd_r, isv1r_2)) { id1->decl()->ti()->domain(new SetLit(Location(), nd)); FloatSetRanges nd_r_2(nd); FloatSetRanges isv0r_2(isv0); if (Ranges::equal(nd_r_2, isv0r_2)) { id1->decl()->ti()->setComputedDomain(id0->decl()->ti()->computedDomain()); } else { id1->decl()->ti()->setComputedDomain(false); } } }
} else { id1->decl()->ti()->domain(id0->decl()->ti()->domain()); } }
// If both variables are output variables, unify them in the output model if (is_output(id0->decl())) { assert(env.outputFlatVarOccurrences.find(id0->decl()) != -1); VarDecl* id0_output = (*env.output)[env.outputFlatVarOccurrences.find(id0->decl())]->cast<VarDeclI>()->e(); assert(env.outputFlatVarOccurrences.find(id1->decl()) != -1); VarDecl* id1_output = (*env.output)[env.outputFlatVarOccurrences.find(id1->decl())]->cast<VarDeclI>()->e(); if (id0_output->e() == nullptr) { id0_output->e(id1_output->id()); } }
env.varOccurrences.unify(env, env.flat(), id0, id1); }}
void substitute_fixed_vars(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls);void simplify_bool_constraint(EnvI& env, Item* ii, VarDecl* vd, bool& remove, std::deque<unsigned int>& vardeclQueue, std::deque<Item*>& constraintQueue, std::vector<Item*>& toRemove, std::vector<VarDecl*>& deletedVarDecls, std::unordered_map<Expression*, int>& nonFixedLiteralCount);
bool simplify_constraint(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls, std::deque<Item*>& constraintQueue, std::deque<unsigned int>& vardeclQueue);
void push_vardecl(EnvI& env, VarDeclI* vdi, unsigned int vd_idx, std::deque<unsigned int>& q) { if (!vdi->removed() && !vdi->flag()) { vdi->flag(true); q.push_back(vd_idx); }}void push_vardecl(EnvI& env, unsigned int vd_idx, std::deque<unsigned int>& q) { push_vardecl(env, (*env.flat())[vd_idx]->cast<VarDeclI>(), vd_idx, q);}
void push_dependent_constraints(EnvI& env, Id* id, std::deque<Item*>& q) { auto it = env.varOccurrences.itemMap.find(id->decl()->id()); if (it != env.varOccurrences.itemMap.end()) { for (auto* item : it->second) { if (auto* ci = item->dynamicCast<ConstraintI>()) { if (!ci->removed() && !ci->flag()) { ci->flag(true); q.push_back(ci); } } else if (auto* vdi = item->dynamicCast<VarDeclI>()) { if (vdi->e()->id()->decl() != vdi->e()) { vdi = (*env.flat())[env.varOccurrences.find(vdi->e()->id()->decl())]->cast<VarDeclI>(); } if (!vdi->removed() && !vdi->flag() && (vdi->e()->e() != nullptr)) { vdi->flag(true); q.push_back(vdi); } } } }}
void optimize(Env& env, bool chain_compression) { if (env.envi().failed()) { return; } try { EnvI& envi = env.envi(); Model& m = *envi.flat(); std::vector<int> toAssignBoolVars; std::vector<int> toRemoveConstraints; std::vector<VarDecl*> deletedVarDecls;
// Queue of constraint and variable items that still need to be optimised std::deque<Item*> constraintQueue; // Queue of variable declarations (indexes into the model) that still need to be optimised std::deque<unsigned int> vardeclQueue;
std::vector<int> boolConstraints;
GCLock lock;
// Phase 0: clean up // - clear flags for all constraint and variable declaration items // (flags are used to indicate whether an item is already queued or not) for (auto& i : m) { if (!i->removed()) { if (auto* ci = i->dynamicCast<ConstraintI>()) { ci->flag(false); } else if (auto* vdi = i->dynamicCast<VarDeclI>()) { vdi->flag(false); } } }
// Phase 1: initialise queues // - remove equality constraints between identifiers // - remove toplevel forall constraints // - collect exists, clauses and reified foralls in boolConstraints // - remove "constraint x" where x is a bool var // - unify variables that are assigned to an identifier // - push bool vars that are fixed and have a RHS (to propagate the RHS constraint) // - push int vars that are fixed (either have a RHS or a singleton domain) for (unsigned int i = 0; i < m.size(); i++) { if (m[i]->removed()) { continue; } if (auto* ci = m[i]->dynamicCast<ConstraintI>()) { ci->flag(false); if (!ci->removed()) { if (Call* c = ci->e()->dynamicCast<Call>()) { if ((c->id() == constants().ids.int_.eq || c->id() == constants().ids.bool_eq || c->id() == constants().ids.float_.eq || c->id() == constants().ids.set_eq) && c->arg(0)->isa<Id>() && c->arg(1)->isa<Id>() && (c->arg(0)->cast<Id>()->decl()->e() == nullptr || c->arg(1)->cast<Id>()->decl()->e() == nullptr)) { // Equality constraint between two identifiers: unify
if (Call* defVar = c->ann().getCall(constants().ann.defines_var)) { // First, remove defines_var/is_defined_var annotations if present if (Expression::equal(defVar->arg(0), c->arg(0))) { c->arg(0)->cast<Id>()->decl()->ann().remove(constants().ann.is_defined_var); } else { c->arg(1)->cast<Id>()->decl()->ann().remove(constants().ann.is_defined_var); } } unify(envi, deletedVarDecls, c->arg(0)->cast<Id>(), c->arg(1)->cast<Id>()); { VarDecl* vd = c->arg(0)->cast<Id>()->decl(); int v0idx = envi.varOccurrences.find(vd); push_vardecl(envi, m[v0idx]->cast<VarDeclI>(), v0idx, vardeclQueue); }
push_dependent_constraints(envi, c->arg(0)->cast<Id>(), constraintQueue); CollectDecls cd(envi.varOccurrences, deletedVarDecls, ci); top_down(cd, c); ci->e(constants().literalTrue); ci->remove(); } else if (c->id() == constants().ids.int_.lin_eq && Expression::equal(c->arg(2), IntLit::a(0))) { auto* al_c = follow_id(c->arg(0))->cast<ArrayLit>(); if (al_c->size() == 2 && (*al_c)[0]->cast<IntLit>()->v() == -(*al_c)[1]->cast<IntLit>()->v()) { auto* al_x = follow_id(c->arg(1))->cast<ArrayLit>(); if ((*al_x)[0]->isa<Id>() && (*al_x)[1]->isa<Id>() && ((*al_x)[0]->cast<Id>()->decl()->e() == nullptr || (*al_x)[1]->cast<Id>()->decl()->e() == nullptr)) { // Equality constraint between two identifiers: unify
if (Call* defVar = c->ann().getCall(constants().ann.defines_var)) { // First, remove defines_var/is_defined_var annotations if present if (Expression::equal(defVar->arg(0), (*al_x)[0])) { (*al_x)[0]->cast<Id>()->decl()->ann().remove(constants().ann.is_defined_var); } else { (*al_x)[1]->cast<Id>()->decl()->ann().remove(constants().ann.is_defined_var); } } unify(envi, deletedVarDecls, (*al_x)[0]->cast<Id>(), (*al_x)[1]->cast<Id>()); { VarDecl* vd = (*al_x)[0]->cast<Id>()->decl(); int v0idx = envi.varOccurrences.find(vd); push_vardecl(envi, m[v0idx]->cast<VarDeclI>(), v0idx, vardeclQueue); }
push_dependent_constraints(envi, (*al_x)[0]->cast<Id>(), constraintQueue); CollectDecls cd(envi.varOccurrences, deletedVarDecls, ci); top_down(cd, c); ci->e(constants().literalTrue); ci->remove(); } } } else if (c->id() == constants().ids.forall) { // Remove forall constraints, assign variables inside the forall to true
auto* al = follow_id(c->arg(0))->cast<ArrayLit>(); for (unsigned int j = al->size(); (j--) != 0U;) { if (Id* id = (*al)[j]->dynamicCast<Id>()) { if (id->decl()->ti()->domain() == nullptr) { toAssignBoolVars.push_back( envi.varOccurrences.idx.find(id->decl()->id())->second); } else if (id->decl()->ti()->domain() == constants().literalFalse) { env.envi().fail(); id->decl()->e(constants().literalTrue); } } // todo: check else case (fixed bool inside a forall at this stage) } toRemoveConstraints.push_back(i); } else if (c->id() == constants().ids.exists || c->id() == constants().ids.clause) { // Add disjunctive constraints to the boolConstraints list
boolConstraints.push_back(i); } } else if (Id* id = ci->e()->dynamicCast<Id>()) { if (id->decl()->ti()->domain() == constants().literalFalse) { env.envi().fail(); ci->e(constants().literalFalse); } else { if (id->decl()->ti()->domain() == nullptr) { toAssignBoolVars.push_back(envi.varOccurrences.idx.find(id->decl()->id())->second); } toRemoveConstraints.push_back(i); } } } } else if (auto* vdi = m[i]->dynamicCast<VarDeclI>()) { vdi->flag(false); if ((vdi->e()->e() != nullptr) && vdi->e()->e()->isa<Id>() && vdi->e()->type().dim() == 0) { // unify variable with the identifier it's assigned to Id* id1 = vdi->e()->e()->cast<Id>(); vdi->e()->e(nullptr);
// Transfer is_defined_var annotation if (id1->decl()->ann().contains(constants().ann.is_defined_var)) { vdi->e()->ann().add(constants().ann.is_defined_var); } else if (vdi->e()->ann().contains(constants().ann.is_defined_var)) { id1->decl()->ann().add(constants().ann.is_defined_var); }
unify(envi, deletedVarDecls, vdi->e()->id(), id1); push_dependent_constraints(envi, id1, constraintQueue); } if (vdi->e()->type().isbool() && vdi->e()->type().dim() == 0 && (vdi->e()->ti()->domain() == constants().literalTrue || vdi->e()->ti()->domain() == constants().literalFalse)) { // push RHS onto constraint queue since this bool var is fixed push_vardecl(envi, vdi, i, vardeclQueue); push_dependent_constraints(envi, vdi->e()->id(), constraintQueue); } if (Call* c = Expression::dynamicCast<Call>(vdi->e()->e())) { if (c->id() == constants().ids.forall || c->id() == constants().ids.exists || c->id() == constants().ids.clause) { // push reified foralls, exists, clauses boolConstraints.push_back(i); } } if (vdi->e()->type().isint()) { if (((vdi->e()->e() != nullptr) && vdi->e()->e()->isa<IntLit>()) || ((vdi->e()->ti()->domain() != nullptr) && vdi->e()->ti()->domain()->isa<SetLit>() && vdi->e()->ti()->domain()->cast<SetLit>()->isv()->size() == 1 && vdi->e()->ti()->domain()->cast<SetLit>()->isv()->min() == vdi->e()->ti()->domain()->cast<SetLit>()->isv()->max())) { // Variable is assigned an integer, or has a singleton domain push_vardecl(envi, vdi, i, vardeclQueue); push_dependent_constraints(envi, vdi->e()->id(), constraintQueue); } } } }
// Phase 2: handle boolean constraints // - check if any boolean constraint is subsumed (e.g. a fixed false in a forall, or a fixed // true in a disjunction) // - check if any boolean constraint has a single non-fixed literal left, then fix that literal for (auto i = static_cast<unsigned int>(boolConstraints.size()); (i--) != 0U;) { Item* bi = m[boolConstraints[i]]; if (bi->removed()) { continue; } Call* c;
if (bi->isa<ConstraintI>()) { c = bi->cast<ConstraintI>()->e()->dynamicCast<Call>(); } else { c = bi->cast<VarDeclI>()->e()->e()->dynamicCast<Call>(); } if (c == nullptr) { continue; } bool isConjunction = (c->id() == constants().ids.forall); bool subsumed = false; Id* finalId = nullptr; bool finalIdNeg = false; int idCount = 0; std::vector<VarDecl*> pos; std::vector<VarDecl*> neg; for (unsigned int j = 0; j < c->argCount(); j++) { bool unit = (j == 0 ? isConjunction : !isConjunction); auto* al = follow_id(c->arg(j))->cast<ArrayLit>(); for (unsigned int k = 0; k < al->size(); k++) { if (Id* ident = (*al)[k]->dynamicCast<Id>()) { if ((ident->decl()->ti()->domain() != nullptr) || ((ident->decl()->e() != nullptr) && ident->decl()->e()->type().isPar())) { bool identValue = ident->decl()->ti()->domain() != nullptr ? eval_bool(envi, ident->decl()->ti()->domain()) : eval_bool(envi, ident->decl()->e()); if (identValue != unit) { subsumed = true; goto subsumed_check_done; } } else { idCount++; finalId = ident; finalIdNeg = (j == 1); if (j == 0) { pos.push_back(ident->decl()); } else { neg.push_back(ident->decl()); } } } else { if ((*al)[k]->cast<BoolLit>()->v() != unit) { subsumed = true; goto subsumed_check_done; } } } } if (!pos.empty() && !neg.empty()) { std::sort(pos.begin(), pos.end()); std::sort(neg.begin(), neg.end()); unsigned int ix = 0; unsigned int iy = 0; for (;;) { if (pos[ix] == neg[iy]) { subsumed = true; break; } if (pos[ix] < neg[iy]) { ix++; } else { iy++; } if (ix == pos.size() || iy == neg.size()) { break; } } }
subsumed_check_done: if (subsumed) { if (isConjunction) { if (bi->isa<ConstraintI>()) { env.envi().fail(); } else { if (bi->cast<VarDeclI>()->e()->ti()->domain() != nullptr) { if (eval_bool(envi, bi->cast<VarDeclI>()->e()->ti()->domain())) { envi.fail(); } } else { CollectDecls cd(envi.varOccurrences, deletedVarDecls, bi); top_down(cd, bi->cast<VarDeclI>()->e()->e()); bi->cast<VarDeclI>()->e()->ti()->domain(constants().literalFalse); bi->cast<VarDeclI>()->e()->ti()->setComputedDomain(true); bi->cast<VarDeclI>()->e()->e(constants().literalFalse); push_vardecl(envi, bi->cast<VarDeclI>(), boolConstraints[i], vardeclQueue); push_dependent_constraints(envi, bi->cast<VarDeclI>()->e()->id(), constraintQueue); } } } else { if (bi->isa<ConstraintI>()) { CollectDecls cd(envi.varOccurrences, deletedVarDecls, bi); top_down(cd, bi->cast<ConstraintI>()->e()); bi->remove(); } else { if (bi->cast<VarDeclI>()->e()->ti()->domain() != nullptr) { if (!eval_bool(envi, bi->cast<VarDeclI>()->e()->ti()->domain())) { envi.fail(); } } else { CollectDecls cd(envi.varOccurrences, deletedVarDecls, bi); top_down(cd, bi->cast<VarDeclI>()->e()->e()); bi->cast<VarDeclI>()->e()->ti()->domain(constants().literalTrue); bi->cast<VarDeclI>()->e()->ti()->setComputedDomain(true); bi->cast<VarDeclI>()->e()->e(constants().literalTrue); push_vardecl(envi, bi->cast<VarDeclI>(), boolConstraints[i], vardeclQueue); push_dependent_constraints(envi, bi->cast<VarDeclI>()->e()->id(), constraintQueue); } } } } else if (idCount == 1 && bi->isa<ConstraintI>()) { assert(finalId->decl()->ti()->domain() == nullptr); finalId->decl()->ti()->domain(constants().boollit(!finalIdNeg)); if (finalId->decl()->e() == nullptr) { finalId->decl()->e(constants().boollit(!finalIdNeg)); } CollectDecls cd(envi.varOccurrences, deletedVarDecls, bi); top_down(cd, bi->cast<ConstraintI>()->e()); bi->remove(); push_vardecl(envi, envi.varOccurrences.idx.find(finalId->decl()->id())->second, vardeclQueue); push_dependent_constraints(envi, finalId, constraintQueue); } // todo: for var decls, we could unify the variable with the remaining finalId (the RHS) }
// Fix all bool vars in toAssignBoolVars to true and push their declarations and constraints for (unsigned int i = static_cast<int>(toAssignBoolVars.size()); (i--) != 0U;) { if (m[toAssignBoolVars[i]]->removed()) { continue; } auto* vdi = m[toAssignBoolVars[i]]->cast<VarDeclI>(); if (vdi->e()->ti()->domain() == nullptr) { vdi->e()->ti()->domain(constants().literalTrue); push_vardecl(envi, vdi, toAssignBoolVars[i], vardeclQueue); push_dependent_constraints(envi, vdi->e()->id(), constraintQueue); } }
// Phase 3: fixpoint of constraint and variable simplification
std::unordered_map<Expression*, int> nonFixedLiteralCount; while (!vardeclQueue.empty() || !constraintQueue.empty()) { while (!vardeclQueue.empty()) { int var_idx = vardeclQueue.front(); vardeclQueue.pop_front(); m[var_idx]->cast<VarDeclI>()->flag(false); VarDecl* vd = m[var_idx]->cast<VarDeclI>()->e();
if (vd->type().isbool() && (vd->ti()->domain() != nullptr)) { bool isTrue = vd->ti()->domain() == constants().literalTrue; bool remove = false; if (vd->e() != nullptr) { if (Id* id = vd->e()->dynamicCast<Id>()) { // Variable assigned to id, so fix id if (id->decl()->ti()->domain() == nullptr) { id->decl()->ti()->domain(vd->ti()->domain()); push_vardecl(envi, envi.varOccurrences.idx.find(id->decl()->id())->second, vardeclQueue); } else if (id->decl()->ti()->domain() != vd->ti()->domain()) { env.envi().fail(); } remove = true; } else if (Call* c = vd->e()->dynamicCast<Call>()) { if (isTrue && c->id() == constants().ids.forall) { // Reified forall is now fixed to true, so make all elements of the conjunction true remove = true; auto* al = follow_id(c->arg(0))->cast<ArrayLit>(); for (unsigned int i = 0; i < al->size(); i++) { if (Id* id = (*al)[i]->dynamicCast<Id>()) { if (id->decl()->ti()->domain() == nullptr) { id->decl()->ti()->domain(constants().literalTrue); push_vardecl(envi, envi.varOccurrences.idx.find(id->decl()->id())->second, vardeclQueue); } else if (id->decl()->ti()->domain() == constants().literalFalse) { env.envi().fail(); remove = true; } } } } else if (!isTrue && (c->id() == constants().ids.exists || c->id() == constants().ids.clause)) { // Reified disjunction is now fixed to false, so make all elements of the // disjunction false remove = true; for (unsigned int i = 0; i < c->argCount(); i++) { bool ispos = i == 0; auto* al = follow_id(c->arg(i))->cast<ArrayLit>(); for (unsigned int j = 0; j < al->size(); j++) { if (Id* id = (*al)[j]->dynamicCast<Id>()) { if (id->decl()->ti()->domain() == nullptr) { id->decl()->ti()->domain(constants().boollit(!ispos)); push_vardecl(envi, envi.varOccurrences.idx.find(id->decl()->id())->second, vardeclQueue); } else if (id->decl()->ti()->domain() == constants().boollit(ispos)) { env.envi().fail(); remove = true; } } } } } } } else { // If bool variable doesn't have a RHS, just remove it remove = true; } push_dependent_constraints(envi, vd->id(), constraintQueue); std::vector<Item*> toRemove; auto it = envi.varOccurrences.itemMap.find(vd->id()->decl()->id());
// Handle all boolean constraints that involve this variable if (it != envi.varOccurrences.itemMap.end()) { for (auto item = it->second.begin(); item != it->second.end(); ++item) { if ((*item)->removed()) { continue; } if (auto* vdi = (*item)->dynamicCast<VarDeclI>()) { // The variable occurs in the RHS of another variable, so // if that is an array variable, simplify all constraints that // mention the array variable if ((vdi->e()->e() != nullptr) && vdi->e()->e()->isa<ArrayLit>()) { auto ait = envi.varOccurrences.itemMap.find(vdi->e()->id()->decl()->id()); if (ait != envi.varOccurrences.itemMap.end()) { for (auto* aitem : ait->second) { simplify_bool_constraint(envi, aitem, vd, remove, vardeclQueue, constraintQueue, toRemove, deletedVarDecls, nonFixedLiteralCount); } } continue; } } // Simplify the constraint *item (which depends on this variable) simplify_bool_constraint(envi, *item, vd, remove, vardeclQueue, constraintQueue, toRemove, deletedVarDecls, nonFixedLiteralCount); } } // Actually remove all items that have become unnecessary in the step above for (auto i = static_cast<unsigned int>(toRemove.size()); (i--) != 0U;) { if (auto* ci = toRemove[i]->dynamicCast<ConstraintI>()) { CollectDecls cd(envi.varOccurrences, deletedVarDecls, ci); top_down(cd, ci->e()); ci->remove(); } else { auto* vdi = toRemove[i]->cast<VarDeclI>(); CollectDecls cd(envi.varOccurrences, deletedVarDecls, vdi); top_down(cd, vdi->e()->e()); vdi->e()->e(nullptr); } } if (remove) { deletedVarDecls.push_back(vd); } else { simplify_constraint(envi, m[var_idx], deletedVarDecls, constraintQueue, vardeclQueue); } } else if (vd->type().isint() && (vd->ti()->domain() != nullptr)) { IntSetVal* isv = eval_intset(envi, vd->ti()->domain()); if (isv->size() == 1 && isv->card() == 1) { simplify_constraint(envi, m[var_idx], deletedVarDecls, constraintQueue, vardeclQueue); } } } // end of processing of variable queue
// Now handle all non-boolean constraints (i.e. anything except forall, clause, exists) bool handledConstraint = false; while (!handledConstraint && !constraintQueue.empty()) { Item* item = constraintQueue.front(); constraintQueue.pop_front(); Call* c; ArrayLit* al = nullptr; if (auto* ci = item->dynamicCast<ConstraintI>()) { ci->flag(false); c = Expression::dynamicCast<Call>(ci->e()); } else { if (item->removed()) { // This variable was removed because of unification, so we look up the // variable it was unified to item = m[envi.varOccurrences.find(item->cast<VarDeclI>()->e()->id()->decl())] ->cast<VarDeclI>(); } item->cast<VarDeclI>()->flag(false); c = Expression::dynamicCast<Call>(item->cast<VarDeclI>()->e()->e()); al = Expression::dynamicCast<ArrayLit>(item->cast<VarDeclI>()->e()->e()); } if (!item->removed()) { if (al != nullptr) { // Substitute all fixed variables by their values in array literals, then // push all constraints that depend on the array substitute_fixed_vars(envi, item, deletedVarDecls); push_dependent_constraints(envi, item->cast<VarDeclI>()->e()->id(), constraintQueue); } else if ((c == nullptr) || !(c->id() == constants().ids.forall || c->id() == constants().ids.exists || c->id() == constants().ids.clause)) { // For any constraint that is not forall, exists or clause, // substitute fixed arguments, then simplify it substitute_fixed_vars(envi, item, deletedVarDecls); handledConstraint = simplify_constraint(envi, item, deletedVarDecls, constraintQueue, vardeclQueue); } } } }
// Clean up constraints that have been removed in the previous phase for (auto i = static_cast<unsigned int>(toRemoveConstraints.size()); (i--) != 0U;) { auto* ci = m[toRemoveConstraints[i]]->cast<ConstraintI>(); CollectDecls cd(envi.varOccurrences, deletedVarDecls, ci); top_down(cd, ci->e()); ci->remove(); }
// Phase 4: Chain Breaking if (chain_compression) { ImpCompressor imp(envi, m, deletedVarDecls, boolConstraints); LECompressor le(envi, m, deletedVarDecls); for (auto& item : m) { imp.trackItem(item); le.trackItem(item); } imp.compress(); le.compress(); }
// Phase 5: handle boolean constraints again (todo: check if we can // refactor this into a separate function) // // Difference to phase 2: constraint argument arrays are actually shortened here if possible for (auto i = static_cast<unsigned int>(boolConstraints.size()); (i--) != 0U;) { Item* bi = m[boolConstraints[i]]; if (bi->removed()) { continue; } Call* c; std::vector<VarDecl*> removedVarDecls;
if (bi->isa<ConstraintI>()) { c = bi->cast<ConstraintI>()->e()->dynamicCast<Call>(); } else { c = Expression::dynamicCast<Call>(bi->cast<VarDeclI>()->e()->e()); } if (c == nullptr || !(c->id() == constants().ids.forall || c->id() == constants().ids.exists || c->id() == constants().ids.clause)) { continue; } bool isConjunction = (c->id() == constants().ids.forall); bool subsumed = false; for (unsigned int j = 0; j < c->argCount(); j++) { bool unit = (j == 0 ? isConjunction : !isConjunction); auto* al = follow_id(c->arg(j))->cast<ArrayLit>(); std::vector<Expression*> compactedAl; for (unsigned int k = 0; k < al->size(); k++) { if (Id* ident = (*al)[k]->dynamicCast<Id>()) { if (ident->decl()->ti()->domain() != nullptr) { if (!(ident->decl()->ti()->domain() == constants().boollit(unit))) { subsumed = true; } removedVarDecls.push_back(ident->decl()); } else { compactedAl.push_back(ident); } } else { if ((*al)[k]->cast<BoolLit>()->v() != unit) { subsumed = true; } } } if (compactedAl.size() < al->size()) { c->arg(j, new ArrayLit(al->loc(), compactedAl)); c->arg(j)->type(Type::varbool(1)); } } if (subsumed) { if (isConjunction) { if (bi->isa<ConstraintI>()) { env.envi().fail(); } else { auto* al = follow_id(c->arg(0))->cast<ArrayLit>(); for (unsigned int j = 0; j < al->size(); j++) { removedVarDecls.push_back((*al)[j]->cast<Id>()->decl()); } bi->cast<VarDeclI>()->e()->ti()->domain(constants().literalFalse); bi->cast<VarDeclI>()->e()->ti()->setComputedDomain(true); bi->cast<VarDeclI>()->e()->e(constants().literalFalse); } } else { if (bi->isa<ConstraintI>()) { CollectDecls cd(envi.varOccurrences, deletedVarDecls, bi); top_down(cd, bi->cast<ConstraintI>()->e()); bi->remove(); } else { CollectDecls cd(envi.varOccurrences, deletedVarDecls, bi); top_down(cd, bi->cast<VarDeclI>()->e()->e()); bi->cast<VarDeclI>()->e()->ti()->domain(constants().literalTrue); bi->cast<VarDeclI>()->e()->ti()->setComputedDomain(true); bi->cast<VarDeclI>()->e()->e(constants().literalTrue); } } } for (auto& removedVarDecl : removedVarDecls) { if (env.envi().varOccurrences.remove(removedVarDecl, bi) == 0) { if ((removedVarDecl->e() == nullptr || removedVarDecl->ti()->domain() == nullptr || removedVarDecl->ti()->computedDomain()) && !is_output(removedVarDecl)) { deletedVarDecls.push_back(removedVarDecl); } } } if (auto* vdi = bi->dynamicCast<VarDeclI>()) { if (envi.varOccurrences.occurrences(vdi->e()) == 0) { if ((vdi->e()->e() == nullptr || vdi->e()->ti()->domain() == nullptr || vdi->e()->ti()->computedDomain()) && !is_output(vdi->e())) { deletedVarDecls.push_back(vdi->e()); } } } }
// Phase 6: remove deleted variables if possible // TODO: The delayed deletion could be done eagerly by the creation of // env.optRemoveItem() which contains the logic in this while loop. while (!deletedVarDecls.empty()) { VarDecl* cur = deletedVarDecls.back(); deletedVarDecls.pop_back(); if (envi.varOccurrences.occurrences(cur) == 0) { auto cur_idx = envi.varOccurrences.idx.find(cur->id()); if (cur_idx != envi.varOccurrences.idx.end() && !m[cur_idx->second]->removed()) { if (is_output(cur)) { // We have to change the output model if we remove this variable Expression* val = nullptr; if (cur->type().isbool() && (cur->ti()->domain() != nullptr)) { val = cur->ti()->domain(); } else if (cur->type().isint()) { if ((cur->e() != nullptr) && cur->e()->isa<IntLit>()) { val = cur->e(); } else if ((cur->ti()->domain() != nullptr) && cur->ti()->domain()->isa<SetLit>() && cur->ti()->domain()->cast<SetLit>()->isv()->size() == 1 && cur->ti()->domain()->cast<SetLit>()->isv()->min() == cur->ti()->domain()->cast<SetLit>()->isv()->max()) { val = IntLit::a(cur->ti()->domain()->cast<SetLit>()->isv()->min()); } } if (val != nullptr) { // Find corresponding variable in output model and fix it VarDecl* vd_out = (*envi.output)[envi.outputFlatVarOccurrences.find(cur)]->cast<VarDeclI>()->e(); vd_out->e(val); CollectDecls cd(envi.varOccurrences, deletedVarDecls, m[cur_idx->second]->cast<VarDeclI>()); top_down(cd, cur->e()); (*envi.flat())[cur_idx->second]->remove(); } } else { CollectDecls cd(envi.varOccurrences, deletedVarDecls, m[cur_idx->second]->cast<VarDeclI>()); top_down(cd, cur->e()); (*envi.flat())[cur_idx->second]->remove(); } } } } } catch (ModelInconsistent&) { }}
class SubstitutionVisitor : public EVisitor {protected: std::vector<VarDecl*> _removed; Expression* subst(Expression* e) { if (auto* vd = follow_id_to_decl(e)->dynamicCast<VarDecl>()) { if (vd->type().isbool() && (vd->ti()->domain() != nullptr)) { _removed.push_back(vd); return vd->ti()->domain(); } if (vd->type().isint()) { if ((vd->e() != nullptr) && vd->e()->isa<IntLit>()) { _removed.push_back(vd); return vd->e(); } if ((vd->ti()->domain() != nullptr) && vd->ti()->domain()->isa<SetLit>() && vd->ti()->domain()->cast<SetLit>()->isv()->size() == 1 && vd->ti()->domain()->cast<SetLit>()->isv()->min() == vd->ti()->domain()->cast<SetLit>()->isv()->max()) { _removed.push_back(vd); return IntLit::a(vd->ti()->domain()->cast<SetLit>()->isv()->min()); } } } return e; }
public: /// Visit array literal void vArrayLit(ArrayLit& al) { for (unsigned int i = 0; i < al.size(); i++) { al.set(i, subst(al[i])); } } /// Visit call void vCall(Call& c) { for (unsigned int i = 0; i < c.argCount(); i++) { c.arg(i, subst(c.arg(i))); } } /// Determine whether to enter node static bool enter(Expression* e) { return !e->isa<Id>(); } void remove(EnvI& env, Item* item, std::vector<VarDecl*>& deletedVarDecls) { for (auto& i : _removed) { i->ann().remove(constants().ann.is_defined_var); if (env.varOccurrences.remove(i, item) == 0) { if ((i->e() == nullptr || i->ti()->domain() == nullptr || i->ti()->computedDomain()) && !is_output(i)) { deletedVarDecls.push_back(i); } } } }};
void substitute_fixed_vars(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls) { SubstitutionVisitor sv; if (auto* ci = ii->dynamicCast<ConstraintI>()) { top_down(sv, ci->e()); for (ExpressionSetIter it = ci->e()->ann().begin(); it != ci->e()->ann().end(); ++it) { top_down(sv, *it); } } else if (auto* vdi = ii->dynamicCast<VarDeclI>()) { top_down(sv, vdi->e()); for (ExpressionSetIter it = vdi->e()->ann().begin(); it != vdi->e()->ann().end(); ++it) { top_down(sv, *it); } } else { auto* si = ii->cast<SolveI>(); top_down(sv, si->e()); for (ExpressionSetIter it = si->ann().begin(); it != si->ann().end(); ++it) { top_down(sv, *it); } } sv.remove(env, ii, deletedVarDecls);}
bool simplify_constraint(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls, std::deque<Item*>& constraintQueue, std::deque<unsigned int>& vardeclQueue) { Expression* con_e; bool is_true; bool is_false; if (auto* ci = ii->dynamicCast<ConstraintI>()) { con_e = ci->e(); is_true = true; is_false = false; } else { auto* vdi = ii->cast<VarDeclI>(); con_e = vdi->e()->e(); is_true = (vdi->e()->type().isbool() && vdi->e()->ti()->domain() == constants().literalTrue); is_false = (vdi->e()->type().isbool() && vdi->e()->ti()->domain() == constants().literalFalse); assert(is_true || is_false || !vdi->e()->type().isbool() || vdi->e()->ti()->domain() == nullptr); } if (Call* c = Expression::dynamicCast<Call>(con_e)) { if (c->id() == constants().ids.int_.eq || c->id() == constants().ids.bool_eq || c->id() == constants().ids.float_.eq) { if (is_true && c->arg(0)->isa<Id>() && c->arg(1)->isa<Id>() && (c->arg(0)->cast<Id>()->decl()->e() == nullptr || c->arg(1)->cast<Id>()->decl()->e() == nullptr)) { if (Call* defVar = c->ann().getCall(constants().ann.defines_var)) { // First, remove defines_var/is_defined_var annotations if present if (Expression::equal(defVar->arg(0), c->arg(0))) { c->arg(0)->cast<Id>()->decl()->ann().remove(constants().ann.is_defined_var); } else { c->arg(1)->cast<Id>()->decl()->ann().remove(constants().ann.is_defined_var); } } unify(env, deletedVarDecls, c->arg(0)->cast<Id>(), c->arg(1)->cast<Id>()); push_dependent_constraints(env, c->arg(0)->cast<Id>(), constraintQueue); CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); ii->remove(); } else if (c->arg(0)->type().isPar() && c->arg(1)->type().isPar()) { Expression* e0 = eval_par(env, c->arg(0)); Expression* e1 = eval_par(env, c->arg(1)); bool is_equal = Expression::equal(e0, e1); if ((is_true && is_equal) || (is_false && !is_equal)) { // do nothing } else if ((is_true && !is_equal) || (is_false && is_equal)) { env.fail(); } else { auto* vdi = ii->cast<VarDeclI>(); CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); vdi->e()->e(constants().boollit(is_equal)); vdi->e()->ti()->domain(constants().boollit(is_equal)); vdi->e()->ti()->setComputedDomain(true); push_vardecl(env, vdi, env.varOccurrences.find(vdi->e()), vardeclQueue); push_dependent_constraints(env, vdi->e()->id(), constraintQueue); } if (ii->isa<ConstraintI>()) { CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); ii->remove(); } } else if (is_true && ((c->arg(0)->isa<Id>() && c->arg(1)->type().isPar()) || (c->arg(1)->isa<Id>() && c->arg(0)->type().isPar()))) { Id* ident = c->arg(0)->isa<Id>() ? c->arg(0)->cast<Id>() : c->arg(1)->cast<Id>(); Expression* arg = c->arg(0)->isa<Id>() ? c->arg(1) : c->arg(0); bool canRemove = false; TypeInst* ti = ident->decl()->ti(); switch (ident->type().bt()) { case Type::BT_BOOL: if (ti->domain() == nullptr) { ti->domain(constants().boollit(eval_bool(env, arg))); ti->setComputedDomain(false); canRemove = true; } else { if (eval_bool(env, ti->domain()) == eval_bool(env, arg)) { canRemove = true; } else { env.fail(); canRemove = true; } } break; case Type::BT_INT: { IntVal d = eval_int(env, arg); if (ti->domain() == nullptr) { ti->domain(new SetLit(Location().introduce(), IntSetVal::a(d, d))); ti->setComputedDomain(false); canRemove = true; } else { IntSetVal* isv = eval_intset(env, ti->domain()); if (isv->contains(d)) { ident->decl()->ti()->domain(new SetLit(Location().introduce(), IntSetVal::a(d, d))); ident->decl()->ti()->setComputedDomain(false); canRemove = true; } else { env.fail(); canRemove = true; } } } break; case Type::BT_FLOAT: { if (ti->domain() == nullptr) { ti->domain(new BinOp(Location().introduce(), arg, BOT_DOTDOT, arg)); ti->setComputedDomain(false); canRemove = true; } else { FloatVal value = eval_float(env, arg); if (LinearTraits<FloatLit>::domainContains(eval_floatset(env, ti->domain()), value)) { ti->domain(new BinOp(Location().introduce(), arg, BOT_DOTDOT, arg)); ti->setComputedDomain(false); canRemove = true; } else { env.fail(); canRemove = true; } } } break; default: break; } if (ident->decl()->e() == nullptr) { ident->decl()->e(c->arg(0)->isa<Id>() ? c->arg(1) : c->arg(0)); ti->setComputedDomain(true); canRemove = true; }
if (ident->decl()->e()->isa<Call>()) { constraintQueue.push_back((*env.flat())[env.varOccurrences.find(ident->decl())]); } push_dependent_constraints(env, ident, constraintQueue); if (canRemove) { CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); ii->remove(); } } } else if ((is_true || is_false) && c->id() == constants().ids.int_.le && ((c->arg(0)->isa<Id>() && c->arg(1)->type().isPar()) || (c->arg(1)->isa<Id>() && c->arg(0)->type().isPar()))) { Id* ident = c->arg(0)->isa<Id>() ? c->arg(0)->cast<Id>() : c->arg(1)->cast<Id>(); Expression* arg = c->arg(0)->isa<Id>() ? c->arg(1) : c->arg(0); IntSetVal* domain = ident->decl()->ti()->domain() != nullptr ? eval_intset(env, ident->decl()->ti()->domain()) : nullptr; if (domain != nullptr) { BinOpType bot = c->arg(0)->isa<Id>() ? (is_true ? BOT_LQ : BOT_GR) : (is_true ? BOT_GQ : BOT_LE); IntSetVal* newDomain = LinearTraits<IntLit>::limitDomain(bot, domain, eval_int(env, arg)); if (newDomain->card() == 0) { env.fail(); } else { ident->decl()->ti()->domain(new SetLit(Location().introduce(), newDomain)); ident->decl()->ti()->setComputedDomain(false);
if (newDomain->min() == newDomain->max()) { push_dependent_constraints(env, ident, constraintQueue); } CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c);
if (auto* vdi = ii->dynamicCast<VarDeclI>()) { vdi->e()->e(constants().boollit(is_true)); push_dependent_constraints(env, vdi->e()->id(), constraintQueue); if (env.varOccurrences.occurrences(vdi->e()) == 0) { if (is_output(vdi->e())) { VarDecl* vd_out = (*env.output)[env.outputFlatVarOccurrences.find(vdi->e())] ->cast<VarDeclI>() ->e(); vd_out->e(constants().boollit(is_true)); } vdi->remove(); } } else { ii->remove(); } } } } else if (c->id() == constants().ids.bool2int) { auto* vdi = ii->dynamicCast<VarDeclI>(); VarDecl* vd; bool fixed = false; bool b_val = false; if (vdi != nullptr) { vd = vdi->e(); } else if (Id* ident = c->arg(1)->dynamicCast<Id>()) { vd = ident->decl(); } else { vd = nullptr; } IntSetVal* vd_dom = nullptr; if (vd != nullptr) { if (vd->ti()->domain() != nullptr) { vd_dom = eval_intset(env, vd->ti()->domain()); if (vd_dom->max() < 0 || vd_dom->min() > 1) { env.fail(); return true; } fixed = vd_dom->min() == vd_dom->max(); b_val = (vd_dom->min() == 1); } } else { fixed = true; b_val = (eval_int(env, c->arg(1)) == 1); } if (fixed) { if (c->arg(0)->type().isPar()) { bool b2i_val = eval_bool(env, c->arg(0)); if (b2i_val != b_val) { env.fail(); } else { CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); ii->remove(); } } else { Id* ident = c->arg(0)->cast<Id>(); TypeInst* ti = ident->decl()->ti(); if (ti->domain() == nullptr) { ti->domain(constants().boollit(b_val)); ti->setComputedDomain(false); } else if (eval_bool(env, ti->domain()) != b_val) { env.fail(); } CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); if (vd != nullptr) { vd->e(IntLit::a(static_cast<long long>(b_val))); vd->ti()->setComputedDomain(true); } push_dependent_constraints(env, ident, constraintQueue); if (vdi != nullptr) { if (env.varOccurrences.occurrences(vd) == 0) { vdi->remove(); } } else { ii->remove(); } } } else { IntVal v = -1; if (auto* bl = c->arg(0)->dynamicCast<BoolLit>()) { v = bl->v() ? 1 : 0; } else if (Id* ident = c->arg(0)->dynamicCast<Id>()) { if (ident->decl()->ti()->domain() != nullptr) { v = eval_bool(env, ident->decl()->ti()->domain()) ? 1 : 0; } } if (v != -1) { if ((vd_dom != nullptr) && !vd_dom->contains(v)) { env.fail(); } else { CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); vd->e(IntLit::a(v)); vd->ti()->domain(new SetLit(Location().introduce(), IntSetVal::a(v, v))); vd->ti()->setComputedDomain(true); push_vardecl(env, env.varOccurrences.find(vd), vardeclQueue); push_dependent_constraints(env, vd->id(), constraintQueue); } } }
} else { // General propagation: call a propagator registered for this constraint type Expression* rewrite = nullptr; GCLock lock; switch (OptimizeRegistry::registry().process(env, ii, c, rewrite)) { case OptimizeRegistry::CS_NONE: return false; case OptimizeRegistry::CS_OK: return true; case OptimizeRegistry::CS_FAILED: if (is_true) { env.fail(); return true; } else if (is_false) { if (ii->isa<ConstraintI>()) { CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); ii->remove(); } else { deletedVarDecls.push_back(ii->cast<VarDeclI>()->e()); } return true; } else { auto* vdi = ii->cast<VarDeclI>(); vdi->e()->ti()->domain(constants().literalFalse); CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); vdi->e()->e(constants().literalFalse); push_vardecl(env, vdi, env.varOccurrences.find(vdi->e()), vardeclQueue); return true; } case OptimizeRegistry::CS_ENTAILED: if (is_true) { if (ii->isa<ConstraintI>()) { CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); ii->remove(); } else { deletedVarDecls.push_back(ii->cast<VarDeclI>()->e()); } return true; } else if (is_false) { env.fail(); return true; } else { auto* vdi = ii->cast<VarDeclI>(); vdi->e()->ti()->domain(constants().literalTrue); CollectDecls cd(env.varOccurrences, deletedVarDecls, ii); top_down(cd, c); vdi->e()->e(constants().literalTrue); push_vardecl(env, vdi, env.varOccurrences.find(vdi->e()), vardeclQueue); return true; } case OptimizeRegistry::CS_REWRITE: { std::vector<VarDecl*> tdv; CollectDecls cd(env.varOccurrences, tdv, ii); top_down(cd, c);
CollectOccurrencesE ce(env.varOccurrences, ii); top_down(ce, rewrite);
for (auto& i : tdv) { if (env.varOccurrences.occurrences(i) == 0) { deletedVarDecls.push_back(i); } }
assert(rewrite != nullptr); if (auto* ci = ii->dynamicCast<ConstraintI>()) { ci->e(rewrite); constraintQueue.push_back(ii); } else { auto* vdi = ii->cast<VarDeclI>(); vdi->e()->e(rewrite); if ((vdi->e()->e() != nullptr) && vdi->e()->e()->isa<Id>() && vdi->e()->type().dim() == 0) { Id* id1 = vdi->e()->e()->cast<Id>(); vdi->e()->e(nullptr); // Transfer is_defined_var annotation if (id1->decl()->ann().contains(constants().ann.is_defined_var)) { vdi->e()->ann().add(constants().ann.is_defined_var); } else if (vdi->e()->ann().contains(constants().ann.is_defined_var)) { id1->decl()->ann().add(constants().ann.is_defined_var); } unify(env, deletedVarDecls, vdi->e()->id(), id1); push_dependent_constraints(env, id1, constraintQueue); } if ((vdi->e()->e() != nullptr) && vdi->e()->e()->type().isPar() && (vdi->e()->ti()->domain() != nullptr)) { if (vdi->e()->e()->type().isint()) { IntVal iv = eval_int(env, vdi->e()->e()); IntSetVal* dom = eval_intset(env, vdi->e()->ti()->domain()); if (!dom->contains(iv)) { env.fail(); } } else if (vdi->e()->e()->type().isIntSet()) { IntSetVal* isv = eval_intset(env, vdi->e()->e()); IntSetVal* dom = eval_intset(env, vdi->e()->ti()->domain()); IntSetRanges isv_r(isv); IntSetRanges dom_r(dom); if (!Ranges::subset(isv_r, dom_r)) { env.fail(); } } else if (vdi->e()->e()->type().isfloat()) { FloatVal fv = eval_float(env, vdi->e()->e()); FloatSetVal* dom = eval_floatset(env, vdi->e()->ti()->domain()); if (!dom->contains(fv)) { env.fail(); } } } if (vdi->e()->ti()->type() != Type::varbool() || vdi->e()->ti()->domain() == nullptr) { push_vardecl(env, vdi, env.varOccurrences.find(vdi->e()), vardeclQueue); }
if (is_true) { constraintQueue.push_back(ii); } } return true; } } } } return false;}
int bool_state(EnvI& env, Expression* e) { if (e->type().isPar()) { return static_cast<int>(eval_bool(env, e)); } Id* id = e->cast<Id>(); if (id->decl()->ti()->domain() == nullptr) { return 2; } return static_cast<int>(id->decl()->ti()->domain() == constants().literalTrue);}
int decrement_non_fixed_vars(std::unordered_map<Expression*, int>& nonFixedLiteralCount, Call* c) { auto it = nonFixedLiteralCount.find(c); if (it == nonFixedLiteralCount.end()) { int nonFixedVars = 0; for (unsigned int i = 0; i < c->argCount(); i++) { auto* al = follow_id(c->arg(i))->cast<ArrayLit>(); nonFixedVars += static_cast<int>(al->size()); for (unsigned int j = al->size(); (j--) != 0U;) { if ((*al)[j]->type().isPar()) { nonFixedVars--; } } } nonFixedLiteralCount.insert(std::make_pair(c, nonFixedVars)); return nonFixedVars; } it->second--; return it->second;}
void simplify_bool_constraint(EnvI& env, Item* ii, VarDecl* vd, bool& remove, std::deque<unsigned int>& vardeclQueue, std::deque<Item*>& constraintQueue, std::vector<Item*>& toRemove, std::vector<VarDecl*>& deletedVarDecls, std::unordered_map<Expression*, int>& nonFixedLiteralCount) { if (ii->isa<SolveI>()) { remove = false; return; } bool isTrue = vd->ti()->domain() == constants().literalTrue; Expression* e = nullptr; auto* ci = ii->dynamicCast<ConstraintI>(); auto* vdi = ii->dynamicCast<VarDeclI>(); if (ci != nullptr) { e = ci->e();
if (vd->ti()->domain() != nullptr) { if (Call* definedVarCall = e->ann().getCall(constants().ann.defines_var)) { if (Expression::equal(definedVarCall->arg(0), vd->id())) { e->ann().removeCall(constants().ann.defines_var); vd->ann().remove(constants().ann.is_defined_var); } } }
} else if (vdi != nullptr) { e = vdi->e()->e(); if (e == nullptr) { return; } if (Id* id = e->dynamicCast<Id>()) { assert(id->decl() == vd); if (vdi->e()->ti()->domain() == nullptr) { vdi->e()->ti()->domain(constants().boollit(isTrue)); vardeclQueue.push_back(env.varOccurrences.idx.find(vdi->e()->id())->second); } else if (id->decl()->ti()->domain() == constants().boollit(!isTrue)) { env.fail(); remove = false; } return; } } if (Id* ident = e->dynamicCast<Id>()) { assert(ident->decl() == vd); return; } if (e->isa<BoolLit>()) { if (e == constants().literalTrue && (ci != nullptr)) { toRemove.push_back(ci); } return; } Call* c = e->cast<Call>(); if (c->id() == constants().ids.bool_eq) { Expression* b0 = c->arg(0); Expression* b1 = c->arg(1); int b0s = bool_state(env, b0); int b1s = bool_state(env, b1); if (b0s == 2) { std::swap(b0, b1); std::swap(b0s, b1s); } assert(b0s != 2); if ((ci != nullptr) || vdi->e()->ti()->domain() == constants().literalTrue) { if (b0s != b1s) { if (b1s == 2) { b1->cast<Id>()->decl()->ti()->domain(constants().boollit(isTrue)); vardeclQueue.push_back(env.varOccurrences.idx.find(b1->cast<Id>()->decl()->id())->second); if (ci != nullptr) { toRemove.push_back(ci); } } else { env.fail(); remove = false; } } else { if (ci != nullptr) { toRemove.push_back(ci); } } } else if ((vdi != nullptr) && vdi->e()->ti()->domain() == constants().literalFalse) { if (b0s != b1s) { if (b1s == 2) { b1->cast<Id>()->decl()->ti()->domain(constants().boollit(isTrue)); vardeclQueue.push_back(env.varOccurrences.idx.find(b1->cast<Id>()->decl()->id())->second); } } else { env.fail(); remove = false; } } else { remove = false; } } else if (c->id() == constants().ids.forall || c->id() == constants().ids.exists || c->id() == constants().ids.clause) { if (isTrue && c->id() == constants().ids.exists) { if (ci != nullptr) { toRemove.push_back(ci); } else { if (vdi->e()->ti()->domain() == nullptr) { vdi->e()->ti()->domain(constants().literalTrue); vardeclQueue.push_back(env.varOccurrences.idx.find(vdi->e()->id())->second); } else if (vdi->e()->ti()->domain() != constants().literalTrue) { env.fail(); vdi->e()->e(constants().literalTrue); } } } else if (!isTrue && c->id() == constants().ids.forall) { if (ci != nullptr) { env.fail(); toRemove.push_back(ci); } else { if (vdi->e()->ti()->domain() == nullptr) { vdi->e()->ti()->domain(constants().literalFalse); vardeclQueue.push_back(env.varOccurrences.idx.find(vdi->e()->id())->second); } else if (vdi->e()->ti()->domain() != constants().literalFalse) { env.fail(); vdi->e()->e(constants().literalFalse); } } } else { int nonfixed = decrement_non_fixed_vars(nonFixedLiteralCount, c); bool isConjunction = (c->id() == constants().ids.forall); assert(nonfixed >= 0); if (nonfixed <= 1) { bool subsumed = false; int nonfixed_i = -1; int nonfixed_j = -1; int realNonFixed = 0; for (unsigned int i = 0; i < c->argCount(); i++) { bool unit = (i == 0 ? isConjunction : !isConjunction); auto* al = follow_id(c->arg(i))->cast<ArrayLit>(); realNonFixed += static_cast<int>(al->size()); for (unsigned int j = al->size(); (j--) != 0U;) { if ((*al)[j]->type().isPar() || ((*al)[j]->cast<Id>()->decl()->ti()->domain() != nullptr)) { realNonFixed--; } if ((*al)[j]->type().isPar() && eval_bool(env, (*al)[j]) != unit) { subsumed = true; i = 2; // break out of outer loop break; } if (Id* id = (*al)[j]->dynamicCast<Id>()) { if (id->decl()->ti()->domain() != nullptr) { bool idv = (id->decl()->ti()->domain() == constants().literalTrue); if (unit != idv) { subsumed = true; i = 2; // break out of outer loop break; } } else { nonfixed_i = static_cast<int>(i); nonfixed_j = static_cast<int>(j); } } } }
if (subsumed) { if (ci != nullptr) { if (isConjunction) { env.fail(); ci->e(constants().literalFalse); } else { toRemove.push_back(ci); } } else { if (vdi->e()->ti()->domain() == nullptr) { vdi->e()->ti()->domain(constants().boollit(!isConjunction)); vardeclQueue.push_back(env.varOccurrences.idx.find(vdi->e()->id())->second); } else if (vdi->e()->ti()->domain() != constants().boollit(!isConjunction)) { env.fail(); vdi->e()->e(constants().boollit(!isConjunction)); } } } else if (realNonFixed == 0) { if (ci != nullptr) { if (isConjunction) { toRemove.push_back(ci); } else { env.fail(); ci->e(constants().literalFalse); } } else { if (vdi->e()->ti()->domain() == nullptr) { vdi->e()->ti()->domain(constants().boollit(isConjunction)); vardeclQueue.push_back(env.varOccurrences.idx.find(vdi->e()->id())->second); } else if (vdi->e()->ti()->domain() != constants().boollit(isConjunction)) { env.fail(); vdi->e()->e(constants().boollit(isConjunction)); } toRemove.push_back(vdi); } } else if (realNonFixed == 1) { // not subsumed, nonfixed==1 assert(nonfixed_i != -1); auto* al = follow_id(c->arg(nonfixed_i))->cast<ArrayLit>(); Id* ident = (*al)[nonfixed_j]->cast<Id>(); if ((ci != nullptr) || (vdi->e()->ti()->domain() != nullptr)) { bool result = nonfixed_i == 0; if ((vdi != nullptr) && vdi->e()->ti()->domain() == constants().literalFalse) { result = !result; } VarDecl* decl = ident->decl(); if (decl->ti()->domain() == nullptr) { decl->ti()->domain(constants().boollit(result)); vardeclQueue.push_back(env.varOccurrences.idx.find(decl->id())->second); } else if (vd->ti()->domain() != constants().boollit(result)) { env.fail(); decl->e(constants().literalTrue); } } else { if (nonfixed_i == 0) { // this is a clause, exists or forall with a single non-fixed variable, // assigned to a non-fixed variable => turn into simple equality vdi->e()->e(nullptr); // Transfer is_defined_var annotation if (ident->decl()->ann().contains(constants().ann.is_defined_var)) { vdi->e()->ann().add(constants().ann.is_defined_var); } else if (vdi->e()->ann().contains(constants().ann.is_defined_var)) { ident->decl()->ann().add(constants().ann.is_defined_var); } unify(env, deletedVarDecls, vdi->e()->id(), ident); push_dependent_constraints(env, ident, constraintQueue); } else { remove = false; } } } else { remove = false; }
} else if (c->id() == constants().ids.clause) { int posOrNeg = isTrue ? 0 : 1; auto* al = follow_id(c->arg(posOrNeg))->cast<ArrayLit>(); auto* al_other = follow_id(c->arg(1 - posOrNeg))->cast<ArrayLit>();
if ((ci != nullptr) && al->size() == 1 && (*al)[0] != vd->id() && al_other->size() == 1) { // simple implication assert((*al_other)[0] == vd->id()); if (ci != nullptr) { if ((*al)[0]->type().isPar()) { if (eval_bool(env, (*al)[0]) == isTrue) { toRemove.push_back(ci); } else { env.fail(); remove = false; } } else { Id* id = (*al)[0]->cast<Id>(); if (id->decl()->ti()->domain() == nullptr) { id->decl()->ti()->domain(constants().boollit(isTrue)); vardeclQueue.push_back(env.varOccurrences.idx.find(id->decl()->id())->second); } else { if (id->decl()->ti()->domain() == constants().boollit(isTrue)) { toRemove.push_back(ci); } else { env.fail(); remove = false; } } } } } else { // proper clause for (unsigned int i = 0; i < al->size(); i++) { if ((*al)[i] == vd->id()) { if (ci != nullptr) { toRemove.push_back(ci); } else { if (vdi->e()->ti()->domain() == nullptr) { vdi->e()->ti()->domain(constants().literalTrue); vardeclQueue.push_back(env.varOccurrences.idx.find(vdi->e()->id())->second); } else if (vdi->e()->ti()->domain() != constants().literalTrue) { env.fail(); vdi->e()->e(constants().literalTrue); } } break; } } } } } } else { remove = false; }}
} // namespace MiniZinc