Run $ contrib/new-theory fp
Populate the kinds file.
Skeleton implementations of the classes needed by the constant kinds.
Fix glaring syntax error.
Add the helper classes for parametric sorts.
Fix some of the compilation bugs.
A few more compilation fixes.
Create a derived class the data for each of the parameterized operators.
Fixes to get the code to compile with the new kinds.
Implement the rest of the type checking rules.
Separate some utility functions so that better error handling can be provided.
Implement floating-point theory rewriter and changes to makefiles to include the new files in the build.
Implement an SMT-LIB 2 parser and printer along with enough fixes to get it to work.
Move rounding functions into the parser proper rather than having variables for them.
Fix parts of parser and correct the typing rules for the "fp" operator.
Add rewrite rules for a few generic kinds (variables and equalities).
Fix a reference counting bug in the rewriter and add tracing and debugging.
Fix the typing rules for fp.to_real and fixes to tracing.
Improve the trace messages.
Fix the bug in the equality substitution by making sure that the rewrite of equalities works.