projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
[Unit Tests] Add missing include (#6990)
[cvc5.git] / src / preprocessing /
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
2021-03-16 Haniel Barbosa[proof-new] Renaming proof option to be in sync with... tree | commitdiff
2021-03-15 Gereon KremerReplace HistogramStat by IntegralHistogramStat (#6126) 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-09 Andrew ReynoldsRemove logic request (#6089) 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-06 Mathias PreinerRemove partial UDIV/UREM operators. (#6069) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-02 Mathias PreinerRemove non-ASCII characters from source files. (#6039) tree | commitdiff
2021-03-02 Mathias PreinerFix nightly errors. (#6034) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-25 Gereon KremerMove (optional) rewrite from TrustSubstitutionMap to... tree | commitdiff
2021-02-25 Mathias PreinerEnable -Werror. (#5969) tree | commitdiff
2021-02-24 Gereon KremerEnsure static-learning adds rewritten assertions. ... tree | commitdiff
2021-02-24 Andrew ReynoldsAdd interface to TheoryState for sort inference and... tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) tree | commitdiff
2021-02-17 Andrew ReynoldsMove methods from term util to quantifiers registry... tree | commitdiff
2021-02-12 Andrew ReynoldsSimplify and fix decision engine's handling of skolem... tree | commitdiff
2021-02-02 Andrew ReynoldsCleanup some includes (#5847) tree | commitdiff
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817) tree | commitdiff
2021-01-27 Andrew ReynoldsSplit pattern term selector from trigger (#5811) tree | commitdiff
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... tree | commitdiff
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776) tree | commitdiff
2021-01-13 Andrew ReynoldsDo not call ppRewrite on Boolean equalities (#5762) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-09 yoni206Strings arith checks preprocessing pass: step 2 (#5750) tree | commitdiff
2021-01-08 yoni206bv-to-int: avoid binarizing nodes twice (#5749) tree | commitdiff
2021-01-06 yoni206strings arith checks preprocessing pass: step 1 (#5747) tree | commitdiff
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... tree | commitdiff
2020-12-21 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy... tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647) tree | commitdiff
2020-12-16 Andrew ReynoldsMove ownership of term formula removal to theory prepro... tree | commitdiff
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje... tree | commitdiff
2020-12-09 Aina Niemetzite_utilities: Fix infinite loop in compressTerm. ... tree | commitdiff
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... tree | commitdiff
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) tree | commitdiff
2020-12-04 Alex OzdemirUse NodeDfsIterable for makeBinary (#5595) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-11-18 Andrew ReynoldsMinor cleanup of SmtEngine (#5450) tree | commitdiff
2020-11-14 Andrew Reynolds(proof-new) Proofs for non-clausal simplification ... tree | commitdiff
2020-10-22 Andrew Reynolds(proof-new) Make theory preprocessor user-context depen... tree | commitdiff
2020-10-21 Gereon Kremer(proof-new) Make circuit propagator proof producing... tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... tree | commitdiff
2020-10-19 Andrew Reynolds(proof-new) Updates to assertions pipeline and preproce... tree | commitdiff
2020-10-19 Andrew Reynolds(proof-new) Update preprocessing pass context for proof... tree | commitdiff
2020-10-16 yoni206bv2int: caching introduced terms (#5283) tree | commitdiff
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263) tree | commitdiff
2020-10-13 yoni206bv2int: improving bvand tables (#5235) tree | commitdiff
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) tree | commitdiff
2020-10-10 yoni206bv2int: bvand translation code move (#5227) tree | commitdiff
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in... tree | commitdiff
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... tree | commitdiff
2020-10-01 Andrew Reynolds(proof-new) Preprocessing passes use proper interfaces... tree | commitdiff
2020-09-29 Andrew Reynolds(proof-new) Fixes for preprocess proof generator and... tree | commitdiff
2020-09-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064) tree | commitdiff
2020-09-23 yoni206bv2int: new options for bvand translation (#5096) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-18 yoni206bv2int: quantifiers support (#5080) tree | commitdiff
next