projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
api: More comprehensive documentation of INTERNAL_KIND. (#8400)
2022-03-25 Andres Noetzli[Parser] Fix resolution of indexed symbols (#8383)
 commit | commitdiff | tree
2022-03-25 Andres NoetzliGenerate `enum` bindings for Python and Java (#8393)
 commit | commitdiff | tree
2022-03-25 Andres NoetzliFix 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 NoetzliRemove `Op::getIndices()` (#8355)
 commit | commitdiff | tree
2022-03-17 Andres Noetzli[Parser] Simplify `Smt2::addIndexedOperator()` (#8333)
 commit | commitdiff | tree
2022-03-17 Andres NoetzliRemove 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 NoetzliRemove 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 NoetzliFix shared library Windows builds with LibPoly (#8306)
 commit | commitdiff | tree
2022-03-16 Andres NoetzliIgnore `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 NoetzliSimplify `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 NoetzliRefactor 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 NoetzliUpdate documentation of `Solver::getUnsatCore()` (...
commit | commitdiff | tree
2022-03-06 Andres NoetzliDisallow 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 NoetzliRemove 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 NoetzliRemove 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 NoetzliImprove `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)
 commit | commitdiff | tree
2022-02-18 Andres NoetzliFix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121)
 commit | commitdiff | tree
2022-02-11 Andres NoetzliFix type check of `seq.nth` (#8093)
 commit | commitdiff | tree
2022-02-09 Andres NoetzliFix 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 NoetzliSend 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 NoetzliFix 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 NoetzliSend `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 NoetzliFix `Nth-Update` rule, add `Update-Bound` rule (#7968)
 commit | commitdiff | tree
2022-01-20 Andres NoetzliFix CI build for macOS (#7970)
 commit | commitdiff | tree
2022-01-19 Andres NoetzliAdd 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 NoetzliUnify abstract values and uninterpreted constants ...
commit | commitdiff | tree
2022-01-11 Andres NoetzliFix `TypeNode::substitute()` for type constants (#7920)
 commit | commitdiff | tree
2022-01-11 Andres NoetzliFix `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 NoetzliExecute `(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 NoetzliFix rewrite for `str.update(str.rev(s), n, t))` (#7838)
 commit | commitdiff | tree
2021-12-16 Andres NoetzliExplicitly disallow `mkConst(Rational)` (#7818)
 commit | commitdiff | tree
2021-12-14 Andres NoetzliAdd switches to toggle eager and inclusion solvers...
commit | commitdiff | tree
2021-12-03 Andres NoetzliFaster hasing for `cvc5::String` (#7742)
 commit | commitdiff | tree
2021-11-24 Andres NoetzliAlways enable API black box unit tests (#7696)
 commit | commitdiff | tree
2021-11-24 Andres NoetzliRemove dependency of `TypeNode` on `Node` (#7690)
 commit | commitdiff | tree
2021-11-24 Andres NoetzliMinor fixes (#7691)
 commit | commitdiff | tree
2021-11-23 Andres NoetzliMake `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 NoetzliClean up relationship of metakind and node_manager...
commit | commitdiff | tree
2021-11-17 Andres NoetzliFix binding of quoted symbols in `define-fun` (#7655)
 commit | commitdiff | tree
2021-11-16 Andres NoetzliRefactor `metakind` (#7639)
 commit | commitdiff | tree
2021-11-15 Andres Noetzli[Strings] Minor refactor of eager solver (#7628)
 commit | commitdiff | tree
2021-11-13 Andres NoetzliSkip `str.code` inferences for sequence eqcs (#7644)
 commit | commitdiff | tree
2021-11-12 Andres NoetzliFix redundant definitions of `NodeValue::getConst`...
commit | commitdiff | tree
2021-11-12 Andres NoetzliRemove `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 NoetzliMake `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 NoetzliRequire 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 NoetzliFix 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 NoetzliRefactor regressions script (#7249)
 commit | commitdiff | tree
2021-10-21 Andres NoetzliEnable and fix dump test (#7387)
 commit | commitdiff | tree
2021-10-18 Andres NoetzliUpdate SMT-COMP script (#7389)
 commit | commitdiff | tree
2021-09-30 Andres Noetzli[Printer] Only quote `set-info` value if necessary...
commit | commitdiff | tree
2021-09-29 Andres Noetzli[API] Update comments w.r.t. SymFPU, fix typos (#7263)
 commit | commitdiff | tree
2021-09-29 Andres NoetzliUpdate `--lang=help` (#7260)
 commit | commitdiff | tree
2021-09-21 Andres NoetzliFix handling of conversions between FP and reals (...
commit | commitdiff | tree
2021-09-20 Andres NoetzliOptionally enable interprocedural optimization (#7209)
 commit | commitdiff | tree
2021-09-17 Andres NoetzliUse a single `NodeManager` per thread (#7204)
 commit | commitdiff | tree
2021-09-14 Andres NoetzliMake `-o raw-benchmark` work with `--parse-only` (...
commit | commitdiff | tree
2021-09-13 Andres NoetzliRemove context getters from `TheoryState` (#7174)
 commit | commitdiff | tree
2021-09-10 Andres NoetzliUse C++17 attributes (#7154)
 commit | commitdiff | tree
2021-09-09 Andres NoetzliRemove `TheoryState::getEnv()` (#7163)
 commit | commitdiff | tree
2021-09-09 Andres NoetzliRemove `TheoryState::options()` (#7148)
 commit | commitdiff | tree
2021-09-07 Andres NoetzliUse `EnvObj` methods instead of `Theory` methods (...
commit | commitdiff | tree
next