projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix another rewrite involving iand (#8054)
[cvc5.git]
/
src
/
prop
/
2022-01-18
Andrew Reynolds
Print original form for substitutions and learned liter...
tree
|
commitdiff
2022-01-12
Andrew Reynolds
Add -o learned-lits to output learned literals (#7934)
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Remove unused shutdown infrastructure (#7872)
tree
|
commitdiff
2022-01-04
Haniel Barbosa
[proofs] [sat] Add manager for optimized clauses and...
tree
|
commitdiff
2022-01-03
Gereon Kremer
Remove static options from sat solver. (#7790)
tree
|
commitdiff
2021-12-16
Haniel Barbosa
[proofs] Simplifying and adding new utils to SAT proof...
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Initial cut at distinguishing uses of CONST_RATIONAL...
tree
|
commitdiff
2021-12-07
Gereon Kremer
Remove more static accesses to options (#7764)
tree
|
commitdiff
2021-12-02
Haniel Barbosa
[proofs] Fix a trace in SAT proof manager (#7732)
tree
|
commitdiff
2021-11-22
Haniel Barbosa
[prop] Remove unused #define in theory proxy (#7670)
tree
|
commitdiff
2021-11-18
Haniel Barbosa
[proofs] Fix trace in SatProofManager (#7664)
tree
|
commitdiff
2021-11-17
Haniel Barbosa
[sat] Fix indentation in "reason" (#7662)
tree
|
commitdiff
2021-11-12
Andres Noetzli
Remove `ConstantMap<Rational>` (#7635)
tree
|
commitdiff
2021-11-06
Gereon Kremer
Remove `Notice()` in favor of new `verbose()` (#7588)
tree
|
commitdiff
2021-11-05
Haniel Barbosa
[proofs] Fix open sat proof (#7509)
tree
|
commitdiff
2021-11-04
Andrew Reynolds
Replace the old dump infrastructure (#7572)
tree
|
commitdiff
2021-11-01
Mathias Preiner
bv: Remove layered solver. (#7455)
tree
|
commitdiff
2021-10-26
Haniel Barbosa
[proofs] Reset local var in SatProofManager since incre...
tree
|
commitdiff
2021-10-21
Haniel Barbosa
[proofs] Fix open proof in SAT solver due to cycles...
tree
|
commitdiff
2021-10-11
Aina Niemetz
Rename SmtScope to SolverEngineScope. (#7284)
tree
|
commitdiff
2021-10-08
Andrew Reynolds
Make skolem definition manager robust to function skole...
tree
|
commitdiff
2021-10-08
Andrew Reynolds
Add argument to distinguish lemmas and input assertions...
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Use skolem lemma in prop layer interfaces (#7320)
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Eliminate more circular dependencies on solver engine...
tree
|
commitdiff
2021-10-06
Andrew Reynolds
Refactor skolem definitions notifications for the decis...
tree
|
commitdiff
2021-10-04
Andrew Reynolds
Make decision engine use env (#7300)
tree
|
commitdiff
2021-10-01
Andrew Reynolds
Update theory preprocessor to use Env (#7288)
tree
|
commitdiff
2021-10-01
Aina Niemetz
Rename SmtEngine to SolverEngine. (#7282)
tree
|
commitdiff
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
next