Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-11-12 | Possible fix for bug594 | Morgan Deters | |
2014-11-12 | Merge pull request #65 from mdeters/bv-ineq-cachefix | Morgan Deters | |
Fix BV inequality solver caching, and TNode fix. | |||
2014-11-12 | BV inequality graph TNode fix. | Morgan Deters | |
2014-11-12 | Fix BV inequality solver caching. | Morgan Deters | |
2014-11-12 | Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5. | Morgan Deters | |
2014-11-11 | Minor cleanup. | Morgan Deters | |
2014-11-11 | Merge pull request #64 from mdeters/theorysets-hashset-iteration | Kshitij Bansal | |
Update TheorySets to use CDHashSet<>::key_begin() / key_end(). | |||
2014-11-11 | Work on synchronizing decision=justification and E-matching. | ajreynol | |
2014-11-10 | Merge pull request #63 from mdeters/theorystrings-hashset-iteration | Tianyi Liang | |
Update TheoryStrings to use CDHashSet<>::key_begin() / key_end(). | |||
2014-11-10 | Bug 593 fix: if the type is finite, it is now considered for detecting ↵ | Dejan Jovanović | |
theories of nested terms. | |||
2014-11-10 | Do not eliminate variables only occurring in patterns. Minor improvements ↵ | ajreynol | |
to sort inference. Remove unused code. | |||
2014-11-09 | Merge branch '1.4.x' | Morgan Deters | |
2014-11-09 | Update TheorySets to use CDHashSet<>::key_begin() / key_end(). | Morgan Deters | |
2014-11-09 | Update TheoryStrings to use CDHashSet<>::key_begin() / key_end(). | Morgan Deters | |
2014-11-09 | Work around an apparent bug in libc++ that was causing crashes on Mac.. | Morgan Deters | |
2014-11-09 | Fix a deterministic assignment-ordering for get-assignment (fixes a ↵ | Morgan Deters | |
regression failure on Mac). | |||
2014-11-09 | Increase stack size when running regressions (fixes some regression crashes ↵ | Morgan Deters | |
on Mac). | |||
2014-11-09 | Fix dt shared terms issue, reenable regression. | ajreynol | |
2014-11-08 | Fix bug with incremental+datatypes. Minor cleanup. Disable regression ↵ | ajreynol | |
bug484, enable parsing_ringer. | |||
2014-11-08 | Merge pull request #62 from mdeters/bv-cleanup | Morgan Deters | |
Remove some unused variables. | |||
2014-11-07 | Remove some unused variables. | Morgan Deters | |
2014-11-07 | Fixed bug in model builder with subtypes | Clark Barrett | |
2014-11-07 | Remove some dead code. | Morgan Deters | |
2014-11-07 | Fix a memory leak in SatSolverRegistry (re: bug #594). | Morgan Deters | |
2014-11-07 | Fix memory issues in bitvector theory, which is now valgrind-clean (mostly ↵ | Morgan Deters | |
resolves bug #594). | |||
2014-11-07 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: src/smt/model_postprocessor.cpp test/regress/regress0/Makefile.am | |||
2014-11-07 | Fix missing case in Boolean terms rewriting. (Resolves bug #596.) | Morgan Deters | |
2014-11-07 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: src/smt/model_postprocessor.cpp | |||
2014-11-07 | Corrected fix for missing case in model postprocessor (resolves bug #595). | Morgan Deters | |
2014-11-07 | Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor ↵ | ajreynol | |
improvement to performance of E-matching. | |||
2014-11-07 | Revert "Fix missing case in model postprocessor (resolves bug #595)." | Morgan Deters | |
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. | |||
2014-11-07 | Revert "Fix missing case in model postprocessor (resolves bug #595)." | Morgan Deters | |
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. Conflicts: test/regress/regress0/Makefile.am | |||
2014-11-07 | Update competition build rules. | Morgan Deters | |
2014-11-07 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: test/regress/regress0/Makefile.am | |||
2014-11-07 | Fix missing case in model postprocessor (resolves bug #595). | Morgan Deters | |
2014-11-07 | Properly distinguish which EQC to assign values in datatypes, use ↵ | ajreynol | |
assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure. | |||
2014-11-06 | Minor fix for getInstCons | ajreynol | |
2014-11-06 | Reenable regression. Add (for now, disabled) changes to datatypes theory ↵ | ajreynol | |
combination. Relax communication of dt facts. | |||
2014-11-05 | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. | ajreynol | |
2014-11-05 | Merge branch '1.4.x' | Morgan Deters | |
2014-11-05 | Fix get-bug-attachments script. | Morgan Deters | |
2014-11-05 | More work on datatypes theory combination: fix bug in care graph, do not ↵ | ajreynol | |
assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes. | |||
2014-11-01 | Added cache to getModelValue | Clark Barrett | |
2014-11-01 | Fix cegqi for synthesis without syntax. | ajreynol | |
2014-11-01 | Simplify which lemmas to communicate in dt. | ajreynol | |
2014-11-01 | Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in ↵ | ajreynol | |
lemmas being rewritten). Minor improvement to dt care graph. Reenable regressions. | |||
2014-11-01 | Fix some mistakes in datatypes theory combination, disable two regressions. ↵ | ajreynol | |
Minor fix for fun defs. | |||
2014-10-31 | Do not allow duplication of function definitions. Set incomplete flag in ↵ | ajreynol | |
model builder. | |||
2014-10-30 | Be more lazy about generating array lemmas | Clark Barrett | |
2014-10-29 | Added new, much faster, care graph computation for arrays | Clark Barrett | |
Force split on true first in combineTheories Fix bugs in getModelValue in bit-vectors |