Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-03-27 | adds new feature: re.loop | Tianyi Liang | |
2014-03-27 | adds intersection | Tianyi Liang | |
2014-03-27 | deriv symbolic regexp | Tianyi Liang | |
2014-03-27 | adds intersection | Tianyi Liang | |
2014-03-26 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: src/theory/arith/normal_form.cpp | |||
2014-03-26 | Win32 build script fixes (to allow portfolio builds). | Morgan Deters | |
2014-03-26 | Fix an off-the-end string pointer bug (showed up only in some Win32 builds). | Morgan Deters | |
2014-03-26 | Merging 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-26 | Fixes an idempotency issue for non-linear multiplication with integer and ↵ | Tim King | |
real variables. | |||
2014-03-20 | Merge pull request #22 from kbansal/sets-model | Kshitij Bansal | |
Sets model | |||
2014-03-20 | cleanup | Kshitij Bansal | |
2014-03-20 | fix 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-20 | Fix for registration issues of term appearing in a shared lemma | Kshitij 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-20 | rewriter fix, weaken an assertion | Kshitij Bansal | |
2014-03-20 | constant normal form and rewrite | Kshitij Bansal | |
2014-03-20 | fix a sharing issues with sets | Kshitij Bansal | |
2014-03-20 | push subtyping for sets to the element type | Kshitij Bansal | |
for eg, (Set Int) is subtype of (Set Real) if Int is subtype of Real | |||
2014-03-20 | enable check-models for sets/ regressions | Kshitij Bansal | |
2014-03-20 | work on set model | Kshitij Bansal | |
2014-03-20 | testlemma regressions | Kshitij Bansal | |
2014-03-20 | Minor fix for CBQI, ignore inst constant nodes. | Andrew Reynolds | |
2014-03-19 | Fix documentation for Theory::preRegisterTerm(). | Morgan Deters | |
2014-03-19 | Refactor 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-19 | Set dumping options from (set-option..) and API more directly. | Morgan Deters | |
2014-03-19 | Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting. | Morgan Deters | |
2014-03-19 | Move the translator binary from src/main to examples, no longer built by ↵ | Morgan Deters | |
default. | |||
2014-03-19 | Appease compilers from latest XCode release (v5.1). | Morgan Deters | |
2014-03-19 | Minor usability fixes related to SMT-LIB compliance. | Morgan Deters | |
2014-03-19 | Fix proof signatures makefile | Morgan Deters | |
2014-03-19 | Minor documentation fixups. | Morgan Deters | |
2014-03-19 | Fix 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-17 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-03-17 | hot fix for pre-reg term caching in strings | Tianyi Liang | |
2014-03-17 | hot fix for pre-reg term caching in strings | Tianyi Liang | |
2014-03-14 | SMT-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-14 | dos2unix on the proof signatures, and fix the makefile. | Morgan Deters | |
2014-03-14 | Add ability to provide theory-specific proof rules to EqualityEngine, ↵ | Andrew Reynolds | |
extends enumeration of MergeReasonType. Add initial use in TheoryArrays. | |||
2014-03-13 | Add working example of LFSC proof with quantifiers. Update quantifiers ↵ | Andrew Reynolds | |
signature to avoid dependent types in side condition. | |||
2014-03-12 | Work 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-12 | Minor fixes post-merge of RR. | Andrew Reynolds | |
2014-03-12 | Fix LogicInfo unit test. | Morgan Deters | |
2014-03-12 | Some standardization of regression Makefiles that got out of sync. Fixes ↵ | Morgan Deters | |
cases of nonterminating rewrite-rules regressions. | |||
2014-03-12 | Draft contrib/get-abc script for bitvectors libabc support. | Morgan Deters | |
2014-03-11 | Merge branch '1.3.x' | Morgan Deters | |
2014-03-11 | Fix for rewriterules build breakage. | Morgan Deters | |
2014-03-11 | Fix for random-seed option. | Morgan Deters | |
2014-03-11 | Fix for portfolio. | Morgan Deters | |
2014-03-11 | Minor cleanup. | Morgan Deters | |
* Reenable parts of bvsimple test * Fix typo in #endif comment | |||
2014-03-11 | Fix for (get-assignment), resolves bug 553. | Morgan Deters | |
2014-03-11 | Merge branch '1.3.x' | Morgan Deters | |