summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-11-12Possible fix for bug594Morgan Deters
2014-11-12Merge pull request #65 from mdeters/bv-ineq-cachefixMorgan Deters
Fix BV inequality solver caching, and TNode fix.
2014-11-12BV inequality graph TNode fix.Morgan Deters
2014-11-12Fix BV inequality solver caching.Morgan Deters
2014-11-12Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5.Morgan Deters
2014-11-11Minor cleanup.Morgan Deters
2014-11-11Merge pull request #64 from mdeters/theorysets-hashset-iterationKshitij Bansal
Update TheorySets to use CDHashSet<>::key_begin() / key_end().
2014-11-11Work on synchronizing decision=justification and E-matching.ajreynol
2014-11-10Merge pull request #63 from mdeters/theorystrings-hashset-iterationTianyi Liang
Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().
2014-11-10Bug 593 fix: if the type is finite, it is now considered for detecting ↵Dejan Jovanović
theories of nested terms.
2014-11-10Do not eliminate variables only occurring in patterns. Minor improvements ↵ajreynol
to sort inference. Remove unused code.
2014-11-09Merge branch '1.4.x'Morgan Deters
2014-11-09Update TheorySets to use CDHashSet<>::key_begin() / key_end().Morgan Deters
2014-11-09Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().Morgan Deters
2014-11-09Work around an apparent bug in libc++ that was causing crashes on Mac..Morgan Deters
2014-11-09Fix a deterministic assignment-ordering for get-assignment (fixes a ↵Morgan Deters
regression failure on Mac).
2014-11-09Increase stack size when running regressions (fixes some regression crashes ↵Morgan Deters
on Mac).
2014-11-09Fix dt shared terms issue, reenable regression.ajreynol
2014-11-08Fix bug with incremental+datatypes. Minor cleanup. Disable regression ↵ajreynol
bug484, enable parsing_ringer.
2014-11-08Merge pull request #62 from mdeters/bv-cleanupMorgan Deters
Remove some unused variables.
2014-11-07Remove some unused variables.Morgan Deters
2014-11-07Fixed bug in model builder with subtypesClark Barrett
2014-11-07Remove some dead code.Morgan Deters
2014-11-07Fix a memory leak in SatSolverRegistry (re: bug #594).Morgan Deters
2014-11-07Fix memory issues in bitvector theory, which is now valgrind-clean (mostly ↵Morgan Deters
resolves bug #594).
2014-11-07Merge branch '1.4.x'Morgan Deters
Conflicts: src/smt/model_postprocessor.cpp test/regress/regress0/Makefile.am
2014-11-07Fix missing case in Boolean terms rewriting. (Resolves bug #596.)Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
Conflicts: src/smt/model_postprocessor.cpp
2014-11-07Corrected fix for missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-11-07Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor ↵ajreynol
improvement to performance of E-matching.
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. Conflicts: test/regress/regress0/Makefile.am
2014-11-07Update competition build rules.Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
Conflicts: test/regress/regress0/Makefile.am
2014-11-07Fix missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-11-07Properly 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-06Minor fix for getInstConsajreynol
2014-11-06Reenable regression. Add (for now, disabled) changes to datatypes theory ↵ajreynol
combination. Relax communication of dt facts.
2014-11-05Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.ajreynol
2014-11-05Merge branch '1.4.x'Morgan Deters
2014-11-05Fix get-bug-attachments script.Morgan Deters
2014-11-05More 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-01Added cache to getModelValueClark Barrett
2014-11-01Fix cegqi for synthesis without syntax.ajreynol
2014-11-01Simplify which lemmas to communicate in dt.ajreynol
2014-11-01Fix 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-01Fix some mistakes in datatypes theory combination, disable two regressions. ↵ajreynol
Minor fix for fun defs.
2014-10-31Do not allow duplication of function definitions. Set incomplete flag in ↵ajreynol
model builder.
2014-10-30Be more lazy about generating array lemmasClark Barrett
2014-10-29Added new, much faster, care graph computation for arraysClark Barrett
Force split on true first in combineTheories Fix bugs in getModelValue in bit-vectors
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback