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.

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