| 2015-11-17 |
ajreynol | Improve relevant domain computation for arithmetic... |
commit | commitdiff | tree |
| 2015-11-12 |
Tim King | Updating the contrib/new-theory script and travis to... |
commit | commitdiff | tree |
| 2015-11-12 |
Tim King | Updating the contrib/new-theory script and travis to... |
commit | commitdiff | tree |
| 2015-11-12 |
ajreynol | Minor fixes and improvements to purify quant, relationa... |
commit | commitdiff | tree |
| 2015-11-11 |
ajreynol | Minor fixes to cbqi, purify-quant. Better error checkin... |
commit | commitdiff | tree |
| 2015-11-10 |
ajreynol | Fix infinite loop in datatype enumerator. Minor fixes... |
commit | commitdiff | tree |
| 2015-11-09 |
Tim King | Replacing an inefficient use of std::find(...) to use... |
commit | commitdiff | tree |
| 2015-11-07 |
Tim King | Changing file permissions to add or remove executable... |
commit | commitdiff | tree |
| 2015-11-05 |
Tim King | Merging the google branch back into master. |
commit | commitdiff | tree |
| 2015-11-05 |
Tim King | Fixes some initialization and desctruction problems... |
commit | commitdiff | tree |
| 2015-11-05 |
Tim King | This commit slightly generalizes the scripts for genera... |
commit | commitdiff | tree |
| 2015-11-04 |
ajreynol | Better combination of UF with cbqi, refactor quantifier... |
commit | commitdiff | tree |
| 2015-11-04 |
Tim King | Fixing typo. |
commit | commitdiff | tree |
| 2015-11-03 |
Tim King | Adding a test to ensure the <build>/src/theory director... |
commit | commitdiff | tree |
| 2015-10-31 |
ajreynol | Improvements to handling of mixed Int/Real quantifiers. |
commit | commitdiff | tree |
| 2015-10-30 |
Tim King | Removes an extra dollar sign from src/options/mktaghead... |
commit | commitdiff | tree |
| 2015-10-27 |
Tim King | Adding the new mkdirs script to EXTRA_DIST. This should... |
commit | commitdiff | tree |
| 2015-10-26 |
Tim King | This commit fixes a bug related to a public header... |
commit | commitdiff | tree |
| 2015-10-26 |
Tim King | This commit removes using absolute paths in the generat... |
commit | commitdiff | tree |
| 2015-10-26 |
Tim King | This commit moves the scripts for building the Debug_ta... |
commit | commitdiff | tree |
| 2015-10-26 |
Tim King | This fixes a one definition rule violation for reduceDB... |
commit | commitdiff | tree |
| 2015-10-26 |
ajreynol | Promote InstStrategyCbqi to quantifier module. Cleanup... |
commit | commitdiff | tree |
| 2015-10-26 |
ajreynol | Extend counterexample-guided instantiation to extended... |
commit | commitdiff | tree |
| 2015-10-25 |
Kshitij Bansal | Revert "Default builds are now proof enabled." |
commit | commitdiff | tree |
| 2015-10-24 |
ajreynol | Fixes related to string contains. |
commit | commitdiff | tree |
| 2015-10-24 |
Tim King | This removes a bug for reading data that has been poppe... |
commit | commitdiff | tree |
| 2015-10-24 |
Tim King | Specify that the default initialization must always... |
commit | commitdiff | tree |
| 2015-10-24 |
Tim King | Switching Options::current() to return a pointer. This... |
commit | commitdiff | tree |
| 2015-10-24 |
Tim King | Changes configure.ac so that the single recurisve invoc... |
commit | commitdiff | tree |
| 2015-10-24 |
Tim King | This patch slightly generalizes how the std::isfinite... |
commit | commitdiff | tree |
| 2015-10-22 |
ajreynol | Enable counterexample-guided quantifier instantiation... |
commit | commitdiff | tree |
| 2015-10-21 |
ajreynol | Minor refactoring in strings related to length. |
commit | commitdiff | tree |
| 2015-10-20 |
ajreynol | Refactor strings, remove old cycle checks in normalize... |
commit | commitdiff | tree |
| 2015-10-19 |
ajreynol | Clean up explanations involving string length. Add... |
commit | commitdiff | tree |
| 2015-10-19 |
ajreynol | Improve stratification of strings extended function... |
commit | commitdiff | tree |
| 2015-10-19 |
ajreynol | Improve regexp rewriter, simplify regexp preprocess... |
commit | commitdiff | tree |
| 2015-10-18 |
ajreynol | Fix for no condense func values. |
commit | commitdiff | tree |
| 2015-10-16 |
ajreynol | Add option to interleave enumerative instantiation... |
commit | commitdiff | tree |
| 2015-10-16 |
ajreynol | Throw error for recursively defined types involving... |
commit | commitdiff | tree |
| 2015-10-16 |
ajreynol | Fix for codatatype constant rewrite, add regression. |
commit | commitdiff | tree |
| 2015-10-15 |
ajreynol | Fix congruence check in strings, fixes bug 686. |
commit | commitdiff | tree |
| 2015-10-15 |
ajreynol | Change semantics of str.substr to allow endpoint out... |
commit | commitdiff | tree |
| 2015-10-15 |
ajreynol | Decompose string contains, minor refactoring. |
commit | commitdiff | tree |
| 2015-10-14 |
Kshitij Bansal | Merge pull request #77 from kbansal/macsegfault |
commit | commitdiff | tree |
| 2015-10-13 |
Kshitij Bansal | remove options infrastructure code which depended on... |
commit | commitdiff | tree |
| 2015-10-12 |
Kshitij Bansal | Merge pull request #76 from CVC4/proofs |
commit | commitdiff | tree |
| 2015-10-11 |
Kshitij Bansal | fix regression tests, support fallback mode for proofs |
commit | commitdiff | tree |
| 2015-10-11 |
Liana Hadarean | Default builds are now proof enabled. |
commit | commitdiff | tree |
| 2015-10-11 |
ajreynol | Fix strings preprocessing + incremental, fixes bug... |
commit | commitdiff | tree |
| 2015-10-09 |
Liana Hadarean | Temporary reverting commit 477e72b (proofs as default... |
commit | commitdiff | tree |
| 2015-10-08 |
ajreynol | Minor improvements to strings. Refactor rewriter. Enabl... |
commit | commitdiff | tree |
| 2015-10-07 |
Liana Hadarean | Default builds are now proof enabled. |
commit | commitdiff | tree |
| 2015-10-07 |
Liana Hadarean | Disabled donePPSimpITE when unsat-cores are enabled... |
commit | commitdiff | tree |
| 2015-10-07 |
ajreynol | Minor improvements, add endpoint eq inference to strings. |
commit | commitdiff | tree |
| 2015-10-06 |
ajreynol | More improvements to strings rewriter for regexps,... |
commit | commitdiff | tree |
| 2015-10-02 |
ajreynol | Fixes related to explanations for cycles, sym inference... |
commit | commitdiff | tree |
| 2015-10-02 |
ajreynol | Improvements to rewriter for regexp, contains, indexof... |
commit | commitdiff | tree |
| 2015-10-01 |
ajreynol | Evaluate extended operators on partially concrete argum... |
commit | commitdiff | tree |
| 2015-10-01 |
ajreynol | More improvements to strings. More aggressive inference... |
commit | commitdiff | tree |
| 2015-09-30 |
ajreynol | Refactor strings, bug fix inferences vs lemmas. |
commit | commitdiff | tree |
| 2015-09-29 |
ajreynol | Fix for fmf+incremental. Restrict cbqi to literals... |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Improve quantifiers engine wrt incremental presolve... |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Minor fix |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Minor fixes to strings, add regressions. |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Add missing regression |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Fix bug for trivial extf inferences in strings. Improve... |
commit | commitdiff | tree |
| 2015-09-27 |
ajreynol | Improved handling of extended operators. Do preprocess... |
commit | commitdiff | tree |
| 2015-09-26 |
ajreynol | Lazy preprocessing of extended operators in strings... |
commit | commitdiff | tree |
| 2015-09-26 |
ajreynol | Better organization of quantifiers modules, promote... |
commit | commitdiff | tree |
| 2015-09-25 |
ajreynol | Clear term caches for quantifiers + incremental, fixes... |
commit | commitdiff | tree |
| 2015-09-24 |
ajreynol | Counterexample-guided instantiation for datatypes.... |
commit | commitdiff | tree |
| 2015-09-22 |
ajreynol | Improve ITE redundant branch elimination in quantifiers. |
commit | commitdiff | tree |
| 2015-09-21 |
Kshitij Bansal | Fix for sets segfault (reported by Ravi Kandhadai) |
commit | commitdiff | tree |
| 2015-09-18 |
ajreynol | Fix bug in quantifiers engine where model construction... |
commit | commitdiff | tree |
| 2015-09-18 |
ajreynol | More work mixing UF and sygus. |
commit | commitdiff | tree |
| 2015-09-17 |
ajreynol | Allow most smt2 commands as sygus commands. Fix bug... |
commit | commitdiff | tree |
| 2015-09-16 |
ajreynol | Add option --fmf-fun-rlv, remove deprecated option... |
commit | commitdiff | tree |
| 2015-09-15 |
ajreynol | Fix bug related to quantifiers + incremental, thanks... |
commit | commitdiff | tree |
| 2015-09-11 |
ajreynol | Minor cleanup related to codatatypes. |
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Models for codatatypes. Fixes bug 662. |
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Normalization of codatatype constants, codatatype now... |
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Fix bug 670. Minor. |
commit | commitdiff | tree |
| 2015-09-09 |
ajreynol | Fix bug in strings rewriter regarding lengths of substr... |
commit | commitdiff | tree |
| 2015-09-09 |
ajreynol | Working towards a fair enumerator for codatatypes. |
commit | commitdiff | tree |
| 2015-09-06 |
ajreynol | Improve quantifiers rewriter, minor refactoring. |
commit | commitdiff | tree |
| 2015-09-05 |
ajreynol | Working fix for bugs 610 and 643 regarding check-model... |
commit | commitdiff | tree |
| 2015-09-05 |
ajreynol | Fix bugs related to fmf with incremental. Reinitialize... |
commit | commitdiff | tree |
| 2015-09-04 |
ajreynol | Fix bugs 605 and 667. |
commit | commitdiff | tree |
| 2015-09-02 |
Kshitij Bansal | fix regressions |
commit | commitdiff | tree |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
commit | commitdiff | tree |
| 2015-09-01 |
Clark Barrett | Fixed but with getAssertions |
commit | commitdiff | tree |
| 2015-08-30 |
ajreynol | Minor improvement to sygus sol reconstruction. |
commit | commitdiff | tree |
| 2015-08-28 |
ajreynol | Improvements to sygus, register equivalent terms based... |
commit | commitdiff | tree |
| 2015-08-27 |
ajreynol | Do ITE term bookkeeping when solving Sygus inputs.... |
commit | commitdiff | tree |
| 2015-08-27 |
ajreynol | Modify slow regressions. |
commit | commitdiff | tree |
| 2015-08-26 |
ajreynol | Minor improvements to cbqi, fix bug in solving with... |
commit | commitdiff | tree |
| 2015-08-25 |
ajreynol | Use zero in cbqi when not using infinities. |
commit | commitdiff | tree |
| 2015-08-24 |
Liana Hadarean | Added threshold for core bv cardinality lemmas |
commit | commitdiff | tree |
| 2015-08-24 |
Liana Hadarean | Fix for bv core cardinality lemma generation |
commit | commitdiff | tree |
| 2015-08-24 |
Liana Hadarean | eager bit-blasting gives models for boolean variables... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog