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