| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-06-10 | Merging CAV14 paper bit-vector work. | lianah | |
| 2014-06-08 | test for prvs commit (tokenize emptyset) | Kshitij Bansal | |
| 9978c259f30b1f4b2c70c04589a309033a6eb1f6 | |||
| 2014-06-06 | Merge pull request #28 from kbansal/sets | Kshitij Bansal | |
| Sets translator, bug fixes | |||
| 2014-06-06 | Patch for the subtype theoryof mode to make the equalities over disequal ↵ | Tim King | |
| types get sent to the theory of the type. Adding a new test case for bug 569. Fixes to the normal form of arithmetic so that real terms are before integer terms. | |||
| 2014-06-06 | sets: fix equality propagation | Kshitij Bansal | |
| 2014-05-30 | Update submission make rules. | Morgan Deters | |
| 2014-05-27 | update stats_black | Kshitij Bansal | |
| 2014-05-25 | Improve quantifier instantiation: always use original terms when matching ↵ | Andrew Reynolds | |
| (was missing for simple triggers). Minor updates to scripts. | |||
| 2014-05-23 | Fix bug in E-matching Real/Int terms. | Andrew Reynolds | |
| 2014-05-16 | sets: fix a bug in model building, another in handling set of sets | Kshitij Bansal | |
| 2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ↵ | ajreynol | |
| Add regressions. | |||
| 2014-05-12 | Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report. | Tianyi Liang | |
| 2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, ↵ | Andrew Reynolds | |
| minor changes. | |||
| 2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King | |
| This commit includes work from the past month on the T-entailment check infrastructure (due to Tim), an entailment check for arithmetic (also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds). Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
| 2014-04-29 | fix was compiler warning in antlr_input, crashing test case with the old fix | Kshitij Bansal | |
| 2014-04-29 | add leading zeros support for str.to.int | Tianyi Liang | |
| 2014-04-28 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal | |
| 2014-04-28 | travis, please! | Kshitij Bansal | |
| 2014-04-27 | attempt to improve CVC4's "parse error" message | Kshitij Bansal | |
| 2014-04-14 | Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ↵ | Andrew Reynolds | |
| Improve datatypes rewrite, make option for previous dt semantics. | |||
| 2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for ↵ | Andrew Reynolds | |
| incorrectly applied selector terms. | |||
| 2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵ | Andrew Reynolds | |
| Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit. | |||
| 2014-04-09 | add tests | Kshitij Bansal | |
| 2014-04-09 | inputs to trigger bug | Kshitij Bansal | |
| 2014-04-06 | Reduced example from pcc's bug report. | Tim King | |
| 2014-04-06 | Merge pull request #21 from pcc/ite-fix | Tim King | |
| Fix for ite of >=64bit wide bitvectors with unconstrained condition. | |||
| 2014-04-03 | Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis ↵ | Morgan Deters | |
| Deligiannis and Jeroen Ketema for discovering this issue. | |||
| 2014-04-01 | Merge branch '1.3.x' | Tim King | |
| 2014-04-01 | Fixing bug 552. There was a bug when integers are made using a string with ↵1.3.x | Tim King | |
| a lot of leading 0s on old versions of CLN. | |||
| 2014-03-31 | add str to u16/u32, and u16/u32 to str | Tianyi Liang | |
| 2014-03-28 | add construles, type_rules rm redundant, kinds cleanup | Kshitij Bansal | |
| 2014-03-27 | adds new feature: re.loop | Tianyi Liang | |
| 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 | fix a sharing issues with sets | Kshitij Bansal | |
| 2014-03-20 | enable check-models for sets/ regressions | Kshitij Bansal | |
| 2014-03-20 | testlemma regressions | Kshitij Bansal | |
| 2014-03-19 | Minor usability fixes related to SMT-LIB compliance. | Morgan Deters | |
| 2014-03-16 | Fix for ite of >=64bit wide bitvectors with unconstrained condition. | Peter Collingbourne | |
| 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 | 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-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 | 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-08 | Merge remote-tracking branch 'CVC4root/master' | Tim King | |
| 2014-03-07 | Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵ | Morgan Deters | |
| bodies; fix bug 551, improper ITE removal under quantifiers. | |||
| 2014-03-07 | Fix run_regression on Mac. | Morgan Deters | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback