projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix a subtle issue with double negations in coverings proof (#7967)
[cvc5.git] / src / preprocessing /
2022-01-18 Andrew ReynoldsPrint original form for substitutions and learned liter... tree | commitdiff
2022-01-14 Andrew ReynoldsImplement -o subs to show learned top-level substitutio... tree | commitdiff
2022-01-14 Andrew ReynoldsFix learned rewrite pass for non-real equalties (#7936) tree | commitdiff
2022-01-11 Gereon KremerRemove static accesses to options (#7913) tree | commitdiff
2022-01-07 Andrew ReynoldsFix eager string preprocessing in incremental mode... tree | commitdiff
2022-01-06 Andrew ReynoldsMinor cleaning of non-clausal simplification (#7886) tree | commitdiff
2021-12-20 Andrew ReynoldsEliminating some uses of const rational in arithmetic... tree | commitdiff
2021-12-17 Andrew ReynoldsRefactoring initialization of proofs (#7834) tree | commitdiff
2021-12-17 Andrew ReynoldsEliminate more uses of CONST_RATIONAL (#7816) tree | commitdiff
2021-12-16 yoni206int-to-bv: fail if one of the arguments has type real... tree | commitdiff
2021-12-13 Andrew ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... tree | commitdiff
2021-12-13 yoni206Integrate new int-blaster (#7781) tree | commitdiff
2021-12-10 Gereon KremerEliminate more static rewrites (#7786) tree | commitdiff
2021-12-09 Andrew ReynoldsDo not make SyGuS subsolver in unsat state after solvin... tree | commitdiff
2021-12-07 Andrew ReynoldsTowards support for incremental sygus (#7736) tree | commitdiff
2021-12-07 Andrew ReynoldsEliminate more static calls to Rewriter::rewrite (... tree | commitdiff
2021-12-07 makaimannAdd bitwise option to IntBlaster (#7721) tree | commitdiff
2021-12-02 Andrew ReynoldsFixes for sygus-rr-synth-input (#7716) tree | commitdiff
2021-11-19 Andrew ReynoldsRemove n-ary builder (#7671) tree | commitdiff
2021-11-17 Andrew ReynoldsPreparations for eliminating arithmetic subtyping ... tree | commitdiff
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) tree | commitdiff
2021-11-09 Andrew ReynoldsOnly eliminate lambdas in higher-order elimination... tree | commitdiff
2021-11-09 Gereon KremerRemove `CVC5Message` (#7610) tree | commitdiff
2021-11-05 Gereon KremerRemove `Chat()` in favor of new `verbose()` (#7586) tree | commitdiff
2021-11-05 Gereon KremerEliminate `Warning` macro in favor of `EnvObj::warning... tree | commitdiff
2021-11-04 Andrew ReynoldsReplace the old dump infrastructure (#7572) tree | commitdiff
2021-11-03 Andrew ReynoldsFix debug trace for miplib (#7563) tree | commitdiff
2021-11-03 Andrew ReynoldsRefactor skolem construction (#7561) tree | commitdiff
2021-11-01 Mathias Preinerbv: Remove layered solver. (#7455) tree | commitdiff
2021-10-25 Andrew ReynoldsFix more missing uses of CDProof::isSame (#7491) tree | commitdiff
2021-10-22 Andrew ReynoldsRemove `--uf-ho` option (#7463) tree | commitdiff
2021-10-11 Aina NiemetzRename SmtScope to SolverEngineScope. (#7284) tree | commitdiff
2021-10-08 Andrew ReynoldsA few more miscellaneous uses of EnvObj (#7325) tree | commitdiff
2021-10-07 Andrew ReynoldsMove preprocessor to smt solver (#7321) tree | commitdiff
2021-10-07 Andrew ReynoldsUse skolem lemma in prop layer interfaces (#7320) tree | commitdiff
2021-10-04 Andrew ReynoldsEliminating static calls to rewriter from strings ... tree | commitdiff
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) tree | commitdiff
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... tree | commitdiff
2021-09-30 Mathias Preinerbv: Refactor ppRewrite and move to TheoryBV. (#7271) tree | commitdiff
2021-09-30 Mathias PreinerProperly cache assertions in static learning preprocess... tree | commitdiff
2021-09-30 Andrew ReynoldsSimplify the syntax and representation of the separatio... tree | commitdiff
2021-09-30 Gereon KremerRemove usage of static options in arithmetic theory... tree | commitdiff
2021-09-24 Andrew ReynoldsEliminate calls to Rewriter::rewrite from strings entai... tree | commitdiff
2021-09-11 Gereon KremerUse StatisticsRegistry from Env (#7166) tree | commitdiff
2021-09-11 Mathias Preinerbv: Move IsPowerOfTwo rule to preprocessing pass and... tree | commitdiff
2021-09-10 Andres NoetzliUse C++17 attributes (#7154) tree | commitdiff
2021-09-10 Gereon KremerUse EnvObj-based options in preprocessing (#7165) tree | commitdiff
2021-09-09 Aina Niemetzpp passes: Use EnvObj::rewrite() instead of Rewriter... tree | commitdiff
2021-09-08 Andrew ReynoldsImprove pre-skolemization, move quantifiers preprocess... tree | commitdiff
2021-09-08 Andrew ReynoldsTowards standard usage of ExtendedRewriter (#7145) tree | commitdiff
2021-09-03 Aina NiemetzEnvObj: Add options(), context(), userContext(). (... tree | commitdiff
2021-09-03 Aina Niemetzpp: Have PreprocessingPassContext derive from EnvObj... tree | commitdiff
2021-09-02 Aina NiemetzEnvObj: Restrict access. (#7121) tree | commitdiff
2021-09-02 Aina NiemetzRemove PreprocessingPassContext::getSmt(). (#7118) tree | commitdiff
2021-09-02 Aina Niemetzpp: Derive PreprocessingPass from EnvObj. (#7112) tree | commitdiff
2021-09-01 Aina NiemetzClean up and document PP context. (#7102) tree | commitdiff
2021-09-01 Aina Niemetzrewriter: Make clearCaches non-static. (#7100) tree | commitdiff
2021-08-26 Andrew ReynoldsEliminate currentSmtEngine for subsolver calls (#7068) tree | commitdiff
2021-08-26 Mathias Preinerint2bv: Fix conversion of signed bit-vector values... tree | commitdiff
2021-08-25 Andrew ReynoldsEliminate calls to currentSmtEngine (#7060) tree | commitdiff
2021-08-17 Andres NoetzliReplace `Maybe` with `std::optional` (#7005) tree | commitdiff
2021-07-12 Andrew ReynoldsFix for learned rewrite pass, add regression (#6850) tree | commitdiff
2021-07-06 Andrew ReynoldsIntegrate learned rewrite preprocessing pass (#6840) tree | commitdiff
2021-07-06 Andrew ReynoldsAdd implementation of learned rewrite pass (#6843) tree | commitdiff
2021-07-06 Andrew ReynoldsAdd learned rewrite preprocessing pass (#6842) tree | commitdiff
2021-06-30 yoni206int-to-bv: correct model values (#6811) tree | commitdiff
2021-06-15 Gereon KremerRemove public option wrappers (#6716) tree | commitdiff
2021-06-10 Andrew ReynoldsEnsure bv2nat and int2bv are not rewritten when using... tree | commitdiff
2021-06-09 Andres NoetzliMake `--solve-int-as-bv=X` robust to rewriting (#6722) tree | commitdiff
2021-06-09 Andrew ReynoldsIntegrate learned literal manager into preprocessing... tree | commitdiff
2021-06-08 Andrew ReynoldsAdd learned literal manager utility (#6709) tree | commitdiff
2021-06-01 Andrew ReynoldsUse top-level substitutions in ITE simp (#6651) tree | commitdiff
2021-05-27 Andrew ReynoldsUpdate proof namespaces (#6614) 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-21 Aina NiemetzBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589) tree | commitdiff
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-10 Andrew ReynoldsUnify top-level substitutions and model substitutions... tree | commitdiff
2021-05-07 Andrew ReynoldsSimplifications to expand definitions (#6487) tree | commitdiff
2021-05-06 Andrew ReynoldsUse constant folding for evaluating BV eager atom ... tree | commitdiff
2021-04-30 Andrew ReynoldsUse substitutions for implementing defined functions... tree | commitdiff
2021-04-22 Andrew ReynoldsFix models for sygus-inference, bv2int, real2int (... tree | commitdiff
2021-04-22 Haniel BarbosaReconciling proofs and unsat cores (#6405) tree | commitdiff
2021-04-19 Andrew ReynoldsFully incorporate quantifiers macros into ppAssert... tree | commitdiff
2021-04-15 Aina Niemetzpreprocessing context: Add wrapper for model substituti... 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-13 Andrew ReynoldsRefactor quantifiers macros (#6348) 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-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-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... 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-25 Gereon KremerAdd missing includes. (#6207) tree | commitdiff
next