projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add bag inferences for operators: intersection, duplicate_removal, and empty bags...
[cvc5.git] / src / preprocessing /
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
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-16 yoni206bv2int: support models in tests (#5068) tree | commitdiff
2020-09-14 yoni206bv2int: simpler translation for plus and times (#5055) tree | commitdiff
2020-09-14 Andres NoetzliFix type for Windows build (#5062) tree | commitdiff
2020-09-12 Andrew Reynolds(proof-new) Add SMT proof manager (#5054) tree | commitdiff
2020-09-10 yoni206bv2int: refactoring the main translation loop (#5051) tree | commitdiff
2020-09-10 yoni206bv2int: improvement in lazy failures (#5020) tree | commitdiff
2020-09-03 yoni206Changing the handled operators in bv2int preprocessing... tree | commitdiff
2020-09-03 Andrew Reynolds(proof-new) Support proofs of quantifier instantiation... tree | commitdiff
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-08-31 Gereon KremerFix --ackermann in the presence on syntactically differ... tree | commitdiff
2020-08-28 yoni206Incremental support for bv_to_int (#4967) tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-18 Andrew ReynoldsSplit SygusSolver from SmtEngine (#4891) tree | commitdiff
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr... tree | commitdiff
2020-08-03 Andrew ReynoldsSplit dump manager from SmtEngine (#4824) tree | commitdiff
2020-07-27 Andrew Reynolds(proof-new) Proof production for term formula removal... tree | commitdiff
2020-07-18 Andrew Reynolds(proof-new) Proof recording for assertions pipeline... tree | commitdiff
2020-07-15 Andres NoetzliUse Nodes for SmtEngine assertions (#4752) tree | commitdiff
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727) tree | commitdiff
2020-07-14 Andrew ReynoldsMinor refactoring of subsolver initialization (#4731) tree | commitdiff
2020-07-11 yoni206Changing bv_to_int options (#4721) tree | commitdiff
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... tree | commitdiff
2020-06-24 Andres Noetzli[unconstrained] Fix gathering of visited-once vars... tree | commitdiff
2020-06-20 Alex OzdemirUse traversal iterators in IntToBv (#4169) tree | commitdiff
2020-06-19 yoni206Bv to int elimination bugfix (#4435) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-03 Andrew ReynoldsDo not apply unconstrained simplification when quantifi... tree | commitdiff
2020-05-21 Andrew ReynoldsFix missing check for cardinality one in unconstrained... tree | commitdiff
2020-05-05 Andrew ReynoldsAlways introduce fresh variable for unconstrained APPLY... tree | commitdiff
2020-04-21 Andrew ReynoldsMake option names related to CEGQI consistent (#4316) tree | commitdiff
2020-04-10 Andrew ReynoldsTowards proper use of resource managers (#4233) tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... tree | commitdiff
2020-03-25 Ahmed Irfanbv2int : linear mult opt (#4142) tree | commitdiff
2020-03-24 yoni206Int2BV fail on demand (#4079) tree | commitdiff
2020-03-20 Andrew ReynoldsFix variable shadowing issue in sygus-inference (#4121) tree | commitdiff
2020-03-19 yoni206Bv2int fail on demand tree | commitdiff
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110) tree | commitdiff
2020-03-17 Aina NiemetzSmtEngine: Convert members owned by SmtEngine to unique... tree | commitdiff
2020-03-12 Andrew ReynoldsDo not allow quantifiers over real variables in real... tree | commitdiff
2020-03-11 Andrew ReynoldsRemove experimental symmetry breaker (#4005) tree | commitdiff
2020-03-11 Aina Niemetzbv-gauss-elim: Fix handling of inconsistent case. ... tree | commitdiff
2020-03-11 Andrew ReynoldsFix real to int for parameterized kinds (#4016) tree | commitdiff
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) tree | commitdiff
2020-03-10 Andrew Reynolds Fix real as int for incremental (#3979) tree | commitdiff
2020-03-10 Andrew ReynoldsDo not traverse quantifiers in nl ext purify (#3982) tree | commitdiff
2020-03-10 Alex OzdemirDocument bv-to-bool recursion (#3848) tree | commitdiff
2020-03-10 makaimannEnhancement: make the bool-to-bv pass more robust and... tree | commitdiff
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) tree | commitdiff
2020-03-05 Aina NiemetzMove ownership of DecisionEngine into PropEngine. ... tree | commitdiff
2020-03-05 Aina NiemetzRevert "Move ownership of DecisionEngine into PropEngin... tree | commitdiff
2020-03-05 Andrew ReynoldsMove ownership of DecisionEngine into PropEngine. ... tree | commitdiff
2020-03-05 Andrew ReynoldsFix issues with real to int (#3918) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817) tree | commitdiff
2020-02-25 yoni206bv_to_int preprocessing pass tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
next