projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-11-06
Andrew Reynolds
Do not use extended rewrites on recursive function...
commit
|
commitdiff
|
tree
2021-11-06
Gereon Kremer
Only run regress0 for static build (#7592)
commit
|
commitdiff
|
tree
2021-11-06
Gereon Kremer
Remove `Notice()` in favor of new `verbose()` (#7588)
commit
|
commitdiff
|
tree
2021-11-06
Mathias Preiner
Disable regress2 test. (#7591)
commit
|
commitdiff
|
tree
2021-11-05
Andrew Reynolds
Fix exclusion criteria for codatatype model values...
commit
|
commitdiff
|
tree
2021-11-05
Haniel Barbosa
[proofs] Fix open sat proof (#7509)
commit
|
commitdiff
|
tree
2021-11-05
Andrew Reynolds
Eliminate a level of nesting of traversals in theory...
commit
|
commitdiff
|
tree
2021-11-05
Gereon Kremer
Remove `Chat()` in favor of new `verbose()` (#7586)
commit
|
commitdiff
|
tree
2021-11-05
Andrew Reynolds
Move functions and lambdas from builtin to uf (#7570)
commit
|
commitdiff
|
tree
2021-11-05
Andres Noetzli
[FP] Do not assert that model has shared term (#7585)
commit
|
commitdiff
|
tree
2021-11-05
Gereon Kremer
Fix some issues with the java api (#7583)
commit
|
commitdiff
|
tree
2021-11-05
Lachnitt
Alethe: Translate CNF rules (#7532)
commit
|
commitdiff
|
tree
2021-11-05
Haniel Barbosa
Minor changes to circuit propagator (#7584)
commit
|
commitdiff
|
tree
2021-11-05
Andrew Reynolds
Remove many static calls to rewrite (#7580)
commit
|
commitdiff
|
tree
2021-11-05
Gereon Kremer
Remove quadratic solving in NlModel (#7542)
commit
|
commitdiff
|
tree
2021-11-05
Gereon Kremer
Eliminate `Warning` macro in favor of `EnvObj::warning...
commit
|
commitdiff
|
tree
2021-11-05
Gereon Kremer
Remove a bunch of debugging/logging code from the linea...
commit
|
commitdiff
|
tree
2021-11-04
Andrew Reynolds
Add -o sygus-grammar to print auto-generated SyGuS...
commit
|
commitdiff
|
tree
2021-11-04
Andrew Reynolds
Improve defaults for sygus default grammars (#7553)
commit
|
commitdiff
|
tree
2021-11-04
Andrew Reynolds
Replace the old dump infrastructure (#7572)
commit
|
commitdiff
|
tree
2021-11-04
Gereon Kremer
Start refactoring of `-o` and `-v` (#7449)
commit
|
commitdiff
|
tree
2021-11-04
Gereon Kremer
Refactor cmake to build either static or shared (#7534)
commit
|
commitdiff
|
tree
2021-11-04
Gereon Kremer
Fix links in README.md (#7568)
commit
|
commitdiff
|
tree
2021-11-04
Gereon Kremer
Enable CDCAC solver for selected quantified logics...
commit
|
commitdiff
|
tree
2021-11-04
Gereon Kremer
Add support for special tag collectors (#7562)
commit
|
commitdiff
|
tree
2021-11-04
Gereon Kremer
Minor cleanup in SolverEngine::setInfo() (#7566)
commit
|
commitdiff
|
tree
2021-11-04
Andres Noetzli
Make `Theory::get()` private (#7518)
commit
|
commitdiff
|
tree
2021-11-03
Aina Niemetz
api: Rename some separation logic functions for consist...
commit
|
commitdiff
|
tree
2021-11-03
Aina Niemetz
Add unit test to cover previous failure with second...
commit
|
commitdiff
|
tree
2021-11-03
mudathirmahgoub
Enable CI for Junit tests (#7436)
commit
|
commitdiff
|
tree
2021-11-03
Andrew Reynolds
Fix debug trace for miplib (#7563)
commit
|
commitdiff
|
tree
2021-11-03
Andrew Reynolds
Refactor skolem construction (#7561)
commit
|
commitdiff
|
tree
2021-11-03
Andrew Reynolds
Formalize more string skolems (#7554)
commit
|
commitdiff
|
tree
2021-11-03
Andrew Reynolds
Fix preregistration for floating point theory (#7558)
commit
|
commitdiff
|
tree
2021-11-02
Mathias Preiner
bv: Disable equality engine for --bitblast=eager and...
commit
|
commitdiff
|
tree
2021-11-02
Abdalrhman...
Move `fmf.card` printing code. (#7559)
commit
|
commitdiff
|
tree
2021-11-02
Abdalrhman...
Add printing methods for some commands. (#7557)
commit
|
commitdiff
|
tree
2021-11-02
Andrew Reynolds
Improve syntax for fmf cardinality constraints (#7556)
commit
|
commitdiff
|
tree
2021-11-02
Andrew Reynolds
Add LFSC signature for quantifiers (#7540)
commit
|
commitdiff
|
tree
2021-11-02
Mathias Preiner
Fix setDefaults() for proofs with bitblast-internal...
commit
|
commitdiff
|
tree
2021-11-02
Mathias Preiner
bv: Remove remaining Rewriter::rewrite calls. (#7545)
commit
|
commitdiff
|
tree
2021-11-02
Andrew Reynolds
Make quant elimination robust to presence of other...
commit
|
commitdiff
|
tree
2021-11-01
Andrew Reynolds
Eliminate calls to Rewriter::rewrite and options::...
commit
|
commitdiff
|
tree
2021-11-01
Andrew Reynolds
Weaken assertion in CEGQI (#7548)
commit
|
commitdiff
|
tree
2021-11-01
Gereon Kremer
Add explicit option enum value __MAX_VALUE (#7547)
commit
|
commitdiff
|
tree
2021-11-01
Mathias Preiner
bv: Remove layered solver. (#7455)
commit
|
commitdiff
|
tree
2021-11-01
Aina Niemetz
api: Fix documentation for kind IAND. (#7536)
commit
|
commitdiff
|
tree
2021-11-01
Gereon Kremer
Fix a couple of issues with uploading docs for releases...
commit
|
commitdiff
|
tree
2021-11-01
Gereon Kremer
Clean up CLN includes (#7544)
commit
|
commitdiff
|
tree
2021-11-01
Gereon Kremer
Add fuzzing target for murxla (#7490)
commit
|
commitdiff
|
tree
2021-11-01
Andrew Reynolds
Fix upwards closure for relations (#7515)
commit
|
commitdiff
|
tree
2021-11-01
Gereon Kremer
Replace more static options accesses (#7531)
commit
|
commitdiff
|
tree
2021-11-01
Gereon Kremer
Refactor DidYouMean (#7535)
commit
|
commitdiff
|
tree
2021-10-31
Mathias Preiner
api: Add guard against querying value from term with...
commit
|
commitdiff
|
tree
2021-10-31
mudathirmahgoub
Fix soundess issue for bags with negative multiplicity...
commit
|
commitdiff
|
tree
2021-10-31
mudathirmahgoub
Remove assertSkeleton for bag elements during model...
commit
|
commitdiff
|
tree
2021-10-29
Gereon Kremer
Fix proof of nl lemma for a corner case (#7530)
commit
|
commitdiff
|
tree
2021-10-29
Mathias Preiner
Start post-release for 0.0.3
commit
|
commitdiff
|
tree
2021-10-29
Mathias Preiner
Bump version to 0.0.3
commit
|
commitdiff
|
tree
2021-10-29
Gereon Kremer
Remove options::X__numValues (#7419)
commit
|
commitdiff
|
tree
2021-10-29
Andrew Reynolds
Minor cleanup of proof messages (#7494)
commit
|
commitdiff
|
tree
2021-10-29
Andrew Reynolds
Fix model construction for higher order involving irrel...
commit
|
commitdiff
|
tree
2021-10-29
Andrew Reynolds
Add PfRule ARITH_POLY_NORM (#7501)
commit
|
commitdiff
|
tree
2021-10-29
Andrew Reynolds
Improvements for LFSC proof conversion (#7524)
commit
|
commitdiff
|
tree
2021-10-29
Gereon Kremer
Remove static access to options in decision folder...
commit
|
commitdiff
|
tree
2021-10-28
Gereon Kremer
Fix proof for xor in circuit propagator (#7525)
commit
|
commitdiff
|
tree
2021-10-28
Gereon Kremer
Combine `--static` and `--static-binary` (#7520)
commit
|
commitdiff
|
tree
2021-10-28
Haniel Barbosa
[proofs] Fix assertion in EqProof conversion (#7522)
commit
|
commitdiff
|
tree
2021-10-28
Andrew V. Jones
Add support for checking if a `-Wno` flag exists before...
commit
|
commitdiff
|
tree
2021-10-28
Abdalrhman...
Add a `define-fun` command for each `:named` term....
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
Properly guard proof construction for STRINGS_EXTF_EQ_R...
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
LFSC signature for linear arithmetic (#7445)
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
LFSC signature for CNF (#7444)
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
LFSC signature for Booleans (#7443)
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
LFSC signature for equality (#7442)
commit
|
commitdiff
|
tree
2021-10-28
Abdalrhman...
Fix `(set-info <sexpr>)` parsing and printing bugs...
commit
|
commitdiff
|
tree
2021-10-28
Gereon Kremer
Remove separate cpp docs for UnknownExplanation (#7516)
commit
|
commitdiff
|
tree
2021-10-28
Gereon Kremer
Build shared and static in CI (#7472)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Add missing API checks to getValue (#7475)
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Add comments for arith type rules. (#7488)
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Add documentation on output tags (#7499)
commit
|
commitdiff
|
tree
2021-10-27
Andres Noetzli
[Regression Script] Fix use of undefined variables...
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Fix patching for poly on windows (#7513)
commit
|
commitdiff
|
tree
2021-10-27
Andres Noetzli
Require ITE branches to be first class types (#7508)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Fix care graph computation for higher-order (#7474)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Fix model unsoundness for relation join (#7511)
commit
|
commitdiff
|
tree
2021-10-27
yoni206
Python api documentation for sorts (#7440)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Avoid non-terminating check with assumptions in strings...
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Deterministic variables for RE elim (#7489)
commit
|
commitdiff
|
tree
2021-10-27
mudathirmahgoub
Fix mac compile errors in sort.cpp (#7507)
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Make --version exit (#7506)
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Fix libpoly build on windows (#7502)
commit
|
commitdiff
|
tree
2021-10-26
Haniel Barbosa
[proofs] Fix singleton check in MACRO_RES post-processi...
commit
|
commitdiff
|
tree
2021-10-26
Haniel Barbosa
[proofs] Modularize check for whether a clause is singl...
commit
|
commitdiff
|
tree
2021-10-26
Haniel Barbosa
[proofs] Reset local var in SatProofManager since incre...
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Disable automatic symmetry in proofs of theory explanat...
commit
|
commitdiff
|
tree
2021-10-26
Haniel Barbosa
[proofs] Fix and simplify CHAIN_RESOLUTION checker...
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Add regressions for fixed issues (#7495)
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Disable sygus-inst when incremental (#7485)
commit
|
commitdiff
|
tree
2021-10-26
Lachnitt
[proofs] Alethe: Translate Block of clause pattern...
commit
|
commitdiff
|
tree
next