1 //
2 // Copyright (c) 2010-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/dependency_graph.h>
25 #include <clasp/solver.h>
26 #include <clasp/clause.h>
27 #include <clasp/solve_algorithms.h>
28 #include <clasp/util/timer.h>
29 namespace Clasp {
SolveTestEvent(const Solver & s,uint32 a_hcc,bool part)30 SolveTestEvent::SolveTestEvent(const Solver& s, uint32 a_hcc, bool part)
31 : SolveEvent<SolveTestEvent>(s, Event::verbosity_max)
32 , result(-1), hcc(a_hcc), partial(part) {
33 confDelta = s.stats.conflicts;
34 choiceDelta = s.stats.choices;
35 time = 0.0;
36 }
choices() const37 uint64 SolveTestEvent::choices() const {
38 return solver->stats.choices - choiceDelta;
39 }
conflicts() const40 uint64 SolveTestEvent::conflicts() const {
41 return solver->stats.conflicts - confDelta;
42 }
43 namespace Asp {
44 /////////////////////////////////////////////////////////////////////////////////////////
45 // class PrgDepGraph
46 /////////////////////////////////////////////////////////////////////////////////////////
PrgDepGraph(NonHcfMapType m)47 PrgDepGraph::PrgDepGraph(NonHcfMapType m) {
48 // add sentinal atom needed for disjunctions
49 createAtom(lit_false(), PrgNode::noScc);
50 VarVec adj; adj.push_back(idMax);
51 initAtom(sentinel_atom, 0, adj, 0);
52 seenComponents_ = 0;
53 mapType_ = (uint32)m;
54 stats_ = 0;
55 }
56
~PrgDepGraph()57 PrgDepGraph::~PrgDepGraph() {
58 for (AtomVec::size_type i = 0; i != atoms_.size(); ++i) {
59 delete [] atoms_[i].adj_;
60 }
61 for (AtomVec::size_type i = 0; i != bodies_.size(); ++i) {
62 delete [] bodies_[i].adj_;
63 }
64 delete stats_;
65 while (!components_.empty()) {
66 delete components_.back();
67 components_.pop_back();
68 }
69 }
relevantPrgAtom(const Solver & s,PrgAtom * a) const70 bool PrgDepGraph::relevantPrgAtom(const Solver& s, PrgAtom* a) const {
71 return !a->ignoreScc() && a->inUpper() && a->scc() != PrgNode::noScc && !s.isFalse(a->literal());
72 }
relevantPrgBody(const Solver & s,PrgBody * b) const73 bool PrgDepGraph::relevantPrgBody(const Solver& s, PrgBody* b) const {
74 return !s.isFalse(b->literal());
75 }
76
77 // Creates a positive-body-atom-dependency graph (PBADG)
78 // The PBADG contains a node for each atom A of a non-trivial SCC and
79 // a node for each body B, s.th. there is a non-trivially connected atom A with
80 // B in body(A).
81 // Pre : b->seen() = 1 for all new and relevant bodies b
82 // Post: b->seen() = 0 for all bodies that were added to the PBADG
addSccs(LogicProgram & prg,const AtomList & sccAtoms,const NonHcfSet & nonHcfs)83 void PrgDepGraph::addSccs(LogicProgram& prg, const AtomList& sccAtoms, const NonHcfSet& nonHcfs) {
84 // Pass 1: Create graph atom nodes and estimate number of bodies
85 atoms_.reserve(atoms_.size() + sccAtoms.size());
86 AtomList::size_type numBodies = 0;
87 SharedContext& ctx = *prg.ctx();
88 for (AtomList::size_type i = 0, end = sccAtoms.size(); i != end; ++i) {
89 PrgAtom* a = sccAtoms[i];
90 if (relevantPrgAtom(*ctx.master(), a)) {
91 // add graph atom node and store link between program node and graph node for later lookup
92 a->resetId(createAtom(a->literal(), a->scc()), true);
93 // atom is defined by more than just a bunch of clauses
94 ctx.setFrozen(a->var(), true);
95 numBodies += a->supports();
96 }
97 }
98 // Pass 2: Init atom nodes and create body nodes
99 VarVec adj, ext;
100 bodies_.reserve(bodies_.size() + numBodies/2);
101 PrgBody* prgBody; PrgDisj* prgDis;
102 for (AtomList::size_type i = 0, end = sccAtoms.size(); i != end; ++i) {
103 PrgAtom* a = sccAtoms[i];
104 if (relevantPrgAtom(*ctx.master(), a)) {
105 uint32 prop = 0;
106 for (PrgAtom::sup_iterator it = a->supps_begin(), endIt = a->supps_end(); it != endIt; ++it) {
107 assert(it->isBody() || it->isDisj());
108 NodeId bId= PrgNode::noNode;
109 if (it->isBody() && !it->isGamma()) {
110 prgBody = prg.getBody(it->node());
111 bId = relevantPrgBody(*ctx.master(), prgBody) ? addBody(prg, prgBody) : PrgNode::noNode;
112 }
113 else if (it->isDisj()) {
114 prgDis = prg.getDisj(it->node());
115 bId = addDisj(prg, prgDis);
116 prop |= AtomNode::property_in_disj;
117 }
118 if (bId != PrgNode::noNode) {
119 if (!bodies_[bId].seen()) {
120 bodies_[bId].seen(true);
121 adj.push_back(bId);
122 }
123 if (it->isChoice()) {
124 // mark atom as in choice
125 prop |= AtomNode::property_in_choice;
126 }
127 }
128 }
129 uint32 nPred= (uint32)adj.size();
130 for (PrgAtom::dep_iterator it = a->deps_begin(), endIt = a->deps_end(); it != endIt; ++it) {
131 if (!it->sign()) {
132 prgBody = prg.getBody(it->var());
133 if (relevantPrgBody(*ctx.master(), prgBody) && prgBody->scc(prg) == a->scc()) {
134 NodeId bodyId = addBody(prg, prgBody);
135 if (!bodies_[bodyId].extended()) {
136 adj.push_back(bodyId);
137 }
138 else {
139 ext.push_back(bodyId);
140 ext.push_back(bodies_[bodyId].get_pred_idx(a->id()));
141 assert(bodies_[bodyId].get_pred(ext.back()) == a->id());
142 prop |= AtomNode::property_in_ext;
143 }
144 }
145 }
146 }
147 if (!ext.empty()) {
148 adj.push_back(idMax);
149 adj.insert(adj.end(), ext.begin(), ext.end());
150 }
151 adj.push_back(idMax);
152 initAtom(a->id(), prop, adj, nPred);
153 adj.clear(); ext.clear();
154 }
155 }
156 if (nonHcfs.size() != 0 && stats_ == 0 && nonHcfs.config && nonHcfs.config->context().stats) {
157 stats_ = enableNonHcfStats(nonHcfs.config->context().stats, prg.isIncremental());
158 }
159 // "update" existing non-hcf components
160 for (NonHcfIter it = nonHcfBegin(), end = nonHcfEnd(); it != end; ++it) {
161 (*it)->update(ctx);
162 }
163 // add new non-hcf components
164 uint32 hcc = seenComponents_;
165 for (NonHcfSet::const_iterator it = nonHcfs.begin() + seenComponents_, end = nonHcfs.end(); it != end; ++it, ++hcc) {
166 addNonHcf(hcc, ctx, nonHcfs.config, *it);
167 }
168 seenComponents_ = nonHcfs.size();
169 }
170
createAtom(Literal lit,uint32 aScc)171 uint32 PrgDepGraph::createAtom(Literal lit, uint32 aScc) {
172 NodeId id = (uint32)atoms_.size();
173 atoms_.push_back(AtomNode());
174 AtomNode& ua = atoms_.back();
175 ua.lit = lit;
176 ua.scc = aScc;
177 return id;
178 }
179
initAtom(uint32 id,uint32 prop,const VarVec & adj,uint32 numPreds)180 void PrgDepGraph::initAtom(uint32 id, uint32 prop, const VarVec& adj, uint32 numPreds) {
181 AtomNode& ua = atoms_[id];
182 ua.setProperties(prop);
183 ua.adj_ = new NodeId[adj.size()];
184 ua.sep_ = ua.adj_ + numPreds;
185 NodeId* sExt = ua.adj_;
186 NodeId* sSame= sExt + numPreds;
187 uint32 aScc = ua.scc;
188 for (VarVec::const_iterator it = adj.begin(), end = adj.begin()+numPreds; it != end; ++it) {
189 BodyNode& bn = bodies_[*it];
190 if (bn.scc != aScc) { *sExt++ = *it; }
191 else { *--sSame= *it; }
192 bn.seen(false);
193 }
194 std::reverse(sSame, ua.adj_ + numPreds);
195 std::copy(adj.begin()+numPreds, adj.end(), ua.sep_);
196 }
197
createBody(PrgBody * b,uint32 bScc)198 uint32 PrgDepGraph::createBody(PrgBody* b, uint32 bScc) {
199 NodeId id = (uint32)bodies_.size();
200 bodies_.push_back(BodyNode(b, bScc));
201 return id;
202 }
203
204 // Creates and initializes a body node for the given body b.
addBody(const LogicProgram & prg,PrgBody * b)205 uint32 PrgDepGraph::addBody(const LogicProgram& prg, PrgBody* b) {
206 if (b->seen()) { // first time we see this body -
207 VarVec preds, atHeads;
208 uint32 bScc = b->scc(prg);
209 NodeId bId = createBody(b, bScc);
210 addPreds(prg, b, bScc, preds);
211 addHeads(prg, b, atHeads);
212 initBody(bId, preds, atHeads);
213 b->resetId(bId, false);
214 prg.ctx()->setFrozen(b->var(), true);
215 }
216 return b->id();
217 }
218
219 // Adds all relevant predecessors of b to preds.
220 // The returned list looks like this:
221 // [[B], a1, [w1], ..., aj, [wj], idMax, l1, [w1], ..., lk, [wk], idMax], where
222 // B is the bound of b (only for card/weight rules),
223 // ai is a positive predecessor from bScc,
224 // wi is the weight of ai (only for weight rules), and
225 // li is a literal of a subgoal from some other scc (only for cardinality/weight rules)
addPreds(const LogicProgram & prg,PrgBody * b,uint32 bScc,VarVec & preds) const226 void PrgDepGraph::addPreds(const LogicProgram& prg, PrgBody* b, uint32 bScc, VarVec& preds) const {
227 if (bScc == PrgNode::noScc) { preds.clear(); return; }
228 const bool weights = b->type() == Body_t::Sum;
229 for (uint32 i = 0; i != b->size() && !b->goal(i).sign(); ++i) {
230 PrgAtom* pred = prg.getAtom(b->goal(i).var());
231 if (relevantPrgAtom(*prg.ctx()->master(), pred) && pred->scc() == bScc) {
232 preds.push_back( pred->id() );
233 if (weights) { preds.push_back(b->weight(i)); }
234 }
235 }
236 if (b->type() != Body_t::Normal) {
237 preds.insert(preds.begin(), b->bound());
238 preds.push_back(idMax);
239 for (uint32 n = 0; n != b->size(); ++n) {
240 PrgAtom* pred = prg.getAtom(b->goal(n).var());
241 bool ext = b->goal(n).sign() || pred->scc() != bScc;
242 Literal lit = b->goal(n).sign() ? ~pred->literal() : pred->literal();
243 if (ext && !prg.ctx()->master()->isFalse(lit)) {
244 preds.push_back(lit.rep());
245 if (weights) { preds.push_back(b->weight(n)); }
246 }
247 }
248 }
249 preds.push_back(idMax);
250 }
251
252 // Splits the heads of b into atoms and disjunctions.
253 // Disjunctions are flattened to sentinel-enclose datom-lists.
addHeads(const LogicProgram & prg,PrgBody * b,VarVec & heads) const254 uint32 PrgDepGraph::addHeads(const LogicProgram& prg, PrgBody* b, VarVec& heads) const {
255 for (PrgBody::head_iterator it = b->heads_begin(), end = b->heads_end(); it != end; ++it) {
256 if (it->isAtom() && !it->isGamma()) {
257 PrgAtom* a = prg.getAtom(it->node());
258 if (relevantPrgAtom(*prg.ctx()->master(), a)) {
259 heads.push_back(a->id());
260 }
261 }
262 else if (it->isDisj()) {
263 assert(prg.getDisj(it->node())->inUpper() && prg.getDisj(it->node())->supports() == 1);
264 PrgDisj* d = prg.getDisj(it->node());
265 // flatten disjunction and enclose in sentinels
266 heads.push_back(sentinel_atom);
267 getAtoms(prg, d, heads);
268 heads.push_back(sentinel_atom);
269 }
270 }
271 return sizeVec(heads);
272 }
273
274 // Adds the atoms from the given disjunction to atoms and returns the disjunction's scc.
getAtoms(const LogicProgram & prg,PrgDisj * d,VarVec & atoms) const275 uint32 PrgDepGraph::getAtoms(const LogicProgram& prg, PrgDisj* d, VarVec& atoms) const {
276 uint32 scc = PrgNode::noScc;
277 for (PrgDisj::atom_iterator it = d->begin(), end = d->end(); it != end; ++it) {
278 PrgAtom* a = prg.getAtom(*it);
279 if (relevantPrgAtom(*prg.ctx()->master(), a)) {
280 assert(scc == PrgNode::noScc || scc == a->scc());
281 atoms.push_back(a->id());
282 scc = a->scc();
283 }
284 }
285 return scc;
286 }
287
288 // Initializes preds and succs lists of the body node with the given id.
initBody(uint32 id,const VarVec & preds,const VarVec & atHeads)289 void PrgDepGraph::initBody(uint32 id, const VarVec& preds, const VarVec& atHeads) {
290 BodyNode* bn = &bodies_[id];
291 uint32 nSuccs= sizeVec(atHeads);
292 bn->adj_ = new NodeId[nSuccs + preds.size()];
293 bn->sep_ = bn->adj_ + nSuccs;
294 NodeId* sSame= bn->adj_;
295 NodeId* sExt = sSame + nSuccs;
296 uint32 bScc = bn->scc;
297 uint32 hScc = PrgNode::noScc;
298 uint32 disj = 0;
299 for (VarVec::const_iterator it = atHeads.begin(), end = atHeads.end(); it != end;) {
300 if (*it) {
301 hScc = getAtom(*it).scc;
302 if (hScc == bScc) { *sSame++ = *it++; }
303 else { *--sExt = *it++; }
304 }
305 else {
306 hScc = getAtom(it[1]).scc; ++disj;
307 if (hScc == bScc) { *sSame++ = *it++; while ( (*sSame++ = *it++) ) { ; } }
308 else { *--sExt = *it++; while ( (*--sExt = *it++) ) { ; } }
309 }
310 }
311 std::copy(preds.begin(), preds.end(), bn->sep_);
312 bn->sep_ += bn->extended();
313 if (disj) { bodies_[id].data |= BodyNode::flag_has_delta; }
314 }
315
addDisj(const LogicProgram & prg,PrgDisj * d)316 uint32 PrgDepGraph::addDisj(const LogicProgram& prg, PrgDisj* d) {
317 assert(d->inUpper() && d->supports() == 1);
318 if (d->seen()) { // first time we see this disjunction
319 PrgBody* prgBody = prg.getBody(d->supps_begin()->node());
320 uint32 bId = PrgNode::noNode;
321 if (relevantPrgBody(*prg.ctx()->master(), prgBody)) {
322 bId = addBody(prg, prgBody);
323 }
324 d->resetId(bId, false);
325 }
326 return d->id();
327 }
328
addNonHcf(uint32 id,SharedContext & ctx,Configuration * config,uint32 scc)329 void PrgDepGraph::addNonHcf(uint32 id, SharedContext& ctx, Configuration* config, uint32 scc) {
330 VarVec sccAtoms, sccBodies;
331 // get all atoms from scc
332 for (uint32 i = 0; i != numAtoms(); ++i) {
333 if (getAtom(i).scc == scc) {
334 sccAtoms.push_back(i);
335 atoms_[i].set(AtomNode::property_in_non_hcf);
336 }
337 }
338 // get all bodies defining an atom in scc
339 const Solver& generator = *ctx.master(); (void)generator;
340 for (uint32 i = 0; i != sccAtoms.size(); ++i) {
341 const AtomNode& a = getAtom(sccAtoms[i]);
342 for (const NodeId* bodyIt = a.bodies_begin(), *bodyEnd = a.bodies_end(); bodyIt != bodyEnd; ++bodyIt) {
343 BodyNode& B = bodies_[*bodyIt];
344 if (!B.seen()) {
345 assert(generator.value(B.lit.var()) != value_free || !generator.seen(B.lit));
346 sccBodies.push_back(*bodyIt);
347 B.seen(true);
348 }
349 }
350 }
351 for (uint32 i = 0; i != sccBodies.size(); ++i) { bodies_[sccBodies[i]].seen(false); }
352 components_.push_back( new NonHcfComponent(id, *this, ctx, config, scc, sccAtoms, sccBodies) );
353 if (stats_) { stats_->addHcc(*components_.back()); }
354 }
simplify(const Solver & s)355 void PrgDepGraph::simplify(const Solver& s) {
356 const bool shared = s.sharedContext()->isShared();
357 ComponentVec::iterator j = components_.begin();
358 for (ComponentVec::iterator it = components_.begin(), end = components_.end(); it != end; ++it) {
359 bool ok = (*it)->simplify(s);
360 if (!shared) {
361 if (ok) { *j++ = *it; }
362 else {
363 if (stats_) { stats_->removeHcc(**it); }
364 delete *it;
365 }
366 }
367 }
368 if (!shared) { components_.erase(j, components_.end()); }
369 }
enableNonHcfStats(uint32 level,bool inc)370 PrgDepGraph::NonHcfStats* PrgDepGraph::enableNonHcfStats(uint32 level, bool inc) {
371 if (!stats_) { stats_ = new NonHcfStats(*this, level, inc); }
372 return stats_;
373 }
374 /////////////////////////////////////////////////////////////////////////////////////////
375 // class PrgDepGraph::NonHcfComponent::ComponentMap
376 /////////////////////////////////////////////////////////////////////////////////////////
377 class PrgDepGraph::NonHcfComponent::ComponentMap {
378 public:
ComponentMap()379 ComponentMap() { static_assert(sizeof(Mapping) == sizeof(uint64), "Invalid padding!"); }
380 struct Mapping {
MappingClasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping381 explicit Mapping(NodeId id) : node(id), var(0), ext(0) { }
382 uint32 node; // node id in dep-graph of generator program P
383 uint32 var : 30; // var in tester solver
384 uint32 ext : 2; // additional data
385 // Atom
disjClasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping386 bool disj() const { return ext != 0u; }
hasTpClasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping387 bool hasTp() const { return ext == 2u; }
upClasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping388 Literal up() const { return posLit(var); }
hpClasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping389 Literal hp() const { assert(disj()); return posLit(var + 1); }
tpClasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping390 Literal tp() const { assert(disj()); return posLit((var + 2)*uint32(hasTp())); }
391 // Body
fbClasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping392 Literal fb() const { return Literal(var, (ext & 1u) != 0u); }
eqClasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping393 bool eq() const { return ext != 0u; }
operator <Clasp::Asp::PrgDepGraph::NonHcfComponent::ComponentMap::Mapping394 bool operator<(const Mapping& other) const { return node < other.node; }
395 };
396 typedef PrgDepGraph SccGraph;
397 typedef PodVector<Mapping>::type NodeMap;
398 typedef NodeMap::iterator MapIt;
399 typedef NodeMap::const_iterator MapIt_c;
400 typedef std::pair<MapIt_c, MapIt_c> MapRange;
401 void addVars(Solver& generator, const SccGraph& dep, const VarVec& atoms, const VarVec& bodies, SharedContext& out);
402 void addAtomConstraints(SharedContext& out);
403 void addBodyConstraints(const Solver& generator, const SccGraph& dep, uint32 scc, SharedContext& out);
404 void mapGeneratorAssignment(const Solver& generator, const SccGraph& dep, LitVec& out) const;
405 void mapTesterModel(const Solver& tester, VarVec& out) const;
406 bool simplify(const Solver& generator, const SccGraph& dep, Solver& tester);
atoms() const407 MapRange atoms() const { return MapRange(mapping.begin(), mapping.begin() + numAtoms); }
bodies() const408 MapRange bodies()const { return MapRange(mapping.begin() + numAtoms, mapping.end()); }
findAtom(NodeId nodeId) const409 MapIt_c findAtom(NodeId nodeId) const { return std::lower_bound(mapping.begin(), mapping.begin()+numAtoms, Mapping(nodeId)); }
410 NodeMap mapping; // maps nodes of P to literals in C;
411 uint32 numAtoms;// number of atoms
412 };
413 // Adds necessary variables for all atoms and bodies to the component program.
414 // Input-Vars: (set via assumptions)
415 // tp: for each atom p in a proper disjunctive head, tp is true iff p is true in P
416 // fb: for each body b, fb is true iff b is false in P
417 // Aux-Var: (derived)
418 // hp: for each atom p in a proper disjunctive head, hp is true iff tp and ~up
419 // Output: (unfounded sets)
420 // up: for each atom p, up is true iff a is unfounded w.r.t the assignment of P.
addVars(Solver & generator,const SccGraph & dep,const VarVec & atoms,const VarVec & bodies,SharedContext & comp)421 void PrgDepGraph::NonHcfComponent::ComponentMap::addVars(Solver& generator, const SccGraph& dep, const VarVec& atoms, const VarVec& bodies, SharedContext& comp) {
422 assert(generator.decisionLevel() == 0);
423 mapping.reserve(atoms.size() + bodies.size());
424 const PrgDepGraph::NonHcfMapType mt = dep.nonHcfMapType();
425 for (VarVec::const_iterator it = atoms.begin(), end = atoms.end(); it != end; ++it) {
426 const AtomNode& at = dep.getAtom(*it);
427 Literal gen = at.lit;
428 if (generator.isFalse(gen)) { continue; }
429 Mapping map(*it);
430 // up [ hp [tp] ]
431 map.var = comp.addVar(Var_t::Atom); // up
432 map.ext = (mt == PrgDepGraph::map_old || at.inDisjunctive());
433 comp.setFrozen(map.var, true);
434 if (map.ext) {
435 comp.addVar(Var_t::Atom); // hp
436 if (!generator.isTrue(gen)) { // tp
437 comp.setFrozen(comp.addVar(Var_t::Atom), true);
438 ++map.ext;
439 }
440 }
441 mapping.push_back(map);
442 }
443 numAtoms = (uint32)mapping.size();
444 std::stable_sort(mapping.begin(), mapping.end());
445 // add necessary vars for bodies
446 for (VarVec::const_iterator it = bodies.begin(), end = bodies.end(); it != end; ++it) {
447 Literal gen = dep.getBody(*it).lit;
448 if (generator.isFalse(gen)) { continue; }
449 Mapping map(*it);
450 if (!generator.seen(gen) && !generator.isTrue(gen)) {
451 map.var = comp.addVar(Var_t::Atom);
452 comp.setFrozen(map.var, true);
453 generator.markSeen(gen);
454 }
455 else if (generator.isTrue(gen)) {
456 map.ext = 1u;
457 }
458 else {
459 map.ext = 2u;
460 for (MapRange r = this->bodies(); r.first != r.second;) {
461 --r.second;
462 if (dep.getBody(r.second->node).lit == gen) {
463 map.var = r.second->var;
464 break;
465 }
466 }
467 }
468 assert(map.var <= comp.numVars() && (map.var || map.ext == 1u));
469 mapping.push_back(map);
470 }
471 for (MapRange r = this->bodies(); r.first != r.second; ++r.first) {
472 if (!r.first->eq()) {
473 Var v = dep.getBody(r.first->node).lit.var();
474 generator.clearSeen(v);
475 }
476 }
477 }
478
479 // Adds constraints stemming from the given atoms to the component program.
480 // 1. [up(a0) v ... v up(an-1)], where
481 // - ai is an atom in P from the given atom set, and
482 // - up(ai) is the corresponding output-atom in the component program C.
483 // 2. For each atom ai in atom set occurring in a proper disjunction, [hp(ai) <=> tp(ai), ~up(ai)], where
484 // tp(ai), hp(ai), up(ai) are the input, aux, and output atoms in C.
addAtomConstraints(SharedContext & comp)485 void PrgDepGraph::NonHcfComponent::ComponentMap::addAtomConstraints(SharedContext& comp) {
486 ClauseCreator cc1(comp.master()), cc2(comp.master());
487 cc1.addDefaultFlags(ClauseCreator::clause_force_simplify);
488 cc1.start();
489 for (MapRange r = atoms(); r.first != r.second; ++r.first) {
490 const Mapping& m = *r.first;
491 cc1.add(m.up());
492 if (m.disj()) {
493 cc2.start().add(~m.tp()).add(m.up()).add(m.hp()).end(); // [~tp v up v hp]
494 cc2.start().add(~m.hp()).add(m.tp()).end(); // [~hp v tp]
495 cc2.start().add(~m.hp()).add(~m.up()).end(); // [~hp v ~up]
496 }
497 }
498 cc1.end();
499 }
500
501 // Adds constraints stemming from the given bodies to the component program.
502 // For each atom ai and rule a0 | ai | ...| an :- B, s.th. B in bodies
503 // [~up(ai) v fb(B) V hp(aj), j != i V up(p), p in B+ ^ C], where
504 // hp(ai), up(ai) are the aux and output atoms of ai in C.
addBodyConstraints(const Solver & generator,const SccGraph & dep,uint32 scc,SharedContext & comp)505 void PrgDepGraph::NonHcfComponent::ComponentMap::addBodyConstraints(const Solver& generator, const SccGraph& dep, uint32 scc, SharedContext& comp) {
506 ClauseCreator cc(comp.master());
507 cc.addDefaultFlags(ClauseCreator::clause_force_simplify);
508 ClauseCreator dc(comp.master());
509 MapIt j = mapping.begin() + numAtoms;
510 for (MapRange r = bodies(); r.first != r.second; ++r.first) {
511 const BodyNode& B = dep.getBody(r.first->node);
512 if (generator.isFalse(B.lit)) { continue; }
513 POTASSCO_REQUIRE(!B.extended(), "Extended bodies not supported - use '--trans-ext=weight'");
514 for (const NodeId* hIt = B.heads_begin(), *hEnd = B.heads_end(); hIt != hEnd; ++hIt) {
515 uint32 hScc = *hIt ? dep.getAtom(*hIt).scc : dep.getAtom(hIt[1]).scc;
516 if (hScc != scc) {
517 // the head is not relevant to this non-hcf - skip it
518 if (!*hIt) { do { ++hIt; } while (*hIt); }
519 continue;
520 }
521 // [fb(B) v ~up(a) V hp(o) for all o != a in B.disHead V up(b) for each b in B+ ^ C]
522 cc.start().add(r.first->fb());
523 if (B.scc == scc) { // add subgoals from same scc
524 for (const NodeId* aIt = B.preds(); *aIt != idMax; ++aIt) {
525 MapIt_c atMapped = findAtom(*aIt);
526 cc.add(atMapped->up());
527 }
528 }
529 if (*hIt) { // normal head
530 MapIt_c atMapped = findAtom(*hIt);
531 assert(atMapped != atoms().second);
532 cc.add(~atMapped->up());
533 cc.end();
534 }
535 else { // disjunctive head
536 const NodeId* dHead = ++hIt;
537 for (; *hIt; ++hIt) {
538 dc.start();
539 dc = cc;
540 MapIt_c atMapped = findAtom(*hIt);
541 dc.add(~atMapped->up());
542 for (const NodeId* other = dHead; *other; ++other) {
543 if (*other != *hIt) {
544 assert(dep.getAtom(*other).scc == scc);
545 atMapped = findAtom(*other);
546 dc.add(atMapped->hp());
547 }
548 }
549 dc.end();
550 }
551 }
552 }
553 if (!r.first->eq()) { *j++ = *r.first; }
554 }
555 mapping.erase(j, mapping.end());
556 }
557
558 // Maps the generator assignment given in s to a list of tester assumptions.
mapGeneratorAssignment(const Solver & s,const SccGraph & dep,LitVec & assume) const559 void PrgDepGraph::NonHcfComponent::ComponentMap::mapGeneratorAssignment(const Solver& s, const SccGraph& dep, LitVec& assume) const {
560 Literal gen;
561 assume.clear(); assume.reserve(mapping.size());
562 for (MapRange r = atoms(); r.first != r.second; ++r.first) {
563 const Mapping& at = *r.first;
564 gen = dep.getAtom(at.node).lit;
565 if (at.hasTp()) {
566 assume.push_back(at.tp() ^ (!s.isTrue(gen)));
567 }
568 if (s.isFalse(gen)) { assume.push_back(~at.up()); }
569 }
570 for (MapRange r = bodies(); r.first != r.second; ++r.first) {
571 gen = dep.getBody(r.first->node).lit;
572 assume.push_back(r.first->fb() ^ (!s.isFalse(gen)));
573 }
574 }
575 // Maps the tester model given in s back to a list of unfounded atoms in the generator.
mapTesterModel(const Solver & s,VarVec & out) const576 void PrgDepGraph::NonHcfComponent::ComponentMap::mapTesterModel(const Solver& s, VarVec& out) const {
577 assert(s.numFreeVars() == 0);
578 out.clear();
579 for (MapRange r = atoms(); r.first != r.second; ++r.first) {
580 if (s.isTrue(r.first->up())) {
581 out.push_back(r.first->node);
582 }
583 }
584 }
simplify(const Solver & generator,const SccGraph & dep,Solver & tester)585 bool PrgDepGraph::NonHcfComponent::ComponentMap::simplify(const Solver& generator, const SccGraph& dep, Solver& tester) {
586 if (!tester.popRootLevel(UINT32_MAX)) { return false; }
587 if (tester.sharedContext()->isShared() && (tester.sharedContext()->allowImplicit(Constraint_t::Conflict) || tester.sharedContext()->distributor.get())) {
588 // Simplification not safe: top-level assignments of threads are
589 // not necessarily synchronised at this point and clauses simplified
590 // with top-level assignment of this thread might not (yet) be valid
591 // wrt possible assumptions in other threads.
592 return true;
593 }
594 const bool rem = !tester.sharedContext()->isShared();
595 MapIt j = rem ? mapping.begin() : mapping.end();
596 for (MapIt_c it = mapping.begin(), aEnd = it + numAtoms, end = mapping.end(); it != end; ++it) {
597 const Mapping& m = *it;
598 const bool atom = it < aEnd;
599 Literal g = atom ? dep.getAtom(m.node).lit : dep.getBody(m.node).lit;
600 if (generator.topValue(g.var()) == value_free) {
601 if (rem) { *j++ = m; }
602 continue;
603 }
604 bool isFalse = generator.isFalse(g);
605 bool ok = atom || tester.force(isFalse ? m.fb() : ~m.fb());
606 if (atom) {
607 if (!isFalse){ ok = !m.hasTp() || tester.force(m.tp()); if (rem) { *j++ = m; } }
608 else { ok = tester.force(~m.up()) && (!m.hasTp() || tester.force(~m.tp())); numAtoms -= (ok && rem); }
609 }
610 if (!ok) {
611 if (rem) { j = std::copy(it, end, j); }
612 break;
613 }
614 }
615 mapping.erase(j, mapping.end());
616 return tester.simplify();
617 }
618 /////////////////////////////////////////////////////////////////////////////////////////
619 // class PrgDepGraph::NonHcfComponent
620 /////////////////////////////////////////////////////////////////////////////////////////
NonHcfComponent(uint32 id,const PrgDepGraph & dep,SharedContext & genCtx,Configuration * c,uint32 scc,const VarVec & atoms,const VarVec & bodies)621 PrgDepGraph::NonHcfComponent::NonHcfComponent(uint32 id, const PrgDepGraph& dep, SharedContext& genCtx, Configuration* c, uint32 scc, const VarVec& atoms, const VarVec& bodies)
622 : dep_(&dep)
623 , prg_(new SharedContext())
624 , comp_(new ComponentMap())
625 , id_(id)
626 , scc_(scc) {
627 Solver& generator = *genCtx.master();
628 prg_->setConcurrency(genCtx.concurrency(), SharedContext::resize_reserve);
629 prg_->setConfiguration(c, Ownership_t::Retain);
630 comp_->addVars(generator, dep, atoms, bodies, *prg_);
631 prg_->startAddConstraints();
632 comp_->addAtomConstraints(*prg_);
633 comp_->addBodyConstraints(generator, dep, scc, *prg_);
634 prg_->endInit(true);
635 }
636
~NonHcfComponent()637 PrgDepGraph::NonHcfComponent::~NonHcfComponent() {
638 delete prg_;
639 delete comp_;
640 }
641
update(const SharedContext & generator)642 void PrgDepGraph::NonHcfComponent::update(const SharedContext& generator) {
643 for (uint32 i = 0; generator.hasSolver(i); ++i) {
644 if (!prg_->hasSolver(i)) { prg_->attach(prg_->pushSolver()); }
645 else { prg_->initStats(*prg_->solver(i)); }
646 }
647 }
648
assumptionsFromAssignment(const Solver & s,LitVec & assume) const649 void PrgDepGraph::NonHcfComponent::assumptionsFromAssignment(const Solver& s, LitVec& assume) const {
650 comp_->mapGeneratorAssignment(s, *dep_, assume);
651 }
652
test(const Solver & generator,const LitVec & assume,VarVec & unfoundedOut) const653 bool PrgDepGraph::NonHcfComponent::test(const Solver& generator, const LitVec& assume, VarVec& unfoundedOut) const {
654 assert(generator.id() < prg_->concurrency() && "Invalid id!");
655 // Forwards to message handler of generator so that messages are
656 // handled during long running tests.
657 struct Tester : MessageHandler {
658 Tester(Solver& s, MessageHandler* gen) : solver(&s), generator(gen) { if (gen) { s.addPost(this); } }
659 ~Tester() { if (generator) { solver->removePost(this); } }
660 bool handleMessages() { return generator->handleMessages(); }
661 bool propagateFixpoint(Solver&, PostPropagator*) { return Tester::handleMessages() || !terminate(); }
662 bool terminate() { solver->setStopConflict(); return true; }
663 int test(const LitVec& assume) {
664 return int(BasicSolve(*solver).satisfiable(assume, solver->stats.choices == 0) == false);
665 }
666 Solver* solver;
667 MessageHandler* generator;
668 } tester(*prg_->solver(generator.id()), static_cast<MessageHandler*>(generator.getPost(PostPropagator::priority_reserved_msg)));
669 SolveTestEvent ev(*tester.solver, id_, generator.numFreeVars() != 0);
670 tester.solver->stats.addTest(ev.partial);
671 generator.sharedContext()->report(ev);
672 ev.time = ThreadTime::getTime();
673 if ((ev.result = tester.test(assume)) == 0) {
674 tester.solver->stats.addModel(tester.solver->decisionLevel());
675 comp_->mapTesterModel(*tester.solver, unfoundedOut);
676 }
677 ev.time = ThreadTime::getTime() - ev.time;
678 tester.solver->stats.addCpuTime(ev.time);
679 generator.sharedContext()->report(ev);
680 return ev.result != 0;
681 }
simplify(const Solver & s) const682 bool PrgDepGraph::NonHcfComponent::simplify(const Solver& s) const {
683 return comp_->simplify(s, *dep_, *prg_->solver(s.id()));
684 }
685 /////////////////////////////////////////////////////////////////////////////////////////
686 // class PrgDepGraph::NonHcfStats
687 /////////////////////////////////////////////////////////////////////////////////////////
688 struct PrgDepGraph::NonHcfStats::Data {
689 typedef StatsVec<ProblemStats> ProblemVec;
690 typedef StatsVec<SolverStats> SolverVec;
691 struct ComponentStats {
692 ProblemVec problem;
693 SolverVec solvers;
694 SolverVec accu;
695 };
DataClasp::Asp::PrgDepGraph::NonHcfStats::Data696 Data(uint32 level, bool inc) : components(level > 1 ? new ComponentStats : 0) {
697 if (inc) { solvers.multi = new SolverStats(); }
698 }
~DataClasp::Asp::PrgDepGraph::NonHcfStats::Data699 ~Data() { delete components; delete solvers.multi; }
addHccClasp::Asp::PrgDepGraph::NonHcfStats::Data700 void addHcc(const NonHcfComponent& c) {
701 assert(components);
702 ProblemVec& hcc = components->problem;
703 SolverVec& solver = components->solvers;
704 SolverVec* accu = solvers.multi ? &components->accu : 0;
705 uint32 id = c.id();
706 if (id >= hcc.size()) {
707 hcc.growTo(id + 1);
708 solver.growTo(id + 1);
709 if (accu) { accu->growTo(id + 1); }
710 }
711 if (!hcc[id]) {
712 hcc[id] = new ProblemStats(c.ctx().stats());
713 solver[id] = new SolverStats();
714 if (accu) { (*accu)[id] = new SolverStats(); solver[id]->multi = (*accu)[id]; }
715 }
716 }
updateHccClasp::Asp::PrgDepGraph::NonHcfStats::Data717 void updateHcc(const NonHcfComponent& c) {
718 c.ctx().accuStats(solvers);
719 if (components && c.id() < components->solvers.size()) {
720 POTASSCO_REQUIRE(components->solvers[c.id()], "component not added to stats!");
721 c.ctx().accuStats(*components->solvers[c.id()]);
722 components->solvers[c.id()]->flush();
723 }
724 }
725 ProblemStats hccs;
726 SolverStats solvers;
727 ComponentStats* components;
728 };
NonHcfStats(PrgDepGraph & g,uint32 l,bool inc)729 PrgDepGraph::NonHcfStats::NonHcfStats(PrgDepGraph& g, uint32 l, bool inc) : graph_(&g), data_(new Data(l, inc)) {
730 for (NonHcfIter it = g.nonHcfBegin(), end = g.nonHcfEnd(); it != end; ++it) {
731 addHcc(**it);
732 }
733 }
~NonHcfStats()734 PrgDepGraph::NonHcfStats::~NonHcfStats() { delete data_; }
accept(StatsVisitor & out,bool final) const735 void PrgDepGraph::NonHcfStats::accept(StatsVisitor& out, bool final) const {
736 if (!data_->solvers.multi) { final = false; }
737 out.visitProblemStats(data_->hccs);
738 out.visitSolverStats(final ? *data_->solvers.multi : data_->solvers);
739 if (data_->components && out.visitHccs(StatsVisitor::Enter)) {
740 const Data::SolverVec& solver = final ? data_->components->accu : data_->components->solvers;
741 const Data::ProblemVec& hcc = data_->components->problem;
742 for (uint32 i = 0, end = sizeVec(hcc); i != end; ++i) {
743 out.visitHcc(i, *hcc[i], *solver[i]);
744 }
745 out.visitHccs(StatsVisitor::Leave);
746 }
747 }
startStep(uint32 statsLevel)748 void PrgDepGraph::NonHcfStats::startStep(uint32 statsLevel) {
749 data_->solvers.reset();
750 if (data_->components) { data_->components->solvers.reset(); }
751 if (statsLevel > 1 && !data_->components) {
752 data_->components = new Data::ComponentStats();
753 for (NonHcfIter it = graph_->nonHcfBegin(), end = graph_->nonHcfEnd(); it != end; ++it) {
754 data_->addHcc(**it);
755 }
756 }
757 }
endStep()758 void PrgDepGraph::NonHcfStats::endStep() {
759 for (NonHcfIter it = graph_->nonHcfBegin(), end = graph_->nonHcfEnd(); it != end; ++it) {
760 data_->updateHcc(**it);
761 }
762 data_->solvers.flush();
763 }
addHcc(const NonHcfComponent & c)764 void PrgDepGraph::NonHcfStats::addHcc(const NonHcfComponent& c) {
765 data_->hccs.accu(c.ctx().stats());
766 if (data_->components) { data_->addHcc(c); }
767 }
removeHcc(const NonHcfComponent & c)768 void PrgDepGraph::NonHcfStats::removeHcc(const NonHcfComponent& c) {
769 data_->updateHcc(c);
770 }
addTo(StatsMap & problem,StatsMap & solving,StatsMap * accu) const771 void PrgDepGraph::NonHcfStats::addTo(StatsMap& problem, StatsMap& solving, StatsMap* accu) const {
772 data_->solvers.addTo("hccs", solving, accu);
773 problem.add("hccs", StatisticObject::map(&data_->hccs));
774 if (data_->components) {
775 problem.add("hcc", data_->components->problem.toStats());
776 solving.add("hcc", data_->components->solvers.toStats());
777 if (accu) { accu->add("hcc", data_->components->accu.toStats()); }
778 }
779 }
780 } // namespace Asp
781 /////////////////////////////////////////////////////////////////////////////////////////
782 // class ExtDepGraph
783 /////////////////////////////////////////////////////////////////////////////////////////
ExtDepGraph(uint32)784 ExtDepGraph::ExtDepGraph(uint32) : maxNode_(0), comEdge_(0), genCnt_(0) {}
~ExtDepGraph()785 ExtDepGraph::~ExtDepGraph(){}
addEdge(Literal lit,uint32 startNode,uint32 endNode)786 void ExtDepGraph::addEdge(Literal lit, uint32 startNode, uint32 endNode) {
787 POTASSCO_REQUIRE(!frozen(), "ExtDepGraph::update() not called!");
788 fwdArcs_.push_back(Arc::create(lit, startNode, endNode));
789 maxNode_ = std::max(std::max(startNode, endNode)+uint32(1), maxNode_);
790 if (comEdge_ && std::min(startNode, endNode) < nodes_.size()) {
791 invArcs_.clear();
792 comEdge_ = 0;
793 ++genCnt_;
794 }
795 }
frozen() const796 bool ExtDepGraph::frozen() const {
797 return !fwdArcs_.empty() && fwdArcs_.back().tail() == UINT32_MAX;
798 }
update()799 void ExtDepGraph::update() {
800 if (frozen()) {
801 fwdArcs_.pop_back();
802 }
803 }
finalize(SharedContext & ctx)804 uint32 ExtDepGraph::finalize(SharedContext& ctx) {
805 if (frozen()) {
806 return comEdge_;
807 }
808 // sort by end node
809 std::sort(fwdArcs_.begin() + comEdge_, fwdArcs_.end(), CmpArc<1>());
810 invArcs_.reserve(fwdArcs_.size());
811 Node sent = { UINT32_MAX, UINT32_MAX };
812 nodes_.resize(maxNode_, sent);
813 for (ArcVec::const_iterator it = fwdArcs_.begin() + comEdge_, end = fwdArcs_.end(); it != end;) {
814 uint32 node = it->head();
815 POTASSCO_REQUIRE(!comEdge_ || nodes_[node].invOff == UINT32_MAX, "ExtDepGraph: invalid incremental update!");
816 Inv inv;
817 nodes_[node].invOff = (uint32)invArcs_.size();
818 do {
819 inv.lit = it->lit;
820 inv.rep = static_cast<uint32>(it->tail() << 1) | 1u;
821 invArcs_.push_back(inv);
822 ctx.setFrozen(it->lit.var(), true);
823 } while (++it != end && it->head() == node);
824 invArcs_.back().rep ^= 1u;
825 }
826 // sort by start node
827 std::sort(fwdArcs_.begin() + comEdge_, fwdArcs_.end(), CmpArc<0>());
828 for (ArcVec::const_iterator it = fwdArcs_.begin() + comEdge_, end = fwdArcs_.end(); it != end;) {
829 uint32 node = it->tail();
830 POTASSCO_REQUIRE(!comEdge_ || nodes_[node].fwdOff == UINT32_MAX, "ExtDepGraph: invalid incremental update!");
831 nodes_[node].fwdOff = static_cast<uint32>(it - fwdArcs_.begin());
832 it = std::lower_bound(it, end, node + 1, CmpArc<0>());
833 }
834 comEdge_ = (uint32)fwdArcs_.size();
835 fwdArcs_.push_back(Arc::create(lit_false(), UINT32_MAX, UINT32_MAX));
836 return comEdge_;
837 }
attach(Solver & s,Constraint & p,uint64 genId)838 uint64 ExtDepGraph::attach(Solver& s, Constraint& p, uint64 genId) {
839 uint32 count = static_cast<uint32>(genId >> 32);
840 uint32 edges = static_cast<uint32>(genId);
841 uint32 update= count == genCnt_ ? 0 : edges;
842 GenericWatch* w;
843 for (uint32 i = (count == genCnt_ ? edges : 0), eId, end = comEdge_; i < end; ++i) {
844 const Arc& a = fwdArcs_[i];
845 if (a.head() != a.tail()) {
846 if (s.topValue(a.lit.var()) == value_free) {
847 if (!update || (w = s.getWatch(a.lit, &p)) == 0) {
848 s.addWatch(a.lit, &p, i);
849 }
850 else {
851 w->data = i;
852 --update;
853 }
854 }
855 else if (s.isTrue(a.lit)) {
856 p.propagate(s, a.lit, (eId = i));
857 }
858 }
859 else if (!s.force(~a.lit)) {
860 break;
861 }
862 }
863 return (static_cast<uint64>(genCnt_) << 32) | comEdge_;
864 }
detach(Solver * s,Constraint & p)865 void ExtDepGraph::detach(Solver* s, Constraint& p) {
866 if (s) {
867 for (ArcVec::size_type i = fwdArcs_.size(); i--; ) {
868 s->removeWatch(fwdArcs_[i].lit, &p);
869 }
870 }
871 }
872 /////////////////////////////////////////////////////////////////////////////////////////
873 // class AcyclicityCheck
874 /////////////////////////////////////////////////////////////////////////////////////////
875 struct AcyclicityCheck::ReasonStore {
876 typedef PodVector<LitVec*>::type NogoodMap;
877 NogoodMap db;
getReasonClasp::AcyclicityCheck::ReasonStore878 void getReason(Literal p, LitVec& out) {
879 if (const LitVec* r = db[p.var()]) {
880 out.insert(out.end(), r->begin(), r->end());
881 }
882 }
setReasonClasp::AcyclicityCheck::ReasonStore883 void setReason(Literal p, LitVec::const_iterator first, LitVec::const_iterator end) {
884 Var v = p.var();
885 if (v >= db.size()) { db.resize(v+1, 0); }
886 if (db[v] == 0) { db[v] = new LitVec(first, end); }
887 else { db[v]->assign(first, end); }
888 }
~ReasonStoreClasp::AcyclicityCheck::ReasonStore889 ~ReasonStore() {
890 std::for_each(db.begin(), db.end(), DeleteObject());
891 }
892 };
AcyclicityCheck(DependencyGraph * graph)893 AcyclicityCheck::AcyclicityCheck(DependencyGraph* graph) : graph_(graph), solver_(0), nogoods_(0), strat_(bit_mask<uint32>(config_bit)), tagCnt_(0), genId_(0) {
894 }
~AcyclicityCheck()895 AcyclicityCheck::~AcyclicityCheck() {
896 delete nogoods_;
897 }
898
setStrategy(Strategy p)899 void AcyclicityCheck::setStrategy(Strategy p) {
900 strat_ = p;
901 }
setStrategy(const SolverParams & p)902 void AcyclicityCheck::setStrategy(const SolverParams& p) {
903 if (p.acycFwd) { setStrategy(prop_fwd); }
904 else { setStrategy(p.loopRep == LoopReason_t::Implicit ? prop_full_imp : prop_full); }
905 store_set_bit(strat_, config_bit);
906 }
907
init(Solver & s)908 bool AcyclicityCheck::init(Solver& s) {
909 if (!graph_) { graph_ = s.sharedContext()->extGraph.get(); }
910 if (!graph_) { return true; }
911 if (test_bit(strat_, config_bit)) {
912 setStrategy(s.sharedContext()->configuration()->solver(s.id()));
913 }
914 tags_.assign(graph_->nodes(), tagCnt_ = 0);
915 parent_.resize(graph_->nodes());
916 todo_.clear();
917 solver_ = &s;
918 genId_ = graph_->attach(s, *this, genId_);
919 return true;
920 }
921
startSearch()922 uint32 AcyclicityCheck::startSearch() {
923 if (++tagCnt_ != 0) { return tagCnt_; }
924 const uint32 last = tagCnt_ - 1;
925 for (Var v = 0; v != tags_.size(); ++v) {
926 tags_[v] = tags_[v] == last;
927 }
928 return tagCnt_ = 2;
929 }
setReason(Literal p,LitVec::const_iterator first,LitVec::const_iterator end)930 void AcyclicityCheck::setReason(Literal p, LitVec::const_iterator first, LitVec::const_iterator end) {
931 if (!nogoods_) { nogoods_ = new ReasonStore(); }
932 nogoods_->setReason(p, first, end);
933 }
addClauseLit(Solver & s,Literal p)934 void AcyclicityCheck::addClauseLit(Solver& s, Literal p) {
935 assert(s.isFalse(p));
936 uint32 dl = s.level(p.var());
937 if (dl && !s.seen(p)) {
938 s.markSeen(p);
939 s.markLevel(dl);
940 reason_.push_back(p);
941 }
942 }
943
reset()944 void AcyclicityCheck::reset() {
945 todo_.clear();
946 reason_.clear();
947 }
948
valid(Solver & s)949 bool AcyclicityCheck::valid(Solver& s) {
950 if (todo_.empty()) { return true; }
951 return AcyclicityCheck::propagateFixpoint(s, 0);
952 }
isModel(Solver & s)953 bool AcyclicityCheck::isModel(Solver& s) {
954 return AcyclicityCheck::valid(s);
955 }
956
destroy(Solver * s,bool detach)957 void AcyclicityCheck::destroy(Solver* s, bool detach) {
958 if (s && detach) {
959 s->removePost(this);
960 }
961 if (graph_) {
962 graph_->detach(detach ? s : 0, *this);
963 }
964 PostPropagator::destroy(s, detach);
965 }
reason(Solver &,Literal p,LitVec & out)966 void AcyclicityCheck::reason(Solver&, Literal p, LitVec& out) {
967 if (!reason_.empty() && reason_[0] == p) {
968 out.insert(out.end(), reason_.begin()+1, reason_.end());
969 }
970 else if (nogoods_) {
971 nogoods_->getReason(p, out);
972 }
973 }
974
propagateFixpoint(Solver & s,PostPropagator *)975 bool AcyclicityCheck::propagateFixpoint(Solver& s, PostPropagator*) {
976 for (Arc x; !todo_.empty();) {
977 x = todo_.pop_ret();
978 if (!dfsForward(s, x) || (strategy() != prop_fwd && !dfsBackward(s, x))) {
979 return false;
980 }
981 }
982 todo_.clear();
983 return true;
984 }
dfsForward(Solver & s,const Arc & root)985 bool AcyclicityCheck::dfsForward(Solver& s, const Arc& root) {
986 const uint32 tag = startSearch();
987 nStack_.clear();
988 pushVisit(root.head(), tag);
989 for (Var node, nodeNext; !nStack_.empty();) {
990 node = nStack_.back();
991 nStack_.pop_back();
992 for (const Arc* a = graph_->fwdBegin(node); a; a = graph_->fwdNext(a)) {
993 if (s.isTrue(a->lit)) {
994 nodeNext = a->head();
995 if (nodeNext == root.tail()) {
996 setParent(nodeNext, Parent::create(a->lit, node));
997 reason_.assign(1, ~root.lit);
998 for (Var n0 = nodeNext; n0 != root.head();) {
999 Parent parent = parent_[n0];
1000 assert(s.isTrue(parent.lit));
1001 reason_.push_back(parent.lit);
1002 n0 = parent.node;
1003 }
1004 return s.force(~root.lit, this);
1005 }
1006 else if (!visited(nodeNext, tag)) {
1007 setParent(nodeNext, Parent::create(a->lit, node));
1008 pushVisit(nodeNext, tag);
1009 }
1010 }
1011 }
1012 }
1013 return true;
1014 }
dfsBackward(Solver & s,const Arc & root)1015 bool AcyclicityCheck::dfsBackward(Solver& s, const Arc& root) {
1016 const uint32 tag = startSearch();
1017 const uint32 fwd = tag - 1;
1018 nStack_.clear();
1019 pushVisit(root.tail(), tag);
1020 for (Var node, nodeNext; !nStack_.empty(); ) {
1021 node = nStack_.back();
1022 nStack_.pop_back();
1023 for (const Inv* a = graph_->invBegin(node); a; a = graph_->invNext(a)) {
1024 ValueRep val = s.value(a->lit.var());
1025 if (val == falseValue(a->lit) || visited(nodeNext = a->tail(), tag)) { continue; }
1026 if (visited(nodeNext, fwd)) { // a->lit would complete a cycle - force to false
1027 assert(val == value_free || s.level(a->lit.var()) == s.decisionLevel());
1028 reason_.assign(1, ~a->lit);
1029 addClauseLit(s, ~root.lit);
1030 for (Var n = nodeNext; n != root.head(); ) {
1031 Parent parent = parent_[n];
1032 assert(s.isTrue(parent.lit) && visited(parent.node, fwd));
1033 addClauseLit(s, ~parent.lit);
1034 n = parent.node;
1035 }
1036 for (Var n = node; n != root.tail(); ) {
1037 Parent parent = parent_[n];
1038 assert(s.isTrue(parent.lit)&& visited(parent.node, tag));
1039 addClauseLit(s, ~parent.lit);
1040 n = parent.node;
1041 }
1042 if (val == value_free && strategy() == prop_full) {
1043 ConstraintInfo info(Constraint_t::Loop);
1044 s.finalizeConflictClause(reason_, info, 0);
1045 ClauseCreator::create(s, reason_, ClauseCreator::clause_no_prepare, info);
1046 }
1047 else {
1048 for (uint32 i = 1; i != reason_.size(); ++i) {
1049 s.clearSeen(reason_[i].var());
1050 reason_[i] = ~reason_[i];
1051 }
1052 if (!s.force(~a->lit, this)) { return false; }
1053 setReason(~a->lit, reason_.begin()+1, reason_.end());
1054 }
1055 assert(s.isFalse(a->lit));
1056 if (!s.propagateUntil(this)) { return false; }
1057 }
1058 else if (val != value_free) { // follow true edge backward
1059 setParent(nodeNext, Parent::create(a->lit, node));
1060 pushVisit(nodeNext, tag);
1061 }
1062 }
1063 }
1064 return true;
1065 }
1066 }
1067
1068