Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

5 files changed, 316 insertions, 27 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index f009bbbbe..86a43c878 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -438,7 +438,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
   d_tester = em->mkVar(d_name.substr(d_name.find('\0') + 1), em->mkTesterType(self));
   d_name.resize(d_name.find('\0'));
   d_constructor = em->mkVar(d_name, em->mkConstructorType(*this, self));
-  //associate constructor with all selectors
+  // associate constructor with all selectors
   for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
     (*i).d_constructor = d_constructor;
   }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index d39d7110d..b701073c7 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -361,9 +361,9 @@ public:
  *
  * Datatypes may also be defined parametrically, such as this example:
  *
- *  DATATYPE

- *    list[T] = cons(car : T, cdr : list[T]) | null,

- *    tree = node(children : list[tree]) | leaf

+ *  DATATYPE
+ *    list[T] = cons(car : T, cdr : list[T]) | null,
+ *    tree = node(children : list[tree]) | leaf
  *  END;
  * 
  * Here, the definition of the parametric datatype list, where T is a type variable.
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 9d2524170..9a4fc8dc2 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -79,23 +79,30 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   }
 
   // If not an ITE, go deep
-  vector<Node> newChildren;
-  bool somethingChanged = false;
-  if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    newChildren.push_back(node.getOperator());
-  }
-  // Remove the ITEs from the children
-  for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-    Node newChild = run(*it, output, iteSkolemMap);
-    somethingChanged |= (newChild != *it);
-    newChildren.push_back(newChild);
-  }
+  if( node.getKind() != kind::FORALL &&
+      node.getKind() != kind::EXISTS &&
+      node.getKind() != kind::REWRITE_RULE ) {
+    vector<Node> newChildren;
+    bool somethingChanged = false;
+    if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      newChildren.push_back(node.getOperator());
+    }
+    // Remove the ITEs from the children
+    for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+      Node newChild = run(*it, output, iteSkolemMap);
+      somethingChanged |= (newChild != *it);
+      newChildren.push_back(newChild);
+    }
 
-  // If changes, we rewrite
-  if(somethingChanged) {
-    cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
-    nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite);
-    return cachedRewrite;
+    // If changes, we rewrite
+    if(somethingChanged) {
+      cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
+      nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite);
+      return cachedRewrite;
+    } else {
+      nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
+      return node;
+    }
   } else {
     nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
     return node;
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 26881e052..1296fa5af 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -130,6 +130,25 @@ Options::Options() :
   arithRewriteEqSetByUser(false),
   ufSymmetryBreaker(false),
   ufSymmetryBreakerSetByUser(false),
+  miniscopeQuant(true),
+  miniscopeQuantFreeVar(true),
+  prenexQuant(true),
+  varElimQuant(false),
+  cnfQuant(false),
+  preSkolemQuant(false),
+  smartTriggers(true),
+  registerQuantBodyTerms(false),
+  instWhenMode(INST_WHEN_FULL_LAST_CALL),
+  eagerInstQuant(false),
+  finiteModelFind(false),
+  fmfRegionSat(false),
+  fmfModelBasedInst(true),
+  efficientEMatching(false),
+  literalMatchMode(LITERAL_MATCH_NONE),
+  cbqi(false),
+  cbqiSetByUser(false),
+  userPatternsQuant(true),
+  flipDecision(false),
   lemmaOutputChannel(NULL),
   lemmaInputChannel(NULL),
   threads(2),// default should be 1 probably, but say 2 for now
@@ -240,6 +259,27 @@ Additional CVC4 options:\n\
    --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\
                           CADE 2011) [on by default only for QF_UF]\n\
    --disable-symmetry-breaker turns off UF symmetry breaker\n\
+   --disable-miniscope-quant     disable miniscope quantifiers\n\
+   --disable-miniscope-quant-fv  disable miniscope quantifiers for ground subformulas\n\
+   --disable-prenex-quant disable prenexing of quantified formulas\n\
+   --var-elim-quant       enable variable elimination of quantified formulas\n\
+   --cnf-quant            apply CNF conversion to quantified formulas\n\
+   --pre-skolem-quant     apply skolemization eagerly to bodies of quantified formulas\n\
+   --disable-smart-triggers   disable smart triggers\n\
+   --register-quant-body-terms  consider terms within bodies of quantified formulas for matching\n\
+   --inst-when=MODE       when to apply instantiation\n\
+   --eager-inst-quant     apply quantifier instantiation eagerly\n\
+   --finite-model-find    use finite model finding heuristic for quantifier instantiation\n\
+   --use-fmf-region-sat   use region-based SAT heuristic for finite model finding\n\
+   --disable-fmf-model-inst  disable model-based instantiation for finite model finding\n\
+   --efficient-e-matching use efficient E-matching\n\
+   --literal-matching=MODE  choose literal matching mode\n\
+   --enable-cbqi          turns on counterexample-based quantifier instantiation [off by default]\n\
+   --disable-cbqi         turns off counterexample-based quantifier instantiation\n\
+   --ignore-user-patterns ignore user-provided patterns for quantifier instantiation\n\
+   --enable-flip-decision turns on flip decision heuristic\n\
+   --disable-dio-solver   turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
+   --disable-arith-rewrite-equalities   turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\
    --threads=N            sets the number of solver threads\n\
    --threadN=string       configures thread N (0..#threads-1)\n\
    --filter-lemma-length=N don't share lemmas strictly longer than N\n\
@@ -439,7 +479,7 @@ void Options::printLanguageHelp(std::ostream& out) {
  */
 enum OptionValue {
   OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */
-  SMTCOMP, 
+  SMTCOMP,
   STATS,
   SEGV_NOSPIN,
   OUTPUT_LANGUAGE,
@@ -496,6 +536,25 @@ enum OptionValue {
   DISABLE_ARITHMETIC_REWRITE_EQUALITIES,
   ENABLE_SYMMETRY_BREAKER,
   DISABLE_SYMMETRY_BREAKER,
+  DISABLE_MINISCOPE_QUANT,
+  DISABLE_MINISCOPE_QUANT_FV,
+  DISABLE_PRENEX_QUANT,
+  VAR_ELIM_QUANT,
+  CNF_QUANT,
+  PRE_SKOLEM_QUANT,
+  DISABLE_SMART_TRIGGERS,
+  REGISTER_QUANT_BODY_TERMS,
+  INST_WHEN,
+  EAGER_INST_QUANT,
+  FINITE_MODEL_FIND,
+  FMF_REGION_SAT,
+  DISABLE_FMF_MODEL_BASED_INST,
+  EFFICIENT_E_MATCHING,
+  LITERAL_MATCHING,
+  ENABLE_CBQI,
+  DISABLE_CBQI,
+  IGNORE_USER_PATTERNS,
+  ENABLE_FLIP_DECISION,
   PARALLEL_THREADS,
   PARALLEL_SEPARATE_OUTPUT,
   PORTFOLIO_FILTER_LENGTH,
@@ -602,6 +661,25 @@ static struct option cmdlineOptions[] = {
   { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES },
   { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER },
   { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
+  { "disable-miniscope-quant", no_argument, NULL, DISABLE_MINISCOPE_QUANT },
+  { "disable-miniscope-quant-fv", no_argument, NULL, DISABLE_MINISCOPE_QUANT_FV },
+  { "disable-prenex-quant", no_argument, NULL, DISABLE_PRENEX_QUANT },
+  { "var-elim-quant", no_argument, NULL, VAR_ELIM_QUANT },
+  { "cnf-quant", no_argument, NULL, CNF_QUANT },
+  { "pre-skolem-quant", no_argument, NULL, PRE_SKOLEM_QUANT },
+  { "disable-smart-triggers", no_argument, NULL, DISABLE_SMART_TRIGGERS },
+  { "register-quant-body-terms", no_argument, NULL, REGISTER_QUANT_BODY_TERMS },
+  { "inst-when", required_argument, NULL, INST_WHEN },
+  { "eager-inst-quant", no_argument, NULL, EAGER_INST_QUANT },
+  { "finite-model-find", no_argument, NULL, FINITE_MODEL_FIND },
+  { "use-fmf-region-sat", no_argument, NULL, FMF_REGION_SAT },
+  { "disable-fmf-model-inst", no_argument, NULL, DISABLE_FMF_MODEL_BASED_INST },
+  { "efficient-e-matching", no_argument, NULL, EFFICIENT_E_MATCHING },
+  { "literal-matching", required_argument, NULL, LITERAL_MATCHING },
+  { "enable-cbqi", no_argument, NULL, ENABLE_CBQI },
+  { "disable-cbqi", no_argument, NULL, DISABLE_CBQI },
+  { "ignore-user-patterns", no_argument, NULL, IGNORE_USER_PATTERNS },
+  { "enable-flip-decision", no_argument, NULL, ENABLE_FLIP_DECISION },
   { "threads", required_argument, NULL, PARALLEL_THREADS },
   { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT },
   { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH },
@@ -984,7 +1062,7 @@ throw(OptionException) {
     case 'm':
       produceModels = true;
       break;
-      
+
     case PRODUCE_ASSIGNMENTS:
       produceAssignments = true;
       break;
@@ -1016,7 +1094,7 @@ throw(OptionException) {
       throw OptionException("This is not a proof-enabled build of CVC4; --proof cannot be used");
 #endif /* CVC4_PROOF */
       break;
-      
+
     case NO_TYPE_CHECKING:
       typeChecking = false;
       earlyTypeChecking = false;
@@ -1073,7 +1151,91 @@ throw(OptionException) {
       ufSymmetryBreaker = false;
       ufSymmetryBreakerSetByUser = true;
       break;
-
+    case DISABLE_MINISCOPE_QUANT:
+      miniscopeQuant = false;
+      break;
+    case DISABLE_MINISCOPE_QUANT_FV:
+      miniscopeQuantFreeVar = false;
+      break;
+    case DISABLE_PRENEX_QUANT:
+      prenexQuant = false;
+      break;
+    case VAR_ELIM_QUANT:
+      varElimQuant = true;
+      break;
+    case CNF_QUANT:
+      cnfQuant = true;
+      break;
+    case PRE_SKOLEM_QUANT:
+      preSkolemQuant = true;
+      break;
+    case DISABLE_SMART_TRIGGERS:
+      smartTriggers = false;
+      break;
+    case REGISTER_QUANT_BODY_TERMS:
+      registerQuantBodyTerms = true;
+      break;
+    case INST_WHEN:
+      if(!strcmp(optarg, "pre-full")) {
+        instWhenMode = INST_WHEN_PRE_FULL;
+      } else if(!strcmp(optarg, "full")) {
+        instWhenMode = INST_WHEN_FULL;
+      } else if(!strcmp(optarg, "full-last-call")) {
+        instWhenMode = INST_WHEN_FULL_LAST_CALL;
+      } else if(!strcmp(optarg, "last-call")) {
+        instWhenMode = INST_WHEN_LAST_CALL;
+      } else if(!strcmp(optarg, "help")) {
+        //puts(instWhenHelp.c_str());
+        exit(1);
+      } else {
+        throw OptionException(string("unknown option for --inst-when: `") +
+                              optarg + "'.  Try --inst-when help.");
+      }
+      break;
+    case EAGER_INST_QUANT:
+      eagerInstQuant = true;
+      break;
+    case FINITE_MODEL_FIND:
+      finiteModelFind = true;
+      break;
+    case FMF_REGION_SAT:
+      fmfRegionSat = true;
+      break;
+    case DISABLE_FMF_MODEL_BASED_INST:
+      fmfModelBasedInst = false;
+      break;
+    case EFFICIENT_E_MATCHING:
+      efficientEMatching = true;
+      break;
+    case LITERAL_MATCHING:
+      if(!strcmp(optarg, "none")) {
+        literalMatchMode = LITERAL_MATCH_NONE;
+      } else if(!strcmp(optarg, "predicate")) {
+        literalMatchMode = LITERAL_MATCH_PREDICATE;
+      } else if(!strcmp(optarg, "equality")) {
+        literalMatchMode = LITERAL_MATCH_EQUALITY;
+      } else if(!strcmp(optarg, "help")) {
+        //puts(literalMatchHelp.c_str());
+        exit(1);
+      } else {
+        throw OptionException(string("unknown option for --literal-matching: `") +
+                              optarg + "'.  Try --literal-matching help.");
+      }
+      break;
+    case ENABLE_CBQI:
+      cbqi = true;
+      cbqiSetByUser = true;
+      break;
+    case DISABLE_CBQI:
+      cbqi = false;
+      cbqiSetByUser = true;
+      break;
+    case IGNORE_USER_PATTERNS:
+      userPatternsQuant = false;
+      break;
+    case ENABLE_FLIP_DECISION:
+      flipDecision = true;
+      break;
     case TIME_LIMIT:
       {
         int i = atoi(optarg);
@@ -1141,7 +1303,7 @@ throw(OptionException) {
                               optarg + "' is not between 0.0 and 1.0.");
       }
       break;
-      
+
     case SAT_RESTART_FIRST:
       {
         int i = atoi(optarg);
@@ -1151,7 +1313,7 @@ throw(OptionException) {
         satRestartFirst = i;
         break;
       }
-      
+
     case SAT_RESTART_INC:
       {
         int i = atoi(optarg);
@@ -1341,7 +1503,7 @@ throw(OptionException) {
 
     case PORTFOLIO_FILTER_LENGTH:
       sharingFilterByLength = atoi(optarg);
-      break; 
+      break;
 
     case ':':
       // This can be a long or short option, and the way to get at the name of it is different.
diff --git a/src/util/options.h b/src/util/options.h
index 0584fdc2a..fb5f71060 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -310,6 +310,126 @@ struct CVC4_PUBLIC Options {
    */
   bool ufSymmetryBreakerSetByUser;
 
+  /**
+   * Whether to mini-scope quantifiers.
+   * For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
+   * ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
+   */
+  bool miniscopeQuant;
+
+  /**
+   * Whether to mini-scope quantifiers based on formulas with no free variables.
+   * For example, forall x. ( P( x ) V Q ) will be rewritten to
+   * ( forall x. P( x ) ) V Q
+   */
+  bool miniscopeQuantFreeVar;
+
+  /**
+   * Whether to prenex (nested universal) quantifiers
+   */
+  bool prenexQuant;
+
+  /**
+   * 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 )
+   */
+  bool varElimQuant;
+
+  /**
+   * Whether to CNF quantifier bodies
+   */
+  bool cnfQuant;
+
+  /**
+   * Whether to pre-skolemize quantifier bodies.
+   * For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
+   *   forall x. P( x ) => f( S( x ) ) = x
+   */
+  bool preSkolemQuant;
+
+  /**
+   * Whether to use smart triggers
+   */
+  bool smartTriggers;
+
+  /**
+   * Whether to consider terms in the bodies of quantifiers for matching
+   */
+  bool registerQuantBodyTerms;
+
+  /** Enumeration of inst_when modes (when to instantiate). */
+  typedef enum {
+    /** Apply instantiation round before full effort (possibly at standard effort) */
+    INST_WHEN_PRE_FULL,
+    /** Apply instantiation round at full effort or above  */
+    INST_WHEN_FULL,
+    /** Apply instantiation round at full effort half the time, and last call always */
+    INST_WHEN_FULL_LAST_CALL,
+    /** Apply instantiation round at last call only */
+    INST_WHEN_LAST_CALL,
+  } InstWhenMode;
+  /** When to perform instantiation round. */
+  InstWhenMode instWhenMode;
+
+  /**
+   * Whether to eagerly instantiate quantifiers
+   */
+  bool eagerInstQuant;
+
+  /**
+   * Whether to use finite model find heuristic
+   */
+  bool finiteModelFind;
+
+  /**
+   * Whether to use region-based SAT for finite model finding
+   */
+  bool fmfRegionSat;
+
+  /**
+   * Whether to use model-based exhaustive instantiation for finite model finding
+   */
+  bool fmfModelBasedInst;
+
+  /**
+   * Whether to use efficient E-matching
+   */
+  bool efficientEMatching;
+
+  /** Enumeration of literal matching modes. */
+  typedef enum {
+    /** 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,
+  } LiteralMatchMode;
+
+  /** Which literal matching mode to use. */
+  LiteralMatchMode literalMatchMode;
+
+  /**
+   * Whether to do counterexample-based quantifier instantiation
+   */
+  bool cbqi;
+
+  /**
+   * Whether the user explicitly requested that counterexample-based
+   * quantifier instantiation be enabled or disabled.
+   */
+  bool cbqiSetByUser;
+
+  /**
+   * Whether to use user patterns for pattern-based instantiation
+   */
+  bool userPatternsQuant;
+
+  /**
+   * Whether to use flip decision (useful when cbqi=true)
+   */
+  bool flipDecision;
 
   /** The output channel to receive notfication events for new lemmas */
   LemmaOutputChannel* lemmaOutputChannel;