summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2020-08-20Add TheoryState objects to each Theory (#4920)Andrew Reynolds
2020-08-20Split QuantElimSolver from SmtEngine (#4919)Andrew Reynolds
2020-08-19Simplify trigger notifications in equality engine (#4921)Andrew Reynolds
2020-08-18Split SygusSolver from SmtEngine (#4891)Andrew Reynolds
2020-08-17Dynamic allocation of equality engine in Theory (#4890)Andrew Reynolds
2020-08-14Simplify equality engine notifications (#4896)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-11Remove instantiation model true option (#4861)Andrew Reynolds
2020-08-09Make valuation class more robust to null underlying TheoryEngine. (#4864)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-08-03Generalize interface for candidate rewrite database (#4797)Andrew Reynolds
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-28Use lemma property enum for OutputChannel::lemma (#4755)Andrew Reynolds
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-13Debug instantiations output (#4739)Andrew Reynolds
2020-07-13Minor refactoring of subsolver initialization (#4731)Andrew Reynolds
2020-07-13Fix whitespace issue in instantiations output. (#4737)Andrew Reynolds
2020-07-13 User-facing print debug option for sygus candidates (#4720)Andrew Reynolds
2020-07-13Statistics on instantiations per quantified formula. (#4719)Andrew Reynolds
2020-07-10(proof-new) Update Theory interface for proof-new (#4648)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-17Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)Andrew Reynolds
2020-06-17Improve polynomial anyterm grammar (#3566)Haniel Barbosa
2020-06-16Update copyright headers.Aina Niemetz
2020-06-15(proof-new) Add quantifiers proof checker (#4593)Andrew Reynolds
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-06-03Update CEGQI to use lemma status instead of forcing preprocess (#4551)Andrew Reynolds
2020-06-02Use prenex normal form when using cegqi-nested-qe (#4522)Andrew Reynolds
2020-06-02Fix scope issue with pulling ITEs in extended rewriter. (#4547)Andrew Reynolds
2020-06-02Do not handle universal quantification on functions in model-based FMF (#4226)Andrew Reynolds
2020-05-20CegqiBv: Clean up after renaming options. (#4487)Aina Niemetz
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)Andrew Reynolds
2020-05-19Fix cached free variable identifiers in sygus term database (#4394)Andrew Reynolds
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-05-19Use fresh variables when miniscoping (#4296)Andrew Reynolds
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-16SyGuS instantiation quantifiers module (#3910)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback