summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
2021-09-14bv: Unify bit-blasting code for udiv and urem. (#7188)Mathias Preiner
2021-09-14proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147)Mathias Preiner
2021-09-13Remove context getters from `TheoryState` (#7174)Andres Noetzli
2021-09-11Use StatisticsRegistry from Env (#7166)Gereon Kremer
2021-09-11bv: Move IsPowerOfTwo rule to preprocessing pass and use EnvObj. (#7179)Mathias Preiner
2021-09-10bv: Use EnvObj::rewrite() and EnvObj::options() in NodeBitblaster. (#7172)Mathias Preiner
2021-09-10bv: Use EnvObj::rewrite() and EnvObj::options() in BvSolver. (#7171)Mathias Preiner
2021-09-07Use `EnvObj` methods instead of `Theory` methods (#7144)Andres Noetzli
2021-08-31bv: Remove dump=bv-rewrites. (#7099)Aina Niemetz
2021-08-31bv-to-int-module: implementations and stubs for translating operators (#7086)yoni206
2021-08-24bv-to-int: more implementations (#7051)yoni206
2021-08-16Push Env class into TheoryState (#7012)Gereon Kremer
2021-08-16Make Theory class use Env (#7011)Gereon Kremer
2021-08-02bv: Enable equality engine for bitblast-internal. (#6961)Mathias Preiner
2021-07-27bv: Refactor getEqualityStatus and use for both bitblasting solvers. (#6933)Mathias Preiner
2021-07-23FP: Add option to word-blast more lazily. (#6904)Aina Niemetz
2021-07-15bv: Rename BBSimple to NodeBitblaster. (#6891)Mathias Preiner
2021-07-15bv: Rename lazy solver to layered solver. (#6889)Mathias Preiner
2021-07-14bv: Rename simple solver to bitblast-internal. (#6888)Mathias Preiner
2021-07-13bv: Add missing BV_EAGER_ATOM proof rule. (#6874)Mathias Preiner
2021-07-13bv: Simplify BV_BITBLAST_* proof rules. (#6871)Mathias Preiner
2021-07-13bv: Do not rewrite below BV leafs in BBProof's TConvProofGenerator. (#6869)Mathias Preiner
2021-07-13bv: Expand bitblast proof steps in the proof post processor. (#6867)Mathias Preiner
2021-07-02Fix bv assert input reset assertions (#6820)Mathias Preiner
2021-06-30Use SAT context level for --bv-assert-input instead of decision level. (#6758)Mathias Preiner
2021-06-29Fix statistics in AigBitblaster. (#6810)Mathias Preiner
2021-06-22modular bv2int: Stubs and some implementations (#6760)yoni206
2021-06-21Fix model issues with --bitblast=eager. (#6753)Mathias Preiner
2021-06-21Move cnfConversionTime statistic to CnfStream. (#6769)Mathias Preiner
2021-06-15Remove public option wrappers (#6716)Gereon Kremer
2021-06-11Remove support for lazy BV extended function reductions and inferences (#6728)Andrew Reynolds
2021-06-10Ensure bv2nat and int2bv are not rewritten when using solve-bv-as-int (#6725)Andrew Reynolds
2021-06-04bv: Enable bitblast solver by default. (#6660)Mathias Preiner
2021-05-27Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)Andres Noetzli
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-19bv: Add support for --bitblast=eager. (#6516)Mathias Preiner
2021-05-14bv: Assert input facts on user-level 0. (#6515)Mathias Preiner
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-06Use constant folding for evaluating BV eager atom (#6494)Andrew Reynolds
2021-04-30bv: Refactor ppAssert and move to TheoryBV. (#6470)Mathias Preiner
2021-04-23BV: Add proof logging for bit-blasting. (#6373)Aina Niemetz
2021-04-22Move expand definition from Theory to TheoryRewriter (#6408)Andrew Reynolds
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
2021-04-20BV: Move implementation of type rules from header to .cpp. (#6360)Aina Niemetz
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor resource manager (#6322)Gereon Kremer
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback