projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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
2021-06-02
Aina Niemetz
Remove redundant logic ALL_SUPPORTED. (#6664)
commit
|
commitdiff
|
tree
2021-06-02
yoni206
Move `toPythonObj` tests to the new API unit test direc...
commit
|
commitdiff
|
tree
2021-06-02
Gereon Kremer
Use proper variable name (#6670)
commit
|
commitdiff
|
tree
2021-06-02
Andrew Reynolds
Fix unsat core proofs (#6655)
commit
|
commitdiff
|
tree
2021-06-02
Andres Noetzli
Make `STRINGS_CTN_DECOMPOSE` an explicit conflict ...
commit
|
commitdiff
|
tree
2021-06-02
Gereon Kremer
Remove `Options::operator[]` (#6649)
commit
|
commitdiff
|
tree
2021-06-02
Gereon Kremer
Move public wrapper functions out of options class...
commit
|
commitdiff
|
tree
2021-06-02
Gereon Kremer
Fix issues with double negation in circuit propagator...
commit
|
commitdiff
|
tree
2021-06-02
Gereon Kremer
Fix issues when poly is disabled (#6668)
commit
|
commitdiff
|
tree
2021-06-02
Gereon Kremer
Make `Options::assign()` specializations free functions...
commit
|
commitdiff
|
tree
2021-06-02
Gereon Kremer
Do manual squash cleanup for docs (#6646)
commit
|
commitdiff
|
tree
2021-06-02
Aina Niemetz
docs: Migrate input languages page. (#6659)
commit
|
commitdiff
|
tree
2021-06-02
Aina Niemetz
docs: Restructure index page, fix style issue. (#6657)
commit
|
commitdiff
|
tree
2021-06-01
yoni206
Some additions to the datatypes python API (#6640)
commit
|
commitdiff
|
tree
2021-06-01
Andrew Reynolds
Use top-level substitutions in ITE simp (#6651)
commit
|
commitdiff
|
tree
2021-06-01
Andrew Reynolds
Disable timeout regressions (#6650)
commit
|
commitdiff
|
tree
2021-06-01
yoni206
FP value support in python API (#6644)
commit
|
commitdiff
|
tree
2021-05-31
Gereon Kremer
Remove Options::ref() (#6647)
commit
|
commitdiff
|
tree
2021-05-31
Andres Noetzli
Remove invalid options from run scripts (#6645)
commit
|
commitdiff
|
tree
2021-05-31
yoni206
Update `toPythonObj` to use new getters -- part 1 ...
commit
|
commitdiff
|
tree
2021-05-31
Andres Noetzli
Compute model values for nested sequences in order...
commit
|
commitdiff
|
tree
2021-05-29
Gereon Kremer
Remove `Options::set()` method (#6556)
commit
|
commitdiff
|
tree
2021-05-28
Ouyancheng
(Optimization) remove popObjective, add resetObjectives...
commit
|
commitdiff
|
tree
2021-05-28
yoni206
Python API: bugfix + translating tests from cpp unit...
commit
|
commitdiff
|
tree
2021-05-28
Gereon Kremer
Add non-templated method to set option defaults (#6540)
commit
|
commitdiff
|
tree
2021-05-28
Andres Noetzli
Disable `--jh-rlv-order` for slow regressions (#6633)
commit
|
commitdiff
|
tree
2021-05-28
Andres Noetzli
`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts ...
commit
|
commitdiff
|
tree
2021-05-27
Andrew Reynolds
Fix regular expression aggressive elim (#6627)
commit
|
commitdiff
|
tree
2021-05-27
Andres Noetzli
Fix `str.replace_re` and `str.replace_re_all` (#6615)
commit
|
commitdiff
|
tree
2021-05-27
Ouyancheng
Add Lexicographic + Pareto Optimizations (#6626)
commit
|
commitdiff
|
tree
2021-05-27
Andrew Reynolds
Update proof namespaces (#6614)
commit
|
commitdiff
|
tree
2021-05-27
Andrew Reynolds
Fix CEGQI for datatypes with Boolean subfields (#6630)
commit
|
commitdiff
|
tree
2021-05-27
Andrew Reynolds
Fix spurious assertion for trivial abduction (#6629)
commit
|
commitdiff
|
tree
2021-05-27
Aina Niemetz
FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD...
commit
|
commitdiff
|
tree
2021-05-27
Andres Noetzli
Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)
commit
|
commitdiff
|
tree
2021-05-27
Ouyancheng
Add support for Box optimization (#6599)
commit
|
commitdiff
|
tree
2021-05-27
Gereon Kremer
Avoid uploading docs if they did not change (#6621)
commit
|
commitdiff
|
tree
2021-05-27
Andrew Reynolds
Enable new justification heuristic by default (#6613)
commit
|
commitdiff
|
tree
2021-05-26
Gereon Kremer
Use references instead of getter functions (#6597)
commit
|
commitdiff
|
tree
2021-05-26
Andres Noetzli
More precise includes of `Node` constants (#6617)
commit
|
commitdiff
|
tree
2021-05-26
Gereon Kremer
Add more examples to the documentation (#6569)
commit
|
commitdiff
|
tree
2021-05-26
Gereon Kremer
Ensure proper types in unit tests (#6598)
commit
|
commitdiff
|
tree
2021-05-26
Gereon Kremer
Reduce size of sphinx-gh output (#6601)
commit
|
commitdiff
|
tree
2021-05-25
Aina Niemetz
api docs: Fix and tweak style for home and top links...
commit
|
commitdiff
|
tree
2021-05-25
Andres Noetzli
Replace deprecated calls to `std::allocator` (#6606)
commit
|
commitdiff
|
tree
2021-05-25
Andres Noetzli
[Unit tests] Fix path of Java bindings (#6616)
commit
|
commitdiff
|
tree
2021-05-24
Andrew Reynolds
Fix non-fixed length case in re-elim (#6612)
commit
|
commitdiff
|
tree
2021-05-24
Andrew Reynolds
Implementation of the new justification heuristic ...
commit
|
commitdiff
|
tree
next