Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | Fix #include for minisat headers in bvminisat. (#2463) | Mathias Preiner | |
2018-09-13 | Uses information gain heuristic for building better solutions from DTs (#2451) | Haniel Barbosa | |
2018-09-13 | Simplify storing of transcendental function applications that occur in ↵ | Andrew Reynolds | |
assertions (#2458) | |||
2018-09-13 | Decision strategy: incorporate CEGQI (#2460) | Andrew Reynolds | |
2018-09-12 | New C++ API: Try to fix (false positive) Coverity warnings. (#2454) | Aina Niemetz | |
2018-09-12 | Initial infrastructure for theory decision manager (#2447) | Andrew Reynolds | |
2018-09-11 | Fix for when strings process loop is disabled. (#2456) | Andrew Reynolds | |
2018-09-11 | Fixe compiler warning in line_buffer.cpp. (#2453) | Aina Niemetz | |
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-11 | Avoid calling size() every iteration (#2450) | yoni206 | |
2018-09-10 | Fix global negate (#2449) | Andrew Reynolds | |
2018-09-10 | fix (#2446) | Haniel Barbosa | |
2018-09-10 | Set NodeManager to nullptr when exporting vars (#2445) | Andres Noetzli | |
PR #2409 assumed that temporarily setting the NodeManager to nullptr when creating variables is not needed anymore. However, this made our portfolio build fail. This commit reintroduces the temporary NodeManager change while creating variables. | |||
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. | |||
2018-09-10 | Refactor non-clausal simplify preprocessing pass. (#2425) | Aina Niemetz | |
2018-09-10 | Squash implementation of counterexample-guided instantiation (#2423) | Andrew Reynolds | |
2018-09-10 | Add (str.replace (str.replace y w y) y z) rewrite (#2441) | Andres Noetzli | |
2018-09-07 | Replace boost::integer_traits with std::numeric_limits. (#2439) | Mathias Preiner | |
Further, remove redundant gmp.h include in options_handler.cpp. | |||
2018-09-07 | Remove clock_gettime() replacement for macOS. (#2436) | Mathias Preiner | |
Not needed anymore since macOS 10.12 introduced clock_gettime(). | |||
2018-09-07 | Make isClosedEnumerable a member of TypeNode (#2434) | Andrew Reynolds | |
2018-09-06 | Further simplify and fix initialization of ce guided instantiation (#2437) | Andrew Reynolds | |
2018-09-06 | Refactor and document quantifiers variable elimination and conditional ↵ | Andrew Reynolds | |
splitting (#2424) | |||
2018-09-06 | Minor improvements to interface for rep set. (#2435) | Andrew Reynolds | |
2018-09-05 | More extended rewrites for strings equality (#2431) | Andrew Reynolds | |
2018-09-05 | Eliminate select over store in quantifier bodies (#2433) | Andrew Reynolds | |
2018-09-05 | Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432) | Mathias Preiner | |
2018-09-05 | Remove printing support for sygus enumeration types (#2430) | Andrew Reynolds | |
2018-09-05 | Finer-grained inference of substitutions in incremental mode (#2403) | Andrew Reynolds | |
2018-09-05 | Extended rewriter for string equalities (#2427) | Andrew Reynolds | |
2018-09-04 | Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428) | Mathias Preiner | |
2018-09-04 | Remove redundant strings rewrite. (#2422) | Andrew Reynolds | |
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) ) str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z ) This PR removes the above rewrite, which was implemented incorrectly and was dead code. | |||
2018-09-04 | Remove CVC3 compatibility layer (#2418) | Andres Noetzli | |
2018-09-04 | Remove unused options file (#2413) | Andres Noetzli | |
2018-09-04 | Minor improvements to theory model builder interface. (#2408) | Andrew Reynolds | |
2018-09-04 | Make quantifiers strategies exit immediately when in conflict (#2099) | Andrew Reynolds | |
2018-09-04 | Transfer ownership of learned literals from SMT engine to circuit ↵ | Aina Niemetz | |
propagator. (#2421) | |||
2018-09-04 | Fix merge mishap of #2359. | Aina Niemetz | |
2018-09-04 | Refactor ceg conjecture initialization (#2411) | Andrew Reynolds | |
2018-08-31 | Allows SAT checks of repair const to have different options (#2412) | Haniel Barbosa | |
2018-08-31 | Refactor and document alpha equivalence. (#2402) | Andrew Reynolds | |
2018-08-31 | Fix export of bound variables (#2409) | Haniel Barbosa | |
2018-08-30 | Refactor theory preprocess into preprocessing pass. (#2395) | Mathias Preiner | |
2018-08-30 | Use useBland option in FCSimplexDecisionProcedure (#2405) | Andres Noetzli | |
2018-08-30 | Add regular expression elimination module (#2400) | Andrew Reynolds | |
2018-08-29 | Refactor MipLibTrick preprocessing pass. (#2359) | Mathias Preiner | |
2018-08-29 | Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370) | Tim King | |
2018-08-29 | fix bv total ops printing (#2365) | Haniel Barbosa | |
2018-08-28 | Split term canonize utility to own file and document (#2398) | Andrew Reynolds | |