summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2018-09-14Add 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-13Generalize CandidateRewriteDatabase to ExprMiner (#2340)Andrew Reynolds
2018-09-13Fix #include for minisat headers in bvminisat. (#2463)Mathias Preiner
2018-09-13Uses information gain heuristic for building better solutions from DTs (#2451)Haniel Barbosa
2018-09-13Simplify storing of transcendental function applications that occur in ↵Andrew Reynolds
assertions (#2458)
2018-09-13 Decision strategy: incorporate CEGQI (#2460)Andrew Reynolds
2018-09-12New 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-11Fix for when strings process loop is disabled. (#2456)Andrew Reynolds
2018-09-11Fixe compiler warning in line_buffer.cpp. (#2453)Aina Niemetz
2018-09-11Support 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-11Avoid calling size() every iteration (#2450)yoni206
2018-09-10Fix global negate (#2449)Andrew Reynolds
2018-09-10fix (#2446)Haniel Barbosa
2018-09-10Set 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-10Using 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-10Refactor non-clausal simplify preprocessing pass. (#2425)Aina Niemetz
2018-09-10Squash implementation of counterexample-guided instantiation (#2423)Andrew Reynolds
2018-09-10Add (str.replace (str.replace y w y) y z) rewrite (#2441)Andres Noetzli
2018-09-07Replace boost::integer_traits with std::numeric_limits. (#2439)Mathias Preiner
Further, remove redundant gmp.h include in options_handler.cpp.
2018-09-07Remove 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-06Refactor and document quantifiers variable elimination and conditional ↵Andrew Reynolds
splitting (#2424)
2018-09-06Minor 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-05Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)Mathias Preiner
2018-09-05Remove printing support for sygus enumeration types (#2430)Andrew Reynolds
2018-09-05Finer-grained inference of substitutions in incremental mode (#2403)Andrew Reynolds
2018-09-05 Extended rewriter for string equalities (#2427)Andrew Reynolds
2018-09-04Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)Mathias Preiner
2018-09-04Remove 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-04Remove CVC3 compatibility layer (#2418)Andres Noetzli
2018-09-04Remove unused options file (#2413)Andres Noetzli
2018-09-04Minor improvements to theory model builder interface. (#2408)Andrew Reynolds
2018-09-04Make quantifiers strategies exit immediately when in conflict (#2099)Andrew Reynolds
2018-09-04Transfer ownership of learned literals from SMT engine to circuit ↵Aina Niemetz
propagator. (#2421)
2018-09-04Fix merge mishap of #2359.Aina Niemetz
2018-09-04Refactor ceg conjecture initialization (#2411)Andrew Reynolds
2018-08-31Allows SAT checks of repair const to have different options (#2412)Haniel Barbosa
2018-08-31Refactor and document alpha equivalence. (#2402)Andrew Reynolds
2018-08-31Fix export of bound variables (#2409)Haniel Barbosa
2018-08-30Refactor theory preprocess into preprocessing pass. (#2395)Mathias Preiner
2018-08-30Use useBland option in FCSimplexDecisionProcedure (#2405)Andres Noetzli
2018-08-30Add regular expression elimination module (#2400)Andrew Reynolds
2018-08-29Refactor MipLibTrick preprocessing pass. (#2359)Mathias Preiner
2018-08-29Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)Tim King
2018-08-29fix bv total ops printing (#2365)Haniel Barbosa
2018-08-28 Split term canonize utility to own file and document (#2398)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback