summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-06-17Fix interface for bindingsnext_model_cherry_fixAndres Noetzli
2019-06-17document nodesToBlockyoni206
2019-06-17passing reference instead of pointeryoni206
2019-06-17minoryoni206
2019-06-17better interfaceyoni206
2019-06-17remove includeyoni206
2019-06-17model blocker with get valuesyoni206
2019-06-07Merge pull request #17 from yoni206/next_modelAndrew Reynolds
2019-06-06more fixesyoni206
2019-06-06fixesyoni206
2019-06-06compilingyoni206
2019-06-06Merge branch 'modelBlocker' of https://github.com/ajreynol/CVC4 into next_modelyoni206
2019-06-06Bug fix, docajreynol
2019-05-17Merge remote-tracking branch 'ajreynol/modelBlocker' into next_modelyoni206
2019-05-17Formatajreynol
2019-05-17Fix docajreynol
2019-05-17Merge branch 'master' of https://github.com/CVC4/CVC4 into modelBlockerajreynol
2019-05-17Fix degenerate caseajreynol
2019-05-17Merge remote-tracking branch 'ajreynol/modelBlocker' into next_modelyoni206
2019-05-15Fix 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-15cmake: 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-15Fix 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-15Fix printing of bvurem (#2963)Andrew Reynolds
2019-05-10Disable relational triggers (#2994)Andrew Reynolds
2019-05-09Fixes for relational triggers (#2967)Andrew Reynolds
2019-05-06Add support for re.all (#2980)Andres Noetzli
2019-05-02Simple optimizations to core strings theory. (#2988)Andrew Reynolds
2019-05-01Fix 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-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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback