Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-08-26 | Fix unsigned integer type issues in strings (#2380) | Andrew Reynolds | |
* Fix unsigned integer types in strings. * Format | |||
2018-08-25 | Refactor unconstrained simplification pass (#2374) | Andres Noetzli | |
2018-08-25 | Refactor quantifier macros preprocessing pass (#1840) | yoni206 | |
Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`, and added the necessary methods for inheritance from PreprocessingPass. No need to add a test - regress0 fails when adding Assert(false) when assertions had changed. | |||
2018-08-24 | Refactor nlExtPurify preprocessing pass (#1963) | Haniel Barbosa | |
2018-08-24 | Clean up quantifiers engine initialization. (#2371) | Andrew Reynolds | |
2018-08-24 | Fix more simple coverity warnings (#2372) | Andrew Reynolds | |
2018-08-24 | Remove spurious disabling of cbqi-all (#2368) | Andrew Reynolds | |
2018-08-24 | Add tests that enumerate and verify rewrite rules (#2344) | Andres Noetzli | |
2018-08-23 | Do not print internally generated datatypes in external outputs with sygus ↵ | Andrew Reynolds | |
(#2234) | |||
2018-08-23 | New C++ API: Add checks for kind arguments. (#2369) | Aina Niemetz | |
This should hopefully also take care of the open coverity issues for cvc4cpp.cpp. | |||
2018-08-23 | Replacing allocatedInCMM and d_noTrash with false everywhere in cdhashmap ↵ | Tim King | |
(#2355) There do not appear to be any instances these can be positive. | |||
2018-08-23 | Makes the filename be set in the SMT engine by default (#2366) | Haniel Barbosa | |
2018-08-23 | Fixing some coverity warnings (#2357) | Andrew Reynolds | |
2018-08-23 | Refactor ITE simplification preprocessing pass. (#2360) | Aina Niemetz | |
2018-08-23 | Use "filename" instead of "name" in SmtEngine::setInfo() (#2361) | Andres Noetzli | |
2018-08-22 | global-negate preprocessing pass (#2317) | yoni206 | |
2018-08-22 | More unused code elimination (#2358) | Andrew Reynolds | |
2018-08-22 | Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253) | yoni206 | |
2018-08-22 | Wrapping TheorySetsPrivate in a unique_ptr. (#2356) | Tim King | |
2018-08-22 | Fix invalid iterator comparisons (#2349) | Andrew Reynolds | |
2018-08-21 | Fix processing of nested Variable construct in sygus let bodies (#2351) | Andrew Reynolds | |
2018-08-21 | Removing unused bool members in command.cpp. Also initializes a bool member. ↵ | Tim King | |
(#2321) | |||
2018-08-21 | Warn and enable quantifiers when using sygus + logics with QF (#2352) | Andrew Reynolds | |
2018-08-21 | Makes the new row propagation system default (#2335) | Haniel Barbosa | |
2018-08-21 | Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350) | Mathias Preiner | |
2018-08-21 | Add constexpr annotations to help coverity understand constant ... (#2314) | Tim King | |
2018-08-21 | Use cbqi-full for sygus (#2346) | Andrew Reynolds | |
2018-08-20 | Fix initialization of d_smt in ValidityChecker for changes from #2240. (#2343) | Aina Niemetz | |
2018-08-20 | More unused code elimination (#2339) | Andrew Reynolds | |
2018-08-20 | Remove support for prototype (non-sygus) synthesis (#2338) | Andrew Reynolds | |
2018-08-20 | Minor improvements to the interface for sygus sampler (#2326) | Andrew Reynolds | |
2018-08-20 | Make sygus inference a preprocessing pass (#2334) | Andrew Reynolds | |
2018-08-17 | Remove support for flipDecision (#2319) | Andrew Reynolds | |
2018-08-17 | Remove miscellaneous unused code (#2333) | Andrew Reynolds | |
2018-08-17 | Split sygus grammar to its own ANTLR grammar (#2307) | Andrew Reynolds | |
2018-08-17 | Fix spurious warning in sort inference (#2331) | Andrew Reynolds | |
2018-08-17 | Fix arithmetic division by zero in sygus repair constant module (#2329) | Andrew Reynolds | |
2018-08-17 | Eliminate partial operators in sygus grammar normalization (#2323) | Andrew Reynolds | |
This corrects a bug that was introduced in #2266 (the hack removed there was necessary). This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus. This also enables total semantics for BV div-by-zero for sygus. | |||
2018-08-16 | Initialize inputAssertions only when proofRecipe is non-null (#2325) | Tim King | |
Most of the PR is clang-format cruft from picking up the contents of a PROOF({ ... }); | |||
2018-08-16 | Refactor eager atoms preprocessing pass. (#2318) | Mathias Preiner | |
2018-08-17 | cleaning unnecessary timers/dumps (#2327) | Haniel Barbosa | |
2018-08-16 | Adding support for bitvector SyGuS problems without grammars (#2328) | Haniel Barbosa | |
2018-08-16 | Make quantifiers-preprocess preprocessing pass (#2322) | Caleb Donovick | |
2018-08-16 | Removing coverity warnings from theory_sep.cpp (#2320) | Tim King | |
2018-08-16 | Refactor IteRemoval preprocessing pass (#1793) | Andres Noetzli | |
This commit refactors the IteRemoval pass to follow the new format. In addition to moving the code, this entails the following changes: - The timer for the ITE removal is now called differently (the default timer of PreprocessingPass is used) and measures just the preprocessing pass without applySubstitutions(). It also measures the time used by both invocations of the ITE removal pass. - Debug output will be slightly different because we now just rely on the default functionality of PreprocessingPass. - d_iteRemover is now passed into the PreprocessingPassContext. - AssertionPipeline now owns the d_iteSkolemMap, which makes it accessible by preprocessing passes. The idea behind this is that the preprocessing passes collect information in AssertionPipeline and d_iteSkolemMap fits that pattern. | |||
2018-08-16 | Move node algorithms to separate file (#2311) | Andres Noetzli | |
2018-08-16 | Minor fixes and improvement for sygus to builtin. (#2306) | Andrew Reynolds | |
2018-08-16 | Refactor extended rewriter preprocessing pass (#2324) | Haniel Barbosa | |
2018-08-16 | Refactor apply2const (#2316) | Haniel Barbosa | |
2018-08-15 | Switching an Assert to a CVC4_CHECK to test if it resolves CID 1459595. (#2315) | Tim King | |