Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-03-12 | Minor fixes post-merge of RR. | Andrew Reynolds | |
2014-03-11 | Fix for rewriterules build breakage. | 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 | 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 | 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 | 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 | remove unrolling depth | Tianyi Liang | |
2014-03-07 | bring back D-Norm | Tianyi Liang | |
2014-03-06 | adds incremental for strings; clean-up codes | Tianyi Liang | |
2014-03-05 | Improving support for POW in arithmetic. Resolves bug 549. | Tim King | |
2014-03-04 | Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵ | Morgan Deters | |
(resolves bug #548). | |||
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 | theory/sets: cleanup | Kshitij Bansal | |
2014-02-28 | rename kind::IN to kind::MEMBER (fixes some windows build conflicts) | Kshitij Bansal | |
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 | bug fix (caused by merge), move cardinality option to expert option | Tianyi Liang | |
2014-02-26 | for merging | Tianyi Liang | |
2014-02-25 | Add options --full-saturate-quant and --mbqi=trust. Other minor changes. | Andrew Reynolds | |
2014-02-24 | bug fix: strings preprocess for the orignal term, causing unknown in some cases | Tianyi Liang | |
2014-02-21 | Merge branch '1.3.x' | Morgan Deters | |
2014-02-21 | No diamond-breaking under quantifiers (resolves bug #550). | Morgan Deters | |
2014-02-21 | reorganize substr, fix some potential bugs, adds cache for preprocessing | Tianyi Liang | |
2014-02-21 | disable test cvc3_main, attempt to fix dist_check | Kshitij Bansal | |
2014-02-21 | add new theory (sets) | Kshitij Bansal | |
Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment | |||
2014-02-21 | fix a -Wunused | Kshitij Bansal | |
2014-02-20 | add more tests, and define int.to.str(NEGATIVE)="" | Tianyi Liang | |
2014-02-20 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: src/theory/strings/theory_strings_preprocess.cpp | |||
2014-02-20 | hot fix for str2int/int2str | Tianyi Liang | |
2014-02-20 | add negative int2str | Tianyi Liang | |
2014-02-20 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: src/theory/strings/theory_strings_preprocess.cpp | |||
2014-02-20 | hot fix for str2int/int2str | Tianyi Liang | |
2014-02-20 | add negative int2str | Tianyi Liang | |
2014-02-20 | Fix ite and iff handling in QCF. Add option for heuristic instantiation in ↵ | Andrew Reynolds | |
QCF (not working yet). Improve automatic option setting for quantifiers. | |||
2014-02-19 | Merge branch 'master' of github.com:CVC4/CVC4 | Tim King | |
2014-02-19 | Merge branch '1.3.x' | Tim King | |
2014-02-19 | Stopping non-linear terms from entering the dio solver. Fixes bug 547. | Tim King | |
2014-02-19 | add negative int2str | Tianyi Liang | |
2014-02-18 | missed files for the latter commit | Tianyi Liang | |
2014-02-18 | str.to.int(INVALID) = -1 | Tianyi Liang | |
2014-02-18 | switch to total function str.to.int: maps invalid and non-digit strings to 0 | Tianyi Liang | |
2014-02-17 | bring back the commits which is lost accidentally. | Tianyi Liang | |
2014-02-17 | add str2int | Tianyi Liang | |
2014-02-17 | Fix strings preprocessing for justification heuristic | Morgan Deters | |
2014-02-17 | type conversion | Tianyi Liang | |