Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-07-01 | reword NEWS | Morgan Deters | |
2014-07-01 | Merge pull request #44 from mdeters/prio-queue-updates | Morgan Deters | |
BinaryHeap unit test and some usability/build fixes for the data structu... | |||
2014-06-30 | Merge pull request #45 from mdeters/turn-off-strings-exp | Morgan Deters | |
Turn strings-exp off by default (for the release) | |||
2014-06-30 | Update NEWS | Kshitij Bansal | |
2014-06-30 | Merge pull request #47 from kbansal/sets | Kshitij Bansal | |
Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are: SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset* API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET (those marked with [*] have changed or been added, others are as earlier) In the set-logic string use FS to enable sets. A not-so-well-tested perl command for translating old benchmarks: perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; ' | |||
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-28 | Automatically make SMT options from command-line option names, warn when not ↵ | Morgan Deters | |
possible. | |||
2014-06-28 | Fix bug in datatypes options specification | Morgan Deters | |
2014-06-27 | Another fix for 32-bit (amends commit b825605). | Morgan Deters | |
2014-06-27 | Fix for bug543 | Clark Barrett | |
2014-06-27 | Updated run script for QF_ABV | Clark Barrett | |
2014-06-26 | Merge pull request #46 from mdeters/bug573 | Kshitij Bansal | |
Potential fix for bug 573. | |||
2014-06-26 | Fix for 32-bit (esp. win32 failing build). | Morgan Deters | |
2014-06-26 | Merge tag 'smtcomp2014-resubmission' | Morgan Deters | |
Conflicts: src/main/portfolio.cpp | |||
2014-06-26 | Potential fix for bug 573. | Morgan Deters | |
2014-06-26 | Ignore error result when an error is squelched via command verbosity. | Morgan Deters | |
2014-06-26 | Remove leftover debugging output. | Morgan Deters | |
2014-06-26 | Minor language bindings fixes. | Morgan Deters | |
2014-06-26 | Add missing function definition. | Morgan Deters | |
2014-06-25 | sets api example | Kshitij Bansal | |
2014-06-25 | Merge pull request #34 from mdeters/datatypes-kinds | Andrew Reynolds | |
Datatypes kinds documentation | |||
2014-06-25 | Merge pull request #37 from mdeters/quants-kinds | Andrew Reynolds | |
Quantifiers kinds documentation | |||
2014-06-25 | Merge pull request #38 from mdeters/uf-kinds | Andrew Reynolds | |
UF kinds documentation | |||
2014-06-25 | Turn strings-exp off by default (for the release) | Morgan Deters | |
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-25 | Merge pull request #43 from mdeters/threadstack | Kshitij Bansal | |
stack-size portfolio fix. boost 1.50 now required "The intended behavior is this. If Boost threading library is available and portfolio is requested, we do a try-link during configure that sees if we can set a thread attribute. If that compiles and links, we set a #define in cvc4autoconfig.h. There's a new option --thread-stack=N, with N given in megabytes. 0 is default for the platform (which can be based on ulimit I guess as I mentioned in an email). If --thread-stack=N is given to sequential CVC4, it's an error. If it's given to pcvc4 and N > 0 and there isn't support in that Boost version for it, it's an error." | |||
2014-06-25 | BinaryHeap unit test and some usability/build fixes for the data structure ↵ | Morgan Deters | |
itself. | |||
2014-06-25 | Fixing the previous bugfix.smtcomp2014-resubmission | Tim King | |
2014-06-25 | Merge branch 'master' of github.com:CVC3/CVC4 | Tim King | |
2014-06-25 | Fixing the previous bugfix. | Tim King | |
2014-06-25 | Stack-size portfolio fix. If using Boost 1.50, --thread-stack=MB is now ↵ | Morgan Deters | |
supported. | |||
2014-06-25 | Fix some #line annotations. | Morgan Deters | |
2014-06-25 | Don't allow libabc to load extensions at runtime. | Morgan Deters | |
2014-06-24 | stack-size portfolio fix. boost 1.50 now required | Morgan Deters | |
2014-06-24 | Alternative lazier heuristic for assertion rewriting. | Tim King | |
2014-06-24 | Alternative lazier heuristic for assertion rewriting. | Tim King | |
2014-06-24 | Fixing a soundness bug in arithmetic and a roubustness problem in rings. | Tim King | |
2014-06-24 | Fix header check for glpk.h. | Morgan Deters | |
2014-06-24 | Fixing a soundness bug in arithmetic and a roubustness problem in rings. | Tim King | |
2014-06-24 | Merge pull request #41 from mdeters/tianyi-merge | Tianyi Liang | |
Merge from Tianyi | |||
2014-06-24 | Squashed commit of the following: | Morgan Deters | |
* Fix a bug in intersection * merging... * add delayed length lemmas * PreRegisterTerm is changed. * Bug fix for string-opt2 * PreRegisterTerm is changed. * add delayed length lemmas * Bug fix for string-opt2 * PreRegisterTerm is changed. * Bug fix for string-opt2 * PreRegisterTerm is changed. * Bug fix for string-opt2 * PreRegisterTerm is changed. | |||
2014-06-23 | Fix header check for glpk.h. | Morgan Deters | |
2014-06-23 | Fatal error if --unconstrained-simp and --produce-models used together ↵ | Morgan Deters | |
(before it would just override the user and turn off models). | |||
2014-06-23 | Make language explicit in casc scripts | ajreynol | |
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". |