summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2014-10-10Add owner map to better manage QuantifiersModules. Initial infrastructure fo...ajreynol
2014-10-09Refactor quantifier prenex option. By default, do not pull quantifiers with ...ajreynol
2014-10-08Cache for getInstance, thanks to Johannes Kanig for the report. Do not mkRep...ajreynol
2014-10-07Refactor quantifiers attributes.ajreynol
2014-10-01Option for more aggressive merging in UEE.ajreynol
2014-09-29Add option for aggressive model filtering in conjecture generator (enumerate ...ajreynol
2014-09-24Fix infinite loop in datatypes enumerator. Minor work on conjecture generator.ajreynol
2014-09-24Refactor option for uf+cardinality constraints solver.ajreynol
2014-09-23Support :no-pattern.ajreynol
2014-09-23Do not throw error when codatatype is not well-founded. Add option for disab...ajreynol
2014-09-17Fix soundness bug for quantifier macros involving Int/Real.ajreynol
2014-09-17Refactor entailment filtering for conjecture generator. Other minor cleanup.ajreynol
2014-09-17More refactoring of conjecture generation. Term generation into own class.ajreynol
2014-09-16Bug fix variable triggers with --inst-max-level : use term in EQC with minima...ajreynol
2014-09-16Refactoring of conjecture generator. Determine subgoals are non-canonical ba...ajreynol
2014-09-09Fix bug for variable term triggers within multi-triggers.ajreynol
2014-09-09Accept user-provided triggers with variable terms. Flush lemmas before quant...ajreynol
2014-09-03Merge remote-tracking branch 'origin/master'Kshitij Bansal
2014-09-03check() optimizationKshitij Bansal
2014-09-03Implement and enable --dt-var-exp-quant, cleanup trace messages, minor change...ajreynol
2014-09-03Work on conjecture generator : do not generalize subterms with concrete value...ajreynol
2014-08-29Set instantiation level on skolemized bodies of quantifiers. Rename inst-lev...ajreynol
2014-08-29Do not use pure theory terms as single triggers. Minor cleanup.ajreynol
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-20Add option for inductive strengthening based on well-founded induction for in...ajreynol
2014-08-18Add support for quantifier-specific instantiation levels. Add option for set...ajreynol
2014-08-05Minor fix : do not drop instantiation patterns when merging quantifiers.ajreynol
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-21initialization in model_engineKshitij Bansal
2014-07-19Minor fix for explanations for co-datatypes. Bug fix for explanations in FMF...ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-06-30Merge pull request #47 from kbansal/setsKshitij Bansal
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij Bansal
2014-06-20Quantifiers kinds documentationMorgan Deters
2014-06-19dos2unix-convert some sources.Morgan Deters
2014-06-19Minor fixes, spelling etc.Morgan Deters
2014-06-19More proof support for CASC : include skolemizationajreynol
2014-06-03Support E-matching/QCF for Set operators.ajreynol
2014-05-30Improve --dt-stc-ind for multi-variable datatype properties.ajreynol
2014-05-28Minor changes to script. Disable cbqi sat.ajreynol
2014-05-25Improve quantifier instantiation: always use original terms when matching (wa...Andrew Reynolds
2014-05-23Fix bug in E-matching Real/Int terms.Andrew Reynolds
2014-05-14Finish --dump-instantiations option. Update scripts.Andrew Reynolds
2014-05-13Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ...ajreynol
2014-05-12Minor updates/fix to --cbqi-recurseAndrew Reynolds
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback