| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-31 | Remove hasAssertions() method from eager BV solver. (#2239) | Mathias Preiner | |
| 2018-07-31 | Fix option handler for lazy/bv-sat-solver combinations. (#2225) | Mathias Preiner | |
| Further, unifies all *limitHandler and *limitPerHandler to limitHandler. | |||
| 2018-07-30 | Add support for incremental eager bit-blasting. (#1838) | Mathias Preiner | |
| Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat. | |||
| 2018-07-30 | Fix several spelling errors (#2231) | FabianWolff | |
| 2018-07-29 | Storing a std::pair<Key,Data> on CDOhash_map. | Tim King | |
| Changing the return type of CDHashMap::iterator* to return a reference. Requires performance testing. | |||
| 2018-07-27 | Require argument description for non-{bool,void} options. (#2228) | Mathias Preiner | |
| Not adding the argument description for non-{bool,void} options is now an error. Further, adds missing argument descriptions. | |||
| 2018-07-27 | Fix issues related to cxxtest in configure.ac (#2226) | Andres Noetzli | |
| Fixes #2188. There were two issues related to cxxtest in configure.ac: - `AC_PATH_PROGS` was used wrong (the third argument is a value to assign to the first argument and cannot be used for arbitrary commands) - The `test` command always executes both sides of an "and" (`-a`), so `basename` was called without arguments when `CXXTESTGEN` was empty This commit fixes both issues. | |||
| 2018-07-27 | Make Python a required CVC4 dependency. (#2227) | Mathias Preiner | |
| Python is required for generating the options code. The dependency is now required. Now autoconf searches for a Python version >= 2.7 and sets the corresponding environment variables. mkoptions.py is now called with $(PYTHON). This fixes the broken competition and windows nightly builds. | |||
| 2018-07-27 | Fix for candidate rewrite rule filtering. (#2220) | Andrew Reynolds | |
| 2018-07-27 | Make check-synth robust for assertions that are not the synth conjecture ↵ | Andrew Reynolds | |
| (#2217) | |||
| 2018-07-27 | Fix Node::hasFreeVar for function variables (#2216) | Andrew Reynolds | |
| A Node has free variables if its operator has free variables. | |||
| 2018-07-26 | Fix CryptoMiniSat config to allow system versions. (#2223) | Mathias Preiner | |
| 2018-07-26 | New C++ API: Enable examples. (#2222) | Aina Niemetz | |
| 2018-07-26 | Removing unused CDTrailHashmap. (#2221) | Tim King | |
| 2018-07-26 | Disabling bvLazyRewriteExtf in the right place (#2214) | yoni206 | |
| 2018-07-26 | Changing CDInsertHashMap to store <const Key, const Data> pairs. This is in ↵ | Tim King | |
| preparation for adding map utility functions. (#2209) | |||
| 2018-07-26 | Changing the arithmetic static learner to use CDHashMap. This is 2/3 PRs for ↵ | Tim King | |
| deprecating CDTrailHashMap. (#2207) | |||
| 2018-07-26 | Fix rewriter for lambda (#2211) | Andrew Reynolds | |
| The rewriter for lambda is currently too aggressive, there are cases like: lambda xy. x = y that are converted into an array representation that when indexing based on x gives (store y true false), which is subsequently converted to: lambda fv_1 fv_2. fv_1 = y where fv_1 and fv_2 are canonical free variables. Here, y is used as index but was not substituted hence is incorrectly made free. To make things simpler, this PR disables any rewriting for lambda unless the array representation of the lambda is a constant, which hardcodes/simplifies a previous argument (reqConst=true). This fixes a sygus issue I ran into yesterday (regression added in this PR). Some parts of the code were formatted as a result. | |||
| 2018-07-26 | Fix a few issues in the sygus sampler related to evaluation (#2215) | Andrew Reynolds | |
| 2018-07-26 | Avoid explicit dependency on Python 3 (#2195) | ayveejay | |
| 2018-07-26 | New C++ API: Third batch of commands (SMT-LIB). (#2212) | Aina Niemetz | |
| 2018-07-26 | New C++ API: Second batch of commands (SMT-LIB). (#2201) | Aina Niemetz | |
| 2018-07-25 | Changing ArithIteUtils to use CDInsertHashMap. (#2206) | Tim King | |
| This is 1/3 PRs for deprecating CDTrailHashMap. | |||
| 2018-07-25 | Removing support for CDHashMap::iterator's postfix increment. (#2208) | Tim King | |
| 2018-07-25 | Move reg exp rewrites from prerewrite to postrewrite (#2204) | Andrew Reynolds | |
| 2018-07-25 | Performing clang-format on the original change-set of #2194 (#2203) | ayveejay | |
| 2018-07-25 | Use CryptoMiniSat 5.6.3. (#2205) | Mathias Preiner | |
| 2018-07-24 | Improvements to sets + cardinality + quantifiers (#2200) | Andrew Reynolds | |
| 2018-07-24 | Adding API access methods to get heap/nil expressions when using separation ↵ | ayveejay | |
| logic (#2194) | |||
| 2018-07-24 | New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199) | Aina Niemetz | |
| 2018-07-23 | Improve rewriter for regular expression concatenation (#2196) | Andrew Reynolds | |
| 2018-07-23 | Generalize symmetry detection for 1 symmetry variable mapped to n input ↵ | Andrew Reynolds | |
| variables (#1888) | |||
| 2018-07-23 | New C++ API: Implementation of Solver class: OpTerm handling. (#2164) | Aina Niemetz | |
| 2018-07-23 | New C++ API: declare-datatype. (#2166) | Aina Niemetz | |
| 2018-07-23 | sygusComp2018: add regressions (#2191) | Andrew Reynolds | |
| 2018-07-23 | Fix warning in sygus PBE (#2190) | Andrew Reynolds | |
| 2018-07-21 | sygusComp2018: Improvements to CEGIS loop (#2187) | Andrew Reynolds | |
| 2018-07-21 | Optimizations and fixes for computing whether a type is finite (#2179) | Andrew Reynolds | |
| 2018-07-21 | sygusComp2018: refactor and improve sygus io utility (#2185) | Andrew Reynolds | |
| 2018-07-21 | Remove --no-check-proofs and --no-check-unsat-cores from a satisfiable test ↵ | yoni206 | |
| (#2184) | |||
| 2018-07-21 | Cleanup and additions for candidate generator (#2173) | Andrew Reynolds | |
| 2018-07-20 | sygusComp2018: minor changes to repair constant utility (#2110) | Andrew Reynolds | |
| 2018-07-18 | sygusComp2018: pbe multi-enumerator fairness option (#2178) | Andrew Reynolds | |
| 2018-07-17 | Refactor sep-pre-skolem-emp preprocessing pass | yoni206 | |
| 2018-07-17 | Minor cleanup and fixes for conflict-based instantiation (#2123) | Andrew Reynolds | |
| 2018-07-17 | Do extended rewrite on results of quantifier elimination. (#2119) | Andrew Reynolds | |
| 2018-07-17 | Purify applications of exp to transcendental arguments (#2097) | Andrew Reynolds | |
| 2018-07-17 | sygusComp2018: update policies for solution reconstruction (#2109) | Andrew Reynolds | |
| 2018-07-17 | sygusComp2018: Improvements to datatypes sygus solver (#2177) | Andrew Reynolds | |
| 2018-07-17 | sygusComp 2018: updates to sygus term database (#2170) | 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