projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2022-03-30
Andrew Reynolds
Fix subtype issue in cegqi arithmetic (#8440)
commit
|
commitdiff
|
tree
2022-03-30
Aina Niemetz
TypeNode: Unify functions to instantiate parametric...
commit
|
commitdiff
|
tree
2022-03-30
Andres Noetzli
[API] Move `UnknownExplanation` to `cvc5_types.h` ...
commit
|
commitdiff
|
tree
2022-03-30
Haniel Barbosa
[proof] [doc] Document external proof rules (#8439)
commit
|
commitdiff
|
tree
2022-03-30
Mathias Preiner
Move cvc5::internal::main to cvc5::main. (#8454)
commit
|
commitdiff
|
tree
2022-03-30
yoni206
Add information for cardinality constraint to the Pytho...
commit
|
commitdiff
|
tree
2022-03-30
yoni206
Adding some missing python API methods and tests (...
commit
|
commitdiff
|
tree
2022-03-30
Andrew Reynolds
Change tuple tokens and update datatypes theory ref...
commit
|
commitdiff
|
tree
2022-03-30
Andrew Reynolds
Add LFSC to internal proof checker (#8442)
commit
|
commitdiff
|
tree
2022-03-30
mudathirmahgoub
Fix some documentation warnings (#8453)
commit
|
commitdiff
|
tree
2022-03-30
Mathias Preiner
Rename master branch to main. (#8452)
commit
|
commitdiff
|
tree
2022-03-30
Abdalrhman...
Show the code for utilities in the docs. (#8387)
commit
|
commitdiff
|
tree
2022-03-30
Aina Niemetz
TypeNode: Rename isSort() and getSortConstructorArity...
commit
|
commitdiff
|
tree
2022-03-29
Mathias Preiner
Introduce internal namespace and remove api namespace...
commit
|
commitdiff
|
tree
2022-03-29
Aina Niemetz
api: Add Sort::getInstantiatedParameters(). (#8445)
commit
|
commitdiff
|
tree
2022-03-29
yoni206
bv-to-int: fix translation of bvneg (#8437)
commit
|
commitdiff
|
tree
2022-03-29
Andrew Reynolds
Make ensureTermSort private (#8436)
commit
|
commitdiff
|
tree
2022-03-29
Andrew Reynolds
Add information for cardinality constraint to the API...
commit
|
commitdiff
|
tree
2022-03-29
Andrew Reynolds
Make ProofNodeManager mkScope more robust (#8435)
commit
|
commitdiff
|
tree
2022-03-29
mudathirmahgoub
Add bags.rst (#8432)
commit
|
commitdiff
|
tree
2022-03-29
Andrew Reynolds
Fix issue related to use of Boolean term variable for...
commit
|
commitdiff
|
tree
2022-03-29
Andres Noetzli
[API] Add `{is,get}RoundingModeValue()` (#8429)
commit
|
commitdiff
|
tree
2022-03-29
Aina Niemetz
TypeNode: Refactor get param types handling. (#8428)
commit
|
commitdiff
|
tree
2022-03-29
Clark Barrett
Fix for issue 5925: constant arrays should be nonlinear...
commit
|
commitdiff
|
tree
2022-03-29
Aina Niemetz
api: Add Sort::isInstantiated(). (#8425)
commit
|
commitdiff
|
tree
2022-03-29
Andres Noetzli
Move `RoundingMode` to `cvc5_types.h` (#8427)
commit
|
commitdiff
|
tree
2022-03-28
Andrew Reynolds
Mark more methods as experimental (#8426)
commit
|
commitdiff
|
tree
2022-03-28
Mathias Preiner
Rename get-interpol to get-interpolant. (#8424)
commit
|
commitdiff
|
tree
2022-03-28
Andres Noetzli
[API] Mark methods as experimental (#8249)
commit
|
commitdiff
|
tree
2022-03-28
Mathias Preiner
ci: Enable all language bindings for debug build. ...
commit
|
commitdiff
|
tree
2022-03-28
Aina Niemetz
api: Remove left-over Sort::getUninterpretedSortName...
commit
|
commitdiff
|
tree
2022-03-28
Lachnitt
[proofs] Alethe: Call Printer (#8408)
commit
|
commitdiff
|
tree
2022-03-28
Lachnitt
[proofs] Alethe: Add ALETHE_RULE to builtin proof check...
commit
|
commitdiff
|
tree
2022-03-28
Andrew Reynolds
Fix synth result python unit test (#8418)
commit
|
commitdiff
|
tree
2022-03-28
Mathias Preiner
Mark solve-bv-as-int as expert. (#8417)
commit
|
commitdiff
|
tree
2022-03-26
yoni206
Separating produce-interpols from the mode of interpola...
commit
|
commitdiff
|
tree
2022-03-26
Aina Niemetz
builtin: Move type rules implementation to .cpp file...
commit
|
commitdiff
|
tree
2022-03-26
Aina Niemetz
api: Rename *SortConstructor* to *UninterpretedSortCons...
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Fix spurious assertion failure (#8404)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Throw logic exception for set.map (#8403)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
More minor cleaning of options (#8401)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Fixes for API kind documentation (#8397)
commit
|
commitdiff
|
tree
2022-03-26
Gereon Kremer
Add API unit tests for options (#8339)
commit
|
commitdiff
|
tree
2022-03-25
Mathias Preiner
api: Unify mkOp variants. (#8369)
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: More comprehensive documentation of INTERNAL_KIND...
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
[Parser] Fix resolution of indexed symbols (#8383)
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: Remove Sort::isParametricDatatype(). (#8405)
commit
|
commitdiff
|
tree
2022-03-25
Haniel Barbosa
[proofs] [sat] Have SAT solver communicate whether...
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: Rename kind NULL_EXPR to NULL_TERM. (#8402)
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
Generate `enum` bindings for Python and Java (#8393)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Update checkSynth and checkSynthNext to return SynthRes...
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Change output of abduction/interpolation for failed...
commit
|
commitdiff
|
tree
2022-03-25
Lachnitt
[proofs] Alethe: Bug Fix in Cong Rule (#8391)
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: Remove blocks in kinds header. (#8398)
commit
|
commitdiff
|
tree
2022-03-25
Haniel Barbosa
[proofs] [cnf] Utilities to notify and track proofs...
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Fixes related to set defaults for sygus/proofs (#8395)
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
Fix Python API tests (#8392)
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: Refactor kinds documentation. (#8384)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Properly guard commands in the SyGuS API (#8390)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Recategorize options (#8386)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Fixes for theory reference for datatypes (#8380)
commit
|
commitdiff
|
tree
2022-03-24
Gereon Kremer
Document proof rules for coverings solver (#8376)
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Minor updates for quantifiers options (#8385)
commit
|
commitdiff
|
tree
2022-03-24
Haniel Barbosa
[proofs] [sat] Handle resolution proofs for optimized...
commit
|
commitdiff
|
tree
2022-03-24
Gereon Kremer
Document arithmetic proof rules (#8373)
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Standardize more instances of skolems (#8351)
commit
|
commitdiff
|
tree
2022-03-24
Haniel Barbosa
[sat] Add option to disable Minisat simplifications...
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Fix a couple of parse error messages for sygus (#8381)
commit
|
commitdiff
|
tree
2022-03-24
Haniel Barbosa
[unsat-cores] [sat-proof] Fix open proofs due to theory...
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Clean options (#8309)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Add API unit tests for statistics (#8341)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Add SynthResult to the API (#8370)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Add `getOptionInfo()` and `getOptionNames()` to python...
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Document proof rules for transcendentals (#8375)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Make IDOF_MAX rewrite only apply when all children...
commit
|
commitdiff
|
tree
2022-03-23
Mathias Preiner
Only update latest tag if commit changed. (#8379)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Add internal synth result class (#8352)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Run gen-versioninfo unconditionally (#8368)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Store latest builds in a special release (#8337)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Remove dependency on build (#8367)
commit
|
commitdiff
|
tree
2022-03-23
mudathirmahgoub
update SET_COMPREHENSION documentation (#8372)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Initial documentation on LFSC (#8365)
commit
|
commitdiff
|
tree
2022-03-23
mudathirmahgoub
Fix cvc5-projects issue 497 (#8331)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Fix non-termination issue in sygus enumerator (#8340)
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Change null terminator for regular expression intersect...
commit
|
commitdiff
|
tree
2022-03-22
Gereon Kremer
Refactor proof rule documentation (#8303)
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Updates for the theory reference for separation logic...
commit
|
commitdiff
|
tree
2022-03-22
Gereon Kremer
Make uncovered-api-functions.py exit with 1 if somethin...
commit
|
commitdiff
|
tree
2022-03-22
Haniel Barbosa
[proofs] Alethe: fixing formatting and adding missing...
commit
|
commitdiff
|
tree
2022-03-22
mudathirmahgoub
update sets-and-relations.rst (#8364)
commit
|
commitdiff
|
tree
2022-03-22
Abdalrhman...
Add a timeout option for verification of synthesized...
commit
|
commitdiff
|
tree
2022-03-22
Andres Noetzli
[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Fixes for witness terms appearing in CEGQI instantiatio...
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Refactor result class (#8313)
commit
|
commitdiff
|
tree
2022-03-22
Mathias Preiner
api: Unify mkTerm variants. (#8357)
commit
|
commitdiff
|
tree
2022-03-22
Andres Noetzli
[API] Support `Op::operator[]` in Java and Python ...
commit
|
commitdiff
|
tree
2022-03-21
Andres Noetzli
Remove `Op::getIndices()` (#8355)
commit
|
commitdiff
|
tree
2022-03-21
Andrew Reynolds
Fix return value for candidate rewrite database (#8354)
commit
|
commitdiff
|
tree
2022-03-21
Gereon Kremer
Refactor documentation (#8288)
commit
|
commitdiff
|
tree
2022-03-21
Andrew Reynolds
Fix LFSC conversion for seq unit (#8353)
commit
|
commitdiff
|
tree
next