summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2014-11-18All Minisat solve calls now return lbool (fixes bug 599)lianah
2014-11-18Compute model basis only for fmf. Add another co-datatype regression.ajreynol
2014-11-18Add local theory extensions instantiation strategy (incomplete). Refactor ho...ajreynol
2014-11-17added command line option for extractArith bv rewritelianah
2014-11-17Short-circuit in TheoryArithPrivate::check(), care of Tim.Morgan Deters
2014-11-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-11-17Resource-limiting work.Liana Hadarean
2014-11-16Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e...ajreynol
2014-11-14Be lazier to consider EQC in UF+cardinality solver. Minor cleanup.ajreynol
2014-11-13Merge pull request #69 from mdeters/bug594Morgan Deters
2014-11-13Remove two obsolete versions of MBQI.ajreynol
2014-11-13More preparation for filtering relevant terms in TermDb.ajreynol
2014-11-12Possible fix for bug594Morgan Deters
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
2014-11-11Work on synchronizing decision=justification and E-matching.ajreynol
2014-11-10Merge pull request #63 from mdeters/theorystrings-hashset-iterationTianyi Liang
2014-11-10Bug 593 fix: if the type is finite, it is now considered for detecting theori...Dejan Jovanović
2014-11-10Do not eliminate variables only occurring in patterns. Minor improvements to...ajreynol
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 regressio...Morgan Deters
2014-11-09Fix dt shared terms issue, reenable regression.ajreynol
2014-11-08Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug48...ajreynol
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 re...Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
2014-11-07Fix missing case in Boolean terms rewriting. (Resolves bug #596.)Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
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 impr...ajreynol
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
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 assertRepre...ajreynol
2014-11-06Minor fix for getInstConsajreynol
2014-11-06Reenable regression. Add (for now, disabled) changes to datatypes theory com...ajreynol
2014-11-05Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.ajreynol
2014-11-05More work on datatypes theory combination: fix bug in care graph, do not assi...ajreynol
2014-11-01Added cache to getModelValueClark Barrett
2014-11-01Fix cegqi for synthesis without syntax.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback