summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2014-08-29Do not use pure theory terms as single triggers. Minor cleanup.ajreynol
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-27Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.ajreynol
2014-08-26Bug fixes for --purify-triggers, --dt-force-assignment.ajreynol
2014-08-25New option --purify-triggers. Refactoring of InstMatchGenerator.ajreynol
2014-08-24remove some debugging codeKshitij Bansal
2014-08-24improvements to sets sharingKshitij Bansal
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-21Avoid doing work in quantifiers engine when no quantifiers are asserted.ajreynol
2014-08-21Fix --inst-max-level for strategies that use arbitrary representative terms.ajreynol
2014-08-20Add option for inductive strengthening based on well-founded induction for in...ajreynol
2014-08-18Making getEqualityStatus more powerful for bit-vector theory.lianah
2014-08-18Add support for quantifier-specific instantiation levels. Add option for set...ajreynol
2014-08-05fixed bug575 for bv modelslianah
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-04Some fixes to symmetry breaker (resolves bug 576).Morgan Deters
2014-08-01Minor cleanup from previous commit. Better organization for how quantifiers ...ajreynol
2014-07-31New module for generating candidate equality conjectures used in inductive pr...ajreynol
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 FMF...ajreynol
2014-07-12Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre f...Morgan Deters
2014-07-11Spelling.Morgan Deters
2014-07-10Merge remote-tracking branch 'origin/master' into segfaultfixKshitij Bansal
2014-07-04initialize variablesKshitij Bansal
2014-07-03change lemma generation behaviorKshitij Bansal
2014-07-01Update copyrights.Morgan Deters
2014-06-30Merge pull request #47 from kbansal/setsKshitij Bansal
2014-06-30Use FS as the set-logic string for theory of setsKshitij Bansal
2014-06-29sets: "insert" operatorKshitij Bansal
2014-06-28Fix bug in datatypes options specificationMorgan Deters
2014-06-27Fix for bug543Clark Barrett
2014-06-25Merge pull request #34 from mdeters/datatypes-kindsAndrew Reynolds
2014-06-25Merge pull request #37 from mdeters/quants-kindsAndrew Reynolds
2014-06-25Merge pull request #38 from mdeters/uf-kindsAndrew Reynolds
2014-06-25fix sets eager lemmasKshitij Bansal
2014-06-25mv default care graph function inside the theory implementationKshitij Bansal
2014-06-25Fixing the previous bugfix.smtcomp2014-resubmissionTim King
2014-06-25Fixing the previous bugfix.Tim King
2014-06-24Alternative lazier heuristic for assertion rewriting.Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback