summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2014-05-05Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and c...Morgan Deters
2014-05-02Simplification of EqualityEngine::areDisequal. Comparison for production : h...Andrew Reynolds
2014-05-02Fix assertion from previous commit.ajreynol
2014-05-02Add option --dt-stc-ind for strengthening skolemization. Refactor skolemizat...Andrew Reynolds
2014-05-02More minor optimizations for datatypes.ajreynol
2014-05-01Minor optimizations to datatypes, revert to checkClash not mod eq. Minor cle...ajreynol
2014-04-30T-entailment work, and QCF (quant conflict find) work that uses it.Tim King
2014-04-29Fix warnings, cleanup in strings typechecker.Morgan Deters
2014-04-29Fix compiler warning re: TheoryUF destructor.Morgan Deters
2014-04-29Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrit...Morgan Deters
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-04-29fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlrTianyi Liang
2014-04-29add leading zeros support for str.to.intTianyi Liang
2014-04-29Significantly improve performance for producing datatypes models.ajreynol
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-28add strings-opt2 for regular splittingTianyi Liang
2014-04-28nodemanager robust skolem numberingKshitij Bansal
2014-04-28Merge pull request #25 from kbansal/setsKshitij Bansal
2014-04-28Preparation for models for co-inductive datatypes. Minor cleanup.Andrew Reynolds
2014-04-28Optimizations for datatypes: check for clashes modulo equality. Avoid buildi...ajreynol
2014-04-28minor fixKshitij Bansal
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-24minor change: add a heuristic for preventing constant splitting.Tianyi Liang
2014-04-24optimizationKshitij Bansal
2014-04-24Avoid assigning constructor terms to 1-constructor datatype eqcs, when possib...ajreynol
2014-04-24Compute care graph for datatypes. Preliminary results show 20x speed up on l...Andrew Reynolds
2014-04-24Add --inst-max-level=N option for Kshitij. Support define-const command in S...Andrew Reynolds
2014-04-22Minor fix to avoid rewriting datatype equalities into non-equalitiers, as req...Andrew Reynolds
2014-04-19fix warnings in strings/Kshitij Bansal
2014-04-17Allow fmf-bound-int to be set with set-option and via API.Morgan Deters
2014-04-17simplify mkSkolem naming system: don't use $$Kshitij Bansal
2014-04-17use internal skolem numberingKshitij Bansal
2014-04-17Minor refactoring and optimizing.Andrew Reynolds
2014-04-14Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ...Andrew Reynolds
2014-04-14Add initial support for co-datatypes.Andrew Reynolds
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-04-10minor fix for stringsTianyi Liang
2014-04-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ...Andrew Reynolds
2014-04-09Merge pull request #24 from kbansal/sets-modelKshitij Bansal
2014-04-09Minor change to better support parameterized partial/total kinds (for upcomin...Morgan Deters
2014-04-09Revert E-matching datatypes fix.Andrew Reynolds
2014-04-09Handle fmf.card as input from user, add support in SMT2 parser, as requested ...Andrew Reynolds
2014-04-09fixKshitij Bansal
2014-04-09prep for fixKshitij Bansal
2014-04-09try foreach on CD datastructureKshitij Bansal
2014-04-09moreKshitij Bansal
2014-04-09some debugging changesKshitij Bansal
2014-04-06Merge pull request #21 from pcc/ite-fixTim King
2014-04-01windows build fix for UINT32_MAXTianyi Liang
2014-03-31add str to u16/u32, and u16/u32 to strTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback