summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2022-01-07Update rewritermatthew-bellman-non-incMatthew Sotoudeh
2022-01-07BF non-incrementalMatthew Sotoudeh
2022-01-07Revert "Working on incremental solving"Matthew Sotoudeh
2022-01-06Working on incremental solvingMatthew Sotoudeh
2022-01-06Floyd-Warshall is betterMatthew Sotoudeh
2022-01-06Check in some scriptsMatthew Sotoudeh
2022-01-06Bellman-Ford don't try to return as many cyclesMatthew Sotoudeh
2022-01-05Timeouts on the new cycle-findingMatthew Sotoudeh
2022-01-05Better cycle findingMatthew Sotoudeh
2022-01-04Switch to Bellman-Ford, extract the negative cycle, use as conflictMatthew Sotoudeh
2022-01-04Use skolem var instead of constantMatthew Sotoudeh
2022-01-04Support asserts like (= x 5)Matthew Sotoudeh
2022-01-03Some formatting, remove sanitizersMatthew Sotoudeh
2022-01-03Initial workingMatthew Sotoudeh
2022-01-03Update projectAndres Noetzli
2022-01-03Add instructions for cluster runsAndres Noetzli
2022-01-03IDL solver starter projectAndres Noetzli
2021-12-23[Regressions] Support more complex scrubbers (#7819)Andres Noetzli
2021-12-22Remove most uses of mkRationalNode (#7854)Andrew Reynolds
2021-12-22Add support for incremental + interpolants (#7853)Andrew Reynolds
2021-12-21Support get-abduct-next (#7850)Andrew Reynolds
2021-12-21Eliminate remaining calls to callExtendedRewrite (#7839)Andrew Reynolds
2021-12-21Rewrite (pow2 x) to (pow 2 x) when x is a constant (#7849)yoni206
2021-12-21Disable unit tests without poly (#7844)Gereon Kremer
2021-12-20Connect sequences array solver to strategy in theory of strings (#7847)Andrew Reynolds
2021-12-20Eliminating some uses of const rational in arithmetic (#7846)Andrew Reynolds
2021-12-20Updates to LFSC signatures (#7840)Andrew Reynolds
2021-12-20Allow SyGuS subsolver to be reused in incremental mode (#7785)Andrew Reynolds
2021-12-20[Sequences/Array Solver] Minor refactoring (#7843)Andres Noetzli
2021-12-20[proofs] Fix helper LFSC script (#7845)Haniel Barbosa
2021-12-17api: java: Support default arity for Solver::mkUnresolvedSort(). (#7842)Aina Niemetz
2021-12-17[Strings] Minor fixes/improvements (#7837)Andres Noetzli
2021-12-17Array-inspired Sequence Solver - Fixing several issues in the ArrayCoreSolver...Ying Sheng
2021-12-17Simplify contrib/get-lfsc-checker and use cvc5 repo for LFSC signatures (#7835)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback