summaryrefslogtreecommitdiff
path: root/src/preprocessing
AgeCommit message (Expand)Author
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-20(proof-new) Update add lazy step interface in LazyCDProof (#5299)Andrew Reynolds
2020-10-19(proof-new) Updates to assertions pipeline and preprocess generator (#5300)Andrew Reynolds
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-29(proof-new) Fixes for preprocess proof generator and proofs in assertion pipe...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-16Dump commands in internal code using command printing functions. (#5040)Abdalrhman Mohamed
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-11(proof-new) Add SMT proof manager (#5054)Andrew Reynolds
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
2020-08-31Fix --ackermann in the presence on syntactically different but possibly equal...Gereon Kremer
2020-08-28Incremental support for bv_to_int (#4967)yoni206
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-18Split SygusSolver from SmtEngine (#4891)Andrew Reynolds
2020-08-06Updates not related to creation for eliminating Expr-level datatype (#4838)Andrew Reynolds
2020-08-03Split dump manager from SmtEngine (#4824)Andrew Reynolds
2020-07-27(proof-new) Proof production for term formula removal (#4687)Andrew Reynolds
2020-07-17(proof-new) Proof recording for assertions pipeline (#4766)Andrew Reynolds
2020-07-15Use Nodes for SmtEngine assertions (#4752)Andres Noetzli
2020-07-14Remove sygus print callback (#4727)Andrew Reynolds
2020-07-13Minor refactoring of subsolver initialization (#4731)Andrew Reynolds
2020-07-11Changing bv_to_int options (#4721)yoni206
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-06-24[unconstrained] Fix gathering of visited-once vars (#4652)Andres Noetzli
2020-06-19Use traversal iterators in IntToBv (#4169)Alex Ozdemir
2020-06-18Bv to int elimination bugfix (#4435)yoni206
2020-06-16Update copyright headers.Aina Niemetz
2020-06-03Do not apply unconstrained simplification when quantifiers are present (#4532)Andrew Reynolds
2020-05-20Fix missing check for cardinality one in unconstrained simplifier (#4504)Andrew Reynolds
2020-05-05Always introduce fresh variable for unconstrained APPLY_UF (#4472)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback