projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add method to get leaves of a NodeTrie (#8583)
[cvc5.git]
/
test
/
2022-04-07
Andrew Reynolds
Make sets and bags operators left-associative (#8584)
tree
|
commitdiff
2022-04-05
Mathias Preiner
Update copyright headers for release 1.0 (#8539)
tree
|
commitdiff
2022-04-05
Andrew Reynolds
Make inst constant attribute robust to purification...
tree
|
commitdiff
2022-04-05
Gereon Kremer
Make rewriter more robust against RAN becoming rational...
tree
|
commitdiff
2022-04-05
Andrew Reynolds
Be permissive for subtyping in function definitions...
tree
|
commitdiff
2022-04-04
Andrew Reynolds
Rename getInstantiatedConstructorTerm to getInstantiate...
tree
|
commitdiff
2022-04-04
Haniel Barbosa
[proofs] [sat] Make SAT assumption bookeeping robust...
tree
|
commitdiff
2022-04-04
Andrew Reynolds
Fix for get-value with empty uninterpreted sort domain...
tree
|
commitdiff
2022-04-02
Andrew Reynolds
Rename mkSygusGrammar to mkGrammar (#8544)
tree
|
commitdiff
2022-04-02
Andrew Reynolds
Remove variant of mkDatatypeDecl with one sort paramete...
tree
|
commitdiff
2022-04-02
Aina Niemetz
api: Rename get(Selector|Constructor)Term() to getTerm...
tree
|
commitdiff
2022-04-02
Andrew Reynolds
Ignore irrelevant exponential terms (#8534)
tree
|
commitdiff
2022-04-02
Aina Niemetz
api: Remove DatatypeConstructor::getSelectorTerm()...
tree
|
commitdiff
2022-04-02
Andrew Reynolds
Require that used model values are constant in CEGQI...
tree
|
commitdiff
2022-04-02
mudathirmahgoub
Remove java API methods that accepts lists as arguments...
tree
|
commitdiff
2022-04-01
Gereon Kremer
Simplify the python base API in a few places (#8514)
tree
|
commitdiff
2022-04-01
Andrew Reynolds
Simplifications to the datatypes API (#8511)
tree
|
commitdiff
2022-04-01
Gereon Kremer
Prevent using the coverings solver with extended operat...
tree
|
commitdiff
2022-04-01
Aina Niemetz
api: Remove Datatype::getConstructorTerm(). (#8529)
tree
|
commitdiff
2022-04-01
Haniel Barbosa
Replace regression by minimized one via ddSMT (#8531)
tree
|
commitdiff
2022-04-01
Aina Niemetz
Python API: Do not rename enumerators. (#8507)
tree
|
commitdiff
2022-04-01
Haniel Barbosa
[proofs] [alethe] Fix Alethe post-processor (#8525)
tree
|
commitdiff
2022-04-01
Andrew Reynolds
Internal simplifications to constructing datatypes...
tree
|
commitdiff
2022-04-01
Gereon Kremer
Remove decorator from python API (#8505)
tree
|
commitdiff
2022-04-01
Andres Noetzli
[API] Add mode argument for `Solver::blockModel()`...
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
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
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
Andrew Reynolds
Fix lower vs upper bound issue for eager RE conflicts...
tree
|
commitdiff
2022-03-31
Andres Noetzli
Move Java package to `io.github.cvc5` (#8469)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix non-termination in the strings rewriter (#8438)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix case of Boolean skolem for ground term E-matching...
tree
|
commitdiff
2022-03-30
Gereon Kremer
Allow for multiple (equal) base model values (#8467)
tree
|
commitdiff
2022-03-30
Mathias Preiner
Exclude competition build for issue8377-resolve-indexed...
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
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
mudathirmahgoub
Fix some documentation warnings (#8453)
tree
|
commitdiff
2022-03-30
Mathias Preiner
Rename master branch to main. (#8452)
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
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
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
Mathias Preiner
Rename get-interpol to get-interpolant. (#8424)
tree
|
commitdiff
2022-03-28
Aina Niemetz
api: Remove left-over Sort::getUninterpretedSortName...
tree
|
commitdiff
2022-03-28
Andrew Reynolds
Fix synth result python unit test (#8418)
tree
|
commitdiff
2022-03-26
yoni206
Separating produce-interpols from the mode of interpola...
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
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
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
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
Andres Noetzli
Fix Python API tests (#8392)
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
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
2022-03-23
Andrew Reynolds
Add SynthResult to the API (#8370)
tree
|
commitdiff
2022-03-23
Gereon Kremer
Add `getOptionInfo()` and `getOptionNames()` to python...
tree
|
commitdiff
2022-03-23
Andrew Reynolds
Make IDOF_MAX rewrite only apply when all children...
tree
|
commitdiff
2022-03-23
mudathirmahgoub
Fix cvc5-projects issue 497 (#8331)
tree
|
commitdiff
2022-03-23
Andrew Reynolds
Fix non-termination issue in sygus enumerator (#8340)
tree
|
commitdiff
2022-03-22
Andres Noetzli
[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)
tree
|
commitdiff
2022-03-22
Andrew Reynolds
Fixes for witness terms appearing in CEGQI instantiatio...
tree
|
commitdiff
2022-03-22
Andrew Reynolds
Refactor result class (#8313)
tree
|
commitdiff
2022-03-22
Mathias Preiner
api: Unify mkTerm variants. (#8357)
tree
|
commitdiff
2022-03-22
Andres Noetzli
[API] Support `Op::operator[]` in Java and Python ...
tree
|
commitdiff
2022-03-21
Andres Noetzli
Remove `Op::getIndices()` (#8355)
tree
|
commitdiff
2022-03-21
Gereon Kremer
Fix names of unit tests (#8338)
tree
|
commitdiff
2022-03-20
Gereon Kremer
Add `getStatistics()` to python API (#8343)
tree
|
commitdiff
2022-03-17
Aina Niemetz
ctest: Fix labels for python unit tests. (#8328)
tree
|
commitdiff
2022-03-17
Gereon Kremer
Replace `Debug` by `Trace` (#7793)
tree
|
commitdiff
2022-03-16
Aina Niemetz
Add unit test and assertion to test and catch cvc5...
tree
|
commitdiff
2022-03-16
Andres Noetzli
Remove unused files in `regress0` (#8325)
tree
|
commitdiff
next