summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2014-06-30Merge pull request #47 from kbansal/setsKshitij Bansal
2014-06-30Use FS as the set-logic string for theory of setsKshitij Bansal
2014-06-29sets: "insert" operatorKshitij Bansal
2014-06-28Fix bug in datatypes options specificationMorgan Deters
2014-06-27Fix for bug543Clark Barrett
2014-06-25Merge pull request #34 from mdeters/datatypes-kindsAndrew Reynolds
2014-06-25Merge pull request #37 from mdeters/quants-kindsAndrew Reynolds
2014-06-25Merge pull request #38 from mdeters/uf-kindsAndrew Reynolds
2014-06-25fix sets eager lemmasKshitij Bansal
2014-06-25mv default care graph function inside the theory implementationKshitij Bansal
2014-06-25Fixing the previous bugfix.Tim King
2014-06-24Alternative lazier heuristic for assertion rewriting.Tim King
2014-06-24Fixing a soundness bug in arithmetic and a roubustness problem in rings.Tim King
2014-06-24Squashed commit of the following:Morgan Deters
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij Bansal
2014-06-22Merge pull request #39 from mdeters/bv-warningslianah
2014-06-22Merge pull request #35 from mdeters/bv-kindslianah
2014-06-21Fix compiler warnings (mostly unused variables).Morgan Deters
2014-06-21Fix compiler warnings in BV-related code (unused vars mostly).Morgan Deters
2014-06-21Sets kinds documentationMorgan Deters
2014-06-21Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, ...Morgan Deters
2014-06-21fixed build failurelianah
2014-06-20Implement RecordProperties::mkGroundTerm(). Resolves bug #546.Morgan Deters
2014-06-20Bit-vector kinds documentationMorgan Deters
2014-06-20Datatypes kinds documentationMorgan Deters
2014-06-20Quantifiers kinds documentationMorgan Deters
2014-06-20UF kinds documentationMorgan Deters
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-06-19Fix GLPK builds: correct access specifier on cut classes.Morgan Deters
2014-06-19disable unate lemmas when using incremental modeKshitij Bansal
2014-06-19Fix for pre-C++11 is_sorted().Morgan Deters
2014-06-19Final preparations for arithmetic for building with libc++.Morgan Deters
2014-06-19This commit adds a priority queue implementation. This is to avoid compilati...Tim King
2014-06-19Fix rewriter typo.Morgan Deters
2014-06-19Clean up glpk detection a little, fix a detection bug.Morgan Deters
2014-06-19Fix compile errors with some versions of GCC.Morgan Deters
2014-06-19dos2unix-convert some sources.Morgan Deters
2014-06-19Minor fixes, spelling etc.Morgan Deters
2014-06-19More proof support for CASC : include skolemizationajreynol
2014-06-15core solver fixlianah
2014-06-15fixed bv bug due to applying equisatisfiable transformations in ppRewritelianah
2014-06-15fixed fuzzer assertion failures for bvlianah
2014-06-14added rewriting to bv-pow2 passlianah
2014-06-14Evil bitvector preprocessing pass for simplifying powers of two.lianah
2014-06-14bv static learning and rewrites for power of 2 termslianah
2014-06-14more bv rewriteslianah
2014-06-14fix to inequality rewritelianah
2014-06-14added bv inequality rewritelianah
2014-06-14added bv inequality lemmasLiana Hadarean
2014-06-14Fix for fmf with large finite cardinalities.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback