| 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-09 | Disallow copy/assignment of SmtEngine. | Morgan Deters | |
| 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-28 | Add option to avoid dumping partial models/proofs. | Andrew Reynolds | |
| 2014-05-27 | Some fixes to GC order in Java. | Morgan Deters | |
| 2014-05-26 | Separating an implicit inclusion of smt_engine.h from theory.h. | Tim King | |
| 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-14 | Add initial support for co-datatypes. | Andrew Reynolds | |
| 2014-04-10 | Fix the build; --check-proof works for UF but not for the new UFC logic. | Morgan Deters | |
| 2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for ↵ | Andrew Reynolds | |
| incorrectly applied selector terms. | |||
| 2014-04-10 | Boolean terms conversion fix for datatypes, fixes a problem Andy discovered ↵ | Morgan Deters | |
| on his branch. | |||
| 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-04 | For security, add --no-filesystem-access option, which disables SMT-LIB ↵ | Morgan Deters | |
| script access to filesystem. | |||
| 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-20 | Merge pull request #22 from kbansal/sets-model | Kshitij Bansal | |
| Sets model | |||
| 2014-03-20 | cleanup | Kshitij Bansal | |
| 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-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-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-03-04 | Guard java-specific swig code with SWIGJAVA. | Thomas Hunger | |
| Without this building just the python bindings will fail. Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
| 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 | |
 |
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