projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Make difficulty manager only consider lemmas at full effort (#7685)
2021-11-23
Andrew Reynolds
Make difficulty manager only consider lemmas at full...
commit
|
commitdiff
|
tree
2021-11-23
Andrew Reynolds
Enable model-based reduction technique for strings...
commit
|
commitdiff
|
tree
2021-11-23
Gereon Kremer
Add kinds to python docs (#7672)
commit
|
commitdiff
|
tree
2021-11-23
Gereon Kremer
Push output language inside the printing code (#7683)
commit
|
commitdiff
|
tree
2021-11-23
mudathirmahgoub
Add rewrite rule for bag.card operator using bag.map...
commit
|
commitdiff
|
tree
2021-11-23
yoni206
Python API documentation: terms (#7659)
commit
|
commitdiff
|
tree
2021-11-23
Andres Noetzli
Make `node_value.h` not depend on `node_manager.h`...
commit
|
commitdiff
|
tree
2021-11-22
Gereon Kremer
Refactor IO stream manipulators (#7555)
commit
|
commitdiff
|
tree
2021-11-22
Andrew Reynolds
Add rewrite for repeated re.allchar (#7681)
commit
|
commitdiff
|
tree
2021-11-22
Gereon Kremer
Set proper system processor for arm64 toolchain (#7665)
commit
|
commitdiff
|
tree
2021-11-22
Haniel Barbosa
[prop] Remove unused #define in theory proxy (#7670)
commit
|
commitdiff
|
tree
2021-11-22
Andrew Reynolds
Improve error for check theory assertions with model...
commit
|
commitdiff
|
tree
2021-11-22
Andrew Reynolds
Fix const RE test for internal regexp rv kind (#7678)
commit
|
commitdiff
|
tree
2021-11-20
yoni206
bv2int module: translation of more cases (#7653)
commit
|
commitdiff
|
tree
2021-11-19
Andres Noetzli
[API] Avoid copying values (#7666)
commit
|
commitdiff
|
tree
2021-11-19
Andres Noetzli
Clean up relationship of metakind and node_manager...
commit
|
commitdiff
|
tree
2021-11-19
Andrew Reynolds
Remove n-ary builder (#7671)
commit
|
commitdiff
|
tree
2021-11-19
Mathias Preiner
Allow negative denominator for CLN Rationals constructed...
commit
|
commitdiff
|
tree
2021-11-18
Aina Niemetz
api: Fix categorization of DT kinds in kind maps. ...
commit
|
commitdiff
|
tree
2021-11-18
Gereon Kremer
Refactor CAD option for linear model seed (#7657)
commit
|
commitdiff
|
tree
2021-11-18
Haniel Barbosa
[proofs] Fix trace in SatProofManager (#7664)
commit
|
commitdiff
|
tree
2021-11-18
Lachnitt
[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661)
commit
|
commitdiff
|
tree
2021-11-18
Aina Niemetz
api: Fix kind documentation for BAG_MAKE. (#7663)
commit
|
commitdiff
|
tree
2021-11-17
Haniel Barbosa
Improve naming in term canonization when handling HO...
commit
|
commitdiff
|
tree
2021-11-17
Haniel Barbosa
[sat] Fix indentation in "reason" (#7662)
commit
|
commitdiff
|
tree
2021-11-17
Gereon Kremer
Add documentation for z3py compatibility API (#7652)
commit
|
commitdiff
|
tree
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 generator...
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 intersection...
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 Mohamed
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 variables...
commit
|
commitdiff
|
tree
2021-11-11
Andrew Reynolds
Add lazy approach for handling lambdas in the HO extension...
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 LazyCDProofCh...
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 Mohamed
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 Alethe...
commit
|
commitdiff
|
tree
2021-11-06
Gereon Kremer
Integrate java unit tests into ctest (#7593)
commit
|
commitdiff
|
tree
2021-11-06
Abdalrhman Mohamed
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
next