projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-01-03 Aina Niemetzapi: Remove redundant check in Sort::toString(). (... commit | commitdiff | tree
2022-01-03 Gereon KremerRemove static options from sat solver. (#7790) 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-22 Andrew ReynoldsRemove most uses of mkRationalNode (#7854) commit | commitdiff | tree
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) commit | commitdiff | tree
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) commit | commitdiff | tree
2021-12-21 Andrew ReynoldsEliminate remaining calls to callExtendedRewrite (... commit | commitdiff | tree
2021-12-21 yoni206Rewrite (pow2 x) to (pow 2 x) when x is a constant... commit | commitdiff | tree
2021-12-21 Gereon KremerDisable unit tests without poly (#7844) commit | commitdiff | tree
2021-12-21 Andrew ReynoldsConnect sequences array solver to strategy in theory... commit | commitdiff | tree
2021-12-20 Andrew ReynoldsEliminating some uses of const rational in arithmetic... commit | commitdiff | tree
2021-12-20 Andrew ReynoldsUpdates to LFSC signatures (#7840) commit | commitdiff | tree
2021-12-20 Andrew ReynoldsAllow SyGuS subsolver to be reused in incremental mode... commit | commitdiff | tree
2021-12-20 Andres Noetzli[Sequences/Array Solver] Minor refactoring (#7843) commit | commitdiff | tree
2021-12-20 Haniel Barbosa[proofs] Fix helper LFSC script (#7845) commit | commitdiff | tree
2021-12-17 Aina Niemetzapi: java: Support default arity for Solver::mkUnresolv... commit | commitdiff | tree
2021-12-17 Andres Noetzli[Strings] Minor fixes/improvements (#7837) commit | commitdiff | tree
2021-12-17 Ying ShengArray-inspired Sequence Solver - Fixing several issues... commit | commitdiff | tree
2021-12-17 Andrew ReynoldsSimplify contrib/get-lfsc-checker and use cvc5 repo... commit | commitdiff | tree
2021-12-17 Andres NoetzliFix rewrite for `str.update(str.rev(s), n, t))` (#7838) commit | commitdiff | tree
2021-12-17 Andrew ReynoldsMinor refactoring of API for eliminating arithmetic... commit | commitdiff | tree
2021-12-17 Gereon KremerFix tracker in SubstitutionMap (#7829) commit | commitdiff | tree
2021-12-17 mudathirmahgoubRemove Rewriter::rewrite from bags type enumerator... commit | commitdiff | tree
2021-12-17 Andrew ReynoldsRefactoring initialization of proofs (#7834) commit | commitdiff | tree
2021-12-17 mudathirmahgoubAdd relations.cpp, relations.py examples (#7801) commit | commitdiff | tree
2021-12-17 Alex OzdemirMore documentation for idiomatic python API (#7798) commit | commitdiff | tree
2021-12-17 Andrew ReynoldsGet getRealOrIntegerValueSign to the API (#7832) commit | commitdiff | tree
2021-12-17 Andrew ReynoldsImplement model construction for the array extension... commit | commitdiff | tree
2021-12-17 Aina Niemetzapi: Rename DatatypeSelector::getRangeSort() to getCodo... commit | commitdiff | tree
2021-12-17 Aina Niemetzapi: Add Solver::mkUnresolvedSort(). (#7817) commit | commitdiff | tree
2021-12-17 Andrew ReynoldsEliminate more uses of CONST_RATIONAL (#7816) commit | commitdiff | tree
2021-12-17 Mathias PreinerDisable unsat cores for quaternion_ds1_symm_0428.fof... commit | commitdiff | tree
2021-12-16 Andrew ReynoldsEliminate most static calls to rewrite in quantifiers... commit | commitdiff | tree
2021-12-16 Andrew ReynoldsFix get-model when sort constructors are present (... commit | commitdiff | tree
2021-12-16 Haniel Barbosa[proofs] Simplifying and adding new utils to SAT proof... commit | commitdiff | tree
2021-12-16 Aina Niemetzapi: Add Sort::hasSymbol() and Sort::getSymbol(). ... commit | commitdiff | tree
2021-12-16 Andrew ReynoldsMinor fix for print benchmark. (#7821) commit | commitdiff | tree
2021-12-16 yoni206bv-to-int: use pow2 operator (#7812) commit | commitdiff | tree
2021-12-16 yoni206int-to-bv: fail if one of the arguments has type real... commit | commitdiff | tree
2021-12-16 mudathirmahgoubAdd regression bags-of-bags-subtypes.smt2 (#7814) commit | commitdiff | tree
2021-12-16 Andres NoetzliExplicitly disallow `mkConst(Rational)` (#7818) commit | commitdiff | tree
2021-12-15 Andrew ReynoldsEnsure match terms are exhaustive in its type rule... commit | commitdiff | tree
2021-12-15 Aina Niemetzapi: Fix smt-lib code blocks and math in C++ docs.... commit | commitdiff | tree
2021-12-15 Andrew ReynoldsAdd trace to see inferences in final proof (#7813) commit | commitdiff | tree
2021-12-14 Andrew ReynoldsEliminate static calls to rewrite in strings (#7803) commit | commitdiff | tree
2021-12-14 mudathirmahgoubFix cvc5-projects issue 358 (#7804) commit | commitdiff | tree
2021-12-14 Abdalrhman... Add a random Sygus enumerator. (#7782) commit | commitdiff | tree
2021-12-14 Gereon KremerMake some undocumented options regular/expert (#7805) commit | commitdiff | tree
2021-12-14 Gereon KremerFix issues with tracing builds (#7809) commit | commitdiff | tree
2021-12-14 Andres NoetzliAdd switches to toggle eager and inclusion solvers... commit | commitdiff | tree
2021-12-14 Andrew ReynoldsConnecting the core array solver in strings (#7800) commit | commitdiff | tree
2021-12-14 Andrew ReynoldsMinor fix for sygus unsat query generator (#7811) commit | commitdiff | tree
2021-12-14 Andrew ReynoldsThrow exception for getting value of non-well-founded... commit | commitdiff | tree
2021-12-14 Andrew ReynoldsEliminate use of rewrite, CONST_RATIONAL in ArithMSum... commit | commitdiff | tree
2021-12-14 Aina Niemetzapi: Add note to Solver::mkDatatypeSorts. (#7799) commit | commitdiff | tree
2021-12-13 Andrew ReynoldsDistinguishing more uses of CONST_RATIONAL (#7802) commit | commitdiff | tree
2021-12-13 mudathirmahgoubA more efficient implementation for bag.card operator... commit | commitdiff | tree
2021-12-13 Andrew ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... commit | commitdiff | tree
2021-12-13 Andrew ReynoldsFixes and additions for API for parametric datatypes... commit | commitdiff | tree
2021-12-13 mudathirmahgoubUpdate Relations.java (#7796) commit | commitdiff | tree
2021-12-13 Gereon KremerImprove nonlinear solver (#7787) commit | commitdiff | tree
2021-12-13 yoni206Integrate new int-blaster (#7781) commit | commitdiff | tree
2021-12-13 mudathirmahgoubFix cvc5-projects issues #358 and #375 (#7743) commit | commitdiff | tree
2021-12-10 Aina Niemetzapi: Use 'note' constructs for API documentation. ... commit | commitdiff | tree
2021-12-10 Aina NiemetzReorganize declareDatatype unit tests. (#7767) commit | commitdiff | tree
2021-12-10 Andrew ReynoldsRefactor and fixes related to getSpecializedConstructor... commit | commitdiff | tree
2021-12-10 Ying ShengArray-inspired Sequence Solver - Adding the ArrayCoreSo... commit | commitdiff | tree
2021-12-10 Gereon KremerEliminate more static rewrites (#7786) commit | commitdiff | tree
2021-12-10 Gereon KremerSome cleanup around trace and debug (#7792) commit | commitdiff | tree
2021-12-10 Abdalrhman... Mute `define-fun` command generated for named terms... commit | commitdiff | tree
2021-12-10 Gereon KremerAllow for wildcards in `-t` (#7791) commit | commitdiff | tree
2021-12-10 Haniel Barbosa[proofs] Make LazyCDProofChain extend CDProof (#7726) commit | commitdiff | tree
2021-12-10 Haniel Barbosa[proofs] Add option to prune inputs from final proof... commit | commitdiff | tree
2021-12-09 Andrew ReynoldsConsider polarity in relevance manager (#7768) commit | commitdiff | tree
2021-12-09 Gereon KremerFix sine symmetry proof (#7783) commit | commitdiff | tree
2021-12-09 Andrew ReynoldsRemove a few static access to options in proof code... commit | commitdiff | tree
2021-12-09 Andrew ReynoldsDo not make SyGuS subsolver in unsat state after solvin... commit | commitdiff | tree
2021-12-09 Aina Niemetzapi: Add note to Sort::getTesterCodomainSort(). (#7776) commit | commitdiff | tree
2021-12-09 Mathias Preinertest: Remove CDList memory limit test. (#7777) commit | commitdiff | tree
2021-12-08 Andrew ReynoldsReturn bool for lemmaTheoryInference (#7773) commit | commitdiff | tree
2021-12-08 Gereon KremerRemove rewrites from iand and pow2 solvers (#7775) commit | commitdiff | tree
2021-12-08 Gereon KremerEliminate rewriter from transcendental solver (#7772) commit | commitdiff | tree
2021-12-08 Gereon KremerStatic options acceses again (#7771) commit | commitdiff | tree
2021-12-08 Andrew ReynoldsMake several regressions faster (#7769) commit | commitdiff | tree
2021-12-08 Andrew ReynoldsFix type rule for datatype updater for parametric sorts... commit | commitdiff | tree
2021-12-08 Gereon KremerTurn kinds in python API into a proper Enum (#7686) commit | commitdiff | tree
2021-12-08 Aina Niemetzapi: Improve documentation for getDatatypeParamSorts... commit | commitdiff | tree
2021-12-08 Aina Niemetzapi: Fix Sort::getDatatypeArity() for non-parametric... commit | commitdiff | tree
2021-12-08 Aina NiemetzFP: Remove static call to Rewriter. (#7765) commit | commitdiff | tree
2021-12-08 Gereon KremerImprove options tests (#7761) commit | commitdiff | tree
2021-12-07 Gereon KremerRemove more static accesses to options (#7764) commit | commitdiff | tree
2021-12-07 Gereon KremerSimpler versioning if release flag is set (#7758) commit | commitdiff | tree
2021-12-07 Andrew ReynoldsAdd proof annotation option (#7750) commit | commitdiff | tree
2021-12-07 mudathirmahgoubFix some java documentation links (#7757) commit | commitdiff | tree
2021-12-07 Lachnitt[proofs] Alethe: Add ARITH_TRICHOTOMY to updater (... commit | commitdiff | tree
2021-12-07 Lachnitt[proofs] Alethe: Fix Bug in Finalize (#7746) commit | commitdiff | tree
2021-12-07 Andrew ReynoldsAllow sygus in incremental mode (#7756) commit | commitdiff | tree
2021-12-07 Andrew ReynoldsMake data structures in relevance manager SAT-context... commit | commitdiff | tree
2021-12-07 Andrew ReynoldsEliminate more static calls to Rewriter::rewrite (... commit | commitdiff | tree
next