class Z3::Printer
Public Instance Methods
format(a)
click to toggle source
# File lib/z3/printer.rb, line 3 def format(a) format_ast(a).to_s end
Private Instance Methods
format_app(a)
click to toggle source
# File lib/z3/printer.rb, line 40 def format_app(a) if LowLevel::is_algebraic_number(a) PrintedExpr.new(LowLevel::get_numeral_decimal_string(a, 10)) elsif LowLevel::is_as_array(a) decl = FuncDecl.new( LowLevel::get_as_array_func_decl(a) ) PrintedExpr.new(decl.sexpr.gsub(/k!\d+/, "k!")) elsif a.func_decl.name == "fp.numeral" and a.sort.is_a?(FloatSort) # This API chaged in Z3 4.6 s = a.significand_string e = "%+d" % a.exponent_string(false).to_i PrintedExpr.new("#{s}B#{e}") else decl = a.func_decl name = decl.name args = a.arguments.map{|x| format_ast(x)} return PrintedExpr.new(name, false) if args.size == 0 # Special case common Bitvec operators case name when "rotate_left", "rotate_right", "zero_extend", "sign_extend" if args.size == 1 n = Z3::LowLevel.get_decl_int_parameter(a.func_decl, 0) return PrintedExpr.new("#{name}(#{args[0]}, #{n})", true) end when "bvxor", "bvand", "bvor", "bvadd", "bvsub" if args.size == 2 pretty_name = {"bvxor" => "^", "bvand" => "&", "bvor" => "|", "bvadd" => "+", "bvsub" => "-"}[name] return PrintedExpr.new("#{args[0].enforce_parentheses} #{pretty_name} #{args[1].enforce_parentheses}", true) end when "bvnot" if args.size == 1 return PrintedExpr.new("~#{args[0].enforce_parentheses}") end when "bvneg" if args.size == 1 return PrintedExpr.new("-#{args[0].enforce_parentheses}") end when "extract" if args.size == 1 u = Z3::LowLevel.get_decl_int_parameter(a.func_decl, 0) v = Z3::LowLevel.get_decl_int_parameter(a.func_decl, 1) return PrintedExpr.new("#{name}(#{args[0]}, #{u}, #{v})", true) end end if name !~ /[a-z0-9]/ if args.size == 2 return PrintedExpr.new("#{args[0].enforce_parentheses} #{name} #{args[1].enforce_parentheses}", true) elsif args.size == 1 return PrintedExpr.new("#{name}#{args[0].enforce_parentheses}", true) end end PrintedExpr.new("#{name}(#{args.join(", ")})") end end
format_ast(a)
click to toggle source
# File lib/z3/printer.rb, line 27 def format_ast(a) case a.ast_kind when :numeral PrintedExpr.new(Z3::LowLevel.get_numeral_string(a)) when :app format_app(a) when :var, :quantifier, :func_decl, :unknown PrintedExpr.new(a.sexpr) else raise Z3::Exception, "Unknown AST kind #{a.ast_kind}" end end