Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-10-11 | Fix heuristic for string length approximation (#2622) | Andrew Reynolds | |
2018-10-11 | Refactor printing of parameterized operators in smt2 (#2609) | Andrew Reynolds | |
2018-10-11 | Improve reasoning about empty strings in rewriter (#2615) | Andres Noetzli | |
2018-10-11 | Fix partial operator elimination in sygus grammar normalization (#2620) | Andrew Reynolds | |
2018-10-11 | Fix string ext inference for rewrites that introduce negation (#2618) | Andrew Reynolds | |
2018-10-10 | Fix default setting of CegisUnif options (#2605) | Haniel Barbosa | |
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-10 | Optimize regular expression elimination (#2612) | Andrew Reynolds | |
2018-10-10 | Add length-based rewrites for (str.substr _ _ _) (#2610) | Andres Noetzli | |
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 | Fix compiler warnings. (#2601) | Aina Niemetz | |
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 | Fix string register extended terms (#2597) | Andrew Reynolds | |
A regress2 benchmark was failing, due to a recent change in our strings rewriter. The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings. The fix is to ensure that extended function terms in any assertions *or shared terms* are registered. This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed. | |||
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-04 | New C++ API: Add checks for Sorts. (#2519) | Aina Niemetz | |
2018-10-04 | Infrastructure for string length entailments via approximations (#2514) | Andrew Reynolds | |
2018-10-04 | Fix end constraint for regexp elimination (#2571) | Andrew Reynolds | |
2018-10-04 | Clean remaining references to getNextDecisionRequest and simplify (#2500) | Andrew Reynolds | |
2018-10-03 | Simplify datatypes printing (#2573) | Andrew Reynolds | |
2018-10-03 | Fix compiler warnings. (#2585) | Aina Niemetz | |
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 | Fix stale op list in sets (#2572) | Andrew Reynolds | |
2018-10-03 | Eliminate partial operators within lambdas during grammar normalization (#2570) | Andrew Reynolds | |
2018-10-02 | Allow (_ to_fp ...) in strict parsing mode (#2566) | Andres Noetzli | |
When parsing with `--strict-parsing`, we are checking whether the operators that we encounter have been explicitly added to the `d_logicOperators` set in the `Parser` class. We did not do that for the indexed operator `(_ to_fp ...)` (which is represented by the kind `FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator. | |||
2018-10-02 | Make registration of preprocessing passes explicit (#2564) | Andres Noetzli | |
As it turns out, self-registering types are problematic with static linkage [0]. Instead of fixing the issue with linker flags, which seems possible but also brittle (e.g. the flags may be different for different linkers), this commit adds an explicit registration of each preprocessing pass. [0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html | |||
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-10-01 | Fix dumping pre/post preprocessing passes (#2469) | Andres Noetzli | |
This commit changes the hard-coded list of checks for preprocessing-related dump tags to take advantage of the new preprocessing pass registration mechanism from PR #2468. It also fixes a typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()` and adds a list of available passes to the `--dump help` output. | |||
2018-10-01 | Refactor preprocessing pass registration (#2468) | Andres Noetzli | |
This commit refactors how preprocessing pass registration works, inspired by LLVM's approach [0]. The basic idea is that every preprocessing pass declares a static variable of type `RegisterPass` in its source file that registers the pass with the `PreprocessingPassRegistry` when starting the program. The registry is a singleton that keeps track of all the available passes and allows other code to create instances of the passes (note: previously the registry itself was owning the passes but this is no longer the case). One of the advantages of this solution is that we have a list of available passes directly at the beginning of the program, which is useful for example when parsing options. As a side effect, this commit also fixes the SortInference pass, which was expecting arguments other than the preprocessing pass context in its constructor. This commit is required for fixing dumping pre/post preprocessing passes. It is also the ground work for allowing the user to specify a preprocessing pipeline using command-line arguments. [0] https://llvm.org/docs/WritingAnLLVMPass.html | |||
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 | Fix bug in getSymbols. (#2544) | Andrew Reynolds | |
2018-09-26 | Makes SyGuS parsing more robust in invariant problems (#2509) | Haniel Barbosa | |
2018-09-26 | Symmetry breaking for variable agnostic enumerators (#2527) | Andrew Reynolds | |