summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2014-07-01Merge pull request #44 from mdeters/prio-queue-updatesMorgan Deters
BinaryHeap unit test and some usability/build fixes for the data structu...
2014-06-30Merge pull request #45 from mdeters/turn-off-strings-expMorgan Deters
Turn strings-exp off by default (for the release)
2014-06-30Merge pull request #47 from kbansal/setsKshitij 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-30Use FS as the set-logic string for theory of setsKshitij Bansal
2014-06-29sets: "insert" operatorKshitij 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-28Automatically make SMT options from command-line option names, warn when not ↵Morgan Deters
possible.
2014-06-28Fix bug in datatypes options specificationMorgan Deters
2014-06-27Another fix for 32-bit (amends commit b825605).Morgan Deters
2014-06-27Fix for bug543Clark Barrett
2014-06-26Merge pull request #46 from mdeters/bug573Kshitij Bansal
Potential fix for bug 573.
2014-06-26Fix for 32-bit (esp. win32 failing build).Morgan Deters
2014-06-26Potential fix for bug 573.Morgan Deters
2014-06-26Ignore error result when an error is squelched via command verbosity.Morgan Deters
2014-06-26Remove leftover debugging output.Morgan Deters
2014-06-26Minor language bindings fixes.Morgan Deters
2014-06-26Add missing function definition.Morgan Deters
2014-06-25Merge pull request #34 from mdeters/datatypes-kindsAndrew Reynolds
Datatypes kinds documentation
2014-06-25Merge pull request #37 from mdeters/quants-kindsAndrew Reynolds
Quantifiers kinds documentation
2014-06-25Merge pull request #38 from mdeters/uf-kindsAndrew Reynolds
UF kinds documentation
2014-06-25Turn strings-exp off by default (for the release)Morgan Deters
2014-06-25fix sets eager lemmasKshitij Bansal
2014-06-25cosmeticKshitij Bansal
2014-06-25mv default care graph function inside the theory implementationKshitij Bansal
2014-06-25make emptyset construction with no arguments privateKshitij Bansal
2014-06-25rename subseteq to subset in smtlib, all kinds and smt operator names are ↵Kshitij Bansal
now consistent
2014-06-25Merge pull request #43 from mdeters/threadstackKshitij 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-25BinaryHeap unit test and some usability/build fixes for the data structure ↵Morgan Deters
itself.
2014-06-25Merge branch 'master' of github.com:CVC3/CVC4Tim King
2014-06-25Fixing the previous bugfix.Tim King
2014-06-25Stack-size portfolio fix. If using Boost 1.50, --thread-stack=MB is now ↵Morgan Deters
supported.
2014-06-25Fix some #line annotations.Morgan Deters
2014-06-24Alternative lazier heuristic for assertion rewriting.Tim King
2014-06-24Fixing a soundness bug in arithmetic and a roubustness problem in rings.Tim King
2014-06-24Squashed 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-23Fatal error if --unconstrained-simp and --produce-models used together ↵Morgan Deters
(before it would just override the user and turn off models).
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-22Output 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-22Minor cleanup stuff.Morgan Deters
2014-06-22Re-enable UNTERMINATED_QUOTED_SYMBOL rules.Morgan Deters
2014-06-22Merge tag 'smtcomp2014-application'Morgan Deters
Conflicts: contrib/run-script-smtcomp2014-application src/main/driver_unified.cpp
2014-06-22QuitCommand needs "success" output for trace executor. :-(smtcomp2014-applicationMorgan Deters
2014-06-22Final fixes for smtcomp2014-application.Morgan Deters
2014-06-22Merge pull request #39 from mdeters/bv-warningslianah
Fix compiler warnings in BV-related code (unused vars mostly).
2014-06-22Merge pull request #35 from mdeters/bv-kindslianah
Bit-vector kinds documentation
2014-06-21Fix compiler warnings (mostly unused variables).Morgan Deters
2014-06-21API documentation improvements.Morgan Deters
2014-06-21Fix compiler warnings in BV-related code (unused vars mostly).Morgan Deters
2014-06-21Fix to the compatibility library (this does fix the build).Morgan Deters
2014-06-21Fix compat-Java layer, should fix build.Morgan Deters
2014-06-21Sets kinds documentationMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback