Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |
2014-03-11 | Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok. | 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 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-03-10 | minor change for strings-fmf | 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 | Merge pull request #18 from timothy-king/master | Tim King | |
Merging in the glpk changes | |||
2014-03-08 | Fixing name changes that cam in from the merge. | Tim King | |