summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2022-01-11Fix bugs in reporting multiple cyclesmultiple-cycles-quickMatthew Sotoudeh
2022-01-11Report multiple conflicts when availableMatthew Sotoudeh
2022-01-11This seems to be the best of the past few commitsincremental-current-bestincremental-adj-for-dirtyMatthew Sotoudeh
2022-01-11Just the dirty bit and CSEMatthew Sotoudeh
2022-01-11Revert "Try storing adjacency list"Matthew Sotoudeh
2022-01-11Try storing adjacency listMatthew Sotoudeh
2022-01-11Try #1 for dirty nodesMatthew Sotoudeh
2022-01-10Use integer where easy toMatthew Sotoudeh
2022-01-10Avoid hash tablesMatthew Sotoudeh
2022-01-10Fix bug with incremental solverMatthew Sotoudeh
2022-01-07Propagate facts only at decision levelsMatthew Sotoudeh
2022-01-07Update rewriterMatthew Sotoudeh
2022-01-07Incremental Bellman-Ford implementation, seems to work fastMatthew Sotoudeh
2022-01-07Buggy incremental Floyd-WarshallMatthew 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback