← Back to branch summary

~ubuntu-branches/ubuntu/wily/clasp/wily

« back to all changes in this revision

Viewing changes to libclasp/src/logic_program.cpp

  • Committer: Package Import Robot
  • Author(s): Thomas Krennwallner
  • Date: 2015-05-12 07:18:25 UTC
  • mfrom: (20.1.12 sid)
  • Revision ID: package-import@ubuntu.com-20150512071825-vlgtxbw5245d6wni
Tags: 3.1.2-1
* Imported Upstream version 3.1.2
* Fix dep5-copyright-license-name-not-unique and
  missing-license-paragraph-in-dep5-copyright lintian warnings.

Show diffs side-by-side

added added

removed removed

Lines of Context:
libclasp/src/logic_program.cpp
139
139
        DisjList().swap(disjunctions_);
140
140
        bodyIndex_.clear();
141
141
        disjIndex_.clear();
142
 
        MinimizeRule* r = minimize_;
143
 
        while (r) {
144
 
                MinimizeRule* t = r;
 
142
        for (MinimizeRule* r = minimize_, *t; r; ) {
 
143
                t = r;
145
144
                r = r->next_;
146
145
                delete t;
147
146
        }
161
160
                stats.reset();
162
161
                startAux_ = atoms_.size();
163
162
        }
 
163
        else {
 
164
                // make sure that we have a reference to any minimize constraint
 
165
                getMinimizeConstraint();
 
166
        }
164
167
        activeHead_.clear();
165
168
        activeBody_.reset();
166
169
}
229
232
                                support->addHead(a, PrgEdge::CHOICE_EDGE);
230
233
                        }
231
234
                }
232
 
                else if (!a->eq() && a->value() == value_false) {
 
235
                else if (a->removed() || (!a->eq() && a->value() == value_false)) {
233
236
                        a->setEq(getFalseId());
234
 
                } 
 
237
                }
235
238
        }
236
239
        // delete any introduced aux atoms
237
240
        // this is safe because aux atoms are never part of the input program
324
327
                        else {
325
328
                                activeHead_.clear();
326
329
                                for (PrgBody::head_iterator hIt = b->heads_begin(); hIt != b->heads_end(); ++hIt) {
327
 
                                        if (!getHead(*hIt)->hasVar()) { continue; }
 
330
                                        if (!getHead(*hIt)->hasVar() || hIt->isGamma()) { continue; }
328
331
                                        if (hIt->isAtom()) {
329
332
                                                if      (hIt->isNormal()) { os << activeBody_.ruleType() << " " << hIt->node() << " " << activeBody_ << "\n"; }
330
333
                                                else if (hIt->isChoice()) { activeHead_.push_back(hIt->node()); }
353
356
        for (AtomList::size_type i = 1; i < atoms_.size(); ++i) {
354
357
                // write the equivalent atoms
355
358
                if (atoms_[i]->eq()) {
356
 
                        os << "1 " << i << " 1 0 " << getEqAtom(Var(i)) << " \n";
 
359
                        PrgAtom* eq = getAtom(getEqAtom(Var(i)));
 
360
                        if (eq->inUpper() && eq->value() != value_false) {
 
361
                                os << "1 " << i << " 1 0 " << getEqAtom(Var(i)) << " \n";
 
362
                        }
357
363
                }
358
364
                if ( (i == falseAtom || atoms_[i]->inUpper()) && atoms_[i]->value() != value_free ) {
359
365
                        std::stringstream& str = atoms_[i]->value() == value_false ? bm : bp;
737
743
        setFrozen(false);
738
744
        uint32 shifted = 0, added = 0;
739
745
        stats.nonHcfs  = uint32(nonHcfs_.size());
 
746
        Literal bot    = negLit(0);
740
747
        for (uint32 id = 0, maxId = disj.size(); id != maxId; ++id) {
741
748
                PrgDisj* d = disj[id];
742
 
                Literal dx = d->inUpper() ? d->literal() : negLit(0);
 
749
                Literal dx = d->inUpper() ? d->literal() : bot;
743
750
                PrgEdge e  = PrgEdge::newEdge(id, PrgEdge::CHOICE_EDGE, PrgEdge::DISJ_NODE);
744
751
                d->resetId(id, true); // id changed during scc checking
745
752
                // remove from program and 
746
753
                // replace with shifted rules or component-shifted disjunction
747
754
                head.clear(); supports.clear();
748
755
                for (PrgDisj::atom_iterator it = d->begin(), end = d->end(); it != end; ++it) {
749
 
                        PrgAtom* at = getAtom(it->node());
 
756
                        uint32  aId = it->node();
 
757
                        PrgAtom* at = getAtom(aId);
750
758
                        at->removeSupport(e);
751
 
                        if (at->inUpper()) { 
752
 
                                head.push_back(it->node()); 
753
 
                                if (at->scc() != PrgNode::noScc) { sccMap[at->scc()] = seen_scc; }
 
759
                        if (dx == bot) { continue; }
 
760
                        if (at->eq())  { 
 
761
                                at = getAtom(aId = getEqAtom(aId));
 
762
                        }
 
763
                        if (at->inUpper()) {
 
764
                                head.push_back(aId); 
 
765
                                if (at->scc() != PrgNode::noScc){ sccMap[at->scc()] = seen_scc; }
754
766
                        }
755
767
                }
756
768
                EdgeVec temp;
762
774
                }
763
775
                d->destroy();
764
776
                // create shortcut for supports to avoid duplications during shifting
765
 
                Literal supportLit = dx != negLit(0) ? getEqAtomLit(dx, supports, p, sccMap) : dx;
 
777
                Literal supportLit = dx != bot ? getEqAtomLit(dx, supports, p, sccMap) : dx;
766
778
                // create shifted rules and split disjunctions into non-hcf components
767
779
                for (VarVec::iterator hIt = head.begin(), hEnd = head.end(); hIt != hEnd; ++hIt) {
768
780
                        uint32 scc = getAtom(*hIt)->scc();
805
817
                                                for (uint32 i = x->size();;) {
806
818
                                                        t = simplifyRule(rule_, activeHead_, activeBody_);
807
819
                                                        B = t != ENDRULE ? assignBodyFor(activeBody_, PrgEdge::GAMMA_EDGE, true) : 0;
808
 
                                                        if (B && B->value() != value_false) { B->addHead(getAtom(activeHead_[0]), PrgEdge::GAMMA_EDGE); ++stats.gammas; }
 
820
                                                        if (B && B->value() != value_false && !B->hasHead(getAtom(activeHead_[0]), PrgEdge::NORMAL_EDGE)) {
 
821
                                                                B->addHead(getAtom(activeHead_[0]), PrgEdge::GAMMA_EDGE);
 
822
                                                                ++stats.gammas;
 
823
                                                        }
809
824
                                                        if (--i == 0) { break; }
810
825
                                                        Var h          = rule_.heads[0];
811
826
                                                        rule_.heads[0] = (--bIt)->first.var();
942
957
        // add atoms from this step and finalize symbol table
943
958
        typedef SymbolTable::const_iterator symbol_iterator;
944
959
        const bool freezeAll   = incData_ && ctx()->satPrepro.get() != 0;
 
960
        const bool freezeShown = options().freezeShown;
945
961
        symbol_iterator sym    = ctx()->symbolTable().lower_bound(ctx()->symbolTable().curBegin(), startAtom());
946
962
        symbol_iterator symEnd = ctx()->symbolTable().end();
947
963
        Var             atomId = startAtom();
950
966
                if (freezeAll && (*it)->hasVar())  { ctx()->setFrozen((*it)->var(), true); }
951
967
                if (sym != symEnd && atomId == sym->first) {
952
968
                        sym->second.lit = atoms_[getEqAtom(atomId)]->literal();
 
969
                        if (freezeShown) { ctx()->setFrozen(sym->second.lit.var(), true); }
953
970
                        ++sym;
954
971
                }
955
972
        }
1095
1112
                else if ((sumW - minW) < bound) { resType = BASICRULE;      bound = (weight_t)sBody.size(); }
1096
1113
                else if (minW == maxW)          { resType = CONSTRAINTRULE; bound = (bound+(minW-1))/minW;  }
1097
1114
        }
 
1115
        if (hasWeights(r.type()) && !hasWeights(resType) && maxW > 1 && resType != ENDRULE) {
 
1116
                for (WeightLitVec::iterator it = sBody.begin(), end = sBody.end(); it != end; ++it) {
 
1117
                        it->second = 1;
 
1118
                }
 
1119
        }
1098
1120
        info.init(resType, bound, hash, pos);
1099
1121
        return resType;
1100
1122
}
1265
1287
                LogicProgram::IndexRange eqRange = disjIndex_.equal_range(headHash);
1266
1288
                for (; eqRange.first != eqRange.second; ++eqRange.first) {
1267
1289
                        PrgDisj& o = *disjunctions_[eqRange.first->second];
1268
 
                        if (o.relevant() && o.size() == heads.size() && ruleState_.allMarked(heads, RuleState::head_flag)) {
 
1290
                        if (o.relevant() && o.size() == heads.size() && ruleState_.allMarked(o.begin(), o.end(), RuleState::head_flag)) {
1269
1291
                                assert(o.id() == eqRange.first->second);
1270
1292
                                d = &o;
1271
1293
                                break;