Age | Commit message (Collapse) | Author | |
---|---|---|---|
2015-01-14 | sygus input language and benchmark | Morgan Deters | |
2015-01-13 | Fix a memory issue in ResourceManager on 32-bit (resolves bug #606). | Morgan Deters | |
2015-01-11 | adjusted to both v2.0 and v2.5 string literals | Tianyi Liang | |
2015-01-08 | switch ascii encoding to unsigned char | Tianyi Liang | |
2014-12-22 | Do not collapse wrongly applied selectors for non-well-founded codatatypes ↵ | ajreynol | |
pre-model. | |||
2014-12-11 | Minor fixes to language bindings. (Resolves #607.) | Morgan Deters | |
2014-12-06 | Added 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-12-03 | Fix UnsatCore in language bindings. | Morgan Deters | |
2014-12-03 | Floating point infrastructure. | Martin Brain | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-11-22 | added number of resource units used as a stat | lianah | |
2014-11-19 | Distribute UnsafeInterruptException interface file for SWIG. | Morgan Deters | |
2014-11-18 | All Minisat solve calls now return lbool (fixes bug 599) | lianah | |
2014-11-17 | Resource-limiting work. | Liana Hadarean | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-11-10 | Do not eliminate variables only occurring in patterns. Minor improvements ↵ | ajreynol | |
to sort inference. Remove unused code. | |||
2014-11-07 | Properly distinguish which EQC to assign values in datatypes, use ↵ | ajreynol | |
assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure. | |||
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters | |
* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.) | |||
2014-10-21 | Fixed bug 589 | Tianyi Liang | |
2014-10-02 | Merge branch '1.4.x'. | Morgan Deters | |
2014-10-02 | Fix for an array-of-record model generation assert-fail (assert was too strong). | Morgan Deters | |
2014-09-26 | Merge branch '1.4.x' | Morgan Deters | |
2014-09-26 | Clarify some licensing-related things. | Morgan Deters | |
2014-09-23 | Do not throw error when codatatype is not well-founded. Add option for ↵ | ajreynol | |
disabling codatatype reasoning. Minor cleanup. | |||
2014-08-26 | Improved SMT-LIBv2 language support for unsat cores. | Morgan Deters | |
2014-08-24 | remove some debugging code | Kshitij Bansal | |
(it can be brought back from version control, if needed) | |||
2014-08-24 | improvements to sets sharing | Kshitij Bansal | |
* Add TheorySets::getEqualityStatus(TNode, TNode) * Add TheorySets::getModelValue(TNode) | |||
2014-08-23 | Unsat core printing. | Morgan Deters | |
2014-08-22 | Java-side interface improvements for unsat cores. | Morgan Deters | |
2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters | |
2014-07-01 | Update copyrights. | 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 #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-26 | Add missing function definition. | Morgan Deters | |
2014-06-25 | make emptyset construction with no arguments private | Kshitij Bansal | |
2014-06-25 | BinaryHeap unit test and some usability/build fixes for the data structure ↵ | Morgan Deters | |
itself. | |||
2014-06-22 | Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3: | Morgan Deters | |
1. no decimals used for rational literals 2. queries/check-sats wrapped with PUSH/POP | |||
2014-06-22 | Minor cleanup stuff. | Morgan Deters | |
2014-06-21 | Add some missing functions in configuration and compat library. | Morgan Deters | |
2014-06-19 | Java bindings fixes. | Morgan Deters | |
2014-06-19 | More minor code cleanup. | Morgan Deters | |
2014-06-19 | Code cleanup. | Morgan Deters | |
2014-06-19 | This commit adds a priority queue implementation. This is to avoid ↵ | Tim King | |
compilation troubles with libc++. | |||
2014-06-19 | For casc : print models of functions rewritten by sort inference. | ajreynol | |
2014-06-19 | dos2unix-convert some sources. | Morgan Deters | |
2014-06-11 | Some clean-up, post bv-merge. | Morgan Deters | |
Add abc to build id and fix static building. Add abc to --show-config output and Configuration class API. Add ability to select abc source path. Fix arch_flags for abc. | |||
2014-06-10 | Merging CAV14 paper bit-vector work. | lianah | |
2014-05-27 | fix timespec printing | Kshitij Bansal | |
sorry prvs fix added some unrelated code | |||
2014-05-27 | Revert "timespec printing bug" | Kshitij Bansal | |
This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6. | |||
2014-05-27 | timespec printing bug | Kshitij Bansal | |
2014-05-24 | Some cleanup, fix warnings raised by Debian packager. | Morgan Deters | |
2014-05-20 | Fix compiler warning (missing virtual dtor) | Morgan Deters | |