Merge branch 'master' of https://github.com/CVC4/CVC4.git

Conflicts:
	proofs/signatures/Makefile.am
	src/Makefile.am
	src/expr/datatype.cpp
	src/options/datatypes_options
	src/options/options_template.cpp
	src/options/quantifiers_options
	src/proof/arith_proof.cpp
	src/proof/arith_proof.h
	src/proof/array_proof.cpp
	src/proof/array_proof.h
	src/proof/bitvector_proof.cpp
	src/proof/bitvector_proof.h
	src/proof/cnf_proof.cpp
	src/proof/cnf_proof.h
	src/proof/proof_manager.cpp
	src/proof/proof_manager.h
	src/proof/sat_proof.h
	src/proof/sat_proof_implementation.h
	src/proof/skolemization_manager.h
	src/proof/theory_proof.cpp
	src/proof/theory_proof.h
	src/proof/uf_proof.cpp
	src/proof/uf_proof.h
	src/prop/cnf_stream.cpp
	src/prop/cnf_stream.h
	src/prop/minisat/core/Solver.cc
	src/prop/prop_engine.cpp
	src/prop/prop_engine.h
	src/prop/theory_proxy.cpp
	src/smt/smt_engine.cpp
	src/smt/smt_engine_check_proof.cpp
	src/theory/arrays/array_proof_reconstruction.cpp
	src/theory/arrays/theory_arrays.cpp
	src/theory/bv/eager_bitblaster.cpp
	src/theory/bv/lazy_bitblaster.cpp
	src/theory/datatypes/theory_datatypes.cpp
	src/theory/quantifiers/alpha_equivalence.cpp
	src/theory/quantifiers/candidate_generator.cpp
	src/theory/quantifiers/candidate_generator.h
	src/theory/quantifiers/ce_guided_single_inv.cpp
	src/theory/quantifiers/ceg_instantiator.cpp
	src/theory/quantifiers/conjecture_generator.cpp
	src/theory/quantifiers/equality_infer.cpp
	src/theory/quantifiers/equality_infer.h
	src/theory/quantifiers/inst_match_generator.cpp
	src/theory/quantifiers/inst_propagator.cpp
	src/theory/quantifiers/inst_propagator.h
	src/theory/quantifiers/inst_strategy_e_matching.cpp
	src/theory/quantifiers/inst_strategy_e_matching.h
	src/theory/quantifiers/instantiation_engine.cpp
	src/theory/quantifiers/model_builder.cpp
	src/theory/quantifiers/model_engine.cpp
	src/theory/quantifiers/quant_conflict_find.cpp
	src/theory/quantifiers/quant_conflict_find.h
	src/theory/quantifiers/quant_split.cpp
	src/theory/quantifiers/quant_util.cpp
	src/theory/quantifiers/quantifiers_rewriter.cpp
	src/theory/quantifiers/quantifiers_rewriter.h
	src/theory/quantifiers/term_database.cpp
	src/theory/quantifiers/term_database.h
	src/theory/quantifiers/trigger.cpp
	src/theory/quantifiers/trigger.h
	src/theory/quantifiers_engine.cpp
	src/theory/quantifiers_engine.h
	src/theory/sets/kinds
	src/theory/sets/theory_sets_private.cpp
	src/theory/sets/theory_sets_private.h
	src/theory/sets/theory_sets_rewriter.cpp
	src/theory/sets/theory_sets_type_rules.h
	src/theory/strings/theory_strings.cpp
	src/theory/strings/theory_strings.h
	src/theory/theory_engine.cpp
	src/theory/theory_engine.h
	src/theory/uf/equality_engine.cpp
	test/regress/regress0/fmf/Makefile.am
	test/regress/regress0/quantifiers/Makefile.am
	test/regress/regress0/strings/Makefile.am
	test/regress/regress0/sygus/Makefile.am
	test/regress/regress0/sygus/max2-univ.sy

13 files changed, 244 insertions, 38 deletions

diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 643932781..1eb84b45f 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -10,7 +10,7 @@
 # Step 4: Generate X_options.h from X_options.sed
 # Step 5: Generate X_options.cpp from X_options.sed.
 #   This stage also waits for X_options.h as otherwise it cannot compile.
-# 
+#
 
 OPTIONS_SRC_FILES = \
 	arith_options \
@@ -30,6 +30,7 @@ OPTIONS_SRC_FILES = \
 	proof_options \
 	prop_options \
 	quantifiers_options \
+	sep_options \
 	sets_options \
 	smt_options \
 	strings_options \
@@ -54,6 +55,7 @@ OPTIONS_TEMPS = \
 	proof_options.tmp \
 	prop_options.tmp \
 	quantifiers_options.tmp \
+	sep_options.tmp \
 	sets_options.tmp \
 	smt_options.tmp \
 	strings_options.tmp \
@@ -78,6 +80,7 @@ OPTIONS_OPTIONS_FILES = \
 	proof_options.options \
 	prop_options.options \
 	quantifiers_options.options \
+	sep_options.options \
 	sets_options.options \
 	smt_options.options \
 	strings_options.options \
@@ -102,6 +105,7 @@ OPTIONS_SEDS = \
 	proof_options.sed \
 	prop_options.sed \
 	quantifiers_options.sed \
+	sep_options.sed \
 	sets_options.sed \
 	smt_options.sed \
 	strings_options.sed \
@@ -126,6 +130,7 @@ OPTIONS_HEADS = \
 	proof_options.h \
 	prop_options.h \
 	quantifiers_options.h \
+	sep_options.h \
 	sets_options.h \
 	smt_options.h \
 	strings_options.h \
@@ -150,6 +155,7 @@ OPTIONS_CPPS = \
 	proof_options.cpp \
 	prop_options.cpp \
 	quantifiers_options.cpp \
+	sep_options.cpp \
 	sets_options.cpp \
 	smt_options.cpp \
 	strings_options.cpp \
@@ -295,14 +301,14 @@ options_holder_template.h options_template.cpp options_get_option_template.cpp o
 
 # Make sure the implicit rules never mistake X_options for the -o file for a
 # CPP file.
-arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sets_options smt_options strings_options theory_options uf_options:;
+arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sep_options sets_options smt_options strings_options theory_options uf_options:;
 
 
 # These are phony to force them to be made everytime.
-.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp
+.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp
 
 # Make is happier being listed explictly. Not sure why.
-arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp:
+arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp:
 	echo "$@" "$(@:.tmp=)"
 	$(AM_V_GEN)(cp "@srcdir@/$(@:.tmp=)" "$@" || true)
 #TIM:
@@ -424,4 +430,3 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed
 # directories that are cleaned first.  Without this rule, "distclean"
 # fails.
 %.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@"
-
diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp
index 9cf47fe33..f331345f7 100644
--- a/src/options/bv_bitblast_mode.cpp
+++ b/src/options/bv_bitblast_mode.cpp
@@ -53,4 +53,19 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) {
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode solver) {
+  switch(solver) {
+  case theory::bv::SAT_SOLVER_MINISAT:
+    out << "SAT_SOLVER_MINISAT"; 
+    break;
+  case theory::bv::SAT_SOLVER_CRYPTOMINISAT:
+    out << "SAT_SOLVER_CRYPTOMINISAT"; 
+    break;
+  default:
+    out << "SatSolverMode:UNKNOWN![" << unsigned(solver) << "]";
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */
diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 4c8c4f626..3a6474104 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -60,12 +60,19 @@ enum BvSlicerMode {
 
 };/* enum BvSlicerMode */
 
+/** Enumeration of sat solvers that can be used. */
+enum SatSolverMode {
+  SAT_SOLVER_MINISAT,
+  SAT_SOLVER_CRYPTOMINISAT,
+};/* enum SatSolver */
+
 
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 
 std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode);
 std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode);
+std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode);
 
 }/* CVC4 namespace */
 
diff --git a/src/options/bv_options b/src/options/bv_options
index 8edc809e3..2e6fa2e7a 100644
--- a/src/options/bv_options
+++ b/src/options/bv_options
@@ -7,6 +7,9 @@ module BV "options/bv_options.h" Bitvector theory
 
 # Option to set the bit-blasting mode (lazy, eager)
 
+expert-option bvSatSolver bv-sat-solver --bv-sat-solver=MODE CVC4::theory::bv::SatSolverMode :predicate satSolverEnabledBuild :handler stringToSatSolver :default CVC4::theory::bv::SAT_SOLVER_MINISAT :read-write :include "options/bv_bitblast_mode.h"
+ choose which sat solver to use, see --bv-sat-solver=help
+
 option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h"
  choose bitblasting mode, see --bitblast=help
 
diff --git a/src/options/datatypes_options b/src/options/datatypes_options
index e9578f8d7..bb92b4e05 100644
--- a/src/options/datatypes_options
+++ b/src/options/datatypes_options
@@ -27,5 +27,7 @@ option dtInferAsLemmas --dt-infer-as-lemmas bool :default false
  always send lemmas out instead of making internal inferences
 #option dtRExplainLemmas --dt-rexplain-lemmas bool :default true
 # regression explanations for datatype lemmas
+option dtBlastSplits --dt-blast-splits bool :default false
+ when applicable, blast splitting lemmas for all variables at once
  
 endmodule
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index a2809bd67..6a5f6cd39 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -254,15 +254,21 @@ last-call\n\
 const std::string OptionsHandler::s_literalMatchHelp = "\
 Literal match modes currently supported by the --literal-match option:\n\
 \n\
-none (default)\n\
+none \n\
 + Do not use literal matching.\n\
 \n\
-predicate\n\
-+ Consider the phase requirements of predicate literals when applying heuristic\n\
-  quantifier instantiation.  For example, the trigger P( x ) in the quantified \n\
-  formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
-  terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
-  Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
+use (default)\n\
++ Consider phase requirements of triggers conservatively. For example, the\n\
+  trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n\
+  terms in the equivalence class of true, and likewise Q( x ) will not be matched\n\
+  terms in the equivalence class of false. Extends to equality.\n\
+\n\
+agg-predicate \n\
++ Consider phase requirements aggressively for predicates. In the above example,\n\
+  only match P( x ) with terms that are in the equivalence class of false.\n\
+\n\
+agg \n\
++ Consider the phase requirements aggressively for all triggers.\n\
 \n\
 ";
 
@@ -384,7 +390,7 @@ uf-dt-size \n\
 + Enforce fairness using an uninterpreted function for datatypes size.\n\
 \n\
 default | dt-size \n\
-+ Default, enforce fairness using size theory operator.\n\
++ Default, enforce fairness using size operator.\n\
 \n\
 dt-height-bound \n\
 + Enforce fairness by height bound predicate.\n\
@@ -419,6 +425,24 @@ all \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_cegqiSingleInvHelp = "\
+Modes for single invocation techniques, supported by --cegqi-si:\n\
+\n\
+none  \n\
++ Do not use single invocation techniques.\n\
+\n\
+use (default) \n\
++ Use single invocation techniques only if grammar is not restrictive.\n\
+\n\
+all-abort  \n\
++ Always use single invocation techniques, abort if solution reconstruction will likely fail,\
+  for instance, when the grammar does not have ITE and solution requires it.\n\
+\n\
+all \n\
++ Always use single invocation techniques. \n\
+\n\
+";
+
 const std::string OptionsHandler::s_sygusInvTemplHelp = "\
 Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
 \n\
@@ -506,10 +530,12 @@ void OptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::
 theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg ==  "none") {
     return theory::quantifiers::LITERAL_MATCH_NONE;
-  } else if(optarg ==  "predicate") {
-    return theory::quantifiers::LITERAL_MATCH_PREDICATE;
-  } else if(optarg ==  "equality") {
-    return theory::quantifiers::LITERAL_MATCH_EQUALITY;
+  } else if(optarg ==  "use") {
+    return theory::quantifiers::LITERAL_MATCH_USE;
+  } else if(optarg ==  "agg-predicate") {
+    return theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE;
+  } else if(optarg ==  "agg") {
+    return theory::quantifiers::LITERAL_MATCH_AGG;
   } else if(optarg ==  "help") {
     puts(s_literalMatchHelp.c_str());
     exit(1);
@@ -520,9 +546,7 @@ theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(s
 }
 
 void OptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) {
-  if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) {
-    throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
-  }
+
 }
 
 theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) {
@@ -651,6 +675,8 @@ theory::quantifiers::CegqiFairMode OptionsHandler::stringToCegqiFairMode(std::st
     return theory::quantifiers::CEGQI_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;
   } else if(optarg == "none") {
     return theory::quantifiers::CEGQI_FAIR_NONE;
   } else if(optarg ==  "help") {
@@ -692,6 +718,24 @@ theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(s
   }
 }
 
+theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "none" ) {
+    return theory::quantifiers::CEGQI_SI_MODE_NONE;
+  } else if(optarg == "use" || optarg == "default") {
+    return theory::quantifiers::CEGQI_SI_MODE_USE;
+  } else if(optarg == "all-abort") {
+    return theory::quantifiers::CEGQI_SI_MODE_ALL_ABORT;
+  } else if(optarg == "all") {
+    return theory::quantifiers::CEGQI_SI_MODE_ALL;
+  } else if(optarg ==  "help") {
+    puts(s_cegqiSingleInvHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --cegqi-si: `") +
+                          optarg + "'.  Try --cegqi-si help.");
+  }
+}
+
 theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "none" ) {
     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE;
@@ -777,6 +821,72 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) thro
 #endif /* CVC4_USE_ABC */
 }
 
+void OptionsHandler::satSolverEnabledBuild(std::string option,
+                                           bool value) throw(OptionException) {
+#ifndef CVC4_USE_CRYPTOMINISAT
+  if(value) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_USE_CRYPTOMINISAT */
+}
+
+void OptionsHandler::satSolverEnabledBuild(std::string option,
+                                           std::string value) throw(OptionException) {
+#ifndef CVC4_USE_CRYPTOMINISAT
+  if(!value.empty()) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_USE_CRYPTOMINISAT */
+}
+
+const std::string OptionsHandler::s_bvSatSolverHelp = "\
+Sat solvers currently supported by the --bv-sat-solver option:\n\
+\n\
+minisat (default)\n\
+\n\
+cryptominisat\n\
+";
+
+theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
+                                                            std::string optarg) throw(OptionException) {
+  if(optarg == "minisat") {
+    return theory::bv::SAT_SOLVER_MINISAT;
+  } else if(optarg == "cryptominisat") {
+    
+    if (options::incrementalSolving() &&
+        options::incrementalSolving.wasSetByUser()) {
+      throw OptionException(std::string("Cryptominsat does not support incremental mode. \n\
+                                         Try --bv-sat-solver=minisat"));
+    }
+
+    if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
+        options::bitblastMode.wasSetByUser()) {
+      throw OptionException(std::string("Cryptominsat does not support lazy bit-blsating. \n\
+                                         Try --bv-sat-solver=minisat"));
+    }
+    if (!options::bitvectorToBool.wasSetByUser()) {
+      options::bitvectorToBool.set(true);
+    }
+
+    // if (!options::bvAbstraction.wasSetByUser() &&
+    //     !options::skolemizeArguments.wasSetByUser()) {
+    //   options::bvAbstraction.set(true);
+    //   options::skolemizeArguments.set(true); 
+    // }
+    return theory::bv::SAT_SOLVER_CRYPTOMINISAT;
+  } else if(optarg == "help") {
+    puts(s_bvSatSolverHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --bv-sat-solver: `") +
+                          optarg + "'.  Try --bv-sat-solver=help.");
+  }
+}
+
 const std::string OptionsHandler::s_bitblastingModeHelp = "\
 Bit-blasting modes currently supported by the --bitblast option:\n\
 \n\
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index baa6cea96..5db2887c0 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -98,6 +98,7 @@ public:
   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);
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException);
@@ -106,10 +107,15 @@ public:
   // theory/bv/options_handlers.h
   void abcEnabledBuild(std::string option, bool value) throw(OptionException);
   void abcEnabledBuild(std::string option, std::string value) throw(OptionException);
+  void satSolverEnabledBuild(std::string option, bool value) throw(OptionException);
+  void satSolverEnabledBuild(std::string option, std::string optarg) throw(OptionException);
+
   theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException);
   theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException);
   void setBitblastAig(std::string option, bool arg) throw(OptionException);
 
+  theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException);
+    
 
   // theory/booleans/options_handlers.h
   theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException);
@@ -192,6 +198,7 @@ public:
 
   /* Help strings */
   static const std::string s_bitblastingModeHelp;
+  static const std::string s_bvSatSolverHelp;
   static const std::string s_booleanTermConversionModeHelp;
   static const std::string s_bvSlicerModeHelp;
   static const std::string s_cegqiFairModeHelp;
@@ -209,6 +216,7 @@ public:
   static const std::string s_qcfModeHelp;
   static const std::string s_qcfWhenModeHelp;
   static const std::string s_simplificationHelp;
+  static const std::string s_cegqiSingleInvHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_termDbModeHelp;
   static const std::string s_theoryOfModeHelp;
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index f029dfd17..694d46d31 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -720,7 +720,7 @@ void Options::parseOptionsRecursive(Options* options,
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 722 "${template}"
+#line 724 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
@@ -798,7 +798,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th
 
 static const char* smtOptions[] = {
   ${all_modules_smt_options},
-#line 800 "${template}"
+#line 802 "${template}"
   NULL
 };/* smtOptions[] */
 
@@ -820,7 +820,7 @@ std::vector< std::vector<std::string> > Options::getOptions() const throw() {
 
   ${all_modules_get_options}
 
-#line 762 "${template}"
+#line 824 "${template}"
 
   return opts;
 }
diff --git a/src/options/proof_options b/src/options/proof_options
index 7feb00b0d..a99d858bc 100644
--- a/src/options/proof_options
+++ b/src/options/proof_options
@@ -5,4 +5,7 @@
 
 module PROOF "options/proof_options.h" Proof
 
+option lfscLetification --lfsc-letification bool :default true
+ turns on global letification in LFSC proofs
+
 endmodule
diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp
index a58120974..e2cd78de5 100644
--- a/src/options/quantifiers_modes.cpp
+++ b/src/options/quantifiers_modes.cpp
@@ -46,11 +46,14 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod
   case theory::quantifiers::LITERAL_MATCH_NONE:
     out << "LITERAL_MATCH_NONE";
     break;
-  case theory::quantifiers::LITERAL_MATCH_PREDICATE:
-    out << "LITERAL_MATCH_PREDICATE";
+  case theory::quantifiers::LITERAL_MATCH_USE:
+    out << "LITERAL_MATCH_USE";
     break;
-  case theory::quantifiers::LITERAL_MATCH_EQUALITY:
-    out << "LITERAL_MATCH_EQUALITY";
+  case theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE:
+    out << "LITERAL_MATCH_AGG_PREDICATE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_AGG:
+    out << "LITERAL_MATCH_AGG";
     break;
   default:
     out << "LiteralMatchMode!UNKNOWN";
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 5749da972..65445be17 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -44,10 +44,12 @@ enum InstWhenMode {
 enum LiteralMatchMode {
   /** Do not consider polarity of patterns */
   LITERAL_MATCH_NONE,
-  /** Consider polarity of boolean predicates only */
-  LITERAL_MATCH_PREDICATE,
-  /** Consider polarity of boolean predicates, as well as equalities */
-  LITERAL_MATCH_EQUALITY,
+  /** Conservatively consider polarity of patterns */
+  LITERAL_MATCH_USE,
+  /** Aggressively consider polarity of Boolean predicates */
+  LITERAL_MATCH_AGG_PREDICATE,
+  /** Aggressively consider polarity of all terms */
+  LITERAL_MATCH_AGG,
 };
 
 enum MbqiMode {
@@ -129,6 +131,8 @@ enum CegqiFairMode {
   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,
 };
@@ -149,6 +153,17 @@ enum IteLiftQuantMode {
   ITE_LIFT_QUANT_MODE_ALL,
 };
 
+enum CegqiSingleInvMode {
+  /** do not use single invocation techniques */
+  CEGQI_SI_MODE_NONE,
+  /** use single invocation techniques */
+  CEGQI_SI_MODE_USE,
+  /** always use single invocation techniques, abort if solution reconstruction will fail */
+  CEGQI_SI_MODE_ALL_ABORT,
+  /** always use single invocation techniques */
+  CEGQI_SI_MODE_ALL,
+};
+
 enum SygusInvTemplMode {
   /** synthesize I( x ) */
   SYGUS_INV_TEMPL_MODE_NONE,
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 74b3011a6..4d228bbad 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -54,6 +54,8 @@ option purifyQuant --purify-quant bool :default false
  purify quantified formulas
 option elimExtArithQuant --elim-ext-arith-quant bool :default true
  eliminate extended arithmetic symbols in quantified formulas
+option condRewriteQuant --cond-rewrite-quant bool :default true
+ conditional rewriting of quantified formulas
  
 #### E-matching options
  
@@ -109,6 +111,8 @@ option instLevelInputOnly --inst-level-input-only bool :default true
  only input terms are assigned instantiation level zero
 option quantRepMode --quant-rep-mode=MODE  CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode
  selection mode for representatives in quantifiers engine
+option instRelevantCond --inst-rlv-cond bool :default false
+ add relevancy conditions for instantiations
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
@@ -120,7 +124,7 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
 option fullSaturateInst --fs-inst bool :default false
  interleave full saturate instantiation with other techniques
 
-option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_USE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
  choose literal matching mode
 
 ### finite model finding options
@@ -144,7 +148,7 @@ option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default fa
 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
  only add instantiations for one quantifier per round for mbqi
 
-option fmfInstEngine --fmf-inst-engine bool :default false
+option fmfInstEngine --fmf-inst-engine bool :default false :read-write
  use instantiation engine in conjunction with finite model finding
 option fmfInstGen --fmf-inst-gen bool :default true
  enable Inst-Gen instantiation techniques for finite model finding 
@@ -171,13 +175,23 @@ option qcfTConstraint --qcf-tconstraint bool :read-write :default false
  enable entailment checks for t-constraints in qcf algorithm
 option qcfAllConflict --qcf-all-conflict bool :read-write :default false
  add all available conflicting instances during conflict-based instantiation
+option qcfNestedConflict --qcf-nested-conflict bool :default false
+ consider conflicts for nested quantifiers
+option qcfVoExp --qcf-vo-exp bool :default false
+ qcf experimental variable ordering
+ 
+ 
 
 option instNoEntail --inst-no-entail bool :read-write :default true
  do not consider instances of quantified formulas that are currently entailed
 
-option instPropagate --inst-propagate bool :read-write :default false
+option instPropagate --inst-prop bool :read-write :default false
  internal propagation for instantiations for selecting relevant instances
  
+option qcfEagerTest --qcf-eager-test bool :default true
+ optimization, test qcf instances eagerly
+option qcfSkipRd --qcf-skip-rd bool :default false
+ optimization, skip instances based on possibly irrelevant portions of quantified formulas
 ### rewrite rules options 
  
 option quantRewriteRules --rewrite-rules bool :default false
@@ -219,8 +233,8 @@ 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 cegqiSingleInv --cegqi-si bool :default false :read-write
-  process single invocation synthesis conjectures
+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
   combined techniques for synthesis conjectures that are partially single invocation 
 option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
@@ -229,8 +243,6 @@ 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 cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
-  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
@@ -248,6 +260,9 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
 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 sygusDirectEval --sygus-direct-eval bool :default true
+  direct unfolding of evaluation functions
+  
 # approach applied to general quantified formulas
 option cbqiSplx --cbqi-splx bool :read-write :default false
  turns on old implementation of counterexample-based quantifier instantiation
diff --git a/src/options/sep_options b/src/options/sep_options
new file mode 100644
index 000000000..043355bda
--- /dev/null
+++ b/src/options/sep_options
@@ -0,0 +1,20 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module SEP "options/sep_options.h" Sep
+
+option sepCheckNeg --sep-check-neg bool :default true
+ check negated spatial assertions
+
+option sepExp --sep-exp bool :default false
+ experimental flag for sep
+option sepMinimalRefine --sep-min-refine bool :default false
+ only add refinement lemmas for minimal (innermost) assertions
+option sepPreciseBound --sep-prec-bound bool :default false
+ calculate precise bounds for labels
+option sepDisequalC --sep-deq-c bool :default true
+ assume cardinality elements are distinct
+
+endmodule