1 //
2 // Copyright (c) 2013-2017 Benjamin Kaufmann
3 //
4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
5 //
6 // Permission is hereby granted, free of charge, to any person obtaining a copy
7 // of this software and associated documentation files (the "Software"), to
8 // deal in the Software without restriction, including without limitation the
9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
10 // sell copies of the Software, and to permit persons to whom the Software is
11 // furnished to do so, subject to the following conditions:
12 //
13 // The above copyright notice and this permission notice shall be included in
14 // all copies or substantial portions of the Software.
15 //
16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
22 // IN THE SOFTWARE.
23 //
24 #include <clasp/logic_program.h>
25 #include <clasp/shared_context.h>
26 #include <clasp/solver.h>
27 #include <clasp/minimize_constraint.h>
28 #include <clasp/util/misc_types.h>
29 #include <clasp/asp_preprocessor.h>
30 #include <clasp/clause.h>
31 #include <clasp/dependency_graph.h>
32 #include <clasp/parser.h>
33 #include <potassco/theory_data.h>
34 #include <potassco/string_convert.h>
35 #include <stdexcept>
36 #include <cctype>
37 #include <cstdio>
38 namespace Clasp { namespace Asp {
39 /////////////////////////////////////////////////////////////////////////////////////////
40 // Statistics
41 /////////////////////////////////////////////////////////////////////////////////////////
42 #define RK(x) RuleStats::x
toStr(int k)43 const char* RuleStats::toStr(int k) {
44 POTASSCO_ASSERT(k >= 0 && uint32(k) <= numKeys(), "Invalid key");
45 switch (k) {
46 case Normal : return "Normal";
47 case Choice : return "Choice";
48 case Minimize : return "Minimize";
49 case Acyc : return "Acyc";
50 case Heuristic: return "Heuristic";
51 default: return "None";
52 }
53 }
sum() const54 uint32 RuleStats::sum() const {
55 return std::accumulate(key, key + numKeys(), uint32(0));
56 }
toStr(int t)57 const char* BodyStats::toStr(int t) {
58 POTASSCO_ASSERT(t >= 0 && uint32(t) < numKeys(), "Invalid body type!");
59 switch (t) {
60 default : return "Normal";
61 case Body_t::Count: return "Count";
62 case Body_t::Sum : return "Sum";
63 }
64 }
sum() const65 uint32 BodyStats::sum() const {
66 return std::accumulate(key, key + numKeys(), uint32(0));
67 }
68
69 namespace {
70 template <unsigned i>
sumBodies(const LpStats * self)71 double sumBodies(const LpStats* self) { return self->bodies[i].sum(); }
72 template <unsigned i>
sumRules(const LpStats * self)73 double sumRules(const LpStats* self) { return self->rules[i].sum(); }
sumEqs(const LpStats * self)74 double sumEqs(const LpStats* self) { return self->eqs(); }
75 }
76 #define LP_STATS( APPLY ) \
77 APPLY("atoms" , VALUE(atoms)) \
78 APPLY("atoms_aux" , VALUE(auxAtoms)) \
79 APPLY("disjunctions" , VALUE(disjunctions[0])) \
80 APPLY("disjunctions_non_hcf", VALUE(disjunctions[1])) \
81 APPLY("bodies" , FUNC(sumBodies<0>)) \
82 APPLY("bodies_tr" , FUNC(sumBodies<1>)) \
83 APPLY("sum_bodies" , VALUE(bodies[0][Body_t::Sum])) \
84 APPLY("sum_bodies_tr" , VALUE(bodies[1][Body_t::Sum])) \
85 APPLY("count_bodies" , VALUE(bodies[0][Body_t::Count]))\
86 APPLY("count_bodies_tr" , VALUE(bodies[1][Body_t::Count]))\
87 APPLY("sccs" , VALUE(sccs)) \
88 APPLY("sccs_non_hcf" , VALUE(nonHcfs)) \
89 APPLY("gammas" , VALUE(gammas)) \
90 APPLY("ufs_nodes" , VALUE(ufsNodes)) \
91 APPLY("rules" , FUNC(sumRules<0>)) \
92 APPLY("rules_normal" , VALUE(rules[0][RK(Normal)])) \
93 APPLY("rules_choice" , VALUE(rules[0][RK(Choice)])) \
94 APPLY("rules_minimize" , VALUE(rules[0][RK(Minimize)])) \
95 APPLY("rules_acyc" , VALUE(rules[0][RK(Acyc)])) \
96 APPLY("rules_heuristic" , VALUE(rules[0][RK(Heuristic)]))\
97 APPLY("rules_tr" , FUNC(sumRules<1>)) \
98 APPLY("rules_tr_normal" , VALUE(rules[1][RK(Normal)])) \
99 APPLY("rules_tr_choice" , VALUE(rules[1][RK(Choice)])) \
100 APPLY("rules_tr_minimize" , VALUE(rules[1][RK(Minimize)])) \
101 APPLY("rules_tr_acyc" , VALUE(rules[1][RK(Acyc)])) \
102 APPLY("rules_tr_heuristic" , VALUE(rules[1][RK(Heuristic)]))\
103 APPLY("eqs" , FUNC(sumEqs)) \
104 APPLY("eqs_atom" , VALUE(eqs_[Var_t::Atom-1])) \
105 APPLY("eqs_body" , VALUE(eqs_[Var_t::Body-1])) \
106 APPLY("eqs_other" , VALUE(eqs_[Var_t::Hybrid-1]))
107
reset()108 void LpStats::reset() {
109 std::memset(this, 0, sizeof(LpStats));
110 }
111
accu(const LpStats & o)112 void LpStats::accu(const LpStats& o) {
113 atoms += o.atoms;
114 auxAtoms += o.auxAtoms;
115 ufsNodes += o.ufsNodes;
116 if (sccs == PrgNode::noScc || o.sccs == PrgNode::noScc) {
117 sccs = o.sccs;
118 nonHcfs = o.nonHcfs;
119 }
120 else {
121 sccs += o.sccs;
122 nonHcfs+= o.nonHcfs;
123 }
124 for (int i = 0; i != 2; ++i) {
125 disjunctions[i] += o.disjunctions[i];
126 for (uint32 k = 0; k != BodyStats::numKeys(); ++k) {
127 bodies[i][k] += o.bodies[i][k];
128 }
129 for (uint32 k = 0; k != RuleStats::numKeys(); ++k) {
130 rules[i][k] += o.rules[i][k];
131 }
132 }
133 for (int i = 0; i != sizeof(eqs_)/sizeof(eqs_[0]); ++i) {
134 eqs_[i] += o.eqs_[i];
135 }
136 }
137
138 static const char* lpStats_s[] = {
139 #define KEY(x, y) x,
140 LP_STATS(KEY)
141 #undef KEY
142 "lp"
143 };
size()144 uint32 LpStats::size() {
145 return (sizeof(lpStats_s)/sizeof(const char*))-1;
146 }
key(uint32 i)147 const char* LpStats::key(uint32 i) {
148 return i < size() ? lpStats_s[i] : throw std::out_of_range(POTASSCO_FUNC_NAME);
149 }
at(const char * k) const150 StatisticObject LpStats::at(const char* k) const {
151 #define MAP_IF(x, A) if (std::strcmp(k, x) == 0) return A;
152 #define VALUE(X) StatisticObject::value(&(X))
153 #define FUNC(F) StatisticObject::value<LpStats, F>(this)
154 LP_STATS(MAP_IF)
155 #undef VALUE
156 #undef FUNC
157 #undef MAP_IF
158 throw std::out_of_range(POTASSCO_FUNC_NAME);
159 }
160 #undef LP_STATS
161 /////////////////////////////////////////////////////////////////////////////////////////
162 // class LogicProgram
163 /////////////////////////////////////////////////////////////////////////////////////////
164 static PrgAtom trueAtom_g(0, false);
165 static const uint32 falseId = PrgNode::noNode;
166 static const uint32 bodyId = PrgNode::noNode + 1;
167 static bool init_trueAtom_g = (trueAtom_g.setEq(0), true);
isAtom(Id_t uid)168 inline bool isAtom(Id_t uid) { return Potassco::atom(Potassco::lit(uid)) < bodyId; }
isBody(Id_t uid)169 inline bool isBody(Id_t uid) { return Potassco::atom(Potassco::lit(uid)) >= bodyId; }
nodeId(Id_t uid)170 inline Id_t nodeId(Id_t uid) { return Potassco::atom(Potassco::lit(uid)) - (isAtom(uid) ? 0 : bodyId); }
signId(Id_t uid)171 inline bool signId(Id_t uid) { return Potassco::lit(uid) < 0; }
172
173 namespace {
174 typedef std::pair<Atom_t, Potassco::Value_t> AtomVal;
encodeExternal(Atom_t a,Potassco::Value_t value)175 inline uint32 encodeExternal(Atom_t a, Potassco::Value_t value) {
176 return (a << 2) | static_cast<uint32>(value);
177 }
decodeExternal(uint32 x)178 inline AtomVal decodeExternal(uint32 x) {
179 return AtomVal(x >> 2, static_cast<Potassco::Value_t>(x & 3u));
180 }
181 struct LessBodySize {
LessBodySizeClasp::Asp::__anon66151f780211::LessBodySize182 LessBodySize(const BodyList& bl) : bodies_(&bl) {}
operator ()Clasp::Asp::__anon66151f780211::LessBodySize183 bool operator()(Id_t b1, Id_t b2 ) const {
184 return (*bodies_)[b1]->size() < (*bodies_)[b2]->size()
185 || ((*bodies_)[b1]->size() == (*bodies_)[b2]->size() && (*bodies_)[b1]->type() < (*bodies_)[b2]->type());
186 }
187 private:
188 const BodyList* bodies_;
189 };
190 // Adds nogoods representing this node to the solver.
191 template <class NT>
toConstraint(NT * node,const LogicProgram & prg,ClauseCreator & c)192 bool toConstraint(NT* node, const LogicProgram& prg, ClauseCreator& c) {
193 if (node->value() != value_free && !prg.ctx()->addUnary(node->trueLit())) {
194 return false;
195 }
196 return !node->relevant() || node->addConstraints(prg, c);
197 }
198 }
199
LogicProgram()200 LogicProgram::LogicProgram() : theory_(0), input_(1, UINT32_MAX), auxData_(0), incData_(0) {
201 POTASSCO_ASSERT(init_trueAtom_g, "invalid static init");
202 }
~LogicProgram()203 LogicProgram::~LogicProgram() { dispose(true); }
Incremental()204 LogicProgram::Incremental::Incremental() : startScc(0) {}
dispose(bool force)205 void LogicProgram::dispose(bool force) {
206 // remove rules
207 std::for_each(bodies_.begin(), bodies_.end(), DestroyObject());
208 std::for_each(disjunctions_.begin(), disjunctions_.end(), DestroyObject());
209 std::for_each(extended_.begin(), extended_.end(), DeleteObject());
210 std::for_each(minimize_.begin(), minimize_.end(), DeleteObject());
211 PodVector<ShowPair>::destruct(show_);
212 delete auxData_; auxData_ = 0;
213 MinList().swap(minimize_);
214 RuleList().swap(extended_);
215 BodyList().swap(bodies_);
216 DisjList().swap(disjunctions_);
217 bodyIndex_.clear();
218 disjIndex_.clear();
219 VarVec().swap(initialSupp_);
220 if (theory_) {
221 theory_->reset();
222 }
223 if (force || !incData_) {
224 deleteAtoms(0);
225 AtomList().swap(atoms_);
226 AtomState().swap(atomState_);
227 delete theory_;
228 delete incData_;
229 VarVec().swap(propQ_);
230 stats.reset();
231 incData_ = 0;
232 theory_ = 0;
233 input_ = AtomRange(1, UINT32_MAX);
234 statsId_ = 0;
235 }
236 rule_.clear();
237 }
deleteAtoms(uint32 start)238 void LogicProgram::deleteAtoms(uint32 start) {
239 for (AtomList::const_iterator it = atoms_.begin() + start, end = atoms_.end(); it != end; ++it) {
240 if (*it != &trueAtom_g) { delete *it; }
241 }
242 }
doStartProgram()243 bool LogicProgram::doStartProgram() {
244 dispose(true);
245 // atom 0 is always true
246 PrgAtom* trueAt = new PrgAtom(0, false);
247 atoms_.push_back(trueAt);
248 trueAt->assignValue(value_true);
249 trueAt->setInUpper(true);
250 trueAt->setLiteral(lit_true());
251 atomState_.set(0, AtomState::fact_flag);
252 auxData_ = new Aux();
253 return true;
254 }
setOptions(const AspOptions & opts)255 void LogicProgram::setOptions(const AspOptions& opts) {
256 opts_ = opts;
257 if (opts.suppMod) { opts_.noSCC = 1; }
258 if (opts.suppMod && ctx() && ctx()->sccGraph.get()) {
259 ctx()->warn("'supp-models' ignored for non-tight programs.");
260 opts_.suppMod = 0;
261 opts_.noSCC = 0;
262 }
263 }
enableDistinctTrue()264 void LogicProgram::enableDistinctTrue() {
265 opts_.distinctTrue();
266 }
doCreateParser()267 ProgramParser* LogicProgram::doCreateParser() {
268 return new AspParser(*this);
269 }
doUpdateProgram()270 bool LogicProgram::doUpdateProgram() {
271 if (!incData_) { incData_ = new Incremental(); }
272 if (!frozen()) { return true; }
273 // delete bodies/disjunctions...
274 dispose(false);
275 setFrozen(false);
276 auxData_ = new Aux();
277 if (theory_) { theory_->update(); }
278 incData_->unfreeze.clear();
279 input_.hi = std::min(input_.hi, endAtom());
280 // reset prop queue and add supported atoms from previous steps
281 // {ai | ai in P}.
282 PrgBody* support = input_.hi > 1 ? getTrueBody() : 0;
283 propQ_.clear();
284 for (Atom_t i = 1, end = startAuxAtom(); i != end; ++i) {
285 if (getRootId(i) >= end) {
286 // atom is equivalent to some aux atom - make i the new root
287 uint32 r = getRootId(i);
288 std::swap(atoms_[i], atoms_[r]);
289 atoms_[r]->setEq(i);
290 }
291 // remove dangling references
292 PrgAtom* a = atoms_[i];
293 a->clearSupports();
294 a->clearDeps(PrgAtom::dep_all);
295 a->setIgnoreScc(false);
296 if (a->relevant() || a->frozen()) {
297 ValueRep v = a->value();
298 a->setValue(value_free);
299 a->resetId(i, !a->frozen());
300 if (ctx()->master()->value(a->var()) != value_free && !a->frozen()) {
301 v = ctx()->master()->isTrue(a->literal()) ? value_true : value_false;
302 }
303 if (v != value_free) { assignValue(a, v, PrgEdge::noEdge()); }
304 if (!a->frozen() && a->value() != value_false) {
305 a->setIgnoreScc(true);
306 support->addHead(a, PrgEdge::GammaChoice);
307 }
308 }
309 else if (a->removed() || (!a->eq() && a->value() == value_false)) {
310 a->resetId(i, true);
311 a->setValue(value_false);
312 atomState_.set(i, AtomState::false_flag);
313 }
314 }
315 // delete any introduced aux atoms
316 // this is safe because aux atoms are never part of the input program
317 // it is necessary in order to free their ids, i.e. the id of an aux atom
318 // from step I might be needed for a program atom in step I+1
319 deleteAtoms(startAuxAtom());
320 atoms_.erase(atoms_.begin()+startAuxAtom(), atoms_.end());
321 uint32 nAtoms = (uint32)atoms_.size();
322 atomState_.resize(nAtoms);
323 input_ = AtomRange(nAtoms, UINT32_MAX);
324 stats.reset();
325 statsId_ = 0;
326 return true;
327 }
doEndProgram()328 bool LogicProgram::doEndProgram() {
329 if (!frozen() && ctx()->ok()) {
330 prepareProgram(!opts_.noSCC);
331 addConstraints();
332 addDomRules();
333 addAcycConstraint();
334 }
335 return ctx()->ok();
336 }
337
clone(SharedContext & oCtx)338 bool LogicProgram::clone(SharedContext& oCtx) {
339 assert(frozen());
340 if (&oCtx == ctx()) {
341 return true;
342 }
343 for (Var v = oCtx.numVars() + 1; ctx()->validVar(v); ++v) {
344 oCtx.addVar(Var_t::Atom, ctx()->varInfo(v).rep);
345 }
346 SharedContext* t = ctx();
347 setCtx(&oCtx);
348 bool ok = addConstraints();
349 if (ok) {
350 oCtx.output = ctx()->output;
351 oCtx.heuristic = t->heuristic;
352 }
353 setCtx(t);
354 return ok;
355 }
356
addMinimize()357 void LogicProgram::addMinimize() {
358 POTASSCO_ASSERT(frozen());
359 for (MinList::iterator it = minimize_.begin(), end = minimize_.end(); it != end; ++it) {
360 const LpWLitVec& lits = (*it)->lits;
361 const weight_t prio = (*it)->prio;
362 for (LpWLitVec::const_iterator xIt = lits.begin(), xEnd = lits.end(); xIt != xEnd; ++xIt) {
363 addMinLit(prio, WeightLiteral(getLiteral(Potassco::id(xIt->lit)), xIt->weight));
364 }
365 // Make sure minimize constraint is not empty
366 if (lits.empty()) addMinLit(prio, WeightLiteral(lit_false(), 1));
367 }
368 }
outRule(Potassco::AbstractProgram & out,const Rule & r)369 static void outRule(Potassco::AbstractProgram& out, const Rule& r) {
370 if (r.normal()) { out.rule(r.ht, r.head, r.cond); }
371 else { out.rule(r.ht, r.head, r.agg.bound, r.agg.lits); }
372 }
373
accept(Potassco::AbstractProgram & out)374 void LogicProgram::accept(Potassco::AbstractProgram& out) {
375 if (!ok()) {
376 out.rule(Head_t::Disjunctive, Potassco::toSpan<Potassco::Atom_t>(), Potassco::toSpan<Potassco::Lit_t>());
377 return;
378 }
379 // visit external directives
380 for (VarVec::const_iterator it = auxData_->external.begin(), end = auxData_->external.end(); it != end; ++it) {
381 AtomVal x = decodeExternal(*it);
382 out.external(x.first, x.second);
383 }
384 // visit eq- and assigned atoms
385 for (Atom_t i = startAtom(); i < atoms_.size(); ++i) {
386 if (atoms_[i]->eq()) {
387 Potassco::AtomSpan head = Potassco::toSpan(&i, 1);
388 Potassco::Lit_t body = Potassco::lit(getRootId(i));
389 if (isFact(Potassco::atom(body))) {
390 out.rule(Head_t::Disjunctive, head, Potassco::toSpan<Potassco::Lit_t>());
391 }
392 else if (inProgram(Potassco::atom(body))) {
393 out.rule(Head_t::Disjunctive, head, Potassco::toSpan(&body, 1));
394 }
395 }
396 else if (!atomState_.isFact(i) && atoms_[i]->value() != value_free) {
397 Potassco::AtomSpan head = Potassco::toSpan<Potassco::Atom_t>();
398 Potassco::Lit_t body = Potassco::neg(i);
399 if (atoms_[i]->value() != value_false) {
400 out.rule(Head_t::Disjunctive, head, Potassco::toSpan(&body, 1));
401 }
402 else if (inProgram(i)) {
403 body = Potassco::neg(body);
404 out.rule(Head_t::Disjunctive, head, Potassco::toSpan(&body, 1));
405 }
406 }
407 }
408 // visit program rules
409 const bool simp = frozen();
410 using Potassco::Lit_t;
411 VarVec choice;
412 for (BodyList::iterator bIt = bodies_.begin(); bIt != bodies_.end(); ++bIt) {
413 rule_.clear();
414 choice.clear();
415 Atom_t head;
416 Lit_t auxB;
417 PrgBody* b = *bIt;
418 if (b->relevant() && (b->inRule() || b->value() == value_false) && b->toData(*this, rule_)) {
419 if (b->value() == value_false) {
420 outRule(out, rule_.rule());
421 continue;
422 }
423 uint32 numDis = 0;
424 Rule r = rule_.rule();
425 for (PrgBody::head_iterator hIt = b->heads_begin(); hIt != b->heads_end(); ++hIt) {
426 if (hIt->isGamma() || (simp && !getHead(*hIt)->hasVar())) { continue; }
427 if (hIt->isAtom() && hIt->node() && inProgram(hIt->node())) {
428 if (hIt->isNormal()) { r.head = Potassco::toSpan(&(head = hIt->node()), 1); outRule(out, r); }
429 else if (hIt->isChoice()) { choice.push_back(hIt->node()); }
430 if (simp && getRootAtom(hIt->node())->var() == b->var() && !r.normal()) {
431 // replace complex body with head atom
432 auxB = Potassco::lit(hIt->node());
433 if (getRootAtom(hIt->node())->literal() != b->literal()) { auxB *= -1; }
434 r.bt = Body_t::Normal;
435 r.cond = Potassco::toSpan(&auxB, 1);
436 }
437 }
438 else if (hIt->isDisj()) { ++numDis; }
439 }
440 if (!choice.empty()) {
441 r.head = Potassco::toSpan(choice);
442 r.ht = Head_t::Choice;
443 outRule(out, r);
444 }
445 for (PrgBody::head_iterator hIt = b->heads_begin(); hIt != b->heads_end() && numDis; ++hIt) {
446 if (hIt->isDisj()) {
447 PrgDisj* d = getDisj(hIt->node());
448 r.head = Potassco::toSpan(d->begin(), d->size());
449 r.ht = Head_t::Disjunctive;
450 outRule(out, r);
451 --numDis;
452 }
453 }
454 }
455 }
456 LpWLitVec wlits;
457 for (MinList::iterator it = minimize_.begin(), end = minimize_.end(); it != end; ++it) {
458 Potassco::WeightLitSpan ws = Potassco::toSpan((*it)->lits);
459 for (const Potassco::WeightLit_t* x = Potassco::begin(ws), *xEnd = Potassco::end(ws); x != xEnd; ++x) {
460 if (x->weight == 0 || !inProgram(Potassco::atom(*x))) { // simplify literals
461 wlits.assign(Potassco::begin(ws), x);
462 for (; x != xEnd; ++x) {
463 if (x->weight != 0 && (x->weight < 0 || x->lit < 0 || inProgram(Potassco::atom(*x)))) {
464 wlits.push_back(*x);
465 }
466 }
467 ws = Potassco::toSpan(wlits);
468 break;
469 }
470 }
471 out.minimize((*it)->prio, ws);
472 }
473 Potassco::LitVec lits;
474 // visit output directives
475 for (ShowVec::const_iterator it = show_.begin(); it != show_.end(); ++it) {
476 if (extractCondition(it->first, lits)) {
477 out.output(Potassco::toSpan(it->second.c_str(), std::strlen(it->second.c_str())), Potassco::toSpan(lits));
478 }
479 }
480 // visit projection directives
481 if (!auxData_->project.empty()) {
482 out.project(auxData_->project.back() ? Potassco::toSpan(auxData_->project) : Potassco::toSpan<Atom_t>());
483 }
484 // visit assumptions
485 if (!auxData_->assume.empty()) {
486 out.assume(Potassco::toSpan(auxData_->assume));
487 }
488 // visit heuristics
489 if (!auxData_->dom.empty()) {
490 for (DomRules::const_iterator it = auxData_->dom.begin(), end = auxData_->dom.end(); it != end; ++it) {
491 if (extractCondition(it->cond, lits)) {
492 out.heuristic(it->atom, static_cast<DomModType>(it->type), it->bias, it->prio, Potassco::toSpan(lits));
493 }
494 }
495 }
496 // visit acyc edges
497 if (!auxData_->acyc.empty()) {
498 for (AcycRules::const_iterator it = auxData_->acyc.begin(), end = auxData_->acyc.end(); it != end; ++it) {
499 if (extractCondition(it->cond, lits)) {
500 out.acycEdge(it->node[0], it->node[1], Potassco::toSpan(lits));
501 }
502 }
503 }
504 if (theory_ && theory_->numAtoms()) {
505 struct This : public Potassco::TheoryData::Visitor {
506 This(const Asp::LogicProgram& p, Potassco::AbstractProgram& o, Potassco::LitVec& c) : self(&p), out(&o), cond(&c) {}
507 virtual void visit(const Potassco::TheoryData& data, Potassco::Id_t termId, const Potassco::TheoryTerm& t) {
508 if (!addSeen(termId, 1)) { return; }
509 data.accept(t, *this, Potassco::TheoryData::visit_current);
510 Potassco::print(*out, termId, t);
511 }
512 virtual void visit(const Potassco::TheoryData& data, Potassco::Id_t elemId, const Potassco::TheoryElement& e) {
513 if (!addSeen(elemId, 2)) { return; }
514 data.accept(e, *this, Potassco::TheoryData::visit_current);
515 cond->clear();
516 if (e.condition()) { self->extractCondition(e.condition(), *cond); }
517 out->theoryElement(elemId, e.terms(), Potassco::toSpan(*cond));
518 }
519 virtual void visit(const Potassco::TheoryData& data, const Potassco::TheoryAtom& a) {
520 data.accept(a, *this, Potassco::TheoryData::visit_current);
521 Potassco::print(*out, a);
522 const Atom_t id = a.atom();
523 if (self->validAtom(id) && self->atomState_.isSet(id, AtomState::false_flag) && !self->inProgram(id)) {
524 Potassco::Lit_t x = Potassco::lit(id);
525 out->rule(Head_t::Disjunctive, Potassco::toSpan<Potassco::Atom_t>(), Potassco::toSpan(&x, 1));
526 }
527 }
528 bool addSeen(Potassco::Id_t id, unsigned char n) {
529 if (id >= seen.size()) { seen.resize(id + 1, 0); }
530 unsigned char old = seen[id];
531 return (seen[id] |= n) != old;
532 }
533 typedef PodVector<unsigned char>::type IdSet;
534 const Asp::LogicProgram* self;
535 Potassco::AbstractProgram* out;
536 Potassco::LitVec* cond;
537 IdSet seen;
538 } self(*this, out, lits);
539 theory_->accept(self, Potassco::TheoryData::visit_current);
540 }
541 }
542 /////////////////////////////////////////////////////////////////////////////////////////
543 // Program mutating functions
544 /////////////////////////////////////////////////////////////////////////////////////////
545 #define check_not_frozen() POTASSCO_REQUIRE(!frozen(), "Can't update frozen program!")
546 #define check_modular(x, atomId) (void)( (!!(x)) || (throw RedefinitionError((atomId), this->findName((atomId))), 0))
RedefinitionError(unsigned atomId,const char * name)547 RedefinitionError::RedefinitionError(unsigned atomId, const char* name)
548 : std::logic_error(POTASSCO_FORMAT("redefinition of atom <'%s',%u>", name && *name ? name : "_", atomId)) {
549 }
550
newAtom()551 Atom_t LogicProgram::newAtom() {
552 check_not_frozen();
553 Atom_t id = static_cast<Atom_t>(atoms_.size());
554 atoms_.push_back( new PrgAtom(id) );
555 return id;
556 }
newCondition(const Potassco::LitSpan & cond)557 Id_t LogicProgram::newCondition(const Potassco::LitSpan& cond) {
558 check_not_frozen();
559 SRule meta;
560 if (simplifyNormal(Head_t::Disjunctive, Potassco::toSpan<Potassco::Atom_t>(), cond, rule_, meta)) {
561 Rule r = rule_.rule();
562 if (r.cond.size == 0) { return 0; }
563 if (r.cond.size == 1) { return Potassco::id(r.cond[0]); }
564 PrgBody* b = getBodyFor(r, meta);
565 b->markFrozen();
566 return static_cast<Id_t>(Clasp::Asp::bodyId | b->id());
567 }
568 return static_cast<Id_t>(Clasp::Asp::falseId);
569 }
addOutput(const ConstString & str,const Potassco::LitSpan & cond)570 LogicProgram& LogicProgram::addOutput(const ConstString& str, const Potassco::LitSpan& cond) {
571 if (cond.size == 1) {
572 POTASSCO_REQUIRE(Potassco::atom(cond[0]) < bodyId, "Atom out of bounds");
573 return addOutput(str, Potassco::id(cond[0]));
574 }
575 if (!ctx()->output.filter(str)) {
576 show_.push_back(ShowPair(newCondition(cond), str));
577 }
578 return *this;
579 }
addOutput(const ConstString & str,Id_t id)580 LogicProgram& LogicProgram::addOutput(const ConstString& str, Id_t id) {
581 if (!ctx()->output.filter(str) && id != falseId) {
582 if (Potassco::atom(id) < bodyId) {
583 resize(Potassco::atom(id));
584 }
585 show_.push_back(ShowPair(id, str));
586 }
587 return *this;
588 }
589
addProject(const Potassco::AtomSpan & atoms)590 LogicProgram& LogicProgram::addProject(const Potassco::AtomSpan& atoms) {
591 check_not_frozen();
592 VarVec& pro = auxData_->project;
593 if (!Potassco::empty(atoms)) {
594 if (!pro.empty() && pro.back() == 0) { pro.pop_back(); }
595 pro.insert(pro.end(), Potassco::begin(atoms), Potassco::end(atoms));
596 }
597 else if (pro.empty()) {
598 pro.push_back(0);
599 }
600 return *this;
601 }
602
theoryData()603 TheoryData& LogicProgram::theoryData() {
604 if (!theory_) { theory_ = new TheoryData(); }
605 return *theory_;
606 }
607
pushFrozen(PrgAtom * atom,ValueRep value)608 void LogicProgram::pushFrozen(PrgAtom* atom, ValueRep value) {
609 if (!atom->frozen()) { frozen_.push_back(atom->id()); }
610 atom->markFrozen(value);
611 }
612
addExternal(Atom_t atomId,Potassco::Value_t value)613 LogicProgram& LogicProgram::addExternal(Atom_t atomId, Potassco::Value_t value) {
614 check_not_frozen();
615 PrgAtom* a = resize(atomId);
616 if (a->supports() == 0 && (isNew(a->id()) || a->frozen())) {
617 ValueRep fv = static_cast<ValueRep>(value);
618 if (value == Potassco::Value_t::Release) {
619 // add dummy edge - will be removed once we update the set of frozen atoms
620 a->addSupport(PrgEdge::noEdge());
621 fv = value_free;
622 }
623 pushFrozen(a, fv);
624 auxData_->external.push_back(encodeExternal(a->id(), value));
625 }
626 return *this;
627 }
628
freeze(Atom_t atomId,ValueRep value)629 LogicProgram& LogicProgram::freeze(Atom_t atomId, ValueRep value) {
630 POTASSCO_ASSERT(value < value_weak_true);
631 return addExternal(atomId, static_cast<Potassco::Value_t>(value));
632 }
633
unfreeze(Atom_t atomId)634 LogicProgram& LogicProgram::unfreeze(Atom_t atomId) {
635 return addExternal(atomId, Potassco::Value_t::Release);
636 }
setMaxInputAtom(uint32 n)637 void LogicProgram::setMaxInputAtom(uint32 n) {
638 check_not_frozen();
639 resize(n++);
640 POTASSCO_REQUIRE(n >= startAtom(), "invalid input range");
641 input_.hi = n;
642 }
startAuxAtom() const643 Atom_t LogicProgram::startAuxAtom() const {
644 return validAtom(input_.hi) ? input_.hi : (uint32)atoms_.size();
645 }
supportsSmodels() const646 bool LogicProgram::supportsSmodels() const {
647 if (incData_ || theory_) { return false; }
648 if (!auxData_->dom.empty()) { return false; }
649 if (!auxData_->acyc.empty()) { return false; }
650 if (!auxData_->assume.empty()) { return false; }
651 if (!auxData_->project.empty()) { return false; }
652 for (ShowVec::const_iterator it = show_.begin(), end = show_.end(); it != end; ++it) {
653 Potassco::Lit_t lit = Potassco::lit(it->first);
654 if (lit <= 0 || static_cast<uint32>(lit) >= bodyId) { return false; }
655 }
656 return true;
657 }
658
isExternal(Atom_t aId) const659 bool LogicProgram::isExternal(Atom_t aId) const {
660 if (!aId || !validAtom(aId)) { return false; }
661 PrgAtom* a = getRootAtom(aId);
662 return a->frozen() && (a->supports() == 0 || frozen());
663 }
isFact(Atom_t aId) const664 bool LogicProgram::isFact(Atom_t aId) const {
665 return validAtom(aId) && (atomState_.isFact(aId) || atomState_.isFact(getRootId(aId)));
666 }
isDefined(Atom_t aId) const667 bool LogicProgram::isDefined(Atom_t aId) const {
668 if (!validAtom(aId) || getAtom(aId)->removed()) {
669 return false;
670 }
671 PrgAtom* a = getAtom(aId);
672 return isFact(aId) || (a->relevant() && a->supports() && !isExternal(aId));
673 }
inProgram(Atom_t id) const674 bool LogicProgram::inProgram(Atom_t id) const {
675 if (PrgAtom* a = (validAtom(id) ? getAtom(id) : 0)) {
676 return a->relevant() && (a->supports() || a->frozen() || !isNew(id));
677 }
678 return false;
679 }
addAssumption(const Potassco::LitSpan & lits)680 LogicProgram& LogicProgram::addAssumption(const Potassco::LitSpan& lits) {
681 auxData_->assume.insert(auxData_->assume.end(), Potassco::begin(lits), Potassco::end(lits));
682 return *this;
683 }
684
addAcycEdge(uint32 n1,uint32 n2,Id_t condId)685 LogicProgram& LogicProgram::addAcycEdge(uint32 n1, uint32 n2, Id_t condId) {
686 if (condId != falseId) {
687 AcycArc arc = { condId, {n1, n2} };
688 auxData_->acyc.push_back(arc);
689 }
690 upStat(RK(Acyc), 1);
691 return *this;
692 }
693
addDomHeuristic(Atom_t atom,DomModType t,int bias,unsigned prio)694 LogicProgram& LogicProgram::addDomHeuristic(Atom_t atom, DomModType t, int bias, unsigned prio) {
695 return addDomHeuristic(atom, t, bias, prio, Potassco::toSpan<Potassco::Lit_t>());
696 }
addDomHeuristic(Atom_t atom,DomModType type,int bias,unsigned prio,Id_t cond)697 LogicProgram& LogicProgram::addDomHeuristic(Atom_t atom, DomModType type, int bias, unsigned prio, Id_t cond) {
698 static_assert(sizeof(DomRule) == sizeof(uint32[3]), "Invalid DomRule size");
699 if (cond != falseId) {
700 auxData_->dom.push_back(DomRule());
701 DomRule& x = auxData_->dom.back();
702 x.atom = atom;
703 x.type = type;
704 x.cond = cond;
705 x.bias = (int16)Range<int>(INT16_MIN, INT16_MAX).clamp(bias);
706 x.prio = (uint16)Range<unsigned>(unsigned(0), unsigned(~uint16(0)) ).clamp(prio);
707 }
708 upStat(RK(Heuristic), 1);
709 return *this;
710 }
addRule(const Rule & rule)711 LogicProgram& LogicProgram::addRule(const Rule& rule) {
712 check_not_frozen();
713 SRule meta;
714 if (simplifyRule(rule, rule_, meta)) {
715 Rule sRule = rule_.rule();
716 upStat(sRule.ht);
717 if (handleNatively(sRule)) { // and can be handled natively
718 addRule(sRule, meta);
719 }
720 else {
721 upStat(sRule.bt);
722 if (Potassco::size(sRule.head) <= 1 && transformNoAux(sRule)) {
723 // rule transformation does not require aux atoms - do it now
724 int oId = statsId_;
725 statsId_ = 1;
726 RuleTransform tm(*this);
727 upStat(sRule.bt, -1);
728 upStat(rule.ht, -1);
729 tm.transform(sRule, RuleTransform::strategy_no_aux);
730 statsId_ = oId;
731 }
732 else {
733 // make sure we have all head atoms
734 for (Potassco::AtomSpan::iterator it = Potassco::begin(sRule.head), end = Potassco::end(sRule.head); it != end; ++it) {
735 resize(*it);
736 }
737 extended_.push_back(new RuleBuilder(rule_));
738 }
739 }
740 }
741 else if (statsId_ == 0) {
742 for (Potassco::AtomSpan::iterator it = Potassco::begin(rule.head), end = Potassco::end(rule.head); it != end; ++it) {
743 if (!validAtom(*it) || (isNew(*it) && getAtom(*it)->supports() == 0)) {
744 auxData_->skippedHeads.insert(*it);
745 }
746 }
747 }
748 rule_.clear();
749 return *this;
750 }
751
addRule(Head_t ht,const Potassco::AtomSpan & head,const Potassco::LitSpan & body)752 LogicProgram& LogicProgram::addRule(Head_t ht, const Potassco::AtomSpan& head, const Potassco::LitSpan& body) {
753 return addRule(Rule::normal(ht, head, body));
754 }
addRule(Head_t ht,const Potassco::AtomSpan & head,Potassco::Weight_t bound,const Potassco::WeightLitSpan & lits)755 LogicProgram& LogicProgram::addRule(Head_t ht, const Potassco::AtomSpan& head, Potassco::Weight_t bound, const Potassco::WeightLitSpan& lits) {
756 return addRule(Rule::sum(ht, head, bound, lits));
757 }
addRule(Potassco::RuleBuilder & rb)758 LogicProgram& LogicProgram::addRule(Potassco::RuleBuilder& rb) {
759 LogicProgramAdapter prg(*this);
760 rb.end(&prg);
761 return *this;
762 }
addMinimize(weight_t prio,const Potassco::WeightLitSpan & lits)763 LogicProgram& LogicProgram::addMinimize(weight_t prio, const Potassco::WeightLitSpan& lits) {
764 SingleOwnerPtr<Min> n(new Min());
765 n->prio = prio;
766 MinList::iterator it = std::lower_bound(minimize_.begin(), minimize_.end(), n.get(), CmpMin());
767 if (it == minimize_.end() || (*it)->prio != prio) {
768 n->lits.assign(Potassco::begin(lits), Potassco::end(lits));
769 minimize_.insert(it, n.get());
770 n.release();
771 upStat(RuleStats::Minimize);
772 }
773 else {
774 (*it)->lits.insert((*it)->lits.end(), Potassco::begin(lits), Potassco::end(lits));
775 }
776 // Touch all atoms in minimize -> these are input atoms even if they won't occur in a head.
777 for (Potassco::WeightLitSpan::iterator wIt = Potassco::begin(lits), end = Potassco::end(lits); wIt != end; ++wIt) {
778 resize(Potassco::atom(*wIt));
779 }
780 return *this;
781 }
782 #undef check_not_frozen
783 /////////////////////////////////////////////////////////////////////////////////////////
784 // Query functions
785 /////////////////////////////////////////////////////////////////////////////////////////
isFact(PrgAtom * a) const786 bool LogicProgram::isFact(PrgAtom* a) const {
787 uint32 eqId = getRootId(a->id());
788 if (atomState_.isFact(eqId)) {
789 return true;
790 }
791 if (a->value() == value_true) {
792 for (PrgAtom::sup_iterator it = a->supps_begin(), end = a->supps_end(); it != end; ++it) {
793 if (it->isBody() && it->isNormal() && getBody(it->node())->bound() == 0) {
794 return true;
795 }
796 }
797 }
798 return false;
799 }
getLiteral(Id_t id,MapLit_t m) const800 Literal LogicProgram::getLiteral(Id_t id, MapLit_t m) const {
801 Literal out = lit_false();
802 Potassco::Id_t nId = nodeId(id);
803 if (isAtom(id) && validAtom(nId)) {
804 out = getRootAtom(nId)->literal();
805 if (m == MapLit_t::Refined) {
806 IndexMap::const_iterator dom;
807 if ((dom = domEqIndex_.find(nId)) != domEqIndex_.end()) {
808 out = posLit(dom->second);
809 }
810 else if (isSentinel(out) && incData_ && !incData_->steps.empty()) {
811 Var v = isNew(id)
812 ? incData_->steps.back().second
813 : std::lower_bound(incData_->steps.begin(), incData_->steps.end(), Incremental::StepTrue(nId, 0))->second;
814 out = Literal(v, out.sign());
815 }
816 }
817 }
818 else if (isBody(id)) {
819 POTASSCO_ASSERT(validBody(nId), "Invalid condition");
820 out = getBody(getEqBody(nId))->literal();
821 }
822 return out ^ signId(id);
823 }
doGetAssumptions(LitVec & out) const824 void LogicProgram::doGetAssumptions(LitVec& out) const {
825 for (VarVec::const_iterator it = frozen_.begin(), end = frozen_.end(); it != end; ++it) {
826 Literal lit = getRootAtom(*it)->assumption();
827 if (lit != lit_true()) { out.push_back( lit ); }
828 }
829 for (Potassco::LitVec::const_iterator it = auxData_->assume.begin(), end = auxData_->assume.end(); it != end; ++it) {
830 out.push_back(getLiteral(Potassco::id(*it)));
831 }
832 }
833 /////////////////////////////////////////////////////////////////////////////////////////
834 // Program definition - private
835 /////////////////////////////////////////////////////////////////////////////////////////
addRule(const Rule & r,const SRule & meta)836 void LogicProgram::addRule(const Rule& r, const SRule& meta) {
837 if (Potassco::size(r.head) <= 1 && r.ht == Head_t::Disjunctive) {
838 if (Potassco::empty(r.head)) { addIntegrity(r, meta); return; }
839 else if (r.normal() && r.cond.size == 0) { addFact(r.head); return; }
840 }
841 PrgBody* b = getBodyFor(r, meta);
842 // only a non-false body can define atoms
843 if (b->value() != value_false) {
844 bool const disjunctive = Potassco::size(r.head) > 1 && r.ht == Head_t::Disjunctive;
845 const EdgeType t = r.ht == Head_t::Disjunctive ? PrgEdge::Normal : PrgEdge::Choice;
846 uint32 headHash = 0;
847 bool ignoreScc = opts_.noSCC || b->size() == 0;
848 for (Potassco::AtomSpan::iterator it = Potassco::begin(r.head), end = Potassco::end(r.head); it != end; ++it) {
849 PrgAtom* a = resize(*it);
850 check_modular(isNew(*it) || a->frozen() || a->value() == value_false, *it);
851 if (!disjunctive) {
852 // Note: b->heads may now contain duplicates. They are removed in PrgBody::simplifyHeads.
853 b->addHead(a, t);
854 if (ignoreScc) { a->setIgnoreScc(ignoreScc); }
855 }
856 else {
857 headHash += hashLit(posLit(*it));
858 atomState_.addToHead(*it);
859 }
860 }
861 if (disjunctive) {
862 PrgDisj* d = getDisjFor(r.head, headHash);
863 b->addHead(d, t);
864 }
865 }
866 }
addFact(const Potassco::AtomSpan & head)867 void LogicProgram::addFact(const Potassco::AtomSpan& head) {
868 PrgBody* tb = 0;
869 for (Potassco::AtomSpan::iterator it = Potassco::begin(head), end = Potassco::end(head); it != end; ++it) {
870 PrgAtom* a = resize(*it);
871 check_modular(isNew(*it) || a->frozen() || a->value() == value_false, *it);
872 if (*it != a->id() || atomState_.isFact(*it)) { continue; }
873 a->setIgnoreScc(true);
874 atomState_.set(*it, AtomState::fact_flag);
875 if (!a->hasDep(PrgAtom::dep_all) && !a->frozen()) {
876 if (!a->assignValue(value_true) || !a->propagateValue(*this, false)) {
877 setConflict();
878 }
879 for (PrgAtom::sup_iterator bIt = a->supps_begin(), bEnd = a->supps_end(); bIt != bEnd; ++bIt) {
880 if (bIt->isBody()) { getBody(bIt->node())->markHeadsDirty(); }
881 else if (bIt->isDisj()) { getDisj(bIt->node())->markDirty(); }
882 }
883 atoms_[*it] = &trueAtom_g;
884 delete a;
885 }
886 else {
887 if (!tb) tb = getTrueBody();
888 tb->addHead(a, PrgEdge::Normal);
889 assignValue(a, value_true, PrgEdge::newEdge(*tb, PrgEdge::Normal));
890 }
891 }
892 }
addIntegrity(const Rule & r,const SRule & meta)893 void LogicProgram::addIntegrity(const Rule& r, const SRule& meta) {
894 if (r.sum() || r.cond.size != 1 || meta.bid != varMax) {
895 PrgBody* B = getBodyFor(r, meta);
896 if (!B->assignValue(value_false) || !B->propagateValue(*this, true)) {
897 setConflict();
898 }
899 }
900 else {
901 PrgAtom* a = resize(Potassco::atom(r.cond[0]));
902 ValueRep v = r.cond[0] > 0 ? value_false : value_weak_true;
903 assignValue(a, v, PrgEdge::noEdge());
904 }
905 }
assignValue(PrgAtom * a,ValueRep v,PrgEdge reason)906 bool LogicProgram::assignValue(PrgAtom* a, ValueRep v, PrgEdge reason) {
907 if (a->eq()) { a = getRootAtom(a->id()); }
908 ValueRep old = a->value();
909 if (old == value_weak_true && v != value_weak_true) old = value_free;
910 if (!a->assignValue(v)) { setConflict(); return false; }
911 if (old == value_free) { propQ_.push_back(a->id()); }
912 if (v == value_false) {
913 atomState_.set(a->id(), AtomState::false_flag);
914 }
915 else if (v == value_true && reason.isBody() && reason.isNormal() && getBody(reason.node())->bound() == 0) {
916 atomState_.set(a->id(), AtomState::fact_flag);
917 }
918 return true;
919 }
assignValue(PrgHead * h,ValueRep v,PrgEdge reason)920 bool LogicProgram::assignValue(PrgHead* h, ValueRep v, PrgEdge reason) {
921 return !h->isAtom() || assignValue(static_cast<PrgAtom*>(h), v, reason);
922 }
923
handleNatively(const Rule & r) const924 bool LogicProgram::handleNatively(const Rule& r) const {
925 ExtendedRuleMode m = opts_.erMode;
926 if (m == mode_native || (r.normal() && r.ht == Head_t::Disjunctive)) {
927 return true;
928 }
929 else if (m == mode_transform_integ || m == mode_transform_scc || m == mode_transform_nhcf) {
930 return true;
931 }
932 else if (m == mode_transform) {
933 return false;
934 }
935 else if (m == mode_transform_dynamic) {
936 return r.normal() || transformNoAux(r) == false;
937 }
938 else if (m == mode_transform_choice) {
939 return r.ht != Head_t::Choice;
940 }
941 else if (m == mode_transform_card) {
942 return r.bt != Body_t::Count;
943 }
944 else if (m == mode_transform_weight) {
945 return r.normal();
946 }
947 assert(false && "unhandled extended rule mode");
948 return true;
949 }
950
transformNoAux(const Rule & r) const951 bool LogicProgram::transformNoAux(const Rule& r) const {
952 return r.ht == Head_t::Disjunctive && r.sum() && (r.agg.bound == 1 || (Potassco::size(r.agg.lits) <= 6 && choose(toU32(Potassco::size(r.agg.lits)), r.agg.bound) <= 15));
953 }
954
transformExtended()955 void LogicProgram::transformExtended() {
956 uint32 a = numAtoms();
957 RuleTransform tm(*this);
958 for (RuleList::size_type i = 0; i != extended_.size(); ++i) {
959 Rule r = extended_[i]->rule();
960 upStat(r.ht, -1);
961 upStat(r.bt, -1);
962 if (r.normal() || (r.ht == Head_t::Disjunctive && Potassco::size(r.head) < 2)) {
963 tm.transform(r);
964 }
965 else {
966 using Potassco::Lit_t;
967 Atom_t aux = newAtom();
968 Lit_t auxB = Potassco::lit(aux);
969 Rule rAux1 = r; // aux :- body
970 rAux1.ht = Head_t::Disjunctive;
971 rAux1.head = Potassco::toSpan(&aux, 1);
972 Rule rAux2 = Rule::normal(r.ht, r.head, Potassco::toSpan(&auxB, 1)); // head :- auxB
973 if (handleNatively(rAux1)) { addRule(rAux1); }
974 else {
975 RuleTransform::Strategy st = transformNoAux(rAux1) ? RuleTransform::strategy_no_aux : RuleTransform::strategy_default;
976 tm.transform(rAux1, st);
977 }
978 if (handleNatively(rAux2)) { addRule(rAux2); }
979 else { tm.transform(rAux2); }
980 }
981 delete extended_[i];
982 }
983 extended_.clear();
984 incTrAux(numAtoms() - a);
985 }
986
transformIntegrity(uint32 nAtoms,uint32 maxAux)987 void LogicProgram::transformIntegrity(uint32 nAtoms, uint32 maxAux) {
988 if (stats.bodies[1][Body_t::Count] == 0) { return; }
989 // find all constraint rules that are integrity constraints
990 BodyList integrity;
991 for (uint32 i = 0, end = static_cast<uint32>(bodies_.size()); i != end; ++i) {
992 PrgBody* b = bodies_[i];
993 if (b->relevant() && b->type() == Body_t::Count && b->value() == value_false) {
994 integrity.push_back(b);
995 }
996 }
997 if (!integrity.empty() && (integrity.size() == 1 || (nAtoms/double(bodies_.size()) > 0.5 && integrity.size() / double(bodies_.size()) < 0.01))) {
998 uint32 aux = static_cast<uint32>(atoms_.size());
999 RuleTransform tr(*this);
1000 RuleBuilder temp;
1001 // transform integrity constraints
1002 for (BodyList::size_type i = 0; i != integrity.size(); ++i) {
1003 PrgBody* b = integrity[i];
1004 uint32 est = b->bound()*( b->sumW()-b->bound() );
1005 if (est > maxAux) {
1006 // reached limit on aux atoms - stop transformation
1007 break;
1008 }
1009 if (b->toData(*this, temp) && temp.bodyType() != Body_t::Normal) {
1010 maxAux -= est;
1011 // transform rule
1012 setFrozen(false);
1013 upStat(Head_t::Disjunctive, -1);
1014 upStat(Body_t::Count, -1);
1015 tr.transform(Rule::sum(Head_t::Disjunctive, Potassco::toSpan<Potassco::Atom_t>(), temp.sum()));
1016 setFrozen(true);
1017 // propagate integrity condition to new rules
1018 propagate(true);
1019 b->markRemoved();
1020 }
1021 temp.clear();
1022 }
1023 // create vars for new atoms/bodies
1024 for (uint32 i = aux; i != atoms_.size(); ++i) {
1025 PrgAtom* a = atoms_[i];
1026 for (PrgAtom::sup_iterator it = a->supps_begin(); it != a->supps_end(); ++it) {
1027 PrgBody* nb = bodies_[it->node()];
1028 assert(nb->value() != value_false);
1029 nb->assignVar(*this);
1030 }
1031 a->assignVar(*this, a->supports() ? *a->supps_begin() : PrgEdge::noEdge());
1032 }
1033 incTrAux(static_cast<uint32>(atoms_.size()) - aux);
1034 }
1035 }
1036
prepareExternals()1037 void LogicProgram::prepareExternals() {
1038 if (auxData_->external.empty()) { return; }
1039 VarVec& external = auxData_->external;
1040 VarVec::iterator j = external.begin();
1041 for (VarVec::const_iterator it = j, end = external.end(); it != end; ++it) {
1042 Atom_t id = getRootId(decodeExternal(*it).first);
1043 const PrgAtom* atom = getAtom(id);
1044 if (!atomState_.inHead(id) && (atom->supports() == 0 || *atom->supps_begin() == PrgEdge::noEdge())) {
1045 Potassco::Value_t value = atom->supports() == 0 ? static_cast<Potassco::Value_t>(atom->freezeValue()) : Potassco::Value_t::Release;
1046 atomState_.addToHead(id);
1047 *j++ = encodeExternal(id, value);
1048 }
1049 }
1050 external.erase(j, external.end());
1051 for (VarVec::const_iterator it = external.begin(), end = external.end(); it != end; ++it) {
1052 atomState_.clearRule(decodeExternal(*it).first);
1053 }
1054 }
updateFrozenAtoms()1055 void LogicProgram::updateFrozenAtoms() {
1056 if (frozen_.empty()) { return; }
1057 PrgBody* support = 0;
1058 VarVec::iterator j = frozen_.begin();
1059 for (VarVec::const_iterator it = j, end = frozen_.end(); it != end; ++it) {
1060 Id_t id = getRootId(*it);
1061 PrgAtom* a = getAtom(id);
1062 assert(a->frozen());
1063 a->resetId(id, false);
1064 if (a->supports() == 0) {
1065 assert(a->relevant());
1066 POTASSCO_REQUIRE(id < startAuxAtom(), "frozen atom shall be an input atom");
1067 if (!support) { support = getTrueBody(); }
1068 a->setIgnoreScc(true);
1069 support->addHead(a, PrgEdge::GammaChoice);
1070 *j++ = id; // still frozen
1071 }
1072 else {
1073 a->clearFrozen();
1074 if (*a->supps_begin() == PrgEdge::noEdge()) {
1075 // remove dummy edge added in unfreeze()
1076 a->removeSupport(PrgEdge::noEdge());
1077 }
1078 if (!isNew(id) && incData_) {
1079 // add to unfreeze so that we can later perform completion
1080 incData_->unfreeze.push_back(id);
1081 }
1082 }
1083 }
1084 frozen_.erase(j, frozen_.end());
1085 }
1086
prepareProgram(bool checkSccs)1087 void LogicProgram::prepareProgram(bool checkSccs) {
1088 assert(!frozen());
1089 prepareExternals();
1090 // Given that freezeTheory() might introduce otherwise
1091 // unused atoms, it must be called before we fix the
1092 // number of input atoms.
1093 freezeTheory();
1094 uint32 nAtoms = (input_.hi = std::min(input_.hi, endAtom()));
1095 stats.auxAtoms += endAtom() - nAtoms;
1096 for (uint32 i = 0; i != RuleStats::numKeys(); ++i) {
1097 stats.rules[1][i] += stats.rules[0][i];
1098 }
1099 for (uint32 i = 0; i != BodyStats::numKeys(); ++i) {
1100 stats.bodies[1][i] += stats.bodies[0][i];
1101 }
1102 statsId_ = 1;
1103 transformExtended();
1104 updateFrozenAtoms();
1105 PrgAtom* suppAtom = 0;
1106 if (opts_.suppMod) {
1107 VarVec h;
1108 suppAtom = getAtom(newAtom());
1109 h.assign(1, suppAtom->id());
1110 addRule(Head_t::Choice, Potassco::toSpan(h), Potassco::toSpan<Potassco::Lit_t>());
1111 Potassco::Lit_t body = Potassco::lit(suppAtom->id());
1112 h.clear();
1113 for (Atom_t v = startAtom(), end = suppAtom->id(); v != end; ++v) {
1114 if (atoms_[v]->supports() != 0) { h.push_back(v); }
1115 }
1116 addRule(Head_t::Choice, Potassco::toSpan(h), Potassco::toSpan(&body, 1));
1117 }
1118 setFrozen(true);
1119 Preprocessor p;
1120 if (hasConflict() || !propagate(true) || !p.preprocess(*this, opts_.iters != 0 ? Preprocessor::full_eq : Preprocessor::no_eq, opts_.iters, opts_.dfOrder != 0)) {
1121 setConflict();
1122 return;
1123 }
1124 if (suppAtom && (!assignValue(suppAtom, value_false, PrgEdge::noEdge()) || !propagate(true))) {
1125 setConflict();
1126 return;
1127 }
1128 if (opts_.erMode == mode_transform_integ || opts_.erMode == mode_transform_dynamic) {
1129 nAtoms -= startAtom();
1130 transformIntegrity(nAtoms, std::min(uint32(15000), nAtoms*2));
1131 }
1132 addMinimize();
1133 uint32 sccs = 0;
1134 if (checkSccs) {
1135 uint32 startScc = incData_ ? incData_->startScc : 0;
1136 SccChecker c(*this, auxData_->scc, startScc);
1137 sccs = c.sccs();
1138 stats.sccs = (sccs-startScc);
1139 if (incData_) { incData_->startScc = c.sccs(); }
1140 if (!disjunctions_.empty() || (opts_.erMode == mode_transform_scc && sccs)) {
1141 // reset node ids changed by scc checking
1142 for (uint32 i = 0; i != bodies_.size(); ++i) {
1143 if (getBody(i)->relevant()) { getBody(i)->resetId(i, true); }
1144 }
1145 for (uint32 i = 0; i != atoms_.size(); ++i) {
1146 if (getAtom(i)->relevant()) { getAtom(i)->resetId(i, true); }
1147 }
1148 }
1149 }
1150 else { stats.sccs = PrgNode::noScc; }
1151 finalizeDisjunctions(p, sccs);
1152 prepareComponents();
1153 prepareOutputTable();
1154 freezeAssumptions();
1155 if (incData_ && options().distTrue) {
1156 for (Var a = startAtom(), end = startAuxAtom(); a != end; ++a) {
1157 if (isSentinel(getRootAtom(a)->literal())) {
1158 Incremental::StepTrue t(end - 1, 0);
1159 if (!incData_->steps.empty()) { t.second = ctx()->addVar(Var_t::Atom, 0); }
1160 incData_->steps.push_back(t);
1161 break;
1162 }
1163 }
1164 }
1165 if (theory_) {
1166 TFilter f = { this };
1167 theory_->filter(f);
1168 }
1169 stats.atoms = static_cast<uint32>(atoms_.size()) - startAtom();
1170 bodyIndex_.clear();
1171 disjIndex_.clear();
1172 }
freezeTheory()1173 void LogicProgram::freezeTheory() {
1174 if (theory_) {
1175 const IdSet& skippedHeads = auxData_->skippedHeads;
1176 for (TheoryData::atom_iterator it = theory_->currBegin(), end = theory_->end(); it != end; ++it) {
1177 const Potassco::TheoryAtom& a = **it;
1178 if (isFact(a.atom()) || !isNew(a.atom())) { continue; }
1179 PrgAtom* atom = resize(a.atom());
1180 if (!atom->frozen() && atom->supports() == 0 && atom->relevant() && skippedHeads.count(a.atom()) == 0) {
1181 pushFrozen(atom, value_free);
1182 }
1183 }
1184 }
1185 }
operator ()(const Potassco::TheoryAtom & a) const1186 bool LogicProgram::TFilter::operator()(const Potassco::TheoryAtom& a) const {
1187 Atom_t id = a.atom();
1188 if (self->getLiteral(id) != lit_false() && self->getRootAtom(id)->value() != value_false) {
1189 self->ctx()->setFrozen(self->getLiteral(id).var(), true);
1190 return false;
1191 }
1192 PrgAtom* at = self->getRootAtom(id);
1193 return !at->frozen();
1194 }
1195 struct LogicProgram::DlpTr : public RuleTransform::ProgramAdapter {
DlpTrClasp::Asp::LogicProgram::DlpTr1196 DlpTr(LogicProgram* x, EdgeType et) : self(x), type(et), scc(PrgNode::noScc) {}
newAtomClasp::Asp::LogicProgram::DlpTr1197 Atom_t newAtom() {
1198 Atom_t x = self->newAtom();
1199 PrgAtom* a = self->getAtom(x);
1200 a->setScc(scc);
1201 a->setSeen(true);
1202 atoms.push_back(x);
1203 if (scc != PrgNode::noScc) { self->auxData_->scc.push_back(a); }
1204 return x;
1205 }
addRuleClasp::Asp::LogicProgram::DlpTr1206 virtual void addRule(const Rule& r) {
1207 SRule meta;
1208 if (!self->simplifyRule(r, rule, meta)) { return; }
1209 bool gamma = type == PrgEdge::Gamma;
1210 Rule rs = rule.rule();
1211 PrgAtom* a = self->getAtom(rs.head[0]);
1212 PrgBody* B = self->assignBodyFor(rs, meta, type, gamma);
1213 if (B->value() != value_false && !B->hasHead(a, PrgEdge::Normal)) {
1214 B->addHead(a, type);
1215 self->stats.gammas += uint32(gamma);
1216 }
1217 }
assignAuxAtomsClasp::Asp::LogicProgram::DlpTr1218 void assignAuxAtoms() {
1219 self->incTrAux(sizeVec(atoms));
1220 while (!atoms.empty()) {
1221 PrgAtom* ax = self->getAtom(atoms.back());
1222 atoms.pop_back();
1223 if (ax->supports()) {
1224 ax->setInUpper(true);
1225 ax->assignVar(*self, *ax->supps_begin());
1226 }
1227 else { self->assignValue(ax, value_false, PrgEdge::noEdge()); }
1228 }
1229 }
1230 LogicProgram* self;
1231 EdgeType type;
1232 uint32 scc;
1233 VarVec atoms;
1234 RuleBuilder rule;
1235 };
1236
1237 // replace disjunctions with gamma (shifted) and delta (component-shifted) rules
finalizeDisjunctions(Preprocessor & p,uint32 numSccs)1238 void LogicProgram::finalizeDisjunctions(Preprocessor& p, uint32 numSccs) {
1239 if (disjunctions_.empty()) { return; }
1240 VarVec head; BodyList supports;
1241 disjIndex_.clear();
1242 SccMap sccMap;
1243 sccMap.resize(numSccs, 0);
1244 enum SccFlag { seen_scc = 1u, is_scc_non_hcf = 128u };
1245 // replace disjunctions with shifted rules and non-hcf-disjunctions
1246 DisjList disj; disj.swap(disjunctions_);
1247 setFrozen(false);
1248 uint32 shifted = 0;
1249 stats.nonHcfs = uint32(nonHcfs_.size());
1250 Literal bot = lit_false();
1251 DlpTr tr(this, PrgEdge::Gamma);
1252 RuleTransform shifter(tr);
1253 Potassco::LitVec rb;
1254 VarVec rh;
1255 for (uint32 id = 0, maxId = sizeVec(disj); id != maxId; ++id) {
1256 PrgDisj* d = disj[id];
1257 Literal dx = d->inUpper() ? d->literal() : bot;
1258 d->resetId(id, true); // id changed during scc checking
1259 PrgEdge e = PrgEdge::newEdge(*d, PrgEdge::Choice);
1260 // remove from program and
1261 // replace with shifted rules or component-shifted disjunction
1262 head.clear(); supports.clear();
1263 for (PrgDisj::atom_iterator it = d->begin(), end = d->end(); it != end; ++it) {
1264 uint32 aId = *it;
1265 PrgAtom* at = getAtom(aId);
1266 at->removeSupport(e);
1267 if (dx == bot) { continue; }
1268 if (at->eq()) {
1269 at = getAtom(aId = getRootId(aId));
1270 }
1271 if (isFact(at)){
1272 dx = bot;
1273 continue;
1274 }
1275 if (at->inUpper()) {
1276 head.push_back(aId);
1277 if (at->scc() != PrgNode::noScc){ sccMap[at->scc()] = seen_scc; }
1278 }
1279 }
1280 EdgeVec temp;
1281 d->clearSupports(temp);
1282 for (EdgeVec::iterator it = temp.begin(), end = temp.end(); it != end; ++it) {
1283 PrgBody* b = getBody(it->node());
1284 if (b->relevant() && b->value() != value_false) { supports.push_back(b); }
1285 b->removeHead(d, PrgEdge::Normal);
1286 }
1287 d->destroy();
1288 // create shortcut for supports to avoid duplications during shifting
1289 Literal supportLit = dx != bot ? getEqAtomLit(dx, supports, p, sccMap) : dx;
1290 // create shifted rules and split disjunctions into non-hcf components
1291 for (VarVec::iterator hIt = head.begin(), hEnd = head.end(); hIt != hEnd; ++hIt) {
1292 uint32 scc = getAtom(*hIt)->scc();
1293 if (scc == PrgNode::noScc || (sccMap[scc] & seen_scc) != 0) {
1294 if (scc != PrgNode::noScc) { sccMap[scc] &= ~seen_scc; }
1295 else { scc = UINT32_MAX; }
1296 rh.assign(1, *hIt);
1297 rb.clear();
1298 if (supportLit.var() != 0) { rb.push_back(toInt(supportLit)); }
1299 else if (supportLit.sign()){ continue; }
1300 for (VarVec::iterator oIt = head.begin(); oIt != hEnd; ++oIt) {
1301 if (oIt != hIt) {
1302 if (getAtom(*oIt)->scc() == scc) { rh.push_back(*oIt); }
1303 else { rb.push_back(Potassco::neg(*oIt)); }
1304 }
1305 }
1306 SRule meta;
1307 if (!simplifyRule(Rule::normal(Head_t::Disjunctive, Potassco::toSpan(rh), Potassco::toSpan(rb)), rule_, meta)) {
1308 continue;
1309 }
1310 Rule sr = rule_.rule();
1311 PrgBody* B = assignBodyFor(sr, meta, PrgEdge::Normal, true);
1312 if (B->value() != value_false && Potassco::size(sr.head) == 1) {
1313 ++shifted;
1314 B->addHead(getAtom(sr.head[0]), PrgEdge::Normal);
1315 }
1316 else if (B->value() != value_false && Potassco::size(sr.head) > 1) {
1317 PrgDisj* x = getDisjFor(sr.head, 0);
1318 B->addHead(x, PrgEdge::Normal);
1319 x->assignVar(*this, *x->supps_begin());
1320 x->setInUpper(true);
1321 x->setSeen(true);
1322 if ((sccMap[scc] & is_scc_non_hcf) == 0) {
1323 sccMap[scc] |= is_scc_non_hcf;
1324 nonHcfs_.add(scc);
1325 }
1326 if (!options().noGamma) {
1327 tr.scc = scc;
1328 shifter.transform(sr, Potassco::size(sr.cond) < 4 ? RuleTransform::strategy_no_aux : RuleTransform::strategy_default);
1329 }
1330 else {
1331 // only add support edge
1332 for (PrgDisj::atom_iterator a = x->begin(), end = x->end(); a != end; ++a) {
1333 B->addHead(getAtom(*a), PrgEdge::GammaChoice);
1334 }
1335 }
1336 }
1337 }
1338 }
1339 }
1340 tr.assignAuxAtoms();
1341 if (!disjunctions_.empty() && nonHcfs_.config == 0) {
1342 nonHcfs_.config = ctx()->configuration()->config("tester");
1343 }
1344 upStat(RK(Normal), shifted);
1345 stats.nonHcfs = uint32(nonHcfs_.size()) - stats.nonHcfs;
1346 rh.clear();
1347 setFrozen(true);
1348 }
1349 // optionally transform extended rules in sccs
prepareComponents()1350 void LogicProgram::prepareComponents() {
1351 int trRec = opts_.erMode == mode_transform_scc;
1352 // HACK: force transformation of extended rules in non-hcf components
1353 // REMOVE this once minimality check supports aggregates
1354 if (!disjunctions_.empty() && trRec != 1) {
1355 trRec = 2;
1356 }
1357 if (trRec != 0) {
1358 DlpTr tr(this, PrgEdge::Normal);
1359 RuleTransform trans(tr);
1360 RuleBuilder temp;
1361 setFrozen(false);
1362 EdgeVec heads;
1363 // find recursive aggregates
1364 for (uint32 bIdx = 0, bEnd = numBodies(); bIdx != bEnd; ++bIdx) {
1365 PrgBody* B = bodies_[bIdx];
1366 if (B->type() == Body_t::Normal || !B->hasVar() || B->value() == value_false) { continue; } // not aggregate or not relevant
1367 tr.scc = B->scc(*this);
1368 if (tr.scc == PrgNode::noScc || (trRec == 2 && !nonHcfs_.find(tr.scc))) { continue; } // not recursive
1369 // transform all rules a :- B, where scc(a) == scc(B):
1370 heads.clear();
1371 for (PrgBody::head_iterator hIt = B->heads_begin(), hEnd = B->heads_end(); hIt != hEnd; ++hIt) {
1372 assert(hIt->isAtom());
1373 if (getAtom(hIt->node())->scc() == tr.scc) { heads.push_back(*hIt); }
1374 }
1375 if (heads.empty()) { continue; }
1376 using Potassco::Lit_t;
1377 Head_t ht = !isChoice(heads[0].type()) ? Head_t::Disjunctive : Head_t::Choice;
1378 Atom_t h = heads[0].node();
1379 Lit_t aux = 0;
1380 if (heads.size() > 1) { // more than one head, make body eq to some new aux atom
1381 ht = Head_t::Disjunctive;
1382 h = tr.newAtom();
1383 aux = Potassco::lit(h);
1384 }
1385 temp.clear();
1386 if (!B->toData(*this, temp) || temp.bodyType() == Body_t::Normal) {
1387 B->simplify(*this, true, 0);
1388 continue;
1389 }
1390 trans.transform(Rule::sum(ht, Potassco::toSpan(&h, 1), temp.sum()));
1391 for (EdgeVec::const_iterator hIt = heads.begin(); hIt != heads.end(); ++hIt) {
1392 B->removeHead(getAtom(hIt->node()), hIt->type());
1393 if (h != hIt->node()) {
1394 ht = !isChoice(hIt->type()) ? Head_t::Disjunctive : Head_t::Choice;
1395 h = hIt->node();
1396 tr.addRule(Rule::normal(ht, Potassco::toSpan(&h, 1), Potassco::toSpan(&aux, 1)));
1397 }
1398 }
1399 }
1400 tr.assignAuxAtoms();
1401 setFrozen(true);
1402 }
1403 }
prepareOutputTable()1404 void LogicProgram::prepareOutputTable() {
1405 OutputTable& out = ctx()->output;
1406 // add new output predicates in program order to output table
1407 std::stable_sort(show_.begin(), show_.end(), compose22(std::less<Id_t>(), select1st<ShowPair>(), select1st<ShowPair>()));
1408 for (ShowVec::iterator it = show_.begin(), end = show_.end(); it != end; ++it) {
1409 Literal lit = getLiteral(it->first);
1410 bool isAtom = it->first < startAuxAtom();
1411 if (!isSentinel(lit)) { out.add(it->second, lit, it->first); if (isAtom) ctx()->setOutput(lit.var(), true); }
1412 else if (lit == lit_true()) { out.add(it->second); }
1413 }
1414 if (!auxData_->project.empty()) {
1415 for (VarVec::const_iterator it = auxData_->project.begin(), end = auxData_->project.end(); it != end; ++it) {
1416 out.addProject(getLiteral(*it));
1417 }
1418 }
1419 }
1420
1421 // Make assumptions/externals exempt from sat-preprocessing
freezeAssumptions()1422 void LogicProgram::freezeAssumptions() {
1423 for (VarVec::const_iterator it = frozen_.begin(), end = frozen_.end(); it != end; ++it) {
1424 ctx()->setFrozen(getRootAtom(*it)->var(), true);
1425 }
1426 for (Potassco::LitVec::const_iterator it = auxData_->assume.begin(), end = auxData_->assume.end(); it != end; ++it) {
1427 ctx()->setFrozen(getLiteral(Potassco::id(*it)).var(), true);
1428 }
1429 }
1430
1431 // add (completion) nogoods
addConstraints()1432 bool LogicProgram::addConstraints() {
1433 ClauseCreator gc(ctx()->master());
1434 if (options().iters == 0) {
1435 gc.addDefaultFlags(ClauseCreator::clause_force_simplify);
1436 }
1437 ctx()->startAddConstraints();
1438 // handle initial conflict, if any
1439 if (!ctx()->ok() || !ctx()->addUnary(getTrueAtom()->trueLit())) {
1440 return false;
1441 }
1442 if (incData_ && !incData_->steps.empty() && !ctx()->addUnary(posLit(incData_->steps.back().second))) {
1443 return false;
1444 }
1445 if (options().noGamma && !disjunctions_.empty()) {
1446 // add "rule" nogoods for disjunctions
1447 for (DisjList::const_iterator it = disjunctions_.begin(); it != disjunctions_.end(); ++it) {
1448 gc.start().add(~(*it)->literal());
1449 for (PrgDisj::atom_iterator a = (*it)->begin(); a != (*it)->end(); ++a) {
1450 gc.add(getAtom(*a)->literal());
1451 }
1452 if (!gc.end()) { return false; }
1453 }
1454 }
1455 // add bodies from this step
1456 for (BodyList::const_iterator it = bodies_.begin(); it != bodies_.end(); ++it) {
1457 if (!toConstraint((*it), *this, gc)) { return false; }
1458 }
1459 // add atoms thawed in this step
1460 for (VarIter it = unfreeze_begin(), end = unfreeze_end(); it != end; ++it) {
1461 if (!toConstraint(getAtom(*it), *this, gc)) { return false; }
1462 }
1463 // add atoms from this step
1464 const bool freezeAll = incData_ != 0;
1465 const uint32 hiAtom = startAuxAtom();
1466 uint32 id = startAtom();
1467 for (AtomList::const_iterator it = atoms_.begin()+startAtom(), end = atoms_.end(); it != end; ++it, ++id) {
1468 if (!toConstraint(*it, *this, gc)) { return false; }
1469 if (id < hiAtom && (*it)->hasVar()){
1470 if (freezeAll) { ctx()->setFrozen((*it)->var(), true); }
1471 ctx()->setInput((*it)->var(), true);
1472 }
1473 }
1474 if (!auxData_->scc.empty()) {
1475 if (ctx()->sccGraph.get() == 0) {
1476 ctx()->sccGraph = new PrgDepGraph(static_cast<PrgDepGraph::NonHcfMapType>(opts_.oldMap == 0));
1477 }
1478 uint32 oldNodes = ctx()->sccGraph->nodes();
1479 ctx()->sccGraph->addSccs(*this, auxData_->scc, nonHcfs_);
1480 stats.ufsNodes = ctx()->sccGraph->nodes()-oldNodes;
1481 }
1482 return true;
1483 }
addDomRules()1484 void LogicProgram::addDomRules() {
1485 if (auxData_->dom.empty()) { return; }
1486 VarVec domVec;
1487 EqVec eqVec;
1488 DomRules& doms = auxData_->dom;
1489 Solver const& s = *ctx()->master();
1490 // mark any previous domain atoms so that we can decide
1491 // whether existing variables can be used for the atoms in doms
1492 if (incData_) {
1493 domVec.swap(incData_->doms);
1494 for (VarVec::const_iterator it = domVec.begin(); it != domVec.end(); ++it) {
1495 if (s.value(*it) == value_free) { ctx()->mark(posLit(*it)); }
1496 }
1497 }
1498 DomRules::iterator j;
1499 IndexMap::const_iterator eq;
1500 DomRule r;
1501 for (DomRules::iterator it = (j = doms.begin()), end = doms.end(); it != end; ++it) {
1502 Literal cond = getLiteral(it->cond);
1503 Literal slit = getLiteral(it->atom);
1504 Var svar = slit.var();
1505 if (s.isFalse(cond) || s.value(svar) != value_free) { continue; }
1506 if (s.isTrue(cond)) { it->cond = 0; cond = lit_true(); }
1507 // check if atom is the root for its var
1508 if (!atomState_.isSet(it->atom, AtomState::dom_flag)) {
1509 if (!ctx()->marked(posLit(svar))) {
1510 // var(it->atom) is not yet used - make it->atom its root
1511 ctx()->mark(posLit(svar));
1512 atomState_.set(it->atom, AtomState::dom_flag);
1513 domVec.push_back(svar);
1514 }
1515 else if ((eq = domEqIndex_.find(it->atom)) != domEqIndex_.end()) {
1516 // var(it->atom) is used but we already created a new var for it->atom
1517 slit = posLit(svar = eq->second);
1518 }
1519 else {
1520 // var(it->atom) is used - introduce new aux var and make it eq to lit(atom)
1521 Eq n = { ctx()->addVar(Var_t::Atom, VarInfo::Nant), slit };
1522 eqVec.push_back(n);
1523 svar = n.var;
1524 slit = posLit(svar);
1525 domEqIndex_.insert(IndexMap::value_type(static_cast<uint32>(it->atom), svar));
1526 }
1527 }
1528 *j++ = (r = *it);
1529 if (slit.sign()) {
1530 if (r.type == DomModType::Sign) { r.bias = r.bias != 0 ? -r.bias : 0; }
1531 else if (r.type == DomModType::True) { r.type = DomModType::False; }
1532 else if (r.type == DomModType::False) { r.type = DomModType::True; }
1533 }
1534 ctx()->heuristic.add(svar, static_cast<DomModType>(r.type), r.bias, r.prio, cond);
1535 }
1536 if (j != doms.end()) {
1537 upStat(RK(Heuristic), -static_cast<int>(doms.end() - j));
1538 doms.erase(j, doms.end());
1539 }
1540 // cleanup var flags
1541 for (VarVec::const_iterator it = domVec.begin(); it != domVec.end(); ++it) {
1542 ctx()->unmark(*it);
1543 }
1544 if (incData_) {
1545 incData_->doms.swap(domVec);
1546 }
1547 if (!eqVec.empty()) {
1548 ctx()->startAddConstraints();
1549 for (EqVec::const_iterator it = eqVec.begin(), end = eqVec.end(); it != end; ++it) {
1550 // it->var == it->lit
1551 ctx()->addBinary(~it->lit, posLit(it->var));
1552 ctx()->addBinary( it->lit, negLit(it->var));
1553 }
1554 }
1555 }
1556
addAcycConstraint()1557 void LogicProgram::addAcycConstraint() {
1558 AcycRules& acyc = auxData_->acyc;
1559 if (acyc.empty()) { return; }
1560 SharedContext& ctx = *this->ctx();
1561 ExtDepGraph* graph = ctx.extGraph.get();
1562 const Solver& s = *ctx.master();
1563 if (graph) { graph->update(); }
1564 else { ctx.extGraph = (graph = new ExtDepGraph()); }
1565 for (AcycRules::const_iterator it = acyc.begin(), end = acyc.end(); it != end; ++it) {
1566 Literal lit = getLiteral(it->cond);
1567 if (!s.isFalse(lit)) {
1568 graph->addEdge(lit, it->node[0], it->node[1]);
1569 }
1570 else {
1571 upStat(RK(Acyc), -1);
1572 }
1573 }
1574 if (graph->finalize(ctx) == 0) { ctx.extGraph = 0; }
1575 }
1576 #undef check_modular
1577 /////////////////////////////////////////////////////////////////////////////////////////
1578 // misc/helper functions
1579 /////////////////////////////////////////////////////////////////////////////////////////
resize(Atom_t atomId)1580 PrgAtom* LogicProgram::resize(Atom_t atomId) {
1581 while (atoms_.size() <= AtomList::size_type(atomId)) {
1582 newAtom();
1583 }
1584 return getRootAtom(atomId);
1585 }
1586
propagate(bool backprop)1587 bool LogicProgram::propagate(bool backprop) {
1588 assert(frozen());
1589 bool oldB = opts_.backprop != 0;
1590 opts_.backprop = backprop;
1591 for (VarVec::size_type i = 0; i != propQ_.size(); ++i) {
1592 PrgAtom* a = getAtom(propQ_[i]);
1593 if (!a->relevant()) { continue; }
1594 if (!a->propagateValue(*this, backprop)) {
1595 setConflict();
1596 return false;
1597 }
1598 if (a->hasVar() && a->id() < startAtom() && !ctx()->addUnary(a->trueLit())) {
1599 setConflict();
1600 return false;
1601 }
1602 }
1603 opts_.backprop = oldB;
1604 propQ_.clear();
1605 return true;
1606 }
litVal(const PrgAtom * a,bool pos) const1607 ValueRep LogicProgram::litVal(const PrgAtom* a, bool pos) const {
1608 if (a->value() != value_free || !a->relevant()) {
1609 bool vSign = a->value() == value_false || !a->relevant();
1610 if (vSign == pos) { return value_false; }
1611 return a->value() != value_weak_true ? value_true : value_free;
1612 }
1613 return value_free;
1614 }
1615
1616 // Simplifies the given normal rule H :- l1, ..., ln
1617 // - removes true and duplicate literals from body: {T,a,b,a} -> {a, b}.
1618 // - checks for contradictions and false literals in body: {a, not a} -> F
1619 // - checks for satisfied head and removes false atoms from head
1620 // POST: if true out contains the simplified normal rule.
simplifyNormal(Head_t ht,const Potassco::AtomSpan & head,const Potassco::LitSpan & body,RuleBuilder & out,SRule & meta)1621 bool LogicProgram::simplifyNormal(Head_t ht, const Potassco::AtomSpan& head, const Potassco::LitSpan& body, RuleBuilder& out, SRule& meta) {
1622 out.clear();
1623 out.startBody();
1624 meta = SRule();
1625 bool ok = true;
1626 for (Potassco::LitSpan::iterator it = Potassco::begin(body), end = Potassco::end(body); it != end; ++it) {
1627 POTASSCO_CHECK(Potassco::atom(*it) < bodyId, EOVERFLOW, "Atom out of bounds");
1628 PrgAtom* a = resize(Potassco::atom(*it));
1629 Literal p = Literal(a->id(), *it < 0);// replace any eq atoms
1630 ValueRep v = litVal(a, !p.sign());
1631 if (v == value_false || atomState_.inBody(~p)) {
1632 ok = false;
1633 break;
1634 }
1635 else if (v != value_true && !atomState_.inBody(p)) {
1636 atomState_.addToBody(p);
1637 out.addGoal(toInt(p));
1638 meta.pos += !p.sign();
1639 meta.hash += hashLit(p);
1640 }
1641 }
1642 uint32_t bs = toU32(size(out.body()));
1643 meta.bid = ok ? findBody(meta.hash, Body_t::Normal, bs) : varMax;
1644 ok = ok && pushHead(ht, head, 0, out);
1645 for (const Potassco::Lit_t* it = out.lits_begin(); bs--;) {
1646 atomState_.clearRule(Potassco::atom(*it++));
1647 }
1648 return ok;
1649 }
1650
1651 struct IsLit {
IsLitClasp::Asp::IsLit1652 IsLit(Potassco::Lit_t x) : lhs(x) {}
1653 template <class P>
operator ()Clasp::Asp::IsLit1654 bool operator()(const P& rhs) const { return lhs == Potassco::lit(rhs); }
1655 Potassco::Lit_t lhs;
1656 };
1657
1658 // Simplifies the given sum rule: H :- lb { l1 = w1 ... ln = wn }.
1659 // - removes assigned literals and updates lb accordingly
1660 // - removes literals li with weight wi = 0
1661 // - reduces weights wi > bound() to bound
1662 // - merges duplicate literals in sum, i.e. lb {a=w1, b=w2, a=w3} -> lb {a=w1+w3, b=w2}
1663 // - checks for contradiction, i.e. sum contains both p and not p and both are needed
1664 // - replaces sum with count if all weights are equal
1665 // - replaces sum with normal body if all literals must be true for the sum to be satisfied
1666 // POST: if true out contains the simplified rule.
simplifySum(Head_t ht,const Potassco::AtomSpan & head,const Potassco::Sum_t & body,RuleBuilder & out,SRule & meta)1667 bool LogicProgram::simplifySum(Head_t ht, const Potassco::AtomSpan& head, const Potassco::Sum_t& body, RuleBuilder& out, SRule& meta) {
1668 meta = SRule();
1669 weight_t bound = body.bound, maxW = 1, minW = CLASP_WEIGHT_T_MAX, sumW = 0, dirty = 0;
1670 out.clear();
1671 out.startSum(bound);
1672 for (Potassco::WeightLitSpan::iterator it = Potassco::begin(body.lits), end = Potassco::end(body.lits); it != end && bound > 0; ++it) {
1673 POTASSCO_CHECK(it->weight >= 0, EDOM, "Non-negative weight expected!");
1674 POTASSCO_CHECK(Potassco::atom(*it) < bodyId, EOVERFLOW, "Atom out of bounds");
1675 if (it->weight == 0) continue; // skip irrelevant lits
1676 PrgAtom* a = resize(Potassco::atom(*it));
1677 Literal p = Literal(a->id(), Potassco::lit(*it) < 0);// replace any eq atoms
1678 ValueRep v = litVal(a, !p.sign());
1679 weight_t w = Potassco::weight(*it);
1680 if (v == value_true) { bound -= w; }
1681 else if (v != value_false) {
1682 POTASSCO_CHECK((CLASP_WEIGHT_T_MAX-sumW)>= w, EOVERFLOW, "Integer overflow!");
1683 sumW += w;
1684 if (!atomState_.inBody(p)) {
1685 atomState_.addToBody(p);
1686 out.addGoal(toInt(p), w);
1687 meta.pos += !p.sign();
1688 meta.hash += hashLit(p);
1689 }
1690 else { // Merge duplicate lits
1691 Potassco::WeightLit_t* pos = std::find_if(out.wlits_begin(), out.wlits_end(), IsLit(toInt(p)));
1692 POTASSCO_ASSERT(pos != out.wlits_end());
1693 w = (pos->weight += w);
1694 ++dirty;
1695 }
1696 if (w > maxW) { maxW = w; }
1697 if (w < minW) { minW = w; }
1698 dirty += static_cast<weight_t>(atomState_.inBody(~p));
1699 }
1700 }
1701 weight_t sumR = sumW;
1702 if (bound > 0 && (dirty || maxW > bound)) {
1703 sumR = 0, minW = CLASP_WEIGHT_T_MAX;
1704 for (Potassco::WeightLit_t* it = out.wlits_begin(), *end = out.wlits_end(); it != end; ++it) {
1705 Literal p = toLit(it->lit);
1706 weight_t w = it->weight;
1707 if (w > bound) { sumW -= (w - bound); it->weight = (maxW = w = bound); }
1708 if (w < minW) { minW = w; }
1709 sumR += w;
1710 if (p.sign() && atomState_.inBody(~p)) {
1711 // body contains p and ~p: we can achieve at most max(weight(p), weight(~p))
1712 sumR -= std::min(w, std::find_if(out.wlits_begin(), end, IsLit(Potassco::neg(it->lit)))->weight);
1713 }
1714 }
1715 }
1716 out.setBound(bound);
1717 if (bound <= 0 || sumR < bound) {
1718 for (const Potassco::WeightLit_t* it = out.wlits_begin(), *end = out.wlits_end(); it != end; ++it) { atomState_.clearRule(Potassco::atom(*it)); }
1719 return bound <= 0 && simplifyNormal(ht, head, Potassco::toSpan<Potassco::Lit_t>(), out, meta);
1720 }
1721 else if ((sumW - minW) < bound) {
1722 out.weaken(Body_t::Normal);
1723 meta.bid = findBody(meta.hash, Body_t::Normal, toU32(size(out.body())));
1724 bool ok = pushHead(ht, head, 0, out);
1725 for (const Potassco::Lit_t* it = out.lits_begin(), *end = out.lits_end(); it != end; ++it) {
1726 atomState_.clearRule(Potassco::atom(*it));
1727 }
1728 return ok;
1729 }
1730 else if (minW == maxW) {
1731 out.weaken(Body_t::Count, maxW != 1);
1732 bound = out.bound();
1733 }
1734 meta.bid = findBody(meta.hash, out.bodyType(), (uint32_t)std::distance(out.wlits_begin(), out.wlits_end()), out.bound(), out.wlits_begin());
1735 bool ok = pushHead(ht, head, sumW - out.bound(), out);
1736 for (const Potassco::WeightLit_t* it = out.wlits_begin(), *end = out.wlits_end(); it != end; ++it) {
1737 atomState_.clearRule(Potassco::atom(*it));
1738 }
1739 return ok;
1740 }
1741
1742 // Pushes the given rule head to the body given in out.
1743 // Pre: Body literals are marked and lits is != 0 if body is a sum.
pushHead(Head_t ht,const Potassco::AtomSpan & head,weight_t slack,RuleBuilder & out)1744 bool LogicProgram::pushHead(Head_t ht, const Potassco::AtomSpan& head, weight_t slack, RuleBuilder& out) {
1745 const uint8 ignoreMask = AtomState::false_flag|AtomState::head_flag;
1746 uint32 hs = 0;
1747 bool sat = false, sum = out.bodyType() == Body_t::Sum;
1748 out.start(ht);
1749 for (Potassco::AtomSpan::iterator it = Potassco::begin(head), end = Potassco::end(head); it != end; ++it) {
1750 if (!atomState_.isSet(*it, AtomState::simp_mask)) {
1751 out.addHead(*it);
1752 atomState_.addToHead(*it);
1753 ++hs;
1754 }
1755 else if (!atomState_.isSet(*it, ignoreMask)) { // h occurs in B+ and/or B- or is true
1756 weight_t wp = weight_t(atomState_.inBody(posLit(*it))), wn = weight_t(atomState_.inBody(negLit(*it)));
1757 if (wp && sum) { wp = std::find_if(out.wlits_begin(), out.wlits_end(), IsLit(Potassco::lit(*it)))->weight; }
1758 if (wn && sum) { wn = std::find_if(out.wlits_begin(), out.wlits_end(), IsLit(Potassco::neg(*it)))->weight; }
1759 if (atomState_.isFact(*it) || wp > slack) { sat = true; }
1760 else if (wn <= slack) {
1761 out.addHead(*it);
1762 atomState_.addToHead(*it);
1763 ++hs;
1764 }
1765 }
1766 }
1767 for (const Atom_t* it = out.head_begin(), *end = it + hs; it != end; ++it) {
1768 atomState_.clearRule(*it);
1769 }
1770 return !sat || (ht == Head_t::Choice && hs);
1771 }
1772
simplifyRule(const Rule & r,Potassco::RuleBuilder & out,SRule & meta)1773 bool LogicProgram::simplifyRule(const Rule& r, Potassco::RuleBuilder& out, SRule& meta) {
1774 return r.normal()
1775 ? simplifyNormal(r.ht, r.head, r.cond, out, meta)
1776 : simplifySum(r.ht, r.head, r.agg, out, meta);
1777 }
1778 // create new atom aux representing supports, i.e.
1779 // aux == S1 v ... v Sn
getEqAtomLit(Literal lit,const BodyList & supports,Preprocessor & p,const SccMap & sccMap)1780 Literal LogicProgram::getEqAtomLit(Literal lit, const BodyList& supports, Preprocessor& p, const SccMap& sccMap) {
1781 if (supports.empty() || lit == lit_false()) {
1782 return lit_false();
1783 }
1784 else if (supports.size() == 1 && supports[0]->size() < 2 && supports.back()->literal() == lit) {
1785 return supports[0]->size() == 0 ? lit_true() : supports[0]->goal(0);
1786 }
1787 else if (p.getRootAtom(lit) != varMax) {
1788 return posLit(p.getRootAtom(lit));
1789 }
1790 incTrAux(1);
1791 Atom_t auxV = newAtom();
1792 PrgAtom* aux = getAtom(auxV);
1793 uint32 scc = PrgNode::noScc;
1794 aux->setLiteral(lit);
1795 aux->setSeen(true);
1796 p.setRootAtom(aux->literal(), auxV);
1797 for (BodyList::const_iterator sIt = supports.begin(); sIt != supports.end(); ++sIt) {
1798 PrgBody* b = *sIt;
1799 if (b->relevant() && b->value() != value_false) {
1800 for (uint32 g = 0; scc == PrgNode::noScc && g != b->size() && !b->goal(g).sign(); ++g) {
1801 uint32 aScc = getAtom(b->goal(g).var())->scc();
1802 if (aScc != PrgNode::noScc && (sccMap[aScc] & 1u)) { scc = aScc; }
1803 }
1804 b->addHead(aux, PrgEdge::Normal);
1805 if (b->value() != value_free && !assignValue(aux, b->value(), PrgEdge::newEdge(*b, PrgEdge::Normal))) {
1806 break;
1807 }
1808 aux->setInUpper(true);
1809 }
1810 }
1811 if (!aux->inUpper()) {
1812 aux->setValue(value_false);
1813 return lit_false();
1814 }
1815 else if (scc != PrgNode::noScc) {
1816 aux->setScc(scc);
1817 auxData_->scc.push_back(aux);
1818 }
1819 return posLit(auxV);
1820 }
1821
getBodyFor(const Rule & r,const SRule & meta,bool addDeps)1822 PrgBody* LogicProgram::getBodyFor(const Rule& r, const SRule& meta, bool addDeps) {
1823 if (meta.bid < bodies_.size()) {
1824 return getBody(meta.bid);
1825 }
1826 // no corresponding body exists, create a new object
1827 PrgBody* b = PrgBody::create(*this, numBodies(), r, meta.pos, addDeps);
1828 bodyIndex_.insert(IndexMap::value_type(meta.hash, b->id()));
1829 bodies_.push_back(b);
1830 if (b->isSupported()) {
1831 initialSupp_.push_back(b->id());
1832 }
1833 upStat(r.bt);
1834 return b;
1835 }
getTrueBody()1836 PrgBody* LogicProgram::getTrueBody() {
1837 uint32 id = findBody(0, Body_t::Normal, 0);
1838 if (id < bodies_.size()) {
1839 return getBody(id);
1840 }
1841 return getBodyFor(Rule::normal(Head_t::Choice, Potassco::toSpan<Atom_t>(), Potassco::toSpan<Potassco::Lit_t>()), SRule());
1842 }
assignBodyFor(const Rule & r,const SRule & meta,EdgeType depEdge,bool simpStrong)1843 PrgBody* LogicProgram::assignBodyFor(const Rule& r, const SRule& meta, EdgeType depEdge, bool simpStrong) {
1844 PrgBody* b = getBodyFor(r, meta, depEdge != PrgEdge::Gamma);
1845 if (!b->hasVar() && !b->seen()) {
1846 uint32 eqId;
1847 b->markDirty();
1848 b->simplify(*this, simpStrong, &eqId);
1849 if (eqId != b->id()) {
1850 assert(b->id() == bodies_.size()-1);
1851 removeBody(b, meta.hash);
1852 bodies_.pop_back();
1853 if (depEdge != PrgEdge::Gamma) {
1854 for (uint32 i = 0; i != b->size(); ++i) {
1855 getAtom(b->goal(i).var())->removeDep(b->id(), !b->goal(i).sign());
1856 }
1857 }
1858 b->destroy();
1859 b = bodies_[eqId];
1860 }
1861 }
1862 b->setSeen(true);
1863 b->assignVar(*this);
1864 return b;
1865 }
1866
equalLits(const PrgBody & b,const WeightLitSpan & lits) const1867 bool LogicProgram::equalLits(const PrgBody& b, const WeightLitSpan& lits) const {
1868 WeightLitSpan::iterator lBeg = Potassco::begin(lits), lEnd = Potassco::end(lits);
1869 for (uint32 i = 0, end = b.size(); i != end; ++i) {
1870 Potassco::WeightLit_t wl = { toInt(b.goal(i)), b.weight(i) };
1871 if (!std::binary_search(lBeg, lEnd, wl)) { return false; }
1872 }
1873 return true;
1874 }
1875
1876 // Pre: all literals in body are marked.
findBody(uint32 hash,Body_t type,uint32 size,weight_t bound,Potassco::WeightLit_t * sum)1877 uint32 LogicProgram::findBody(uint32 hash, Body_t type, uint32 size, weight_t bound, Potassco::WeightLit_t* sum) {
1878 IndexRange bodies = bodyIndex_.equal_range(hash);
1879 bool sorted = false;
1880 if (type == Body_t::Normal) { bound = static_cast<weight_t>(size); }
1881 for (IndexIter it = bodies.first; it != bodies.second; ++it) {
1882 const PrgBody& b = *getBody(it->second);
1883 if (!checkBody(b, type, size, bound) || !atomState_.inBody(b.goals_begin(), b.goals_end())) {
1884 continue;
1885 }
1886 else if (!b.hasWeights()) {
1887 return b.id();
1888 }
1889 else if (sum) {
1890 if (!sorted) {
1891 std::sort(sum, sum + size);
1892 sorted = true;
1893 }
1894 if (equalLits(b, Potassco::toSpan(sum, size))) { return b.id(); }
1895 }
1896 }
1897 return varMax;
1898 }
1899
findEqBody(const PrgBody * b,uint32 hash)1900 uint32 LogicProgram::findEqBody(const PrgBody* b, uint32 hash) {
1901 IndexRange bodies = bodyIndex_.equal_range(hash);
1902 if (bodies.first == bodies.second) { return varMax; }
1903 uint32 eqId = varMax, n = 0, r = 0;
1904 for (IndexIter it = bodies.first; it != bodies.second && eqId == varMax; ++it) {
1905 const PrgBody& rhs = *getBody(it->second);
1906 if (!checkBody(rhs, b->type(), b->size(), b->bound())) { continue; }
1907 else if (b->size() == 0) { eqId = rhs.id(); }
1908 else if (b->size() == 1) { eqId = b->goal(0) == rhs.goal(0) && b->weight(0) == rhs.weight(0) ? rhs.id() : varMax; }
1909 else {
1910 if (++n == 1) { std::for_each(b->goals_begin(), b->goals_end(), std::bind1st(std::mem_fun(&AtomState::addToBody), &atomState_)); }
1911 if (!atomState_.inBody(rhs.goals_begin(), rhs.goals_end())) { continue; }
1912 else if (!b->hasWeights()) { eqId = rhs.id(); }
1913 else {
1914 if (n == 1 || r == 0) {
1915 rule_.clear();
1916 if (!b->toData(*this, rule_) || rule_.bodyType() != Body_t::Sum) {
1917 rule_.clear();
1918 continue;
1919 }
1920 r = 1;
1921 std::sort(rule_.wlits_begin(), rule_.wlits_end());
1922 }
1923 if (equalLits(rhs, rule_.sum().lits)) { eqId = rhs.id(); }
1924 }
1925 }
1926 }
1927 if (n) {
1928 rule_.clear();
1929 std::for_each(b->goals_begin(), b->goals_end(), std::bind1st(std::mem_fun(&AtomState::clearBody), &atomState_));
1930 }
1931 return eqId;
1932 }
1933
getDisjFor(const Potassco::AtomSpan & head,uint32 headHash)1934 PrgDisj* LogicProgram::getDisjFor(const Potassco::AtomSpan& head, uint32 headHash) {
1935 PrgDisj* d = 0;
1936 if (headHash) {
1937 LogicProgram::IndexRange eqRange = disjIndex_.equal_range(headHash);
1938 for (; eqRange.first != eqRange.second; ++eqRange.first) {
1939 PrgDisj& o = *disjunctions_[eqRange.first->second];
1940 if (o.relevant() && o.size() == Potassco::size(head) && atomState_.allMarked(o.begin(), o.end(), AtomState::head_flag)) {
1941 assert(o.id() == eqRange.first->second);
1942 d = &o;
1943 break;
1944 }
1945 }
1946 for (Potassco::AtomSpan::iterator it = Potassco::begin(head), end = Potassco::end(head); it != end; ++it) {
1947 atomState_.clearRule(*it);
1948 }
1949 }
1950 if (!d) {
1951 // no corresponding disjunction exists, create a new object
1952 // and link it to all atoms
1953 ++stats.disjunctions[statsId_];
1954 d = PrgDisj::create((uint32)disjunctions_.size(), head);
1955 disjunctions_.push_back(d);
1956 PrgEdge edge = PrgEdge::newEdge(*d, PrgEdge::Choice);
1957 for (Potassco::AtomSpan::iterator it = Potassco::begin(head), end = Potassco::end(head); it != end; ++it) {
1958 getAtom(*it)->addSupport(edge);
1959 }
1960 if (headHash) {
1961 disjIndex_.insert(IndexMap::value_type(headHash, d->id()));
1962 }
1963 }
1964 return d;
1965 }
1966
1967 // body has changed - update index
update(PrgBody * body,uint32 oldHash,uint32 newHash)1968 uint32 LogicProgram::update(PrgBody* body, uint32 oldHash, uint32 newHash) {
1969 uint32 id = removeBody(body, oldHash);
1970 if (body->relevant()) {
1971 uint32 eqId = findEqBody(body, newHash);
1972 if (eqId == varMax) {
1973 // No equivalent body found.
1974 // Add new entry to index
1975 bodyIndex_.insert(IndexMap::value_type(newHash, id));
1976 }
1977 return eqId;
1978 }
1979 return varMax;
1980 }
1981
1982 // body b has changed - remove old entry from body node index
removeBody(PrgBody * b,uint32 hash)1983 uint32 LogicProgram::removeBody(PrgBody* b, uint32 hash) {
1984 IndexRange ra = bodyIndex_.equal_range(hash);
1985 uint32 id = b->id();
1986 for (; ra.first != ra.second; ++ra.first) {
1987 if (bodies_[ra.first->second] == b) {
1988 id = ra.first->second;
1989 bodyIndex_.erase(ra.first);
1990 break;
1991 }
1992 }
1993 return id;
1994 }
1995
mergeEqAtoms(PrgAtom * a,Id_t rootId)1996 PrgAtom* LogicProgram::mergeEqAtoms(PrgAtom* a, Id_t rootId) {
1997 PrgAtom* root = getAtom(rootId = getRootId(rootId));
1998 ValueRep mv = getMergeValue(a, root);
1999 assert(!a->eq() && !root->eq() && !a->frozen());
2000 if (a->ignoreScc()) { root->setIgnoreScc(true); }
2001 if (mv != a->value() && !assignValue(a, mv, PrgEdge::noEdge())) { return 0; }
2002 if (mv != root->value() && !assignValue(root, mv, PrgEdge::noEdge())){ return 0; }
2003 a->setEq(rootId);
2004 incEqs(Var_t::Atom);
2005 return root;
2006 }
2007
2008 // returns whether posSize(root) <= posSize(body)
positiveLoopSafe(PrgBody * body,PrgBody * root) const2009 bool LogicProgram::positiveLoopSafe(PrgBody* body, PrgBody* root) const {
2010 uint32 i = 0, end = std::min(body->size(), root->size());
2011 while (i != end && body->goal(i).sign() == root->goal(i).sign()) { ++i; }
2012 return i == root->size() || root->goal(i).sign();
2013 }
2014
mergeEqBodies(PrgBody * b,Id_t rootId,bool hashEq,bool atomsAssigned)2015 PrgBody* LogicProgram::mergeEqBodies(PrgBody* b, Id_t rootId, bool hashEq, bool atomsAssigned) {
2016 PrgBody* root = getBody(rootId = getEqNode(bodies_, rootId));
2017 bool bp = options().backprop != 0;
2018 if (b == root) { return root; }
2019 assert(!b->eq() && !root->eq() && (hashEq || b->literal() == root->literal()));
2020 if (!b->simplifyHeads(*this, atomsAssigned) || (b->value() != root->value() && (!mergeValue(b, root) || !root->propagateValue(*this, bp) || !b->propagateValue(*this, bp)))) {
2021 setConflict();
2022 return 0;
2023 }
2024 if (hashEq || positiveLoopSafe(b, root)) {
2025 b->setLiteral(root->literal());
2026 if (!root->mergeHeads(*this, *b, atomsAssigned, !hashEq)) {
2027 setConflict();
2028 return 0;
2029 }
2030 incEqs(Var_t::Body);
2031 b->setEq(rootId);
2032 return root;
2033 }
2034 return b;
2035 }
2036
findName(Atom_t x) const2037 const char* LogicProgram::findName(Atom_t x) const {
2038 for (OutputTable::pred_iterator it = ctx()->output.pred_begin(), end = ctx()->output.pred_end(); it != end; ++it) {
2039 if (it->user == x) { return it->name; }
2040 }
2041 for (ShowVec::const_iterator it = show_.begin(), end = show_.end(); it != end; ++it) {
2042 if (it->first == x){ return it->second; }
2043 }
2044 return "";
2045 }
getSupportedBodies(bool sorted)2046 VarVec& LogicProgram::getSupportedBodies(bool sorted) {
2047 if (sorted) {
2048 std::stable_sort(initialSupp_.begin(), initialSupp_.end(), LessBodySize(bodies_));
2049 }
2050 return initialSupp_;
2051 }
2052
falseAtom()2053 Atom_t LogicProgram::falseAtom() {
2054 Atom_t aFalse = 0;
2055 for (Var i = 1; i < atoms_.size() && !aFalse; ++i) {
2056 if (atoms_[i]->value() == value_false || atomState_.isSet(i, AtomState::false_flag)) {
2057 aFalse = i;
2058 }
2059 }
2060 if (!aFalse) {
2061 bool s = frozen();
2062 setFrozen(false);
2063 aFalse = newAtom();
2064 assignValue(getAtom(aFalse), value_false, PrgEdge::noEdge());
2065 setFrozen(s);
2066 }
2067 return aFalse;
2068 }
2069
extractCondition(Id_t id,Potassco::LitVec & out) const2070 bool LogicProgram::extractCondition(Id_t id, Potassco::LitVec& out) const {
2071 out.clear();
2072 if (id == Clasp::Asp::falseId || (frozen() && getLiteral(id) == lit_false())) { return false; }
2073 if (!id || isAtom(id)) {
2074 out.assign(id != 0, Potassco::lit(id));
2075 return true;
2076 }
2077 Id_t bId = nodeId(id);
2078 POTASSCO_ASSERT(validBody(bId), "Invalid literal");
2079 const PrgBody* B = getBody(getEqBody(bId));
2080 out.reserve(B->size());
2081 for (PrgBody::goal_iterator it = B->goals_begin(), end = B->goals_end(); it != end; ++it) {
2082 out.push_back( toInt(*it) );
2083 }
2084 return true;
2085 }
2086 #undef RT
2087 /////////////////////////////////////////////////////////////////////////////////////////
2088 // class LogicProgramAdapter
2089 /////////////////////////////////////////////////////////////////////////////////////////
LogicProgramAdapter(LogicProgram & prg)2090 LogicProgramAdapter::LogicProgramAdapter(LogicProgram& prg) : lp_(&prg), inc_(false) {}
initProgram(bool inc)2091 void LogicProgramAdapter::initProgram(bool inc) {
2092 inc_ = inc;
2093 }
beginStep()2094 void LogicProgramAdapter::beginStep() {
2095 if (inc_ || lp_->frozen()) { lp_->updateProgram(); }
2096 }
endStep()2097 void LogicProgramAdapter::endStep() {
2098
2099 }
rule(Potassco::Head_t ht,const Potassco::AtomSpan & head,const Potassco::LitSpan & body)2100 void LogicProgramAdapter::rule(Potassco::Head_t ht, const Potassco::AtomSpan& head, const Potassco::LitSpan& body) {
2101 lp_->addRule(ht, head, body);
2102 }
rule(Potassco::Head_t ht,const Potassco::AtomSpan & head,Potassco::Weight_t bound,const Potassco::WeightLitSpan & body)2103 void LogicProgramAdapter::rule(Potassco::Head_t ht, const Potassco::AtomSpan& head, Potassco::Weight_t bound, const Potassco::WeightLitSpan& body) {
2104 lp_->addRule(ht, head, bound, body);
2105 }
minimize(Potassco::Weight_t prio,const Potassco::WeightLitSpan & lits)2106 void LogicProgramAdapter::minimize(Potassco::Weight_t prio, const Potassco::WeightLitSpan& lits) {
2107 lp_->addMinimize(prio, lits);
2108 }
project(const Potassco::AtomSpan & atoms)2109 void LogicProgramAdapter::project(const Potassco::AtomSpan& atoms) {
2110 lp_->addProject(atoms);
2111 }
output(const Potassco::StringSpan & str,const Potassco::LitSpan & cond)2112 void LogicProgramAdapter::output(const Potassco::StringSpan& str, const Potassco::LitSpan& cond) {
2113 lp_->addOutput(ConstString(str), cond);
2114 }
external(Potassco::Atom_t a,Potassco::Value_t v)2115 void LogicProgramAdapter::external(Potassco::Atom_t a, Potassco::Value_t v) {
2116 lp_->addExternal(a, v);
2117 }
assume(const Potassco::LitSpan & lits)2118 void LogicProgramAdapter::assume(const Potassco::LitSpan& lits) {
2119 lp_->addAssumption(lits);
2120 }
heuristic(Potassco::Atom_t a,Potassco::Heuristic_t t,int bias,unsigned prio,const Potassco::LitSpan & cond)2121 void LogicProgramAdapter::heuristic(Potassco::Atom_t a, Potassco::Heuristic_t t, int bias, unsigned prio, const Potassco::LitSpan& cond) {
2122 lp_->addDomHeuristic(a, t, bias, prio, cond);
2123 }
acycEdge(int s,int t,const Potassco::LitSpan & cond)2124 void LogicProgramAdapter::acycEdge(int s, int t, const Potassco::LitSpan& cond) {
2125 lp_->addAcycEdge(static_cast<uint32>(s), static_cast<uint32>(t), cond);
2126 }
theoryTerm(Potassco::Id_t termId,int number)2127 void LogicProgramAdapter::theoryTerm(Potassco::Id_t termId, int number) {
2128 lp_->theoryData().addTerm(termId, number);
2129 }
theoryTerm(Potassco::Id_t termId,const Potassco::StringSpan & name)2130 void LogicProgramAdapter::theoryTerm(Potassco::Id_t termId, const Potassco::StringSpan& name) {
2131 lp_->theoryData().addTerm(termId, name);
2132 }
theoryTerm(Potassco::Id_t termId,int cId,const Potassco::IdSpan & args)2133 void LogicProgramAdapter::theoryTerm(Potassco::Id_t termId, int cId, const Potassco::IdSpan& args) {
2134 if (cId >= 0) { lp_->theoryData().addTerm(termId, static_cast<Potassco::Id_t>(cId), args); }
2135 else { lp_->theoryData().addTerm(termId, static_cast<Potassco::Tuple_t>(cId), args); }
2136 }
theoryElement(Potassco::Id_t elementId,const Potassco::IdSpan & terms,const Potassco::LitSpan & cond)2137 void LogicProgramAdapter::theoryElement(Potassco::Id_t elementId, const Potassco::IdSpan& terms, const Potassco::LitSpan& cond) {
2138 lp_->theoryData().addElement(elementId, terms, lp_->newCondition(cond));
2139 }
theoryAtom(Potassco::Id_t atomOrZero,Potassco::Id_t termId,const Potassco::IdSpan & elements)2140 void LogicProgramAdapter::theoryAtom(Potassco::Id_t atomOrZero, Potassco::Id_t termId, const Potassco::IdSpan& elements) {
2141 lp_->theoryData().addAtom(atomOrZero, termId, elements);
2142 }
theoryAtom(Potassco::Id_t atomOrZero,Potassco::Id_t termId,const Potassco::IdSpan & elements,Potassco::Id_t op,Potassco::Id_t rhs)2143 void LogicProgramAdapter::theoryAtom(Potassco::Id_t atomOrZero, Potassco::Id_t termId, const Potassco::IdSpan& elements, Potassco::Id_t op, Potassco::Id_t rhs) {
2144 lp_->theoryData().addAtom(atomOrZero, termId, elements, op, rhs);
2145 }
2146 } } // end namespace Asp
2147
2148