projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
[unconstrained] Fix gathering of visited-once vars (#4652)
[cvc5.git] / src / preprocessing /
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
2019-04-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744) tree | commitdiff
2018-12-10 makaimannBoolToBV modes (off, ite, all) (#2530) tree | commitdiff
2018-10-31 Andres NoetzliRecord assumption info in AssertionPipeline (#2678) tree | commitdiff
2018-10-12 Andrew ReynoldsImprovements to rewrite rules from inputs (#2625) tree | commitdiff
2018-10-11 Andrew ReynoldsSynthesize rewrite rules from inputs (#2608) tree | commitdiff
2018-10-02 Andres NoetzliMake registration of preprocessing passes explicit... tree | commitdiff
2018-10-01 Andres Noetzli Fix dumping pre/post preprocessing passes (#2469) tree | commitdiff
2018-10-01 Andres NoetzliRefactor preprocessing pass registration (#2468) tree | commitdiff
2018-09-18 Andrew ReynoldsImprovements and fixes for symmetry detection and break... tree | commitdiff
2018-09-15 Andres NoetzliRefactor how assertions are added to decision engine... tree | commitdiff
2018-09-11 yoni206Avoid calling size() every iteration (#2450) tree | commitdiff
2018-09-11 Andrew ReynoldsFix global negate (#2449) tree | commitdiff
2018-09-11 Aina NiemetzRefactor non-clausal simplify preprocessing pass. ... tree | commitdiff
2018-08-30 Mathias PreinerRefactor theory preprocess into preprocessing pass... tree | commitdiff
2018-08-29 Mathias PreinerRefactor MipLibTrick preprocessing pass. (#2359) tree | commitdiff
2018-08-26 Andres NoetzliRefactor unconstrained simplification pass (#2374) tree | commitdiff
2018-08-25 yoni206Refactor quantifier macros preprocessing pass (#1840) tree | commitdiff
2018-08-25 Haniel BarbosaRefactor nlExtPurify preprocessing pass (#1963) tree | commitdiff
2018-08-23 Aina NiemetzRefactor ITE simplification preprocessing pass. (#2360) tree | commitdiff
2018-08-23 yoni206global-negate preprocessing pass (#2317) tree | commitdiff
2018-08-22 yoni206Generating less consistency lemmas in bv-ackermann... tree | commitdiff
2018-08-21 Mathias PreinerMove d_realAssertionsEnd from SmtEnginePrivate to Asser... tree | commitdiff
2018-08-20 Andrew Reynolds Make sygus inference a preprocessing pass (#2334) tree | commitdiff
2018-08-17 Mathias PreinerRefactor eager atoms preprocessing pass. (#2318) tree | commitdiff
2018-08-17 Caleb DonovickMake quantifiers-preprocess preprocessing pass (#2322) tree | commitdiff
2018-08-17 Andres NoetzliRefactor IteRemoval preprocessing pass (#1793) tree | commitdiff
2018-08-16 Haniel BarbosaRefactor extended rewriter preprocessing pass (#2324) tree | commitdiff
2018-08-16 Haniel BarbosaRefactor apply2const (#2316) tree | commitdiff
2018-08-15 Andrew ReynoldsMake sort inference a preprocessing pass (#2309) tree | commitdiff
2018-08-01 Mathias PreinerFix bool-to-bv preprocessing pass for non-{bv,bool... tree | commitdiff
2018-07-23 Andrew ReynoldsGeneralize symmetry detection for 1 symmetry variable... tree | commitdiff
2018-07-17 yoni206Refactor sep-pre-skolem-emp preprocessing pass tree | commitdiff
2018-07-11 Caleb DonovickMove rewrite to pass (#2128) tree | commitdiff
2018-07-02 Aina NiemetzRefactor ApplySubsts preprocessing pass. (#2120) tree | commitdiff
2018-06-27 Andrew ReynoldsSynthesize candidate-rewrites from standard inputs... tree | commitdiff
2018-06-25 Aina NiemetzUpdated copyright headers. tree | commitdiff
2018-05-21 makaimannHandle IMPLIES in bool-to-bv and test it in regress0... tree | commitdiff
2018-05-16 yoni206Refactor static learning preprocessing pass (#1857) tree | commitdiff
2018-05-11 Aina NiemetzFix ackermannize preprocessing pass. (#1904) tree | commitdiff
2018-05-10 Aina NiemetzRefactored BVAckermann preprocessing pass. (#1889) tree | commitdiff
2018-05-09 yoni206Reorder class members in bv-to-bool and bool-to-bv... tree | commitdiff
next