summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus
AgeCommit message (Expand)Author
2020-11-02Move sygus qe preproc to its own file (#5375)Andrew Reynolds
2020-10-28Remove more uses of Expr (#5357)Andrew Reynolds
2020-10-27Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)Abdalrhman Mohamed
2020-10-20Add finishInit for getInterpol and getAbduct. (#5316)Abdalrhman Mohamed
2020-10-12Eliminate uses of Expr in SmtEngine interface (#5240)Andrew Reynolds
2020-10-05SyGuS: Add fp.sub to default FP grammar. (#5206)Aina Niemetz
2020-10-05Make sygus more robust to unknown responses in solution verification (#5199)Andrew Reynolds
2020-10-04Remove subtyping for sets theory (#5179)mudathirmahgoub
2020-10-01SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185)Aina Niemetz
2020-09-27Fix sygus quantifier elimination preprocess for multiple functions (#5130)Andrew Reynolds
2020-09-26Use original quantified formula for single invocation reconstruction (#5129)Andrew Reynolds
2020-09-25Make sygus refinement step more robust to unevaluatable counterexamples (#5102)Andrew Reynolds
2020-09-24SyGuS: Add default grammar for FP. (#5133)Aina Niemetz
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-16Dump commands in internal code using command printing functions. (#5040)Abdalrhman Mohamed
2020-09-14Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)Ying Sheng
2020-09-03Minor cleanup of quantifiers engine (#4994)Andrew Reynolds
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-20Split QuantElimSolver from SmtEngine (#4919)Andrew Reynolds
2020-08-18Split SygusSolver from SmtEngine (#4891)Andrew Reynolds
2020-08-13Fixes for corner case of decision tree learning with different types (#4887)Andrew Reynolds
2020-08-12Fixes for degenerate case of sygus decision tree learning (#4800)Andrew Reynolds
2020-08-07Move datatype index constant to its own file (#4859)Andrew Reynolds
2020-08-06Split preprocessor from SmtEngine (#4854)Andrew Reynolds
2020-08-03Add implementation for SyGuS interpolation module (step4) (#4811)Ying Sheng
2020-07-30Fix null case for sygus printing (#4793)Andrew Reynolds
2020-07-28fixing issue #4808. (#4810)Ying Sheng
2020-07-28Interpolation: Add interface for SyGuS interpolation module (step3) (#4726)Ying Sheng
2020-07-17Enumerate shapes feature in fast sygus enumerator (#4742)Andrew Reynolds
2020-07-15Use Nodes for SmtEngine assertions (#4752)Andres Noetzli
2020-07-14Remove sygus print callback (#4727)Andrew Reynolds
2020-07-13Minor refactoring of subsolver initialization (#4731)Andrew Reynolds
2020-07-13 User-facing print debug option for sygus candidates (#4720)Andrew Reynolds
2020-07-10[Interpolation] Add interface for SyGuS interpolation module (#4677)Ying Sheng
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-07-06Front end support for sequences (#4690)Andrew Reynolds
2020-06-29Make ExprManager constructor private (#4669)Andres Noetzli
2020-06-19Convert more uses of strings to words (#4584)Andrew Reynolds
2020-06-17Improve polynomial anyterm grammar (#3566)Haniel Barbosa
2020-06-16Update copyright headers.Aina Niemetz
2020-06-12Move sygus datatype utility functions to their own file (#4595)Andrew Reynolds
2020-06-04Add sygus datatype substitution utility method (#4390)Andrew Reynolds
2020-06-04Fix abduction with datatypes (#4566)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback