python3通过pycharm编译器调用requests接口返回JSON格式Unexpected UTF-8 BOM (decode using utf-8-sig)

Python026

python3通过pycharm编译器调用requests接口返回JSON格式Unexpected UTF-8 BOM (decode using utf-8-sig),第1张

因为你的req内容包含BOM字符，去掉req中BOM头的方法如下

if req.startswith(u'\ufeff'):

    req = req.encode('utf8')[3:].decode('utf8')

Z3支持许多平台以及多种语言接口，这里我们简单介绍其Python接口的使用。

以Mac OS X为例，下载Z3可执行文件后，要设置环境变量PATH和PYTHONPATH：

export PATH=$PATH:<installation path of z3>

export PYTHONPATH=$PYTHONPATH:<installation path of z3>

然后我们编辑一个简单的例子 stock.py：

#!/usr/bin/env python

from z3 import *

def main (argv):

ds = Real('ds')

fs = Real('fs')

ps = Real('ps')

origin = And ( Not (And (0<=ds, 1<=fs, 1<=ps)),

Implies (And (0<=ds, 0<=fs, 0<=ps), ds<=3),

Implies (And (0<=ds, 0<=fs, 0<=ps, fs<=1), ds+fs<=3),

Implies (And (0<=ds, 0<=ps, 1<=fs, ps<=1), ds+ps<=2))

solver2 = Solver()

solver2.add (origin)

solver2.push()

solver2.add (ds == dv/1000)

solver2.add (fs == fv/1000)

solver2.add (ps == pv/1000)

if solver2.check() == sat:

sat_count2 = sat_count2 + 1

solver2.pop()

从31到33行，声明3个实数变量，在35行我们定义一个逻辑公式并在47行加入当前环境中，77行调用check()方法并检查其返回值：sat －－ 公式有解；unsat －－ 公式无法满足。注意72，79行的push()和pop()方法是用来暂存和恢复环境。