projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add missing null terminators for regexp (#8027)
[cvc5.git] / src / prop /
2022-01-18 Andrew ReynoldsPrint original form for substitutions and learned liter... tree | commitdiff
2022-01-12 Andrew ReynoldsAdd -o learned-lits to output learned literals (#7934) tree | commitdiff
2022-01-04 Andrew ReynoldsRemove 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 KremerRemove 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 ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... tree | commitdiff
2021-12-07 Gereon KremerRemove 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 NoetzliRemove `ConstantMap<Rational>` (#7635) tree | commitdiff
2021-11-06 Gereon KremerRemove `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 ReynoldsReplace the old dump infrastructure (#7572) tree | commitdiff
2021-11-01 Mathias Preinerbv: 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 NiemetzRename SmtScope to SolverEngineScope. (#7284) tree | commitdiff
2021-10-08 Andrew ReynoldsMake skolem definition manager robust to function skole... tree | commitdiff
2021-10-08 Andrew ReynoldsAdd argument to distinguish lemmas and input assertions... tree | commitdiff
2021-10-07 Andrew ReynoldsUse skolem lemma in prop layer interfaces (#7320) tree | commitdiff
2021-10-07 Andrew ReynoldsEliminate more circular dependencies on solver engine... tree | commitdiff
2021-10-06 Andrew ReynoldsRefactor skolem definitions notifications for the decis... tree | commitdiff
2021-10-04 Andrew ReynoldsMake decision engine use env (#7300) tree | commitdiff
2021-10-01 Andrew ReynoldsUpdate theory preprocessor to use Env (#7288) tree | commitdiff
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) tree | commitdiff
2021-09-14 Andrew ReynoldsAdd get-difficulty to the API (#7194) tree | commitdiff
2021-09-02 Andrew ReynoldsImplement 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 ReynoldsMake TheoryProxy use Env, simplify initialization of... tree | commitdiff
2021-08-04 Andrew ReynoldsRemove 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 ReynoldsImplement stop-only for new justification heuristic... tree | commitdiff
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead... tree | commitdiff
2021-06-21 Mathias PreinerMove cnfConversionTime statistic to CnfStream. (#6769) tree | commitdiff
2021-06-21 Mathias PreinerMake CaDiCaL a required dependency. (#6761) tree | commitdiff
2021-06-18 Mathias PreinerMake CnfStream::toCNF iterative (#6757) tree | commitdiff
2021-06-15 Gereon KremerRemove public option wrappers (#6716) tree | commitdiff
2021-06-07 Gereon KremerRemove `Options::wasSetByUser()` (#6682) tree | commitdiff
2021-05-27 Andrew ReynoldsUpdate proof namespaces (#6614) tree | commitdiff
2021-05-27 Andrew ReynoldsEnable 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 ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-20 Gereon KremerProperly initialize. (#6586) tree | commitdiff
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) tree | commitdiff
2021-05-19 Mathias PreinerCorrectly handle negated assertions for assumption... tree | commitdiff
2021-05-17 Andres NoetzliInclude cinttypes instead of inttypes.h (#6548) tree | commitdiff
2021-05-14 Mathias Preinerbv: Assert input facts on user-level 0. (#6515) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-05 Andrew ReynoldsMove current decision engine to decision engine old... tree | commitdiff
2021-05-04 Andrew ReynoldsMove env into smt solver, theory engine, prop engine... tree | commitdiff
2021-05-04 Haniel BarbosaDo not use proof CNF stream with assumptions-based... tree | commitdiff
2021-04-28 Gereon KremerMake sure reference stats are reset properly (#6457) tree | commitdiff
2021-04-26 Gereon KremerFirst part of options refactoring (#6428) tree | commitdiff
2021-04-26 Haniel BarbosaFix assertions in SAT solver (#6443) tree | commitdiff
2021-04-24 Mathias PreinerAdd assumption-based unsat cores. (#6427) tree | commitdiff
2021-04-23 Gereon KremerMake 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 BarbosaReconciling proofs and unsat cores (#6405) tree | commitdiff
2021-04-21 Mathias PreinerGoodbye CVC4, hello cvc5! (#6371) tree | commitdiff
2021-04-15 Mathias PreinerBuild support library from base and context. (#6368) tree | commitdiff
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
2021-04-14 Aina NiemetzRename 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 KremerRefactor resource manager (#6322) tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-12 Andrew ReynoldsConsolidate interface to prop engine (#6189) tree | commitdiff
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) tree | commitdiff
2021-04-09 Aina NiemetzRename 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 NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-22 Andrew ReynoldsAdd skolem definition manager (#6187) tree | commitdiff
2021-03-16 Mathias Preinercmake: 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 NoetzliSchedule preregistration lemmas to be satisfied after... tree | commitdiff
2021-03-12 Gereon KremerAdd missing includes for statistics (#6124) tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-11 Mathias PreinerUse CVC4_ASSERTIONS instead of NDEBUG. (#6099) tree | commitdiff
2021-03-10 Mathias PreinerUse Assert instead of assert. (#6095) tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-26 Haniel BarbosaSome 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 PreinerAdd bit-level propagation support to BV bitblast solver... tree | commitdiff
2021-02-12 Andrew ReynoldsSimplify 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