Basic case splitting: Added a Split class and an instance of Split to the blackboard.
Split examines the blackboard and (randomly) selects a potential term to split on, with depth
bounded by default_split. The main module then calls Split and explores each branch, discarding the
results if a contradiction is not found.
Add a constant default seed. May change performance wildly.
Function terms now store references to their defining object, to allow them to share canonizers.
Adding recent bugfixes to the backtracking branch.
Added exponential module file.
start on minimum module
Bugfix: learning equalities in the polyhedron module has been corrected.
Bugfix: learning equalities in the polyhedron multiplicative module has been corrected.
Bugfix: corrected behavior in the FM mult module, when comparisons like 2>=1 are derived.
Generalized the axiom unification routine: if trigger terms are manually defined, can sometimes match axioms where not all variables are in functions. Todo: Needs a better interface.
Removed leftover debug code.
Fixed bug in assert_disequality.
Fixed bugs in function module and polyhedron mult module.
Added a preprocessing step to multiplicative routines that naively tries to cancel nonzero variables.
minimum module working
Refactored minimum_module. Interval classes are now in Geometry, search routines are now in Blackboard.
Fixed bug in canonizing MulPairs with integer exponents represented by Fractions.
Changed function module to maintain a set of axioms rather than a list. Added some functionality to exponential module.
Minor mistake in implies.
moved modules to a new modules directory