summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-03-11Fix for (get-assignment), resolves bug 553.Morgan Deters
2014-03-11Merge branch '1.3.x'Morgan Deters
2014-03-11Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.Morgan Deters
2014-03-11Initial 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-10adds intro vars length cacheTianyi Liang
2014-03-10Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-03-10minor change for strings-fmfTianyi Liang
2014-03-10minor change for strings-fmfTianyi Liang
2014-03-08Re-fix bug 551 by adding a check to the arith ITE simplifier to ignore ↵Morgan Deters
non-ground ITEs also.
2014-03-08Merge pull request #18 from timothy-king/masterTim King
Merging in the glpk changes
2014-03-08Fixing name changes that cam in from the merge.Tim King
2014-03-08Merge remote-tracking branch 'CVC4root/master'Tim King
2014-03-07Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵Morgan Deters
bodies; fix bug 551, improper ITE removal under quantifiers.
2014-03-07Fix run_regression on Mac.Morgan Deters
2014-03-07Fix bug 554 (nominally).Morgan Deters
2014-03-07Fixing a SWIG problem for RationalFromDoubleException.Tim King
2014-03-07Merging 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-07Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-03-07remove unrolling depthTianyi Liang
2014-03-07bring back D-NormTianyi Liang
2014-03-07Fix strings-exp setting.Morgan Deters
2014-03-07remove unrolling depthTianyi Liang
2014-03-07bring back D-NormTianyi Liang
2014-03-07Fix strings-exp setting.Morgan Deters
2014-03-07Add swig renames for new Z3STR language.Thomas Hunger
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-03-06Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-03-06adds incremental for strings; clean-up codesTianyi Liang
2014-03-06adds incremental for strings; clean-up codesTianyi Liang
2014-03-05Merge pull request #14 from kbansal/sets-parserchangesKshitij Bansal
Sets parserchanges
2014-03-05Array smtlib compliance testsKshitij Bansal
2014-03-05Revert "fix naming conflicts in benchmarks"Kshitij Bansal
This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
2014-03-05Don't tokenize SET_THEORY operators in smt2 parserKshitij Bansal
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2014-03-04Guard 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-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵Morgan Deters
(resolves bug #548).
2014-03-04More useful error message when someone tries mkExpr(VARIABLE).Morgan Deters
2014-02-28Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-28add re.nostr for the empty regular expression; add re.allchar for the ↵Tianyi Liang
regular expresssion containing all charactors
2014-02-28minor clean-up, bring back derivativesTianyi Liang
2014-02-28a new regular expression engine for solving both positive and negative ↵Tianyi Liang
membership constraints
2014-02-28add re.nostr for the empty regular expression; add re.allchar for the ↵Tianyi Liang
regular expresssion containing all charactors
2014-02-28minor clean-up, bring back derivativesTianyi Liang
2014-02-28a new regular expression engine for solving both positive and negative ↵Tianyi Liang
membership constraints
2014-02-28Merge pull request #12 from kbansal/in-to-memberKshitij Bansal
rename the kind IN to MEMBER
2014-02-28theory/sets: cleanupKshitij Bansal
2014-02-28rename kind::IN to kind::MEMBER (fixes some windows build conflicts)Kshitij Bansal
2014-02-27Merge pull request #11 from kbansal/improve-stats-every-queryKshitij 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-27Bug 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-26sorry for the missing fileTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback