projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-11-17
Andrew Reynolds
Preparations for eliminating arithmetic subtyping ...
commit
|
commitdiff
|
tree
2021-11-17
Andrew Reynolds
Revert change and clean datatypes cons candidate genera...
commit
|
commitdiff
|
tree
2021-11-17
Gereon Kremer
Implement aggressive pruning in CAD solver (#7650)
commit
|
commitdiff
|
tree
2021-11-17
Alex Ozdemir
Update Python packaging infrastructure (#7654)
commit
|
commitdiff
|
tree
2021-11-17
Gereon Kremer
make default and modes strings instead of enum values...
commit
|
commitdiff
|
tree
2021-11-17
Andres Noetzli
Fix binding of quoted symbols in `define-fun` (#7655)
commit
|
commitdiff
|
tree
2021-11-17
Alex Ozdemir
Remove documentation for --lib-only (#7648)
commit
|
commitdiff
|
tree
2021-11-17
mudathirmahgoub
Update SimpleVC.java (#7647)
commit
|
commitdiff
|
tree
2021-11-16
yoni206
Translating API tests to Python — part 1 (#7597)
commit
|
commitdiff
|
tree
2021-11-16
mudathirmahgoub
Fix compile errors with java examples (#7646)
commit
|
commitdiff
|
tree
2021-11-16
Haniel Barbosa
[proofs] Make sure --proof-check=... is no-op when...
commit
|
commitdiff
|
tree
2021-11-16
Andres Noetzli
Refactor `metakind` (#7639)
commit
|
commitdiff
|
tree
2021-11-15
Aina Niemetz
api: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632)
commit
|
commitdiff
|
tree
2021-11-15
Andres Noetzli
[Strings] Minor refactor of eager solver (#7628)
commit
|
commitdiff
|
tree
2021-11-15
mudathirmahgoub
Add documentation for theory_bags_type_rules.h (#7642)
commit
|
commitdiff
|
tree
2021-11-13
Andres Noetzli
Skip `str.code` inferences for sequence eqcs (#7644)
commit
|
commitdiff
|
tree
2021-11-13
mudathirmahgoub
Fix type error for rewriting bag.map bag.union_disjoint...
commit
|
commitdiff
|
tree
2021-11-13
mudathirmahgoub
Add operator set.map to theory of sets (#7641)
commit
|
commitdiff
|
tree
2021-11-12
mudathirmahgoub
bags: Rename kinds with a more consistent naming scheme...
commit
|
commitdiff
|
tree
2021-11-12
Andrew Reynolds
[proofs] Cancel SYMM in CDProof, throw an error for...
commit
|
commitdiff
|
tree
2021-11-12
Andres Noetzli
Fix redundant definitions of `NodeValue::getConst`...
commit
|
commitdiff
|
tree
2021-11-12
Andrew Reynolds
Add some basic rewrites for regular expression intersec...
commit
|
commitdiff
|
tree
2021-11-12
Andres Noetzli
Remove `ConstantMap<Rational>` (#7635)
commit
|
commitdiff
|
tree
2021-11-12
Gereon Kremer
Various minor docs improvements (#7626)
commit
|
commitdiff
|
tree
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
next