summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2014-08-05fixed bug575 for bv modelslianah
2014-08-05Minor fix : do not drop instantiation patterns when merging quantifiers.ajreynol
2014-08-04Some fixes to symmetry breaker (resolves bug 576).Morgan Deters
2014-08-04Better support for resource-limiting when there aren't any actual conflicts.Morgan Deters
2014-08-01Minor cleanup from previous commit. Better organization for how quantifiers ↵ajreynol
modules check (introduce QuantifiersEngine::QEffort).
2014-07-31New 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-26Minor bug fix for exhaustive instantiation in model_engine.ajreynol
2014-07-25bug fix for pierre 0717Tianyi Liang
2014-07-25fix for regexp union rewritingTianyi Liang
2014-07-25patch for regular expression intersection cachingTianyi Liang
2014-07-24merging...Tianyi Liang
2014-07-24add delayed length lemmasTianyi Liang
2014-07-21initialization in model_engineKshitij Bansal
2014-07-19Minor fix for explanations for co-datatypes. Bug fix for explanations in ↵ajreynol
FMF for quantifiers over arrays.
2014-07-12Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre ↵Morgan Deters
for the report.
2014-07-11Spelling.Morgan Deters
2014-07-11fix for windows buildKshitij Bansal
2014-07-10Merge pull request #48 from kbansal/segfaultfixKshitij Bansal
Segfaultfix
2014-07-10rm warningKshitij Bansal
2014-07-10membership cvc token changed to `IS_IN' to avoid conflict with IN used for letKshitij Bansal
2014-07-10Merge remote-tracking branch 'origin/master' into segfaultfixKshitij Bansal
2014-07-10friendlyparser: go back upto 2 words looking for matchKshitij Bansal
2014-07-10reorganize friendlyparser, behavior unchangedKshitij Bansal
2014-07-09sets cvc parserKshitij Bansal
2014-07-09sets cvc printerKshitij Bansal
2014-07-04initialize variablesKshitij Bansal
2014-07-03change lemma generation behaviorKshitij 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-01Update portfolio_util.cppKshitij Bansal
2014-07-01Update copyrights.Morgan Deters
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-07-01chat about thread creationKshitij Bansal
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback