projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-07-06
Gereon Kremer
Add doc page about transcendentals (#6755)
commit
|
commitdiff
|
tree
2021-07-05
Andres Noetzli
[Strings] Fix incorrect rewrite (#6837)
commit
|
commitdiff
|
tree
2021-07-05
Andrew Reynolds
Make buffered inference manager more robust to backtrac...
commit
|
commitdiff
|
tree
2021-07-03
Andres Noetzli
Fix performance of string regression (#6832)
commit
|
commitdiff
|
tree
2021-07-03
Mathias Preiner
Add output tags -o, --output. (#6826)
commit
|
commitdiff
|
tree
2021-07-02
Mathias Preiner
Fix bv assert input reset assertions (#6820)
commit
|
commitdiff
|
tree
2021-07-02
Andrew Reynolds
Fix rewriter for negative constant seq.nth (#6827)
commit
|
commitdiff
|
tree
2021-07-02
Andres Noetzli
Fix CaDiCaL auto-download on macOS (#6828)
commit
|
commitdiff
|
tree
2021-07-02
Gereon Kremer
Refactor lexer for SMT-LIB in sphinx (#6805)
commit
|
commitdiff
|
tree
2021-07-02
Andres Noetzli
Add reverse iterators to `Node`/`TNode` (#6825)
commit
|
commitdiff
|
tree
2021-07-01
Andrew Reynolds
Add recursive function definitions to subsolver in...
commit
|
commitdiff
|
tree
2021-07-01
Gereon Kremer
Fix message to show that cadical and symfpu are require...
commit
|
commitdiff
|
tree
2021-07-01
Andrew Reynolds
Add option to limit the number of instantiation rounds...
commit
|
commitdiff
|
tree
2021-06-30
Mathias Preiner
Use SAT context level for --bv-assert-input instead...
commit
|
commitdiff
|
tree
2021-06-30
Gereon Kremer
Use authored date instead of commit date. (#6815)
commit
|
commitdiff
|
tree
2021-06-30
yoni206
pow2: new test (#6819)
commit
|
commitdiff
|
tree
2021-06-30
Andrew Reynolds
Do not notify during equality engine initialization...
commit
|
commitdiff
|
tree
2021-06-30
Andrew Reynolds
Do not apply fmfBound to standard quantifiers when...
commit
|
commitdiff
|
tree
2021-06-30
Andrew Reynolds
Fix pre vs. post-rewrite in proofs for theory preproces...
commit
|
commitdiff
|
tree
2021-06-30
yoni206
int-to-bv: correct model values (#6811)
commit
|
commitdiff
|
tree
2021-06-29
Gereon Kremer
Add new variants for the CAD projection (#6794)
commit
|
commitdiff
|
tree
2021-06-29
Mathias Preiner
Fix statistics in AigBitblaster. (#6810)
commit
|
commitdiff
|
tree
2021-06-29
Aina Niemetz
FP: Refactor, rewrite and clean up word blasting. ...
commit
|
commitdiff
|
tree
2021-06-28
yoni206
Rewrite POW to POW2 when the base is 2 (#6806)
commit
|
commitdiff
|
tree
2021-06-28
Andrew Reynolds
Rename internal string kinds to match API (#6797)
commit
|
commitdiff
|
tree
2021-06-28
Ouyancheng
Further fix #6453 (#6804)
commit
|
commitdiff
|
tree
2021-06-28
Haniel Barbosa
[proof] [dot] Make dot printer stateful (#6799)
commit
|
commitdiff
|
tree
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
next