| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-03-19 | Bv2int fail on demand | yoni206 | |
| Postpone failure in bv-to-int preprocessing pass. | |||
| 2020-03-12 | Add options for nec regression (#4056) | Andrew Reynolds | |
| Currently an nec benchmark in regress2 is very slow (57 seconds in production) due to disabling the nec-specific options in 67c730c). This reenables these options for this benchmark. | |||
| 2020-03-11 | Switch to Nodes for conjecture generator (#4026) | Andrew Reynolds | |
| Fixes #4022. | |||
| 2020-03-06 | Remove tester name from APIs (#3929) | Andrew Reynolds | |
| This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers. This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue. This is work towards parser migration. | |||
| 2020-03-06 | Support default sygus grammar construction for sets (#3842) | Andrew Reynolds | |
| Fixes #3645. | |||
| 2020-02-24 | bv_to_int preprocessing pass | yoni206 | |
| Introduces a preprocessing pass that translates bv problems to integer problems. | |||
| 2020-02-03 | Example inference utility (#3670) | Andrew Reynolds | |
| 2020-01-14 | Disable unsat cores for regression that times out (#3607) | Andres Noetzli | |
| Regression `regress2/strings/issue3203.smt2` is currently timing out depending on the version of the libraries loaded (see #3606 for more info). This commit temporarily disables the regression to get the nightlies to pass again. | |||
| 2020-01-07 | Update any-constant and normalization policies for sygus grammars (#3583) | Andrew Reynolds | |
| 2019-12-12 | Make CEGIS sampling robust to non-vanilla CEGIS (#3559) | Andrew Reynolds | |
| 2019-12-05 | Refactor mode options for Unif+PI (#3531) | Andrew Reynolds | |
| 2019-09-19 | Support context-(in)dependent decision strategies. (#3281) | Andrew Reynolds | |
| 2019-09-18 | Decouple fmf-bound and finite-model-find (#3297) | Andrew Reynolds | |
| 2019-09-06 | Remove SMT1 parser. (#3228) | Mathias Preiner | |
| This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version). Fixes #2948 and fixes #1313. | |||
| 2019-09-04 | Remove duplicate regression tests. (#3227) | Mathias Preiner | |
| 2019-08-29 | Better heuristic for str.code/re.range (#3220) | Andres Noetzli | |
| To make sure that our `str.code` function is injectve (except for -1 in the codomain), we send the inference that `str.code(x) == -1 v str.code(x) != str.code(y) v x == y` for each pair of `str.code` terms. Because of the order of disjuncts, `str.code(x) != str.code(y)` was usually assigned true. This in turn lead to a difficult problem for the arithmetic engine if there were more `str.code` applications than the size of the domain. E.g. if we had `0 <= str.code(xi) < 10` for 0 <= i <= 10, then the arithmetic engine had a difficult time finding a conflict. This PR improves the heuristic by setting the phase of `str.code(x) != str.code(y)` to false, so we prefer to keep the `str.code` values equal instead of trying to make them different. This change is also reflected in the models produced for inputs involving `str.code`: Previously, we were producing models with different values for the `str.code` whereas now the models are much more uniform. The PR adds two regressions, one testing `str.code` performance directly and one testing it for `str.code` terms generated by `re.range`. Signed-off-by: Andres Noetzli <anoetzli@amazon.com> | |||
| 2019-08-22 | Local substitutions for context-depdendent simplification in strings (#3204) | Andrew Reynolds | |
| 2019-08-02 | Support default sygus grammar for strings (#3148) | Andrew Reynolds | |
| 2019-07-31 | Parsing THF and adding several regressions (#3131) | Haniel Barbosa | |
| 2019-06-10 | Optimization for negative concatenation membership. (#3048) | Andrew Reynolds | |
| 2019-06-04 | Enable proof checking for QF_LRA benchmarks (#2928) | Andres Noetzli | |
| Due to issues in the current proof code, this commit also disables proof checking for five QF_LRA benchmarks (see issue #2855). | |||
| 2019-05-15 | Fix printing of bvurem (#2963) | Andrew Reynolds | |
| 2019-05-09 | Fixes for relational triggers (#2967) | Andrew Reynolds | |
| 2019-04-16 | Stratify enumerative instantiation (#2954) | Andrew Reynolds | |
| 2019-04-05 | fix fp issue (#2940) | Haniel Barbosa | |
| 2019-04-01 | Move slow string regression to regress3 (#2913) | Andres Noetzli | |
| 2019-01-09 | Do not rewrite 1-constructor sygus testers to true (#2780) | Andrew Reynolds | |
| 2018-12-07 | Strings: Make EXTF_d inference more conservative (#2740) | Andres Noetzli | |
| 2018-11-28 | Optimize re-elim for re.allchar components (#2725) | Andrew Reynolds | |
| 2018-11-21 | Support string replace all (#2704) | Andrew Reynolds | |
| 2018-11-20 | Fix real2int regression. (#2716) | Andrew Reynolds | |
| 2018-10-18 | Constant length regular expression elimination (#2646) | Andrew Reynolds | |
| 2018-10-10 | Optimize regular expression elimination (#2612) | Andrew Reynolds | |
| 2018-10-08 | Address slow sygus regressions (#2598) | Andrew Reynolds | |
| 2018-10-03 | Eliminate partial operators within lambdas during grammar normalization (#2570) | Andrew Reynolds | |
| 2018-09-23 | Fix regress2. (#2502) | Andrew Reynolds | |
| 2018-09-22 | cmake: Added regression tests and target make regress. | Aina Niemetz | |
| 2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
| 2018-09-10 | Fix global negate (#2449) | Andrew Reynolds | |
| 2018-09-10 | Add (str.replace (str.replace y w y) y z) rewrite (#2441) | Andres Noetzli | |
| 2018-08-20 | Remove support for *.expect files in regressions (#2341) | Andres Noetzli | |
| Currently, we can optionally specify an *.expect file with the metadata of a regression test. This commit removes that option because it was not widely used, adds maintenance overhead and makes the transition to a new build system more cumbersome. Regression files can still be fed to a solver without removing the metadata first since they are in comments of the corresponding input format (note that this was not always the case, it changed in efc6163629c6c5de446eccfe81777c93829995d5). | |||
| 2018-08-08 | Disable argument relevance for sygus by default (#2288) | Andrew Reynolds | |
| 2018-07-23 | sygusComp2018: add regressions (#2191) | Andrew Reynolds | |
| 2018-07-02 | Modify cegqi heuristic for finite datatypes (#2126) | Andrew Reynolds | |
| 2018-06-28 | Fix stale reference in MiniSat when generating UC (#2113) | Andres Noetzli | |
| In MiniSat's analyze(), we were taking a reference of a clause that could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can lead to allocation of clauses which in turn can lead to clauses being reallocated, making the reference stale. The commit encloses the reference in a code block that makes the lifetime of the reference more obvious and removes uses of the potentially stale reference. | |||
| 2018-05-25 | Reenable repair const (#1983) | Andrew Reynolds | |
| 2018-05-22 | Repair constants using symbolic constructors (#1960) | Andrew Reynolds | |
| 2018-05-15 | adding regressions (#1925) | Haniel Barbosa | |
| 2018-05-14 | Fix annotations in regress2. (#1917) | Andrew Reynolds | |
| 2018-05-14 | Add regressions, change defaults. (#1911) | Andrew Reynolds | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback