| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-19 | Refactor pbRewrites preprocessing pass (#1767) | Andres Noetzli | |
| This commit refactors the pbRewrites preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. It also makes use of the AssertionPipeline::replace function to do proper dependency tracking. | |||
| 2018-04-16 | RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782) | Andres Noetzli | |
| 2018-04-13 | allowing --bool-to-bv without quantifiers (#1771) | yoni206 | |
| 2018-04-12 | Fixes for free variables in assertions (#1762) | Andrew Reynolds | |
| 2018-04-10 | Refactored BVGauss preprocessing pass. (#1766) | Aina Niemetz | |
| 2018-04-10 | Improve accuracy of stats for sygus sampler (#1755) | Andrew Reynolds | |
| 2018-04-09 | Fix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764) | Aina Niemetz | |
| 2018-04-05 | Add more general SignExtendUltConst rewriting. (#1385) | Mathias Preiner | |
| This also adds an additional check in processAssertions to ensure that all assertions are guaranteed to be rewritten (there was only a comment stating this). | |||
| 2018-04-03 | Refactor IntToBV preprocessing pass (#1716) | Andres Noetzli | |
| This commit refactors the IntToBV preprocessing pass into the new style. This commit is essentially just a code move, it does not attempt to fix issues (e.g. #1715). | |||
| 2018-04-03 | Option to turn arbitrary input into sygus (#1704) | Andrew Reynolds | |
| Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving. This includes improvements to the robustness of the sygus solver. | |||
| 2018-04-02 | Remove references to nyu (#1721) | Clark Barrett | |
| 2018-03-25 | Check model only when sat (#1694) | Andrew Reynolds | |
| 2018-03-13 | SmtEngine::getModel() is now public. (#1665) | Aina Niemetz | |
| 2018-03-09 | Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653) | Aina Niemetz | |
| 2018-03-06 | Make statistics output consistent. (#1647) | Mathias Preiner | |
| * Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv"). | |||
| 2018-03-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
| Adds missing override keywords. | |||
| 2018-03-05 | Add support for check-sat-assuming. (#1637) | Aina Niemetz | |
| This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input formula) under assumption (not (or a b)). | |||
| 2018-03-02 | Fixed comments in smt_engine.h. | Aina Niemetz | |
| 2018-02-28 | SmtEngine::getAssignment now returns a vector of assignments. (#1628) | Aina Niemetz | |
| 2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds | |
| 2018-02-12 | Option to use extended rewriter as a preprocessing pass (#1600) | Andrew Reynolds | |
| 2018-02-08 | Minor improvements to sygus sampling. (#1577) | Andrew Reynolds | |
| 2018-02-02 | Option to check solutions produced by SyGuS solver (#1553) | Haniel Barbosa | |
| 2018-02-01 | Use sygus to synthesize/verify rewrite rules (#1547) | Andrew Reynolds | |
| 2018-01-24 | Commenting out throw specifiers on SmtEngine. These can later be refined ↵ | Tim King | |
| into better documentation. (#1512) | |||
| 2018-01-21 | Only push/pop around check-sat if it is associated with an assertion (#1525) | Andrew Reynolds | |
| 2018-01-15 | Removing more miscellaneous throw specifiers. (#1509) | Tim King | |
| Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places. | |||
| 2018-01-09 | Cleaning up throw specifiers on Exception and subclasses. (#1475) | Tim King | |
| 2018-01-09 | Reorganized bitvector.h. (#1505) | Aina Niemetz | |
| 2018-01-08 | Removes throw specifiers from command.{h,cpp}. (#1485) | Tim King | |
| 2018-01-03 | Global negate (#1466) | Andrew Reynolds | |
| 2017-12-27 | Disable sygus PBE when sygus stream is enabled (#1451) | Andrew Reynolds | |
| 2017-12-20 | Fixes for cbqi-bv (#1449) | Andrew Reynolds | |
| 2017-12-10 | Add new infrastructure for preprocessing passes (#1053) | justinxu421 | |
| This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits). | |||
| 2017-12-07 | Fixes related to SyGuS + real arithmetic (#1432) | Andrew Reynolds | |
| 2017-12-06 | Add command for define-fun-rec and add to API (#1412) | Andrew Reynolds | |
| 2017-12-01 | Fix reset-assertions (#1413) | Andres Noetzli | |
| This commit fixes two issues with reset-assertions: - pending pops were not done in SmtEngine, resulting in the following assertion failure: d_userLevels.size() == 0 && d_userContext->getLevel() == 1 - all definitions were erased on reset-assertion in an SMT2 file, leading to errors about undefined types | |||
| 2017-11-30 | Add Gaussian Elimination as a preprocessing pass for BV. (#1342) | Aina Niemetz | |
| This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur. | |||
| 2017-11-29 | Minor improvements and changes to defaults for cbqi bv (#1406) | Andrew Reynolds | |
| This makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables. Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default Allows cbqiNestedQE to be used in the BV logic. Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic). | |||
| 2017-11-29 | Improve caching in term formula removal (#1398) | Andrew Reynolds | |
| 2017-11-27 | Fix models for --solve-real-as-int. (#1371) | Andrew Reynolds | |
| 2017-11-17 | (Refactor) Document and clean single invocation partition. (#1364) | Andrew Reynolds | |
| * Documenting single invocation partiion. * More * More encapsulation. * More, documentation complete. * Split to own file. * Format * Fully encapsulate. * Format * Improvements to doc. * Format * Address * Format * Missed comment * Newline * Address * Format | |||
| 2017-11-17 | Add random number generator. (#1370) | Aina Niemetz | |
| This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016). | |||
| 2017-11-16 | (Refactor) Arithmetic monomial sum (#1381) | Andrew Reynolds | |
| * Add arithmetic monomial sum utility. * Clang format * Fix * Address review. * Fix missed comment. * Format * Fix | |||
| 2017-11-15 | Adding garbage collection for Proof objects. (#1294) | Tim King | |
| 2017-11-14 | Cleaning up exporting vectors within commands. Resolves CID 1172285 and ↵ | Tim King | |
| 1172284. (#1362) | |||
| 2017-11-13 | Disable sygus qe preprocessing by default (#1353) | Andrew Reynolds | |
| * Disable qe preprocessing for sygus by default, add option. * Fix bug * Unnest one * Format | |||
| 2017-11-09 | Higher-order prep (#1338) | Andrew Reynolds | |
| * Minor preparation for final higher-order merge. * Format | |||
| 2017-11-07 | Allow FORALL in quantifier elimination command (#1322) | Andrew Reynolds | |
| * Allow FORALL passed as an argument to get-qe. * Document * Format * Minor | |||
| 2017-11-03 | Sygus clean main (#1297) | Andrew Reynolds | |
| * Remove front end hack for sygus. * Remove other hack, add sygus solution output mode. * Clang format * Minor * Fix * Minor * Remove unused field. | |||
 |
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