diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-08 14:01:17 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-08 14:01:17 -0600 |
| commit | 8a64433caffd3bedd99c0e73dac0941b87060778 (patch) | |
| tree | 9c3f9502aaf8f750a3c75820e8dc6836239dabb3 /src/options/quantifiers_options | |
| parent | 9b3d7b040def03d1b5764ddfafc24ac24b40d0ef (diff) | |
Minor improvements to sygus sampling. (#1577)
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 48a577faf..e97f11db9 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -300,9 +300,11 @@ option cegisSample --cegis-sample=MODE CVC4::theory::quantifiers::CegisSampleMod mode for using samples in the counterexample-guided inductive synthesis loop # internal uses of sygus -option sygusRewSynth --sygus-rr-synth bool :default false +option sygusRew --sygus-rr bool :default false + use sygus to enumerate and verify correctness of rewrite rules via sampling +option sygusRewSynth --sygus-rr-synth bool :read-write :default false use sygus to enumerate candidate rewrite rules via sampling -option sygusRewVerify --sygus-rr-verify bool :default false +option sygusRewVerify --sygus-rr-verify bool :read-write :default false use sygus to verify the correctness of rewrite rules via sampling option sygusSamples --sygus-samples=N int :read-write :default 100 :read-write number of points to consider when doing sygus rewriter sample testing |