| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-24 | fix mergeinferZero | Andres Noetzli | |
| 2018-09-24 | Merge branch 'master' into inferZero | Andres Noetzli | |
| 2018-09-24 | Make string rewriter unit tests more robust (#2520) | Andres Noetzli | |
| This commit changes the unit test for the string rewriter to use the extended rewriter instead of the regular rewriter to make it more robust, e.g. to different orderings in conjunctions. | |||
| 2018-09-24 | Merge branch 'master' into inferZero | Andrew Reynolds | |
| 2018-09-23 | Fix regress2. (#2502) | Andrew Reynolds | |
| 2018-09-22 | cmake: Fix systemtests dependency. | Mathias Preiner | |
| 2018-09-22 | cmake: Run make coverage in parallel by default. | Mathias Preiner | |
| 2018-09-22 | cmake: Refactor cvc4_add_unit_test macro to support test names with '/'. | Aina Niemetz | |
| Required for consistent naming of tests, unit test names now also use the test naming scheme <category>/<subdir>/<test name>, e.g., unit/theory/theory_bv_white. | |||
| 2018-09-22 | cmake: Require JUnit version 4. | Mathias Preiner | |
| 2018-09-22 | cmake: More documentation, clean up. | Aina Niemetz | |
| 2018-09-22 | cmake: Disable unit tests if assertions are not enabled. | Mathias Preiner | |
| 2018-09-22 | cmake: Do not build examples and unit and system tests by default. | Aina Niemetz | |
| 2018-09-22 | cmake: Added target check | Aina Niemetz | |
| Targets 'check', 'units', 'systemtests' and 'regress' are now run in parallel with the number of available cores by default. This can be overriden by passing ARGS=-jN. | |||
| 2018-09-22 | cmake: Only build libcvc4 and libcvc4parser as libraries. | Mathias Preiner | |
| The sources of all previous libraries are now added to libcvc4 and built as libcvc4. This removes circular dependencies between libcvc4 and libexpr. Further, we now only have one parser library and don't build additional libraries for each language. | |||
| 2018-09-22 | cmake: Rebase with current master, add new tests/source files. | Mathias Preiner | |
| 2018-09-22 | cmake: Compile Java tests and add to ctest if Java bindings are enabled. | Mathias Preiner | |
| 2018-09-22 | cmake: Add dependencies for test targets and support for make coverage. | Aina Niemetz | |
| 2018-09-22 | cmake: Enable parallel execution for test targets regress, units, systemtests. | Aina Niemetz | |
| 2018-09-22 | cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON. | Aina Niemetz | |
| 2018-09-22 | cmake: Added system tests and target make systemtests. | Aina Niemetz | |
| 2018-09-22 | cmake: Added regression tests and target make regress. | Aina Niemetz | |
| 2018-09-22 | cmake: Disable W-suggest-override for unit tests. | Mathias Preiner | |
| 2018-09-22 | cmake: Add target units. | Aina Niemetz | |
| 2018-09-22 | cmake: Removed obsolete CMakeLists file in test. | Aina Niemetz | |
| 2018-09-22 | cmake: Add support for CxxTest. | Aina Niemetz | |
| 2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
| 2018-09-22 | addressed review, fixed rewrite | Andres Noetzli | |
| 2018-09-22 | Use helper function for prefix/suffix | Andres Noetzli | |
| 2018-09-21 | Unify rewrites like (str.contains x y) --> (= x y) | Andres Noetzli | |
| This commit unifies rewrites that turn `(str.contains x y)` into a conjunction of equalities using length-based reasoning. It introduces a generic helper function for determining which `ys` from an inequality `y1 + ... + yn >= x` may be 0 for it to still hold. When we have `(str.contains x y)` and we can show that `str.len(y) >= str.len(x)` then we know that `(str.contains x y) --> (= x y)` and we can use the helper function to determine subterms in `y` that are empty if `y` is in `x`, which allows us to introduce equalities of the form `(= yi "")`. This approach unifies multiple existing rewrites. Additional rewrites will be subsumed once we merge the approximations for arithmetic entailment. | |||
| 2018-09-19 | Add rewrites for str.contains + str.replace/substr (#2496) | Andres Noetzli | |
| 2018-09-18 | Fix issue with str.idof in evaluator (#2493) | Andres Noetzli | |
| 2018-09-17 | Improvements and fixes for symmetry detection and breaking (#2459) | Andrew Reynolds | |
| This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do: - Alpha equivalence to recognize symmetries between quantified formulas, - A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol, - Symmetry breaking for maximal subterms instead of variables. | |||
| 2018-09-17 | Make strings model construction robust to lengths that are not propagated ↵ | Andrew Reynolds | |
| equal (#2444) This fixes #2429. This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment. We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this. Regardless, the strings model construction should be robust to handle this case, which this PR does. | |||
| 2018-09-14 | Refactor how assertions are added to decision engine (#2396) | Andres Noetzli | |
| Before refactoring the preprocessing passes, we were using three arguments to add assertions to the decision engine. Now all that information lives in the AssertionPipeline. This commit moves the AssertionPipeline to its own file and changes the `addAssertions()` methods related to the decision engine to take an AssertionPipeline as an arguement instead of three separate ones. Additionally, the TheoryEngine now uses an AssertionPipeline for lemmas. | |||
| 2018-09-13 | Generalize CandidateRewriteDatabase to ExprMiner (#2340) | Andrew Reynolds | |
| 2018-09-13 | Uses information gain heuristic for building better solutions from DTs (#2451) | Haniel Barbosa | |
| 2018-09-11 | Support model cores via option --produce-model-cores. (#2407) | Andrew Reynolds | |
| This adds support for model cores, fixes #1233. It includes some minor cleanup and additions to utility functions. | |||
| 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-09-06 | Refactor and document quantifiers variable elimination and conditional ↵ | Andrew Reynolds | |
| splitting (#2424) | |||
| 2018-09-05 | Add regex grammar to rewriter verification tests (#2426) | Andres Noetzli | |
| 2018-09-05 | Extended rewriter for string equalities (#2427) | Andrew Reynolds | |
| 2018-09-04 | Remove CVC3 compatibility layer (#2418) | Andres Noetzli | |
| 2018-09-04 | Make quantifiers strategies exit immediately when in conflict (#2099) | Andrew Reynolds | |
| 2018-08-30 | Add regular expression elimination module (#2400) | Andrew Reynolds | |
| 2018-08-28 | Fix for get constraints method in fmf-fun (#2399) | Andrew Reynolds | |
| 2018-08-28 | Fix sort inference for quantified variables of interpreted types (#2393) | Andrew Reynolds | |
| 2018-08-27 | Refactor extended rewriter, move rewrites to aggressive (#2387) | Andrew Reynolds | |
| This is work towards #2305. With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg. | |||
| 2018-08-27 | Make division chainable in the smt2 parser (#2367) | Andrew Reynolds | |
| 2018-08-24 | Refactor nlExtPurify preprocessing pass (#1963) | Haniel Barbosa | |
 |
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