blanchet [Fri, 22 Oct 2010 15:02:27 +0200] rev 40071
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet [Fri, 22 Oct 2010 14:47:43 +0200] rev 40070
replaced references with proper record that's threaded through
blanchet [Fri, 22 Oct 2010 14:10:32 +0200] rev 40069
fixed signature of "is_smt_solver_installed";
renaming
blanchet [Fri, 22 Oct 2010 13:57:54 +0200] rev 40068
renamed modules
blanchet [Fri, 22 Oct 2010 13:54:51 +0200] rev 40067
renamed files
blanchet [Fri, 22 Oct 2010 13:49:44 +0200] rev 40066
took out "smt"/"remote_smt" from default ATPs until they are properly implemented
blanchet [Fri, 22 Oct 2010 13:48:21 +0200] rev 40065
remove more needless code ("run_smt_solvers");
tuning
blanchet [Fri, 22 Oct 2010 12:15:31 +0200] rev 40064
got rid of duplicate functionality ("run_smt_solver_somehow");
added minimization command to SMT solver message
blanchet [Fri, 22 Oct 2010 11:58:33 +0200] rev 40063
bring ATPs and SMT solvers more in line with each other
blanchet [Fri, 22 Oct 2010 11:11:34 +0200] rev 40062
make Sledgehammer minimizer fully work with SMT