summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-03-27adds new feature: re.loopTianyi Liang
2014-03-27adds intersectionTianyi Liang
2014-03-27deriv symbolic regexpTianyi Liang
2014-03-27adds intersectionTianyi Liang
2014-03-26Merge branch '1.3.x'Morgan Deters
Conflicts: src/theory/arith/normal_form.cpp
2014-03-26Win32 build script fixes (to allow portfolio builds).Morgan Deters
2014-03-26Fix an off-the-end string pointer bug (showed up only in some Win32 builds).Morgan Deters
2014-03-26Merging in a fix from 1.3.x.Tim King
Fixes an idempotency issue for non-linear multiplication with integer and real variables. Conflicts: src/theory/arith/normal_form.cpp
2014-03-26Fixes an idempotency issue for non-linear multiplication with integer and ↵Tim King
real variables.
2014-03-20Merge pull request #22 from kbansal/sets-modelKshitij Bansal
Sets model
2014-03-20cleanupKshitij Bansal
2014-03-20fix for sets/mar2014/..317minimized..Kshitij Bansal
Observed behavior: --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) with different set of elements in the model for representative and the node itself. Issue: The trouble with data structure being mainted to ensure that things for which lemmas have been generated are not generated again. This data structure (d_pendingEverInserted) needs to be user context dependent. The bug was in the sequence of steps from requesting that a lemma be generated to when it actually was. Sequence was: addToPending (and also adds to pending ever inserted) -> isComplete (might remove things from pending if requirment met in other ways) -> getLemma (actually generated the lemma, if requirement not already met) Resolution: adding terms to d_pendingEverInserted was moved from addToPending() to getLemma().
2014-03-20Fix for registration issues of term appearing in a shared lemmaKshitij Bansal
(brought to attention by lianah -- fix currently just adapted using arrays -- this is to remind me to raise why do we even have this isPreregistered bussiness)
2014-03-20rewriter fix, weaken an assertionKshitij Bansal
2014-03-20constant normal form and rewriteKshitij Bansal
2014-03-20fix a sharing issues with setsKshitij Bansal
2014-03-20push subtyping for sets to the element typeKshitij Bansal
for eg, (Set Int) is subtype of (Set Real) if Int is subtype of Real
2014-03-20enable check-models for sets/ regressionsKshitij Bansal
2014-03-20work on set modelKshitij Bansal
2014-03-20testlemma regressionsKshitij Bansal
2014-03-20Minor fix for CBQI, ignore inst constant nodes.Andrew Reynolds
2014-03-19Fix documentation for Theory::preRegisterTerm().Morgan Deters
2014-03-19Refactor the theory specific parts of definition expansion into the theory ↵Martin Brain
solvers. In the process of doing this I may have fixed some bugs or some potential bugs so there may be some user visible results of this refactoring. Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-03-19Set dumping options from (set-option..) and API more directly.Morgan Deters
2014-03-19Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.Morgan Deters
2014-03-19Move the translator binary from src/main to examples, no longer built by ↵Morgan Deters
default.
2014-03-19Appease compilers from latest XCode release (v5.1).Morgan Deters
2014-03-19Minor usability fixes related to SMT-LIB compliance.Morgan Deters
2014-03-19Fix proof signatures makefileMorgan Deters
2014-03-19Minor documentation fixups.Morgan Deters
2014-03-19Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan ↵Andrew Reynolds
(problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory. Add example test proof.
2014-03-17Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-03-17hot fix for pre-reg term caching in stringsTianyi Liang
2014-03-17hot fix for pre-reg term caching in stringsTianyi Liang
2014-03-14SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). ↵Morgan Deters
Thanks to David Cok for the bug report.
2014-03-14dos2unix on the proof signatures, and fix the makefile.Morgan Deters
2014-03-14Add ability to provide theory-specific proof rules to EqualityEngine, ↵Andrew Reynolds
extends enumeration of MergeReasonType. Add initial use in TheoryArrays.
2014-03-13Add working example of LFSC proof with quantifiers. Update quantifiers ↵Andrew Reynolds
signature to avoid dependent types in side condition.
2014-03-12Work on array pf signature, add working example. Add quantifiers proof ↵Andrew Reynolds
signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
2014-03-12Minor fixes post-merge of RR.Andrew Reynolds
2014-03-12Fix LogicInfo unit test.Morgan Deters
2014-03-12Some standardization of regression Makefiles that got out of sync. Fixes ↵Morgan Deters
cases of nonterminating rewrite-rules regressions.
2014-03-12Draft contrib/get-abc script for bitvectors libabc support.Morgan Deters
2014-03-11Merge branch '1.3.x'Morgan Deters
2014-03-11Fix for rewriterules build breakage.Morgan Deters
2014-03-11Fix for random-seed option.Morgan Deters
2014-03-11Fix for portfolio.Morgan Deters
2014-03-11Minor cleanup.Morgan Deters
* Reenable parts of bvsimple test * Fix typo in #endif comment
2014-03-11Fix for (get-assignment), resolves bug 553.Morgan Deters
2014-03-11Merge branch '1.3.x'Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback