summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
AgeCommit message (Expand)Author
2021-02-23Add interface to TheoryState for sort inference and facts (#5967)Andrew Reynolds
2021-02-22(proof-new) Change proof-new option to proof (#5955)Andrew Reynolds
2021-02-17Move methods from term util to quantifiers registry (#5916)Andrew Reynolds
2021-02-12Simplify and fix decision engine's handling of skolem definitions (#5888)Andrew Reynolds
2021-02-02Cleanup some includes (#5847)Andrew Reynolds
2021-01-28Always theory-preprocess lemmas (#5817)Andrew Reynolds
2021-01-27Split pattern term selector from trigger (#5811)Andrew Reynolds
2021-01-15Implement --no-strings-lazy-pp as a preprocessing pass (#5777)Andrew Reynolds
2021-01-14Updates to theory preprocess equality (#5776)Andrew Reynolds
2021-01-13Do not call ppRewrite on Boolean equalities (#5762)Andrew Reynolds
2021-01-11Further simplifications in preparation for removing Expr layer (#5756)Andrew Reynolds
2021-01-09Strings arith checks preprocessing pass: step 2 (#5750)yoni206
2021-01-08bv-to-int: avoid binarizing nodes twice (#5749)yoni206
2021-01-06strings arith checks preprocessing pass: step 1 (#5747)yoni206
2020-12-24[proof-new] Only use old proofs for unsat cores if no proof new (#5725)Haniel Barbosa
2020-12-22Make theory preprocess rewrite equalities a preprocessing pass (#5711)Andrew Reynolds
2020-12-21Move ownership of theory preprocessor to TheoryProxy (#5690)Andrew Reynolds
2020-12-16Simplify preprocessing (#5647)Andrew Reynolds
2020-12-16Move ownership of term formula removal to theory preprocessor (#5670)Andrew Reynolds
2020-12-15Consolidate basic sygus utilities regarding sygus conjectures (#5421)Andrew Reynolds
2020-12-08bv-to-int: Expand definitions of bvudiv and bvurem during bv-to-int preproces...yoni206
2020-12-07Add bitwise refinement mode for IAND (#5328)makaimann
2020-12-04Use NodeDfsIterable for makeBinary (#5595)Alex Ozdemir
2020-12-02Update copyright headers.Aina Niemetz
2020-12-02Rename macro Message to CVC4Message. (#5576)Aina Niemetz
2020-11-18Minor cleanup of SmtEngine (#5450)Andrew Reynolds
2020-11-14(proof-new) Proofs for non-clausal simplification (#5409)Andrew Reynolds
2020-10-21(proof-new) Make theory preprocessor user-context dependent (#5296)Andrew Reynolds
2020-10-21(proof-new) Make circuit propagator proof producing (#5318)Gereon Kremer
2020-10-19(proof-new) Update preprocessing pass context for proofs (#5298)Andrew Reynolds
2020-10-16bv2int: caching introduced terms (#5283)yoni206
2020-10-13bv2int: rewritings and unsat cores (#5263)yoni206
2020-10-13bv2int: improving bvand tables (#5235)yoni206
2020-10-12Eliminate uses of Expr in SmtEngine interface (#5240)Andrew Reynolds
2020-10-09bv2int: bvand translation code move (#5227)yoni206
2020-10-08reset-assertions: Remove all non-global symbols in the parser (#5229)Andres Noetzli
2020-10-06(proof-new) Add interface for trusted substitution and update ppAssert (#5193)Andrew Reynolds
2020-10-01(proof-new) Preprocessing passes use proper interfaces to assertions pipeline...Andrew Reynolds
2020-09-24 Function definition fmf preprocessing pass (#5064)Andrew Reynolds
2020-09-23bv2int: new options for bvand translation (#5096)yoni206
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-18bv2int: quantifiers support (#5080)yoni206
2020-09-15bv2int: support models in tests (#5068)yoni206
2020-09-14bv2int: simpler translation for plus and times (#5055)yoni206
2020-09-14Fix type for Windows build (#5062)Andres Noetzli
2020-09-10bv2int: refactoring the main translation loop (#5051)yoni206
2020-09-09bv2int: improvement in lazy failures (#5020)yoni206
2020-09-03Changing the handled operators in bv2int preprocessing pass (#4970)yoni206
2020-09-02(proof-new) Support proofs of quantifier instantiation (#5001)Andrew Reynolds
2020-09-01Removes old proof code (#4964)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback