projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-06-26
yoni206
pow2 -- final changes (#6800)
commit
|
commitdiff
|
tree
2021-06-25
yoni206
pow2: Adding monotonicity lemma (#6793)
commit
|
commitdiff
|
tree
2021-06-24
Aina Niemetz
api: getRealValue: Fix printing of integer values....
commit
|
commitdiff
|
tree
2021-06-24
Mathias Preiner
cmake: Add new code coverage targets. (#6796)
commit
|
commitdiff
|
tree
2021-06-24
Andrew Reynolds
Fix linear arithmetic for duplicate lemmas in increment...
commit
|
commitdiff
|
tree
2021-06-24
Gereon Kremer
Add CoCoA implementation (#6733)
commit
|
commitdiff
|
tree
2021-06-23
Haniel Barbosa
[hol] Disable bound fmf when HOL (#6792)
commit
|
commitdiff
|
tree
2021-06-23
yoni206
pow2: more implementations (#6756)
commit
|
commitdiff
|
tree
2021-06-23
Haniel Barbosa
[regressions] Adding regression from #5371 (#6791)
commit
|
commitdiff
|
tree
2021-06-23
Haniel Barbosa
[proofs] [dot] Adding a counter for subproofs (#6735)
commit
|
commitdiff
|
tree
2021-06-23
Haniel Barbosa
[parser] [hol] Fix parser check for allowing functions...
commit
|
commitdiff
|
tree
2021-06-23
Aina Niemetz
docs: Add quickstart guide. (#6782)
commit
|
commitdiff
|
tree
2021-06-23
Aina Niemetz
FP: Remove sections guarded with undefined macro SYMFPU...
commit
|
commitdiff
|
tree
2021-06-23
Andres Noetzli
Remove `--tear-down-incremental` (#6745)
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Avoid full normalization of lambdas in getValue (#6787)
commit
|
commitdiff
|
tree
2021-06-22
yoni206
python api unit tests for Op (#6785)
commit
|
commitdiff
|
tree
2021-06-22
yoni206
modular bv2int: Stubs and some implementations (#6760)
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Minor simplification to equality engine notifications...
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Always check legal eliminations in quantified logics...
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Fix type enumeration for non first-class sorts in FMF...
commit
|
commitdiff
|
tree
2021-06-22
yoni206
Python api unit tests for Result (#6763)
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Fix cases of ITE within regular expressions (#6783)
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Set up fine grained equality notifications (#6734)
commit
|
commitdiff
|
tree
2021-06-21
Mathias Preiner
Update to CaDiCaL 1.4.1. (#6780)
commit
|
commitdiff
|
tree
2021-06-21
Aina Niemetz
docs: Split out and merge C++ class hierarchy. (#6781)
commit
|
commitdiff
|
tree
2021-06-21
Andres Noetzli
[Attributes] Remove parameter `context_dependent` ...
commit
|
commitdiff
|
tree
2021-06-21
Mathias Preiner
Fix model issues with --bitblast=eager. (#6753)
commit
|
commitdiff
|
tree
2021-06-21
mudathirmahgoub
Add Grammar.java to the java API (#6388)
commit
|
commitdiff
|
tree
2021-06-21
Mathias Preiner
Move cnfConversionTime statistic to CnfStream. (#6769)
commit
|
commitdiff
|
tree
2021-06-21
Mathias Preiner
Make CaDiCaL a required dependency. (#6761)
commit
|
commitdiff
|
tree
2021-06-21
Haniel Barbosa
[proof] Fix documentation of array rule (#6770)
commit
|
commitdiff
|
tree
2021-06-19
Ying Sheng
Adding python API test part 5 (#6743)
commit
|
commitdiff
|
tree
2021-06-19
Aina Niemetz
docs: Fix config to produce unique Sphinx section label...
commit
|
commitdiff
|
tree
2021-06-19
Andres Noetzli
[CI] Build with all available cores (#6768)
commit
|
commitdiff
|
tree
2021-06-19
Aina Niemetz
docs: Remove 'View page source' link in right corner...
commit
|
commitdiff
|
tree
2021-06-18
Mathias Preiner
Make CnfStream::toCNF iterative (#6757)
commit
|
commitdiff
|
tree
2021-06-18
Andres Noetzli
Remove obsolete libpoly patch (#6762)
commit
|
commitdiff
|
tree
2021-06-18
Andres Noetzli
Fix CaDiCaL build on Windows (#6764)
commit
|
commitdiff
|
tree
2021-06-18
Andres Noetzli
Fix build without libpoly (#6759)
commit
|
commitdiff
|
tree
2021-06-16
Aina Niemetz
Make symfpu a required dependency. (#6749)
commit
|
commitdiff
|
tree
2021-06-16
Andres Noetzli
Archive SMT-COMP 2021 run scripts (#6748)
commit
|
commitdiff
|
tree
2021-06-16
Gereon Kremer
Properly consider aliases in option handlers (#6683)
commit
|
commitdiff
|
tree
2021-06-15
Ouyancheng
[Optimization] Use Result in OptimizationResult (#6740)
commit
|
commitdiff
|
tree
2021-06-15
yoni206
pow2: adding a kind, inference rules, and some implemen...
commit
|
commitdiff
|
tree
2021-06-15
Gereon Kremer
Update to a more recent libpoly version. (#6730)
commit
|
commitdiff
|
tree
2021-06-15
Gereon Kremer
Add cocoalib (#6731)
commit
|
commitdiff
|
tree
2021-06-15
Gereon Kremer
Remove public option wrappers (#6716)
commit
|
commitdiff
|
tree
2021-06-15
Aina Niemetz
docs: Fix reference in sep logic reference. (#6747)
commit
|
commitdiff
|
tree
2021-06-15
Haniel Barbosa
CVC4 -> cvc5 in cpp API examples (#6746)
commit
|
commitdiff
|
tree
2021-06-15
Aina Niemetz
docs: Add references instead of links in theory referen...
commit
|
commitdiff
|
tree
2021-06-15
yoni206
An example for a quick start guide (#6686)
commit
|
commitdiff
|
tree
2021-06-14
Andres Noetzli
Final update to SMT-COMP 2021 options (#6739)
commit
|
commitdiff
|
tree
2021-06-13
Andrew Reynolds
Minor simplifications to LogicInfo (#6737)
commit
|
commitdiff
|
tree
2021-06-11
Haniel Barbosa
Better support for HOL parsing and set up (#6697)
commit
|
commitdiff
|
tree
2021-06-11
Gereon Kremer
Add skeleton for new Lazard evaluation (#6732)
commit
|
commitdiff
|
tree
2021-06-11
Andrew Reynolds
Remove support for lazy BV extended function reductions...
commit
|
commitdiff
|
tree
2021-06-10
Andrew Reynolds
Ensure bv2nat and int2bv are not rewritten when using...
commit
|
commitdiff
|
tree
2021-06-10
Mathias Preiner
smtcomp: Change some BV configs for SQ and INC track...
commit
|
commitdiff
|
tree
2021-06-09
Aina Niemetz
docs: Migrate sets and relations theory reference....
commit
|
commitdiff
|
tree
2021-06-09
Andres Noetzli
Make `--solve-int-as-bv=X` robust to rewriting (#6722)
commit
|
commitdiff
|
tree
2021-06-09
Andres Noetzli
Update CVC4 URLs/macros (#6666)
commit
|
commitdiff
|
tree
2021-06-09
Andres Noetzli
Reorder ITE rewrites (#6723)
commit
|
commitdiff
|
tree
2021-06-09
Gereon Kremer
Make squasing more robust (#6713)
commit
|
commitdiff
|
tree
2021-06-09
Andrew Reynolds
Integrate learned literal manager into preprocessing...
commit
|
commitdiff
|
tree
2021-06-09
Andrew Reynolds
Fixes related to printing tuples, define-fun commands...
commit
|
commitdiff
|
tree
2021-06-09
Gereon Kremer
Push complex check inside GetInstantiationsCommand...
commit
|
commitdiff
|
tree
2021-06-09
Andres Noetzli
Update options for SMT-COMP (#6704)
commit
|
commitdiff
|
tree
2021-06-09
Ouyancheng
[Optimization] support for push/pop (#6706)
commit
|
commitdiff
|
tree
2021-06-09
Haniel Barbosa
Removing spurious HO checks (#6707)
commit
|
commitdiff
|
tree
2021-06-09
Gereon Kremer
Require statistics for regression (#6714)
commit
|
commitdiff
|
tree
2021-06-09
Aina Niemetz
docs: Migrate separation logic theory reference. (...
commit
|
commitdiff
|
tree
2021-06-09
Andres Noetzli
docs: Fix `Kind` description (#6712)
commit
|
commitdiff
|
tree
2021-06-08
Andrew Reynolds
Fix for 2 dimensional dependent bounded quantifiers...
commit
|
commitdiff
|
tree
2021-06-08
Andrew Reynolds
Add learned literal manager utility (#6709)
commit
|
commitdiff
|
tree
2021-06-08
Gereon Kremer
Fix statistics option handler (#6703)
commit
|
commitdiff
|
tree
2021-06-08
Gereon Kremer
Make env hold a pointer to the original options to...
commit
|
commitdiff
|
tree
2021-06-08
Gereon Kremer
Remove `binary_name` option (#6693)
commit
|
commitdiff
|
tree
2021-06-08
Alex Ozdemir
Change output of getRealValue to a fraction. (#6692)
commit
|
commitdiff
|
tree
2021-06-08
Andrew Reynolds
Make TheoryUF compatible with central equality engine...
commit
|
commitdiff
|
tree
2021-06-08
Andrew Reynolds
Fix str.update reduction (#6696)
commit
|
commitdiff
|
tree
2021-06-07
Andrew Reynolds
(proof-new) Fix missing connection in trust substitutio...
commit
|
commitdiff
|
tree
2021-06-07
Gereon Kremer
Remove `Options::wasSetByUser()` (#6682)
commit
|
commitdiff
|
tree
2021-06-07
Andrew Reynolds
(proof-new) Lazy proof chain debug names (#6680)
commit
|
commitdiff
|
tree
2021-06-06
Gereon Kremer
Support public option modules (#6691)
commit
|
commitdiff
|
tree
2021-06-05
Andres Noetzli
Remove unwanted side effects in `SPLIT_EQ_STRIP_L`...
commit
|
commitdiff
|
tree
2021-06-04
Andrew Reynolds
Miscellaneous changes from central ee branch (#6687)
commit
|
commitdiff
|
tree
2021-06-04
yoni206
pow2: header file for pow2 solver (#6676)
commit
|
commitdiff
|
tree
2021-06-04
Mathias Preiner
bv: Enable bitblast solver by default. (#6660)
commit
|
commitdiff
|
tree
2021-06-04
Gereon Kremer
Add missing dereference (#6684)
commit
|
commitdiff
|
tree
2021-06-04
Andres Noetzli
Fix handling of start index in `str.indexof_re` (#6674)
commit
|
commitdiff
|
tree
2021-06-04
Gereon Kremer
Some cleanup in `mkoptions.py` (#6667)
commit
|
commitdiff
|
tree
2021-06-04
Aina Niemetz
docs: Migrate datatypes theory reference. (#6662)
commit
|
commitdiff
|
tree
2021-06-03
yoni206
Adding unit tests for the datatypes python API (#6658)
commit
|
commitdiff
|
tree
2021-06-03
Andrew Reynolds
Simplify automatic set-logic in smt2 parser (#6678)
commit
|
commitdiff
|
tree
2021-06-03
Andres Noetzli
[GitHub Actions] Make caching of dependencies depend...
commit
|
commitdiff
|
tree
2021-06-03
yoni206
Renaming pow2 to p2 in regression tests (#6675)
commit
|
commitdiff
|
tree
2021-06-02
Andres Noetzli
Remove references to `bv-div-zero-const` in docs (...
commit
|
commitdiff
|
tree
2021-06-02
Andrew Reynolds
Fixes for printing define-fun-rec (#6673)
commit
|
commitdiff
|
tree
2021-06-02
Andres Noetzli
Remove option to ignore negative memberships (#6665)
commit
|
commitdiff
|
tree
2021-06-02
yoni206
Adding getters to the python API and testing them ...
commit
|
commitdiff
|
tree
next