summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2014-05-28Add option to avoid dumping partial models/proofs.Andrew Reynolds
2014-05-27Some fixes to GC order in Java.Morgan Deters
2014-05-27New --tear-down-incremental mode, useful for debugging and performance ↵Morgan Deters
profiling.
2014-05-27fix timespec printingKshitij Bansal
sorry prvs fix added some unrelated code
2014-05-27Revert "timespec printing bug"Kshitij Bansal
This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.
2014-05-27timespec printing bugKshitij Bansal
2014-05-27Fix typo in Java destruction code; should fix some recent bug reports of ↵Morgan Deters
crashes in Java.
2014-05-27Improved type-checking for tuple and record selects.Morgan Deters
2014-05-26Fix bug 567Kshitij Bansal
This bug got introduced in 96eccb0d6134ccf4ead0134299b2e3750a890083. The backing Node didn't always exist because of the changes.
2014-05-26Fixing Tim's subtype/solving bug for arraysClark Barrett
2014-05-26Separating an implicit inclusion of smt_engine.h from theory.h.Tim King
2014-05-26Fixing a soundness bug due to the default implmentation of ↵Tim King
Theory::ppAssert() not respecting subtyping.
2014-05-25Improve quantifier instantiation: always use original terms when matching ↵Andrew Reynolds
(was missing for simple triggers). Minor updates to scripts.
2014-05-24Some cleanup, fix warnings raised by Debian packager.Morgan Deters
2014-05-23Fix bug in E-matching Real/Int terms.Andrew Reynolds
2014-05-21Safer swig-wrapping for unsigned long long in Java, which will throw an ↵Morgan Deters
exception if the argument is out of bounds for unsigned long long. Thanks to Steve Siegel for the report.
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-16minor improvements (fixes) to did-you-mean suggestionsKshitij Bansal
2014-05-15Minor fixes. Add SMTCOMP 2014 script.Andrew Reynolds
2014-05-14Finish --dump-instantiations option. Update scripts.Andrew Reynolds
2014-05-13Reject native extended ASCII characters. It requires user to use escaped ↵Tianyi Liang
sequence for an extended ASCII character.
2014-05-13Reject un-escaped extended ASCII charactersTianyi Liang
2014-05-13Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ↵ajreynol
Add regressions.
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
assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
2014-05-10Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, ↵Andrew Reynolds
minor changes.
2014-05-09Add variable ordering to ambqi. Bug fix to macros. More preparation for ↵Andrew Reynolds
CASC proofs.
2014-05-08Major simplifications to macros module.ajreynol
2014-05-08Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. ↵Andrew Reynolds
Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
2014-05-08Basic optimizations for ambqi : only normalize UF applied to variables, ↵Andrew Reynolds
direct handling of NOT
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 ↵Andrew Reynolds
sets).
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 ↵Morgan Deters
contract is the same as for TheoryEngine version.
2014-05-02Simplification of EqualityEngine::areDisequal. Comparison for production : ↵Andrew Reynolds
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5. Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.
2014-05-02Fix assertion from previous commit.ajreynol
2014-05-02Add option --dt-stc-ind for strengthening skolemization. Refactor ↵Andrew Reynolds
skolemization.
2014-05-02More minor optimizations for datatypes.ajreynol
2014-05-01Minor optimizations to datatypes, revert to checkClash not mod eq. Minor ↵ajreynol
clean up.
2014-05-01Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-30decision engine: cache start index for and/or nodesKshitij Bansal
This is done only in "hard" case. Limited testing has not shown improvement in the "easy" case. This was triggerred by a benchmark sent by andy/viktor. performance comparison notes for the change on wiki http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback