Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-11-20 | Disable constants sharing in eq engine, disable hack in theory engine. ↵ | ajreynol | |
Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine. | |||
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters | |
* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.) | |||
2014-07-25 | patch for regular expression intersection caching | Tianyi Liang | |
2014-06-25 | Turn strings-exp off by default (for the release) | Morgan Deters | |
2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ↵ | ajreynol | |
Add regressions. | |||
2014-05-12 | Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report. | Tianyi Liang | |
2014-04-29 | add leading zeros support for str.to.int | Tianyi Liang | |
2014-03-31 | add str to u16/u32, and u16/u32 to str | Tianyi Liang | |
2014-03-27 | adds new feature: re.loop | Tianyi Liang | |
2014-03-07 | Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵ | Morgan Deters | |
bodies; fix bug 551, improper ITE removal under quantifiers. | |||
2014-02-28 | a new regular expression engine for solving both positive and negative ↵ | Tianyi Liang | |
membership constraints | |||
2014-02-26 | sorry for the missing file | Tianyi Liang | |
2014-02-26 | bug fix (caused by merge), move cardinality option to expert option | Tianyi Liang | |
2014-02-20 | fix makefile | Tianyi Liang | |
2014-02-20 | add more tests, and define int.to.str(NEGATIVE)="" | Tianyi Liang | |
2014-02-20 | add two cases to the regression test | Tianyi Liang | |
2014-01-28 | merge internal and user of charat & substr into one | Tianyi Liang | |
2014-01-18 | strings with new ideas | Tianyi Liang | |
2014-01-16 | adds partial functions | Tianyi Liang | |
2013-12-26 | new functions in strings | Tianyi Liang | |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line | |||
2013-12-05 | disable substring in default mode | Tianyi Liang | |
2013-12-03 | adds LB strategy | Tianyi Liang | |
2013-10-21 | add a string test case | Tianyi Liang | |
2013-10-20 | adds regular expression range | Tianyi Liang | |
2013-10-16 | adds fmf for strings | Tianyi Liang | |
2013-10-15 | bug fix: string cache cleaning | Tianyi Liang | |
2013-10-14 | add another regexp test | Tianyi Liang | |
2013-10-14 | Adds Regular Expression support. | Tianyi Liang | |
2013-10-11 | Adds regular expression support, it is actually CFL because of variables. | Tianyi Liang | |
2013-10-01 | adds partial function substr. the use of this function should be guarded, ↵ | Tianyi Liang | |
especially for disequalities | |||
2013-09-30 | replace with a new method for disequality, move to QF_S | Tianyi Liang | |
2013-09-27 | Some fixes to recent strings commits. | Morgan Deters | |
2013-09-27 | adds communication with arith engine | Tianyi Liang | |
2013-09-27 | removes unsound cases, adds unrolling | Tianyi Liang | |
2013-09-27 | adds model generation for strings, and a hacked way in arith engine for models | Tianyi Liang | |
2013-09-18 | Support a personal build configuration and make rules. | Morgan Deters | |
2013-09-11 | Theory of strings. | Tianyi Liang | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> |