summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
2021-11-04Replace the old dump infrastructure (#7572)Andrew Reynolds
2021-11-02bv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)Mathias Preiner
2021-11-02bv: Remove remaining Rewriter::rewrite calls. (#7545)Mathias Preiner
2021-11-01bv: Remove layered solver. (#7455)Mathias Preiner
2021-10-22Refactor theory inference manager constructor (#7457)Andrew Reynolds
2021-10-22Making `IntBlaster` inherit from `EnvObj` (#7431)yoni206
2021-10-12Eliminate calls to currentResourceManager (#7350)Andrew Reynolds
2021-10-12Clean up occurrences of SmtEngine in comments. (#7349)Aina Niemetz
2021-10-11Rename SmtScope to SolverEngineScope. (#7284)Aina Niemetz
2021-09-30Rename SmtEngine to SolverEngine. (#7282)Aina Niemetz
2021-09-30Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)Aina Niemetz
2021-09-30bv: Refactor ppRewrite and move to TheoryBV. (#7271)Mathias Preiner
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback