projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
[API] Add mode argument for `Solver::blockModel()` (#8521)
[cvc5.git]
/
src
/
2022-04-01
Andres Noetzli
[API] Add mode argument for `Solver::blockModel()`...
tree
|
commitdiff
2022-04-01
Andres Noetzli
Remove `UnknownExplanation::NO_STATUS` (#8518)
tree
|
commitdiff
2022-04-01
mudathirmahgoub
Fix javadoc custom tag warning (#8502)
tree
|
commitdiff
2022-04-01
Mathias Preiner
docs: Add documentation for modes. (#8509)
tree
|
commitdiff
2022-04-01
Aina Niemetz
Python api: Various fixes in docs. (#8480)
tree
|
commitdiff
2022-04-01
Andres Noetzli
[API] Remove redundant version of `mkFunctionSort`...
tree
|
commitdiff
2022-04-01
Andrew Reynolds
Fix sygus-inst when combined with bounded string quanti...
tree
|
commitdiff
2022-04-01
Mathias Preiner
api: Swap arguments of declareSygusVar. (#8499)
tree
|
commitdiff
2022-04-01
Mathias Preiner
api: Use std::optional for symbols in mk* functions...
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Handled quoted symbols in indexed operators (#8491)
tree
|
commitdiff
2022-03-31
Aina Niemetz
Various fixes related to isDatatypeXXX checks. (#8473)
tree
|
commitdiff
2022-03-31
Aina Niemetz
Sort, TypeNode: Rename functions related to datatypes...
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Disable minisat variable elimination when a parametric...
tree
|
commitdiff
2022-03-31
Aina Niemetz
api: Remove warning for Sort::instantiate(). (#8475)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Do not export dt.size (#8483)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix check for whether PI is reduced (#8485)
tree
|
commitdiff
2022-03-31
Gereon Kremer
Improve documentation for Statistics in C++ API (#8476)
tree
|
commitdiff
2022-03-31
Haniel Barbosa
[proofs] Adding post-visit processing to proof node...
tree
|
commitdiff
2022-03-31
Andres Noetzli
Fix Java examples (#8484)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix lower vs upper bound issue for eager RE conflicts...
tree
|
commitdiff
2022-03-31
Gereon Kremer
Improve documentation for OptionInfo (#8474)
tree
|
commitdiff
2022-03-31
Andres Noetzli
Move Java package to `io.github.cvc5` (#8469)
tree
|
commitdiff
2022-03-31
Haniel Barbosa
[proofs] [doc] Documenting arrays, bit-vectors, datatyp...
tree
|
commitdiff
2022-03-31
Haniel Barbosa
[proofs] [doc] Document equality rules (#8462)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix non-termination in the strings rewriter (#8438)
tree
|
commitdiff
2022-03-31
Aina Niemetz
api: Mark experimental kinds. (#8464)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix case of Boolean skolem for ground term E-matching...
tree
|
commitdiff
2022-03-31
Mathias Preiner
api: Remove isUninterpretedSortParameterized from heade...
tree
|
commitdiff
2022-03-30
Gereon Kremer
Allow for multiple (equal) base model values (#8467)
tree
|
commitdiff
2022-03-30
Mathias Preiner
Move cvc5::internal::context to cvc5::context. (#8451)
tree
|
commitdiff
2022-03-30
mudathirmahgoub
Patch cross reference in Kind.java documentation (...
tree
|
commitdiff
2022-03-30
Aina Niemetz
api: Add Sort::getUninterpretedSortConstructor(). ...
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Fix policy for purifying arguments of exp (#8416)
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Fixes for sygus-inst (#8448)
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Fix subtype issue in cegqi arithmetic (#8440)
tree
|
commitdiff
2022-03-30
Aina Niemetz
TypeNode: Unify functions to instantiate parametric...
tree
|
commitdiff
2022-03-30
Andres Noetzli
[API] Move `UnknownExplanation` to `cvc5_types.h` ...
tree
|
commitdiff
2022-03-30
Haniel Barbosa
[proof] [doc] Document external proof rules (#8439)
tree
|
commitdiff
2022-03-30
Mathias Preiner
Move cvc5::internal::main to cvc5::main. (#8454)
tree
|
commitdiff
2022-03-30
yoni206
Add information for cardinality constraint to the Pytho...
tree
|
commitdiff
2022-03-30
yoni206
Adding some missing python API methods and tests (...
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Change tuple tokens and update datatypes theory ref...
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Add LFSC to internal proof checker (#8442)
tree
|
commitdiff
2022-03-30
mudathirmahgoub
Fix some documentation warnings (#8453)
tree
|
commitdiff
2022-03-30
Mathias Preiner
Rename master branch to main. (#8452)
tree
|
commitdiff
2022-03-30
Abdalrhman Mohamed
Show the code for utilities in the docs. (#8387)
tree
|
commitdiff
2022-03-30
Aina Niemetz
TypeNode: Rename isSort() and getSortConstructorArity...
tree
|
commitdiff
2022-03-29
Mathias Preiner
Introduce internal namespace and remove api namespace...
tree
|
commitdiff
2022-03-29
Aina Niemetz
api: Add Sort::getInstantiatedParameters(). (#8445)
tree
|
commitdiff
2022-03-29
yoni206
bv-to-int: fix translation of bvneg (#8437)
tree
|
commitdiff
2022-03-29
Andrew Reynolds
Make ensureTermSort private (#8436)
tree
|
commitdiff
2022-03-29
Andrew Reynolds
Add information for cardinality constraint to the API...
tree
|
commitdiff
2022-03-29
Andrew Reynolds
Make ProofNodeManager mkScope more robust (#8435)
tree
|
commitdiff
2022-03-29
Andrew Reynolds
Fix issue related to use of Boolean term variable for...
tree
|
commitdiff
2022-03-29
Andres Noetzli
[API] Add `{is,get}RoundingModeValue()` (#8429)
tree
|
commitdiff
2022-03-29
Aina Niemetz
TypeNode: Refactor get param types handling. (#8428)
tree
|
commitdiff
2022-03-29
Clark Barrett
Fix for issue 5925: constant arrays should be nonlinear...
tree
|
commitdiff
2022-03-29
Aina Niemetz
api: Add Sort::isInstantiated(). (#8425)
tree
|
commitdiff
2022-03-29
Andres Noetzli
Move `RoundingMode` to `cvc5_types.h` (#8427)
tree
|
commitdiff
2022-03-28
Andrew Reynolds
Mark more methods as experimental (#8426)
tree
|
commitdiff
2022-03-28
Mathias Preiner
Rename get-interpol to get-interpolant. (#8424)
tree
|
commitdiff
2022-03-28
Andres Noetzli
[API] Mark methods as experimental (#8249)
tree
|
commitdiff
2022-03-28
Aina Niemetz
api: Remove left-over Sort::getUninterpretedSortName...
tree
|
commitdiff
2022-03-28
Lachnitt
[proofs] Alethe: Call Printer (#8408)
tree
|
commitdiff
2022-03-28
Lachnitt
[proofs] Alethe: Add ALETHE_RULE to builtin proof check...
tree
|
commitdiff
2022-03-28
Mathias Preiner
Mark solve-bv-as-int as expert. (#8417)
tree
|
commitdiff
2022-03-26
yoni206
Separating produce-interpols from the mode of interpola...
tree
|
commitdiff
2022-03-26
Aina Niemetz
builtin: Move type rules implementation to .cpp file...
tree
|
commitdiff
2022-03-26
Aina Niemetz
api: Rename *SortConstructor* to *UninterpretedSortCons...
tree
|
commitdiff
2022-03-26
Andrew Reynolds
Fix spurious assertion failure (#8404)
tree
|
commitdiff
2022-03-26
Andrew Reynolds
Throw logic exception for set.map (#8403)
tree
|
commitdiff
2022-03-26
Andrew Reynolds
More minor cleaning of options (#8401)
tree
|
commitdiff
2022-03-26
Andrew Reynolds
Fixes for API kind documentation (#8397)
tree
|
commitdiff
2022-03-26
Gereon Kremer
Add API unit tests for options (#8339)
tree
|
commitdiff
2022-03-25
Mathias Preiner
api: Unify mkOp variants. (#8369)
tree
|
commitdiff
2022-03-25
Aina Niemetz
api: More comprehensive documentation of INTERNAL_KIND...
tree
|
commitdiff
2022-03-25
Andres Noetzli
[Parser] Fix resolution of indexed symbols (#8383)
tree
|
commitdiff
2022-03-25
Aina Niemetz
api: Remove Sort::isParametricDatatype(). (#8405)
tree
|
commitdiff
2022-03-25
Haniel Barbosa
[proofs] [sat] Have SAT solver communicate whether...
tree
|
commitdiff
2022-03-25
Aina Niemetz
api: Rename kind NULL_EXPR to NULL_TERM. (#8402)
tree
|
commitdiff
2022-03-25
Andres Noetzli
Generate `enum` bindings for Python and Java (#8393)
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Update checkSynth and checkSynthNext to return SynthRes...
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Change output of abduction/interpolation for failed...
tree
|
commitdiff
2022-03-25
Lachnitt
[proofs] Alethe: Bug Fix in Cong Rule (#8391)
tree
|
commitdiff
2022-03-25
Aina Niemetz
api: Remove blocks in kinds header. (#8398)
tree
|
commitdiff
2022-03-25
Haniel Barbosa
[proofs] [cnf] Utilities to notify and track proofs...
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Fixes related to set defaults for sygus/proofs (#8395)
tree
|
commitdiff
2022-03-25
Aina Niemetz
api: Refactor kinds documentation. (#8384)
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Properly guard commands in the SyGuS API (#8390)
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Recategorize options (#8386)
tree
|
commitdiff
2022-03-24
Gereon Kremer
Document proof rules for coverings solver (#8376)
tree
|
commitdiff
2022-03-24
Andrew Reynolds
Minor updates for quantifiers options (#8385)
tree
|
commitdiff
2022-03-24
Haniel Barbosa
[proofs] [sat] Handle resolution proofs for optimized...
tree
|
commitdiff
2022-03-24
Gereon Kremer
Document arithmetic proof rules (#8373)
tree
|
commitdiff
2022-03-24
Andrew Reynolds
Standardize more instances of skolems (#8351)
tree
|
commitdiff
2022-03-24
Haniel Barbosa
[sat] Add option to disable Minisat simplifications...
tree
|
commitdiff
2022-03-24
Andrew Reynolds
Fix a couple of parse error messages for sygus (#8381)
tree
|
commitdiff
2022-03-24
Haniel Barbosa
[unsat-cores] [sat-proof] Fix open proofs due to theory...
tree
|
commitdiff
2022-03-23
Andrew Reynolds
Clean options (#8309)
tree
|
commitdiff
2022-03-23
Gereon Kremer
Add API unit tests for statistics (#8341)
tree
|
commitdiff
next