| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2013-06-04 | File inclusion in Smt2 parser. | Morgan Deters | |
| The extended command (include-file "filename") now includes file content. | |||
| 2013-06-04 | Add --no-condense-function-values option for explicit function models ↵ | Morgan Deters | |
| (useful in some applications) | |||
| 2013-06-04 | Merge branch '1.2.x' | Morgan Deters | |
| 2013-06-04 | Fix clang static initialization order issue; fixes bug 512. | Morgan Deters | |
| 2013-06-04 | Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ↵ | Andrew Reynolds | |
| bounds for bounded integers. | |||
| 2013-05-29 | Merge branch '1.2.x' | Morgan Deters | |
| 2013-05-29 | Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with ↵ | Morgan Deters | |
| unknown key. | |||
| 2013-05-29 | SMT-LIB printer updates (some missing cases). | Morgan Deters | |
| 2013-05-29 | Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real ↵ | Morgan Deters | |
| division | |||
| 2013-05-28 | Standardize SMT-LIBv2 set of logics to use LogicInfo. | Morgan Deters | |
| Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2. This led to inconsistencies---such as nonstandard logics like "QF_LIRA" being accepted in set-logic but not providing the "Real" sort. Now, the LogicInfo is used and queried, so nonstandard logics should work fine and declare the correct symbols. SMT-LIB v1.2, unfortunately, can't take advantage of this fully since symbols like "Array" have substantially different meanings in different logics. | |||
| 2013-05-23 | Refactoring to prepare for MBQI with integer quantification. Minor bug fixes. | Andrew Reynolds | |
| 2013-05-22 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Andrew Reynolds | |
| Conflicts: src/theory/arith/theory_arith_private.cpp src/theory/quantifiers_engine.cpp | |||
| 2013-05-22 | Significant work on bounded integer quantification to handle non-trivial ↵ | Andrew Reynolds | |
| bounds. Refactoring of InstConstantAttribute to be internal to TermDb. | |||
| 2013-05-22 | Add regressions for finite model finding | Andrew Reynolds | |
| 2013-05-21 | Merge branch '1.2.x' | Morgan Deters | |
| 2013-05-21 | Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵ | Morgan Deters | |
| to improper ITE removal in quantifier instantiations. | |||
| 2013-05-21 | Fix an error that valgrind found. | Morgan Deters | |
| 2013-05-21 | Merge branch '1.2.x' | Morgan Deters | |
| 2013-05-21 | Fix incremental bug in symmetry breaker. | Morgan Deters | |
| Thanks to Christoph Sticksel for reporting this. | |||
| 2013-05-20 | Merge branch '1.2.x' | Morgan Deters | |
| Conflicts: library_versions src/parser/parser.h | |||
| 2013-05-20 | Fix error reporting on use of (nonlinear) div,mod,/ symbols | Morgan Deters | |
| 2013-05-20 | Detect multiply-defined :named annotations and issue an error. | Morgan Deters | |
| Thanks to David Cok for pointing out this issue. Conflicts: library_versions | |||
| 2013-05-20 | Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive ↵ | Morgan Deters | |
| mode. Thanks to David Cok for raising this issue. | |||
| 2013-05-20 | Compliance fixes for :named annotations: they must name closed subterms, the ↵ | Morgan Deters | |
| names must be user-permitted names, etc. Thanks to David Cok for raising this issue. | |||
| 2013-05-20 | Don't allow get-model & co after a user push/pop | Morgan Deters | |
| This makes us more strictly adhere to the spec, but it's useful anyway: previously we would support a get-model until the problem was explicitly changed with e.g. a new assertion. That meant you could check-sat, then pop, then get-model, but you'd only get the part of the model still in scope. This is strange, and would likely lead to problems, so it's now disabled. Thanks to David Cok for inquiring about this. | |||
| 2013-05-20 | As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => ↵ | Morgan Deters | |
| takes n>2 args and is right-assoc. Thanks to David Cok for pointing out this issue. | |||
| 2013-05-20 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters | |
| Thanks to David Cok for reporting this. | |||
| 2013-05-20 | Fix destruction issue in GetValueCommand leading to crash. | Morgan Deters | |
| Thanks to David Cok for reporting this. | |||
| 2013-05-20 | Better error on invalid logic strings. | Morgan Deters | |
| Thanks to David Cok for reporting this issue. Conflicts: library_versions | |||
| 2013-05-20 | Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵ | Morgan Deters | |
| in some places Thanks to David Cok for reporting these issues. | |||
| 2013-05-20 | A couple of fixes to the get-option command for compliance with SMT-LIB. | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-20 | Disallow construction of (_ BitVec 0). | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-20 | Fixed "success" response to (push N) / (pop N) with N > 1. | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-20 | Fix to empty response to (get-assignment). | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-20 | configure fix for building with glpk on redhat, perhaps others | Morgan Deters | |
| 2013-05-20 | minor changes to language bindings | Morgan Deters | |
| 2013-05-20 | disable Logic-checking with finite model finding for now, since FMF uses ↵ | Morgan Deters | |
| Rationals, making the check think arithmetic should be enabled (but it's not) | |||
| 2013-05-20 | Fix erroneous results when the logic was incorrectly specified (by throwing ↵ | Morgan Deters | |
| LogicException). Also correct a case where sharing was doing some work during pure theory solving. | |||
| 2013-05-17 | Add support for --dump-models option, in preparation for casc. | Andrew Reynolds | |
| 2013-05-17 | As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => ↵ | Morgan Deters | |
| takes n>2 args and is right-assoc. Thanks to David Cok for pointing out this issue. | |||
| 2013-05-17 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters | |
| Thanks to David Cok for reporting this. | |||
| 2013-05-17 | Fix destruction issue in GetValueCommand leading to crash. | Morgan Deters | |
| Thanks to David Cok for reporting this. | |||
| 2013-05-17 | Better error on invalid logic strings. | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-17 | Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵ | Morgan Deters | |
| in some places Thanks to David Cok for reporting these issues. | |||
| 2013-05-17 | A couple of fixes to the get-option command for compliance with SMT-LIB. | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-17 | Disallow construction of (_ BitVec 0). | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-17 | Fixed "success" response to (push N) / (pop N) with N > 1. | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-17 | Fix to empty response to (get-assignment). | Morgan Deters | |
| Thanks to David Cok for reporting this issue. | |||
| 2013-05-16 | configure fix for building with glpk on redhat, perhaps others | Morgan Deters | |
| 2013-05-16 | Fix minor bug in full_model_check.cpp | Andrew Reynolds | |
 |
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