projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
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
2021-12-07 Andrew ReynoldsTowards support for incremental sygus (#7736) commit | commitdiff | tree
2021-12-07 Andrew ReynoldsEliminate more static calls to Rewriter::rewrite (... commit | commitdiff | tree
2021-12-07 makaimannAdd bitwise option to IntBlaster (#7721) commit | commitdiff | tree
2021-12-07 Gereon KremerFix 32bit issue in sep_log_api test (#7752) commit | commitdiff | tree
2021-12-07 mudathirmahgoubAdd documentation for QuickStart.java (#7730) commit | commitdiff | tree
2021-12-06 Gereon KremerDisable option regression for competition build (#7751) commit | commitdiff | tree
2021-12-06 Gereon KremerUse unique_ptr instead of raw pointers (#7749) commit | commitdiff | tree
2021-12-06 Andrew ReynoldsAdd regressions for fixed projects issues (#7739) commit | commitdiff | tree
2021-12-04 Gereon KremerMore robust fix for 32bit issues. (#7735) commit | commitdiff | tree
2021-12-03 Lachnitt[proofs] Alethe: Implementation of Process Function... commit | commitdiff | tree
2021-12-03 Aina Niemetzapi: Fix docs for TUPLE_PROJECT. (#7741) commit | commitdiff | tree
2021-12-03 Andres NoetzliFaster hasing for `cvc5::String` (#7742) commit | commitdiff | tree
2021-12-03 Gereon KremerFix a few broken links (#7734) commit | commitdiff | tree
2021-12-03 Andrew ReynoldsCheck constructor is used in APPLY_CONSTRUCTOR (#7737) commit | commitdiff | tree
2021-12-03 Andrew ReynoldsProper error for using constructor in multiple datatype... commit | commitdiff | tree
2021-12-02 Gereon KremerAdd explicit 64bit getters for Integer class (#7728) commit | commitdiff | tree
2021-12-02 Gereon KremerRemove void as possible option type (#7731) commit | commitdiff | tree
2021-12-02 Gereon KremerCheck docs for broken links before uploading (#7729) commit | commitdiff | tree
2021-12-02 Andrew ReynoldsFixes for sygus-rr-synth-input (#7716) commit | commitdiff | tree
2021-12-02 Haniel Barbosa[proofs] Fix a trace in SAT proof manager (#7732) commit | commitdiff | tree
2021-12-02 mudathirmahgoubadd bag.fold operator (#7718) commit | commitdiff | tree
2021-12-02 Gereon KremerAdd unit tests for api::Solver::setOption() (#7708) commit | commitdiff | tree
2021-12-01 Mathias Preinerapi: Add missing bit-width 0 check to mkBVFromStrHelper... commit | commitdiff | tree
2021-12-01 Haniel Barbosa[proofs] Add method to CDProof to obtain number of... commit | commitdiff | tree
2021-12-01 Lachnitt[proofs] Alethe: Add finalize function to insert missin... commit | commitdiff | tree
2021-12-01 Andrew ReynoldsImprovements for get-difficulty (#7720) commit | commitdiff | tree
2021-12-01 Gereon KremerAdd the first example for z3pycompat (#7722) commit | commitdiff | tree
2021-12-01 mudathirmahgoubEnable Java examples (#7702) commit | commitdiff | tree
2021-12-01 LachnittAlethe: Add function that adds final steps to proof... commit | commitdiff | tree
2021-12-01 yoni206Translating API tests to Python — part 2 (#7651) commit | commitdiff | tree
2021-12-01 Gereon KremerUse new token for docs-release (#7709) commit | commitdiff | tree
2021-12-01 Andrew ReynoldsRemove spurious assertion in parser (#7713) commit | commitdiff | tree
2021-12-01 Andrew ReynoldsDefine sort undeclared (#7714) commit | commitdiff | tree
2021-11-30 yoni206Translating more cpp API unit tests to python (#7669) commit | commitdiff | tree
next