projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix spurious antecedant for symbolic regular expressions (#6284)
[cvc5.git]
/
src
/
prop
/
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-22
Andrew Reynolds
Add skolem definition manager (#6187)
tree
|
commitdiff
2021-03-16
Mathias Preiner
cmake: Generate cvc4_export.h and set visibility to...
tree
|
commitdiff
2021-03-16
Haniel Barbosa
[proof-new] Renaming proof option to be in sync with...
tree
|
commitdiff
2021-03-12
Andres Noetzli
Schedule preregistration lemmas to be satisfied after...
tree
|
commitdiff
2021-03-12
Gereon Kremer
Add missing includes for statistics (#6124)
tree
|
commitdiff
2021-03-11
Gereon Kremer
First refactoring of statistics classes (#6105)
tree
|
commitdiff
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
tree
|
commitdiff
2021-03-11
Mathias Preiner
Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)
tree
|
commitdiff
2021-03-10
Mathias Preiner
Use Assert instead of assert. (#6095)
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-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
tree
|
commitdiff
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
tree
|
commitdiff
2021-02-26
Haniel Barbosa
Some formatting and better tracing in prop engine ...
tree
|
commitdiff
2021-02-23
Haniel Barbosa
[proof-new] Fix dangling pointer in SAT proof generatio...
tree
|
commitdiff
2021-02-23
Haniel Barbosa
[proof-new] Fix handling of removable clauses in proof...
tree
|
commitdiff
2021-02-22
Andrew Reynolds
(proof-new) Change proof-new option to proof (#5955)
tree
|
commitdiff
2021-02-17
Mathias Preiner
Add bit-level propagation support to BV bitblast solver...
tree
|
commitdiff
2021-02-12
Andrew Reynolds
Simplify and fix decision engine's handling of skolem...
tree
|
commitdiff
2021-02-11
Haniel Barbosa
[proof-new] Adding a proof-producing ensure literal...
tree
|
commitdiff
2021-02-04
Haniel Barbosa
[proof-new] Catch trivial cycles in SAT proof generatio...
tree
|
commitdiff
2021-02-03
Mathias Preiner
Add BV solver bitblast. (#5851)
tree
|
commitdiff
2021-02-02
Andrew Reynolds
Cleanup some includes (#5847)
tree
|
commitdiff
2021-01-28
Andrew Reynolds
Simplify lemma interface (#5819)
tree
|
commitdiff
2021-01-28
Andrew Reynolds
Always theory-preprocess lemmas (#5817)
tree
|
commitdiff
2021-01-24
Andrew Reynolds
Add interface for getting preprocessed term (#5798)
tree
|
commitdiff
2021-01-11
Andrew Reynolds
Merge theory registrar and theory proxy (#5758)
tree
|
commitdiff
2021-01-06
Andrew Reynolds
Add new interfaces to term formula removal and theory...
tree
|
commitdiff
2021-01-05
Andrew Reynolds
Remove a few miscellaneous references to the expr layer...
tree
|
commitdiff
2020-12-24
Haniel Barbosa
[proof-new] Only use old proofs for unsat cores if...
tree
|
commitdiff
2020-12-23
Andrew Reynolds
Add option to track and notify from CNF stream (#5708)
tree
|
commitdiff
2020-12-21
Andrew Reynolds
Move ownership of theory preprocessor to TheoryProxy...
tree
|
commitdiff
2020-12-17
Haniel Barbosa
[proof-new] Only use old proof code for unsat cores...
tree
|
commitdiff
2020-12-14
Haniel Barbosa
[proof-new] Making the CDCL(T) Minisat proof producing...
tree
|
commitdiff
2020-12-14
Haniel Barbosa
[proof-new] Make prop engine proof producing (#5667)
tree
|
commitdiff
2020-12-14
Haniel Barbosa
[proof-new] Updating interfaces between prop engine...
tree
|
commitdiff
2020-12-11
Haniel Barbosa
[proof-new] Updating theory proxy to new proof infrast...
tree
|
commitdiff
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
tree
|
commitdiff
2020-12-09
Andrew Reynolds
Make decision engine independent of AssertionsPipeline...
tree
|
commitdiff
2020-12-08
Haniel Barbosa
[proof-new] Updating SAT proof to use MACRO_RESOLUTION...
tree
|
commitdiff
2020-12-07
Andrew Reynolds
(proof-new) Split proof ensure closed checks to own...
tree
|
commitdiff
2020-12-03
Andrew Reynolds
(proof-new) Updates to SMT proof manager and SmtEngine...
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-11-19
Aina Niemetz
Include stddef.h (needed for size_t) in cvc4_public...
tree
|
commitdiff
2020-11-16
Gereon Kremer
Improve accuracy of resource limitation (#4763)
tree
|
commitdiff
2020-11-09
Gereon Kremer
Properly clear interrupt for solve() as well. (#5403)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
(proof-new) Update add lazy step interface in LazyCDPro...
tree
|
commitdiff
2020-10-19
Haniel Barbosa
[proof-new] Fixing resolution proof checker (#5262)
tree
|
commitdiff
2020-10-14
Haniel Barbosa
using NOT_NOT_ELIM rather than macros to do double...
tree
|
commitdiff
2020-09-29
Haniel Barbosa
[proof-new] Adds a proof manager for prop engine (...
tree
|
commitdiff
2020-09-29
Haniel Barbosa
[proof-new] Adds a proof post processor for the Prop...
tree
|
commitdiff
2020-09-29
Haniel Barbosa
[proof-new] Adds a proof-producing CNF converter (...
tree
|
commitdiff
2020-09-29
Haniel Barbosa
[proof-new] Removing spurious forward declaration in...
tree
|
commitdiff
2020-09-28
Haniel Barbosa
[proof-new] Adds a proof manager for the SAT solver...
tree
|
commitdiff
2020-09-25
Haniel Barbosa
Cleaning and documenting cnf stream (#5134)
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-12
Andrew Reynolds
(proof-new) Update TheoryEngine lemma and conflict...
tree
|
commitdiff
2020-09-02
Andres Noetzli
Fix CryptoMiniSat build, regression (#5006)
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-09-01
FabianWolff
Fix spelling errors (#4977)
tree
|
commitdiff
2020-08-15
Andrew Reynolds
Add finishInit method to PropEngine (#4895)
tree
|
commitdiff
2020-07-30
Andres Noetzli
Python API: Add support for sequences (#4757)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-05-22
Aina Niemetz
CaDiCaL: Clean up initialization on creation. (#4516)
tree
|
commitdiff
2020-05-22
Aina Niemetz
Cryptominisat: Clean up initialization on creation...
tree
|
commitdiff
2020-05-22
Aina Niemetz
Add support for SAT solver Kissat. (#4514)
tree
|
commitdiff
2020-04-10
Andrew Reynolds
Towards proper use of resource managers (#4233)
tree
|
commitdiff
2020-03-31
Andrew Reynolds
Remove replay and use-theory options and idl (#4186)
tree
|
commitdiff
2020-03-27
Andres Noetzli
Fix issues with unsat cores and reset-assertions (...
tree
|
commitdiff
2020-03-11
Andres Noetzli
Set assertion in `CnfStream::ensureLiteral()` (#3927)
tree
|
commitdiff
2020-03-10
Aina Niemetz
Fix issue with reset-assertions. (#3988)
tree
|
commitdiff
2020-03-09
Andres Noetzli
Make registration of unit clauses more robust (#3965)
tree
|
commitdiff
2020-03-05
Aina Niemetz
Move ownership of DecisionEngine into PropEngine. ...
tree
|
commitdiff
2020-03-05
Aina Niemetz
Revert "Move ownership of DecisionEngine into PropEngin...
tree
|
commitdiff
2020-03-05
Andrew Reynolds
Move ownership of DecisionEngine into PropEngine. ...
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-29
Aina Niemetz
propEngine: Reorder class declaration according to...
tree
|
commitdiff
2020-02-26
Andres Noetzli
Remove portfolio leftovers (#3821)
tree
|
commitdiff
2020-02-22
makaimann
Dump boolean propagations and conflicts for decision...
tree
|
commitdiff
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
2019-12-16
makaimann
Trace tags for dumping the decision tree in org-mode...
tree
|
commitdiff
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-11-08
Mathias Preiner
cmake: Disable C++ GNU extensions. (#3446)
tree
|
commitdiff
2019-10-31
Mathias Preiner
Fix Unimplemented() macros missed in #3366. (#3424)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-09-07
Andrew Reynolds
Remove portfolio (#3236)
tree
|
commitdiff
2019-08-02
Mathias Preiner
Update CaDiCaL to version 1.0.3. (#3137)
tree
|
commitdiff
2019-07-02
Alex Ozdemir
Optimize DRAT optimization: clause matching (#3074)
tree
|
commitdiff
2019-05-18
Andres Noetzli
Support for incremental bit-blasting with CaDiCaL ...
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-04-05
Alex Ozdemir
SatClauseSetHashFunction (#2916)
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-01-23
Andres Noetzli
Avoid using ProofManager in non-proof CMS build (#2814)
tree
|
commitdiff
2019-01-14
Alex Ozdemir
ClausalBitvectorProof (#2786)
tree
|
commitdiff
2018-12-03
Alex Ozdemir
Bit vector proof superclass (#2599)
tree
|
commitdiff
2018-10-19
Mathias Preiner
Remove autotools build system. (#2639)
tree
|
commitdiff
next