projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Remove read_only from options. (#6513)
[cvc5.git] / src / options / quantifiers_options.toml
2021-05-10 Gereon KremerRemove read_only from options. (#6513) blob | commitdiff | raw
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) blob | commitdiff | raw | diff to current
2021-04-13 Andrew ReynoldsAdd pool instantiation strategy (#6308) blob | commitdiff | raw | diff to current
2021-03-11 MikolasJanotaImprovements and refactoring for enumeratative strategy... blob | commitdiff | raw | diff to current
2021-02-10 Andrew ReynoldsRemove track instantiations infrastructure (#5883) blob | commitdiff | raw | diff to current
2021-02-09 Andrew ReynoldsMake term database optionally SAT-context-dependent... blob | commitdiff | raw | diff to current
2021-02-08 Andrew ReynoldsRemove support for inst closure (#5874) blob | commitdiff | raw | diff to current
2021-01-27 Andrew Reynolds(proof-new) Improvements to quantifiers engine and... blob | commitdiff | raw | diff to current
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820) blob | commitdiff | raw | diff to current
2021-01-24 Andrew ReynoldsInitial cleaning of triggers (#5795) blob | commitdiff | raw | diff to current
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) blob | commitdiff | raw | diff to current
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713) blob | commitdiff | raw | diff to current
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) blob | commitdiff | raw | diff to current
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... blob | commitdiff | raw | diff to current
2020-10-11 Mathias PreinerSyGuS instantiation modes (#5228) blob | commitdiff | raw | diff to current
2020-10-05 Andrew ReynoldsMake sygus more robust to unknown responses in solution... blob | commitdiff | raw | diff to current
2020-10-01 Mathias PreinerAdd additional ground terms to SyGuS instantiation... blob | commitdiff | raw | diff to current
2020-08-11 Andrew ReynoldsRemove instantiation model true option (#4861) blob | commitdiff | raw | diff to current
2020-07-14 Andrew ReynoldsDebug instantiations output (#4739) blob | commitdiff | raw | diff to current
2020-07-13 Andrew Reynolds User-facing print debug option for sygus candidates... blob | commitdiff | raw | diff to current
2020-07-13 Andrew ReynoldsStatistics on instantiations per quantified formula... blob | commitdiff | raw | diff to current
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... blob | commitdiff | raw | diff to current
2020-06-03 Andrew ReynoldsUse prenex normal form when using cegqi-nested-qe ... blob | commitdiff | raw | diff to current
2020-05-20 Aina NiemetzCegqiBv: Clean up after renaming options. (#4487) blob | commitdiff | raw | diff to current
2020-04-21 Andrew ReynoldsMake option names related to CEGQI consistent (#4316) blob | commitdiff | raw | diff to current
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910) blob | commitdiff | raw | diff to current
2020-04-14 Andrew ReynoldsRemove a few options (#4295) blob | commitdiff | raw | diff to current
2020-03-19 Andrew ReynoldsAlways enable cbqi literal dependency (#4116) blob | commitdiff | raw | diff to current
2020-03-13 Andrew ReynoldsRemoving a few deprecated options (#4052) blob | commitdiff | raw | diff to current
2020-03-12 Andrew ReynoldsRemove local theory extension option (#4048) blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsRemove partial instantiation for local theory extension... blob | commitdiff | raw | diff to current
2020-03-10 Andrew ReynoldsRename sygus option name (#3977) blob | commitdiff | raw | diff to current
2020-02-29 Andrew ReynoldsReplace conditional rewrite pass in quantifiers with... blob | commitdiff | raw | diff to current
2020-02-17 Andrew ReynoldsOption to limit the number of rounds of enumerative... blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) blob | commitdiff | raw | diff to current
2020-01-31 Andrew ReynoldsAllow PBE symmetry breaking with sygus stream (#3686) blob | commitdiff | raw | diff to current
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) blob | commitdiff | raw | diff to current
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... blob | commitdiff | raw | diff to current
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531) blob | commitdiff | raw | diff to current
2019-12-04 Andrew ReynoldsNew grammar construction modes for SyGuS (#3486) blob | commitdiff | raw | diff to current
2019-11-27 Haniel BarbosaEnable sygusRecFun by default and fixes SyGuS+RecFun... blob | commitdiff | raw | diff to current
2019-11-21 Haniel Barbosahard limit for rec-fun eval (#3485) blob | commitdiff | raw | diff to current
2019-11-06 Andrew ReynoldsSupport for SyGuS PBE + recursive functions (#3433) blob | commitdiff | raw | diff to current
2019-09-16 Andrew ReynoldsRemove equality inference option for quantifiers (... blob | commitdiff | raw | diff to current
2019-08-23 Andrew ReynoldsUpdate dynamic splitting strategy for quantifiers ... blob | commitdiff | raw | diff to current
2019-08-14 Andrew ReynoldsCall separate SMT engine for single invocation sygus... blob | commitdiff | raw | diff to current
2019-08-10 Andrew ReynoldsAdd option to only dump unsolved queries for --sygus... blob | commitdiff | raw | diff to current
2019-07-29 Andrew ReynoldsSupport get-abduct smt2 command (#3122) blob | commitdiff | raw | diff to current
2019-07-01 Andrew ReynoldsAdd higher-order elimination preprocessing pass (#2865) blob | commitdiff | raw | diff to current
2019-05-10 Andrew ReynoldsDisable relational triggers (#2994) blob | commitdiff | raw | diff to current
2019-05-09 Andrew ReynoldsFixes for relational triggers (#2967) blob | commitdiff | raw | diff to current
2019-04-16 Andrew ReynoldsStratify enumerative instantiation (#2954) blob | commitdiff | raw | diff to current
2019-04-16 Andrew ReynoldsMinor simplifications to theory quantifiers (#2953) blob | commitdiff | raw | diff to current
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744) blob | commitdiff | raw | diff to current
2019-03-12 Andrew ReynoldsAdd option --sygus-rr-synth-rec for considering all... blob | commitdiff | raw | diff to current
2018-11-28 Andrew ReynoldsGeneralize sygus stream solution filtering to logical... blob | commitdiff | raw | diff to current
2018-11-05 Andrew ReynoldsChange default sygus enumeration mode to auto (#2689) blob | commitdiff | raw | diff to current
2018-10-31 Andrew ReynoldsAdd optimized sygus enumeration (#2677) blob | commitdiff | raw | diff to current
2018-10-20 Andrew ReynoldsSygus streaming non-implied predicates (#2660) blob | commitdiff | raw | diff to current
2018-10-18 Andrew ReynoldsSygus query generator (#2465) blob | commitdiff | raw | diff to current
2018-10-16 Haniel BarbosaOption for shuffling condition pool in CegisUnif (... blob | commitdiff | raw | diff to current
2018-10-13 Andres NoetzliReset input language for ExprMiner subsolver (#2624) blob | commitdiff | raw | diff to current
2018-10-12 Andrew ReynoldsImprovements to rewrite rules from inputs (#2625) blob | commitdiff | raw | diff to current
2018-10-11 Haniel BarbosaFix default setting of CegisUnif options (#2605) blob | commitdiff | raw | diff to current
2018-10-11 Andrew ReynoldsSynthesize rewrite rules from inputs (#2608) blob | commitdiff | raw | diff to current
2018-10-09 Andrew Reynolds Support for basic actively-generated enumerators ... blob | commitdiff | raw | diff to current
2018-10-05 Andrew ReynoldsUpdate default options for sygus (#2586) blob | commitdiff | raw | diff to current
2018-10-03 Andrew ReynoldsAdd actively generated sygus enumerators (#2552) blob | commitdiff | raw | diff to current
2018-09-14 Andrew ReynoldsGeneralize CandidateRewriteDatabase to ExprMiner (... blob | commitdiff | raw | diff to current
2018-09-13 Haniel BarbosaUses information gain heuristic for building better... blob | commitdiff | raw | diff to current
2018-09-11 Haniel BarbosaUsing a single condition enumerator in sygus-unif ... blob | commitdiff | raw | diff to current
2018-08-31 Haniel BarbosaAllows SAT checks of repair const to have different... blob | commitdiff | raw | diff to current
2018-08-21 Andrew ReynoldsMore unused code elimination (#2339) blob | commitdiff | raw | diff to current
2018-08-08 Andrew ReynoldsDisable argument relevance for sygus by default (#2288) blob | commitdiff | raw | diff to current
2018-07-27 Mathias PreinerRequire argument description for non-{bool,void} option... blob | commitdiff | raw | diff to current
2018-07-24 Andrew ReynoldsImprovements to sets + cardinality + quantifiers (... blob | commitdiff | raw | diff to current
2018-07-22 Andrew Reynolds sygusComp2018: Improvements to CEGIS loop (#2187) blob | commitdiff | raw | diff to current
2018-07-21 Andrew ReynoldsOptimizations and fixes for computing whether a type... blob | commitdiff | raw | diff to current
2018-07-20 Andrew Reynolds sygusComp2018: minor changes to repair constant utilit... blob | commitdiff | raw | diff to current
2018-07-17 Andrew Reynolds sygusComp2018: pbe multi-enumerator fairness option... blob | commitdiff | raw | diff to current
2018-07-17 Andrew Reynolds sygusComp2018: update policies for solution reconstruc... blob | commitdiff | raw | diff to current
2018-07-08 Andres NoetzliAdd more sophisticated floating-point sampler (#2155) blob | commitdiff | raw | diff to current
2018-07-06 Andres NoetzliAdd option for timeout for rewrite candidate check... blob | commitdiff | raw | diff to current
2018-06-26 Andres NoetzlisygusComp2018: Add evaluator (#2090) blob | commitdiff | raw | diff to current
2018-06-15 Andrew ReynoldsDisable solving non-linear BV literals by default ... blob | commitdiff | raw | diff to current
2018-05-25 Andrew ReynoldsReenable repair const (#1983) blob | commitdiff | raw | diff to current
2018-05-23 Andrew ReynoldsRepair constants using symbolic constructors (#1960) blob | commitdiff | raw | diff to current
2018-05-19 Haniel Barbosachanging default (#1944) blob | commitdiff | raw | diff to current
2018-05-17 Haniel BarbosaOption to force return values of Bool functions to... blob | commitdiff | raw | diff to current
2018-05-17 Andrew ReynoldsCegis-specific infrastructure (#1933) blob | commitdiff | raw | diff to current
2018-05-14 Andrew ReynoldsAdd regressions, change defaults. (#1911) blob | commitdiff | raw | diff to current
2018-05-10 Andrew ReynoldsSygus repair constants (#1812) blob | commitdiff | raw | diff to current
2018-05-09 Andrew ReynoldsBetter option names for PBE (#1891) blob | commitdiff | raw | diff to current
2018-04-27 Haniel BarbosaNew module for synthesizing functions in a data-driven... blob | commitdiff | raw | diff to current
2018-04-20 Andrew Reynolds Reenable filtering based on ordering in sygus sampler... blob | commitdiff | raw | diff to current
2018-04-04 Andrew ReynoldsOption to turn arbitrary input into sygus (#1704) blob | commitdiff | raw | diff to current
2018-04-03 Andrew ReynoldsImprovements to extended rewriter for Booleans and... blob | commitdiff | raw | diff to current
2018-03-27 Andrew ReynoldsFix for --sygus-rr-synth (#1723) blob | commitdiff | raw | diff to current
2018-03-26 Andrew ReynoldsSynth-check and accelerate options for sygus-rr (#1691) blob | commitdiff | raw | diff to current
2018-03-26 Andrew ReynoldsAbort when sygus-verify finds unsoundness. (#1717) blob | commitdiff | raw | diff to current
next