• 设为首页
  • 点击收藏
  • 手机版
    手机扫一扫访问
    迪恩网络手机版
  • 关注官方公众号
    微信扫一扫关注
    迪恩网络公众号

C++ XorClause类代码示例

原作者: [db:作者] 来自: [db:来源] 收藏 邀请

本文整理汇总了C++中XorClause的典型用法代码示例。如果您正苦于以下问题:C++ XorClause类的具体用法?C++ XorClause怎么用?C++ XorClause使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。



在下文中一共展示了XorClause类的5个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。

示例1: assert

inline const bool ClauseCleaner::cleanClause(XorClause& c)
{
    Lit *i, *j, *end;
    Var origVar1 = c[0].var();
    Var origVar2 = c[1].var();
    uint32_t origSize = c.size();
    for (i = j = c.getData(), end = i + c.size();  i != end; i++) {
        const lbool& val = solver.assigns[i->var()];
        if (val.isUndef()) {
            *j = *i;
            j++;
        } else c.invert(val.getBool());
    }
    c.shrink(i-j);

    assert(c.size() != 1);
    switch (c.size()) {
        case 0: {
            solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
            return true;
        }
        case 2: {
            c[0] = c[0].unsign();
            c[1] = c[1].unsign();
            solver.varReplacer->replace(c, c.xorEqualFalse(), c.getGroup());
            solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
            return true;
        }
        default: {
            if (i-j > 0) {
                solver.clauses_literals -= i-j;
            }
            return false;
        }
    }

    assert(false);
    return false;
}
开发者ID:donehl,项目名称:kodkod,代码行数:39,代码来源:ClauseCleaner.cpp


示例2: assert

void XorFinder::addXorAsNormal3(XorClause& c)
{
    assert(c.size() == 3);
    Clause *tmp;
    vec<Var> vars;
    vec<Lit> vars2(c.size());
    const bool inverted = c.xor_clause_inverted();

    for (uint32_t i = 0; i < c.size(); i++) {
        vars.push(c[i].var());
    }

    vars2[0] = Lit(vars[0], false ^ inverted);
    vars2[1] = Lit(vars[1], false ^ inverted);
    vars2[2] = Lit(vars[2], false ^ inverted);
    tmp = solver.addClauseInt(vars2, c.getGroup());
    if (tmp) solver.clauses.push(tmp);

    vars2[0] = Lit(vars[0], true ^ inverted);
    vars2[1] = Lit(vars[1], true ^ inverted);
    vars2[2] = Lit(vars[2], false ^ inverted);
    tmp = solver.addClauseInt(vars2, c.getGroup());
    if (tmp) solver.clauses.push(tmp);

    vars2[0] = Lit(vars[0], true ^ inverted);
    vars2[1] = Lit(vars[1], false ^ inverted);
    vars2[2] = Lit(vars[2], true ^ inverted);
    tmp = solver.addClauseInt(vars2, c.getGroup());
    if (tmp) solver.clauses.push(tmp);

    vars2[0] = Lit(vars[0], false ^ inverted);
    vars2[1] = Lit(vars[1], true ^ inverted);
    vars2[2] = Lit(vars[2], true ^ inverted);
    tmp = solver.addClauseInt(vars2, c.getGroup());
    if (tmp) solver.clauses.push(tmp);
}
开发者ID:AmesianX,项目名称:stp,代码行数:36,代码来源:XorFinder.cpp


示例3: replace_set

/**
@brief Helper function for replace_set()
*/
bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, const Var origVar2)
{
    uint32_t origSize = c.size();
    std::sort(c.getData(), c.getDataEnd());
    Lit p;
    uint32_t i, j;
    for (i = j = 0, p = lit_Undef; i != c.size(); i++) {
        if (c[i].var() == p.var()) {
            //added, but easily removed
            j--;
            p = lit_Undef;
            if (!solver.assigns[c[i].var()].isUndef())
                c.invert(solver.assigns[c[i].var()].getBool());
        } else if (solver.assigns[c[i].var()].isUndef()) //just add
            c[j++] = p = c[i];
        else c.invert(solver.assigns[c[i].var()].getBool()); //modify xorEqualFalse instead of adding
    }
    c.shrink(i - j);

    //Even if i==j, the clause *has* changed
    c.setChanged();

    #ifdef VERBOSE_DEBUG
    cout << "xor-clause after replacing: ";
    c.plainPrint();
    #endif

    switch (c.size()) {
    case 0:
        solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
        if (!c.xorEqualFalse()) {
            solver.ok = false;
        }
        return true;
    case 1:
        solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
        solver.uncheckedEnqueue(Lit(c[0].var(), c.xorEqualFalse()));
        solver.ok = (solver.propagate<false>().isNULL());
        return true;
    case 2: {
        solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
        c[0] = c[0].unsign() ^ c.xorEqualFalse();
        c[1] = c[1].unsign();
        addBinaryXorClause(c[0], c[1]);
        return true;
    }
    default:
        solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
        solver.attachClause(c);
        return false;
    }

    assert(false);
    return false;
}
开发者ID:audemard,项目名称:CVC4,代码行数:58,代码来源:VarReplacer.cpp


示例4: unlinkClause

const bool XorSubsumer::removeDependent()
{
    for (Var var = 0; var < occur.size(); var++) {
        if (cannot_eliminate[var] || !solver.decision_var[var] || solver.assigns[var] != l_Undef) continue;
        vec<XorClauseSimp>& occ = occur[var];

        if (occ.size() == 1) {
#ifdef VERBOSE_DEBUG
            std::cout << "Eliminating dependent var " << var + 1 << std::endl;
            std::cout << "-> Removing dependent clause ";
            occ[0].clause->plainPrint();
#endif //VERBOSE_DEBUG
            unlinkClause(occ[0], var);
            solver.setDecisionVar(var, false);
            var_elimed[var] = true;
            numElimed++;
        } else if (occ.size() == 2) {
            vec<Lit> lits;
            XorClause& c1 = *(occ[0].clause);
            lits.growTo(c1.size());
            std::copy(c1.getData(), c1.getDataEnd(), lits.getData());
            bool inverted = c1.xorEqualFalse();

            XorClause& c2 = *(occ[1].clause);
            lits.growTo(lits.size() + c2.size());
            std::copy(c2.getData(), c2.getDataEnd(), lits.getData() + c1.size());
            inverted ^= !c2.xorEqualFalse();
            uint32_t group = c2.getGroup();
            uint32_t ret = removeAll(lits, var);
            release_assert(ret == 2);

#ifdef VERBOSE_DEBUG
            std::cout << "Eliminating var " << var + 1 << " present in 2 xor-clauses" << std::endl;
            std::cout << "-> Removing xor clause ";
            occ[0].clause->plainPrint();
            std::cout << "-> Removing xor clause ";
            occ[1].clause->plainPrint();
#endif //VERBOSE_DEBUG
            XorClauseSimp toUnlink0 = occ[0];
            XorClauseSimp toUnlink1 = occ[1];
            unlinkClause(toUnlink0);
            unlinkClause(toUnlink1, var);
            solver.setDecisionVar(var, false);
            var_elimed[var] = true;
            numElimed++;

            for (uint32_t i = 0; i < lits.size(); i++)
                cannot_eliminate[lits[i].var()] = true;
            XorClause* c = solver.addXorClauseInt(lits, inverted, group);
#ifdef VERBOSE_DEBUG
            if (c != NULL) {
                std::cout << "-> Added combined xor clause:";
                c->plainPrint();
            } else
                std::cout << "-> Combined xor clause is NULL" << std::endl;
#endif
            if (c != NULL) linkInClause(*c);
            if (!solver.ok) {
#ifdef VERBOSE_DEBUG
                std::cout << "solver.ok is false after var-elim through xor" << std::endl;
#endif //VERBOSE_DEBUG
                return false;
            }
        }
    }

    return true;
}
开发者ID:yp,项目名称:reHCstar,代码行数:68,代码来源:XorSubsumer.cpp


示例5: while

bool XorFinder::findXors(uint& sumLengths)
{
    #ifdef VERBOSE_DEBUG
    cout << "Finding Xors started" << endl;
    #endif

    sumLengths = 0;

    ClauseTable::iterator begin = table.begin();
    ClauseTable::iterator end = table.begin();
    vec<Lit> lits;
    bool impair;
    while (getNextXor(begin,  end, impair)) {
        const Clause& c = *(begin->first);
        lits.clear();
        for (const Lit *it = &c[0], *cend = it+c.size() ; it != cend; it++) {
            lits.push(Lit(it->var(), false));
        }
        uint old_group = c.getGroup();

        #ifdef VERBOSE_DEBUG
        cout << "- Found clauses:" << endl;
        #endif

        for (ClauseTable::iterator it = begin; it != end; it++)
            if (impairSigns(*it->first) == impair){
            #ifdef VERBOSE_DEBUG
            it->first->plainPrint();
            #endif
            toRemove[it->second] = true;
            solver.removeClause(*it->first);
        }

        switch(lits.size()) {
        case 2: {
            solver.varReplacer->replace(lits, impair, old_group);

            #ifdef VERBOSE_DEBUG
            XorClause* x = XorClause_new(lits, impair, old_group);
            cout << "- Final 2-long xor-clause: ";
            x->plainPrint();
            clauseFree(x);
            #endif
            break;
        }
        default: {
            XorClause* x = solver.clauseAllocator.XorClause_new(lits, impair, old_group);
            solver.xorclauses.push(x);
            solver.attachClause(*x);

            #ifdef VERBOSE_DEBUG
            cout << "- Final xor-clause: ";
            x->plainPrint();
            #endif
        }
        }

        foundXors++;
        sumLengths += lits.size();
    }

    return solver.ok;
}
开发者ID:AmesianX,项目名称:stp,代码行数:63,代码来源:XorFinder.cpp



注:本文中的XorClause类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。


鲜花

握手

雷人

路过

鸡蛋
该文章已有0人参与评论

请发表评论

全部评论

专题导读
上一篇:
C++ XsByteArray类代码示例发布时间:2022-05-31
下一篇:
C++ XnSensorImageStream类代码示例发布时间:2022-05-31
热门推荐
阅读排行榜

扫描微信二维码

查看手机版网站

随时了解更新最新资讯

139-2527-9053

在线客服(服务时间 9:00~18:00)

在线QQ客服
地址:深圳市南山区西丽大学城创智工业园
电邮:jeky_zhao#qq.com
移动电话:139-2527-9053

Powered by 互联科技 X3.4© 2001-2213 极客世界.|Sitemap