Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-06-30 | Use FS as the set-logic string for theory of sets | Kshitij Bansal | |
2014-06-29 | sets: "insert" operator | Kshitij Bansal | |
new™! support for (insert (X (Set X)) (Set X) :right-associative) from the finte sets theory prosoal. e.g., (insert 1 2 3 4 (singleton 5)) | |||
2014-06-25 | sets api example | Kshitij Bansal | |
2014-06-25 | fix sets eager lemmas | Kshitij Bansal | |
2014-06-25 | cosmetic | Kshitij Bansal | |
2014-06-25 | mv default care graph function inside the theory implementation | Kshitij Bansal | |
2014-06-25 | make emptyset construction with no arguments private | Kshitij Bansal | |
2014-06-25 | rename subseteq to subset in smtlib, all kinds and smt operator names are ↵ | Kshitij Bansal | |
now consistent | |||
2014-06-22 | Renaming of SMT2 operator names, kinds for set theory | Kshitij 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-21 | Sets kinds documentation | Morgan Deters | |
2014-06-21 | fixed build failure | lianah | |
2014-06-20 | Implement RecordProperties::mkGroundTerm(). Resolves bug #546. | Morgan Deters | |
2014-06-19 | fixed merge conflict | lianah | |
2014-06-19 | added model generation to eager bit-blasting and turned abc off by default | lianah | |
2014-06-19 | update to abc install instructions | lianah | |
2014-06-19 | Better --segv-spin messages. | Morgan Deters | |
2014-06-19 | Fix make install-examples. | Morgan Deters | |
2014-06-19 | Proper escaping in option documentation. | Morgan Deters | |
2014-06-19 | Version of the run script that works with trace executor; waiting on ↵ | Morgan Deters | |
StarExec infrastructure for testing. | |||
2014-06-19 | forgot to add the test with fix | Kshitij Bansal | |
according to bug report, fix was in 6267f3 | |||
2014-06-19 | basic fixes for sets translator, separate binaries | Kshitij Bansal | |
2014-06-19 | Options script fix. | Morgan Deters | |
2014-06-19 | Fix for mac readline. | Morgan Deters | |
2014-06-19 | Better error for invalid concrete syntax of sorts with too many parens, like ↵ | Morgan Deters | |
(Int). Thanks to Dan Liew for the report. | |||
2014-06-19 | Fix GLPK builds: correct access specifier on cut classes. | Morgan Deters | |
2014-06-19 | Java bindings fixes. | Morgan Deters | |
2014-06-19 | Minor Doxygen fixes. | Morgan Deters | |
2014-06-19 | disable unate lemmas when using incremental mode | Kshitij Bansal | |
2014-06-19 | Fix for pre-C++11 is_sorted(). | Morgan Deters | |
2014-06-19 | More minor code cleanup. | Morgan Deters | |
2014-06-19 | No more dependence on libstdc++ or PBDS stuff: remove build stuff that ↵ | Morgan Deters | |
supported it. | |||
2014-06-19 | New translator features: expand define-funs and combine assertions. | Morgan Deters | |
2014-06-19 | Code cleanup. | Morgan Deters | |
2014-06-19 | Documentation clean-ups. | Morgan Deters | |
2014-06-19 | Another fix for the CASC stuff. | Morgan Deters | |
2014-06-19 | Final preparations for arithmetic for building with libc++. | Morgan Deters | |
2014-06-19 | Fix for new CASC features, fixes Java builds. | Morgan Deters | |
2014-06-19 | Some reversions of recent commits re: portfolio failure. | Morgan Deters | |
* Partial reversion of b8e28a7, do it a different way. * Revert "Test portfolio with --no-wait-to-join." This reverts commit 8b56004ee8bf6c34aaf045bec12bf0e4401a044c. | |||
2014-06-19 | This commit adds a priority queue implementation. This is to avoid ↵ | Tim King | |
compilation troubles with libc++. | |||
2014-06-19 | Test portfolio with --no-wait-to-join. | Morgan Deters | |
2014-06-19 | For casc : print models of functions rewritten by sort inference. | ajreynol | |
2014-06-19 | Fix rewriter typo. | Morgan Deters | |
2014-06-19 | Clean up glpk detection a little, fix a detection bug. | Morgan Deters | |
2014-06-19 | fix typo | Morgan Deters | |
2014-06-19 | More application-track fixes for use with trace executor. | Morgan Deters | |
2014-06-19 | Versioning preparation. | Morgan Deters | |
2014-06-19 | Some fixes for tear-down-incremental and "success" output. | Morgan Deters | |
2014-06-19 | Disallow context-dependent copy/assignment. | Morgan Deters | |
2014-06-19 | Fix compile errors with some versions of GCC. | Morgan Deters | |
2014-06-19 | Clean up some compiler warnings on 32-bit. | Morgan Deters | |