| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-09 | Merge branch 'master' into miscWarns | Andres Noetzli | |
| 2018-10-09 | address comments | Andres Noetzli | |
| 2018-10-09 | Support for basic actively-generated enumerators (#2606) | Andrew Reynolds | |
| 2018-10-09 | Random: support URNG interface (#2595) | Aina Niemetz | |
| Use std::shuffle (with Random as the unified random generator) instead of std::random_shuffle for deterministic, reproducable random shuffling. | |||
| 2018-10-09 | Allow multiple synthesis conjectures. (#2593) | Andrew Reynolds | |
| 2018-10-08 | BV instantiator: Factor out util functions. (#2604) | Aina Niemetz | |
| Previously, all util functions for the BV instantiator were static functions in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h). Asan reported errors for the corresponing unit test because of this. | |||
| 2018-10-08 | BV inverter: Factor out util functions. (#2603) | Aina Niemetz | |
| Previously, all invertibility condition functions were static functions in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/bv_inverter_utils.(cpp|h). | |||
| 2018-10-08 | Fix string register extended terms (#2597) | Andrew Reynolds | |
| A regress2 benchmark was failing, due to a recent change in our strings rewriter. The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings. The fix is to ensure that extended function terms in any assertions *or shared terms* are registered. This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed. | |||
| 2018-10-08 | Fix compiler warnings | Andres Noetzli | |
| This commit fixes two compiler warnings related to parentheses and two warnings related to derived classes hiding methods from the base class with the same name. | |||
| 2018-10-08 | Disable extended rewriter when applicable with var agnostic enumeration (#2594) | Andrew Reynolds | |
| 2018-10-05 | Fix unif trace (#2550) | Haniel Barbosa | |
| 2018-10-05 | Fix cache for sygus post-condition inference (#2592) | Andrew Reynolds | |
| 2018-10-05 | Update default options for sygus (#2586) | Andrew Reynolds | |
| 2018-10-04 | Fix rewrite rule filtering. (#2591) | Andrew Reynolds | |
| 2018-10-04 | Infrastructure for string length entailments via approximations (#2514) | Andrew Reynolds | |
| 2018-10-04 | Fix end constraint for regexp elimination (#2571) | Andrew Reynolds | |
| 2018-10-04 | Clean remaining references to getNextDecisionRequest and simplify (#2500) | Andrew Reynolds | |
| 2018-10-03 | Fix compiler warnings. (#2585) | Aina Niemetz | |
| 2018-10-03 | Add actively generated sygus enumerators (#2552) | Andrew Reynolds | |
| 2018-10-03 | Make CegisUnif with condition independent robust to var agnostic (#2565) | Haniel Barbosa | |
| 2018-10-03 | Fix stale op list in sets (#2572) | Andrew Reynolds | |
| 2018-10-03 | Eliminate partial operators within lambdas during grammar normalization (#2570) | Andrew Reynolds | |
| 2018-10-01 | init scalar class members (coverity issues 1473720 and 1473721) (#2554) | Haniel Barbosa | |
| 2018-10-01 | Fix compiler warnings. (#2555) | Aina Niemetz | |
| 2018-09-30 | Add rewrite for solving stoi (#2532) | Andrew Reynolds | |
| 2018-09-29 | Stream concrete values for variable agnostic enumerators (#2526) | Haniel Barbosa | |
| 2018-09-28 | Rewrites for (= "" _) and (= (str.replace _) _) (#2546) | Andres Noetzli | |
| 2018-09-27 | Remove assertion. (#2549) | Andrew Reynolds | |
| 2018-09-27 | Infrastructure for using active enumerators in sygus modules (#2547) | Andrew Reynolds | |
| 2018-09-27 | Incorporate all unification enumerators into getTermList. (#2541) | Andrew Reynolds | |
| 2018-09-27 | Fix Taylor overapproximation for large exponentials (#2538) | Andrew Reynolds | |
| 2018-09-26 | Fix homogeneous string constant rewrite (#2545) | Andrew Reynolds | |
| 2018-09-26 | Symmetry breaking for variable agnostic enumerators (#2527) | Andrew Reynolds | |
| 2018-09-25 | Eagerly ensure literal on active guards for sygus enumerators (#2531) | Andrew Reynolds | |
| 2018-09-25 | Fix warnings uncovered by cmake build (#2521) | Andrew Reynolds | |
| 2018-09-24 | Fix quantifiers selector over store rewrite (#2510) | Andrew Reynolds | |
| Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in. After the change, we are +61-7 on SMT LIB: https://www.starexec.org/starexec/secure/details/job.jsp?id=30581 | |||
| 2018-09-24 | Allow partial models for multiple sygus enumerators (#2499) | Andrew Reynolds | |
| 2018-09-24 | Infrastructure for variable agnostic sygus enumerators (#2511) | Andrew Reynolds | |
| 2018-09-24 | Improve non-linear check model error handling (#2497) | Andrew Reynolds | |
| 2018-09-24 | Refactor strings equality rewriting (#2513) | Andrew Reynolds | |
| This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter. | |||
| 2018-09-24 | cmake: Fix dependencies for code generation. (#2524) | Mathias Preiner | |
| 2018-09-24 | cmake: Fix theory order #2. (#2522) | Mathias Preiner | |
| 2018-09-24 | Unify rewrites related to (str.contains x y) --> (= x y) (#2512) | Andres Noetzli | |
| 2018-09-24 | cmake: Fix theory order. (#2518) | Mathias Preiner | |
| 2018-09-22 | cmake: Only build libcvc4 and libcvc4parser as libraries. | Mathias Preiner | |
| The sources of all previous libraries are now added to libcvc4 and built as libcvc4. This removes circular dependencies between libcvc4 and libexpr. Further, we now only have one parser library and don't build additional libraries for each language. | |||
| 2018-09-22 | cmake: Remove unused CMakeLists.txt | Mathias Preiner | |
| 2018-09-22 | cmake: Working build infrastructure. | Mathias Preiner | |
| TODO: cvc4autoconfig.h | |||
| 2018-09-22 | cmake: .cpp generation done, .h generation not yet complete | Aina Niemetz | |
| 2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
| 2018-09-19 | Decision strategy: incorporate arrays. (#2495) | 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