summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
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-20Support nested quantifier elimination for get-qe command (#5490)Andrew Reynolds
2020-11-19Enable new implementation of CEGQI based on nested quantifier elimination (#5...Andrew Reynolds
2020-11-19Add nested quantifier elimination module (#5422)Andrew Reynolds
2020-11-19Fix issues related to eliminating extended arithmetic operators (#5475)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-12(proof-new) Proofs for skolemization (#5339)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-23Apply alpha equivalence to annotated quantified formulas (#5324)Andrew Reynolds
2020-10-20Add finishInit for getInterpol and getAbduct. (#5316)Abdalrhman Mohamed
2020-10-20(proof-new) Update add lazy step interface in LazyCDProof (#5299)Andrew Reynolds
2020-10-20Make seq.nth a trigger kind (#5314)Andrew Reynolds
2020-10-18 (proof-new) Witness axiom reconstruction for purification skolems (#5289)Andrew Reynolds
2020-10-12Eliminate uses of Expr in SmtEngine interface (#5240)Andrew Reynolds
2020-10-11SyGuS instantiation modes (#5228)Mathias Preiner
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-03sygus-inst: Add more special BV values. (#5191)Aina Niemetz
2020-10-01SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185)Aina Niemetz
2020-10-01Add additional ground terms to SyGuS instantiation grammar (#5167)Mathias Preiner
2020-10-01Make SygusSolver use sygus attributes directly (#5172)Andrew Reynolds
2020-09-28Minor fixes to quantifiers proofs (#5151)Andrew Reynolds
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-24 Function definition fmf preprocessing pass (#5064)Andrew Reynolds
2020-09-22Allow E-matching by default when strings are enabled (#5117)Andrew Reynolds
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-14Move quantifiers engine private to own file (#5053)Andrew Reynolds
2020-09-14Fix needsModel method for CEGQI (#5048)Andrew Reynolds
2020-09-14Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)Ying Sheng
2020-09-11Move finite model minimization to UF last call effort (#5050)Andrew Reynolds
2020-09-09Fixes for regular expressions + sygus (#5044)Andrew Reynolds
2020-09-03Minor cleanup of quantifiers engine (#4994)Andrew Reynolds
2020-09-02(proof-new) Support proofs of quantifier instantiation (#5001)Andrew Reynolds
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-28Replace Theory::Set with TheoryIdSet (#4959)Andrew Reynolds
2020-08-28(new theory) Update TheoryQuantifiers to the new interface (#4950)Andrew Reynolds
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-20Add TheoryState objects to each Theory (#4920)Andrew Reynolds
2020-08-20Split QuantElimSolver from SmtEngine (#4919)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback