diff options
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/options_handler.cpp | 47 | ||||
| -rw-r--r-- | src/options/options_handler.h | 3 | ||||
| -rw-r--r-- | src/options/quantifiers_modes.h | 10 | ||||
| -rw-r--r-- | src/options/quantifiers_options | 31 | ||||
| -rw-r--r-- | src/options/smt_options | 3 |
5 files changed, 85 insertions, 9 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index c29cfc4d2..61f7646ee 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -492,6 +492,25 @@ all \n\ \n\ "; +const std::string OptionsHandler::s_cegisSampleHelp = + "\ +Modes for sampling with counterexample-guided inductive synthesis (CEGIS),\ +supported by --cegis-sample:\n\ +\n\ +none (default) \n\ ++ Do not use sampling with CEGIS.\n\ +\n\ +use \n\ ++ Use sampling to accelerate CEGIS. This will rule out solutions for a\ + conjecture when they are not satisfied by a sample point.\n\ +\n\ +trust \n\ ++ Trust that when a solution for a conjecture is always true under sampling,\ + then it is indeed a solution. Note this option may print out spurious\ + solutions for synthesis conjectures.\n\ +\n\ +"; + const std::string OptionsHandler::s_sygusInvTemplHelp = "\ Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ \n\ @@ -877,6 +896,34 @@ OptionsHandler::stringToCegqiSingleInvMode(std::string option, } } +theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode( + std::string option, std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::CEGIS_SAMPLE_NONE; + } + else if (optarg == "use") + { + return theory::quantifiers::CEGIS_SAMPLE_USE; + } + else if (optarg == "trust") + { + return theory::quantifiers::CEGIS_SAMPLE_TRUST; + } + else if (optarg == "help") + { + puts(s_cegisSampleHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --cegis-sample: `") + + optarg + + "'. Try --cegis-sample help."); + } +} + theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index e7bd87ebd..304009a98 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -108,6 +108,8 @@ public: std::string option, std::string optarg); theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode( std::string option, std::string optarg); + theory::quantifiers::CegisSampleMode stringToCegisSampleMode( + std::string option, std::string optarg); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( std::string option, std::string optarg); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode( @@ -243,6 +245,7 @@ public: static const std::string s_sygusSolutionOutModeHelp; static const std::string s_cbqiBvIneqModeHelp; static const std::string s_cegqiSingleInvHelp; + static const std::string s_cegisSampleHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_termDbModeHelp; static const std::string s_theoryOfModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 6274269ce..91fab54ff 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -216,6 +216,16 @@ enum CegqiSingleInvMode { CEGQI_SI_MODE_ALL, }; +enum CegisSampleMode +{ + /** do not use samples for CEGIS */ + CEGIS_SAMPLE_NONE, + /** use samples for CEGIS */ + CEGIS_SAMPLE_USE, + /** trust samples for CEGQI */ + CEGIS_SAMPLE_TRUST, +}; + enum SygusInvTemplMode { /** synthesize I( x ) */ SYGUS_INV_TEMPL_MODE_NONE, diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 2166f0add..48a577faf 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -270,8 +270,6 @@ option sygusQePreproc --sygus-qe-preproc bool :default false option sygusMinGrammar --sygus-min-grammar bool :default true statically minimize sygus grammars -option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false - aggressively minimize sygus grammars option sygusAddConstGrammar --sygus-add-const-grammar bool :default true statically add constants appearing in conjecture to grammars option sygusGrammarNorm --sygus-grammar-norm bool :default false @@ -294,10 +292,23 @@ option sygusCRefEval --sygus-cref-eval bool :default true direct evaluation of refinement lemmas for conflict analysis option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true use min explain for direct evaluation of refinement lemmas for conflict analysis - -option sygusStream --sygus-stream bool :default false + +option sygusStream --sygus-stream bool :read-write :default false enumerate a stream of solutions instead of terminating after the first one +option cegisSample --cegis-sample=MODE CVC4::theory::quantifiers::CegisSampleMode :read-write :default CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE :include "options/quantifiers_modes.h" :handler stringToCegisSampleMode + mode for using samples in the counterexample-guided inductive synthesis loop + +# internal uses of sygus +option sygusRewSynth --sygus-rr-synth bool :default false + use sygus to enumerate candidate rewrite rules via sampling +option sygusRewVerify --sygus-rr-verify bool :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 +option sygusSampleGrammar --sygus-sample-grammar bool :default true + when applicable, use grammar for choosing sample points + # CEGQI applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation @@ -315,6 +326,10 @@ option cbqiMultiInst --cbqi-multi-inst bool :read-write :default false when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation option cbqiRepeatLit --cbqi-repeat-lit bool :read-write :default false solve literals more than once in counterexample-based quantifier instantiation +option cbqiInnermost --cbqi-innermost bool :read-write :default true + only process innermost quantified formulas in counterexample-based quantifier instantiation +option cbqiNestedQE --cbqi-nested-qe bool :read-write :default false + process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation # CEGQI for arithmetic option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false @@ -333,10 +348,6 @@ option cbqiNopt --cbqi-nopt bool :default true non-optimal bounds for counterexample-based quantifier instantiation option cbqiLitDepend --cbqi-lit-dep bool :default true dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation -option cbqiInnermost --cbqi-innermost bool :read-write :default true - only process innermost quantified formulas in counterexample-based quantifier instantiation -option cbqiNestedQE --cbqi-nested-qe bool :read-write :default false - process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation # CEGQI for EPR option quantEpr --quant-epr bool :default false :read-write @@ -345,7 +356,7 @@ option quantEprMatching --quant-epr-match bool :default true use matching heuristics for EPR instantiation # CEGQI for BV -option cbqiBv --cbqi-bv bool :read-write :default true +option cbqiBv cbqi-bv --cbqi-bv bool :read-write :default true use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false interleave model value instantiation with word-level inversion approach @@ -355,6 +366,8 @@ option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true replaces extract terms with variables for counterexample-guided instantiation for bit-vectors option cbqiBvLinearize --cbqi-bv-linear bool :read-write :default true linearize adder chains for variables +option cbqiBvConcInv cbqi-bv-concat-inv --cbqi-bv-concat-inv bool :read-write :default true + compute inverse for concat over equalities rather than producing an invertibility condition ### local theory extensions options diff --git a/src/options/smt_options b/src/options/smt_options index fa6c3ae4e..b19420060 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -54,6 +54,9 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch dump the full unsat core, including unlabeled assertions +option checkSynthSol --check-synth-sol bool :default false + checks whether produced solutions to functions-to-synthesize satisfy the conjecture + option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch support the get-assignment command |