summaryrefslogtreecommitdiff
path: root/src/rewriter/mkrewrites.py
AgeCommit message (Expand)Author
2021-10-05tmpproof-new-dslAndres Noetzli
2021-07-07[DSL] Add support for isFixedPoint flagAndres Noetzli
2021-06-29[DSL] Evaluate integer constantsAndres Noetzli
2021-06-29Rewriter as oracle for eager pruning, add more rules, down to 127 unproven on...ajreynol
2021-06-28[DSL] Fix `App` comparison, make CSE more strictAndres Noetzli
2021-06-28[DSL] Support for RegLan and check for list varsAndres Noetzli
2021-06-28Move to nary term utilajreynol
2021-06-27Sketching term utilities for list semantics, generalize term canonizer, fixesajreynol
2021-06-27Separate term utilajreynol
2021-06-25[DSL] List attributesAndres Noetzli
2021-06-25[DSL] Support for more operatorsAndres Noetzli
2021-06-25[DSL] Check for unused variablesAndres Noetzli
2021-06-25Merge branch 'proof-new' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-06-25Add a few more dsl rules for Amazon benchmarkajreynol
2021-06-25Arith rulesAndres Noetzli
2021-06-25[DSL] Support integer constantsAndres Noetzli
2021-06-25A handful of important DSL rulesajreynol
2021-06-25Real sort, add basic arithmetic eq rules to DSLajreynol
2021-06-25Update internal string kinds, add support for str.replace to DSL to testajreynol
2021-06-24Move rewriterAndres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback