projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
fix incorrect 64-bit detection -- powerpc64le doesn't end in 64 but is 64-bit
2022-04-01
Andres Noetzli
[API] Add mode argument for `Solver::blockModel()`...
commit
|
commitdiff
|
tree
2022-04-01
Andres Noetzli
Remove `UnknownExplanation::NO_STATUS` (#8518)
commit
|
commitdiff
|
tree
2022-04-01
Andres Noetzli
[API] Remove redundant version of `mkFunctionSort`...
commit
|
commitdiff
|
tree
2022-03-31
Andres Noetzli
Remove examples that use the old API (#8486)
commit
|
commitdiff
|
tree
2022-03-31
Andres Noetzli
Remove support for Python 2.x (#8488)
commit
|
commitdiff
|
tree
2022-03-31
Andres Noetzli
Fix Java examples (#8484)
commit
|
commitdiff
|
tree
2022-03-31
Andres Noetzli
Move Java package to `io.github.cvc5` (#8469)
commit
|
commitdiff
|
tree
2022-03-30
Andres Noetzli
[API] Move `UnknownExplanation` to `cvc5_types.h` ...
commit
|
commitdiff
|
tree
2022-03-29
Andres Noetzli
[API] Add `{is,get}RoundingModeValue()` (#8429)
commit
|
commitdiff
|
tree
2022-03-29
Andres Noetzli
Move `RoundingMode` to `cvc5_types.h` (#8427)
commit
|
commitdiff
|
tree
2022-03-28
Andres Noetzli
[API] Mark methods as experimental (#8249)
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
[Parser] Fix resolution of indexed symbols (#8383)
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
Generate `enum` bindings for Python and Java (#8393)
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
Fix Python API tests (#8392)
commit
|
commitdiff
|
tree
2022-03-22
Andres Noetzli
[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)
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-17
Andres Noetzli
[Parser] Simplify `Smt2::addIndexedOperator()` (#8333)
commit
|
commitdiff
|
tree
2022-03-17
Andres Noetzli
Remove unused options handler (#8335)
commit
|
commitdiff
|
tree
2022-03-17
Andres Noetzli
[CI] Use ccache for Windows builds (#8332)
commit
|
commitdiff
|
tree
2022-03-17
Andres Noetzli
[CI] Strip stored binaries (#8327)
commit
|
commitdiff
|
tree
2022-03-16
Andres Noetzli
Remove unused files in `regress0` (#8325)
commit
|
commitdiff
|
tree
2022-03-16
Andres Noetzli
[CI] Build and release Win64 binaries (#8321)
commit
|
commitdiff
|
tree
2022-03-16
Andres Noetzli
Fix shared library Windows builds with LibPoly (#8306)
commit
|
commitdiff
|
tree
2022-03-16
Andres Noetzli
Ignore `CMAKE_SYSROOT` when cross-compiling (#8318)
commit
|
commitdiff
|
tree
2022-03-15
Andres Noetzli
[BV] Fix strategy for rewriting `bvnot` (#8297)
commit
|
commitdiff
|
tree
2022-03-15
Andres Noetzli
Simplify `Scope` (#8307)
commit
|
commitdiff
|
tree
2022-03-11
Andres Noetzli
[API/Python] Add support for `Solver::getModel()` ...
commit
|
commitdiff
|
tree
2022-03-11
Andres Noetzli
[CI] Make building static/shared configurable (#8272)
commit
|
commitdiff
|
tree
2022-03-11
Andres Noetzli
Refactor kinds parser (#8287)
commit
|
commitdiff
|
tree
2022-03-08
Andres Noetzli
[API/Python] Add support for `Solver::getProof()` ...
commit
|
commitdiff
|
tree
2022-03-07
Andres Noetzli
Update documentation of `Solver::getUnsatCore()` (...
commit
|
commitdiff
|
tree
2022-03-06
Andres Noetzli
Disallow models with `--arrays-weak-equiv` (#8217)
commit
|
commitdiff
|
tree
2022-03-05
Andres Noetzli
[Docs] Add missing requirement (#8238)
commit
|
commitdiff
|
tree
2022-03-01
Andres Noetzli
[BV] Fix rewriter policy for `bvneg` (#8196)
commit
|
commitdiff
|
tree
2022-03-01
Andres Noetzli
Remove unused data members from `TheoryArrays` (#8197)
commit
|
commitdiff
|
tree
2022-02-28
Andres Noetzli
[Seq/Model] Do not enumerate elements of constants...
commit
|
commitdiff
|
tree
2022-02-28
Andres Noetzli
Remove broken/unused `--mmap` option (#8178)
commit
|
commitdiff
|
tree
2022-02-25
Andres Noetzli
[Python API] Add support for blocking models (#8134)
commit
|
commitdiff
|
tree
2022-02-23
Andres Noetzli
[Rewriter] Do not attempt to rewrite constants (#8061)
commit
|
commitdiff
|
tree
2022-02-18
Andres Noetzli
Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)
commit
|
commitdiff
|
tree
2022-02-18
Andres Noetzli
Fix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121)
commit
|
commitdiff
|
tree
2022-02-11
Andres Noetzli
Fix type check of `seq.nth` (#8093)
commit
|
commitdiff
|
tree
2022-02-09
Andres Noetzli
Fix handling of `LogicException` during solving (#8000)
commit
|
commitdiff
|
tree
2022-02-09
Andres Noetzli
[Seq] Fix rewrite of `(seq.nth s n)` for large `n`...
commit
|
commitdiff
|
tree
2022-02-07
Andres Noetzli
[BV] Fix response of `RewriteConcat` (#8074)
commit
|
commitdiff
|
tree
2022-02-06
Andres Noetzli
[Seq] Check types for split on indices (#8066)
commit
|
commitdiff
|
tree
2022-02-04
Andres Noetzli
[Rewriter] Always rewrite again when kind changes ...
commit
|
commitdiff
|
tree
2022-02-03
Andres Noetzli
Send all `nth` terms to the core array solver (#7990)
commit
|
commitdiff
|
tree
2022-02-01
Andres Noetzli
[BV] Fix strategy for `RewriteExtract` (#8011)
commit
|
commitdiff
|
tree
2022-02-01
Andres Noetzli
[BV] Fix order of rewrites for `concat` (#8010)
commit
|
commitdiff
|
tree
2022-02-01
Andres Noetzli
[Arrays] Fix response for `store` chains (#8015)
commit
|
commitdiff
|
tree
2022-01-31
Andres Noetzli
Fix memory leak in quantifier info (#8005)
commit
|
commitdiff
|
tree
2022-01-28
Andres Noetzli
[Rewrite Synthesis] Fix args for non-chaining ops ...
commit
|
commitdiff
|
tree
2022-01-25
Andres Noetzli
Send `nth(unit(...), ...)` terms to array solver (...
commit
|
commitdiff
|
tree
2022-01-25
Andres Noetzli
[Strings] Avoid trivial explanation (#7982)
commit
|
commitdiff
|
tree
2022-01-25
Andres Noetzli
[Strings] Remove redundant call to rewriter (#7978)
commit
|
commitdiff
|
tree
2022-01-25
Andres Noetzli
[FP] Fix unused variable warning (#7977)
commit
|
commitdiff
|
tree
2022-01-20
Andres Noetzli
Fix `Nth-Update` rule, add `Update-Bound` rule (#7968)
commit
|
commitdiff
|
tree
2022-01-20
Andres Noetzli
Fix CI build for macOS (#7970)
commit
|
commitdiff
|
tree
2022-01-19
Andres Noetzli
Add rewrites for `seq.update`/`seq.nth` (#7966)
commit
|
commitdiff
|
tree
2022-01-18
Andres Noetzli
[API] Add missing arity check (#7905)
commit
|
commitdiff
|
tree
2022-01-17
Andres Noetzli
[Strings] Fix rewriter for `re.loop` (#7956)
commit
|
commitdiff
|
tree
2022-01-13
Andres Noetzli
Unify abstract values and uninterpreted constants ...
commit
|
commitdiff
|
tree
2022-01-11
Andres Noetzli
Fix `TypeNode::substitute()` for type constants (#7920)
commit
|
commitdiff
|
tree
2022-01-11
Andres Noetzli
Fix `TypeNode::substitute()` (#7916)
commit
|
commitdiff
|
tree
2022-01-11
Andres Noetzli
[Win64] Link LibPoly statically for static builds ...
commit
|
commitdiff
|
tree
2022-01-07
Andres Noetzli
[Regressions] Add directive for disabling testers ...
commit
|
commitdiff
|
tree
2022-01-03
Andres Noetzli
[BV] Remove non-existent `friend` class (#7864)
commit
|
commitdiff
|
tree
2022-01-03
Andres Noetzli
Execute `(reset)` command in parse-only mode (#7862)
commit
|
commitdiff
|
tree
2021-12-23
Andres Noetzli
[Regressions] Support more complex scrubbers (#7819)
commit
|
commitdiff
|
tree
2021-12-20
Andres Noetzli
[Sequences/Array Solver] Minor refactoring (#7843)
commit
|
commitdiff
|
tree
2021-12-17
Andres Noetzli
[Strings] Minor fixes/improvements (#7837)
commit
|
commitdiff
|
tree
2021-12-17
Andres Noetzli
Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)
commit
|
commitdiff
|
tree
2021-12-16
Andres Noetzli
Explicitly disallow `mkConst(Rational)` (#7818)
commit
|
commitdiff
|
tree
2021-12-14
Andres Noetzli
Add switches to toggle eager and inclusion solvers...
commit
|
commitdiff
|
tree
2021-12-03
Andres Noetzli
Faster hasing for `cvc5::String` (#7742)
commit
|
commitdiff
|
tree
2021-11-24
Andres Noetzli
Always enable API black box unit tests (#7696)
commit
|
commitdiff
|
tree
2021-11-24
Andres Noetzli
Remove dependency of `TypeNode` on `Node` (#7690)
commit
|
commitdiff
|
tree
2021-11-24
Andres Noetzli
Minor fixes (#7691)
commit
|
commitdiff
|
tree
2021-11-23
Andres Noetzli
Make `node_value.h` not depend on `node_manager.h`...
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-17
Andres Noetzli
Fix binding of quoted symbols in `define-fun` (#7655)
commit
|
commitdiff
|
tree
2021-11-16
Andres Noetzli
Refactor `metakind` (#7639)
commit
|
commitdiff
|
tree
2021-11-15
Andres Noetzli
[Strings] Minor refactor of eager solver (#7628)
commit
|
commitdiff
|
tree
2021-11-13
Andres Noetzli
Skip `str.code` inferences for sequence eqcs (#7644)
commit
|
commitdiff
|
tree
2021-11-12
Andres Noetzli
Fix redundant definitions of `NodeValue::getConst`...
commit
|
commitdiff
|
tree
2021-11-12
Andres Noetzli
Remove `ConstantMap<Rational>` (#7635)
commit
|
commitdiff
|
tree
2021-11-05
Andres Noetzli
[FP] Do not assert that model has shared term (#7585)
commit
|
commitdiff
|
tree
2021-11-04
Andres Noetzli
Make `Theory::get()` private (#7518)
commit
|
commitdiff
|
tree
2021-10-27
Andres Noetzli
[Regression Script] Fix use of undefined variables...
commit
|
commitdiff
|
tree
2021-10-27
Andres Noetzli
Require ITE branches to be first class types (#7508)
commit
|
commitdiff
|
tree
2021-10-25
Andres Noetzli
[Regression Script] Support older Python versions ...
commit
|
commitdiff
|
tree
2021-10-22
Andres Noetzli
Fix memory management of `ErrorInformation` (#7388)
commit
|
commitdiff
|
tree
2021-10-21
Andres Noetzli
[Regression Script] Fix printing of error diff (#7451)
commit
|
commitdiff
|
tree
2021-10-21
Andres Noetzli
Refactor regressions script (#7249)
commit
|
commitdiff
|
tree
2021-10-21
Andres Noetzli
Enable and fix dump test (#7387)
commit
|
commitdiff
|
tree
2021-10-18
Andres Noetzli
Update SMT-COMP script (#7389)
commit
|
commitdiff
|
tree
2021-09-30
Andres Noetzli
[Printer] Only quote `set-info` value if necessary...
commit
|
commitdiff
|
tree
next