Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-03-11 | Merge branch '1.3.x' | Morgan Deters | |
2014-03-11 | Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok. | Morgan Deters | |
2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. ↵ | Andrew Reynolds | |
Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter. Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up. QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master. Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern. Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE. Merging rewrite rules into master, check-model current fails on 3 FMF regressions. Fix check-model issue, a line of code was omitted during merge. | |||
2014-03-10 | adds intro vars length cache | Tianyi Liang | |
2014-03-10 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-03-10 | minor change for strings-fmf | Tianyi Liang | |
2014-03-10 | minor change for strings-fmf | Tianyi Liang | |
2014-03-08 | Re-fix bug 551 by adding a check to the arith ITE simplifier to ignore ↵ | Morgan Deters | |
non-ground ITEs also. | |||
2014-03-08 | Merge pull request #18 from timothy-king/master | Tim King | |
Merging in the glpk changes | |||
2014-03-08 | Fixing name changes that cam in from the merge. | Tim King | |
2014-03-08 | Merge remote-tracking branch 'CVC4root/master' | Tim King | |
2014-03-07 | Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵ | Morgan Deters | |
bodies; fix bug 551, improper ITE removal under quantifiers. | |||
2014-03-07 | Fix run_regression on Mac. | Morgan Deters | |
2014-03-07 | Fix bug 554 (nominally). | Morgan Deters | |
2014-03-07 | Fixing a SWIG problem for RationalFromDoubleException. | Tim King | |
2014-03-07 | Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into ↵ | Tim King | |
master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled. | |||
2014-03-07 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-03-07 | remove unrolling depth | Tianyi Liang | |
2014-03-07 | bring back D-Norm | Tianyi Liang | |
2014-03-07 | Fix strings-exp setting. | Morgan Deters | |
2014-03-07 | remove unrolling depth | Tianyi Liang | |
2014-03-07 | bring back D-Norm | Tianyi Liang | |
2014-03-07 | Fix strings-exp setting. | Morgan Deters | |
2014-03-07 | Add swig renames for new Z3STR language. | Thomas Hunger | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-03-06 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-03-06 | adds incremental for strings; clean-up codes | Tianyi Liang | |
2014-03-06 | adds incremental for strings; clean-up codes | Tianyi Liang | |
2014-03-05 | Merge pull request #14 from kbansal/sets-parserchanges | Kshitij Bansal | |
Sets parserchanges | |||
2014-03-05 | Array smtlib compliance tests | Kshitij Bansal | |
2014-03-05 | Revert "fix naming conflicts in benchmarks" | Kshitij Bansal | |
This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971. | |||
2014-03-05 | Don't tokenize SET_THEORY operators in smt2 parser | Kshitij Bansal | |
2014-03-05 | Improving support for POW in arithmetic. Resolves bug 549. | Tim King | |
2014-03-04 | Guard java-specific swig code with SWIGJAVA. | Thomas Hunger | |
Without this building just the python bindings will fail. Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-03-04 | Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵ | Morgan Deters | |
(resolves bug #548). | |||
2014-03-04 | More useful error message when someone tries mkExpr(VARIABLE). | Morgan Deters | |
2014-02-28 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-02-28 | add re.nostr for the empty regular expression; add re.allchar for the ↵ | Tianyi Liang | |
regular expresssion containing all charactors | |||
2014-02-28 | minor clean-up, bring back derivatives | Tianyi Liang | |
2014-02-28 | a new regular expression engine for solving both positive and negative ↵ | Tianyi Liang | |
membership constraints | |||
2014-02-28 | add re.nostr for the empty regular expression; add re.allchar for the ↵ | Tianyi Liang | |
regular expresssion containing all charactors | |||
2014-02-28 | minor clean-up, bring back derivatives | Tianyi Liang | |
2014-02-28 | a new regular expression engine for solving both positive and negative ↵ | Tianyi Liang | |
membership constraints | |||
2014-02-28 | Merge pull request #12 from kbansal/in-to-member | Kshitij Bansal | |
rename the kind IN to MEMBER | |||
2014-02-28 | theory/sets: cleanup | Kshitij Bansal | |
2014-02-28 | rename kind::IN to kind::MEMBER (fixes some windows build conflicts) | Kshitij Bansal | |
2014-02-27 | Merge pull request #11 from kbansal/improve-stats-every-query | Kshitij Bansal | |
--stats-every-query option: print increment in addition to cumulative va... | |||
2014-02-27 | --stats-every-query option: print increment in addition to cumulative value ↵ | Kshitij Bansal | |
of each stat the increment is printed in parantheses at the end, e.g. sat::decisions, 100 (50) | |||
2014-02-27 | Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the ↵ | Andrew Reynolds | |
default QCF setting. Bug fix to prevent non-ground terms from entering relevant domains. | |||
2014-02-26 | sorry for the missing file | Tianyi Liang | |
2014-02-26 | bug fix (caused by merge), move cardinality option to expert option | Tianyi Liang | |