summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-12-16Merge branch 'master' into deleteInvalidMkConstdeleteInvalidMkConstAndrew Reynolds
2021-12-15Ensure match terms are exhaustive in its type rule (#7807)Andrew Reynolds
2021-12-15api: Fix smt-lib code blocks and math in C++ docs. (#7795)Aina Niemetz
2021-12-15Explicitly disallow `mkConst(Rational)`Andres Noetzli
2021-12-15Add trace to see inferences in final proof (#7813)Andrew Reynolds
2021-12-14Eliminate static calls to rewrite in strings (#7803)Andrew Reynolds
2021-12-14Fix cvc5-projects issue 358 (#7804)mudathirmahgoub
2021-12-14Add a random Sygus enumerator. (#7782)Abdalrhman Mohamed
2021-12-14Make some undocumented options regular/expert (#7805)Gereon Kremer
2021-12-14Fix issues with tracing builds (#7809)Gereon Kremer
2021-12-14Add switches to toggle eager and inclusion solvers (#7784)Andres Noetzli
2021-12-14Connecting the core array solver in strings (#7800)Andrew Reynolds
2021-12-14Minor fix for sygus unsat query generator (#7811)Andrew Reynolds
2021-12-14Throw exception for getting value of non-well-founded datatype (#7806)Andrew Reynolds
2021-12-14Eliminate use of rewrite, CONST_RATIONAL in ArithMSum (#7808)Andrew Reynolds
2021-12-14api: Add note to Solver::mkDatatypeSorts. (#7799)Aina Niemetz
2021-12-13Distinguishing more uses of CONST_RATIONAL (#7802)Andrew Reynolds
2021-12-13A more efficient implementation for bag.card operator (#7797)mudathirmahgoub
2021-12-13Initial cut at distinguishing uses of CONST_RATIONAL (#7682)Andrew Reynolds
2021-12-13Fixes and additions for API for parametric datatypes (#7760)Andrew Reynolds
2021-12-13Update Relations.java (#7796)mudathirmahgoub
2021-12-13Improve nonlinear solver (#7787)Gereon Kremer
2021-12-13Integrate new int-blaster (#7781)yoni206
2021-12-13Fix cvc5-projects issues #358 and #375 (#7743)mudathirmahgoub
2021-12-10api: Use 'note' constructs for API documentation. (#7794)Aina Niemetz
2021-12-10Reorganize declareDatatype unit tests. (#7767)Aina Niemetz
2021-12-10Refactor and fixes related to getSpecializedConstructorTerm (#7774)Andrew Reynolds
2021-12-10Array-inspired Sequence Solver - Adding the ArrayCoreSolver class and options...Ying Sheng
2021-12-10Eliminate more static rewrites (#7786)Gereon Kremer
2021-12-10Some cleanup around trace and debug (#7792)Gereon Kremer
2021-12-10Mute `define-fun` command generated for named terms. (#7788)Abdalrhman Mohamed
2021-12-10Allow for wildcards in `-t` (#7791)Gereon Kremer
2021-12-10[proofs] Make LazyCDProofChain extend CDProof (#7726)Haniel Barbosa
2021-12-10[proofs] Add option to prune inputs from final proof (#7789)Haniel Barbosa
2021-12-09Consider polarity in relevance manager (#7768)Andrew Reynolds
2021-12-09Fix sine symmetry proof (#7783)Gereon Kremer
2021-12-09Remove a few static access to options in proof code (#7780)Andrew Reynolds
2021-12-09Do not make SyGuS subsolver in unsat state after solving (#7759)Andrew Reynolds
2021-12-08api: Add note to Sort::getTesterCodomainSort(). (#7776)Aina Niemetz
2021-12-09test: Remove CDList memory limit test. (#7777)Mathias Preiner
2021-12-08Return bool for lemmaTheoryInference (#7773)Andrew Reynolds
2021-12-08Remove rewrites from iand and pow2 solvers (#7775)Gereon Kremer
2021-12-08Eliminate rewriter from transcendental solver (#7772)Gereon Kremer
2021-12-08Static options acceses again (#7771)Gereon Kremer
2021-12-08Make several regressions faster (#7769)Andrew Reynolds
2021-12-08Fix type rule for datatype updater for parametric sorts (#7762)Andrew Reynolds
2021-12-08Turn kinds in python API into a proper Enum (#7686)Gereon Kremer
2021-12-08api: Improve documentation for getDatatypeParamSorts(). (#7763)Aina Niemetz
2021-12-08api: Fix Sort::getDatatypeArity() for non-parametric datatypes. (#7766)Aina Niemetz
2021-12-08FP: Remove static call to Rewriter. (#7765)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback