| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-06-23 | Fatal error if --unconstrained-simp and --produce-models used together ↵ | Morgan Deters | |
| (before it would just override the user and turn off models). | |||
| 2014-06-19 | added model generation to eager bit-blasting and turned abc off by default | lianah | |
| 2014-06-19 | New translator features: expand define-funs and combine assertions. | Morgan Deters | |
| 2014-06-19 | Fix for new CASC features, fixes Java builds. | Morgan Deters | |
| 2014-06-19 | For casc : print models of functions rewritten by sort inference. | ajreynol | |
| 2014-06-14 | Evil bitvector preprocessing pass for simplifying powers of two. | lianah | |
| 2014-06-13 | Fix handling of ALIA. | ajreynol | |
| 2014-06-11 | Some clean-up, post bv-merge. | Morgan Deters | |
| Add abc to build id and fix static building. Add abc to --show-config output and Configuration class API. Add ability to select abc source path. Fix arch_flags for abc. | |||
| 2014-06-10 | Merging Tim's pseudoboolean work from his fmcad14 branch. | Tim King | |
| Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
| 2014-06-10 | Merging CAV14 paper bit-vector work. | lianah | |
| 2014-06-06 | Sets translate, and other short fixes | Kshitij Bansal | |
| - $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine | |||
| 2014-06-04 | SmtEngine::checkModel() now checks that model values are of the correct type ↵ | Morgan Deters | |
| (related to bug #569). | |||
| 2014-05-15 | Minor fixes. Add SMTCOMP 2014 script. | Andrew Reynolds | |
| 2014-05-14 | Finish --dump-instantiations option. Update scripts. | Andrew Reynolds | |
| 2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ↵ | ajreynol | |
| Add regressions. | |||
| 2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ↵ | Andrew Reynolds | |
| assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real. | |||
| 2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, ↵ | Andrew Reynolds | |
| minor changes. | |||
| 2014-05-09 | Add variable ordering to ambqi. Bug fix to macros. More preparation for ↵ | Andrew Reynolds | |
| CASC proofs. | |||
| 2014-05-02 | Add option --dt-stc-ind for strengthening skolemization. Refactor ↵ | Andrew Reynolds | |
| skolemization. | |||
| 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-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 | fix get-info error-behavior | Kshitij Bansal | |
| 2014-04-03 | Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis ↵ | Morgan Deters | |
| Deligiannis and Jeroen Ketema for discovering this issue. | |||
| 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-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-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 bug 554 (nominally). | Morgan Deters | |
| 2014-03-07 | Fix strings-exp setting. | Morgan Deters | |
| 2014-02-28 | a new regular expression engine for solving both positive and negative ↵ | Tianyi Liang | |
| membership constraints | |||
| 2014-02-21 | portfolio: fix export of emptyset | Kshitij Bansal | |
| 2014-02-20 | Fix ite and iff handling in QCF. Add option for heuristic instantiation in ↵ | Andrew Reynolds | |
| QCF (not working yet). Improve automatic option setting for quantifiers. | |||
| 2014-02-18 | switch to total function str.to.int: maps invalid and non-digit strings to 0 | Tianyi Liang | |
| 2014-02-17 | bring back the commits which is lost accidentally. | Tianyi Liang | |
| 2014-02-17 | add str2int | Tianyi Liang | |
| 2014-02-17 | Fix for strings-exp: enable quantifiers | Morgan Deters | |
| 2014-02-17 | Fix strings preprocessing for justification heuristic | Morgan Deters | |
| 2014-02-17 | type conversion | Tianyi Liang | |
| 2014-02-13 | fix expanding def | Tianyi Liang | |
| 2014-01-28 | merge internal and user of charat & substr into one | Tianyi Liang | |
| 2014-01-22 | Some minor fixes to SmtEngine strings settings. | Morgan Deters | |
| 2014-01-22 | add warning for using strings in ALL_SUPPORTED | Tianyi Liang | |
| 2014-01-22 | Smarter options, but still have a bug | Tianyi Liang | |
| 2014-01-18 | strings with new ideas | Tianyi Liang | |
| 2014-01-16 | adds partial functions | Tianyi Liang | |
| 2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified ↵ | Andrew Reynolds | |
| formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup. | |||
| 2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for ↵ | Andrew Reynolds | |
| inst gen-style MBQI. | |||
| 2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing ↵ | Andrew Reynolds | |
| proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup. | |||
| 2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters | |
| 2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
| generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line | |||
 |
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