Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-08-05 | fixed bug575 for bv models | lianah | |
2014-08-05 | Minor fix : do not drop instantiation patterns when merging quantifiers. | ajreynol | |
2014-08-04 | Some fixes to symmetry breaker (resolves bug 576). | Morgan Deters | |
2014-08-04 | Better support for resource-limiting when there aren't any actual conflicts. | Morgan Deters | |
2014-08-01 | Minor cleanup from previous commit. Better organization for how quantifiers ↵ | ajreynol | |
modules check (introduce QuantifiersEngine::QEffort). | |||
2014-07-31 | New module for generating candidate equality conjectures used in inductive ↵ | ajreynol | |
proofs. Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness. Refactoring of term database. QcfEngine now uses central data structure for term indexing. Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check). | |||
2014-07-26 | Minor bug fix for exhaustive instantiation in model_engine. | ajreynol | |
2014-07-25 | bug fix for pierre 0717 | Tianyi Liang | |
2014-07-25 | fix for regexp union rewriting | Tianyi Liang | |
2014-07-25 | patch for regular expression intersection caching | Tianyi Liang | |
2014-07-24 | merging... | Tianyi Liang | |
2014-07-24 | add delayed length lemmas | Tianyi Liang | |
2014-07-21 | initialization in model_engine | Kshitij Bansal | |
2014-07-19 | Minor fix for explanations for co-datatypes. Bug fix for explanations in ↵ | ajreynol | |
FMF for quantifiers over arrays. | |||
2014-07-12 | Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre ↵ | Morgan Deters | |
for the report. | |||
2014-07-11 | Spelling. | Morgan Deters | |
2014-07-11 | fix for windows build | Kshitij Bansal | |
2014-07-10 | Merge pull request #48 from kbansal/segfaultfix | Kshitij Bansal | |
Segfaultfix | |||
2014-07-10 | rm warning | Kshitij Bansal | |
2014-07-10 | membership cvc token changed to `IS_IN' to avoid conflict with IN used for let | Kshitij Bansal | |
2014-07-10 | Merge remote-tracking branch 'origin/master' into segfaultfix | Kshitij Bansal | |
2014-07-10 | friendlyparser: go back upto 2 words looking for match | Kshitij Bansal | |
2014-07-10 | reorganize friendlyparser, behavior unchanged | Kshitij Bansal | |
2014-07-09 | sets cvc parser | Kshitij Bansal | |
2014-07-09 | sets cvc printer | Kshitij Bansal | |
2014-07-04 | initialize variables | Kshitij Bansal | |
2014-07-03 | change lemma generation behavior | Kshitij Bansal | |
don't store lemmas in a pending queue, instead generate them right away doing with pending queue is tricky, needs rethinking to do it properly | |||
2014-07-01 | Update portfolio_util.cpp | Kshitij Bansal | |
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-07-01 | chat about thread creation | Kshitij Bansal | |
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 | 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-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 | 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 | 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 | |