| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-04-24 | Dco fix (#2973) | Clark Barrett | |
| 2019-04-24 | README: Remove project leaders, history. | Aina Niemetz | |
| 2019-04-24 | CONTRIBUTING: Fix project leaders link. | Aina Niemetz | |
| 2019-04-23 | [BV] An option for SAT proof optimization (#2915) | Alex Ozdemir | |
| * [BV] An option for SAT proof optimization The option doesn't **do** anything yet, but exists. * CopyPaste Fix: BvOptimizeSatProof documentation It was the documentation for a different option. Now it has been updated. * Fix Typos per Mathias' review. Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu> | |||
| 2019-04-23 | Refactor normal forms in strings (#2897) | Andrew Reynolds | |
| 2019-04-22 | Add CONTRIBUTING file. (#2968) | Aina Niemetz | |
| 2019-04-18 | Fail fast strategy for propagating instances (#2939) | Andrew Reynolds | |
| 2019-04-18 | Less aggressive caching in equality engine when proofs are enabled (#2964) | Andrew Reynolds | |
| 2019-04-17 | Cache explanations in the equality engine (#2937) | Andrew Reynolds | |
| 2019-04-17 | More use of isClosure (#2959) | Andrew Reynolds | |
| 2019-04-17 | Fix extended function decomposition (#2960) | Andrew Reynolds | |
| Fixes #2958. The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with. The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering. | |||
| 2019-04-16 | Add interface for term enumeration (#2956) | Andrew Reynolds | |
| 2019-04-16 | Make bv{add,mul,and,or,xor,xnor} left-associative (#2955) | Andres Noetzli | |
| The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor} [0, 1] as left-associative. CVC4 treats all but bvxnor as having variable arity anyway but the arity check was too strict when using `--strict-parsing`. This commit changes the strict parsing check. For bvxnor, it adds code to the parser that expands an application of bvxnor into multiple applications of a binary bvxnor if needed. References: [0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand, bvor, bvadd, bvmul) [1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor) | |||
| 2019-04-16 | Stratify enumerative instantiation (#2954) | Andrew Reynolds | |
| 2019-04-16 | Minor simplifications to theory quantifiers (#2953) | Andrew Reynolds | |
| 2019-04-15 | Check for rt library in configuration -- support for glibc<2.17 (#2854) | makaimann | |
| This is a minor fix for systems with glibc version < 2.17. In that case, we need to link with `-lrt` according to the clock_gettime man page. | |||
| 2019-04-15 | Initial version of run scripts for SMT-COMP 2019 (#2951) | Andres Noetzli | |
| For now, they are just copies of the 2018 version of the scripts. | |||
| 2019-04-12 | Referring to prerelease 1.8 (#2943) | Haniel Barbosa | |
| 2019-04-11 | Eliminate Boolean ITE within terms, fixes 2947 (#2949) | Andrew Reynolds | |
| 2019-04-09 | Removing references to cvc4-bugs@... (#2945) | Haniel Barbosa | |
| 2019-04-08 | "prerelease -> release" in INSTALL (#2944) | Haniel Barbosa | |
| 2019-04-08 | Fix email address of the bugs email list and delete obsolete RELEASE-NOTES. | Aina Niemetz | |
| 2019-04-08 | fix copyright year in configuration file (#2942) | Haniel Barbosa | |
| 2019-04-05 | prerelease -> release (#2941) | Haniel Barbosa | |
| 2019-04-05 | Fix another corner case of datatypes+PBE (#2938) | Andrew Reynolds | |
| 2019-04-05 | fix fp issue (#2940) | Haniel Barbosa | |
| 2019-04-05 | SatClauseSetHashFunction (#2916) | Alex Ozdemir | |
| * SatClauseHashFunction Added to the same file as SatLiteralHashFunction. * clang-format Thanks Andres! | |||
| 2019-04-04 | adding sygus news (#2934) | Haniel Barbosa | |
| 2019-04-04 | Ignoring FP benchmarks with "unsafe" sizes unless option (#2931) | Haniel Barbosa | |
| 2019-04-03 | Update release notes and lib version (#2933) | Haniel Barbosa | |
| 2019-04-03 | Update copyright headers. | Aina Niemetz | |
| 2019-04-03 | get-authors: Add GitHub user ayveejay -> Andrew V. Jones. | Aina Niemetz | |
| 2019-04-03 | Fix combination of datatypes + strings in PBE (#2930) | Andrew Reynolds | |
| 2019-04-01 | FP: Fix wrong model due to partial assignment (#2910) | Andres Noetzli | |
| For a simple query `(not (= (fp.isSubnormal x) false))`, we were getting a wrong model. The issue was that `(sign x)` was not assigned a value and did not appear in the shared terms. In `TheoryFp::collectModelInfo()`, however, we generate an expression that connects the components of `x` to `x`, which contains `(sign x)`. As a result, the normalization while building a model did not result in a constant. This commit fixes the issue by marking `(sign x)` (and `(significand x)`) as assignable. Assignable terms can take any value while building a model if there is no existing value. | |||
| 2019-04-01 | Fix RewriteITEBv to ensure rewrite to fixpoint (#2878) | Andres Noetzli | |
| `TheoryBVRewriter::RewriteITEBv()` is currently always returning the status `REWRITE_DONE`. This can result in a situation where a rewritten node can be rewritten again (which breaks the contract of our rewriter). The unit test in this commit illustrates the issue. The commit fixes the issue by returning `REWRITE_AGAIN` or `REWRITE_AGAIN_FULL` if a node changed. `REWRITE_AGAIN_FULL` is needed if the resulting node may have a child that is not a subterm of the original expression. | |||
| 2019-04-01 | Update includes to use cvc4 top-level directory in examples (#2877) | makaimann | |
| Because the headers are now installed in a `cvc4` directory, the examples need to include from there as well. | |||
| 2019-04-01 | Move slow string regression to regress3 (#2913) | Andres Noetzli | |
| 2019-04-01 | Modify strategy in sets+cardinality (#2909) | Andrew Reynolds | |
| 2019-03-29 | Apply empty splits more aggressively in sets+cardinality (#2907) | Andrew Reynolds | |
| 2019-03-29 | removing deprecated rewriting signature / example (#2906) | Haniel Barbosa | |
| 2019-03-28 | Fix freeing nodes with maxed refcounts (#2903) | Andres Noetzli | |
| 2019-03-28 | Fix issues in cvc parser (#2901) | Andrew Reynolds | |
| 2019-03-28 | fix ex_bv.plf (#2905) | Haniel Barbosa | |
| 2019-03-26 | Update copyright headers. | Aina Niemetz | |
| 2019-03-26 | update-copyright: Update to 2019. | Aina Niemetz | |
| 2019-03-26 | get-authors: Exclude empty lines. | Mathias Preiner | |
| 2019-03-26 | Fix warnings about wrong line numbers (#2899) | Andres Noetzli | |
| 2019-03-26 | Fix a few warnings (#2898) | Andrew Reynolds | |
| 2019-03-25 | get-authors: Exclude common source code patterns. (#2900) | Mathias Preiner | |
| Exclude lines that #include header files and define namespaces. Since we use git blame -C -M to determine the current top contributors, git tries to match all #include and namespace definitions to an original author, which is not accurate since these lines are usually not copied over from other files. | |||
| 2019-03-25 | update-copyright: Fix matching of excluded paths. | Aina Niemetz | |
 |
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