summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2018-08-07Delete functions instead of using CVC4_UNDEFINED (#1794)Andres Noetzli
2018-08-06 Move sygus quantifier elimination step for non-ground-single-invocation to s...Andrew Reynolds
2018-08-06Fixes for sygus inference (#2238)Andrew Reynolds
2018-08-01Remove outdated references to TLS (#2245)Andres Noetzli
2018-08-01Fix issues with printing parametric datatypes in smt2 (#2213)Andrew Reynolds
2018-07-31Improvements and tests for the API around separation logic (#2229)ayveejay
2018-07-31Fix option handler for lazy/bv-sat-solver combinations. (#2225)Mathias Preiner
2018-07-30Add support for incremental eager bit-blasting. (#1838)Mathias Preiner
2018-07-27 Make check-synth robust for assertions that are not the synth conjecture (#2...Andrew Reynolds
2018-07-26Disabling bvLazyRewriteExtf in the right place (#2214)yoni206
2018-07-25Performing clang-format on the original change-set of #2194 (#2203)ayveejay
2018-07-24Adding API access methods to get heap/nil expressions when using separation l...ayveejay
2018-07-23Generalize symmetry detection for 1 symmetry variable mapped to n input varia...Andrew Reynolds
2018-07-17Refactor sep-pre-skolem-emp preprocessing passyoni206
2018-07-17Do extended rewrite on results of quantifier elimination. (#2119)Andrew Reynolds
2018-07-10Move rewrite to pass (#2128)Caleb Donovick
2018-07-02sygusComp2018: update sygus-related options setting in smt engine (#2108)Andrew Reynolds
2018-07-02Remove miscellaneous dead and unused code from quantifiers (#2121)Andrew Reynolds
2018-07-02Refactor ApplySubsts preprocessing pass. (#2120)Aina Niemetz
2018-07-02Add missing include (#2127)Caleb Donovick
2018-06-27Synthesize candidate-rewrites from standard inputs (#1918)Andrew Reynolds
2018-06-26 Disable uf symmetry breaker in incremental mode (#2091)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-13Disable unconstrainedSimp pass when proofs enabled (#1976)Andres Noetzli
2018-06-08Reset decisions at SAT level after solving (#2059)Andres Noetzli
2018-06-04Enable cegqi (with model values) for floating point by default (#2023)Andrew Reynolds
2018-05-30Ignore license key in set-info command. (#2021)Aina Niemetz
2018-05-30Fixes for quantifiers + incremental (#2009)Andrew Reynolds
2018-05-29 Make user's SMT2 version override file version (#2004)Andres Noetzli
2018-05-29Disable minisat elimination when nonlinear is enabled (#2006)Andrew Reynolds
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-22Set same options for proofs as for unsat cores (#1957)Andres Noetzli
2018-05-22Disable symmetry breaker for unsat cores (#1958)Andres Noetzli
2018-05-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-05-21Improvements in parsing and printing related to mixed int/real (#1879)Andrew Reynolds
2018-05-15Refactor static learning preprocessing pass (#1857)yoni206
2018-05-14Minor improvements to --nl-ext-purify (#1896)Andrew Reynolds
2018-05-11Fix ackermannize preprocessing pass. (#1904)Aina Niemetz
2018-05-10Sygus repair constants (#1812)Andrew Reynolds
2018-05-10Refactored BVAckermann preprocessing pass. (#1889)Aina Niemetz
2018-05-09Better option names for PBE (#1891)Andrew Reynolds
2018-05-09Make symmetry-breaker-exp into a preprocessing pass (#1890)Andrew Reynolds
2018-05-09Add the symmetry breaker module (#1847)PaulMeng
2018-05-08Refactor bv-abstraction preprocessing pass. (#1860)Mathias Preiner
2018-05-08Infrastructure for approximations in model output (#1884)Andrew Reynolds
2018-05-08Fix order of preprocessing pass registration. (#1887)Aina Niemetz
2018-05-03Refactor bv-intro-pow2 preprocessing pass. (#1851)Mathias Preiner
2018-05-03Fix redundant internalPush calls. (#1865)Mathias Preiner
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback