summaryrefslogtreecommitdiff
path: root/contrib/theoryskel
AgeCommit message (Collapse)Author
2014-09-03check() optimizationKshitij Bansal
Details of testing here: http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
2014-03-31Travis-CI test for new-theory script, also related bugfixes.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing
2013-11-12Fix new-theory script for new, flattened build system.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-06-08Fix typos in alttheoryskelMorgan Deters
2013-04-23Theory "alternates" supportMorgan Deters
* This is a feature that Dejan and I want for the upcoming tutorial. It allows rapid prototyping of new decision procedure implementations (which we may choose to demonstrate), and a new --use-theory command-line option to select from different available implementations. It has no affect on the current set of theories, as no "alternates" are defined. * Also update the new-theory script, which was broken and incomplete.
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ↵Morgan Deters
\file tags corrected, copyright added to files that had it missing, etc. I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
2012-02-27fixes to new-theory script; resolves bug #307Morgan Deters
2012-02-13precision in theoryskelFrançois Bobot
2012-02-12separate new-theory components into a "theoryskel" directory so that new ↵Morgan Deters
files can be added to it without modifying the script.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback