summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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
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-05-01Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-30decision engine: cache start index for and/or nodesKshitij Bansal
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 simplify output for SMT2 printer.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 for --force-logic to extend its reach to the parser.Morgan Deters
2014-04-29fixed couple of more warningsKshitij Bansal
2014-04-29fix was compiler warning in antlr_input, crashing test case with the old fixKshitij Bansal
2014-04-29Revert a compiler warning fix from ea6a5a6.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-28cleanupKshitij Bansal
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-27attempt to improve CVC4's "parse error" messageKshitij Bansal
2014-04-27rm undocument/non-working* "feature"Kshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback