summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Collapse)Author
2020-03-18Always enable cbqi literal dependency (#4116)Andrew Reynolds
Fixes #4105. It appears that the two (experimental) options in that issue were incompatible. A block of code changed indentation in this PR and was updated to guidelines.
2020-03-13Removing a few deprecated options (#4052)Andrew Reynolds
2020-03-12Remove local theory extension option (#4048)Andrew Reynolds
This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0.
2020-03-11Hide options for and related to the BV abstraction module. (#4041)Aina Niemetz
All things related to the current BV solver are obsolete in the sense that we are working on a new BV solver implementation. The BV abstraction module has several issues and is quite hacky, it should only be enabled in experimental settings. We don't want to remove it yet though, we want to keep it around for future evaluation purposes. This commit categorizes the option to enable the module and a second option related to the module as 'undocumented'.
2020-03-11Remove experimental symmetry breaker (#4005)Andrew Reynolds
This never impacted performance positively. Fixes #3997 and fixes #4015. There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique.
2020-03-11Remove partial instantiation for local theory extensions (#4020)Andrew Reynolds
Fixes #4019. This feature was never fully implemented.
2020-03-09Rename sygus option name (#3977)Andrew Reynolds
This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach). It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.
2020-03-05Remove --apply-to-const preprocessing pass (#3919)Andres Noetzli
Fixes #3914. The pass was only applicable to inputs with UFs that were exclusively applied to single integer values. This limitation seems to make the preprocessing pass not very useful in practice and it is subsumed by our Ackermannization pass, which can remove UFs from more complex inputs. Thus, this commit removes the preprocessing pass.
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. Co-authored-by: Clark Barrett <barrett@cs.stanford.edu> Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com> Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com> Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu> Co-authored-by: makaimann <makaim@stanford.edu> Co-authored-by: yoni206 <yoni206@users.noreply.github.com> Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> Co-authored-by: AleksandarZeljic <zeljic@stanford.edu> Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com> Co-authored-by: Amalee <amaleewilson@gmail.com> Co-authored-by: Scott Kovach <dskovach@gmail.com> Co-authored-by: ntsis <nekuna@gmail.com>
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter ↵Andrew Reynolds
(#3841) Fixes #3839. Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy. This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy. Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards. This PR relies on #3840.
2020-02-26Support for witnessing choice in models (#3781)Andrew Reynolds
Fixes #3300. This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
2020-02-26Remove portfolio leftovers (#3821)Andres Noetzli
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio build but there were some leftovers. This commit removes them.
2020-02-24bv_to_int preprocessing passyoni206
Introduces a preprocessing pass that translates bv problems to integer problems.
2020-02-21Adding checks to the validation of 'bv-sat-solver' to ensure that the ↵Andrew V. Jones
selected SAT solver is compiled-in (#3771)
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`). Fixes #3751.
2020-02-17Option to limit the number of rounds of enumerative instantiation (#3760)Andrew Reynolds
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-11Remove `--strings-binary-csp` option (#3743)Andres Noetzli
2020-01-31Allow PBE symmetry breaking with sygus stream (#3686)Andrew Reynolds
2019-12-19Fix typo in smt_options.toml. (#3579)Mathias Preiner
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
2019-12-10Fix ufho issues (#3551)Haniel Barbosa
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-04New grammar construction modes for SyGuS (#3486)Andrew Reynolds
2019-11-29Check free variables in assertions when using SyGuS (#3504)Andrew Reynolds
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
2019-11-21hard limit for rec-fun eval (#3485)Haniel Barbosa
2019-11-16Add support for ThreadSanitizer instrumentation (#3467)Andres Noetzli
This commit adds support for compiling CVC4 with ThreadSanitizer instrumentation. This is useful for debugging issues when CVC4 is used in a multi-threaded context (e.g. #3292).
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-20Cleaning-up the declaration of wrapped functions/methods, which have no ↵Andrew V. Jones
definitions (#3399) Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
2019-10-11Add support for UBSan instrumentation (#3382)Andres Noetzli
This commit adds support for compiling CVC4 with UBSan instrumentation. The commit also adds a dummy version of `AigBitblaster`. Previously, when CVC4 was built without ABC, `AigBitblaster` was not fully defined (the class was declared but the implementation was not being compiled). This lead to missing RTTI information when compiling with UBSan instrumentation.
2019-10-08Make ackermannization generally applicable rather than just BV (#3315)Ying Sheng
The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.
2019-09-29Add help for sygus 2.0 (#3318)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-09-16Fix compiler warning in options.cpp. (#3284)Aina Niemetz
2019-09-12 Rename UF with cardinality extension (#3241)Andrew Reynolds
2019-09-06Remove portfolio (#3236)Andrew Reynolds
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version). Fixes #2948 and fixes #1313.
2019-08-23Update dynamic splitting strategy for quantifiers (#3162)Andrew Reynolds
2019-08-14Remove option --continued-execution. (#3189)Mathias Preiner
2019-08-14Call separate SMT engine for single invocation sygus (#3151)Andrew Reynolds
2019-08-13Implement check abduct feature (#3152)Andrew Reynolds
2019-08-10Add option to only dump unsolved queries for --sygus-query-gen (#3173)Andrew Reynolds
2019-08-03Collapse @ chains in SMT2 printer (#3140)Haniel Barbosa
2019-08-02Update CaDiCaL to version 1.0.3. (#3137)Mathias Preiner
* Removes incremental API check (#3011) * Fixes toSatValueLit to use the new semantics of CaDiCaL's val() Fixes #3011
2019-08-01 Regular expression intersection modes (#3134)Andrew Reynolds
2019-07-31Parsing THF and adding several regressions (#3131)Haniel Barbosa
2019-07-29Model blocker feature (#3112)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback