2014-06-06 |
Morgan Deters | Fix submission script (again). |
commit | commitdiff | tree |
2014-06-06 |
Tim King | Patch for the subtype theoryof mode to make the equalit... |
commit | commitdiff | tree |
2014-06-05 |
Morgan Deters | SMT-COMP version gets built --with-abc. |
commit | commitdiff | tree |
2014-06-05 |
Morgan Deters | Add --default-dag-thresh to translator, build translato... |
commit | commitdiff | tree |
2014-06-05 |
Morgan Deters | When printing in SMT, print N-ary bvadd/bvmul/concat... |
commit | commitdiff | tree |
2014-06-04 |
Morgan Deters | Add operator support (resolves bug #563). |
commit | commitdiff | tree |
2014-06-04 |
Morgan Deters | SmtEngine::checkModel() now checks that model values... |
commit | commitdiff | tree |
2014-06-04 |
Morgan Deters | Update commit # for get-abc script, anticipating Liana... |
commit | commitdiff | tree |
2014-06-04 |
Morgan Deters | Fix usability issue with tear-down incremental mode. |
commit | commitdiff | tree |
2014-06-04 |
Morgan Deters | SMT strict mode now disallows N-ary use of concat,... |
commit | commitdiff | tree |
2014-06-04 |
Morgan Deters | Fixing run-script for smt-comp |
commit | commitdiff | tree |
2014-06-03 |
Morgan Deters | Another check when making SMT-COMP submission zipfiles. |
commit | commitdiff | tree |
2014-06-03 |
Morgan Deters | Fix StarExec description files for new requirements. |
commit | commitdiff | tree |
2014-06-03 |
ajreynol | Support E-matching/QCF for Set operators. |
commit | commitdiff | tree |
2014-06-01 |
Morgan Deters | Fix for Windows builds (rlimit doesn't exist on Windows). |
commit | commitdiff | tree |
2014-05-30 |
Morgan Deters | More make rules |
commit | commitdiff | tree |
2014-05-30 |
Morgan Deters | One final bit (I hope) of make magic |
commit | commitdiff | tree |
2014-05-30 |
Morgan Deters | More make rules |
commit | commitdiff | tree |
2014-05-30 |
Morgan Deters | Bug fix for string-opt2 (copied from Tianyi's branch). |
commit | commitdiff | tree |
2014-05-30 |
Morgan Deters | Update submission make rules. |
commit | commitdiff | tree |
2014-05-30 |
ajreynol | Change SMT COMP script to use external timeouts. |
commit | commitdiff | tree |
2014-05-30 |
Morgan Deters | Run script updates: no --stats, also application-track... |
commit | commitdiff | tree |
2014-05-30 |
Kshitij Bansal | run script fix |
commit | commitdiff | tree |
2014-05-30 |
ajreynol | Improve --dt-stc-ind for multi-variable datatype proper... |
commit | commitdiff | tree |
2014-05-30 |
ajreynol | Fixes for --inst-max-level |
commit | commitdiff | tree |
2014-05-30 |
Morgan Deters | Fix personal.mk for some make targets. |
commit | commitdiff | tree |
2014-05-28 |
ajreynol | Minor changes to script. Disable cbqi sat. |
commit | commitdiff | tree |
2014-05-28 |
Andrew Reynolds | Add option to avoid dumping partial models/proofs. |
commit | commitdiff | tree |
2014-05-28 |
Morgan Deters | Some fixes to GC order in Java. |
commit | commitdiff | tree |
2014-05-27 |
Kshitij Bansal | Merge pull request #27 from kbansal/statistics |
commit | commitdiff | tree |
2014-05-27 |
Kshitij Bansal | update stats_black |
commit | commitdiff | tree |
2014-05-27 |
Morgan Deters | New --tear-down-incremental mode, useful for debugging... |
commit | commitdiff | tree |
2014-05-27 |
Kshitij Bansal | fix timespec printing |
commit | commitdiff | tree |
2014-05-27 |
Kshitij Bansal | Revert "timespec printing bug" |
commit | commitdiff | tree |
2014-05-27 |
Kshitij Bansal | timespec printing bug |
commit | commitdiff | tree |
2014-05-27 |
Morgan Deters | Fix typo in Java destruction code; should fix some... |
commit | commitdiff | tree |
2014-05-27 |
Morgan Deters | Improved type-checking for tuple and record selects. |
commit | commitdiff | tree |
2014-05-27 |
Kshitij Bansal | Fix bug 567 |
commit | commitdiff | tree |
2014-05-26 |
Clark Barrett | Fixing Tim's subtype/solving bug for arrays |
commit | commitdiff | tree |
2014-05-26 |
Tim King | Separating an implicit inclusion of smt_engine.h from... |
commit | commitdiff | tree |
2014-05-26 |
Tim King | Fixing a soundness bug due to the default implmentation... |
commit | commitdiff | tree |
2014-05-25 |
Andrew Reynolds | Improve quantifier instantiation: always use original... |
commit | commitdiff | tree |
2014-05-25 |
Morgan Deters | Some cleanup, fix warnings raised by Debian packager. |
commit | commitdiff | tree |
2014-05-23 |
Andrew Reynolds | Fix bug in E-matching Real/Int terms. |
commit | commitdiff | tree |
2014-05-21 |
Morgan Deters | Safer swig-wrapping for unsigned long long in Java... |
commit | commitdiff | tree |
2014-05-20 |
Morgan Deters | Fix compiler warning (missing virtual dtor) |
commit | commitdiff | tree |
2014-05-19 |
Tim King | More documentation fixes. Apologies for multiple commits. |
commit | commitdiff | tree |
2014-05-19 |
Tim King | Fixing documentation for glpk configuration. |
commit | commitdiff | tree |
2014-05-19 |
Tianyi Liang | minor fix for string equality engine assertion. |
commit | commitdiff | tree |
2014-05-17 |
Kshitij Bansal | Merge pull request #26 from kbansal/sets |
commit | commitdiff | tree |
2014-05-16 |
Kshitij Bansal | lfsc_checker: fix some warnings reported by _both_... |
commit | commitdiff | tree |
2014-05-16 |
Kshitij Bansal | sets: fix a bug in model building, another in handling... |
commit | commitdiff | tree |
2014-05-16 |
Kshitij Bansal | minor improvements (fixes) to did-you-mean suggestions |
commit | commitdiff | tree |
2014-05-15 |
Andrew Reynolds | Minor fixes. Add SMTCOMP 2014 script. |
commit | commitdiff | tree |
2014-05-14 |
Andrew Reynolds | Finish --dump-instantiations option. Update scripts. |
commit | commitdiff | tree |
2014-05-13 |
Tianyi Liang | Reject native extended ASCII characters. It requires... |
commit | commitdiff | tree |
2014-05-13 |
Tianyi Liang | Reject un-escaped extended ASCII characters |
commit | commitdiff | tree |
2014-05-13 |
ajreynol | Add lazy strategy for bounded integers to avoid non... |
commit | commitdiff | tree |
2014-05-13 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
2014-05-13 |
Tianyi Liang | Fix a bug in the IndexOf function. |
commit | commitdiff | tree |
2014-05-13 |
Tianyi Liang | Fix a bug in the IndexOf function. |
commit | commitdiff | tree |
2014-05-12 |
Andrew Reynolds | Minor updates/fix to --cbqi-recurse |
commit | commitdiff | tree |
2014-05-12 |
Tim King | Merge remote-tracking branch 'timothy-king/master' |
commit | commitdiff | tree |
2014-05-12 |
Tim King | Merging in additional glpk options and statistics from... |
commit | commitdiff | tree |
2014-05-12 |
Tianyi Liang | Add a benchmark that detects a bug in parsing. Thank... |
commit | commitdiff | tree |
2014-05-12 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
2014-05-12 |
Tianyi Liang | Replace lemma sending with EQ assertions. Fix a typo... |
commit | commitdiff | tree |
2014-05-12 |
Tianyi Liang | Replace lemma sending with EQ assertions. Fix a typo... |
commit | commitdiff | tree |
2014-05-11 |
Andrew Reynolds | More preparation for CASC proofs. Minor fix for sort... |
commit | commitdiff | tree |
2014-05-10 |
Andrew Reynolds | Bug fixes to CBQI. Add first draft of CASC j7 TFF... |
commit | commitdiff | tree |
2014-05-10 |
Morgan Deters | Fix for example installation. |
commit | commitdiff | tree |
2014-05-09 |
Andrew Reynolds | Initial draft of run scripts for CASC j7 |
commit | commitdiff | tree |
2014-05-09 |
Andrew Reynolds | Add variable ordering to ambqi. Bug fix to macros... |
commit | commitdiff | tree |
2014-05-08 |
ajreynol | Major simplifications to macros module. |
commit | commitdiff | tree |
2014-05-08 |
Andrew Reynolds | Fixes to quantifiers rewriter to prevent miniscoping... |
commit | commitdiff | tree |
2014-05-08 |
Andrew Reynolds | Basic optimizations for ambqi : only normalize UF appli... |
commit | commitdiff | tree |
2014-05-08 |
Dejan Jovanovic | Adding encoding of sha1 collision for the hashing example |
commit | commitdiff | tree |
2014-05-08 |
Tianyi Liang | patch to the last commit: add a single character case |
commit | commitdiff | tree |
2014-05-07 |
Tianyi Liang | fix a bug in contain |
commit | commitdiff | tree |
2014-05-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
2014-05-07 |
Tianyi Liang | add splits |
commit | commitdiff | tree |
2014-05-07 |
Tianyi Liang | add splits |
commit | commitdiff | tree |
2014-05-07 |
Andrew Reynolds | Fixes to ambqi, now solution-sound. |
commit | commitdiff | tree |
2014-05-06 |
Andrew Reynolds | First draft of ambqi_builder (new implementation of... |
commit | commitdiff | tree |
2014-05-06 |
Tianyi Liang | fix a bug in replace and contains |
commit | commitdiff | tree |
2014-05-05 |
Tianyi Liang | add constant regular expression check for intersection. |
commit | commitdiff | tree |
2014-05-05 |
Tim King | Improving documentation for glpk-cut-log switch. |
commit | commitdiff | tree |
2014-05-05 |
Morgan Deters | Valuation::entailmentCheck() proxy for TheoryEngine... |
commit | commitdiff | tree |
2014-05-02 |
Morgan Deters | Fix typo in bitvectors example; thanks to Adam Gashlin... |
commit | commitdiff | tree |
2014-05-02 |
Andrew Reynolds | Simplification of EqualityEngine::areDisequal. Compari... |
commit | commitdiff | tree |
2014-05-02 |
ajreynol | Fix assertion from previous commit. |
commit | commitdiff | tree |
2014-05-02 |
Andrew Reynolds | Add option --dt-stc-ind for strengthening skolemization... |
commit | commitdiff | tree |
2014-05-02 |
ajreynol | More minor optimizations for datatypes. |
commit | commitdiff | tree |
2014-05-01 |
ajreynol | Minor optimizations to datatypes, revert to checkClash... |
commit | commitdiff | tree |
2014-05-01 |
Kshitij Bansal | Merge remote-tracking branch 'upstream/master' into... |
commit | commitdiff | tree |
2014-05-01 |
Kshitij Bansal | decision engine: cache start index for and/or nodes |
commit | commitdiff | tree |
2014-04-30 |
Tim King | T-entailment work, and QCF (quant conflict find) work... |
commit | commitdiff | tree |
2014-04-30 |
Morgan Deters | Fix warnings, cleanup in strings typechecker. |
commit | commitdiff | tree |
2014-04-30 |
Morgan Deters | Fix compiler warning re: TheoryUF destructor. |
commit | commitdiff | tree |
2014-04-30 |
Morgan Deters | Fix simplify output for SMT2 printer. |
commit | commitdiff | tree |
next |