projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)
[cvc5.git]
/
src
/
prop
/
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
2018-10-01
Aina Niemetz
Fix compiler warnings. (#2555)
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Various CMakeLists.txt fixes/cleanup.
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Only build libcvc4 and libcvc4parser as libraries.
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Cleanup CMakeLists.txt files, remove SHARED.
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Working build infrastructure.
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-09-13
Mathias Preiner
Fix #include for minisat headers in bvminisat. (#2463)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Remove support for flipDecision (#2319)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Delete functions instead of using CVC4_UNDEFINED (...
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Remove references to deprecated propagate as decision...
tree
|
commitdiff
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
tree
|
commitdiff
2018-07-30
FabianWolff
Fix several spelling errors (#2231)
tree
|
commitdiff
2018-07-13
Andres Noetzli
Properly clean up assertion stack in CnfProof (#2147)
tree
|
commitdiff
2018-06-28
Andres Noetzli
Fix stale reference in MiniSat when generating UC ...
tree
|
commitdiff
2018-06-25
Aina Niemetz
Updated copyright headers.
tree
|
commitdiff
2018-06-13
Andres Noetzli
Workaround for incremental unsat cores (#1962)
tree
|
commitdiff
2018-06-09
Andres Noetzli
Reset decisions at SAT level after solving (#2059)
tree
|
commitdiff
2018-05-25
Andres Noetzli
MiniSat: Be more careful about running proof code ...
tree
|
commitdiff
2018-05-23
Andres Noetzli
Remove ProofProxy (#1965)
tree
|
commitdiff
2018-04-04
Andres Noetzli
[BVMiniSat] Avoid duplicates in conflicts (#1745)
tree
|
commitdiff
2018-03-26
Andres Noetzli
Fix memory leak in bvminisat (#1710)
tree
|
commitdiff
2018-03-20
Mathias Preiner
Add support for CaDiCaL as eager BV SAT solver. (#1675)
tree
|
commitdiff
2018-03-13
Mathias Preiner
Use Cryptominisat version 5.0.2 (instead of 4.2.0)...
tree
|
commitdiff
2018-03-09
Mathias Preiner
Cleanup Cryptominisat SAT wrapper. (#1652)
tree
|
commitdiff
2018-03-07
Mathias Preiner
Make statistics output consistent. (#1647)
tree
|
commitdiff
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
tree
|
commitdiff
2018-02-07
Mathias Preiner
Cleanup Cryptominisat header. (#1561)
tree
|
commitdiff
next