projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-11-11
Abdalrhman...
Add an API method to get the raw name of a term. (...
commit
|
commitdiff
|
tree
2021-11-11
Andrew Reynolds
Generalize front-end checks to check for shadowed varia...
commit
|
commitdiff
|
tree
2021-11-11
Andrew Reynolds
Add lazy approach for handling lambdas in the HO extens...
commit
|
commitdiff
|
tree
2021-11-11
Andrew Reynolds
Fixes for update/nth over constant sequences (#7631)
commit
|
commitdiff
|
tree
2021-11-10
Aina Niemetz
api: Add Solver::mkRegexpAll(). (#7614)
commit
|
commitdiff
|
tree
2021-11-10
Lachnitt
[proofs] Alethe: Translate of Arithmetic rules (#7613)
commit
|
commitdiff
|
tree
2021-11-10
Lachnitt
[proofs] Alethe: Translate INSTANTIATE rule (#7607)
commit
|
commitdiff
|
tree
2021-11-10
Mathias Preiner
docs: Also create javadoc for generated Kind.java ...
commit
|
commitdiff
|
tree
2021-11-10
mudathirmahgoub
Fix soundness issue of missing premises for count bag...
commit
|
commitdiff
|
tree
2021-11-10
Mathias Preiner
java: Fix building cvc5.jar for cmake 3.16. (#7623)
commit
|
commitdiff
|
tree
2021-11-10
Andrew Reynolds
Fix parsing array constants (#7617)
commit
|
commitdiff
|
tree
2021-11-10
Aina Niemetz
sets: Rename set.intersection to set.inter. (#7622)
commit
|
commitdiff
|
tree
2021-11-10
Aina Niemetz
Reorganize test/unit/api directory. (#7612)
commit
|
commitdiff
|
tree
2021-11-09
Lachnitt
[proofs] Alethe: Translate Further Equality rules ...
commit
|
commitdiff
|
tree
2021-11-09
Lachnitt
[proofs] Alethe: Translate Equality rules (#7605)
commit
|
commitdiff
|
tree
2021-11-09
Andrew Reynolds
Only eliminate lambdas in higher-order elimination...
commit
|
commitdiff
|
tree
2021-11-09
Andrew Reynolds
Minor optimizations for term database (#7600)
commit
|
commitdiff
|
tree
2021-11-09
Aina Niemetz
Clean up ctest configuration and CI test configuration...
commit
|
commitdiff
|
tree
2021-11-09
Haniel Barbosa
[proofs] Generalize trivial cycle detection in LazyCDPr...
commit
|
commitdiff
|
tree
2021-11-09
Lachnitt
[proofs] Alethe: Translate REORDERING rule (#7533)
commit
|
commitdiff
|
tree
2021-11-09
Aina Niemetz
sets: Update theory reference and smt2 examples. (...
commit
|
commitdiff
|
tree
2021-11-09
Andrew Reynolds
Preparation for non-constant lambda models (#7604)
commit
|
commitdiff
|
tree
2021-11-09
Gereon Kremer
Make secant points user context dependent (#7567)
commit
|
commitdiff
|
tree
2021-11-09
Abdalrhman...
Remove redundant rules for generating Java and Python...
commit
|
commitdiff
|
tree
2021-11-09
Andrew Reynolds
Add LFSC signature for strings (#7523)
commit
|
commitdiff
|
tree
2021-11-09
Aina Niemetz
regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match...
commit
|
commitdiff
|
tree
2021-11-09
Gereon Kremer
Remove `CVC5Message` (#7610)
commit
|
commitdiff
|
tree
2021-11-09
Gereon Kremer
Remove antlr_tracing.h (#7608)
commit
|
commitdiff
|
tree
2021-11-09
Gereon Kremer
Remove more static option accesses (#7582)
commit
|
commitdiff
|
tree
2021-11-09
Gereon Kremer
Remove command-verbosity option (#7581)
commit
|
commitdiff
|
tree
2021-11-09
Mathias Preiner
cmake: Use fastcov for generating coverage reports...
commit
|
commitdiff
|
tree
2021-11-08
Gereon Kremer
Improve rendering of expert options. (#7589)
commit
|
commitdiff
|
tree
2021-11-08
mudathirmahgoub
expand bag.choose operator (#7481)
commit
|
commitdiff
|
tree
2021-11-08
Andrew Reynolds
Add lambda lift utility (#7601)
commit
|
commitdiff
|
tree
2021-11-08
Aina Niemetz
sets: Rename kinds with a more consistent naming scheme...
commit
|
commitdiff
|
tree
2021-11-08
Andrew Reynolds
Evaluate cast-to-real operator (#7599)
commit
|
commitdiff
|
tree
2021-11-08
Haniel Barbosa
[proofs] Adding NoSubtype node converter to Alethe...
commit
|
commitdiff
|
tree
2021-11-08
Haniel Barbosa
[proofs] Method to convert node representation of Aleth...
commit
|
commitdiff
|
tree
2021-11-06
Gereon Kremer
Integrate java unit tests into ctest (#7593)
commit
|
commitdiff
|
tree
2021-11-06
Abdalrhman...
Print `unsupported` for unrecognized flags. (#7384)
commit
|
commitdiff
|
tree
2021-11-06
Haniel Barbosa
better traces in node converter (#7590)
commit
|
commitdiff
|
tree
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
next