summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus
AgeCommit message (Expand)Author
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-02-22Eliminate raw use of output channel and valuation in quantifiers (#5933)Andrew Reynolds
2021-02-22Move quantifiers attributes to quantifiers registry (#5929)Andrew Reynolds
2021-02-17Eliminate non-static members in term util (#5919)Andrew Reynolds
2021-02-17Move methods from term util to quantifiers registry (#5916)Andrew Reynolds
2021-02-17Add InferenceId to buffered inference manager (#5911)Gereon Kremer
2021-02-08Use quantifiers inference manager for lemma management (#5867)Andrew Reynolds
2021-02-04Introduce quantifiers registry utility (#5829)Andrew Reynolds
2021-02-02Cleanup some includes (#5847)Andrew Reynolds
2021-01-26Use standard conflict mechanism in quantifiers state (#5822)Andrew Reynolds
2021-01-26Introduce quantifiers inference manager (#5821)Andrew Reynolds
2021-01-26Refactor quantifiers engine initialization (#5813)Andrew Reynolds
2021-01-20Refactoring the single invocation solver (#5706)Andrew Reynolds
2021-01-11Further simplifications in preparation for removing Expr layer (#5756)Andrew Reynolds
2020-12-23Dumping unsat cores after check-sat-assuming/QUERY (#5724)Haniel Barbosa
2020-12-18Simplify internal API for sygus (#5687)Andrew Reynolds
2020-12-15Consolidate basic sygus utilities regarding sygus conjectures (#5421)Andrew Reynolds
2020-12-09Fixed a bunch of clang warnings. (#5637)Gereon Kremer
2020-12-02Update copyright headers.Aina Niemetz
2020-11-30Remove includes for old API from internal code (#5536)Andrew Reynolds
2020-11-23Fix for sygusToBuiltinEval for non-ground composite terms (#5466)Andrew Reynolds
2020-11-20RoundingMode: Rename enum values to conform to code style guidelines. (#5494)Aina Niemetz
2020-11-19Enable new implementation of CEGQI based on nested quantifier elimination (#5...Andrew Reynolds
2020-11-12Simplify sygus solver and sygus stream (#5389)Andrew Reynolds
2020-11-12Fix redundant refinement lemma in sygus solver (#5399)Andrew Reynolds
2020-11-05Split sygus template inference to its own file (#5388)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback