Age | Commit message (Expand) | Author |
2013-09-24 | Reduce compiler dependencies on substitutions.h, | Clark Barrett |
2013-09-23 | Revert Clark's last commit, at his request; there are some bugs. | Morgan Deters |
2013-09-23 | Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h | Clark Barrett |
2013-09-18 | Support for bv2nat/int2bv in parser and BV rewriter. | Morgan Deters |
2013-09-18 | Fixes to theoryof-mode; no longer static in Theory class. | Morgan Deters |
2013-09-15 | Change default option of simple ite lifting within quantifier bodies. add so... | Andrew Reynolds |
2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
2013-09-11 | Theory of strings. | Tianyi Liang |
2013-09-09 | Another minor fix for datatypes to repair my previous commit. | Andrew Reynolds |
2013-09-09 | Support empty (and 1-ary) tuples and records. | Morgan Deters |
2013-09-09 | Ensure no cost for datatypes debugging when not tracing it. | Morgan Deters |
2013-09-06 | Fix datatypes for bug 503 | Andrew Reynolds |
2013-09-05 | Fix bugs/issues with missed-t-prop dump output | Morgan Deters |
2013-08-13 | Minor cleanup. | Morgan Deters |
2013-08-13 | Minor fixes for --fmf-fmc for quantifiers containing datatypes | Andrew Reynolds |
2013-08-13 | initial modifications for per-ic cbqi | Andrew Reynolds |
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters |
2013-07-22 | Allow BV and DT in either order in the logic string | Morgan Deters |
2013-07-22 | Add option --cbqi-recurse. | Andrew Reynolds |
2013-07-22 | Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru... | Andrew Reynolds |
2013-07-19 | possible fix for bug 521 | Dejan Jovanovic |
2013-07-19 | Minor fix for --no-condense-function-values | Morgan Deters |
2013-07-18 | Fix quantifier instantiation bug in cbqi, add default priorities in rewrite e... | Andrew Reynolds |
2013-07-17 | Fix bug 516; include some bug testcases. | Morgan Deters |
2013-07-16 | fixed seg fault when bv equality is turned off | Liana Hadarean |
2013-07-16 | fixed bug520 | Liana Hadarean |
2013-07-16 | "Tabular"-style function definitions in models with --no-condense-function-va... | Morgan Deters |
2013-07-16 | Minor bugfixes to model-building | Morgan Deters |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters |
2013-07-09 | Fix for bug 519; don't involve ITESimplifier in model generation. | Morgan Deters |
2013-07-09 | add relevant domain computation | Andrew Reynolds |
2013-07-02 | Make uf strong solver user-context dependent, fixes bug 522. | Andrew Reynolds |
2013-07-02 | Minor fixes for bounded integers, rewrite engine. | Andrew Reynolds |
2013-06-28 | More bug fixes for interval models. | Andrew Reynolds |
2013-06-27 | Better check-models output for some kinds of problems; add anassertion that t... | Morgan Deters |
2013-06-27 | Small fix for IS_INTEGER. | Morgan Deters |
2013-06-26 | Add support for interval models in bounded integers MBQI (in progress). | Andrew Reynolds |
2013-06-25 | Refactoring of model engine to separate individual implementations of model b... | Andrew Reynolds |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
2013-06-24 | Add options for symmetry breaking in uf+ss totality axiom approach, option fo... | Andrew Reynolds |
2013-06-19 | Workaround for suspected clang 3.0 codegen bug on Mac | Morgan Deters |
2013-06-17 | Make --var-elim-quant true by default. Add rewrite engine to quantifiers mod... | Andrew Reynolds |
2013-06-07 | Fix for bug 517. | Morgan Deters |
2013-06-06 | small parese issue in IDL | Dejan Jovanović |
2013-06-06 | typo | Dejan Jovanović |
2013-06-06 | IDL example theory (to be used with --use-theory=idl). | Dejan Jovanović |
2013-06-05 | Fix bug in --fmf-fmc for producing models of functions not appearing in quant... | Andrew Reynolds |
2013-06-04 | Add --no-condense-function-values option for explicit function models (useful... | Morgan Deters |
2013-06-04 | Merge branch '1.2.x' | Morgan Deters |
2013-06-04 | Fix clang static initialization order issue; fixes bug 512. | Morgan Deters |