Some specs and Z3::Sort#to_s etc.

Author: taw

.rspec

@@ -0,0 +1,2 @@
+--color
+--require spec_helper

README.md

@@ -10,6 +10,8 @@ The rest of `Z3` is high level API, but the interface is extremely unstable at t
 
 You can use most Ruby operators to construct ASTs, but use `~ | &` instead of `! || &&` for boolean operators.
 
+As for API internals, attributes starting with `_` are FFI internals you shouldn't touch, other attributes are generally legitimate Ruby objects.
+
 ### Requirements
 
 To use it, you'll need to install `z3`. On OSX that would be:

lib/z3/core.rb

@@ -18,6 +18,7 @@ module Z3::Core
   attach_function :Z3_mk_bool_sort, [ctx_pointer], sort_pointer
   attach_function :Z3_mk_int_sort, [ctx_pointer], sort_pointer
   attach_function :Z3_mk_real_sort, [ctx_pointer], sort_pointer
+  attach_function :Z3_sort_to_string, [ctx_pointer, sort_pointer], :string
   # Solver API
   attach_function :Z3_mk_solver, [ctx_pointer], solver_pointer
   attach_function :Z3_solver_push, [ctx_pointer, solver_pointer], :void

lib/z3/sort.rb

@@ -1,11 +1,23 @@
 class Z3::Sort
-  attr_reader :_sort
+  attr_reader :_sort, :ctx
   # Do not use .new directly
-  def initialize(_sort, ctx:Z3::Context.main)
+  def initialize(_sort, ctx: Z3::Context.main)
     @ctx = ctx
     @_sort = _sort
   end
 
+  def ==(other)
+    other.is_a?(Z3::Sort) and @_sort == other._sort
+  end
+
+  def to_s
+    Z3::Core.Z3_sort_to_string(@ctx._context, @_sort)
+  end
+
+  def inspect
+    "Z3::Sort<#{to_s}>"
+  end
+
   class << self
     def bool(ctx: Z3::Context.main)
       Z3::Sort.new(Z3::Core::Z3_mk_bool_sort(ctx._context), ctx: ctx)

spec/sort_spec.rb

@@ -0,0 +1,22 @@
+describe Z3::Sort do
+  it "create Bool sort" do
+    expect(Z3::Sort.bool.to_s).to eq("Bool")
+    expect(Z3::Sort.bool.inspect).to eq("Z3::Sort<Bool>")
+  end
+
+  it "create Int sort" do
+    expect(Z3::Sort.int.to_s).to eq("Int")
+    expect(Z3::Sort.int.inspect).to eq("Z3::Sort<Int>")
+  end
+
+  it "create Real sort" do
+    expect(Z3::Sort.real.to_s).to eq("Real")
+    expect(Z3::Sort.real.inspect).to eq("Z3::Sort<Real>")
+  end
+
+  it "supports ==" do
+    expect(Z3::Sort.bool).to eq(Z3::Sort.bool)
+    expect(Z3::Sort.int).to eq(Z3::Sort.int)
+    expect(Z3::Sort.bool).to_not eq(Z3::Sort.int)
+  end
+end

spec/spec_helper.rb

@@ -0,0 +1,98 @@
+require_relative "../lib/z3"
+
+# This file was generated by the `rspec --init` command. Conventionally, all
+# specs live under a `spec` directory, which RSpec adds to the `$LOAD_PATH`.
+# The generated `.rspec` file contains `--require spec_helper` which will cause
+# this file to always be loaded, without a need to explicitly require it in any
+# files.
+#
+# Given that it is always loaded, you are encouraged to keep this file as
+# light-weight as possible. Requiring heavyweight dependencies from this file
+# will add to the boot time of your test suite on EVERY test run, even for an
+# individual file that may not need all of that loaded. Instead, consider making
+# a separate helper file that requires the additional dependencies and performs
+# the additional setup, and require it from the spec files that actually need
+# it.
+#
+# The `.rspec` file also contains a few flags that are not defaults but that
+# users commonly want.
+#
+# See http://rubydoc.info/gems/rspec-core/RSpec/Core/Configuration
+RSpec.configure do |config|
+  # rspec-expectations config goes here. You can use an alternate
+  # assertion/expectation library such as wrong or the stdlib/minitest
+  # assertions if you prefer.
+  config.expect_with :rspec do |expectations|
+    # This option will default to `true` in RSpec 4. It makes the `description`
+    # and `failure_message` of custom matchers include text for helper methods
+    # defined using `chain`, e.g.:
+    #     be_bigger_than(2).and_smaller_than(4).description
+    #     # => "be bigger than 2 and smaller than 4"
+    # ...rather than:
+    #     # => "be bigger than 2"
+    expectations.include_chain_clauses_in_custom_matcher_descriptions = true
+  end
+
+  # rspec-mocks config goes here. You can use an alternate test double
+  # library (such as bogus or mocha) by changing the `mock_with` option here.
+  config.mock_with :rspec do |mocks|
+    # Prevents you from mocking or stubbing a method that does not exist on
+    # a real object. This is generally recommended, and will default to
+    # `true` in RSpec 4.
+    mocks.verify_partial_doubles = true
+  end
+
+# The settings below are suggested to provide a good initial experience
+# with RSpec, but feel free to customize to your heart's content.
+=begin
+  # These two settings work together to allow you to limit a spec run
+  # to individual examples or groups you care about by tagging them with
+  # `:focus` metadata. When nothing is tagged with `:focus`, all examples
+  # get run.
+  config.filter_run :focus
+  config.run_all_when_everything_filtered = true
+
+  # Allows RSpec to persist some state between runs in order to support
+  # the `--only-failures` and `--next-failure` CLI options. We recommend
+  # you configure your source control system to ignore this file.
+  config.example_status_persistence_file_path = "spec/examples.txt"
+
+  # Limits the available syntax to the non-monkey patched syntax that is
+  # recommended. For more details, see:
+  #   - http://myronmars.to/n/dev-blog/2012/06/rspecs-new-expectation-syntax
+  #   - http://www.teaisaweso.me/blog/2013/05/27/rspecs-new-message-expectation-syntax/
+  #   - http://myronmars.to/n/dev-blog/2014/05/notable-changes-in-rspec-3#new__config_option_to_disable_rspeccore_monkey_patching
+  config.disable_monkey_patching!
+
+  # This setting enables warnings. It's recommended, but in some cases may
+  # be too noisy due to issues in dependencies.
+  config.warnings = true
+
+  # Many RSpec users commonly either run the entire suite or an individual
+  # file, and it's useful to allow more verbose output when running an
+  # individual spec file.
+  if config.files_to_run.one?
+    # Use the documentation formatter for detailed output,
+    # unless a formatter has already been configured
+    # (e.g. via a command-line flag).
+    config.default_formatter = 'doc'
+  end
+
+  # Print the 10 slowest examples and example groups at the
+  # end of the spec run, to help surface which specs are running
+  # particularly slow.
+  config.profile_examples = 10
+
+  # Run specs in random order to surface order dependencies. If you find an
+  # order dependency and want to debug it, you can fix the order by providing
+  # the seed, which is printed after each run.
+  #     --seed 1234
+  config.order = :random
+
+  # Seed global randomization in this process using the `--seed` CLI option.
+  # Setting this allows you to use `--seed` to deterministically reproduce
+  # test failures related to randomization by passing the same `--seed` value
+  # as the one that triggered the failure.
+  Kernel.srand config.seed
+=end
+end