projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
floatingpoint: Use unique_ptr for FloatingPointLiteral pointer. (#5503)
[cvc5.git] / src / preprocessing /
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
2019-12-16 Ying ShengSupport ackermannization on uninterpreted sorts in... tree | commitdiff
2019-12-13 Andrew ReynoldsEliminate Expr-level calls in TypeNode (#3562) tree | commitdiff
2019-12-02 makaimannOpTerm Refactor: Allow retrieving OpTerm used to create... tree | commitdiff
2019-12-02 Andrew ReynoldsFix case of higher-order + sygus inference (#3509) tree | commitdiff
2019-11-27 Andrew ReynoldsFix sygus inference for choice functions introduced... tree | commitdiff
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) tree | commitdiff
2019-11-18 Andrew ReynoldsUse standard sygus interface for abduction and rewrite... tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-10-08 Andrew ReynoldsLimit cases of sygus inference based on type (#3370) tree | commitdiff
2019-10-08 Ying ShengMake ackermannization generally applicable rather than... tree | commitdiff
2019-09-27 Andres NoetzliMake substitution index context-independent (#2474) tree | commitdiff
2019-08-20 Andrew ReynoldsFixes for sygus inference on quantifier free problems... tree | commitdiff
2019-08-02 Mathias PreinerFix BVGauss unit tests. (#3142) tree | commitdiff
2019-08-01 Andrew ReynoldsMove some generic utilities out of quantifiers (#3139) tree | commitdiff
2019-07-30 Haniel BarbosaCode to activate hoelim preprocessing pass (#3129) tree | commitdiff
2019-07-29 Andrew ReynoldsSupport get-abduct smt2 command (#3122) tree | commitdiff
2019-07-26 Andrew ReynoldsInput user grammar in sygus abduct (#3119) tree | commitdiff
2019-07-01 Andrew ReynoldsAdd higher-order elimination preprocessing pass (#2865) tree | commitdiff
2019-04-25 Aina NiemetzFix compiler warning. (#2975) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-17 Andrew ReynoldsMore use of isClosure (#2959) tree | commitdiff
next