Age | Commit message (Expand) | Author |
2016-09-16 | Let arith_proof print its own terms | Guy |
2016-09-16 | More refactoring of cbqi, start developing new interface. | ajreynol |
2016-09-15 | Further refactor cbqi. | ajreynol |
2016-09-15 | Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul... | ajreynol |
2016-09-15 | Make sep pto a trigger kind, track in equality engines and term database. | ajreynol |
2016-09-15 | Refactor setIncomplete in quantifiers. | ajreynol |
2016-09-14 | Support for unique variable generation in node manager. | ajreynol |
2016-09-14 | Lemma cache in theory sep. Minor optimization for sets. Minor improvements to... | ajreynol |
2016-09-13 | Minor changes to sep logic, epr, quantifier splitting. | ajreynol |
2016-09-12 | Refactor prenex modes. | ajreynol |
2016-09-12 | Remove old implementation of cbqi | ajreynol |
2016-09-12 | Prefer non-cardinality constants in term models for sep logic. | ajreynol |
2016-09-12 | Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry b... | ajreynol |
2016-09-09 | Fix bug in unconstrained simplifier related to sep.nil/distinguished variables. | ajreynol |
2016-09-09 | Support for separation logic + EPR. Refactor preprocessing of sep.nil, only a... | ajreynol |
2016-09-08 | Refactor seplog preprocess. Handle case where sep data type cannot be inferred. | ajreynol |
2016-09-03 | Miniscope top level conjunctions for prenex normal form, allow one level mini... | ajreynol |
2016-09-03 | Option for prenex normal form | ajreynol |
2016-09-01 | Merge pull request #91 from timothy-king/no-throw | Tim King |
2016-09-01 | Fix boolean term issue in invariants from sygus. Minor default options change... | ajreynol |
2016-09-01 | Cleanup quantifier elimination in smt engine. | ajreynol |
2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier... | ajreynol |
2016-09-01 | Relaxing the throw specifiers for the destructors for Node, TypeNode, the con... | Tim King |
2016-08-31 | Removing the forward declaration of QuantInfo from rewrite_engine.h. | Tim King |
2016-08-31 | Cleaning up the dead FORIT macros. | Tim King |
2016-08-31 | Removing the usage of typeof from theory_sets_private. | Tim King |
2016-08-31 | Beautifying theory_model.h. | Tim King |
2016-08-31 | Removing BOOST_FOREACH from theory/sets/scrutinize.h. | Tim King |
2016-08-31 | Removing typeof from sets normal form and beautifying the file. | Tim King |
2016-08-31 | Removing typeof from command_executor_portfolio.cpp. | Tim King |
2016-08-31 | Removing typeof from didyoumean.cpp. | Tim King |
2016-08-26 | Basic support for EPR+CBQI. Minor cleanup. | ajreynol |
2016-08-25 | Minor cleanup preprocessing, add ppNotifyAssertions. | ajreynol |
2016-08-25 | Options for counterexample guided instantiation. | ajreynol |
2016-08-19 | Fixed two bugs | Clark Barrett |
2016-08-19 | Added fitsSignedLong and fitsUnsignedLong | Clark Barrett |
2016-08-16 | Initial infrastructure for ExtTheory, generalize extended term handling in Th... | ajreynol |
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for bounde... | ajreynol |
2016-08-12 | Minor fixes to model construction to take singleton equivalence classes into ... | ajreynol |
2016-08-12 | Merge pull request #90 from 4tXJ7f/fewer_preproc_holes | guykatzz |
2016-08-11 | Add support for fewer preprocessing holes | Andres Notzli |
2016-08-11 | Minor change to strings, introduce proxy vars only when necessary. | ajreynol |
2016-08-10 | Improvements to strings: work on propagations for reverse normal form process... | ajreynol |
2016-08-09 | Merge pull request #89 from 4tXJ7f/fix_proof_spaces | guykatzz |
2016-08-09 | Fixes for sep star rewrite. | ajreynol |
2016-08-09 | Fix missing/redundant spaces in proofsfix_proof_spaces | Andres Notzli |
2016-08-05 | Minor: add/fix comments, remove redundant includes | Andres Notzli |
2016-08-03 | Fixed an issue where arrays proofs would sometimes have an extra ")" at the end. | Guy |
2016-08-03 | Merge pull request #87 from 4tXJ7f/fix_oob_access | barrettcw |
2016-07-30 | Prioritize inferences when processing normal forms in strings. | ajreynol |