summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-12-17Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)Andres Noetzli
2021-12-17Minor refactoring of API for eliminating arithmetic subtypes (#7833)Andrew Reynolds
2021-12-17Fix tracker in SubstitutionMap (#7829)Gereon Kremer
2021-12-17Remove Rewriter::rewrite from bags type enumerator (#7827)mudathirmahgoub
2021-12-17Refactoring initialization of proofs (#7834)Andrew Reynolds
2021-12-17Add relations.cpp, relations.py examples (#7801)mudathirmahgoub
2021-12-17More documentation for idiomatic python API (#7798)Alex Ozdemir
2021-12-17Get getRealOrIntegerValueSign to the API (#7832)Andrew Reynolds
2021-12-17Implement model construction for the array extension of sequences (#7815)Andrew Reynolds
2021-12-16api: Rename DatatypeSelector::getRangeSort() to getCodomainSort(). (#7831)Aina Niemetz
2021-12-17api: Add Solver::mkUnresolvedSort(). (#7817)Aina Niemetz
2021-12-17Eliminate more uses of CONST_RATIONAL (#7816)Andrew Reynolds
2021-12-16Disable unsat cores for quaternion_ds1_symm_0428.fof.smt2. (#7830)Mathias Preiner
2021-12-16Eliminate most static calls to rewrite in quantifiers (#7823)Andrew Reynolds
2021-12-16Fix get-model when sort constructors are present (#7828)Andrew Reynolds
2021-12-16[proofs] Simplifying and adding new utils to SAT proof manager and Proof Cnf ...Haniel Barbosa
2021-12-16api: Add Sort::hasSymbol() and Sort::getSymbol(). (#7825)Aina Niemetz
2021-12-16Minor fix for print benchmark. (#7821)Andrew Reynolds
2021-12-16bv-to-int: use pow2 operator (#7812)yoni206
2021-12-16int-to-bv: fail if one of the arguments has type real (#7810)yoni206
2021-12-16Add regression bags-of-bags-subtypes.smt2 (#7814)mudathirmahgoub
2021-12-16Explicitly disallow `mkConst(Rational)` (#7818)Andres Noetzli
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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback