diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:06:52 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:07:11 -0500 |
commit | f3590092818d9eab9d961ea602093029ff472a85 (patch) | |
tree | 1401f00df0d9659ba2321ea2088fe0c3f4de9f52 /src/options | |
parent | d598a9644862d176632071bca8448765d9cc3cc1 (diff) |
Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/Makefile.am | 1 | ||||
-rw-r--r-- | src/options/datatypes_modes.h | 44 | ||||
-rw-r--r-- | src/options/datatypes_options | 18 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 22 | ||||
-rw-r--r-- | src/options/options_handler.h | 3 | ||||
-rw-r--r-- | src/options/quantifiers_modes.h | 13 | ||||
-rw-r--r-- | src/options/quantifiers_options | 34 |
7 files changed, 95 insertions, 40 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 5a9fa54e6..ff889bcb2 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -229,6 +229,7 @@ liboptions_la_SOURCES = \ base_handlers.h \ bv_bitblast_mode.cpp \ bv_bitblast_mode.h \ + datatypes_modes.h \ decision_mode.cpp \ decision_mode.h \ decision_weight.h \ diff --git a/src/options/datatypes_modes.h b/src/options/datatypes_modes.h new file mode 100644 index 000000000..3576ffc72 --- /dev/null +++ b/src/options/datatypes_modes.h @@ -0,0 +1,44 @@ +/********************* */ +/*! \file datatypes_modes.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__BASE__DATATYPES_MODES_H +#define __CVC4__BASE__DATATYPES_MODES_H + +#include <iostream> + +namespace CVC4 { +namespace theory { + +enum SygusFairMode { + /** enforce fairness by direct conflict lemmas */ + SYGUS_FAIR_DIRECT, + /** enforce fairness by datatypes size */ + SYGUS_FAIR_DT_SIZE, + /** enforce fairness by datatypes height bound */ + SYGUS_FAIR_DT_HEIGHT_PRED, + /** enforce fairness by datatypes size bound */ + SYGUS_FAIR_DT_SIZE_PRED, + /** do not use fair strategy for CEGQI */ + SYGUS_FAIR_NONE, +}; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__BASE__DATATYPES_MODES_H */ diff --git a/src/options/datatypes_options b/src/options/datatypes_options index bb92b4e05..d4d3e941c 100644 --- a/src/options/datatypes_options +++ b/src/options/datatypes_options @@ -29,5 +29,23 @@ option dtInferAsLemmas --dt-infer-as-lemmas bool :default false # regression explanations for datatype lemmas option dtBlastSplits --dt-blast-splits bool :default false when applicable, blast splitting lemmas for all variables at once +option dtSharedSelectors --dt-share-sel bool :default true + internally use shared selectors across multiple constructors +option sygusSymBreak --sygus-sym-break bool :default true + simple sygus sym break lemmas +option sygusSymBreakDynamic --sygus-sym-break-dynamic bool :default true + dynamic sygus sym break lemmas +option sygusOpt1 --sygus-opt1 bool :default false + sygus experimental option +option sygusSymBreakLazy --sygus-sym-break-lazy bool :default true + lazily add symmetry breaking lemmas for terms +option sygusSymBreakRlv --sygus-sym-break-rlv bool :default true + add relevancy conditions to symmetry breaking lemmas + +option sygusFair --sygus-fair=MODE CVC4::theory::SygusFairMode :default CVC4::theory::SYGUS_FAIR_DT_SIZE :include "options/datatypes_modes.h" :handler stringToSygusFairMode + if and how to apply fairness for sygus +option sygusFairMax --sygus-fair-max bool :default true + use max instead of sum for multi-function sygus conjectures + endmodule diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 85fe1453f..5658b17b0 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -36,6 +36,7 @@ #include "options/bv_options.h" #include "options/decision_mode.h" #include "options/decision_options.h" +#include "options/datatypes_modes.h" #include "options/didyoumean.h" #include "options/language.h" #include "options/option_exception.h" @@ -399,11 +400,14 @@ norm \n\ "; const std::string OptionsHandler::s_cegqiFairModeHelp = "\ -Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\ +Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --sygus-fair:\n\ \n\ uf-dt-size \n\ + Enforce fairness using an uninterpreted function for datatypes size.\n\ \n\ +direct \n\ ++ Enforce fairness using direct conflict lemmas.\n\ +\n\ default | dt-size \n\ + Default, enforce fairness using size operator.\n\ \n\ @@ -716,17 +720,17 @@ theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std } } -theory::quantifiers::CegqiFairMode OptionsHandler::stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "uf-dt-size" ) { - return theory::quantifiers::CEGQI_FAIR_UF_DT_SIZE; +theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "direct") { + return theory::SYGUS_FAIR_DIRECT; } else if(optarg == "default" || optarg == "dt-size") { - return theory::quantifiers::CEGQI_FAIR_DT_SIZE; + return theory::SYGUS_FAIR_DT_SIZE; } else if(optarg == "dt-height-bound" ){ - return theory::quantifiers::CEGQI_FAIR_DT_HEIGHT_PRED; - //} else if(optarg == "dt-size-bound" ){ - // return theory::quantifiers::CEGQI_FAIR_DT_SIZE_PRED; + return theory::SYGUS_FAIR_DT_HEIGHT_PRED; + } else if(optarg == "dt-size-bound" ){ + return theory::SYGUS_FAIR_DT_SIZE_PRED; } else if(optarg == "none") { - return theory::quantifiers::CEGQI_FAIR_NONE; + return theory::SYGUS_FAIR_NONE; } else if(optarg == "help") { puts(s_cegqiFairModeHelp.c_str()); exit(1); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index fa87149f8..16c77b166 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -29,6 +29,7 @@ #include "options/base_handlers.h" #include "options/bv_bitblast_mode.h" #include "options/decision_mode.h" +#include "options/datatypes_modes.h" #include "options/language.h" #include "options/option_exception.h" #include "options/options.h" @@ -95,7 +96,6 @@ public: theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException); @@ -104,6 +104,7 @@ public: theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::FmfBoundMinMode stringToFmfBoundMinMode(std::string option, std::string optarg) throw(OptionException); + theory::SygusFairMode stringToSygusFairMode(std::string option, std::string optarg) throw(OptionException); // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value) throw(OptionException); diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 18c3bfeda..0b410e3fe 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -133,19 +133,6 @@ enum CVC4_PUBLIC PrenexQuantMode { PRENEX_QUANT_NORMAL, }; -enum CegqiFairMode { - /** enforce fairness by UF corresponding to datatypes size */ - CEGQI_FAIR_UF_DT_SIZE, - /** enforce fairness by datatypes size */ - CEGQI_FAIR_DT_SIZE, - /** enforce fairness by datatypes height bound */ - CEGQI_FAIR_DT_HEIGHT_PRED, - /** enforce fairness by datatypes size bound */ - CEGQI_FAIR_DT_SIZE_PRED, - /** do not use fair strategy for CEGQI */ - CEGQI_FAIR_NONE, -}; - enum TermDbMode { /** consider all terms in master equality engine */ TERM_DB_ALL, diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index f15723e08..2cbf15873 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -245,8 +245,6 @@ option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3 option ceGuidedInst --cegqi bool :default false :read-write counterexample-guided quantifier instantiation -option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler stringToCegqiFairMode - if and how to apply fairness for cegqi option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write mode for processing single invocation synthesis conjectures option cegqiSingleInvPartial --cegqi-si-partial bool :default false @@ -261,29 +259,31 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default include constants when reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvAbort --cegqi-si-abort bool :default false abort if synthesis conjecture is not single invocation +option sygusPbe --sygus-pbe bool :default true + sygus advanced pruning based on examples -option sygusNormalForm --sygus-nf bool :default true - only search for sygus builtin terms that are in normal form -option sygusNormalFormArg --sygus-nf-arg bool :default true - account for relationship between arguments of operations in sygus normal form -option sygusNormalFormGlobal --sygus-nf-sym bool :default true - narrow sygus search space based on global state of current candidate program -option sygusNormalFormGlobalGen --sygus-nf-sym-gen bool :default true - generalize lemmas for global search space narrowing -option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true - generalize based on arguments in global search space narrowing -option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true - generalize based on content in global search space narrowing +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 sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode template mode for sygus invariant synthesis -option sygusUnifCondSol --sygus-unif-csol bool :default false - enable approach which unifies conditional solutions +option sygusInvAutoUnfold --sygus-auto-unfold bool :default true + enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems +option sygusUnifCondSol --sygus-unif-csol bool :default true + enable new approach which unifies conditional solutions option sygusDirectEval --sygus-direct-eval bool :default true direct unfolding of evaluation functions -option sygusCRefEval --sygus-cref-eval bool :default false +option sygusUnfoldBool --sygus-unfold-bool bool :default true + do unfolding of Boolean evaluation functions that appear in refinement lemmas +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 # approach applied to general quantified formulas option cbqi --cbqi bool :read-write :default false |