projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Reimplement support for relational triggers (#7063)
[cvc5.git] / src / theory / bv /
2021-10-12 Andrew ReynoldsEliminate calls to currentResourceManager (#7350) tree | commitdiff
2021-10-12 Aina NiemetzClean up occurrences of SmtEngine in comments. (#7349) tree | commitdiff
2021-10-11 Aina NiemetzRename SmtScope to SolverEngineScope. (#7284) tree | commitdiff
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) tree | commitdiff
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... tree | commitdiff
2021-09-30 Mathias Preinerbv: Refactor ppRewrite and move to TheoryBV. (#7271) tree | commitdiff
2021-09-14 Mathias Preinerbv: Unify bit-blasting code for udiv and urem. (#7188) tree | commitdiff
2021-09-14 Mathias Preinerproofs: Properly track pre- and post-rewrites in bbAtom... tree | commitdiff
2021-09-13 Andres NoetzliRemove context getters from `TheoryState` (#7174) tree | commitdiff
2021-09-11 Gereon KremerUse StatisticsRegistry from Env (#7166) tree | commitdiff
2021-09-11 Mathias Preinerbv: Move IsPowerOfTwo rule to preprocessing pass and... tree | commitdiff
2021-09-10 Mathias Preinerbv: Use EnvObj::rewrite() and EnvObj::options() in... tree | commitdiff
2021-09-10 Mathias Preinerbv: Use EnvObj::rewrite() and EnvObj::options() in... tree | commitdiff
2021-09-07 Andres NoetzliUse `EnvObj` methods instead of `Theory` methods (... tree | commitdiff
2021-08-31 Aina Niemetzbv: Remove dump=bv-rewrites. (#7099) tree | commitdiff
2021-08-31 yoni206bv-to-int-module: implementations and stubs for transla... tree | commitdiff
2021-08-24 yoni206bv-to-int: more implementations (#7051) tree | commitdiff
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012) tree | commitdiff
2021-08-16 Gereon KremerMake Theory class use Env (#7011) tree | commitdiff
2021-08-02 Mathias Preinerbv: Enable equality engine for bitblast-internal. ... tree | commitdiff
2021-07-27 Mathias Preinerbv: Refactor getEqualityStatus and use for both bitblas... tree | commitdiff
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904) tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename BBSimple to NodeBitblaster. (#6891) tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename lazy solver to layered solver. (#6889) tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename simple solver to bitblast-internal. (#6888) tree | commitdiff
2021-07-14 Mathias Preinerbv: Add missing BV_EAGER_ATOM proof rule. (#6874) tree | commitdiff
2021-07-13 Mathias Preinerbv: Simplify BV_BITBLAST_* proof rules. (#6871) tree | commitdiff
2021-07-13 Mathias Preinerbv: Do not rewrite below BV leafs in BBProof's TConvPro... tree | commitdiff
2021-07-13 Mathias Preinerbv: Expand bitblast proof steps in the proof post proce... tree | commitdiff
2021-07-02 Mathias PreinerFix bv assert input reset assertions (#6820) tree | commitdiff
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead... tree | commitdiff
2021-06-29 Mathias PreinerFix statistics in AigBitblaster. (#6810) tree | commitdiff
2021-06-22 yoni206modular bv2int: Stubs and some implementations (#6760) tree | commitdiff
2021-06-21 Mathias PreinerFix model issues with --bitblast=eager. (#6753) tree | commitdiff
2021-06-21 Mathias PreinerMove cnfConversionTime statistic to CnfStream. (#6769) tree | commitdiff
2021-06-15 Gereon KremerRemove public option wrappers (#6716) tree | commitdiff
2021-06-11 Andrew ReynoldsRemove support for lazy BV extended function reductions... tree | commitdiff
2021-06-10 Andrew ReynoldsEnsure bv2nat and int2bv are not rewritten when using... tree | commitdiff
2021-06-04 Mathias Preinerbv: Enable bitblast solver by default. (#6660) tree | commitdiff
2021-05-27 Andres NoetzliReturn `REWRITE_AGAIN` after rewriting bvcomp (#6624) tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-21 Aina NiemetzBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589) tree | commitdiff
2021-05-19 Mathias Preinerbv: Add support for --bitblast=eager. (#6516) tree | commitdiff
2021-05-14 Mathias Preinerbv: Assert input facts on user-level 0. (#6515) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-06 Andrew ReynoldsUse constant folding for evaluating BV eager atom ... tree | commitdiff
2021-04-30 Mathias Preinerbv: Refactor ppAssert and move to TheoryBV. (#6470) tree | commitdiff
2021-04-23 Aina NiemetzBV: Add proof logging for bit-blasting. (#6373) tree | commitdiff
2021-04-22 Andrew ReynoldsMove expand definition from Theory to TheoryRewriter... tree | commitdiff
2021-04-21 Mathias PreinerGoodbye CVC4, hello cvc5! (#6371) tree | commitdiff
2021-04-20 Aina NiemetzBV: Move implementation of type rules from header to... tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-12 Gereon KremerRefactor resource manager (#6322) tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-05 Haniel Barbosa[proof-new] Registering proof checkers uniformly from... tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-29 yoni206Modular bv2int part 1 (#6212) tree | commitdiff
2021-03-19 Aina NiemetzBitVector: Change setBit to set the bit in place. ... tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Update ppRewrite to use skolem lemmas ... tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-06 Mathias PreinerRemove partial UDIV/UREM operators. (#6069) tree | commitdiff
2021-03-04 Aina NiemetzAdd initial bit-blaster for proof logging. (#6053) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-02 Mathias PreinerRemove non-ASCII characters from source files. (#6039) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-18 Gereon KremerAdd statistic for InferenceId to TheoryInferenceManager... tree | commitdiff
2021-02-18 Gereon KremerNew InferenceIds for BV theory (#5909) tree | commitdiff
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver... tree | commitdiff
2021-02-13 Mathias PreinerProperly set up equality engine for BV bitblast solver... tree | commitdiff
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect... tree | commitdiff
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) tree | commitdiff
2021-01-11 Andrew ReynoldsMerge theory registrar and theory proxy (#5758) tree | commitdiff
2020-12-23 Andrew ReynoldsAdd option to track and notify from CNF stream (#5708) tree | commitdiff
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672) tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting... tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-10-20 Andrew ReynoldsFix miscellaneous warnings (#5256) tree | commitdiff
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... tree | commitdiff
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181) tree | commitdiff
2020-10-01 Aina NiemetzBitVector: Extend interface of setBit to set it to... tree | commitdiff
2020-09-25 Haniel BarbosaCleaning and documenting cnf stream (#5134) tree | commitdiff
2020-09-22 Mathias PreinerAdd simple BV solver (#5065) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-15 Andres NoetzliFix ABC build (#5061) tree | commitdiff
2020-09-04 Andrew Reynolds(new theory) Update TheoryBV to new standard for collec... tree | commitdiff
2020-09-04 Mathias PreinerSplit lazy bit-vector solver from TheoryBV (#5009) tree | commitdiff
2020-09-03 Gereon KremerAdded a new rule to simplify (bvugt (bvurem T x) x... tree | commitdiff
2020-09-03 Andrew ReynoldsMake ExtTheory independent of Theory (#5010) tree | commitdiff
next