summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Collapse)Author
2018-08-22 More unused code elimination (#2358)Andrew Reynolds
2018-08-21Makes the new row propagation system default (#2335)Haniel Barbosa
2018-08-20More unused code elimination (#2339)Andrew Reynolds
2018-08-08Disable argument relevance for sygus by default (#2288)Andrew Reynolds
2018-08-07Require 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-07Delete 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-06Make flat form inferences optional in strings (#2277)Andrew Reynolds
2018-08-03Eliminate option for sygus UF evaluation functions (#2262)Andrew Reynolds
2018-08-02Remove Subversion build info (#2250)Andres Noetzli
2018-08-01Remove outdated references to TLS (#2245)Andres Noetzli
2018-07-31Fix option handler for lazy/bv-sat-solver combinations. (#2225)Mathias Preiner
Further, unifies all *limitHandler and *limitPerHandler to limitHandler.
2018-07-30Add 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-30Fix several spelling errors (#2231)FabianWolff
2018-07-27Require 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-27Make 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-26Avoid explicit dependency on Python 3 (#2195)ayveejay
2018-07-24Improvements to sets + cardinality + quantifiers (#2200)Andrew Reynolds
2018-07-21 sygusComp2018: Improvements to CEGIS loop (#2187)Andrew Reynolds
2018-07-21Optimizations 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-17Minor cleanup and fixes for conflict-based instantiation (#2123)Andrew Reynolds
2018-07-17 sygusComp2018: update policies for solution reconstruction (#2109)Andrew Reynolds
2018-07-17sygusComp 2018: updates to sygus term database (#2170)Andrew Reynolds
2018-07-08Add 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-06Add option for timeout for rewrite candidate check (#2156)Andres Noetzli
2018-07-02Remove miscellaneous dead and unused code from quantifiers (#2121)Andrew Reynolds
2018-07-02Remove some dead code from theory strings (#2125)Andrew Reynolds
2018-06-27Synthesize candidate-rewrites from standard inputs (#1918)Andrew Reynolds
2018-06-26sygusComp2018: 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-25Updated copyright headers.Aina Niemetz
2018-06-15Disable solving non-linear BV literals by default (#2070)Andrew Reynolds
2018-05-28Builtin evaluation functions for sygus (#1991)Andrew Reynolds
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-21Add SymFPU licensing information. (#1952)Mathias Preiner
2018-05-18changing default (#1944)Haniel Barbosa
2018-05-17Option to force return values of Bool functions to be constant in CegisUnif ↵Haniel Barbosa
(#1930)
2018-05-17Cegis-specific infrastructure (#1933)Andrew Reynolds
2018-05-14Add regressions, change defaults. (#1911)Andrew Reynolds
2018-05-10Sygus repair constants (#1812)Andrew Reynolds
2018-05-09Better option names for PBE (#1891)Andrew Reynolds
2018-05-09Add the symmetry breaker module (#1847)PaulMeng
2018-05-04Make --output-lang consistent with --lang (#1877)Andres Noetzli
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-05-02Remove (dummy) SMT1 printer (#1854)Andres Noetzli
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-05-01Improve tangent planes for transcendental functions (#1832)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback