summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus
AgeCommit message (Expand)Author
2020-05-19Fix cached free variable identifiers in sygus term database (#4394)Andrew Reynolds
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-16SyGuS instantiation quantifiers module (#3910)Mathias Preiner
2020-04-15Convert more cases of strings to words (#4206)Andrew Reynolds
2020-04-14Remove a few spurious assertions (#4294)Andrew Reynolds
2020-04-12Fixes for extended rewriter (#4278)Andrew Reynolds
2020-04-10Ensure exported sygus solutions match grammar (#4270)Andrew Reynolds
2020-03-25 Generalize more uses of string-specific functions (#4145)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-20Fix sort comparison within assertion in cegis (#4113)Andrew Reynolds
2020-03-20Handle failures for sygus QE preprocess (#4072)Andrew Reynolds
2020-03-13Removing a few deprecated options (#4052)Andrew Reynolds
2020-03-11Guard against null relevancy condition in SyGuS (#4033)Andrew Reynolds
2020-03-10Fix -Wshadow warnings in sygus_grammar_cons.cpp. (#3986)Aina Niemetz
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-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-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-16Fix simple issue with cache (#3762)Andrew Reynolds
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-07Interface for example evaluation cache utilities (#3726)Andrew Reynolds
2020-02-07Statistics for fast enumerator (#3699)Andrew Reynolds
2020-02-07Example evaluation cache utility (#3698)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-02-03Example inference utility (#3670)Andrew Reynolds
2020-01-31Update sygus grammar normalization to use node-level datatype. (#3567)Andrew Reynolds
2020-01-31Refactor sygus stats (#3684)Andrew Reynolds
2020-01-31Minor refactoring of constructor classes in fast enumerator (#3685)Andrew Reynolds
2020-01-30Eliminate spurious postprocessing step for single invocation (#3674)Andrew Reynolds
2020-01-30Example minimize evaluation utility. (#3671)Andrew Reynolds
2020-01-23Fix trivial solve method for single invocation (#3650)Andrew Reynolds
2020-01-22Fix check for subtypes in sygus PBE (#3640)Andrew Reynolds
2020-01-22Fix parameteric sorts involving Booleans in sygus default grammars (#3629)Andrew Reynolds
2020-01-17Use axioms when checking goal entailment for abduction algorithm (#3611)Andrew Reynolds
2020-01-14Generalize example-based sym breaking to conjectures with constant function a...Andrew Reynolds
2020-01-10Fix side condition check in sygus core connective (#3600)Andrew Reynolds
2020-01-10Track trivial cases in transition inference (#3598)Andrew Reynolds
2020-01-08Fix backtracking issue in sygus fast enumerator (#3593)Andrew Reynolds
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)Andrew Reynolds
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-16Fix evaluator for non-evaluatable nodes (#3575)Andrew Reynolds
2019-12-13Eliminate Expr-level calls in TypeNode (#3562)Andrew Reynolds
2019-12-12Make CEGIS sampling robust to non-vanilla CEGIS (#3559)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback