projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Reimplement support for relational triggers (#7063)
[cvc5.git]
/
src
/
theory
/
bv
/
2021-10-12
Andrew Reynolds
Eliminate calls to currentResourceManager (#7350)
tree
|
commitdiff
2021-10-12
Aina Niemetz
Clean up occurrences of SmtEngine in comments. (#7349)
tree
|
commitdiff
2021-10-11
Aina Niemetz
Rename SmtScope to SolverEngineScope. (#7284)
tree
|
commitdiff
2021-10-01
Aina Niemetz
Rename SmtEngine to SolverEngine. (#7282)
tree
|
commitdiff
2021-09-30
Aina Niemetz
Rename files smt_engine.(cpp|h) to solver_engine.(cpp...
tree
|
commitdiff
2021-09-30
Mathias Preiner
bv: Refactor ppRewrite and move to TheoryBV. (#7271)
tree
|
commitdiff
2021-09-14
Mathias Preiner
bv: Unify bit-blasting code for udiv and urem. (#7188)
tree
|
commitdiff
2021-09-14
Mathias Preiner
proofs: Properly track pre- and post-rewrites in bbAtom...
tree
|
commitdiff
2021-09-13
Andres Noetzli
Remove context getters from `TheoryState` (#7174)
tree
|
commitdiff
2021-09-11
Gereon Kremer
Use StatisticsRegistry from Env (#7166)
tree
|
commitdiff
2021-09-11
Mathias Preiner
bv: Move IsPowerOfTwo rule to preprocessing pass and...
tree
|
commitdiff
2021-09-10
Mathias Preiner
bv: Use EnvObj::rewrite() and EnvObj::options() in...
tree
|
commitdiff
2021-09-10
Mathias Preiner
bv: Use EnvObj::rewrite() and EnvObj::options() in...
tree
|
commitdiff
2021-09-07
Andres Noetzli
Use `EnvObj` methods instead of `Theory` methods (...
tree
|
commitdiff
2021-08-31
Aina Niemetz
bv: Remove dump=bv-rewrites. (#7099)
tree
|
commitdiff
2021-08-31
yoni206
bv-to-int-module: implementations and stubs for transla...
tree
|
commitdiff
2021-08-24
yoni206
bv-to-int: more implementations (#7051)
tree
|
commitdiff
2021-08-17
Gereon Kremer
Push Env class into TheoryState (#7012)
tree
|
commitdiff
2021-08-16
Gereon Kremer
Make Theory class use Env (#7011)
tree
|
commitdiff
2021-08-02
Mathias Preiner
bv: Enable equality engine for bitblast-internal. ...
tree
|
commitdiff
2021-07-27
Mathias Preiner
bv: Refactor getEqualityStatus and use for both bitblas...
tree
|
commitdiff
2021-07-23
Aina Niemetz
FP: Add option to word-blast more lazily. (#6904)
tree
|
commitdiff
2021-07-15
Mathias Preiner
bv: Rename BBSimple to NodeBitblaster. (#6891)
tree
|
commitdiff
2021-07-15
Mathias Preiner
bv: Rename lazy solver to layered solver. (#6889)
tree
|
commitdiff
2021-07-15
Mathias Preiner
bv: Rename simple solver to bitblast-internal. (#6888)
tree
|
commitdiff
2021-07-14
Mathias Preiner
bv: Add missing BV_EAGER_ATOM proof rule. (#6874)
tree
|
commitdiff
2021-07-13
Mathias Preiner
bv: Simplify BV_BITBLAST_* proof rules. (#6871)
tree
|
commitdiff
2021-07-13
Mathias Preiner
bv: Do not rewrite below BV leafs in BBProof's TConvPro...
tree
|
commitdiff
2021-07-13
Mathias Preiner
bv: Expand bitblast proof steps in the proof post proce...
tree
|
commitdiff
2021-07-02
Mathias Preiner
Fix bv assert input reset assertions (#6820)
tree
|
commitdiff
2021-06-30
Mathias Preiner
Use SAT context level for --bv-assert-input instead...
tree
|
commitdiff
2021-06-29
Mathias Preiner
Fix statistics in AigBitblaster. (#6810)
tree
|
commitdiff
2021-06-22
yoni206
modular bv2int: Stubs and some implementations (#6760)
tree
|
commitdiff
2021-06-21
Mathias Preiner
Fix model issues with --bitblast=eager. (#6753)
tree
|
commitdiff
2021-06-21
Mathias Preiner
Move cnfConversionTime statistic to CnfStream. (#6769)
tree
|
commitdiff
2021-06-15
Gereon Kremer
Remove public option wrappers (#6716)
tree
|
commitdiff
2021-06-11
Andrew Reynolds
Remove support for lazy BV extended function reductions...
tree
|
commitdiff
2021-06-10
Andrew Reynolds
Ensure bv2nat and int2bv are not rewritten when using...
tree
|
commitdiff
2021-06-04
Mathias Preiner
bv: Enable bitblast solver by default. (#6660)
tree
|
commitdiff
2021-05-27
Andres Noetzli
Return `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 Reynolds
Move proof utilities to src/proof/ (#6611)
tree
|
commitdiff
2021-05-21
Aina Niemetz
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
tree
|
commitdiff
2021-05-19
Mathias Preiner
bv: Add support for --bitblast=eager. (#6516)
tree
|
commitdiff
2021-05-14
Mathias Preiner
bv: Assert input facts on user-level 0. (#6515)
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
tree
|
commitdiff
2021-05-06
Andrew Reynolds
Use constant folding for evaluating BV eager atom ...
tree
|
commitdiff
2021-04-30
Mathias Preiner
bv: Refactor ppAssert and move to TheoryBV. (#6470)
tree
|
commitdiff
2021-04-23
Aina Niemetz
BV: Add proof logging for bit-blasting. (#6373)
tree
|
commitdiff
2021-04-22
Andrew Reynolds
Move expand definition from Theory to TheoryRewriter...
tree
|
commitdiff
2021-04-21
Mathias Preiner
Goodbye CVC4, hello cvc5! (#6371)
tree
|
commitdiff
2021-04-20
Aina Niemetz
BV: Move implementation of type rules from header to...
tree
|
commitdiff
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
tree
|
commitdiff
2021-04-14
Aina Niemetz
Rename public and private headers in src/include. ...
tree
|
commitdiff
2021-04-12
Gereon Kremer
Refactor resource manager (#6322)
tree
|
commitdiff
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
tree
|
commitdiff
2021-04-10
Aina Niemetz
Rename CVC4_ macros to CVC5_. (#6327)
tree
|
commitdiff
2021-04-09
Aina Niemetz
Rename CVC4__ header guards to CVC5__. (#6326)
tree
|
commitdiff
2021-04-07
Andrew Reynolds
Replace calls to NodeManager::mkSkolem with SkolemManag...
tree
|
commitdiff
2021-04-06
Andres Noetzli
Remove 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 Niemetz
Rename namespace CVC5 to cvc5. (#6258)
tree
|
commitdiff
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
tree
|
commitdiff
2021-03-29
yoni206
Modular bv2int part 1 (#6212)
tree
|
commitdiff
2021-03-19
Aina Niemetz
BitVector: Change setBit to set the bit in place. ...
tree
|
commitdiff
2021-03-11
Gereon Kremer
First 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 Kremer
Some more cleanup of includes (#6083)
tree
|
commitdiff
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
tree
|
commitdiff
2021-03-06
Mathias Preiner
Remove partial UDIV/UREM operators. (#6069)
tree
|
commitdiff
2021-03-04
Aina Niemetz
Add initial bit-blaster for proof logging. (#6053)
tree
|
commitdiff
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
tree
|
commitdiff
2021-03-02
Mathias Preiner
Remove non-ASCII characters from source files. (#6039)
tree
|
commitdiff
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
tree
|
commitdiff
2021-02-18
Gereon Kremer
Add statistic for InferenceId to TheoryInferenceManager...
tree
|
commitdiff
2021-02-18
Gereon Kremer
New InferenceIds for BV theory (#5909)
tree
|
commitdiff
2021-02-17
Mathias Preiner
Add bit-level propagation support to BV bitblast solver...
tree
|
commitdiff
2021-02-13
Mathias Preiner
Properly set up equality engine for BV bitblast solver...
tree
|
commitdiff
2021-02-11
Gereon Kremer
Make most methods of TheoryInferenceManager expect...
tree
|
commitdiff
2021-02-03
Mathias Preiner
Add BV solver bitblast. (#5851)
tree
|
commitdiff
2021-01-11
Andrew Reynolds
Merge theory registrar and theory proxy (#5758)
tree
|
commitdiff
2020-12-23
Andrew Reynolds
Add option to track and notify from CNF stream (#5708)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Remove bv divide by zero option (#5672)
tree
|
commitdiff
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
tree
|
commitdiff
2020-12-08
Mathias Preiner
Add support for BV proofs with the simple bitblasting...
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Do not expand theory definitions at the beginning of...
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-10-20
Andrew Reynolds
Fix miscellaneous warnings (#5256)
tree
|
commitdiff
2020-10-06
Andrew Reynolds
(proof-new) Add interface for trusted substitution...
tree
|
commitdiff
2020-10-03
Andrew Reynolds
Standardization of Theory (#5181)
tree
|
commitdiff
2020-10-01
Aina Niemetz
BitVector: Extend interface of setBit to set it to...
tree
|
commitdiff
2020-09-25
Haniel Barbosa
Cleaning and documenting cnf stream (#5134)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Add simple BV solver (#5065)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-16
Abdalrhman Mohamed
Dump commands in internal code using command printing...
tree
|
commitdiff
2020-09-15
Andres Noetzli
Fix 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 Preiner
Split lazy bit-vector solver from TheoryBV (#5009)
tree
|
commitdiff
2020-09-03
Gereon Kremer
Added a new rule to simplify (bvugt (bvurem T x) x...
tree
|
commitdiff
2020-09-03
Andrew Reynolds
Make ExtTheory independent of Theory (#5010)
tree
|
commitdiff
next