summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-01mergecav2019strings_countRewRedAndres Noetzli
2019-04-30fixAndres Noetzli
2019-04-30Merge branch 'master' into cav2019stringsAndres Noetzli
2019-04-30revert diffAndres Noetzli
2019-04-30Fix concat-find regexp elimination (#2983)Andres Noetzli
2019-04-30Remove stoi solve rewrite (#2985)Andrew Reynolds
2019-04-30Fix use of APPLY kind in examples (#2984)Andres Noetzli
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-29Optimization for evaluation with unfolding (#2979)Andrew Reynolds
2019-04-25New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)Aina Niemetz
This cleans up naming of API functions to create first-order constants and variables. mkVar -> mkConst mkBoundVar -> mkVar declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed. Note that we want to avoid redundancy in order to reduce code duplication and maintenance overhead (we do not allow nested API calls, since this is problematic when tracing API calls).
2019-04-24Fix compiler warning. (#2975)Aina Niemetz
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-04-24Dco fix (#2973)Clark Barrett
2019-04-24README: Remove project leaders, history.Aina Niemetz
2019-04-24CONTRIBUTING: 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-23Refactor normal forms in strings (#2897)Andrew Reynolds
2019-04-22Add CONTRIBUTING file. (#2968)Aina Niemetz
2019-04-18Add option to do extended rewriting preprocessing onlyAndres Noetzli
2019-04-18Fail 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-17Cache explanations in the equality engine (#2937)Andrew Reynolds
2019-04-17More use of isClosure (#2959)Andrew Reynolds
2019-04-17Add rewrite for splitting equalitiesAndres Noetzli
This commit adds an extended rewrite that splits a given string equality into multiple equalities if it can find prefixes of equal lengths. For example: `(= (str.++ x "AB" z) (str.++ "A" x y)) ---> (and (= (str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y))`
2019-04-17mergeAndres Noetzli
2019-04-17Fix 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-16Add interface for term enumeration (#2956)Andrew Reynolds
2019-04-16Make 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-16Stratify enumerative instantiation (#2954)Andrew Reynolds
2019-04-16Minor simplifications to theory quantifiers (#2953)Andrew Reynolds
2019-04-15Check 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-15Initial 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-12Referring to prerelease 1.8 (#2943)Haniel Barbosa
2019-04-11 Eliminate Boolean ITE within terms, fixes 2947 (#2949)Andrew Reynolds
2019-04-09Removing references to cvc4-bugs@... (#2945)Haniel Barbosa
2019-04-08"prerelease -> release" in INSTALL (#2944)Haniel Barbosa
2019-04-08Fix email address of the bugs email list and delete obsolete RELEASE-NOTES.Aina Niemetz
2019-04-08fix copyright year in configuration file (#2942)Haniel Barbosa
2019-04-05prerelease -> release (#2941)Haniel Barbosa
2019-04-05Fix another corner case of datatypes+PBE (#2938)Andrew Reynolds
2019-04-05fix fp issue (#2940)Haniel Barbosa
2019-04-05SatClauseSetHashFunction (#2916)Alex Ozdemir
* SatClauseHashFunction Added to the same file as SatLiteralHashFunction. * clang-format Thanks Andres!
2019-04-04adding sygus news (#2934)Haniel Barbosa
2019-04-04Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)Haniel Barbosa
2019-04-03Update release notes and lib version (#2933)Haniel Barbosa
2019-04-03Update copyright headers.Aina Niemetz
2019-04-03get-authors: Add GitHub user ayveejay -> Andrew V. Jones.Aina Niemetz
2019-04-03Fix combination of datatypes + strings in PBE (#2930)Andrew Reynolds
2019-04-01FP: 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-01Fix 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback