projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
arrays: Move type enumerator implementation to .cpp. (#7216)
[cvc5.git]
/
src
/
prop
/
2021-09-14
Andrew Reynolds
Add get-difficulty to the API (#7194)
tree
|
commitdiff
2021-09-02
Andrew Reynolds
Implement lazy proof checking modes (#7106)
tree
|
commitdiff
2021-09-01
Haniel Barbosa
[proof] [sat] Fix lost reference to reason when process...
tree
|
commitdiff
2021-08-19
Haniel Barbosa
[unsat cores] [proofs] Revert test about when to explai...
tree
|
commitdiff
2021-08-18
Andrew Reynolds
Make TheoryProxy use Env, simplify initialization of...
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Remove dependencies on smt engine in smt solver (#6965)
tree
|
commitdiff
2021-07-14
Haniel Barbosa
[proof] Fix open proof issues in SAT proof (#6887)
tree
|
commitdiff
2021-07-13
Haniel Barbosa
[rewriter] Add rewrite to order IFF (equality for Boole...
tree
|
commitdiff
2021-07-09
Andrew Reynolds
Implement stop-only for new justification heuristic...
tree
|
commitdiff
2021-06-30
Mathias Preiner
Use SAT context level for --bv-assert-input instead...
tree
|
commitdiff
2021-06-21
Mathias Preiner
Move cnfConversionTime statistic to CnfStream. (#6769)
tree
|
commitdiff
2021-06-21
Mathias Preiner
Make CaDiCaL a required dependency. (#6761)
tree
|
commitdiff
2021-06-18
Mathias Preiner
Make CnfStream::toCNF iterative (#6757)
tree
|
commitdiff
2021-06-15
Gereon Kremer
Remove public option wrappers (#6716)
tree
|
commitdiff
2021-06-07
Gereon Kremer
Remove `Options::wasSetByUser()` (#6682)
tree
|
commitdiff
2021-05-27
Andrew Reynolds
Update proof namespaces (#6614)
tree
|
commitdiff
2021-05-27
Andrew Reynolds
Enable new justification heuristic by default (#6613)
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-20
Gereon Kremer
Properly initialize. (#6586)
tree
|
commitdiff
2021-05-20
Haniel Barbosa
Remove old unsat cores (#6581)
tree
|
commitdiff
2021-05-19
Mathias Preiner
Correctly handle negated assertions for assumption...
tree
|
commitdiff
2021-05-17
Andres Noetzli
Include cinttypes instead of inttypes.h (#6548)
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-05
Andrew Reynolds
Move current decision engine to decision engine old...
tree
|
commitdiff
2021-05-04
Andrew Reynolds
Move env into smt solver, theory engine, prop engine...
tree
|
commitdiff
2021-05-04
Haniel Barbosa
Do not use proof CNF stream with assumptions-based...
tree
|
commitdiff
2021-04-28
Gereon Kremer
Make sure reference stats are reset properly (#6457)
tree
|
commitdiff
2021-04-26
Gereon Kremer
First part of options refactoring (#6428)
tree
|
commitdiff
2021-04-26
Haniel Barbosa
Fix assertions in SAT solver (#6443)
tree
|
commitdiff
2021-04-24
Mathias Preiner
Add assumption-based unsat cores. (#6427)
tree
|
commitdiff
2021-04-23
Gereon Kremer
Make sure a ReferenceStat is set to values of the corre...
tree
|
commitdiff
2021-04-22
Andrew Reynolds
Reorganizing use of skolem definition manager in prop...
tree
|
commitdiff
2021-04-22
Haniel Barbosa
Reconciling proofs and unsat cores (#6405)
tree
|
commitdiff
2021-04-21
Mathias Preiner
Goodbye CVC4, hello cvc5! (#6371)
tree
|
commitdiff
2021-04-15
Mathias Preiner
Build support library from base and context. (#6368)
tree
|
commitdiff
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
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-14
Haniel Barbosa
[unsat-cores] Improving new unsat cores (#6356)
tree
|
commitdiff
2021-04-14
Haniel Barbosa
[proof-new] Fix explanation of literals in SAT proof...
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-12
Andrew Reynolds
Consolidate interface to prop engine (#6189)
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-09
Haniel Barbosa
[proof-new] Optimizing sat proof (#6324)
tree
|
commitdiff
2021-04-07
Haniel Barbosa
[proof-new] Fixing SMT post-processor's handling of...
tree
|
commitdiff
2021-04-06
Andres Noetzli
Remove template argument from `NodeBuilder` (#6290)
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-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
next