Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-06-17 | Fix interface for bindingsnext_model_cherry_fix | Andres Noetzli | |
2019-06-17 | document nodesToBlock | yoni206 | |
2019-06-17 | passing reference instead of pointer | yoni206 | |
2019-06-17 | minor | yoni206 | |
2019-06-17 | better interface | yoni206 | |
2019-06-17 | remove include | yoni206 | |
2019-06-17 | model blocker with get values | yoni206 | |
2019-06-07 | Merge pull request #17 from yoni206/next_model | Andrew Reynolds | |
2019-06-06 | more fixes | yoni206 | |
2019-06-06 | fixes | yoni206 | |
2019-06-06 | compiling | yoni206 | |
2019-06-06 | Merge branch 'modelBlocker' of https://github.com/ajreynol/CVC4 into next_model | yoni206 | |
2019-06-06 | Bug fix, doc | ajreynol | |
2019-05-17 | Merge remote-tracking branch 'ajreynol/modelBlocker' into next_model | yoni206 | |
2019-05-17 | Format | ajreynol | |
2019-05-17 | Fix doc | ajreynol | |
2019-05-17 | Merge branch 'master' of https://github.com/CVC4/CVC4 into modelBlocker | ajreynol | |
2019-05-17 | Fix degenerate case | ajreynol | |
2019-05-17 | Merge remote-tracking branch 'ajreynol/modelBlocker' into next_model | yoni206 | |
2019-05-15 | Fix iterators in Java API (#3000) | Andres Noetzli | |
Fixes #2989. SWIG 3 seems to have an issue properly resolving `T::const_iterator::value_type` if that type itself is a `typedef`. This is for example the case in the `UnsatCore` class, which `typedef`s `const_iterator` to `std::vector<Expr>::const_iterator`. As a workaround, this commit changes the `JavaIteratorAdapter` class to take two template parameters, one of which is the `value_type`. The commit also adds a compile-time assertion that `T::const_iterator::value_type` can be converted to `value_type` to avoid nasty surprises. A nice side-effect of this solution is that explicit `typemap`s are not necessary anymore, so they are removed. Additionally, the commit adds a `toString()` method for the Java API of `UnsatCore` and adds examples that show and test the iteration over the unsat core and the statistics. Iterating over `Statistics` now returns instances of `Statistic` instead of `Object[]`, which is a bit cleaner and requires less glue code. | |||
2019-05-15 | cmake: Install JAR and JNI files for Java bindings. (#3002) | Mathias Preiner | |
Default install paths are: - libcvc4jni.so in /usr/lib/ - CVC4.jar in /usr/share/java/cvc4 Fixes #2990. | |||
2019-05-15 | BV: Do not enable abstraction when eager bit-blasting by default. (#3001) | Aina Niemetz | |
2019-05-15 | Fix model of Boolean vars with eager bit-blaster (#2998) | Andres Noetzli | |
When bit-blasting eagerly, we were not assigning values to the Boolean variables in the `TheoryModel`. With eager bit-blasting, the BV SAT solver gets all (converted) terms, including the Boolean ones, so `EagerBitblaster::collectModelInfo()` is responsible for assigning values to Boolean variables. However, it has only been assigning values to bit-vector variables, which lead to wrong models. This commit fixes the issue by asking the `CnfStream` for the Boolean variables, querying the SAT solver for their value, and assigning them in the `TheoryModel`. | |||
2019-05-15 | Fix printing of bvurem (#2963) | Andrew Reynolds | |
2019-05-10 | Disable relational triggers (#2994) | Andrew Reynolds | |
2019-05-09 | Fixes for relational triggers (#2967) | Andrew Reynolds | |
2019-05-06 | Add support for re.all (#2980) | Andres Noetzli | |
2019-05-02 | Simple optimizations to core strings theory. (#2988) | Andrew Reynolds | |
2019-05-01 | Fix re-elim-agg regressions (#2987) | Andrew Reynolds | |
2019-05-01 | Use total versions of div/mod in re-elim-agg (#2986) | Andrew Reynolds | |
2019-04-30 | Fix concat-find regexp elimination (#2983) | Andres Noetzli | |
2019-04-30 | Remove stoi solve rewrite (#2985) | Andrew Reynolds | |
2019-04-30 | Fix use of APPLY kind in examples (#2984) | Andres Noetzli | |
2019-04-29 | Eliminate APPLY kind (#2976) | Andrew Reynolds | |
2019-04-29 | Optimization for evaluation with unfolding (#2979) | Andrew Reynolds | |
2019-04-25 | New 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-24 | Fix compiler warning. (#2975) | Aina Niemetz | |
2019-04-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
Fixes 2887. | |||
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 | |