本文整理汇总了Python中z3.simplify函数的典型用法代码示例。如果您正苦于以下问题：Python simplify函数的具体用法？Python simplify怎么用？Python simplify使用的例子？那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了simplify函数的20个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: construct
def construct(self, obj):
'''
Takes in a ConstructableObject with preconditions
and postconditions. Checks that preconditions hold
in the proof context and if so, asserts the post-conditions.
'''
self.solver.push()
for prereq in obj.prereqs:
self.solver.add(simplify(prereq, blast_distinct = True))
prereqCheck = self.solver.check()
if str(prereqCheck) != 'sat':
print "ProofCheck >> Construction Failed - Could not meet: " + str(prereq)
self.solver.pop()
return False
if len(obj.prereqs) > 0:
self.assumptions.extend(obj.prereqs)
for conclusion in obj.conclusions:
self.solver.add(simplify(conclusion, blast_distinct=True))
self.conclusions.append(conclusion)
if isinstance(obj, Point):
self.points[obj.label] = obj
elif isinstance(obj, Line):
self.lines[obj.label] = obj
elif isinstance(obj, Circle):
self.circles[obj.label] = obj
self.solver.pop()
self.solver.add(obj.prereqs)
self.solver.add(obj.conclusions)
return True
开发者ID:kr0，项目名称:PyEuclid，代码行数:33，代码来源:core.py
示例2: prove
def prove(self, hypotheses, conclusion=None, report=None):
report = self.reportFun(report)
x_hyps, x_concl = self.analyse_expt(hypotheses, conclusion, report)
f_hyps, f_concl = self.fun_to_var([x_hyps, x_concl], report)[:]
hyps = z3.simplify(f_hyps); concl = z3.simplify(f_concl)
report('to_smt_w_expt.prove:')
report(' hypotheses = ', hyps)
report(' conclusion = ', concl)
return super(to_smt_w_expt, self).prove(hyps, concl)
开发者ID:VladimirHo，项目名称:acl2，代码行数:11，代码来源:RewriteExpt.py
示例3: getValue
def getValue(self, op):
assert(self.m <> None)
if (op.isReg()):
#if (literal):
#
#
var = map(lambda b: z3.BitVec(b,8), op.get_bytes())
var = map(lambda b: self.m[b], var)
if (len(var) > 1):
return z3.simplify(z3.Concat(var)).as_signed_long()
else:
return z3.simplify(var[0]).as_signed_long()
elif (op.isMem()):
array = z3.Array(op.mem_source, z3.BitVecSort(16), z3.BitVecSort(8))
#print "debug getValue:"
#print op, op.mem_offset ,"->", array
f = self.m[array]
#print f
#
#var = map(lambda b: z3.BitVec(b,8), op.get_bytes())
#var = map(lambda b: self.m[b], var)
#
##if (self.m):
#print "eax:"
#print "%x" % self.m[eax].as_unsigned()
#assert(0)
##print op.mem_source
##print op.mem_offset
es = f.as_list()[:-1]
var = []
for i in range(op.size):
byte = None
for entry in es:
if op.mem_offset + i == entry[0].as_signed_long():
byte = entry[1]#.as_signed_long()
break
if (byte == None):
byte = f.else_value()
var.append(byte)
var.reverse()
if (len(var) > 1):
return z3.simplify(z3.Concat(var)).as_signed_long()
else:
return z3.simplify(var[0]).as_signed_long()
开发者ID:mayfly74，项目名称:SEA，代码行数:53，代码来源:SMT.py
示例4: getDimacsMap
def getDimacsMap(goal):
d = DimacsConverter()
t = Tactic("tseitin-cnf")
cnf = t(goal)
#print cnf
clauses = []
#print(cnf)
for i in cnf:
for j in i:
variables = []
#print (j)
#print j.__class__
if len(j.children()) == 0:
variables.append(str(d.getVarIndex(str(j))))
for k in j.children():
#print k
if is_not(k):
neg="-"
newk = (simplify(Not(k)))
else:
neg=""
newk = k
variables.append(neg + str(d.getVarIndex(str(newk))))
clauses.append(variables)
inv_map = {v:k for k, v in d.vars.items()}
return inv_map
开发者ID:ai-se，项目名称:parGALE，代码行数:27，代码来源:MapDimacsBackToBestVars.py
示例5: convertToDimacs
def convertToDimacs(goal, file):
#f_n = open(Options.DIMACS_FILE, 'w')
d = DimacsConverter()
t = Tactic("tseitin-cnf")
cnf = t(goal)
#print cnf
clauses = []
#print(cnf)
for i in cnf:
for j in i:
variables = []
#print (j)
#print j.__class__
if len(j.children()) == 0:
variables.append(str(d.getVarIndex(str(j))))
for k in j.children():
#print k
if is_not(k):
neg="-"
newk = (simplify(Not(k)))
else:
neg=""
newk = k
variables.append(neg + str(d.getVarIndex(str(newk))))
clauses.append(variables)
inv_map = {v:k for k, v in d.vars.items()}
#print(inv_map)
f = open(file, 'r')
for line in f:
[var, val] = split(line)
print("\"" + str(inv_map[int(var)])+"\",")
开发者ID:ai-se，项目名称:parGALE，代码行数:32，代码来源:MapDimacsBackToBestVars.py
示例6: simplify
def simplify(self, expr):
if expr._simplified:
return expr
if self._enable_simplification_cache:
try:
k = self._simplification_cache_key[expr._cache_key]
#print "HIT WEAK KEY CACHE"
return k
except KeyError:
pass
try:
k = self._simplification_cache_val[expr._cache_key]
#print "HIT WEAK VALUE CACHE"
return k
except KeyError:
pass
#print "MISS CACHE"
l.debug("SIMPLIFYING EXPRESSION")
#print "SIMPLIFYING"
expr_raw = self.convert(expr)
#l.debug("... before: %s (%s)", expr_raw, expr_raw.__class__.__name__)
if isinstance(expr_raw, z3.BoolRef):
tactics = z3.Then(z3.Tactic("simplify"), z3.Tactic("propagate-ineqs"), z3.Tactic("propagate-values"), z3.Tactic("unit-subsume-simplify"))
s = tactics(expr_raw).as_expr()
n = s.decl().name()
if n == 'true':
s = True
elif n == 'false':
s = False
elif isinstance(expr_raw, z3.BitVecRef):
s = z3.simplify(expr_raw)
else:
s = expr_raw
for b in _eager_backends:
try:
o = self.wrap(b.convert(s))
break
except BackendError:
continue
else:
o = self._abstract(s)
#print "SIMPLIFIED"
#l.debug("... after: %s (%s)", s, s.__class__.__name__)
o._simplified = Base.FULL_SIMPLIFY
if self._enable_simplification_cache:
self._simplification_cache_val[expr._cache_key] = o
self._simplification_cache_key[expr._cache_key] = o
return o
开发者ID:zhuyue1314，项目名称:claripy，代码行数:60，代码来源:backend_z3.py
示例7: bitblast
def bitblast (e):
ctx = e.ctx
goal = z3.Goal (ctx=ctx)
goal.add (z3.simplify (e))
tactic = z3.Tactic ('bit-blast', ctx=ctx)
res = tactic.apply (goal, blast_full=True)
assert (len (res) == 1)
return res [0].as_expr ()
开发者ID:edmcman，项目名称:seahorn，代码行数:8，代码来源:z3_utils.py
示例8: PEPPolicy
def PEPPolicy(PEP, model):
disjunctions = []
for or_id in range(NUM_ORS):
conjunctions = []
for enum_id in range(NUM_ENUMS):
enumVar = TEMPLATE_ENUM_VARS[PEP][or_id][enum_id]
if model[enumVar] is not None:
synthVal = model[enumVar].as_long()
else:
synthVal = -1
if synthVal >= 0 and synthVal < len(ENUM_INDEX.keys()):
if not isinstance(ENUM_INDEX[synthVal], list):
boolVar = ENUM_INDEX[synthVal]
conjunctions.append(boolVar)
else:
[enumVar, val] = ENUM_INDEX[synthVal]
conjunctions.append(enumVar == val)
elif synthVal >= len(ENUM_INDEX.keys()) and synthVal < 2 * len(ENUM_INDEX.keys()):
if not isinstance(ENUM_INDEX[synthVal - len(ENUM_INDEX.keys())], list):
boolVar = ENUM_INDEX[synthVal - len(ENUM_INDEX.keys())]
conjunctions.append(Not(boolVar))
else:
[enumVar, val] = ENUM_INDEX[synthVal - len(ENUM_INDEX.keys())]
conjunctions.append(enumVar != val)
elif synthVal == 2 * len(ENUM_INDEX.keys()):
conjunctions.append(True)
else:
conjunctions.append(False)
for num_id in range(NUM_NUMERIC):
minVar = TEMPLATE_NUMERIC_VARS[PEP][or_id][num_id]['min']
maxVar = TEMPLATE_NUMERIC_VARS[PEP][or_id][num_id]['max']
if model[minVar] is not None and model[maxVar] is not None:
crosscheck = Solver()
crosscheck.add(model[minVar] <= model[maxVar])
if crosscheck.check() == sat:
conjunctions.append(NUM_VAR >= model[minVar].as_long())
conjunctions.append(NUM_VAR <= model[maxVar].as_long())
elif model[minVar] is not None:
conjunctions.append(NUM_VAR >= model[minVar].as_long())
elif model[maxVar] is not None:
conjunctions.append(NUM_VAR <= model[maxVar].as_long())
disjunctions.append(simplify(And(conjunctions)))
return simplify(Or(disjunctions))
开发者ID:ptsankov，项目名称:spctl，代码行数:43，代码来源:template.py
示例9: z3_flatten_exp
def z3_flatten_exp (z3exp) :
return z3.simplify (z3exp, flat=True,
# don't care about other options,
# which are true by default...
algebraic_number_evaluator=False,
bit2bool=False,
elim_sign_ext=False,
hi_div0=False,
mul_to_power=False,
push_to_real=False)
开发者ID:edmcman，项目名称:seahorn，代码行数:10，代码来源:z3_utils.py
示例10: simplify
def simplify(self, expr):
if expr._simplified:
return expr
if self._enable_simplification_cache:
try:
k = self._simplification_cache_key[expr._cache_key]
#print "HIT WEAK KEY CACHE"
return k
except KeyError:
pass
try:
k = self._simplification_cache_val[expr._cache_key]
#print "HIT WEAK VALUE CACHE"
return k
except KeyError:
pass
#print "MISS CACHE"
l.debug("SIMPLIFYING EXPRESSION")
#print "SIMPLIFYING"
expr_raw = self.convert(expr)
#l.debug("... before: %s (%s)", expr_raw, expr_raw.__class__.__name__)
#s = expr_raw
if isinstance(expr_raw, z3.BoolRef):
tactics = z3.Then(
z3.Tactic("simplify", ctx=self._context),
z3.Tactic("propagate-ineqs", ctx=self._context),
z3.Tactic("propagate-values", ctx=self._context),
z3.Tactic("unit-subsume-simplify", ctx=self._context),
ctx=self._context
)
s = tactics(expr_raw).as_expr()
#n = s.decl().name()
#if n == 'true':
# s = True
#elif n == 'false':
# s = False
elif isinstance(expr_raw, z3.BitVecRef):
s = z3.simplify(expr_raw)
else:
s = expr_raw
o = self._abstract(s)
o._simplified = Base.FULL_SIMPLIFY
if self._enable_simplification_cache:
self._simplification_cache_val[expr._cache_key] = o
self._simplification_cache_key[expr._cache_key] = o
return o
开发者ID:redragonvn，项目名称:claripy，代码行数:55，代码来源:backend_z3.py
示例11: solve_for
def solve_for(inps):
r1, r2, r3, r4, v11 = [BVV(x, 64) for x in map(int, inps.split(', '))]
print r1, r2, r3, r4, v11
for choice1, choice2, choice3 in all_choices():
v6 = choose_op(r1, r2, choice1)
v6_1 = choose_op(v6, r3, choice2)
v6_2 = choose_op(v6_1, r4, choice3)
if simplify(weird_op(v6_2)) == v11:
return choice1, choice2, choice3
开发者ID:isislab，项目名称:CTF-Solutions，代码行数:11，代码来源:rasf.py
示例12: interpret
def interpret(self, i, j):
""" Convert logical indices i and j into a physical index. """
Bx = i / self.lsize0()
By = j / self.lsize1()
p = self.fragment(Bx, By)
if not self.terminal():
x = i % self.lsize0()
y = j % self.lsize1()
p *= self.elem_size()
p += self.rest.interpret(x, y)
return z3.simplify(p)
开发者ID:mbdriscoll，项目名称:LogicalIndexingLibrary，代码行数:11，代码来源:lil.py
示例13: _pattern
def _pattern(self, pattern, L):
# we can exit early if we have a variable
if self._is_var(pattern):
return True
constraints = [True]
f, *args = breakout(pattern)
# now we'll recurse appropriately
for i, arg in enumerate(args):
constraints.append( self._connect(f, i, arg, L) )
constraints.append( self._pattern(arg, L))
return simplify(And(constraints))
开发者ID:csmith49，项目名称:morlock，代码行数:11，代码来源:equations.py
示例14: getValue
def getValue(self, op):
assert(self.m <> None)
if (op |iss| RegOp):
var = map(lambda b: z3.BitVec(str(b),8), op.getLocations())
var = map(lambda b: self.m[b], var)
if (len(var) > 1):
return z3.simplify(z3.Concat(var)).as_signed_long()
else:
return z3.simplify(var[0]).as_signed_long()
elif (op.isMem()):
array = z3.Array(op.name, z3.BitVecSort(16), z3.BitVecSort(8))
f = self.m[array]
#print self.m
es = f.as_list()[:-1]
var = []
for loc in op.getLocations():
byte = None
for entry in es:
#print entry
if loc.getIndex() == entry[0].as_signed_long():
byte = entry[1]#.as_signed_long()
break
if (byte == None):
byte = f.else_value()
var.append(byte)
var.reverse()
if (len(var) > 1):
return z3.simplify(z3.Concat(var)).as_signed_long()
else:
return z3.simplify(var[0]).as_signed_long()
else:
assert(0)
开发者ID:Debug-Orz，项目名称:SEA，代码行数:41，代码来源:SMT.py
示例15: prove
def prove(self, hypotheses, conclusion=None, report=None):
report = self.reportFun(report)
if (conclusion is None):
conclusion = hypotheses
hypotheses = True
x_hyps, x_concl = self.analyse_expt(z3.And(hypotheses,z3.Not(conclusion)), conclusion, report)
f_hyps, f_concl = self.fun_to_var([x_hyps, x_concl], report)[:]
if(f_hyps is None):
hyps = f_hyps
else:
hyps = z3.simplify(f_hyps)
if(f_concl is None):
concl = f_concl
else:
concl = z3.simplify(f_concl)
report('to_smt_w_expt.prove:')
report(' hypotheses = ', hyps)
report(' conclusion = ', concl)
return super(to_smt_w_expt, self).prove(hyps, concl)
开发者ID:harshrc，项目名称:acl2，代码行数:22，代码来源:RewriteExpt.py
示例16: simplify
def simplify(self, expr): #pylint:disable=arguments-differ
if expr._simplified:
return expr
if self._enable_simplification_cache:
try:
k = self._simplification_cache_key[expr._cache_key]
#print "HIT WEAK KEY CACHE"
return k
except KeyError:
pass
try:
k = self._simplification_cache_val[expr._cache_key]
#print "HIT WEAK VALUE CACHE"
return k
except KeyError:
pass
#print "MISS CACHE"
l.debug("SIMPLIFYING EXPRESSION")
#print "SIMPLIFYING"
expr_raw = self.convert(expr)
#l.debug("... before: %s (%s)", expr_raw, expr_raw.__class__.__name__)
#s = expr_raw
if isinstance(expr_raw, z3.BoolRef):
boolref_tactics = self._boolref_tactics
s = boolref_tactics(expr_raw).as_expr()
#n = s.decl().name()
#if n == 'true':
# s = True
#elif n == 'false':
# s = False
elif isinstance(expr_raw, z3.BitVecRef):
s = z3.simplify(expr_raw)
else:
s = expr_raw
o = self._abstract(s)
o._simplified = Base.FULL_SIMPLIFY
if self._enable_simplification_cache:
self._simplification_cache_val[expr._cache_key] = o
self._simplification_cache_key[expr._cache_key] = o
return o
开发者ID:iamahuman，项目名称:claripy，代码行数:49，代码来源:backend_z3.py
示例17: constraints_for_call
def constraints_for_call(self, call):
situations = []
rule = self.rule_for_call(call)
for priority, z3_meaning in rule.meaning_of(self.history, call):
situational_exprs = [z3_meaning]
for unmade_call, unmade_rule in self._call_to_rule.iteritems():
for unmade_priority, unmade_z3_meaning in unmade_rule.meaning_of(self.history, unmade_call):
if self.system.priority_ordering.lt(priority, unmade_priority):
if self.explain and self.expected_call == call:
print "Adding negation %s (%s) to %s:" % (unmade_rule.name, unmade_call.name, rule.name)
print " %s" % z3.simplify(z3.Not(unmade_z3_meaning))
situational_exprs.append(z3.Not(unmade_z3_meaning))
situations.append(z3.And(situational_exprs))
return z3.Or(situations)
开发者ID:abortz，项目名称:saycbridge，代码行数:15，代码来源:bidder.py
示例18: _constrain_eq_vars
def _constrain_eq_vars(self, E, L):
constraints = []
for l, r in combinations(L, 2):
if l.type == "return" and r.type == "return":
lcomp, rcomp = self.components[l.component], self.components[r.component]
if lcomp.sexpr != rcomp.sexpr:
constraints.append( E[(l, r)] == False )
else:
local = [True]
for i in range(len(lcomp.parameters)):
li, ri = get_ith_input(l.component, i, L), get_ith_input(r.component, i, L)
local.append( E[(li, ri)] )
constraints.append( E[(l, r)] == And(local) )
elif l.type == "parameter" and r.type == "parameter": # type is parameter
local = [(l.value == r.value)]
for f, g in permutations([get_output(c, L) for c, _ in self.components.items()], 2):
local.append( And([l.value == f.value, r.value == g.value, E[(f, g)]]) )
constraints.append( E[(l, r)] == Or(local) )
return simplify(And(constraints))
开发者ID:csmith49，项目名称:morlock，代码行数:19，代码来源:equations.py
示例19: test19
def test19 () :
x = z3.Int ('x')
y = z3.Int ('y')
z = z3.Int ('z')
s = z3.Solver ()
cons = z3.Or ([])
print 'cons', cons
print 'simplify', z3.simplify (cons)
s.add (cons)
s.add (z3.Or (x == y, x == z))
print 'constraints to solve:', s
c = s.check ()
print 'result:', c
if c == z3.sat :
m = s.model ()
print 'model:', m
开发者ID:nojero，项目名称:pod，代码行数:20，代码来源:test.py
示例20: smt_solution
def smt_solution(self, timeout, neg_points=None):
neg_points = neg_points or []
solver = z3.Solver()
solver.set("timeout", timeout)
b = self.offset
z3_b = z3.Int("b")
if b > 0:
solver.add(z3_b >= 0)
solver.add(z3_b <= b)
elif b < 0:
solver.add(z3_b <= 0)
solver.add(z3_b >= b)
else:
solver.add(z3_b == 0)
pos_x = True
simple = sum(abs(x) for x in self.normal) < 1
non_trivial = False
if not simple:
some_consume = False
some_produce = False
diff_sol = z3_b != b
h1 = b
h2 = z3_b
variables = []
for t_id, val in enumerate(self.normal):
if not val:
continue
z3_val = z3.Int("a" + str(t_id))
x = z3.Int("x" + str(t_id))
variables.append(x)
pos_x = z3.And(pos_x, x >= 0)
if val > 0:
solver.add(0 <= z3_val)
solver.add(z3_val <= val)
elif val < 0:
solver.add(z3_val <= 0)
solver.add(val <= z3_val)
if not simple:
some_consume = z3.Or(some_consume, z3_val < 0)
some_produce = z3.Or(some_produce, z3_val > 0)
non_trivial = z3.Or(non_trivial, z3_val != 0)
diff_sol = z3.Or(diff_sol, z3_val != val)
h1 = h1 + val * x
h2 = h2 + z3_val * x
if not simple:
solver.add(z3.simplify(some_consume))
solver.add(z3.simplify(some_produce))
solver.add(z3.simplify(non_trivial))
solver.add(z3.simplify(diff_sol))
solver.add(z3.simplify(z3.ForAll(variables, z3.Implies(z3.And(pos_x, h1 <= 0), h2 <= 0))))
## non negative point should be a solution
for np in list(neg_points)[:min(100,len(neg_points))]:
smt_np = False
ineq_np = self.offset
for t_id, val in enumerate(self.normal):
z3_var = z3.Int("a" + str(t_id))
ineq_np = ineq_np + z3_var * np[t_id]
smt_np = z3.simplify(z3.Or(smt_np, ineq_np < 0))
solver.add(smt_np)
#import pdb;pdb.set_trace()
sol = solver.check()
if sol == z3.unsat or sol == z3.unknown:
ret = False
del(solver)
del(sol)
else:
ret = solver.model()
return ret
开发者ID:Macuyiko，项目名称:PacH，代码行数:78，代码来源:halfspace.py
注：本文中的z3.simplify函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。 |
客服电话
APP下载
官方微信
请发表评论