summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2014-06-12Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2014-06-12fixing bv inequality solver explanation buglianah
2014-06-12added bvcomp case to bv to bool liftinglianah
2014-06-11added optionException for trying to use abc in an non-abc buildlianah
2014-06-11switched bv equality orderlianah
2014-06-11Merge pull request #31 from kbansal/setsKshitij Bansal
2014-06-11fixed unit tests failureslianah
2014-06-11sets: comment out an assertion too strongKshitij Bansal
2014-06-11user/sat context issue in setsKshitij Bansal
2014-06-11fix in sets rewriterKshitij Bansal
2014-06-11fixing bv ackermanization cache buglianah
2014-06-10Merging Tim's pseudoboolean work from his fmcad14 branch.Tim King
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-06-06Merge pull request #28 from kbansal/setsKshitij Bansal
2014-06-06Patch for the subtype theoryof mode to make the equalities over disequal type...Tim King
2014-06-06sets: fix equality propagationKshitij Bansal
2014-06-03Support E-matching/QCF for Set operators.ajreynol
2014-05-30Bug fix for string-opt2 (copied from Tianyi's branch).Morgan Deters
2014-05-30Improve --dt-stc-ind for multi-variable datatype properties.ajreynol
2014-05-30Fixes for --inst-max-levelajreynol
2014-05-28Minor changes to script. Disable cbqi sat.ajreynol
2014-05-27Improved type-checking for tuple and record selects.Morgan Deters
2014-05-26Fix bug 567Kshitij Bansal
2014-05-26Fixing Tim's subtype/solving bug for arraysClark Barrett
2014-05-26Fixing a soundness bug due to the default implmentation of Theory::ppAssert()...Tim King
2014-05-25Improve quantifier instantiation: always use original terms when matching (wa...Andrew Reynolds
2014-05-23Fix bug in E-matching Real/Int terms.Andrew Reynolds
2014-05-20Fix compiler warning (missing virtual dtor)Morgan Deters
2014-05-18minor fix for string equality engine assertion.Tianyi Liang
2014-05-16sets: fix a bug in model building, another in handling set of setsKshitij Bansal
2014-05-14Finish --dump-instantiations option. Update scripts.Andrew Reynolds
2014-05-13Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ...ajreynol
2014-05-12Fix a bug in the IndexOf function.Tianyi Liang
2014-05-12Minor updates/fix to --cbqi-recurseAndrew Reynolds
2014-05-12Merging in additional glpk options and statistics from CAV submission.Tim King
2014-05-11Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.Tianyi Liang
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ...Andrew Reynolds
2014-05-10Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m...Andrew Reynolds
2014-05-09Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC...Andrew Reynolds
2014-05-08Major simplifications to macros module.ajreynol
2014-05-08Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Min...Andrew Reynolds
2014-05-08Basic optimizations for ambqi : only normalize UF applied to variables, direc...Andrew Reynolds
2014-05-07patch to the last commit: add a single character caseTianyi Liang
2014-05-07fix a bug in containTianyi Liang
2014-05-07add splitsTianyi Liang
2014-05-07Fixes to ambqi, now solution-sound.Andrew Reynolds
2014-05-06First draft of ambqi_builder (new implementation of MBQI based on disjoint se...Andrew Reynolds
2014-05-05fix a bug in replace and containsTianyi Liang
2014-05-05add constant regular expression check for intersection.Tianyi Liang
2014-05-05Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and c...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback