2014-12-28 |
ajreynol | Disable prenex by default when using fmf bound int...
|
commit | commitdiff | tree |
2014-12-22 |
ajreynol | Do not collapse wrongly applied selectors for non-well...
|
commit | commitdiff | tree |
2014-12-21 |
ajreynol | Add misc trigger options.
|
commit | commitdiff | tree |
2014-12-12 |
ajreynol | Add cvc parsing support for cardinality constraints...
|
commit | commitdiff | tree |
2014-12-11 |
ajreynol | Option to enable/disable cyclicity check in datatypes.
|
commit | commitdiff | tree |
2014-12-06 |
ajreynol | Fix dt.size care graph.
|
commit | commitdiff | tree |
2014-11-28 |
ajreynol | Synchronize conjecture generation with E-matching....
|
commit | commitdiff | tree |
2014-11-25 |
ajreynol | Fix bug in --term-db-mode=relevant with variable triggers...
|
commit | commitdiff | tree |
2014-11-21 |
ajreynol | Throw error when pattern is not list of terms.
|
commit | commitdiff | tree |
2014-11-21 |
ajreynol | Change default option to --inst-when=full-last-call...
|
commit | commitdiff | tree |
2014-11-20 |
ajreynol | Disable constants sharing in eq engine, disable hack...
|
commit | commitdiff | tree |
2014-11-18 |
ajreynol | Compute model basis only for fmf. Add another co-datatype...
|
commit | commitdiff | tree |
2014-11-18 |
ajreynol | Add local theory extensions instantiation strategy...
|
commit | commitdiff | tree |
2014-11-16 |
ajreynol | Add term db mode. Minor changes to quantifiers rewriter...
|
commit | commitdiff | tree |
2014-11-14 |
ajreynol | Be lazier to consider EQC in UF+cardinality solver...
|
commit | commitdiff | tree |
2014-11-13 |
ajreynol | Remove two obsolete versions of MBQI.
|
commit | commitdiff | tree |
2014-11-13 |
ajreynol | More preparation for filtering relevant terms in TermDb.
|
commit | commitdiff | tree |
2014-11-11 |
ajreynol | Work on synchronizing decision=justification and E...
|
commit | commitdiff | tree |
2014-11-10 |
ajreynol | Do not eliminate variables only occurring in patterns...
|
commit | commitdiff | tree |
2014-11-09 |
ajreynol | Fix dt shared terms issue, reenable regression.
|
commit | commitdiff | tree |
2014-11-08 |
ajreynol | Fix bug with incremental+datatypes. Minor cleanup...
|
commit | commitdiff | tree |
2014-11-07 |
ajreynol | Enable --quant-cf by default. Fix bug in qcf for mixed...
|
commit | commitdiff | tree |
2014-11-07 |
ajreynol | Properly distinguish which EQC to assign values in...
|
commit | commitdiff | tree |
2014-11-06 |
ajreynol | Minor fix for getInstCons
|
commit | commitdiff | tree |
2014-11-06 |
ajreynol | Reenable regression. Add (for now, disabled) changes...
|
commit | commitdiff | tree |
2014-11-05 |
ajreynol | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.
|
commit | commitdiff | tree |
2014-11-05 |
ajreynol | More work on datatypes theory combination: fix bug...
|
commit | commitdiff | tree |
2014-11-01 |
ajreynol | Fix cegqi for synthesis without syntax.
|
commit | commitdiff | tree |
2014-11-01 |
ajreynol | Simplify which lemmas to communicate in dt.
|
commit | commitdiff | tree |
2014-11-01 |
ajreynol | Fix bug 592: introduce skolem for dt instantiate lemma...
|
commit | commitdiff | tree |
2014-11-01 |
ajreynol | Fix some mistakes in datatypes theory combination,...
|
commit | commitdiff | tree |
2014-10-31 |
ajreynol | Do not allow duplication of function definitions. ...
|
commit | commitdiff | tree |
2014-10-28 |
ajreynol | Preprocessing step for finding finite runs of well...
|
commit | commitdiff | tree |
2014-10-28 |
ajreynol | Initial infrastructure for function definition quantifiers...
|
commit | commitdiff | tree |
2014-10-28 |
ajreynol | Improve stats in conjecture generator, minor cleanup.
|
commit | commitdiff | tree |
2014-10-25 |
ajreynol | Minor fix for --user-pat=resort
|
commit | commitdiff | tree |
2014-10-24 |
ajreynol | Add --user-pat=resort. Minor cleanup of options.
|
commit | commitdiff | tree |
2014-10-20 |
ajreynol | Minor cleanup in datatypes.
|
commit | commitdiff | tree |
2014-10-18 |
ajreynol | Fix assertion.
|
commit | commitdiff | tree |
2014-10-18 |
ajreynol | Add dt lemma: zero size implies nullary constructor.
|
commit | commitdiff | tree |
2014-10-18 |
ajreynol | Fix for bounded integers when incremental, fixes bug...
|
commit | commitdiff | tree |
2014-10-16 |
ajreynol | Make --user-pat=trust default. Fix a few warnings...
|
commit | commitdiff | tree |
2014-10-16 |
ajreynol | Use n-ary splits instead of binary splits in theory...
|
commit | commitdiff | tree |
2014-10-16 |
ajreynol | Add dt.size to datatypes theory. Add option for fairness...
|
commit | commitdiff | tree |
2014-10-13 |
ajreynol | CEGQI uses model. Enforce fairness in CEGQI natively.
|
commit | commitdiff | tree |
2014-10-13 |
ajreynol | Model building into quantifiers engine. Simplify axiom...
|
commit | commitdiff | tree |
2014-10-13 |
ajreynol | Refactor model builder from model engine to quant engine...
|
commit | commitdiff | tree |
2014-10-10 |
ajreynol | Initial draft of CEGQI.
|
commit | commitdiff | tree |
2014-10-10 |
ajreynol | Add owner map to better manage QuantifiersModules....
|
commit | commitdiff | tree |
2014-10-09 |
ajreynol | Refactor quantifier prenex option. By default, do...
|
commit | commitdiff | tree |
2014-10-07 |
ajreynol | Cache for getInstance, thanks to Johannes Kanig for...
|
commit | commitdiff | tree |
2014-10-07 |
ajreynol | Refactor quantifiers attributes.
|
commit | commitdiff | tree |
2014-10-01 |
ajreynol | Option for more aggressive merging in UEE.
|
commit | commitdiff | tree |
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-19 |
ajreynol | For casc : print models of functions rewritten by sort...
|
commit | commitdiff | tree |
2014-06-19 |
ajreynol | More proof support for CASC : include skolemization
|
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 |
next |