summaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2013-05-06Change SMT-EVAL run-script to use Tim's best QF_LRA command-line parametersMorgan 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.
2013-04-03Pre-release versioningMorgan Deters
2013-04-03Some final minor changes before cutting 1.1.Morgan Deters
* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression
2013-04-02Fix get-authors script to not extract email addresses, canonicalize names, ↵Morgan Deters
add .mailmap
2013-04-01Adjust release Makefile rules, new run scriptMorgan Deters
2013-04-01Merging some cleanup work:Morgan Deters
* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-03-19Remove PropositionalQuery class and all CUDD-related build stuff (and ↵Morgan Deters
references)
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-04fixed files with DOS newlines; fixed contrib/ scripts to use gitMorgan Deters
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2013-01-24Add win32 support (merge from mdeters/win32, with some cleanup).Morgan Deters
2013-01-22update ANTLR URLs (antlr.org -> antlr3.org)Morgan Deters
2012-12-01Cutting release 1.0.1.0Morgan Deters
2012-12-01fix cut-release sanity checksMorgan Deters
2012-11-30minor fix to release scriptMorgan Deters
2012-10-24Includes many fixes to build system for Solaris (thanks Tim!), and alsoMorgan Deters
just in general, and some documentation adjustments.
2012-10-23The contrib/get-antlr-3.4 script:Tim King
- Has no outdated reference to /usr/share/java/stringtemplate.jar (as discussed on the mailing list). - Attempts to determine if the computer is 64 or 32 bit and configure antlr appropriately. - Warns the user about it's guess. - Tells the user how to correct an incorrect guess.
2012-10-22add bug 425 models regression; fix mac-build execute permissionMorgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
(rather than SAT context) * Enable part of CVC3 system test (resolves bug 375) * Fix infinite recursion in beta reduction code (resolves bug 417) * Some model-building assertions have been added * Other minor changes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-06* Clean up some options documentationMorgan Deters
* Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-03updates to contrib scripts to match docsMorgan Deters
2012-10-03better documentation, allow examples to be installed, etcMorgan Deters
2012-09-26Fix a handful of things for Mac, and Java bindings.Morgan Deters
Also add a "mac-build" script that sets up prerequisites for Mac.
2012-09-26bug #398 test (bug was resolved last night), and a script to download all ↵Morgan Deters
bug attachments from bugzilla and put them in the tree
2012-07-31Options merge. This commit:Morgan Deters
1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options) 2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace. 3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..) The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options: * to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp. * to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser(). * ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options) *** this point is important. If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file *** Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true). Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double). For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h). Benefits of the new options system include: 1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed). 2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.) 3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc. 4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.) 5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose I've taken lots of care not to break anything. Hopefully, I've succeeded in that.
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-06-18qf_lra strategysmtcomp2012Morgan Deters
2012-06-18another qf_lra strategy updateMorgan Deters
2012-06-18unnecessary ^ in regular expression; warning produced on smt-execMorgan Deters
2012-06-18QF_LRA strategy in run script, now final (?) for smt-comp 2012Morgan Deters
2012-06-18final sources (?) for competitionMorgan Deters
2012-06-16updated build script for smt-comp submissionMorgan Deters
2012-06-13Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow ↵Morgan Deters
condition when reading from stdin. This should completely resolve bug #319. However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track). So I updated the submission script and competition build so that * a competition build with antlr-inlining is built for the main and parallel tracks * a competition build without antlr-inlining is built for the application track Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works). For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds. Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree. Closing bug #319.
2012-03-24a cute script to make a video of development from the svn logsDejan Jovanović
2012-02-27fixes to new-theory script; resolves bug #307Morgan Deters
2012-02-13precision in theoryskelFrançois Bobot
2012-02-12copyright year updated to 2012Morgan Deters
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.
2012-02-11ensure using bash for new-theory scriptMorgan Deters
2012-02-10script to ease creating a new theory from scratch (will go along with new ↵Morgan Deters
reference documentation)
2011-11-01Improvements to header installation on user machines. Internally, we canMorgan Deters
still write, for example: #include "expr/node.h" but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever), have such #includes rewritten automatically to: #include <cvc4/expr/node.h>
2011-09-30interfaces fixes and cleanups...and examples of each interface!Morgan Deters
2011-09-16fix serious issue with copyright-updating scriptMorgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-05-05luby sequence generator; can use to plot MiniSat's restart sequenceMorgan Deters
2011-04-23* reviewed BooleanSimplification, added documentation & unit testMorgan Deters
* work around a lexer ambiguity in CVC grammar * add support for tracing antlr parser/lexer * add parsing support for more language features * initial parameterized types parsing work to support Andy's work
2011-03-30Add Valuation::getSatValue() so that theories can access the currentMorgan Deters
(propositional) assignment for theory atoms. Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list. This implementation leads to some compiler warnings in production builds, but these will be corrected in coming days. There appears to be a small speedup in the parser as a result of this fix: http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5 Cleaned up a few CD Boolean attribute things. Various small fixes to coding guidelines / test coverage. This commit: * Resolves bug 252 (tracing not disabled in production builds) * Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())
2011-03-15Merge from cudd branch. This mostly just adds support for linkingMorgan Deters
against cudd libraries, the propositional_query class (in util/), which uses cudd if it's available (and otherwise answers UNKNOWN for all queries), and the arith theory support for it (currently disabled per Tim's request, so he can clean it up). Other changes include: * contrib/debug-keys - script to print all used keys under Debug(), Trace() * test/regress/run_regression - minor fix (don't export a variable) * configure.ac - replace a comment removed by dejan's google perf commit * some minor copyright/documentation updates, and minor changes to source text to make 'clang --analyze' happy.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback