summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2014-03-11Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.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-10Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-03-10minor change for strings-fmfTianyi 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-08Merge pull request #18 from timothy-king/masterTim King
Merging in the glpk changes
2014-03-08Fixing name changes that cam in from the merge.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback