git.libre-soc.org Git - cvc5.git/search

2014-09-29	ajreynol	Add option for aggressive model filtering in conjecture...	commit \| commitdiff \| tree
2014-09-25	ajreynol	Fair datatype enumeration.	commit \| commitdiff \| tree
2014-09-24	ajreynol	Fix infinite loop in datatypes enumerator. Minor work...	commit \| commitdiff \| tree
2014-09-24	ajreynol	Refactor option for uf+cardinality constraints solver.	commit \| commitdiff \| tree
2014-09-24	ajreynol	Partial support for codatatype models.	commit \| commitdiff \| tree
2014-09-23	ajreynol	Support :no-pattern.	commit \| commitdiff \| tree
2014-09-23	ajreynol	Do not throw error when codatatype is not well-founded...	commit \| commitdiff \| tree
2014-09-17	ajreynol	Fix soundness bug for quantifier macros involving Int...	commit \| commitdiff \| tree
2014-09-17	ajreynol	Refactor entailment filtering for conjecture generator...	commit \| commitdiff \| tree
2014-09-17	ajreynol	More refactoring of conjecture generation. Term generation...	commit \| commitdiff \| tree
2014-09-16	ajreynol	Bug fix variable triggers with --inst-max-level : use...	commit \| commitdiff \| tree
2014-09-16	ajreynol	Refactoring of conjecture generator. Determine subgoals...	commit \| commitdiff \| tree
2014-09-09	ajreynol	Fix bug for variable term triggers within multi-triggers.	commit \| commitdiff \| tree
2014-09-08	ajreynol	Accept user-provided triggers with variable terms....	commit \| commitdiff \| tree
2014-09-03	ajreynol	Implement and enable --dt-var-exp-quant, cleanup trace...	commit \| commitdiff \| tree
2014-09-03	ajreynol	Work on conjecture generator : do not generalize subterms...	commit \| commitdiff \| tree
2014-08-29	ajreynol	Set instantiation level on skolemized bodies of quantifiers...	commit \| commitdiff \| tree
2014-08-29	ajreynol	Do not use pure theory terms as single triggers. Minor...	commit \| commitdiff \| tree
2014-08-27	ajreynol	Fix assertion in rep_set.cpp, avoid full check in datatypes...	commit \| commitdiff \| tree
2014-08-26	ajreynol	Bug fixes for --purify-triggers, --dt-force-assignment.	commit \| commitdiff \| tree
2014-08-25	ajreynol	New option --purify-triggers. Refactoring of InstMatchGener...	commit \| commitdiff \| tree
2014-08-21	ajreynol	Avoid doing work in quantifiers engine when no quantifiers...	commit \| commitdiff \| tree
2014-08-20	ajreynol	Fix --inst-max-level for strategies that use arbitrary...	commit \| commitdiff \| tree
2014-08-20	ajreynol	Update bv proof signature and example, after discussions...	commit \| commitdiff \| tree
2014-08-20	ajreynol	Add option for inductive strengthening based on well...	commit \| commitdiff \| tree
2014-08-18	ajreynol	Add support for quantifier-specific instantiation levels...	commit \| commitdiff \| tree
2014-08-08	ajreynol	Add draft of BV proof signature (incomplete) and example...	commit \| commitdiff \| tree
2014-08-05	ajreynol	Minor fix : do not drop instantiation patterns when...	commit \| commitdiff \| tree
2014-08-01	ajreynol	Minor cleanup from previous commit. Better organization...	commit \| commitdiff \| tree
2014-07-31	ajreynol	New module for generating candidate equality conjectures...	commit \| commitdiff \| tree
2014-07-25	ajreynol	Minor bug fix for exhaustive instantiation in model_engine.	commit \| commitdiff \| tree
2014-07-19	ajreynol	Minor fix for explanations for co-datatypes. Bug fix...	commit \| commitdiff \| tree
2014-06-23	ajreynol	Make language explicit in casc scripts	commit \| commitdiff \| tree
2014-06-17	ajreynol	For casc : print models of functions rewritten by sort...	commit \| commitdiff \| tree
2014-06-16	ajreynol	More proof support for CASC : include skolemization	commit \| commitdiff \| tree
2014-06-14	ajreynol	Fix for fmf with large finite cardinalities.	commit \| commitdiff \| tree
2014-06-13	ajreynol	Fix handling of ALIA.	commit \| commitdiff \| tree
2014-06-11	ajreynol	Update SMTCOMP script to handle all quantified logics.	commit \| commitdiff \| tree
2014-06-03	ajreynol	Support E-matching/QCF for Set operators.	commit \| commitdiff \| tree
2014-05-30	ajreynol	Change SMT COMP script to use external timeouts.	commit \| commitdiff \| tree
2014-05-30	ajreynol	Improve --dt-stc-ind for multi-variable datatype properties.	commit \| commitdiff \| tree
2014-05-30	ajreynol	Fixes for --inst-max-level	commit \| commitdiff \| tree
2014-05-28	ajreynol	Minor changes to script. Disable cbqi sat.	commit \| commitdiff \| tree
2014-05-13	ajreynol	Add lazy strategy for bounded integers to avoid non...	commit \| commitdiff \| tree
2014-05-08	ajreynol	Major simplifications to macros module.	commit \| commitdiff \| tree
2014-05-02	ajreynol	Fix assertion from previous commit.	commit \| commitdiff \| tree
2014-05-02	ajreynol	More minor optimizations for datatypes.	commit \| commitdiff \| tree
2014-05-01	ajreynol	Minor optimizations to datatypes, revert to checkClash...	commit \| commitdiff \| tree
2014-04-29	ajreynol	Significantly improve performance for producing datatypes...	commit \| commitdiff \| tree
2014-04-28	ajreynol	Optimizations for datatypes: check for clashes modulo...	commit \| commitdiff \| tree
2014-04-24	ajreynol	Avoid assigning constructor terms to 1-constructor...	commit \| commitdiff \| tree

RSS Atom