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.

1 files changed, 0 insertions, 13 deletions

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,