学废这两篇就能做题了
// 名称可从 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直播授课
