| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-19 | Sygus streaming non-implied predicates (#2660) | Andrew Reynolds | |
| 2018-10-17 | Sygus query generator (#2465) | Andrew Reynolds | |
| 2018-10-16 | Option for shuffling condition pool in CegisUnif (#2587) | Haniel Barbosa | |
| 2018-10-12 | Reset input language for ExprMiner subsolver (#2624) | Andres Noetzli | |
| 2018-10-12 | Improvements to rewrite rules from inputs (#2625) | Andrew Reynolds | |
| 2018-10-11 | Fix partial operator elimination in sygus grammar normalization (#2620) | Andrew Reynolds | |
| 2018-10-10 | Fix compiler warnings (#2602) | Andres Noetzli | |
| 2018-10-10 | Synthesize rewrite rules from inputs (#2608) | Andrew Reynolds | |
| 2018-10-10 | Fix cegis so that evaluation unfolding is not interleaved. (#2614) | Andrew Reynolds | |
| 2018-10-09 | Support for basic actively-generated enumerators (#2606) | Andrew Reynolds | |
| 2018-10-09 | Random: support URNG interface (#2595) | Aina Niemetz | |
| Use std::shuffle (with Random as the unified random generator) instead of std::random_shuffle for deterministic, reproducable random shuffling. | |||
| 2018-10-09 | Allow multiple synthesis conjectures. (#2593) | Andrew Reynolds | |
| 2018-10-08 | BV instantiator: Factor out util functions. (#2604) | Aina Niemetz | |
| Previously, all util functions for the BV instantiator were static functions in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h). Asan reported errors for the corresponing unit test because of this. | |||
| 2018-10-08 | BV inverter: Factor out util functions. (#2603) | Aina Niemetz | |
| Previously, all invertibility condition functions were static functions in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/bv_inverter_utils.(cpp|h). | |||
| 2018-10-08 | Disable extended rewriter when applicable with var agnostic enumeration (#2594) | Andrew Reynolds | |
| 2018-10-05 | Fix unif trace (#2550) | Haniel Barbosa | |
| 2018-10-05 | Fix cache for sygus post-condition inference (#2592) | Andrew Reynolds | |
| 2018-10-05 | Update default options for sygus (#2586) | Andrew Reynolds | |
| 2018-10-04 | Fix rewrite rule filtering. (#2591) | Andrew Reynolds | |
| 2018-10-03 | Add actively generated sygus enumerators (#2552) | Andrew Reynolds | |
| 2018-10-03 | Make CegisUnif with condition independent robust to var agnostic (#2565) | Haniel Barbosa | |
| 2018-10-03 | Eliminate partial operators within lambdas during grammar normalization (#2570) | Andrew Reynolds | |
| 2018-10-01 | init scalar class members (coverity issues 1473720 and 1473721) (#2554) | Haniel Barbosa | |
| 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-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 | 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-22 | cmake: Remove unused CMakeLists.txt | Mathias Preiner | |
| 2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
| 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 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-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-13 | Decision strategy: incorporate CEGQI (#2460) | Andrew Reynolds | |
| 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 (#2446) | Haniel Barbosa | |
| 2018-09-10 | Using a single condition enumerator in sygus-unif (#2440) | Haniel Barbosa | |
| This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case). In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts: - _main advantage_: can quickly enumerate relevant condition values for solving the problem - _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie. A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif. There is also small improvements for trace messages. | |||
 |
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