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 / options /
2020-03-12 Andrew ReynoldsRemove local theory extension option (#4048) tree | commitdiff
2020-03-12 Aina NiemetzHide options for and related to the BV abstraction... tree | commitdiff
2020-03-11 Andrew ReynoldsRemove experimental symmetry breaker (#4005) tree | commitdiff
2020-03-11 Andrew ReynoldsRemove partial instantiation for local theory extension... tree | commitdiff
2020-03-10 Andrew ReynoldsRename sygus option name (#3977) tree | commitdiff
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-29 Andrew ReynoldsReplace conditional rewrite pass in quantifiers with... tree | commitdiff
2020-02-26 Andrew ReynoldsSupport for witnessing choice in models (#3781) tree | commitdiff
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821) tree | commitdiff
2020-02-25 yoni206bv_to_int preprocessing pass tree | commitdiff
2020-02-21 Andrew V. JonesAdding checks to the validation of 'bv-sat-solver'... tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2020-02-17 Andrew ReynoldsOption to limit the number of rounds of enumerative... tree | commitdiff
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) tree | commitdiff
2020-02-11 Andres NoetzliRemove `--strings-binary-csp` option (#3743) tree | commitdiff
2020-01-31 Andrew ReynoldsAllow PBE symmetry breaking with sygus stream (#3686) tree | commitdiff
2019-12-19 Mathias PreinerFix typo in smt_options.toml. (#3579) tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-10 Haniel BarbosaFix ufho issues (#3551) tree | commitdiff
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... tree | commitdiff
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531) tree | commitdiff
2019-12-04 Andrew ReynoldsNew grammar construction modes for SyGuS (#3486) tree | commitdiff
2019-11-29 Andrew ReynoldsCheck free variables in assertions when using SyGuS... tree | commitdiff
2019-11-27 Haniel BarbosaEnable sygusRecFun by default and fixes SyGuS+RecFun... tree | commitdiff
2019-11-21 Haniel Barbosahard limit for rec-fun eval (#3485) tree | commitdiff
2019-11-17 Andres NoetzliAdd support for ThreadSanitizer instrumentation (#3467) tree | commitdiff
2019-11-06 Andrew ReynoldsSupport for SyGuS PBE + recursive functions (#3433) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-10-20 Andrew V. JonesCleaning-up the declaration of wrapped functions/method... tree | commitdiff
2019-10-11 Andres NoetzliAdd support for UBSan instrumentation (#3382) tree | commitdiff
2019-10-08 Ying ShengMake ackermannization generally applicable rather than... tree | commitdiff
2019-09-30 Andrew ReynoldsAdd help for sygus 2.0 (#3318) tree | commitdiff
2019-09-16 Andrew ReynoldsRemove equality inference option for quantifiers (... tree | commitdiff
2019-09-16 Aina NiemetzFix compiler warning in options.cpp. (#3284) tree | commitdiff
2019-09-12 Andrew Reynolds Rename UF with cardinality extension (#3241) tree | commitdiff
2019-09-07 Andrew ReynoldsRemove portfolio (#3236) tree | commitdiff
2019-09-06 Mathias PreinerRemove SMT1 parser. (#3228) tree | commitdiff
2019-08-23 Andrew ReynoldsUpdate dynamic splitting strategy for quantifiers ... tree | commitdiff
2019-08-14 Mathias PreinerRemove option --continued-execution. (#3189) tree | commitdiff
2019-08-14 Andrew ReynoldsCall separate SMT engine for single invocation sygus... tree | commitdiff
2019-08-13 Andrew ReynoldsImplement check abduct feature (#3152) tree | commitdiff
2019-08-10 Andrew ReynoldsAdd option to only dump unsolved queries for --sygus... tree | commitdiff
2019-08-03 Haniel BarbosaCollapse @ chains in SMT2 printer (#3140) tree | commitdiff
2019-08-02 Mathias PreinerUpdate CaDiCaL to version 1.0.3. (#3137) tree | commitdiff
2019-08-01 Andrew Reynolds Regular expression intersection modes (#3134) tree | commitdiff
2019-07-31 Haniel BarbosaParsing THF and adding several regressions (#3131) tree | commitdiff
2019-07-29 Andrew ReynoldsModel blocker feature (#3112) tree | commitdiff
2019-07-29 Andrew ReynoldsSupport get-abduct smt2 command (#3122) tree | commitdiff
2019-07-23 Andrew ReynoldsFix help messages (#3096) tree | commitdiff
2019-07-18 Andrew V. JonesRemoving forward-declaration of undefined function... tree | commitdiff
2019-07-08 Andrew ReynoldsTowards refactoring relations (#3078) tree | commitdiff
2019-07-01 Andrew ReynoldsSupport sygus version 2 format (#3066) tree | commitdiff
2019-07-01 Andrew ReynoldsAdd higher-order elimination preprocessing pass (#2865) tree | commitdiff
2019-06-21 Andres NoetzliFix and simplify handling of --force-logic (#3062) tree | commitdiff
2019-05-18 Andres NoetzliSupport for incremental bit-blasting with CaDiCaL ... tree | commitdiff
2019-05-15 Aina Niemetz BV: Do not enable abstraction when eager bit-blasting... tree | commitdiff
2019-05-10 Andrew ReynoldsDisable relational triggers (#2994) tree | commitdiff
2019-05-09 Andrew ReynoldsFixes for relational triggers (#2967) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-23 Alex Ozdemir[BV] An option for SAT proof optimization (#2915) tree | commitdiff
2019-04-16 Andrew ReynoldsStratify enumerative instantiation (#2954) tree | commitdiff
2019-04-16 Andrew ReynoldsMinor simplifications to theory quantifiers (#2953) tree | commitdiff
2019-04-04 Haniel BarbosaIgnoring FP benchmarks with "unsafe" sizes unless optio... tree | commitdiff
2019-04-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-22 Haniel Barbosafix help information on TPTP parsing (#2884) tree | commitdiff
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744) tree | commitdiff
2019-03-16 Alex OzdemirEnable CryptoMiniSat-backed BV proofs (#2847) tree | commitdiff
2019-03-12 Andrew ReynoldsAdd option --sygus-rr-synth-rec for considering all... tree | commitdiff
2019-01-17 Andres NoetzliAdd option to print BV constants in binary (#2805) tree | commitdiff
2019-01-15 Andres NoetzliStrings: Add option to change loop process mode (#2794) tree | commitdiff
2019-01-09 Alex Ozdemir[BV Proofs] Option for proof format (#2777) tree | commitdiff
2018-12-14 Aina NiemetzFixed typos. tree | commitdiff
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742) tree | commitdiff
2018-12-10 makaimannBoolToBV modes (off, ite, all) (#2530) tree | commitdiff
2018-12-07 Alex OzdemirEnable BV proofs when using an eager bitblaster (#2733) tree | commitdiff
2018-12-04 Andrew ReynoldsEnable regular expression elimination by default. ... tree | commitdiff
2018-11-28 Andrew ReynoldsGeneralize sygus stream solution filtering to logical... tree | commitdiff
2018-11-05 Andrew ReynoldsChange default sygus enumeration mode to auto (#2689) tree | commitdiff
2018-10-31 Andrew ReynoldsAdd optimized sygus enumeration (#2677) tree | commitdiff
2018-10-20 Andrew ReynoldsSygus streaming non-implied predicates (#2660) tree | commitdiff
2018-10-19 Mathias PreinerRemove autotools build system. (#2639) tree | commitdiff
2018-10-19 Andres NoetzliAdd OptionException handling during initialization... tree | commitdiff
2018-10-19 Andrew ReynoldsNon-implied mode for model cores (#2653) tree | commitdiff
2018-10-18 Andres NoetzliShow if ASAN build in --show-config (#2650) tree | commitdiff
2018-10-18 Andrew ReynoldsSygus query generator (#2465) tree | commitdiff
2018-10-16 Haniel BarbosaOption for shuffling condition pool in CegisUnif (... tree | commitdiff
2018-10-15 Andrew ReynoldsDelay initialization of theory engine (#2621) tree | commitdiff
2018-10-13 Andres NoetzliReset input language for ExprMiner subsolver (#2624) tree | commitdiff
2018-10-12 Andrew ReynoldsImprovements to rewrite rules from inputs (#2625) tree | commitdiff
2018-10-11 Haniel BarbosaFix default setting of CegisUnif options (#2605) tree | commitdiff
2018-10-11 Andrew ReynoldsSynthesize rewrite rules from inputs (#2608) tree | commitdiff
2018-10-09 Andrew Reynolds Support for basic actively-generated enumerators ... tree | commitdiff
2018-10-05 Andrew ReynoldsUpdate default options for sygus (#2586) tree | commitdiff
2018-10-04 Aina NiemetzNew C++ API: Add checks for Sorts. (#2519) tree | commitdiff
2018-10-03 Andrew ReynoldsAdd actively generated sygus enumerators (#2552) tree | commitdiff
2018-09-22 Mathias Preinercmake: Only build libcvc4 and libcvc4parser as libraries. tree | commitdiff
2018-09-22 Mathias Preinercmake: Cleanup CMakeLists.txt files, remove SHARED. tree | commitdiff
2018-09-22 Mathias Preinercmake: Working build infrastructure. tree | commitdiff
next