1 // {{{ MIT License
2
3 // Copyright 2017 Roland Kaminski
4
5 // Permission is hereby granted, free of charge, to any person obtaining a copy
6 // of this software and associated documentation files (the "Software"), to
7 // deal in the Software without restriction, including without limitation the
8 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
9 // sell copies of the Software, and to permit persons to whom the Software is
10 // furnished to do so, subject to the following conditions:
11
12 // The above copyright notice and this permission notice shall be included in
13 // all copies or substantial portions of the Software.
14
15 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
20 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
21 // IN THE SOFTWARE.
22
23 // }}}
24
25 #include "gringo/bug.hh"
26 #include "gringo/logger.hh"
27 #include "gringo/input/aggregate.hh"
28
29 namespace Gringo { namespace Input {
30
31 // {{{ definition of AssignLevel
32
add(VarTermBoundVec & vars)33 void AssignLevel::add(VarTermBoundVec &vars) {
34 for (auto &occ : vars) { occurr[occ.first->ref].emplace_back(occ.first); }
35 }
subLevel()36 AssignLevel &AssignLevel::subLevel() {
37 childs.emplace_front();
38 return childs.front();
39 }
assignLevels()40 void AssignLevel::assignLevels() {
41 BoundSet bound;
42 assignLevels(0, bound);
43 }
assignLevels(unsigned level,BoundSet const & parent)44 void AssignLevel::assignLevels(unsigned level, BoundSet const &parent) {
45 BoundSet bound(parent);
46 for (auto &occs : occurr) {
47 unsigned l = bound.emplace(occs.first, level).first->second;
48 for (auto &occ : occs.second) { occ->level = l; }
49 }
50 for (auto &child : childs) { child.assignLevels(level + 1, bound); }
51 }
~AssignLevel()52 AssignLevel::~AssignLevel() { }
53
54 // }}}
55 // {{{ definition of CheckLevel
56
operator <(Ent const &) const57 bool CheckLevel::Ent::operator<(Ent const &) const { return false; }
CheckLevel(Location const & loc,Printable const & p)58 CheckLevel::CheckLevel(Location const &loc, Printable const &p) : loc(loc), p(p) { }
59 CheckLevel::CheckLevel(CheckLevel &&) = default;
var(VarTerm & var)60 CheckLevel::SC::VarNode &CheckLevel::var(VarTerm &var) {
61 auto &node = vars[var.name];
62 if (!node) { node = &dep.insertVar(&var); }
63 return *node;
64 }
check(Logger & log)65 void CheckLevel::check(Logger &log) {
66 dep.order();
67 auto vars(dep.open());
68 if (!vars.empty()) {
69 auto cmp = [](SC::VarNode const *x, SC::VarNode const *y) -> bool{
70 if (x->data->name != y->data->name) { return x->data->name < y->data->name; }
71 return x->data->loc() < y->data->loc();
72 };
73 std::sort(vars.begin(), vars.end(), cmp);
74 std::ostringstream msg;
75 msg << loc << ": error: unsafe variables in:\n " << p << "\n";
76 for (auto &x : vars) { msg << x->data->loc() << ": note: '" << x->data->name << "' is unsafe\n"; }
77 GRINGO_REPORT(log, Warnings::RuntimeError) << msg.str();
78 }
79 }
~CheckLevel()80 CheckLevel::~CheckLevel() { }
81
addVars(ChkLvlVec & levels,VarTermBoundVec & vars)82 void addVars(ChkLvlVec &levels, VarTermBoundVec &vars) {
83 for (auto &x: vars) {
84 auto &lvl(levels[x.first->level]);
85 bool bind = x.second && levels.size() == x.first->level + 1;
86 if (bind) { lvl.dep.insertEdge(*lvl.current, lvl.var(*x.first)); }
87 else { lvl.dep.insertEdge(lvl.var(*x.first), *lvl.current); }
88 }
89 }
90
91 // }}}
92 // {{{ declaration of ToGroundArg
93
ToGroundArg(unsigned & auxNames,DomainData & domains)94 ToGroundArg::ToGroundArg(unsigned &auxNames, DomainData &domains)
95 : auxNames(auxNames)
96 , domains(domains) { }
newId(bool increment)97 String ToGroundArg::newId(bool increment) {
98 auxNames+= increment;
99 return ("#d" + std::to_string(auxNames-increment)).c_str();
100 }
getGlobal(VarTermBoundVec const & vars)101 UTermVec ToGroundArg::getGlobal(VarTermBoundVec const &vars) {
102 std::unordered_set<String> seen;
103 UTermVec global;
104 for (auto &occ : vars) {
105 if (occ.first->level == 0 && seen.emplace(occ.first->name).second) {
106 global.emplace_back(occ.first->clone());
107 }
108 }
109 return global;
110 }
getLocal(VarTermBoundVec const & vars)111 UTermVec ToGroundArg::getLocal(VarTermBoundVec const &vars) {
112 std::unordered_set<String> seen;
113 UTermVec local;
114 for (auto &occ : vars) {
115 if (occ.first->level != 0 && seen.emplace(occ.first->name).second) {
116 local.emplace_back(occ.first->clone());
117 }
118 }
119 return local;
120 }
newId(UTermVec && global,Location const & loc,bool increment)121 UTerm ToGroundArg::newId(UTermVec &&global, Location const &loc, bool increment) {
122 if (!global.empty()) { return make_locatable<FunctionTerm>(loc, newId(increment), std::move(global)); }
123 else { return make_locatable<ValTerm>(loc, Symbol::createId(newId(increment))); }
124 }
~ToGroundArg()125 ToGroundArg::~ToGroundArg() { }
126
127 // }}}
128
printWithCondition(std::ostream & out,UBodyAggrVec const & condition) const129 void HeadAggregate::printWithCondition(std::ostream &out, UBodyAggrVec const &condition) const {
130 out << *this;
131 if (!condition.empty()) {
132 out << ":-";
133 auto f = [](std::ostream &out, UBodyAggr const &x) { out << *x; };
134 print_comma(out, condition, ";", f);
135 }
136 out << ".";
137 }
138
139 } } // namespace Input Gringo
140