projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2014-10-02
Kshitij Bansal
fix getModelValue(<non-preregistered term>)
commit
|
commitdiff
|
tree
2014-10-01
ajreynol
Option for more aggressive merging in UEE.
commit
|
commitdiff
|
tree
2014-09-30
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-09-30
Morgan Deters
Fix improper #inclusion of private header outside library.
commit
|
commitdiff
|
tree
2014-09-30
Morgan Deters
Fix a command-replay bug in tear-down-incremental mode...
commit
|
commitdiff
|
tree
2014-09-30
Morgan Deters
Proofs- and cores-related segfault fixes (mainly a...
commit
|
commitdiff
|
tree
2014-09-29
ajreynol
Add option for aggressive model filtering in conjecture...
commit
|
commitdiff
|
tree
2014-09-27
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-09-27
Morgan Deters
Fix infinite loop in --bitblast-aig/--bv-aig-simp options.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Fix bv options doc.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Fix some configuration-related oddness.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Clarify some licensing-related things.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Finer-grained resource-limiting in quantifiers.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Fix AIG bitblaster for unsat cores.
commit
|
commitdiff
|
tree
2014-09-25
Morgan Deters
fix unit test for new fair datatype enumeration
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-18
Morgan Deters
Resource spending support in theories (and especially...
commit
|
commitdiff
|
tree
2014-09-18
Kshitij Bansal
cvc4terminate infinite loop fix
commit
|
commitdiff
|
tree
2014-09-18
Kshitij Bansal
cvc4terminate infinite loop fix
commit
|
commitdiff
|
tree
2014-09-17
Kshitij Bansal
Merge branch '1.4.x' while ignoring commit 8d5eb49.
commit
|
commitdiff
|
tree
2014-09-17
Kshitij Bansal
Fix fix. There are no unsat cores in 1.4
commit
|
commitdiff
|
tree
2014-09-17
Kshitij Bansal
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-09-17
Kshitij Bansal
Fix (push) and (pop). Thanks to Christoph Sticksel...
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 genera...
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 subgoal...
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-04
Kshitij Bansal
Update command_executor_portfolio.cpp
commit
|
commitdiff
|
tree
2014-09-03
Kshitij Bansal
Merge remote-tracking branch 'origin/master'
commit
|
commitdiff
|
tree
2014-09-03
Kshitij Bansal
check() optimization
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 subter...
commit
|
commitdiff
|
tree
2014-08-29
ajreynol
Set instantiation level on skolemized bodies of quantif...
commit
|
commitdiff
|
tree
2014-08-29
ajreynol
Do not use pure theory terms as single triggers. Minor...
commit
|
commitdiff
|
tree
2014-08-28
lianah
fixing bug580 caused by bad bv inequality explanation
commit
|
commitdiff
|
tree
2014-08-28
lianah
fixing bug580 caused by bad bv inequality explanation
commit
|
commitdiff
|
tree
2014-08-27
ajreynol
Fix assertion in rep_set.cpp, avoid full check in datat...
commit
|
commitdiff
|
tree
2014-08-26
Morgan Deters
Improved SMT-LIBv2 language support for unsat cores.
commit
|
commitdiff
|
tree
2014-08-26
ajreynol
Bug fixes for --purify-triggers, --dt-force-assignment.
commit
|
commitdiff
|
tree
2014-08-25
Morgan Deters
Fix build rule.
commit
|
commitdiff
|
tree
2014-08-25
Morgan Deters
Fix Win32 builds.
commit
|
commitdiff
|
tree
2014-08-25
ajreynol
New option --purify-triggers. Refactoring of InstMatch...
commit
|
commitdiff
|
tree
2014-08-24
Kshitij Bansal
remove some debugging code
commit
|
commitdiff
|
tree
2014-08-24
Kshitij Bansal
improvements to sets sharing
commit
|
commitdiff
|
tree
2014-08-24
Kshitij Bansal
fix option alias (minor)
commit
|
commitdiff
|
tree
2014-08-24
Kshitij Bansal
fix type in sets_translate
commit
|
commitdiff
|
tree
2014-08-23
Morgan Deters
Unsat core printing.
commit
|
commitdiff
|
tree
2014-08-23
Morgan Deters
Some fixes for dump- and get-unsat-core.
commit
|
commitdiff
|
tree
2014-08-23
Morgan Deters
Quieter finish to build.
commit
|
commitdiff
|
tree
2014-08-23
Morgan Deters
Unit test fix.
commit
|
commitdiff
|
tree
2014-08-22
Morgan Deters
One small thing forgotten in core commit.
commit
|
commitdiff
|
tree
2014-08-22
Morgan Deters
Java-side interface improvements for unsat cores.
commit
|
commitdiff
|
tree
2014-08-22
Morgan Deters
Unsat core infrastruture and API (SMT-LIB compliance...
commit
|
commitdiff
|
tree
2014-08-22
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-08-22
Morgan Deters
Fix incorrectly-labeled test.
commit
|
commitdiff
|
tree
2014-08-22
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-08-22
Morgan Deters
Fix operator-printing issue in SMT2.
commit
|
commitdiff
|
tree
2014-08-22
Morgan Deters
Fix SMT1 parser :extrasorts/:extrapreds.
commit
|
commitdiff
|
tree
2014-08-21
ajreynol
Avoid doing work in quantifiers engine when no quantifi...
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 discussion...
commit
|
commitdiff
|
tree
2014-08-20
ajreynol
Add option for inductive strengthening based on well...
commit
|
commitdiff
|
tree
2014-08-19
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-08-19
Morgan Deters
Produce error for bad indexed function names in SMT...
commit
|
commitdiff
|
tree
2014-08-19
lianah
Making getEqualityStatus more powerful for bit-vector...
commit
|
commitdiff
|
tree
2014-08-18
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-08-18
Morgan Deters
Revert a8e0ce67 and add test case (resolves bug #578).
commit
|
commitdiff
|
tree
2014-08-18
ajreynol
Add support for quantifier-specific instantiation level...
commit
|
commitdiff
|
tree
2014-08-15
Kshitij Bansal
Update smt_engine.cpp
commit
|
commitdiff
|
tree
2014-08-13
Morgan Deters
To avoid confusion, permit --enable-staticbinary as...
commit
|
commitdiff
|
tree
2014-08-09
Morgan Deters
Fix a build issue for some configurations, thanks Tianyi.
commit
|
commitdiff
|
tree
2014-08-08
ajreynol
Add draft of BV proof signature (incomplete) and exampl...
commit
|
commitdiff
|
tree
2014-08-07
Morgan Deters
Another build fix.
commit
|
commitdiff
|
tree
2014-08-07
Morgan Deters
Fix win32 build.
commit
|
commitdiff
|
tree
2014-08-06
Morgan Deters
Fix double-linking issue (I think) by simplifying build...
commit
|
commitdiff
|
tree
2014-08-06
Morgan Deters
First crack at fixing double-linking issues in build...
commit
|
commitdiff
|
tree
2014-08-05
Morgan Deters
Fix for manpages.
commit
|
commitdiff
|
tree
2014-08-05
lianah
fixed bug575 for bv models
commit
|
commitdiff
|
tree
2014-08-05
lianah
fixed bug575 for bv models
commit
|
commitdiff
|
tree
2014-08-05
ajreynol
Minor fix : do not drop instantiation patterns when...
commit
|
commitdiff
|
tree
2014-08-04
Morgan Deters
Some fixes to symmetry breaker (resolves bug 576).
commit
|
commitdiff
|
tree
2014-08-04
Morgan Deters
Some fixes to symmetry breaker (resolves bug 576).
commit
|
commitdiff
|
tree
2014-08-04
Morgan Deters
Better support for resource-limiting when there aren...
commit
|
commitdiff
|
tree
2014-08-01
ajreynol
Minor cleanup from previous commit. Better organizatio...
commit
|
commitdiff
|
tree
2014-07-31
ajreynol
New module for generating candidate equality conjecture...
commit
|
commitdiff
|
tree
2014-07-25
ajreynol
Minor bug fix for exhaustive instantiation in model_engine.
commit
|
commitdiff
|
tree
2014-07-25
Tianyi Liang
bug fix for pierre 0717
commit
|
commitdiff
|
tree
2014-07-25
Tianyi Liang
fix for regexp union rewriting
commit
|
commitdiff
|
tree
2014-07-25
Tianyi Liang
patch for regular expression intersection caching
commit
|
commitdiff
|
tree
2014-07-24
Tianyi Liang
merging...
commit
|
commitdiff
|
tree
2014-07-24
Tianyi Liang
add delayed length lemmas
commit
|
commitdiff
|
tree
next