Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-04-26 | FCSimplex branch merge | Tim King | |
2013-04-23 | Theory "alternates" support | Morgan Deters | |
* This is a feature that Dejan and I want for the upcoming tutorial. It allows rapid prototyping of new decision procedure implementations (which we may choose to demonstrate), and a new --use-theory command-line option to select from different available implementations. It has no affect on the current set of theories, as no "alternates" are defined. * Also update the new-theory script, which was broken and incomplete. | |||
2013-04-22 | add bit0 and bit1 constants to smt-lib v1 parser | Morgan Deters | |
2013-04-18 | making sure sat context is zero when user context is popped to 0 in ↵ | lianah | |
SmtEngine destructor | |||
2013-04-18 | fixing destruction order in SmtEngine | lianah | |
2013-04-17 | bool flatten: node num_children workaround | Kshitij Bansal | |
2013-04-17 | boolean flatten: bug fix in dfs search | Kshitij Bansal | |
(this is not intended to (and doesn't) address the issue with NodeBuilder limit) | |||
2013-04-16 | boolean flatten rewrite: dont re-rewrite | Kshitij Bansal | |
2013-04-16 | generalize to handle and | Kshitij Bansal | |
2013-04-16 | flatten or nodes | Kshitij Bansal | |
2013-04-11 | Improved speed of no redundant lemma assertion by using hash set | Clark Barrett | |
2013-04-11 | Fixes for getModelVal in bv theory | Clark Barrett | |
2013-04-11 | Added check for infinite lemma loop | Clark Barrett | |
2013-04-10 | fixed getModelValue to only query the value of leaves and evaluate more ↵ | lianah | |
complex bv terms | |||
2013-04-09 | Change TPTP parser to not use the STRING type; this necessary to repurpose ↵ | Morgan Deters | |
strings for the upcoming string theory | |||
2013-04-03 | * changing the bitblast-eager to bitblast on pre-register | Dejan Jovanović | |
* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate) * when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true) * bitblast-eager implies decision=internal | |||
2013-04-03 | Some final minor changes before cutting 1.1. | Morgan Deters | |
* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression | |||
2013-04-03 | abort quantifiers check if master equality engine is inconsistent. | Andrew Reynolds | |
2013-04-02 | Making arithmetic model reversion on unsat checks an option. | Tim King | |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-02 | Remove old README file from rewrite-rules left over from new-theory script ↵ | Morgan Deters | |
long ago | |||
2013-04-01 | update copyrights | Morgan Deters | |
2013-04-01 | Fix regression error by turning off model-based solver when models are on | Clark Barrett | |
(ironic, yes, but model-based solver doesn't yet produce models) | |||
2013-04-01 | Turning on model based array solver for QF_AX | Clark Barrett | |
2013-04-01 | Made eager lemmas an option, enabled for QF_AX | Clark Barrett | |
2013-04-01 | Disabling eager array index splitting for QF_AX | Clark Barrett | |
2013-04-01 | Fixes for two bugs: | Morgan Deters | |
* one that Tim found in model generation for records containing Booleans * another that the fuzzer found in quantifiers + check-models Test cases enabled/added for both. | |||
2013-04-01 | Cleaning up the demand restart code. | Tim King | |
2013-04-01 | Adding a restart test strategy to integers. | Tim King | |
2013-04-01 | Adding demand restart. | Tim King | |
2013-04-01 | Merging some cleanup work: | Morgan Deters | |
* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed | |||
2013-04-01 | Fix for iff terms over equalities between the same term and differing constants. | Tim King | |
2013-04-01 | Fix bug 491 and related issues with checkModel() and quantifiers. Enabling ↵ | Morgan Deters | |
previously-failing testcase. | |||
2013-04-01 | fixed TheoryBool rewriter bug | lianah | |
2013-04-01 | fixed bug 502; now the core bv solver only gives the model for variables and ↵ | lianah | |
shared terms. | |||
2013-03-30 | changed option to run inequality solver by default | Liana Hadarean | |
2013-03-30 | Disabling eager array index splitting for QF_AUFLIA | Clark Barrett | |
Minor changes to model-based array solver | |||
2013-03-30 | do simple ite rewriting within quantifiers | Andrew Reynolds | |
2013-03-29 | make Boolean term conversion partially non-recursive (resolves bug 501) | Morgan Deters | |
2013-03-29 | Merge branch 'master' of github.com:CVC4/CVC4 | Dejan Jovanović | |
2013-03-29 | removing cryptominisat since we're not using it | Dejan Jovanović | |
2013-03-28 | fix memory corruption in arrays destructor | Morgan Deters | |
2013-03-27 | some Java bindings fixes (fixes Debian build problems) | Morgan Deters | |
2013-03-27 | Fixed a warning, made eager-index default to true (better for QF_AUFBV) | Clark Barrett | |
2013-03-27 | Fixed bug in arrays | Clark Barrett | |
2013-03-27 | Added assertion | Clark Barrett | |
2013-03-27 | Updates to model-based array solver | Clark Barrett | |
Minor fixes to bv and theory_engine | |||
2013-03-27 | New model-based array procedure | Clark Barrett | |
2013-03-27 | reverted the core solver to do static slicing, added option --bv-core-solver | lianah | |
2013-03-27 | fixed inequality checkDisequalities inefficiency | lianah | |