Fork of pySMT which implements support for QF_FXP

Two translators are available in pysmt/rewritings.py:

• A fixed-point to real converter (

  pysmt/pysmt/rewritings.py

  Lines 1249 to 1502 in 0a6a72a

  	class FXPToReal(DagWalker):
  	def __init__(self, environment=None):
  	DagWalker.__init__(self, environment)
  	self.mgr = self.env.formula_manager
  	self.symbol_map = dict()
  	self.st_real = self.mgr.Real(0)
  	self.wp_real = self.mgr.Real(1)
  	self.ru_real = self.mgr.Real(0)
  	self.rd_real = self.mgr.Real(1)
  	#def convert(self, formula):
  	# return self.walk(formula)
  	def walk_and(self, formula, args, **kwargs):
  	return self.mgr.And(*args)
  	def walk_or(self, formula, args, **kwargs):
  	return self.mgr.Or(*args)
  	def walk_implies(self, formula, args, **kwargs):
  	return self.mgr.Implies(args[0], args[1])
  	def process_real_noround(self,realval,om,sign,total_width,frac_width):
  	if sign==0:
  	max_value = self.mgr.Real(Fraction(2**total_width - 1, 2**frac_width))
  	min_value = self.mgr.Real(0)
  	else:
  	max_value = self.mgr.Real(Fraction(2**(total_width - 1)-1, 2**frac_width))
  	min_value = self.mgr.Real(Fraction(-2**(total_width - 1), 2**frac_width))
  	modulo=self.mgr.Real(2**(total_width-frac_width))
  	flodiv=self.mgr.RealToInt(self.mgr.Div(realval,modulo,reduce_const=False))
  	divres=self.mgr.ToReal(flodiv)
  	remain=self.mgr.Minus(realval,self.mgr.Times(modulo,divres))
  	if sign==1:
  	remain=self.mgr.Ite(
  	self.mgr.LE(remain, max_value),
  	remain,
  	self.mgr.Minus(remain,modulo)
  	)
  	wrapped_res = remain
  	saturated_res = self.mgr.Ite(
  	self.mgr.GT(realval, max_value),
  	max_value,
  	self.mgr.Ite(self.mgr.LT(realval, min_value), min_value, realval)
  	)
  	return self.mgr.Ite(self.mgr.Equals(om, self.wp_real),
  	wrapped_res,
  	saturated_res)
  	def round_real(self,realval,rm,frac_width):
  	base=self.mgr.Real(2**frac_width)
  	flo=self.mgr.RealToInt(self.mgr.Times(realval,base))
  	result = self.mgr.ToReal(flo)
  	frac = self.mgr.Minus(result, self.mgr.Times(realval,base))
  	result = self.mgr.Ite(
  	self.mgr.And(
  	self.mgr.Equals(rm, self.ru_real),
  	self.mgr.Not(
  	self.mgr.Equals(
  	frac,
  	self.mgr.Real(0)))),
  	self.mgr.Plus(result,self.mgr.Real(1)),
  	result)
  	result = self.mgr.Div(result,base)
  	return result
  	def process_real_round(self,realval,om,rm,sign,total_width,frac_width):
  	tempres = self.round_real(realval,rm,frac_width)
  	result = self.process_real_noround(tempres,om,sign,total_width,frac_width)
  	return result
  	def walk_ufxp_add(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	om = args[0]
  	left = args[1]
  	right = args[2]
  	result = self.mgr.Plus(left,right)
  	return self.process_real_noround(result,om,0,total_width,frac_width)
  	def walk_sfxp_add(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	om = args[0]
  	left = args[1]
  	right = args[2]
  	result = self.mgr.Plus(left,right)
  	return self.process_real_noround(result,om,1,total_width,frac_width)
  	def walk_ufxp_sub(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	om = args[0]
  	left = args[1]
  	right = args[2]
  	result = self.mgr.Minus(left,right)
  	return self.process_real_noround(result,om,0,total_width,frac_width)
  	def walk_sfxp_sub(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	om = args[0]
  	left = args[1]
  	right = args[2]
  	result = self.mgr.Minus(left,right)
  	return self.process_real_noround(result,om,1,total_width,frac_width)
  	def walk_ufxp_mul(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	om = args[0]
  	rm = args[1]
  	left = args[2]
  	right = args[3]
  	result = self.mgr.Times(left,right)
  	return self.process_real_round(result,om,rm,0,total_width,frac_width)
  	def walk_sfxp_mul(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	om = args[0]
  	rm = args[1]
  	left = args[2]
  	right = args[3]
  	result = self.mgr.Times(left,right)
  	return self.process_real_round(result,om,rm,1,total_width,frac_width)
  	def walk_ufxp_div(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	om = args[0]
  	rm = args[1]
  	left = args[2]
  	right = args[3]
  	return self.process_real_round(self.mgr.Div(left,right,reduce_const=False),om,rm,0,total_width,frac_width)
  	def walk_sfxp_div(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	om = args[0]
  	rm = args[1]
  	left = args[2]
  	right = args[3]
  	return self.process_real_round(self.mgr.Div(left,right,reduce_const=False),om,rm,1,total_width,frac_width)
  	def walk_symbol(self, formula, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	if ty.is_fxp_type():
  	if formula not in self.symbol_map:
  	self.symbol_map[formula] = \
  	self.mgr.FreshSymbol(types.REAL)
  	return self.symbol_map[formula]
  	elif ty.is_fxp_om_type() or ty.is_fxp_rm_type():
  	if formula not in self.symbol_map:
  	self.symbol_map[formula] = \
  	self.mgr.FreshSymbol(types.REAL)
  	return self.symbol_map[formula]
  	else:
  	return formula
  	def walk_st(self, formula, **kwargs):
  	return self.st_real
  	def walk_wp(self, formula, **kwargs):
  	return self.wp_real
  	def walk_ru(self, formula, **kwargs):
  	return self.ru_real
  	def walk_rd(self, formula, **kwargs):
  	return self.rd_real
  	def walk_equals(self, formula, args, **kwargs):
  	left = args[0]
  	right = args[1]
  	return self.mgr.Equals(left, right)
  	def walk_ite(self, formula, args, **kwargs):
  	return formula
  	def walk_not(self, formula, args, **kwargs):
  	return self.mgr.Not(args[0])
  	def walk_bv_constant(self, formula, args, **kwargs):
  	return formula
  	def convert(self, formula):
  	return self.walk(formula)
  	def walk_ufxp_constant(self, formula, args, **kwargs):
  	bv = args[0]
  	bv_val = bv._content.payload[0]
  	frac_width = formula._content.payload[0]
  	return self.mgr.Real(Fraction(bv_val, 2**frac_width))
  	def walk_sfxp_constant(self, formula, args, **kwargs):
  	bv = args[0]
  	bv_val = bv._content.payload[0]
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = formula._content.payload[0]
  	if bv_val>2**(total_width-1)-1:
  	bv_val=bv_val-2**total_width
  	return self.mgr.Real(Fraction(bv_val, 2**frac_width))
  	def walk_ufxp_lt(self, formula, args, **kwargs):
  	return self.mgr.LT(args[0], args[1])
  	def walk_ufxp_le(self, formula, args, **kwargs):
  	return self.mgr.LE(args[0], args[1])
  	def walk_sfxp_gt(self, formula, args, **kwargs):
  	return self.mgr.GT(args[0], args[1])
  	def walk_sfxp_ge(self, formula, args, **kwargs):
  	return self.mgr.GE(args[0], args[1])
  	def walk_sfxp_lt(self, formula, args, **kwargs):
  	return self.mgr.LT(args[0], args[1])
  	def walk_sfxp_le(self, formula, args, **kwargs):
  	return self.mgr.LE(args[0], args[1])
  	def walk_ufxp_gt(self, formula, args, **kwargs):
  	return self.mgr.GT(args[0], args[1])
  	def walk_ufxp_ge(self, formula, args, **kwargs):
  	return self.mgr.GE(args[0], args[1])
  	def walk_bool_constant(self, formula, args, *kwargs):
  	return formula
  	def walk_iff(self, formula, args, *kwargs):
  	return self.mgr.Iff(args[0], args[1])

  )
• A fixed-point to bitvector converter (

  pysmt/pysmt/rewritings.py

  Lines 825 to 1247 in 0a6a72a

  	class FXPToBV(DagWalker):
  	def __init__(self, environment=None):
  	DagWalker.__init__(self, environment)
  	self.mgr = self.env.formula_manager
  	self.symbol_map = dict()
  	self.st_bv = self.mgr.BV(0, 1)
  	self.wp_bv = self.mgr.BV(1, 1)
  	self.ru_bv = self.mgr.BV(0, 1)
  	self.rd_bv = self.mgr.BV(1, 1)
  	self.divz_res = dict()
  	def _get_divz_res(self, sgn, tb, fb):
  	key = (sgn, tb, fb)
  	if key not in self.divz_res.keys():
  	ftype = types.FunctionType(types.BVType(tb), [types.BVType(1), types.BVType(1), types.BVType(tb)])
  	func = self.mgr.FreshSymbol(ftype)
  	self.divz_res[key] = func
  	return self.divz_res[key]
  	def convert(self, formula):
  	return self.walk(formula)
  	def bv_extend(self, bv, length, sign):
  	if sign:
  	return self.mgr.BVSExt(bv, length)
  	else:
  	return self.mgr.BVZExt(bv, length)
  	def walk_ufxp_add(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	extended_width = total_width + 1
  	max_value = self.mgr.BV(2**total_width - 1, total_width)
  	extended_max_value = self.mgr.BV(2**total_width - 1, extended_width)
  	om = args[0]
  	left = args[1]
  	right = args[2]
  	extended_sum = self.mgr.BVAdd(
  	self.bv_extend(left, 1, False),
  	self.bv_extend(right, 1, False))
  	wrapped_sum = self.mgr.BVAdd(left, right)
  	saturated_sum = self.mgr.Ite(
  	self.mgr.BVUGT(extended_sum, extended_max_value),
  	max_value,
  	wrapped_sum)
  	return self.mgr.Ite(self.mgr.Equals(om, self.wp_bv),
  	wrapped_sum,
  	saturated_sum)
  	def convert_sfxp_lop(self, bv_op, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	extended_width = total_width + 1
  	max_value = self.mgr.SBV(2**(total_width - 1) - 1, total_width)
  	extended_max_value = self.mgr.SBV(2**(total_width - 1) - 1, extended_width)
  	min_value = self.mgr.SBV(-2**(total_width - 1), total_width)
  	extended_min_value = self.mgr.SBV(-2**(total_width - 1), extended_width)
  	om = args[0]
  	left = args[1]
  	right = args[2]
  	extended_sum = bv_op(
  	self.bv_extend(left, 1, True),
  	self.bv_extend(right, 1, True))
  	wrapped_sum = bv_op(left, right)
  	saturated_sum = self.mgr.Ite(
  	self.mgr.BVSGT(extended_sum, extended_max_value),
  	max_value,
  	self.mgr.Ite(
  	self.mgr.BVSLT(extended_sum, extended_min_value),
  	min_value,
  	wrapped_sum))
  	return self.mgr.Ite(self.mgr.Equals(om, self.wp_bv),
  	wrapped_sum,
  	saturated_sum)
  	def walk_sfxp_add(self, formula, args, **kwargs):
  	return self.convert_sfxp_lop(self.mgr.BVAdd, formula, args, **kwargs)
  	def walk_ufxp_sub(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	om = args[0]
  	left = args[1]
  	right = args[2]
  	wrapped_sub = self.mgr.BVSub(left, right)
  	saturated_sub = self.mgr.Ite(
  	self.mgr.BVUGT(left, right),
  	wrapped_sub,
  	self.mgr.BV(0, total_width))
  	return self.mgr.Ite(self.mgr.Equals(om, self.wp_bv),
  	wrapped_sub,
  	saturated_sub)
  	def walk_sfxp_sub(self, formula, args, **kwargs):
  	return self.convert_sfxp_lop(self.mgr.BVSub, formula, args, **kwargs)
  	def walk_ufxp_mul(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	extended_width = total_width * 2
  	frac_width = ty.frac_width
  	om = args[0]
  	rm = args[1]
  	left = args[2]
  	right = args[3]
  	# sign extended to double bit-width
  	extended_left = self.bv_extend(left, total_width, False)
  	extended_right = self.bv_extend(right, total_width, False)
  	# perform multiplication
  	# the result is
  	# | integral part (2*int_width) | fractional part (2* frac_width)|
  	# that represents the exact result
  	# x*y/2^(2*fb)
  	precise_res_in_bv = self.mgr.BVMul(extended_left, extended_right)
  	# do rounding
  	dumped_bits = self.mgr.BVExtract(precise_res_in_bv, 0, frac_width - 1)
  	rounded_res_in_bv = self.mgr.BVExtract(precise_res_in_bv, frac_width,
  	extended_width - 1)
  	# if rounding mode is round up and the last frac_width bits are not 0s,
  	# round the left part up by 1
  	# otherwise use the remaining bits
  	rounded_res_in_bv = self.mgr.Ite(
  	self.mgr.And(
  	self.mgr.Equals(rm, self.ru_bv),
  	self.mgr.Not(
  	self.mgr.Equals(
  	dumped_bits,
  	self.mgr.BV(0, frac_width)))),
  	self.mgr.BVAdd(
  	rounded_res_in_bv,
  	self.mgr.BV(1, extended_width - frac_width)),
  	rounded_res_in_bv)
  	# overflow handling
  	max_value_in_extended_width = self.mgr.BV(2**total_width - 1,
  	extended_width - frac_width)
  	wrapped_res = self.mgr.BVExtract(rounded_res_in_bv, 0, total_width - 1)
  	saturated_res = self.mgr.Ite(
  	self.mgr.BVUGT(rounded_res_in_bv, max_value_in_extended_width),
  	self.mgr.BV(2**total_width - 1, total_width),
  	wrapped_res)
  	return self.mgr.Ite(
  	self.mgr.Equals(om, self.wp_bv),
  	wrapped_res,
  	saturated_res)
  	def walk_sfxp_mul(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	extended_width = total_width * 2
  	frac_width = ty.frac_width
  	om = args[0]
  	rm = args[1]
  	left = args[2]
  	right = args[3]
  	# sign extended to double bit-width
  	extended_left = self.bv_extend(left, total_width, True)
  	extended_right = self.bv_extend(right, total_width, True)
  	# perform multiplication
  	# the result is
  	# | integral part (2*int_width) | fractional part (2* frac_width)|
  	# that represents the exact result
  	# x*y/2^(2*fb)
  	precise_res_in_bv = self.mgr.BVMul(extended_left, extended_right)
  	# do rounding
  	dumped_bits = self.mgr.BVExtract(precise_res_in_bv, 0, frac_width - 1)
  	rounded_res_in_bv = self.mgr.BVExtract(precise_res_in_bv, frac_width,
  	extended_width - 1)
  	# if rounding mode is round up and the last frac_width bits are not 0s,
  	# round the left part up by 1
  	# otherwise use the remaining bits
  	rounded_res_in_bv = self.mgr.Ite(
  	self.mgr.And(
  	self.mgr.Equals(rm, self.ru_bv),
  	self.mgr.Not(
  	self.mgr.Equals(
  	dumped_bits,
  	self.mgr.BV(0, frac_width)))),
  	self.mgr.BVAdd(
  	rounded_res_in_bv,
  	self.mgr.BV(1, extended_width - frac_width)),
  	rounded_res_in_bv)
  	# overflow handling
  	max_value_in_extended_width = self.mgr.BV(2**(total_width - 1) - 1,
  	extended_width - frac_width)
  	min_value_in_extended_width = self.mgr.BV((2**(total_width - frac_width
  	+ 1) - 1) << (total_width - 1), extended_width - frac_width)
  	wrapped_res = self.mgr.BVExtract(rounded_res_in_bv, 0, total_width - 1)
  	saturated_res = self.mgr.Ite(
  	self.mgr.BVSGT(rounded_res_in_bv, max_value_in_extended_width),
  	self.mgr.BV(2**(total_width - 1) - 1, total_width),
  	self.mgr.Ite(
  	self.mgr.BVSLT(rounded_res_in_bv,
  	min_value_in_extended_width),
  	self.mgr.BV(1 << (total_width - 1), total_width),
  	wrapped_res))
  	return self.mgr.Ite(
  	self.mgr.Equals(om, self.wp_bv),
  	wrapped_res,
  	saturated_res)
  	def walk_ufxp_div(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	extended_width = total_width + frac_width
  	om = args[0]
  	rm = args[1]
  	dividend = args[2]
  	divisor = args[3]
  	zero = self.mgr.BV(0, total_width)
  	allones = self.mgr.BV(2**total_width - 1, total_width)
  	# x/y needs to rounds to z/(2^fb)
  	# this amounts to (2^fb)*(x/y) rounds to z
  	extended_dividend = self.mgr.BVLShl(
  	self.bv_extend(dividend, frac_width, False),
  	self.mgr.BV(frac_width, extended_width))
  	extended_divisor = self.bv_extend(divisor, frac_width, False)
  	extended_res = self.mgr.BVUDiv(extended_dividend, extended_divisor)
  	remainder = self.mgr.BVURem(extended_dividend, extended_divisor)
  	# do rounding
  	rounded_res = self.mgr.Ite(
  	self.mgr.And(
  	self.mgr.Equals(rm, self.ru_bv),
  	self.mgr.Not(
  	self.mgr.Equals(
  	remainder,
  	self.mgr.BV(0, extended_width)))),
  	self.mgr.BVAdd(extended_res, self.mgr.BV(1, extended_width)),
  	extended_res)
  	# overflow handling
  	max_value = self.mgr.BV(2**total_width - 1, total_width)
  	extended_max_value = self.mgr.BV(2**total_width - 1, extended_width)
  	wrapped_res = self.mgr.BVExtract(rounded_res, 0, total_width - 1)
  	saturated_res = self.mgr.Ite(
  	self.mgr.BVUGT(extended_res, extended_max_value),
  	max_value,
  	wrapped_res)
  	divz_res = self._get_divz_res(False, total_width, frac_width)
  	return self.mgr.Ite(
  	self.mgr.Equals(divisor, zero),
  	divz_res(om, rm, dividend),
  	self.mgr.Ite(
  	self.mgr.Equals(om, self.wp_bv),
  	wrapped_res,
  	saturated_res))
  	def walk_sfxp_div(self, formula, args, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	total_width = ty.total_width
  	frac_width = ty.frac_width
  	# we need the additional bit as the bvsdiv may overflow
  	extended_width = total_width + frac_width + 1
  	om = args[0]
  	rm = args[1]
  	dividend = args[2]
  	divisor = args[3]
  	zero = self.mgr.BV(0, total_width)
  	extended_zero = self.mgr.BV(0, extended_width)
  	extended_one = self.mgr.BV(1, extended_width)
  	allones = self.mgr.BV(2**total_width - 1, total_width)
  	# x/y needs to rounds to z/(2^fb)
  	# this amounts to (2^fb)*(x/y) rounds to z
  	extended_dividend = self.mgr.BVLShl(
  	self.bv_extend(dividend, frac_width + 1, True),
  	self.mgr.BV(frac_width, extended_width))
  	extended_divisor = self.bv_extend(divisor, frac_width + 1, True)
  	extended_res = self.mgr.BVSDiv(extended_dividend, extended_divisor)
  	remainder = self.mgr.BVSRem(extended_dividend, extended_divisor)
  	# do rounding
  	def get_bv_sign(bv):
  	msb_pos = total_width - 1
  	return self.mgr.Equals(
  	self.mgr.BVExtract(bv, msb_pos, msb_pos),
  	self.mgr.BV(1, 1))
  	if_ru = self.mgr.Equals(rm, self.ru_bv)
  	dividend_sign = get_bv_sign(dividend)
  	divisor_sign = get_bv_sign(divisor)
  	if_pos = self.mgr.Not(
  	self.mgr.Xor(dividend_sign, divisor_sign))
  	rounded_res = self.mgr.Ite(
  	self.mgr.Or(
  	self.mgr.Xor(if_ru, if_pos),
  	self.mgr.Equals(
  	remainder,
  	extended_zero)),
  	extended_res,
  	self.mgr.Ite(
  	self.mgr.And(if_ru, if_pos),
  	self.mgr.BVAdd(extended_res, extended_one),
  	self.mgr.BVSub(extended_res, extended_one)))
  	# overflow handling
  	max_value = self.mgr.BV(2**(total_width-1) - 1, total_width)
  	extended_max_value = self.mgr.BV(2**(total_width-1) - 1, extended_width)
  	min_value = self.mgr.SBV(-(2**(total_width - 1)), total_width)
  	extended_min_value = self.mgr.SBV(-(2**(total_width - 1)), extended_width)
  	wrapped_res = self.mgr.BVExtract(rounded_res, 0, total_width - 1)
  	saturated_res = self.mgr.Ite(
  	self.mgr.BVSGT(extended_res, extended_max_value),
  	max_value,
  	self.mgr.Ite(
  	self.mgr.BVSLT(extended_res, extended_min_value),
  	min_value,
  	wrapped_res))
  	divz_res = self._get_divz_res(True, total_width, frac_width)
  	return self.mgr.Ite(
  	self.mgr.Equals(divisor, zero),
  	# Uninterpreted result on division by zero
  	divz_res(om, rm, dividend),
  	self.mgr.Ite(
  	self.mgr.Equals(dividend, zero),
  	zero,
  	self.mgr.Ite(
  	self.mgr.Equals(om, self.wp_bv),
  	wrapped_res,
  	saturated_res)))
  	def walk_symbol(self, formula, **kwargs):
  	ty = self.env.stc.get_type(formula)
  	if ty.is_fxp_type():
  	if formula not in self.symbol_map:
  	self.symbol_map[formula] = \
  	self.mgr.FreshSymbol(types.BVType(ty.total_width))
  	return self.symbol_map[formula]
  	elif ty.is_fxp_om_type() or ty.is_fxp_rm_type():
  	if formula not in self.symbol_map:
  	self.symbol_map[formula] = \
  	self.mgr.FreshSymbol(types.BVType(1))
  	return self.symbol_map[formula]
  	else:
  	return formula
  	def walk_st(self, formula, **kwargs):
  	return self.st_bv
  	def walk_wp(self, formula, **kwargs):
  	return self.wp_bv
  	def walk_ru(self, formula, **kwargs):
  	return self.ru_bv
  	def walk_rd(self, formula, **kwargs):
  	return self.rd_bv
  	def walk_equals(self, formula, args, **kwargs):
  	left = args[0]
  	right = args[1]
  	return self.mgr.Equals(left, right)
  	def walk_and(self, formula, args, **kwargs):
  	return self.mgr.And(*args)
  	def walk_or(self, formula, args, **kwargs):
  	return self.mgr.Or(*args)
  	def walk_function(self, formula, **kwargs):
  	return formula
  	def walk_implies(self, formula, args, **kwargs):
  	left = args[0]
  	right = args[1]
  	return self.mgr.Implies(left, right)
  	def walk_ite(self, formula, args, **kwargs):
  	return formula
  	def walk_not(self, formula, args, **kwargs):
  	return self.mgr.Not(args[0])
  	def walk_bv_constant(self, formula, args, **kwargs):
  	return formula
  	def walk_ufxp_constant(self, formula, args, **kwargs):
  	return formula.arg(0)
  	def walk_sfxp_constant(self, formula, args, **kwargs):
  	return formula.arg(0)
  	def walk_ufxp_lt(self, formula, args, **kwargs):
  	return self.mgr.BVULT(args[0], args[1])
  	def walk_ufxp_le(self, formula, args, **kwargs):
  	return self.mgr.BVULE(args[0], args[1])
  	def walk_sfxp_lt(self, formula, args, **kwargs):
  	return self.mgr.BVSLT(args[0], args[1])
  	def walk_sfxp_le(self, formula, args, **kwargs):
  	return self.mgr.BVSLE(args[0], args[1])
  	def walk_bool_constant(self, formula, args, **kwargs):
  	return formula
  	def walk_iff(self, formula, args, **kwargs):
  	left = args[0]
  	right = args[1]
  	return self.mgr.Iff(left, right)

  )

An example script is also provided (https://github.com/soarlab/pysmt/blob/fixed-points/fxp2smt.py) which converts a QF_FXP smt2 query file to a QF_UFBV or QF_NIRA smt2 query, depending on whether the BV variable is set to True or False respectively.

pySMT: a Python API for SMT

pySMT makes working with Satisfiability Modulo Theory simple:

• Define formulae in a simple, intuitive, and solver independent way
• Solve your formulae using one of the native solvers, or by wrapping any SMT-Lib compliant solver,
• Dump your problems in the SMT-Lib format,
• and more...

Usage

>>> from pysmt.shortcuts import Symbol, And, Not, is_sat
>>>
>>> varA = Symbol("A") # Default type is Boolean
>>> varB = Symbol("B")
>>> f = And(varA, Not(varB))
>>> f
(A & (! B))
>>> is_sat(f)
True
>>> g = f.substitute({varB: varA})
>>> g
(A & (! A))
>>> is_sat(g)
False

A More Complex Example

Is there a value for each letter (between 1 and 9) so that H+E+L+L+O = W+O+R+L+D = 25?

from pysmt.shortcuts import Symbol, And, GE, LT, Plus, Equals, Int, get_model
from pysmt.typing import INT

hello = [Symbol(s, INT) for s in "hello"]
world = [Symbol(s, INT) for s in "world"]
letters = set(hello+world)
domains = And([And(GE(l, Int(1)),
                   LT(l, Int(10))) for l in letters])

sum_hello = Plus(hello) # n-ary operators can take lists
sum_world = Plus(world) # as arguments
problem = And(Equals(sum_hello, sum_world),
              Equals(sum_hello, Int(25)))
formula = And(domains, problem)

print("Serialization of the formula:")
print(formula)

model = get_model(formula)
if model:
  print(model)
else:
  print("No solution found")

Portfolio

Portfolio solving consists of running multiple solvers in parallel. pySMT provides a simple interface to perform portfolio solving using multiple solvers and multiple solver configurations.

from pysmt.shortcuts import Portfolio, Symbol, Not

x, y = Symbol("x"), Symbol("y")
f = x.Implies(y)

with Portfolio(["cvc4",
                "yices",
                ("msat", {"random_seed": 1}),
                ("msat", {"random_seed": 17}),
                ("msat", {"random_seed": 42})],
               logic="QF_UFLIRA",
               incremental=False,
               generate_models=False) as s:
  s.add_assertion(f)
  s.push()
  s.add_assertion(x)
  res = s.solve()
  v_y = s.get_value(y)
  print(v_y) # TRUE

  s.pop()
  s.add_assertion(Not(y))
  res = s.solve()
  v_x = s.get_value(x)
  print(v_x) # FALSE

Using other SMT-LIB Solvers

from pysmt.shortcuts import Symbol, get_env, Solver
from pysmt.logics import QF_UFLRA

name = "mathsat-smtlib" # Note: The API version is called 'msat'

# Path to the solver. The solver needs to take the smtlib file from
# stdin. This might require creating a tiny shell script to set the
# solver options.
path = ["/tmp/mathsat"]
logics = [QF_UFLRA,]    # List of the supported logics

# Add the solver to the environment
env = get_env()
env.factory.add_generic_solver(name, path, logics)

# The solver name of the SMT-LIB solver can be now used anywhere
# where pySMT would accept an API solver name
with Solver(name=name, logic="QF_UFLRA") as s:
  print(s.is_sat(Symbol("x"))) # True

Check out more examples in the examples/ directory and the documentation on ReadTheDocs

Supported Theories and Solvers

pySMT provides methods to define a formula in Linear Real Arithmetic (LRA), Real Difference Logic (RDL), Equalities and Uninterpreted Functions (EUF), Bit-Vectors (BV), Arrays (A), Strings (S) and their combinations. The following solvers are supported through native APIs:

• MathSAT (http://mathsat.fbk.eu/)
• Z3 (https://github.com/Z3Prover/z3/)
• CVC4 (http://cvc4.cs.nyu.edu/web/)
• Yices 2 (http://yices.csl.sri.com/)
• CUDD (http://vlsi.colorado.edu/~fabio/CUDD/)
• PicoSAT (http://fmv.jku.at/picosat/)
• Boolector (http://fmv.jku.at/boolector/)

Additionally, you can use any SMT-LIB 2 compliant solver.

PySMT assumes that the python bindings for the SMT Solver are installed and accessible from your PYTHONPATH.

pySMT works on both Python 3.5 and Python 2.7.

Installation

You can install the latest stable release of pySMT from PyPI:

# pip install pysmt

this will additionally install the pysmt-install command, that can be used to install the solvers: e.g.,

$ pysmt-install --check

will show you which solvers have been found in your PYTHONPATH. PySMT does not depend directly on any solver, but if you want to perform solving, you need to have at least one solver installed. This can be used by pySMT via its native API, or passing through an SMT-LIB file.

The script pysmt-install can be used to simplify the installation of the solvers:

$ pysmt-install --msat

will install MathSAT 5.

By default the solvers are downloaded, unpacked and built in your home directory in the .smt_solvers folder. Compiled libraries and actual solver packages are installed in the relevant site-packages directory (e.g. virtual environment's packages root or local user-site). pysmt-install has many options to customize its behavior. If you have multiple versions of python in your system, we recommend the following syntax to run pysmt-install: python -m pysmt install.

Note: This script does not install required dependencies for building the solver (e.g., make or gcc) and has been tested mainly on Linux Debian/Ubuntu systems. We suggest that you refer to the documentation of each solver to understand how to install it with its python bindings.

For Yices, picosat, and CUDD, we use external wrappers:

• yicespy (https://github.com/pysmt/yicespy)
• repycudd (https://github.com/pysmt/repycudd)
• pyPicoSAT (https://github.com/pysmt/pyPicoSAT)

For instruction on how to use any SMT-LIB complaint solver with pySMT see examples/generic_smtlib.py

For more information, refer to online documentation on ReadTheDocs

Solvers Support

The following table summarizes the features supported via pySMT for each of the available solvers.

Solver	pySMT name	Supported Theories	Quantifiers	Quantifier Elimination	Unsat Core	Interpolation
MathSAT	msat	UF, LIA, LRA, BV, AX	No	msat-fm, msat-lw	Yes	Yes
Z3	z3	UF, LIA, LRA, BV, AX, NRA, NIA	z3	z3	Yes	Yes
CVC4	cvc4	UF, LIA, LRA, BV, AX, S	Yes	No	No	No
Yices	yices	UF, LIA, LRA, BV	No	No	No	No
Boolector	btor	UF, BV, AX	No	No	No	No
SMT-Lib Interface	<custom>	UF, LIA, LRA, BV, AX	Yes	No	No	No
PicoSAT	picosat	[None]	No	[No]	No	No
BDD (CUDD)	bdd	[None]	Yes	bdd	No	No

License

pySMT is released under the APACHE 2.0 License.

For further questions, feel free to open an issue, or write to [email protected] (Browse the Archive).

If you use pySMT in your work, please consider citing:

@inproceedings{pysmt2015,
  title={PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms},
  author={Gario, Marco and Micheli, Andrea},
  booktitle={SMT Workshop 2015},
  year={2015}
}