Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-10-01 | init scalar class members (coverity issues 1473720 and 1473721) (#2554) | Haniel Barbosa | |
2018-10-01 | Fix compiler warnings. (#2555) | Aina Niemetz | |
2018-09-30 | Add rewrite for solving stoi (#2532) | Andrew Reynolds | |
2018-09-29 | Stream concrete values for variable agnostic enumerators (#2526) | Haniel Barbosa | |
2018-09-28 | Rewrites for (= "" _) and (= (str.replace _) _) (#2546) | Andres Noetzli | |
2018-09-27 | Remove assertion. (#2549) | Andrew Reynolds | |
2018-09-27 | Infrastructure for using active enumerators in sygus modules (#2547) | Andrew Reynolds | |
2018-09-27 | Incorporate all unification enumerators into getTermList. (#2541) | Andrew Reynolds | |
2018-09-27 | Fix Taylor overapproximation for large exponentials (#2538) | Andrew Reynolds | |
2018-09-26 | Fix homogeneous string constant rewrite (#2545) | Andrew Reynolds | |
2018-09-26 | Symmetry breaking for variable agnostic enumerators (#2527) | Andrew Reynolds | |
2018-09-25 | Eagerly ensure literal on active guards for sygus enumerators (#2531) | Andrew Reynolds | |
2018-09-25 | Fix warnings uncovered by cmake build (#2521) | Andrew Reynolds | |
2018-09-24 | Fix quantifiers selector over store rewrite (#2510) | Andrew Reynolds | |
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in. After the change, we are +61-7 on SMT LIB: https://www.starexec.org/starexec/secure/details/job.jsp?id=30581 | |||
2018-09-24 | Allow partial models for multiple sygus enumerators (#2499) | Andrew Reynolds | |
2018-09-24 | Infrastructure for variable agnostic sygus enumerators (#2511) | Andrew Reynolds | |
2018-09-24 | Improve non-linear check model error handling (#2497) | Andrew Reynolds | |
2018-09-24 | Refactor strings equality rewriting (#2513) | Andrew Reynolds | |
This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter. | |||
2018-09-24 | cmake: Fix dependencies for code generation. (#2524) | Mathias Preiner | |
2018-09-24 | cmake: Fix theory order #2. (#2522) | Mathias Preiner | |
2018-09-24 | Unify rewrites related to (str.contains x y) --> (= x y) (#2512) | Andres Noetzli | |
2018-09-24 | cmake: Fix theory order. (#2518) | Mathias Preiner | |
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: Remove unused CMakeLists.txt | Mathias Preiner | |
2018-09-22 | cmake: Working build infrastructure. | Mathias Preiner | |
TODO: cvc4autoconfig.h | |||
2018-09-22 | cmake: .cpp generation done, .h generation not yet complete | Aina Niemetz | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-09-19 | Decision strategy: incorporate arrays. (#2495) | Andrew Reynolds | |
2018-09-19 | Add rewrites for str.contains + str.replace/substr (#2496) | Andres Noetzli | |
2018-09-18 | Decision strategy: incorporate separation logic. (#2494) | Andrew Reynolds | |
2018-09-18 | Add two rewrites for string contains character (#2492) | Andrew Reynolds | |
2018-09-18 | Refactor strings extended functions inferences (#2480) | Andrew Reynolds | |
This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type. This is in preparation for working on solving equations and further inferences in this style. | |||
2018-09-18 | Fix issue with str.idof in evaluator (#2493) | Andres Noetzli | |
2018-09-18 | Decision strategy: incorporate strings fmf. (#2485) | Andrew Reynolds | |
2018-09-18 | More aggressive caching of string skolems. (#2491) | Andrew Reynolds | |
2018-09-18 | Move and rename sygus solver classes (#2488) | Andrew Reynolds | |
2018-09-17 | Clean remaining references to getNextDecisionRequest in quantifiers. (#2484) | Andrew Reynolds | |
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 | Move inst_strategy_cbqi to inst_strategy_cegqi (#2477) | Andrew Reynolds | |
2018-09-17 | Decision strategy: incorporate cegis unif (#2482) | Andrew Reynolds | |
2018-09-17 | Decision strategy: incorporate bounded integers (#2481) | Andrew Reynolds | |
2018-09-17 | Decision strategy: incorporate datatypes sygus solver. (#2479) | Andrew Reynolds | |
2018-09-17 | More aggressive skolem caching for strings, document and clean preprocessor ↵ | Andrew Reynolds | |
(#2478) | |||
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-17 | Decision strategy: incorporate UF with cardinality constraints (#2476) | Andrew Reynolds | |
2018-09-17 | Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462) | Andrew Reynolds | |
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-14 | Add Skolem cache for strings, refactor length registration (#2457) | Andrew Reynolds | |
This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor). It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled. | |||
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 | |