projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
bv: Add support for --bitblast=eager. (#6516)
[cvc5.git]
/
src
/
smt
/
set_defaults.cpp
2021-05-19
Mathias Preiner
bv: Add support for --bitblast=eager. (#6516)
blob
|
commitdiff
|
raw
2021-05-17
Gereon Kremer
Improve integration of CAD with nl-Ext (#6542)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-26
Gereon Kremer
First part of options refactoring (#6428)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-23
Andrew Reynolds
Enable strings exp by default for strings specific...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-22
Andrew Reynolds
Minor changes to unsat core default setting (#6425)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-22
Haniel Barbosa
Reconciling proofs and unsat cores (#6405)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-14
Haniel Barbosa
[unsat-cores] Improving new unsat cores (#6356)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-10
Aina Niemetz
Rename CVC4_ macros to CVC5_. (#6327)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-05
Andrew Reynolds
Enable UF when pre-skolem nested option is enabled...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-25
Gereon Kremer
Add missing includes. (#6207)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-17
Andrew Reynolds
(proof-new) Fixes to set defaults (#6163)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-16
Haniel Barbosa
[proof-new] Activating proofs when dumping proofs ...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-16
Haniel Barbosa
[proof-new] Renaming proof option to be in sync with...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Andrew Reynolds
Remove logic request (#6089)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Andrew Reynolds
(proof-new) Minor fix and allow proof option (#6085)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-22
Andrew Reynolds
(proof-new) Change proof-new option to proof (#5955)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-17
Mathias Preiner
Add bit-level propagation support to BV bitblast solver...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-10
Andrew Reynolds
Remove track instantiations infrastructure (#5883)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-03
Mathias Preiner
Add BV solver bitblast. (#5851)
blob
|
commitdiff
|
raw
|
diff to current
2021-01-29
Haniel Barbosa
[proof-new] Connecting new unsat cores (#5834)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-24
Haniel Barbosa
[proof-new] Only use old proofs for unsat cores if...
blob
|
commitdiff
|
raw
|
diff to current
2020-12-23
Andrew Reynolds
Remove quant EPR option (#5716)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-22
Andrew Reynolds
Remove preregister instantiation heuristic (#5713)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-16
Andrew Reynolds
Simplify preprocessing (#5647)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-15
Andrew Reynolds
Remove bv divide by zero option (#5672)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-07
Andrew Reynolds
Fix issue with free variables introduced by quantifier...
blob
|
commitdiff
|
raw
|
diff to current
2020-12-03
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-11-19
Andrew Reynolds
Enable new implementation of CEGQI based on nested...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-27
Gereon Kremer
Disable --nl-cad option by default (#5350)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-27
Gereon Kremer
Enable --nl-cad by default (#5345)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-22
Gereon Kremer
Use theoryof-mode=type for QF_NRA (#5326)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-12
Andrew Reynolds
Ensure uninterpreted sort owner is UF if uf-ho or finit...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-05
Andrew Reynolds
Make sygus more robust to unknown responses in solution...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-02
Gereon Kremer
Allow for theory combination of strings with nonlinear...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-23
Andrew Reynolds
Disable cegqi-bv when using sygus (#5124)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-23
Andrew Reynolds
Allow E-matching by default when strings are enabled...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
Mathias Preiner
Add simple BV solver (#5065)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
mudathirmahgoub
Add skeleton for theory of bags (multisets) (#5100)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-08
Andres Noetzli
Make CVC/API BV div/mod semantics match SMT-LIB (#4997)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-08
Andrew Reynolds
Eliminate a custom use of TheorySep in quantifiers...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-28
yoni206
Incremental support for bv_to_int (#4967)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-21
Andrew Reynolds
Connect the relevance manager to TheoryEngine and use...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-21
Andrew Reynolds
Remove BV equality slicer (#4928)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-28
Andrew Reynolds
Remove arrays lazy rintro option (#4806)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-14
Andrew Reynolds
Make use of options in setDefaults more consistent...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-11
yoni206
Changing bv_to_int options (#4721)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-08
Andrew Reynolds
Always interleave theory combination with quantifiers...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-30
Ying Sheng
Interpolation step 1 (#4638)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-25
Andrew Reynolds
Update option --nl-ext to enable/disable incremental...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-23
Mathias Preiner
Add support for eqrange predicate (#4562)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-22
Andrew Reynolds
(proof-new) Add proof-new to options file (#4641)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-19
yoni206
Bv to int elimination bugfix (#4435)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-06-03
Andrew Reynolds
Use prenex normal form when using cegqi-nested-qe ...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-01
Andres Noetzli
Set theoryof-mode after theory widening (#4545)
blob
|
commitdiff
|
raw
|
diff to current
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
blob
|
commitdiff
|
raw
|
diff to current
2020-05-20
Andrew Reynolds
Use debug-check-model to enable internal debugging...
blob
|
commitdiff
|
raw
|
diff to current
2020-05-12
Andrew Reynolds
Do not enable unconstrained simplification if arithmeti...
blob
|
commitdiff
|
raw
|
diff to current
2020-04-22
Andrew Reynolds
Allow eager bitblasting with solve bv as int in QF_NIA...
blob
|
commitdiff
|
raw
|
diff to current
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-17
Mathias Preiner
SyGuS instantiation quantifiers module (#3910)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-15
Andrew Reynolds
Always assign function values in higher order (#4279)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-15
Andrew Reynolds
Disable preregistration of instantiations for cegqi...
blob
|
commitdiff
|
raw
|
diff to current
2020-04-14
Andrew Reynolds
Disable macros when higher-order (#4266)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-09
Andrew Reynolds
Split ProcessAssertions module from SmtEngine (#4210)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-06
Andrew Reynolds
Remove links field in all toml files (#4201)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-27
Andrew Reynolds
Move set defaults function to its own file (#4154)
blob
|
commitdiff
|
raw
|
diff to current