projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Add option for aggressive model filtering in conjecture generator (enumerate ground...
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