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

Conflicts:
	src/options/quantifiers_options

7 files changed, 96 insertions, 82 deletions

diff --git a/src/options/didyoumean.cpp b/src/options/didyoumean.cpp
index d874c7bc7..693764b37 100644
--- a/src/options/didyoumean.cpp
+++ b/src/options/didyoumean.cpp
@@ -32,45 +32,42 @@ std::vector<std::string> DidYouMean::getMatch(std::string input) {
   const int similarityThreshold = 7;
   const unsigned numMatchesThreshold = 10;
 
-  std::set< std::pair<int, std::string> > scores;
+  typedef std::set<std::pair<int, std::string> > ScoreSet;
+  ScoreSet scores;
   std::vector<std::string> ret;
-  for(typeof(d_words.begin()) it = d_words.begin(); it != d_words.end(); ++it) {
+  for (Words::const_iterator it = d_words.begin(); it != d_words.end(); ++it) {
     std::string s = (*it);
-    if( s == input ) {
+    if (s == input) {
       // if input matches AS-IS just return that
       ret.push_back(s);
       return ret;
     }
     int score;
-    if(s.compare(0, input.size(), input) == 0) {
+    if (s.compare(0, input.size(), input) == 0) {
       score = 0;
     } else {
       score = editDistance(input, s) + 1;
     }
-    scores.insert( make_pair(score, s) );
+    scores.insert(make_pair(score, s));
   }
   int min_score = scores.begin()->first;
-  for(typeof(scores.begin()) i = scores.begin();
-      i != scores.end(); ++i) {
-
+  for (ScoreSet::const_iterator i = scores.begin(); i != scores.end(); ++i) {
     // add if score is overall not too big, and also not much close to
     // the score of the best suggestion
-    if(i->first < similarityThreshold && i->first <= min_score + 1) {
+    if (i->first < similarityThreshold && i->first <= min_score + 1) {
       ret.push_back(i->second);
 #ifdef DIDYOUMEAN_DEBUG
       cout << i->second << ": " << i->first << std::endl;
 #endif
     }
   }
-  if(ret.size() > numMatchesThreshold ){
+  if (ret.size() > numMatchesThreshold) {
     ret.resize(numMatchesThreshold);
   }
   return ret;
 }
 
-
-int DidYouMean::editDistance(const std::string& a, const std::string& b)
-{
+int DidYouMean::editDistance(const std::string& a, const std::string& b) {
   // input string: a
   // desired string: b
 
@@ -86,44 +83,42 @@ int DidYouMean::editDistance(const std::string& a, const std::string& b)
   int* C[3];
   int ii;
   for (ii = 0; ii < 3; ++ii) {
-    C[ii] = new int[len2+1];
+    C[ii] = new int[len2 + 1];
   }
   //  int C[3][len2+1];             // cost
 
-  for(int j = 0; j <= len2; ++j) {
+  for (int j = 0; j <= len2; ++j) {
     C[0][j] = j * addCost;
   }
 
-  for(int i = 1; i <= len1; ++i) {
-
-    int cur = i%3;
-    int prv = (i+2)%3;
-    int pr2 = (i+1)%3;
+  for (int i = 1; i <= len1; ++i) {
+    int cur = i % 3;
+    int prv = (i + 2) % 3;
+    int pr2 = (i + 1) % 3;
 
     C[cur][0] = i * deleteCost;
 
-    for(int j = 1; j <= len2; ++j) {
-
-      C[cur][j] = 100000000;      // INF
+    for (int j = 1; j <= len2; ++j) {
+      C[cur][j] = 100000000;  // INF
 
-      if(a[i-1] == b[j-1]) {
+      if (a[i - 1] == b[j - 1]) {
         // match
-        C[cur][j] = std::min(C[cur][j], C[prv][j-1]);
-      } else if(tolower(a[i-1]) == tolower(b[j-1])){
+        C[cur][j] = std::min(C[cur][j], C[prv][j - 1]);
+      } else if (tolower(a[i - 1]) == tolower(b[j - 1])) {
         // switch case
-        C[cur][j] = std::min(C[cur][j], C[prv][j-1] + switchCaseCost);
+        C[cur][j] = std::min(C[cur][j], C[prv][j - 1] + switchCaseCost);
       } else {
         // substitute
-        C[cur][j] = std::min(C[cur][j], C[prv][j-1] + substituteCost);
+        C[cur][j] = std::min(C[cur][j], C[prv][j - 1] + substituteCost);
       }
 
       // swap
-      if(i >= 2 && j >= 2 && a[i-1] == b[j-2] && a[i-2] == b[j-1]) {
-        C[cur][j] = std::min(C[cur][j], C[pr2][j-2] + swapCost);
+      if (i >= 2 && j >= 2 && a[i - 1] == b[j - 2] && a[i - 2] == b[j - 1]) {
+        C[cur][j] = std::min(C[cur][j], C[pr2][j - 2] + swapCost);
       }
 
       // add
-      C[cur][j] = std::min(C[cur][j], C[cur][j-1] + addCost);
+      C[cur][j] = std::min(C[cur][j], C[cur][j - 1] + addCost);
 
       // delete
       C[cur][j] = std::min(C[cur][j], C[prv][j] + deleteCost);
@@ -132,31 +127,35 @@ int DidYouMean::editDistance(const std::string& a, const std::string& b)
       std::cout << "C[" << cur << "][" << 0 << "] = " << C[cur][0] << std::endl;
 #endif
     }
-
   }
-  int result = C[len1%3][len2];
+  int result = C[len1 % 3][len2];
   for (ii = 0; ii < 3; ++ii) {
-    delete [] C[ii];
+    delete[] C[ii];
   }
   return result;
 }
 
-std::string DidYouMean::getMatchAsString(std::string input, int prefixNewLines, int suffixNewLines) {
+std::string DidYouMean::getMatchAsString(std::string input, int prefixNewLines,
+                                         int suffixNewLines) {
   std::vector<std::string> matches = getMatch(input);
   std::ostringstream oss;
-  if(matches.size() > 0) {
-    while(prefixNewLines --> 0) { oss << std::endl; }
-    if(matches.size() == 1) {
+  if (matches.size() > 0) {
+    while (prefixNewLines-- > 0) {
+      oss << std::endl;
+    }
+    if (matches.size() == 1) {
       oss << "Did you mean this?";
     } else {
       oss << "Did you mean any of these?";
     }
-    for(unsigned i = 0; i < matches.size(); ++i) {
+    for (unsigned i = 0; i < matches.size(); ++i) {
       oss << "\n        " << matches[i];
     }
-    while(suffixNewLines --> 0) { oss << std::endl; }
+    while (suffixNewLines-- > 0) {
+      oss << std::endl;
+    }
   }
   return oss.str();
 }
 
-}/* CVC4 namespace */
+} /* CVC4 namespace */
diff --git a/src/options/didyoumean.h b/src/options/didyoumean.h
index 71a12e6fc..31b58aadb 100644
--- a/src/options/didyoumean.h
+++ b/src/options/didyoumean.h
@@ -19,25 +19,22 @@
 
 #pragma once
 
-#include <vector>
 #include <set>
 #include <string>
+#include <vector>
 
 namespace CVC4 {
 
 class DidYouMean {
+ public:
   typedef std::set<std::string> Words;
-  Words d_words;
 
-public:
   DidYouMean() {}
   ~DidYouMean() {}
 
   DidYouMean(Words words) : d_words(words) {}
 
-  void addWord(std::string word) {
-    d_words.insert(word);
-  }
+  void addWord(std::string word) { d_words.insert(word); }
 
   std::vector<std::string> getMatch(std::string input);
 
@@ -45,9 +42,12 @@ public:
    * This is provided to make it easier to ensure consistency of
    * output. Returned string is empty if there are no matches.
    */
-  std::string getMatchAsString(std::string input, int prefixNewLines = 2, int suffixNewLines = 0);
-private:
+  std::string getMatchAsString(std::string input, int prefixNewLines = 2,
+                               int suffixNewLines = 0);
+
+ private:
   int editDistance(const std::string& a, const std::string& b);
+  Words d_words;
 };
 
-}/*CVC4 namespace*/
+} /*CVC4 namespace*/
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 8cd651da5..1d7355d9f 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -385,15 +385,18 @@ max \n\
 const std::string OptionsHandler::s_prenexQuantModeHelp = "\
 Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
 \n\
-default \n\
-+ Default, prenex all nested quantifiers except those with user patterns.\n\
-\n\
-all \n\
-+ Prenex all nested quantifiers.\n\
-\n\
 none \n\
 + Do no prenex nested quantifiers. \n\
 \n\
+default | simple \n\
++ Default, do simple prenexing of same sign quantifiers.\n\
+\n\
+dnorm \n\
++ Prenex to disjunctive prenex normal form.\n\
+\n\
+norm \n\
++ Prenex to prenex normal form.\n\
+\n\
 ";
 
 const std::string OptionsHandler::s_cegqiFairModeHelp = "\
@@ -679,12 +682,14 @@ theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveS
 }
 
 theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) {
-  if(optarg ==  "default" ) {
-    return theory::quantifiers::PRENEX_NO_USER_PAT;
-  } else if(optarg == "all") {
-    return theory::quantifiers::PRENEX_ALL;
+  if(optarg== "default" || optarg== "simple" ) {
+    return theory::quantifiers::PRENEX_QUANT_SIMPLE;
   } else if(optarg == "none") {
-    return theory::quantifiers::PRENEX_NONE;
+    return theory::quantifiers::PRENEX_QUANT_NONE;
+  } else if(optarg == "dnorm") {
+    return theory::quantifiers::PRENEX_QUANT_DISJ_NORMAL;
+  } else if(optarg == "norm") {
+    return theory::quantifiers::PRENEX_QUANT_NORMAL;
   } else if(optarg ==  "help") {
     puts(s_prenexQuantModeHelp.c_str());
     exit(1);
diff --git a/src/options/proof_options b/src/options/proof_options
index 322ef5a9c..789513334 100644
--- a/src/options/proof_options
+++ b/src/options/proof_options
@@ -12,6 +12,9 @@ option aggressiveCoreMin --aggressive-core-min bool :default false
  turns on aggressive unsat core minimization (experimental)
 
 option fewerPreprocessingHoles --fewer-preprocessing-holes bool :default false :read-write
-  try to eliminate preprocessing holes in proofs
+ try to eliminate preprocessing holes in proofs
+
+option allowEmptyDependencies --allow-empty-dependencies bool :default false
+ if unable to track the dependencies of a rewritten/preprocessed assertion, fail silently
 
 endmodule
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index fe76f8798..cc6abaa8b 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -123,12 +123,14 @@ enum TriggerActiveSelMode {
 };
 
 enum CVC4_PUBLIC PrenexQuantMode {
-  /** default : prenex quantifiers without user patterns */
-  PRENEX_NO_USER_PAT,
-  /** prenex all */
-  PRENEX_ALL,
-  /** prenex none */
-  PRENEX_NONE,
+  /** do not prenex */
+  PRENEX_QUANT_NONE,
+  /** prenex same sign quantifiers */
+  PRENEX_QUANT_SIMPLE,
+  /** aggressive prenex, disjunctive prenex normal form */
+  PRENEX_QUANT_DISJ_NORMAL,
+  /** prenex normal form */
+  PRENEX_QUANT_NORMAL,
 };
 
 enum CegqiFairMode {
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 7536d385d..3269b7574 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -17,10 +17,12 @@ option miniscopeQuant --miniscope-quant bool :default true :read-write
 # ( forall x. P( x ) ) V Q
 option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  miniscope quantifiers for ground subformulas
-option quantSplit --quant-split bool :default true
+option quantSplit --quant-split bool :default true :read-write
  apply splitting to quantified formulas based on variable disjoint disjuncts
-option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode
+option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode
  prenex mode for quantified formulas
+option prenexQuantUser --prenex-quant-user bool :default false :read-write
+ prenex quantified formulas with user patterns
 # Whether to variable-eliminate quantifiers.
 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
 #   forall y. P( c, y )
@@ -45,7 +47,7 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal
 option preSkolemQuant --pre-skolem-quant bool :read-write :default false
  apply skolemization eagerly to bodies of quantified formulas
 option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true
- apply skolemization to nested quantified formulass
+ apply skolemization to nested quantified formulas
 option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
  apply skolemization to quantified formulas aggressively
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
@@ -115,9 +117,6 @@ option quantRepMode --quant-rep-mode=MODE  CVC4::theory::quantifiers::QuantRepMo
  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
 
 option fullSaturateQuant --full-saturate-quant bool :default false :read-write
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
@@ -183,8 +182,6 @@ 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
@@ -194,8 +191,11 @@ option instPropagate --inst-prop bool :read-write :default false
  
 option qcfEagerTest --qcf-eager-test bool :default true
  optimization, test qcf instances eagerly
+option qcfEagerCheckRd --qcf-eager-check-rd bool :default true
+ optimization, eagerly check relevant domain of matched position
 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
@@ -272,8 +272,6 @@ 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
 option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
 option recurseCbqi --cbqi-recurse bool :default true
@@ -292,14 +290,23 @@ option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false
   preregister ground instantiations in counterexample-based quantifier instantiation
 option cbqiMinBounds --cbqi-min-bounds bool :default false
   use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
-option cbqiSymLia --cbqi-sym-lia bool :default false
-  use symbolic integer division in substitutions for counterexample-based quantifier instantiation
 option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false
   round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
 option cbqiMidpoint --cbqi-midpoint bool :default false
   choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation
 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 :default false
+ process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation
+ 
+option quantEpr --quant-epr bool :default false :read-write
+ infer whether in effectively propositional fragment, use for cbqi
+option quantEprMatching --quant-epr-match bool :default true
+ use matching heuristics for EPR instantiation
  
 ### local theory extensions options 
 
diff --git a/src/options/sep_options b/src/options/sep_options
index 043355bda..fecf4401e 100644
--- a/src/options/sep_options
+++ b/src/options/sep_options
@@ -12,8 +12,6 @@ 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