summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2018-08-25Refactor unconstrained simplification pass (#2374)Andres Noetzli
2018-08-25Refactor quantifier macros preprocessing pass (#1840)yoni206
2018-08-24Refactor nlExtPurify preprocessing pass (#1963)Haniel Barbosa
2018-08-24 Remove spurious disabling of cbqi-all (#2368)Andrew Reynolds
2018-08-23 Do not print internally generated datatypes in external outputs with sygus (...Andrew Reynolds
2018-08-23Makes the filename be set in the SMT engine by default (#2366)Haniel Barbosa
2018-08-23Refactor ITE simplification preprocessing pass. (#2360)Aina Niemetz
2018-08-23Use "filename" instead of "name" in SmtEngine::setInfo() (#2361)Andres Noetzli
2018-08-22global-negate preprocessing pass (#2317)yoni206
2018-08-21Removing unused bool members in command.cpp. Also initializes a bool member. ...Tim King
2018-08-21Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350)Mathias Preiner
2018-08-21Use cbqi-full for sygus (#2346)Andrew Reynolds
2018-08-20 Make sygus inference a preprocessing pass (#2334)Andrew Reynolds
2018-08-17 Eliminate partial operators in sygus grammar normalization (#2323)Andrew Reynolds
2018-08-16Refactor eager atoms preprocessing pass. (#2318)Mathias Preiner
2018-08-17cleaning unnecessary timers/dumps (#2327)Haniel Barbosa
2018-08-16Make quantifiers-preprocess preprocessing pass (#2322)Caleb Donovick
2018-08-16Refactor IteRemoval preprocessing pass (#1793)Andres Noetzli
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-08-16Refactor extended rewriter preprocessing pass (#2324)Haniel Barbosa
2018-08-16Refactor apply2const (#2316)Haniel Barbosa
2018-08-15Remove unused tuple classes (#2313)Andres Noetzli
2018-08-15Make sort inference a preprocessing pass (#2309)Andrew Reynolds
2018-08-15Fix dumping of get-unsat-assumptions (#2302)Andres Noetzli
2018-08-13Fix get-unsat-assumptions output (#2301)Andres Noetzli
2018-08-08Do beta-reduction in expandDefinitions (#2286)Andrew Reynolds
2018-08-07Require Swig 3 (#2283)Andres Noetzli
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback