Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-09-17 | More aggressive skolem caching for strings, document and clean preprocessor ↵ | Andrew Reynolds | |
(#2478) | |||
2018-09-13 | Generalize CandidateRewriteDatabase to ExprMiner (#2340) | Andrew Reynolds | |
2018-09-13 | Uses information gain heuristic for building better solutions from DTs (#2451) | Haniel Barbosa | |
2018-09-11 | Support model cores via option --produce-model-cores. (#2407) | Andrew Reynolds | |
This adds support for model cores, fixes #1233. It includes some minor cleanup and additions to utility functions. | |||
2018-09-10 | Using a single condition enumerator in sygus-unif (#2440) | Haniel Barbosa | |
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case). In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts: - _main advantage_: can quickly enumerate relevant condition values for solving the problem - _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie. A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif. There is also small improvements for trace messages. | |||
2018-09-07 | Replace boost::integer_traits with std::numeric_limits. (#2439) | Mathias Preiner | |
Further, remove redundant gmp.h include in options_handler.cpp. | |||
2018-09-04 | Remove unused options file (#2413) | Andres Noetzli | |
2018-08-31 | Allows SAT checks of repair const to have different options (#2412) | Haniel Barbosa | |
2018-08-30 | Add regular expression elimination module (#2400) | Andrew Reynolds | |
2018-08-22 | More unused code elimination (#2358) | Andrew Reynolds | |
2018-08-21 | Makes the new row propagation system default (#2335) | Haniel Barbosa | |
2018-08-20 | More unused code elimination (#2339) | Andrew Reynolds | |
2018-08-08 | Disable argument relevance for sygus by default (#2288) | Andrew Reynolds | |
2018-08-07 | Require Swig 3 (#2283) | Andres Noetzli | |
Removes some hacks due to Swig 2's incomplete C++11 support and adds checks for version 3 at configuration time as well as in swig.h | |||
2018-08-07 | Delete functions instead of using CVC4_UNDEFINED (#1794) | Andres Noetzli | |
C++11 supports explicitly deleting functions that should not be used (explictly or implictly), e.g. copy or assignment constructors. We were previously using the CVC4_UNDEFINED macro that used a compiler-specific attribute. The C++11 feature should be more portable. | |||
2018-08-06 | Make flat form inferences optional in strings (#2277) | Andrew Reynolds | |
2018-08-03 | Eliminate option for sygus UF evaluation functions (#2262) | Andrew Reynolds | |
2018-08-02 | Remove Subversion build info (#2250) | Andres Noetzli | |
2018-08-01 | Remove outdated references to TLS (#2245) | Andres Noetzli | |
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-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 | 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-26 | Avoid explicit dependency on Python 3 (#2195) | ayveejay | |
2018-07-24 | Improvements to sets + cardinality + quantifiers (#2200) | 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-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 | Minor cleanup and fixes for conflict-based instantiation (#2123) | Andrew Reynolds | |
2018-07-17 | sygusComp2018: update policies for solution reconstruction (#2109) | Andrew Reynolds | |
2018-07-17 | sygusComp 2018: updates to sygus term database (#2170) | Andrew Reynolds | |
2018-07-08 | Add more sophisticated floating-point sampler (#2155) | Andres Noetzli | |
This commit adds a floating-point sampler inspired by PyMPF [0]. It also creates a new Sampler class that can be used for creating random values of different sorts (currently BV and FP values). [0] https://github.com/florianschanda/PyMPF | |||
2018-07-06 | Add option for timeout for rewrite candidate check (#2156) | Andres Noetzli | |
2018-07-02 | Remove miscellaneous dead and unused code from quantifiers (#2121) | Andrew Reynolds | |
2018-07-02 | Remove some dead code from theory strings (#2125) | Andrew Reynolds | |
2018-06-27 | Synthesize candidate-rewrites from standard inputs (#1918) | Andrew Reynolds | |
2018-06-26 | sygusComp2018: Add evaluator (#2090) | Andres Noetzli | |
This commit adds the Evaluator class that can be used to quickly evaluate terms under a given substitution without going through the rewriter. This has been shown to lead to significant performance improvements on SyGuS PBE problems with a large number of inputs because candidate solutions are evaluated on those inputs. With this commit, the evaluator only gets called from the SyGuS solver but there are potentially other places in the code that could profit from it. | |||
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-06-15 | Disable solving non-linear BV literals by default (#2070) | Andrew Reynolds | |
2018-05-28 | Builtin evaluation functions for sygus (#1991) | Andrew Reynolds | |
2018-05-25 | Reenable repair const (#1983) | Andrew Reynolds | |
2018-05-23 | Add notions of evaluated kinds in TheoryModel (#1947) | Andrew Reynolds | |
2018-05-23 | Generalize check-model in NonLinearExtension for quadratic equations (#1892) | Andrew Reynolds | |
2018-05-22 | Repair constants using symbolic constructors (#1960) | Andrew Reynolds | |
2018-05-21 | Add SymFPU licensing information. (#1952) | Mathias Preiner | |
2018-05-18 | changing default (#1944) | Haniel Barbosa | |
2018-05-17 | Option to force return values of Bool functions to be constant in CegisUnif ↵ | Haniel Barbosa | |
(#1930) | |||
2018-05-17 | Cegis-specific infrastructure (#1933) | Andrew Reynolds | |