summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-07-09Make regression test `issue4971-0` more robustfixRegression4971Andres Noetzli
2021-07-09Use newer config.sub to fix build on Apple M1 (#6854)Andres Noetzli
2021-07-09Fix sets cardinality inference involving equivalent parents (#6855)Andrew Reynolds
2021-07-09Implement stop-only for new justification heuristic (#6847)Andrew Reynolds
2021-07-08Disable ordering heuristic for justification by default (#6848)Andrew Reynolds
2021-07-08Add script to build wheel for pycvc5 (#6839)makaimann
2021-07-08[proof] [dot] Print let map (of terms in proof) as part of dot proof (#6853)Haniel Barbosa
2021-07-07[unsat cores] Adding regressions from #4971 (#6852)Haniel Barbosa
2021-07-07pow2: Update NEWS. (#6851)Aina Niemetz
2021-07-07Rename operator pow2 to int.pow2. (#6849)Aina Niemetz
2021-07-07Fix regressions for competition build (#6846)Andrew Reynolds
2021-07-07Standard output for trigger selection (#6841)Andrew Reynolds
2021-07-06Integrate Lazard into CAD module (#6812)Gereon Kremer
2021-07-06Integrate learned rewrite preprocessing pass (#6840)Andrew Reynolds
2021-07-06Add implementation of learned rewrite pass (#6843)Andrew Reynolds
2021-07-06Add learned rewrite preprocessing pass (#6842)Andrew Reynolds
2021-07-06Porting C++ API examples to SMT-LIB examples (#6789)Haniel Barbosa
2021-07-05Add some printing functions for OptimizationObjective and OptimizationResult ...Ouyancheng
2021-07-05Add doc page about transcendentals (#6755)Gereon Kremer
2021-07-05[Strings] Fix incorrect rewrite (#6837)Andres Noetzli
2021-07-05Make buffered inference manager more robust to backtracking (#6833)Andrew Reynolds
2021-07-03Fix performance of string regression (#6832)Andres Noetzli
2021-07-03Add output tags -o, --output. (#6826)Mathias Preiner
2021-07-02Fix bv assert input reset assertions (#6820)Mathias Preiner
2021-07-02Fix rewriter for negative constant seq.nth (#6827)Andrew Reynolds
2021-07-02Fix CaDiCaL auto-download on macOS (#6828)Andres Noetzli
2021-07-02Refactor lexer for SMT-LIB in sphinx (#6805)Gereon Kremer
2021-07-02Add reverse iterators to `Node`/`TNode` (#6825)Andres Noetzli
2021-07-01Add recursive function definitions to subsolver in sygus (#6824)Andrew Reynolds
2021-07-01Fix message to show that cadical and symfpu are required (#6823)Gereon Kremer
2021-07-01Add option to limit the number of instantiation rounds (#6818)Andrew Reynolds
2021-06-30Use SAT context level for --bv-assert-input instead of decision level. (#6758)Mathias Preiner
2021-06-30Use authored date instead of commit date. (#6815)Gereon Kremer
2021-06-30pow2: new test (#6819)yoni206
2021-06-30Do not notify during equality engine initialization (#6817)Andrew Reynolds
2021-06-30Do not apply fmfBound to standard quantifiers when only stringsExp is enabled...Andrew Reynolds
2021-06-30Fix pre vs. post-rewrite in proofs for theory preprocessor (#6801)Andrew Reynolds
2021-06-30int-to-bv: correct model values (#6811)yoni206
2021-06-29Add new variants for the CAD projection (#6794)Gereon Kremer
2021-06-29Fix statistics in AigBitblaster. (#6810)Mathias Preiner
2021-06-29FP: Refactor, rewrite and clean up word blasting. (#6802)Aina Niemetz
2021-06-28Rewrite POW to POW2 when the base is 2 (#6806)yoni206
2021-06-28Rename internal string kinds to match API (#6797)Andrew Reynolds
2021-06-28Further fix #6453 (#6804)Ouyancheng
2021-06-28[proof] [dot] Make dot printer stateful (#6799)Haniel Barbosa
2021-06-25pow2 -- final changes (#6800)yoni206
2021-06-24pow2: Adding monotonicity lemma (#6793)yoni206
2021-06-24api: getRealValue: Fix printing of integer values. (#6795)Aina Niemetz
2021-06-24cmake: Add new code coverage targets. (#6796)Mathias Preiner
2021-06-24Fix linear arithmetic for duplicate lemmas in incremental (#6784)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback