summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
AgeCommit message (Expand)Author
2019-12-02OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ AP...makaimann
2019-12-02Fix case of higher-order + sygus inference (#3509)Andrew Reynolds
2019-11-27Fix sygus inference for choice functions introduced at preprocess (#3500)Andrew Reynolds
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-11-18Use standard sygus interface for abduction and rewrite rule synthesis (#3471)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-08Limit cases of sygus inference based on type (#3370)Andrew Reynolds
2019-10-08Make ackermannization generally applicable rather than just BV (#3315)Ying Sheng
2019-09-27Make substitution index context-independent (#2474)Andres Noetzli
2019-08-20Fixes for sygus inference on quantifier free problems (#3202)Andrew Reynolds
2019-08-01Fix BVGauss unit tests. (#3142)Mathias Preiner
2019-08-01Move some generic utilities out of quantifiers (#3139)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-07-25Input user grammar in sygus abduct (#3119)Andrew Reynolds
2019-07-01Add higher-order elimination preprocessing pass (#2865)Andrew Reynolds
2019-04-24Fix compiler warning. (#2975)Aina Niemetz
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-04-17More use of isClosure (#2959)Andrew Reynolds
2019-04-03Update copyright headers.Aina Niemetz
2019-03-26Update copyright headers.Aina Niemetz
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2018-12-10BoolToBV modes (off, ite, all) (#2530)makaimann
2018-10-12Improvements to rewrite rules from inputs (#2625)Andrew Reynolds
2018-10-10Synthesize rewrite rules from inputs (#2608)Andrew Reynolds
2018-10-02Make registration of preprocessing passes explicit (#2564)Andres Noetzli
2018-10-01Refactor preprocessing pass registration (#2468)Andres Noetzli
2018-09-17Improvements and fixes for symmetry detection and breaking (#2459)Andrew Reynolds
2018-09-14Refactor how assertions are added to decision engine (#2396)Andres Noetzli
2018-09-11Avoid calling size() every iteration (#2450)yoni206
2018-09-10Fix global negate (#2449)Andrew Reynolds
2018-09-10Refactor non-clausal simplify preprocessing pass. (#2425)Aina Niemetz
2018-08-30Refactor theory preprocess into preprocessing pass. (#2395)Mathias Preiner
2018-08-29Refactor MipLibTrick preprocessing pass. (#2359)Mathias Preiner
2018-08-25Refactor unconstrained simplification pass (#2374)Andres Noetzli
2018-08-25Refactor quantifier macros preprocessing pass (#1840)yoni206
2018-08-24Refactor nlExtPurify preprocessing pass (#1963)Haniel Barbosa
2018-08-23Refactor ITE simplification preprocessing pass. (#2360)Aina Niemetz
2018-08-22global-negate preprocessing pass (#2317)yoni206
2018-08-22Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)yoni206
2018-08-20 Make sygus inference a preprocessing pass (#2334)Andrew Reynolds
2018-08-16Refactor eager atoms preprocessing pass. (#2318)Mathias Preiner
2018-08-16Make quantifiers-preprocess preprocessing pass (#2322)Caleb Donovick
2018-08-16Refactor IteRemoval preprocessing pass (#1793)Andres Noetzli
2018-08-16Refactor extended rewriter preprocessing pass (#2324)Haniel Barbosa
2018-08-16Refactor apply2const (#2316)Haniel Barbosa
2018-08-15Make sort inference a preprocessing pass (#2309)Andrew Reynolds
2018-08-01Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)Mathias Preiner
2018-07-23Generalize symmetry detection for 1 symmetry variable mapped to n input varia...Andrew Reynolds
2018-07-17Refactor sep-pre-skolem-emp preprocessing passyoni206
2018-07-10Move rewrite to pass (#2128)Caleb Donovick
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback