summaryrefslogtreecommitdiff
path: root/examples
AgeCommit message (Collapse)Author
2014-12-09Cleanup.Morgan Deters
2014-12-06Added string constant in java api example.Tianyi Liang
2014-12-06Added C++/Java api examples;Tianyi Liang
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.
2014-08-24fix type in sets_translateKshitij Bansal
2014-07-01Update copyrights.Morgan Deters
2014-06-30Use FS as the set-logic string for theory of setsKshitij Bansal
2014-06-25sets api exampleKshitij Bansal
2014-06-25rename subseteq to subset in smtlib, all kinds and smt operator names are ↵Kshitij Bansal
now consistent
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij Bansal
* SET_SINGLETON kind renamed to just SINGLETON * "setenum" smt2 opertor renamed to "singleton"[1] * "in" smt2 operator renamed to "member"[2] [1] It was anyhow accepting exactly one argument, so was bit misleading to call set enumerator. [2] The corresponding kind was called MEMBER, so this will also make them consistent. Only inconsistency now is for subset: kind is called SUBSET but operator is called "subseteq".
2014-06-19Fix make install-examples.Morgan Deters
2014-06-19basic fixes for sets translator, separate binariesKshitij Bansal
2014-06-19New translator features: expand define-funs and combine assertions.Morgan Deters
2014-06-08sets translate: a different translation using axiomsKshitij Bansal
todo: set logic correctly, split the code for two translators
2014-06-06sets translator: fix for dagsKshitij Bansal
2014-06-06rm warning from helloworld exampleKshitij Bansal
2014-06-06Sets translate, and other short fixesKshitij Bansal
- $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine
2014-06-05Add --default-dag-thresh to translator, build translator with other examples.Morgan Deters
2014-05-09Fix for example installation.Morgan Deters
2014-05-07Adding encoding of sha1 collision for the hashing exampleDejan Jovanovic
2014-05-02Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.Morgan Deters
2014-03-19Move the translator binary from src/main to examples, no longer built by ↵Morgan Deters
default.
2013-12-24Cleanup related to output language fix.Morgan Deters
2013-12-24Java datatype API fixups, datatype API examplesMorgan Deters
2013-12-13Another fix for clang.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27Incremental is now on by default when using from API, off for command-line ↵Morgan Deters
driver except in interactive mode.
2013-06-17Java streams example I forgot to add a long time agoMorgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
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
2012-12-01updated examplesMorgan Deters
2012-12-01added a new example for the combination of bit-vectors and arrays (includes ↵Liana Hadarean
model generation) and set the logic for the bitvector example
2012-12-01Polishing API examples.Tim King
2012-11-30all API examples now have java versions too; bitvectors gets built; also ↵Morgan Deters
updated old-style copyrights in the examples
2012-11-30Updating the combination.cpp example.Tim King
2012-11-30change detection/handling of output language more reasonably; fixes a ↵Morgan Deters
nagging bug Tim found in API examples (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-30added a simple API example example showing how to use the bit-vector theory. Liana Hadarean
2012-11-30Changes to SExpr to accept autoconversion from bool and const char*. Adding ↵Tim King
an example for combination.
2012-11-28Adding the helloworld.cpp example.Tim King
2012-11-27Adding an example to show how to use arithmetic.Tim King
2012-11-26some fixes to language bindings and function visibilityMorgan Deters
2012-10-22fix misleading comment in exampleMorgan Deters
2012-10-06* Some documentation about building compatibility and language bindingsMorgan Deters
* Better errors/warnings when SWIG isn't installed (resolves bug 373) * Allow compatibility bindings to be built when SWIG isn't available
2012-10-05Bug-related:Morgan Deters
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-03better documentation, allow examples to be installed, etcMorgan Deters
2012-09-28* fix compatibility library naming for SMT-LIBv1Morgan Deters
* change name of JNI library to "libcvc4jni", which works better with Java's System.loadLibrary(). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-16some fixes for language bindingsMorgan Deters
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback