首页
社区
课程
招聘
2021 KCTF 秋季赛 第四题 偶遇棋痴
发表于: 2021-11-25 11:38 21590

2021 KCTF 秋季赛 第四题 偶遇棋痴

2021-11-25 11:38
21590

学废这两篇就能做题了

// 名称可从 vptr 的 typeinfo 中看到
struct term {
    int type
    union {
        char ch;
        term *other;
    }
    term *next;
    int idx;
}
// 名称可从 vptr 的 typeinfo 中看到
struct term {
    int type
    union {
        char ch;
        term *other;
    }
    term *next;
    int idx;
}
void
parse_dump_term(const struct term * t, FILE * stream)
{
    const struct term * pterm = t;
    int nparen = 0;
 
    for (;;)
        switch (pterm->type) {
        case Tlam: {
            // CHANGE
            if (pterm->data.lam.var == 'z') {
                fprintf(stream, "[x%d]", pterm->idx);
                goto Close_paren;
            }
            fprintf(stream, "Lam (%c, ", pterm->data.lam.var);
            pterm = pterm->data.lam.body;
            nparen++;
            continue;
void
parse_dump_term(const struct term * t, FILE * stream)
{
    const struct term * pterm = t;
    int nparen = 0;
 
    for (;;)
        switch (pterm->type) {
        case Tlam: {
            // CHANGE
            if (pterm->data.lam.var == 'z') {
                fprintf(stream, "[x%d]", pterm->idx);
                goto Close_paren;
            }
            fprintf(stream, "Lam (%c, ", pterm->data.lam.var);
            pterm = pterm->data.lam.body;
            nparen++;
            continue;
template<class Archive>
void serialize(Archive& ar, term &t, const unsigned int version) {
    ar& t.type;
    switch (t.type) {
    case Tlam:
        ar& t.data.lam.var;
        ar& t.idx;
        if (t.data.lam.var != 'z') {
            ar& t.data.lam.body;
        }
        break;
    case Tapp:
        ar& t.data.app.left;
        ar& t.data.app.right;
        break;
    case Tvar:
        ar& t.data.var;
        break;
    }
}
 
term* parse_term_in(std::istream &in) {
    boost::archive::text_iarchive ar(in);
    term *ret = nullptr;
    ar >> ret;
    return ret;
}
 
term* parse_term_s(const char* s) {
    std::istringstream ss(s);
    return parse_term_in(ss);
}
template<class Archive>
void serialize(Archive& ar, term &t, const unsigned int version) {
    ar& t.type;
    switch (t.type) {
    case Tlam:
        ar& t.data.lam.var;
        ar& t.idx;
        if (t.data.lam.var != 'z') {
            ar& t.data.lam.body;
        }
        break;
    case Tapp:
        ar& t.data.app.left;
        ar& t.data.app.right;
        break;
    case Tvar:
        ar& t.data.var;
        break;
    }
}
 
term* parse_term_in(std::istream &in) {
    boost::archive::text_iarchive ar(in);
    term *ret = nullptr;
    ar >> ret;
    return ret;
}
 
term* parse_term_s(const char* s) {
    std::istringstream ss(s);
    return parse_term_in(ss);
}
def _ADD(a, b):
    return a + b
def _MULT(a, b):
    return a * b
def _bind(f, a):
    return lambda b: f(a,b)
 
def ADD(a):
    return _bind(_ADD, a)
def MULT(a):
    return _bind(_MULT, a)
def INC(a):
    return a+1
 
from z3 import *
x = IntVector('x', 28)
s = Solver()
 
def _SUB(a, b):
    # 一定要加,不加无解
    s.add(a>=b)
    return a - b
def SUB(a):
    return _bind(_SUB, a)
 
with open("ctf4.txt", "rt") as f:
    data = f.read()
 
def call(p):
    if p[0] == "P":
        p = p[3:]
        a, p = call(p)
        p = p[2:]
        b, p = call(p)
        p = p[1:]
        return a(b), p
    elif p[0] == "A":
        p = p[4:]
        a, p = call(p)
        p = p[1:]
        return ADD(a), p
    elif p[0] == "S":
        p = p[4:]
        a, p = call(p)
        p = p[1:]
        return SUB(a), p
    elif p[0] == "I":
        p = p[4:]
        a, p = call(p)
        p = p[1:]
        return INC(a), p
    elif p[0] == "M":
        p = p[5:]
        a, p = call(p)
        p = p[1:]
        return MULT(a), p
    elif p[0] == "x":
        p = p[1:]
        c = 0
        while p[c]>='0' and p[c]<='9':
            c+=1
        r = int(p[:c])
        p = p[c:]
        return x[r], p
    else:
        c = 0
        while p[c]>='0' and p[c]<='9':
            c+=1
        r = int(p[:c])
        p = p[c:]
        return r, p
 
rr, _ = call(data)
s.add(rr==0)
s.check()
print(s.model())
def _ADD(a, b):
    return a + b
def _MULT(a, b):
    return a * b
def _bind(f, a):
    return lambda b: f(a,b)
 
def ADD(a):
    return _bind(_ADD, a)
def MULT(a):
    return _bind(_MULT, a)
def INC(a):
    return a+1
 
from z3 import *
x = IntVector('x', 28)
s = Solver()
 
def _SUB(a, b):
    # 一定要加,不加无解
    s.add(a>=b)
    return a - b
def SUB(a):
    return _bind(_SUB, a)
 
with open("ctf4.txt", "rt") as f:
    data = f.read()
 
def call(p):
    if p[0] == "P":

[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课

收藏
免费 5
支持
分享
最新回复 (1)
雪    币: 378
活跃值: (1271)
能力值: ( LV6,RANK:98 )
在线值:
发帖
回帖
粉丝
2
学到了
2023-4-9 15:24
0
游客
登录 | 注册 方可回帖
返回
//