summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2020-04-06Cleanup deprecated quantifiers attribute features (#4215)Andrew Reynolds
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
2020-04-01Initialize theory rewriters in theories (#4197)Andres Noetzli
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
2020-03-25 Generalize more uses of string-specific functions (#4145)Andrew Reynolds
2020-03-24Restrict partial triggers to standard quantified formulas (#4144)Andrew Reynolds
2020-03-23Restrict cases of sygus grammar reduction based on argument variants (#4131)Andrew Reynolds
2020-03-23Infer when sygus operators are equivalent to builtin kinds (#4140)Andrew Reynolds
2020-03-23Simplify auxiliary variable handling in CEGQI (#4141)Andrew Reynolds
2020-03-23Throw exception for non-well-founded unimplemented SyGuS types. (#4125)Andrew Reynolds
2020-03-20Generalize mkConcat for types (#4123)Andrew Reynolds
2020-03-20Fix sort comparison within assertion in cegis (#4113)Andrew Reynolds
2020-03-20Split string-specific operators from TheoryStringsRewriter (#3920)Andrew Reynolds
2020-03-20Handle failures for sygus QE preprocess (#4072)Andrew Reynolds
2020-03-20Make handling of illegal internal representatives in quantifiers engine more ...Andrew Reynolds
2020-03-19Remove spurious assertion (#4117)Andrew Reynolds
2020-03-18Always enable cbqi literal dependency (#4116)Andrew Reynolds
2020-03-18Fix issue with multiple infinities in CEGQI for LIRA (#4114)Andrew Reynolds
2020-03-15Handle cases in --sygus-rr where evaluation is not constant (#4100)Andrew Reynolds
2020-03-13Removing a few deprecated options (#4052)Andrew Reynolds
2020-03-13Fix case of non-constant value for sygus sampling (#4051)Andrew Reynolds
2020-03-12Do not make models for quantified function variables (#4039)Andrew Reynolds
2020-03-12Ensure legal candidate equalities when using relational triggers (#4035)Andrew Reynolds
2020-03-11Guard against null relevancy condition in SyGuS (#4033)Andrew Reynolds
2020-03-11Switch to Nodes for conjecture generator (#4026)Andrew Reynolds
2020-03-11Fix non-parametrized operators in subgoal generation (#4023)Andrew Reynolds
2020-03-11Remove partial instantiation for local theory extensions (#4020)Andrew Reynolds
2020-03-11Fix (#4017)Andrew Reynolds
2020-03-11Fix duplicate variable issue in sygus-qe-preproc (#4013)Andrew Reynolds
2020-03-10Logic exception instead of assertion failure for instantiate (#4006)Andrew Reynolds
2020-03-10Fix -Wshadow warnings in sygus_grammar_cons.cpp. (#3986)Aina Niemetz
2020-03-09Remove instantiation propagator infrastructure (#3975)Andrew Reynolds
2020-03-09Ensure standard miniscoping is applied before aggressive miniscoping (#3974)Andrew Reynolds
2020-03-09Eliminate spurious assertion (#3976)Andrew Reynolds
2020-03-06Support default sygus grammar construction for sets (#3842)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-03-03Standardize the interface for SMT engine subsolvers (#3836)Andrew Reynolds
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter (#...Andrew Reynolds
2020-02-28Use enum for quantifiers rewrite steps (#3840)Andrew Reynolds
2020-02-27Fix -Wshadow warnings in common headers (#3826)Andres Noetzli
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-26Use default consts when not using any const during grammar normalization (#3807)Andrew Reynolds
2020-02-24Fixes for quantifiers documentation (#3811)Andrew Reynolds
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2020-02-19Fix symmetry breaking for multiple sygus types (#3775)Andrew Reynolds
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2020-02-17Option to limit the number of rounds of enumerative instantiation (#3760)Andrew Reynolds
2020-02-16Fix simple issue with cache (#3762)Andrew Reynolds
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind aritie...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback