| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-09-25 | Eagerly ensure literal on active guards for sygus enumerators (#2531) | Andrew Reynolds | |
| 2018-09-25 | carefully printing trusted assertions in proofs (#2505) | yoni206 | |
| 2018-09-25 | cmake: Fix tag code generation dependencies. (#2529) | Mathias Preiner | |
| 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 | Fix wiki urls. (#2504) | Mathias Preiner | |
| 2018-09-24 | cmake: Fix git version info (again). (#2523) | Aina Niemetz | |
| 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-24 | cmake: Fix and simplify git version info. (#2516) | Aina Niemetz | |
| 2018-09-24 | cmake: Add program prefix option. (#2515) | Mathias Preiner | |
| 2018-09-24 | Fix generating debug/trace tags. | Mathias Preiner | |
| 2018-09-23 | New C++ API: Add checks for Terms/OpTerms. (#2455) | Aina Niemetz | |
| 2018-09-22 | cmake: Add python3 option. | Mathias Preiner | |
| 2018-09-22 | cmake: Enable -Wall. | Mathias Preiner | |
 |
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