projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-01-05 Aina Niemetzcppapi: Remove Datatype::hasNestedRecursion(). (#7878) commit | commitdiff | tree
2022-01-05 Alex OzdemirPy idiomatic API: Doc sets, datatypes, FP (#7877) commit | commitdiff | tree
2022-01-05 Aina Niemetzapi: Add missing guard for Datatype::isFinite(). (... commit | commitdiff | tree
2022-01-05 Andrew ReynoldsProperly parse arithmetic values (#7876) commit | commitdiff | tree
2022-01-05 Andrew ReynoldsTrack input list for atoms in difficulty manager (... commit | commitdiff | tree
2022-01-05 Alex OzdemirDon't use python's collections.Set (#7875) commit | commitdiff | tree
2022-01-05 yoni206Properly set __file__ in python bindings (#7867) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsFix proofs for datatype purify (#7841) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsChange default granularity of proofs to macro (#7855) commit | commitdiff | tree
2022-01-04 Aina NiemetzReorder NodeManager class according to code guidelines... commit | commitdiff | tree
2022-01-04 Andrew ReynoldsAdd utility expr::isBooleanConnective (#7869) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsRemove spurious call to applySubs (#7871) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsFix int blaster (#7856) commit | commitdiff | tree
2022-01-04 mudathirmahgoubAdd bag.member operator to theory of bags (#7857) commit | commitdiff | tree
2022-01-04 Haniel Barbosa[proofs] [sat] Add manager for optimized clauses and... commit | commitdiff | tree
2022-01-04 mudathirmahgoubRefactor bag solver (#7770) commit | commitdiff | tree
2022-01-04 yoni206Adding interpolation and abduction to the python API... commit | commitdiff | tree
2022-01-04 Aina Niemetzapi: Add unit test for null case of Sort::toString... commit | commitdiff | tree
2022-01-04 Aina Niemetzapi: Remove redundant check in Term::toString(). (... commit | commitdiff | tree
2022-01-03 Andrew ReynoldsUpdate quantifiers compute elim symbols to be iterative... commit | commitdiff | tree
2022-01-03 Andres Noetzli[BV] Remove non-existent `friend` class (#7864) commit | commitdiff | tree
2022-01-03 Gereon KremerAdd download link for examples in documentation (#7836) commit | commitdiff | tree
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
next