Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |
2018-05-14 | Add regressions, change defaults. (#1911) | Andrew Reynolds | |
2018-05-10 | Sygus repair constants (#1812) | Andrew Reynolds | |
2018-05-09 | Better option names for PBE (#1891) | Andrew Reynolds | |
2018-05-09 | Add the symmetry breaker module (#1847) | PaulMeng | |
2018-05-04 | Make --output-lang consistent with --lang (#1877) | Andres Noetzli | |
2018-05-03 | Option to interleave tangent plane inferences (#1833) | Andrew Reynolds | |
2018-05-02 | Remove (dummy) SMT1 printer (#1854) | Andres Noetzli | |
2018-05-02 | Initial support for string standard in smt lib 2.6 (#1848) | Andrew Reynolds | |
2018-05-01 | Improve tangent planes for transcendental functions (#1832) | Andrew Reynolds | |