summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2014-03-12Minor fixes post-merge of RR.Andrew Reynolds
2014-03-11Fix for rewriterules build breakage.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-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-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-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-07remove unrolling depthTianyi Liang
2014-03-07bring back D-NormTianyi Liang
2014-03-06adds incremental for strings; clean-up codesTianyi Liang
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵Morgan Deters
(resolves bug #548).
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-28theory/sets: cleanupKshitij Bansal
2014-02-28rename kind::IN to kind::MEMBER (fixes some windows build conflicts)Kshitij Bansal
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-26bug fix (caused by merge), move cardinality option to expert optionTianyi Liang
2014-02-26for mergingTianyi Liang
2014-02-25Add options --full-saturate-quant and --mbqi=trust. Other minor changes.Andrew Reynolds
2014-02-24bug fix: strings preprocess for the orignal term, causing unknown in some casesTianyi Liang
2014-02-21Merge branch '1.3.x'Morgan Deters
2014-02-21No diamond-breaking under quantifiers (resolves bug #550).Morgan Deters
2014-02-21reorganize substr, fix some potential bugs, adds cache for preprocessingTianyi Liang
2014-02-21disable test cvc3_main, attempt to fix dist_checkKshitij Bansal
2014-02-21add 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-21fix a -WunusedKshitij Bansal
2014-02-20add more tests, and define int.to.str(NEGATIVE)=""Tianyi Liang
2014-02-20Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: src/theory/strings/theory_strings_preprocess.cpp
2014-02-20hot fix for str2int/int2strTianyi Liang
2014-02-20add negative int2strTianyi Liang
2014-02-20Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: src/theory/strings/theory_strings_preprocess.cpp
2014-02-20hot fix for str2int/int2strTianyi Liang
2014-02-20add negative int2strTianyi Liang
2014-02-20Fix 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-19Merge branch 'master' of github.com:CVC4/CVC4Tim King
2014-02-19Merge branch '1.3.x'Tim King
2014-02-19Stopping non-linear terms from entering the dio solver. Fixes bug 547.Tim King
2014-02-19add negative int2strTianyi Liang
2014-02-18missed files for the latter commitTianyi Liang
2014-02-18str.to.int(INVALID) = -1Tianyi Liang
2014-02-18switch to total function str.to.int: maps invalid and non-digit strings to 0Tianyi Liang
2014-02-17bring back the commits which is lost accidentally.Tianyi Liang
2014-02-17add str2intTianyi Liang
2014-02-17Fix strings preprocessing for justification heuristicMorgan Deters
2014-02-17type conversionTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback