| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | Clean remaining references to getNextDecisionRequest and simplify (#2500) | Andrew Reynolds | |
| 2018-09-14 | Refactor how assertions are added to decision engine (#2396) | Andres Noetzli | |
| Before refactoring the preprocessing passes, we were using three arguments to add assertions to the decision engine. Now all that information lives in the AssertionPipeline. This commit moves the AssertionPipeline to its own file and changes the `addAssertions()` methods related to the decision engine to take an AssertionPipeline as an arguement instead of three separate ones. Additionally, the TheoryEngine now uses an AssertionPipeline for lemmas. | |||
| 2018-09-12 | Initial infrastructure for theory decision manager (#2447) | Andrew Reynolds | |
| 2018-09-04 | Minor improvements to theory model builder interface. (#2408) | Andrew Reynolds | |
| 2018-08-25 | Refactor unconstrained simplification pass (#2374) | Andres Noetzli | |
| 2018-08-23 | Refactor ITE simplification preprocessing pass. (#2360) | Aina Niemetz | |
| 2018-08-17 | Remove support for flipDecision (#2319) | Andrew Reynolds | |
| 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 | Move node algorithms to separate file (#2311) | Andres Noetzli | |
| 2018-06-28 | Remove comment about model value hack (#2118) | Andrew Reynolds | |
| This fixes #821. For some background, some special cases were added to equality engine and theory engine a few years ago to handle constants properly. As a result of these changes, a comment in the code was added about a HACK for getModelValue, but the code is completely reasonable looking to me (it says that the model value of a constant is itself). This PR removes that comment. From what I can tell issue #821 can be closed. | |||
| 2018-05-27 | Fix cegqi assertions for quantified non-linear cases. (#1999) | Andrew Reynolds | |
| 2018-05-23 | Add notions of evaluated kinds in TheoryModel (#1947) | Andrew Reynolds | |
| 2018-05-10 | Refactored BVAckermann preprocessing pass. (#1889) | Aina Niemetz | |
| 2018-05-08 | Refactor bv-abstraction preprocessing pass. (#1860) | Mathias Preiner | |
| 2018-05-08 | Infrastructure for approximations in model output (#1884) | Andrew Reynolds | |
| 2018-05-03 | Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834) | Andrew Reynolds | |
| 2018-04-25 | Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788) | yoni206 | |
| 2018-04-16 | RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782) | Andres Noetzli | |
| 2018-04-12 | Fixes for free variables in assertions (#1762) | Andrew Reynolds | |
| 2018-04-08 | Check free variables in assertions (#1737) | Andrew Reynolds | |
| 2018-04-04 | Do not debug check models when unknown (#1748) | Andrew Reynolds | |
| 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-06 | Simplify initialization of quantifiers engine (#1641) | Andrew Reynolds | |
| 2018-02-22 | Fixed disabling the BV equality slicer for quantifiers. (#1623) | Aina Niemetz | |
| This fixes an incorrect condition introduced in #1619 to disable the BV equality slicer. | |||
| 2018-02-21 | Disable BV equality slicer if not pure QF_BV. (#1619) | Aina Niemetz | |
| 2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds | |
| 2018-02-02 | Option to check solutions produced by SyGuS solver (#1553) | Haniel Barbosa | |
| 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. | |||
| 2017-12-08 | Make collect model info return a Bool (#1421) | Andrew Reynolds | |
| 2017-12-06 | Add command for define-fun-rec and add to API (#1412) | Andrew Reynolds | |
| 2017-11-15 | Adding garbage collection for Proof objects. (#1294) | Tim King | |
| 2017-11-01 | (Move-only) Refactor and document theory model part 2 (#1305) | Andrew Reynolds | |
| * Move type set to its own file and document. * Move theory engine model builder to its own class. * Working on documentation. * Document Theory Model. * Minor * Document theory model builder. * Clang format * Address review. | |||
| 2017-10-25 | Removing throw specifiers from OutputChannel and subclasses. (#1209) | Tim King | |
| 2017-09-13 | Floating point symfpu support (#1093) | Martin | |
| Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently. | |||
| 2017-08-23 | Fix typos | Andres Noetzli | |
| 2017-07-20 | Moving from the gnu extensions for hash maps to the c++11 hash maps | Tim King | |
| * Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes. | |||
| 2017-07-07 | Update copyright headers. | Mathias Preiner | |
| 2017-06-18 | Fix assertion | ajreynol | |
| 2017-06-18 | Minor change to ensureTheoryAtoms for bug 828. | ajreynol | |
| 2017-04-04 | Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵ | ajreynol | |
| argument. | |||
| 2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge ↵ | Tim King | |
| commit for nlAlgMaster. | |||
| 2017-03-27 | Making the ExtTheory object a private member of Theory. | Tim King | |
| 2017-03-27 | Making ppNotifyAssertions take a const vector. | Tim King | |
| 2017-03-27 | Moving the CareGraph into its own file. | Tim King | |
| 2017-03-24 | Refactor model building for quantifiers to be a single pass, simplification. ↵ | ajreynol | |
| Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes. | |||
| 2017-03-06 | Adding support for bool-to-bv | Clark Barrett | |
| Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz <katz911@gmail.com> Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass. | |||
| 2017-03-02 | Minor cleanup and reorganization related to last commit. | ajreynol | |
| 2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ | ajreynol | |
| Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. | |||
| 2016-12-16 | Fix dependency tracing for fewerPreprocessingHoles | Andres Notzli | |
| Previously, dependency tracing in `ite_removal.cpp` was only done with the `unsatCores` option but `fewerPreprocessingHoles` requires dependencies, too. This lead to errors during proof construction when `fewerPreprocessingHoles` was active. This commit fixes the condition and includes a test case that previously failed. Additionally, it fixes a similar issue in the theory engine. NOTE: this commit might not fix all instances of this problem. `smt_engine.cpp` turns certain flags off with `unsatCores`. Compatibility between those flags and `fewerPreprocessingHoles` needs to be checked separately. | |||
| 2016-11-18 | Removing some throw specifiers from OutputChannel. Fixes bug 716. | Tim King | |
 |
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