summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-06-10Some news about API changes.Morgan Deters
2014-06-10Merging Tim's pseudoboolean work from his fmcad14 branch.Tim King
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-06-10reverting portfolio hacklianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-06-09Disallow copy/assignment of SmtEngine.Morgan Deters
2014-06-09Tim's options for QF_LIA and QF_LRA---SOI+approx.Morgan Deters
2014-06-09Merge pull request #29 from kbansal/alternatefixKshitij Bansal
Fix for emptyset in smt2 parser, sets translator to quantified logic, misc
2014-06-09Add missing set of braces, fixes --trace.Morgan Deters
Also ensure // commented Debug() lines don't get included in Debug/Trace_tags.
2014-06-08parseErrorHelper : factor out whole word matchingKshitij Bansal
catches some corner cases, more readable too
2014-06-08test for prvs commit (tokenize emptyset)Kshitij Bansal
9978c259f30b1f4b2c70c04589a309033a6eb1f6
2014-06-08Previous "repeat" fix required extra lookahead (leading to assert-fails). ↵Morgan Deters
Fixed, at the cost of an antlr warning that's safe to ignore for now.
2014-06-08smt2 parser: tokenize emptyset only if theory enabledKshitij Bansal
2014-06-08Better error when there are \backslashes in |quoted symbols|.Morgan Deters
2014-06-08Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).Morgan Deters
2014-06-08sets translate: a different translation using axiomsKshitij Bansal
todo: set logic correctly, split the code for two translators
2014-06-06sets translator: fix for dagsKshitij Bansal
2014-06-06Merge pull request #28 from kbansal/setsKshitij Bansal
Sets translator, bug fixes
2014-06-06Fix submission script (again).Morgan Deters
2014-06-06rm warning from helloworld exampleKshitij Bansal
2014-06-06Patch for the subtype theoryof mode to make the equalities over disequal ↵Tim King
types get sent to the theory of the type. Adding a new test case for bug 569. Fixes to the normal form of arithmetic so that real terms are before integer terms.
2014-06-06sets: fix equality propagationKshitij Bansal
2014-06-06-{d,t} help => --show-{debug,trace}-tagsKshitij Bansal
2014-06-06option to hide stats which are zero (off by default), also some aliasesKshitij Bansal
2014-06-06Sets translate, and other short fixesKshitij Bansal
- $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine
2014-06-05SMT-COMP version gets built --with-abc.Morgan Deters
2014-06-05Add --default-dag-thresh to translator, build translator with other examples.Morgan Deters
2014-06-05When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary.Morgan Deters
2014-06-04Add operator support (resolves bug #563).Morgan Deters
2014-06-04SmtEngine::checkModel() now checks that model values are of the correct type ↵Morgan Deters
(related to bug #569).
2014-06-04Update commit # for get-abc script, anticipating Liana's merge.Morgan Deters
2014-06-04Fix usability issue with tear-down incremental mode.Morgan Deters
2014-06-04SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, ↵Morgan Deters
bvor, and bvxor.
2014-06-03Fixing run-script for smt-compMorgan Deters
2014-06-03Another check when making SMT-COMP submission zipfiles.Morgan Deters
2014-06-03Fix StarExec description files for new requirements.Morgan Deters
2014-06-03Support E-matching/QCF for Set operators.ajreynol
2014-06-01Fix for Windows builds (rlimit doesn't exist on Windows).Morgan Deters
2014-05-30More make rulesMorgan Deters
2014-05-30One final bit (I hope) of make magicMorgan Deters
2014-05-30More make rulesMorgan Deters
2014-05-30Bug fix for string-opt2 (copied from Tianyi's branch).Morgan Deters
2014-05-30Update submission make rules.Morgan Deters
2014-05-30Change SMT COMP script to use external timeouts.ajreynol
2014-05-30Run script updates: no --stats, also application-track version.Morgan Deters
2014-05-30run script fixKshitij Bansal
2014-05-30Improve --dt-stc-ind for multi-variable datatype properties.ajreynol
2014-05-30Fixes for --inst-max-levelajreynol
2014-05-30Fix personal.mk for some make targets.Morgan Deters
2014-05-28Minor changes to script. Disable cbqi sat.ajreynol
2014-05-28Add option to avoid dumping partial models/proofs.Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback