Merge branch 'master' into rmTearDownIncrementalrmTearDownIncremental

11 files changed, 119 insertions, 111 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index d672b79a6..5f0da7a0c 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -31,6 +31,7 @@
 #include "expr/symbol_manager.h"
 #include "expr/type_node.h"
 #include "options/options.h"
+#include "options/main_options.h"
 #include "options/printer_options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index e85ea82ef..a46452004 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -32,12 +32,11 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent)
     : d_parent(parent),
       d_optChecker(),
       d_objectives(parent->getUserContext()),
-      d_results(),
-      d_objectiveCombination(LEXICOGRAPHIC)
+      d_results()
 {
 }
 
-OptimizationResult::ResultType OptimizationSolver::checkOpt()
+Result OptimizationSolver::checkOpt(ObjectiveCombination combination)
 {
   // if the results of the previous call have different size than the
   // objectives, then we should clear the pareto optimization context
@@ -48,7 +47,7 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt()
   {
     d_results.emplace_back();
   }
-  switch (d_objectiveCombination)
+  switch (combination)
   {
     case BOX: return optimizeBox(); break;
     case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break;
@@ -76,16 +75,9 @@ void OptimizationSolver::addObjective(TNode target,
 
 std::vector<OptimizationResult> OptimizationSolver::getValues()
 {
-  Assert(d_objectives.size() == d_results.size());
   return d_results;
 }
 
-void OptimizationSolver::setObjectiveCombination(
-    ObjectiveCombination combination)
-{
-  d_objectiveCombination = combination;
-}
-
 std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
     SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
 {
@@ -106,13 +98,12 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
   return optChecker;
 }
 
-OptimizationResult::ResultType OptimizationSolver::optimizeBox()
+Result OptimizationSolver::optimizeBox()
 {
   // resets the optChecker
   d_optChecker = createOptCheckerWithTimeout(d_parent);
   OptimizationResult partialResult;
-  OptimizationResult::ResultType aggregatedResultType =
-      OptimizationResult::OPTIMAL;
+  Result aggregatedResult(Result::Sat::SAT);
   std::unique_ptr<OMTOptimizer> optimizer;
   for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
   {
@@ -134,18 +125,19 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox()
     }
     // match the optimization result type, and aggregate the results of
     // subproblems
-    switch (partialResult.getType())
+    switch (partialResult.getResult().isSat())
     {
-      case OptimizationResult::OPTIMAL: break;
-      case OptimizationResult::UNBOUNDED: break;
-      case OptimizationResult::UNSAT:
-        if (aggregatedResultType == OptimizationResult::OPTIMAL)
+      case Result::SAT: break;
+      case Result::UNSAT:
+        // the assertions are unsatisfiable
+        for (size_t j = 0; j < numObj; ++j)
         {
-          aggregatedResultType = OptimizationResult::UNSAT;
+          d_results[j] = partialResult;
         }
-        break;
-      case OptimizationResult::UNKNOWN:
-        aggregatedResultType = OptimizationResult::UNKNOWN;
+        d_optChecker.reset();
+        return partialResult.getResult();
+      case Result::SAT_UNKNOWN:
+        aggregatedResult = partialResult.getResult();
         break;
       default: Unreachable();
     }
@@ -154,15 +146,20 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox()
   }
   // kill optChecker after optimization ends
   d_optChecker.reset();
-  return aggregatedResultType;
+  return aggregatedResult;
 }
 
-OptimizationResult::ResultType
-OptimizationSolver::optimizeLexicographicIterative()
+Result OptimizationSolver::optimizeLexicographicIterative()
 {
   // resets the optChecker
   d_optChecker = createOptCheckerWithTimeout(d_parent);
-  OptimizationResult partialResult;
+  // partialResult defaults to SAT if no objective is present
+  // NOTE: the parenthesis around Result(Result::SAT) is required,
+  // otherwise the compiler will report "parameter declarator cannot be
+  // qualified". For more details:
+  // https://stackoverflow.com/questions/44045257/c-compiler-error-c2751-what-exactly-causes-it
+  // https://en.wikipedia.org/wiki/Most_vexing_parse
+  OptimizationResult partialResult((Result(Result::SAT)), TNode());
   std::unique_ptr<OMTOptimizer> optimizer;
   for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
   {
@@ -186,26 +183,33 @@ OptimizationSolver::optimizeLexicographicIterative()
     d_results[i] = partialResult;
 
     // checks the optimization result of the current objective
-    switch (partialResult.getType())
+    switch (partialResult.getResult().isSat())
     {
-      case OptimizationResult::OPTIMAL:
+      case Result::SAT:
         // assert target[i] == value[i] and proceed
         d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode(
             kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue()));
         break;
-      case OptimizationResult::UNBOUNDED: return OptimizationResult::UNBOUNDED;
-      case OptimizationResult::UNSAT: return OptimizationResult::UNSAT;
-      case OptimizationResult::UNKNOWN: return OptimizationResult::UNKNOWN;
+      case Result::UNSAT:
+        d_optChecker.reset();
+        return partialResult.getResult();
+      case Result::SAT_UNKNOWN:
+        d_optChecker.reset();
+        return partialResult.getResult();
       default: Unreachable();
     }
+
+    // if the result for the current objective is unbounded
+    // then just stop
+    if (partialResult.isUnbounded()) break;
   }
   // kill optChecker in case pareto misuses it
   d_optChecker.reset();
-  // now all objectives are OPTIMAL, just return OPTIMAL as overall result
-  return OptimizationResult::OPTIMAL;
+  // now all objectives are optimal, just return SAT as the overall result
+  return partialResult.getResult();
 }
 
-OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
+Result OptimizationSolver::optimizeParetoNaiveGIA()
 {
   // initial call to Pareto optimizer, create the checker
   if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent);
@@ -216,8 +220,8 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
 
   switch (satResult.isSat())
   {
-    case Result::Sat::UNSAT: return OptimizationResult::UNSAT;
-    case Result::Sat::SAT_UNKNOWN: return OptimizationResult::UNKNOWN;
+    case Result::Sat::UNSAT: return satResult;
+    case Result::Sat::SAT_UNKNOWN: return satResult;
     case Result::Sat::SAT:
     {
       // if satisfied, use d_results to store the initial results
@@ -226,14 +230,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
       for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
       {
         d_results[i] = OptimizationResult(
-            OptimizationResult::OPTIMAL,
-            d_optChecker->getValue(d_objectives[i].getTarget()));
+            satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
       }
       break;
     }
     default: Unreachable();
   }
 
+  Result lastSatResult = satResult;
+
   // a vector storing assertions saying that no objective is worse
   std::vector<Node> noWorseObj;
   // a vector storing assertions saying that there is at least one objective
@@ -278,15 +283,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
       case Result::Sat::SAT_UNKNOWN:
         // if result is UNKNOWN, abort the current session and return UNKNOWN
         d_optChecker.reset();
-        return OptimizationResult::UNKNOWN;
+        return satResult;
       case Result::Sat::SAT:
       {
+        lastSatResult = satResult;
         // if result is SAT, update d_results to the more optimal values
         for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
         {
           d_results[i] = OptimizationResult(
-              OptimizationResult::OPTIMAL,
-              d_optChecker->getValue(d_objectives[i].getTarget()));
+              satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
         }
         break;
       }
@@ -302,7 +307,7 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
   // for the next run.
   d_optChecker->assertFormula(nm->mkOr(someObjBetter));
 
-  return OptimizationResult::OPTIMAL;
+  return lastSatResult;
 }
 
 }  // namespace smt
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 6d138deb2..d13168780 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -33,63 +33,75 @@ namespace smt {
 /**
  * The optimization result of an optimization objective
  * containing:
- * - whether it's optimal or not
- * - if so, the optimal value, otherwise the value might be empty node or
- *   something suboptimal
+ * - the optimization result: SAT/UNSAT/UNKNOWN
+ * - the optimal value if SAT and bounded
+ *     (optimal value reached and it's not infinity),
+ *   or an empty node if SAT and unbounded
+ *     (optimal value is +inf for maximum or -inf for minimum),
+ *   otherwise the value might be empty node
+ *   or something suboptimal
+ * - whether the objective is unbounded
  */
 class OptimizationResult
 {
  public:
   /**
-   * Enum indicating whether the checkOpt result
-   * is optimal or not.
-   **/
-  enum ResultType
-  {
-    // whether the value is optimal is UNKNOWN
-    UNKNOWN,
-    // the original set of assertions has result UNSAT
-    UNSAT,
-    // the value is optimal
-    OPTIMAL,
-    // the goal is unbounded,
-    // if objective is maximize, it's +infinity
-    // if objective is minimize, it's -infinity
-    UNBOUNDED,
-  };
-
-  /**
    * Constructor
    * @param type the optimization outcome
    * @param value the optimized value
+   * @param unbounded whether the objective is unbounded
    **/
-  OptimizationResult(ResultType type, TNode value)
-      : d_type(type), d_value(value)
+  OptimizationResult(Result result, TNode value, bool unbounded = false)
+      : d_result(result), d_value(value), d_unbounded(unbounded)
+  {
+  }
+  OptimizationResult()
+      : d_result(Result::Sat::SAT_UNKNOWN,
+                 Result::UnknownExplanation::NO_STATUS),
+        d_value(),
+        d_unbounded(false)
   {
   }
-  OptimizationResult() : d_type(UNKNOWN), d_value() {}
   ~OptimizationResult() = default;
 
   /**
    * Returns an enum indicating whether
-   * the result is optimal or not.
-   * @return an enum showing whether the result is optimal, unbounded,
-   *   unsat or unknown.
+   * the result is SAT or not.
+   * @return whether the result is SAT, UNSAT or SAT_UNKNOWN
    **/
-  ResultType getType() const { return d_type; }
+  Result getResult() const { return d_result; }
+
   /**
    * Returns the optimal value.
    * @return Node containing the optimal value,
-   *   if getType() is not OPTIMAL, it might return an empty node or a node
-   *   containing non-optimal value
+   *   if result is unbounded, this will be an empty node,
+   *   if getResult() is UNSAT, it will return an empty node,
+   *   if getResult() is SAT_UNKNOWN, it will return something suboptimal
+   *   or an empty node, depending on how the solver runs.
    **/
   Node getValue() const { return d_value; }
 
+  /**
+   * Checks whether the objective is unbouned
+   * @return whether the objective is unbounded
+   *   if the objective is unbounded (this function returns true), 
+   *   then the optimal value is:
+   *   +inf, if it's maximize;
+   *   -inf, if it's minimize
+   **/
+  bool isUnbounded() const { return d_unbounded; }
+
  private:
-  /** the indicating whether the result is optimal or something else **/
-  ResultType d_type;
-  /** if the result is optimal, this is storing the optimal value **/
+  /** indicating whether the result is SAT, UNSAT or UNKNOWN **/
+  Result d_result;
+  /** if the result is bounded, this is storing the value **/
   Node d_value;
+  /** whether the objective is unbounded
+   * If this is true, then:
+   * if objective is maximize, it's +infinity;
+   * if objective is minimize, it's -infinity
+   **/
+  bool d_unbounded;
 };
 
 /**
@@ -199,10 +211,10 @@ class OptimizationSolver
   /**
    * Run the optimization loop for the added objective
    * For multiple objective combination, it defaults to lexicographic,
-   * and combination could be set by calling
-   *   setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO)
+   * possible combinations: BOX, LEXICOGRAPHIC, PARETO
+   * @param combination BOX / LEXICOGRAPHIC / PARETO
    */
-  OptimizationResult::ResultType checkOpt();
+  Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC);
 
   /**
    * Add an optimization objective.
@@ -223,11 +235,6 @@ class OptimizationSolver
    **/
   std::vector<OptimizationResult> getValues();
 
-  /**
-   * Sets the objective combination
-   **/
-  void setObjectiveCombination(ObjectiveCombination combination);
-
  private:
   /**
    * Initialize an SMT subsolver for offline optimization purpose
@@ -244,26 +251,26 @@ class OptimizationSolver
 
   /**
    * Optimize multiple goals in Box order
-   * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED;
-   *   UNSAT if at least one objective is UNSAT and no objective is UNKNOWN;
-   *   UNKNOWN if any of the objective is UNKNOWN.
+   * @return SAT if all of the objectives are optimal or unbounded;
+   *   UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN;
+   *   SAT_UNKNOWN if any of the objective is SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeBox();
+  Result optimizeBox();
 
   /**
    * Optimize multiple goals in Lexicographic order,
    * using iterative implementation
-   * @return OPTIMAL if all objectives are OPTIMAL and bounded;
-   *   UNBOUNDED if one of the objectives is UNBOUNDED
+   * @return SAT if the objectives are optimal,
+   *     if one of the objectives is unbounded,
+   *     the optimization will stop at that objective;
+   *   UNSAT if any of the objectives is UNSAT
    *     and optimization will stop at that objective;
-   *   UNSAT if one of the objectives is UNSAT
-   *     and optimization will stop at that objective;
-   *   UNKNOWN if one of the objectives is UNKNOWN
+   *   SAT_UNKNOWN if any of the objectives is UNKNOWN
    *     and optimization will stop at that objective;
    *   If the optimization is stopped at an objective,
-   *     all objectives following that objective will be UNKNOWN.
+   *     all objectives following that objective will be SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeLexicographicIterative();
+  Result optimizeLexicographicIterative();
 
   /**
    * Optimize multiple goals in Pareto order
@@ -277,11 +284,12 @@ class OptimizationSolver
    * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm.
    *  Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009.
    *
-   * @return if it finds a new Pareto optimal result it will return OPTIMAL;
+   * @return if it finds a new Pareto optimal result it will return SAT;
    *   if it exhausts the results in the Pareto front it will return UNSAT;
-   *   if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN.
+   *   if the underlying SMT solver returns SAT_UNKNOWN,
+   *   it will return SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeParetoNaiveGIA();
+  Result optimizeParetoNaiveGIA();
 
   /** A pointer to the parent SMT engine **/
   SmtEngine* d_parent;
@@ -294,9 +302,6 @@ class OptimizationSolver
 
   /** The results of the optimizations from the last checkOpt call **/
   std::vector<OptimizationResult> d_results;
-
-  /** The current objective combination method **/
-  ObjectiveCombination d_objectiveCombination;
 };
 
 }  // namespace smt
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 7406b922e..3c0a4ac5b 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -15,6 +15,7 @@
 
 #include "smt/preprocessor.h"
 
+#include "options/base_options.h"
 #include "options/expr_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/preprocessing_pass_context.h"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index cd05b84c4..e119ce4d4 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -66,7 +66,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // unsat cores and proofs shenanigans
   if (options::dumpUnsatCoresFull())
   {
-    opts.smt.dumpUnsatCores = true;
+    opts.driver.dumpUnsatCores = true;
   }
   if (options::checkUnsatCores() || options::dumpUnsatCores()
       || options::unsatAssumptions()
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bd48fe0ea..9056e7c94 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -29,7 +29,6 @@
 #include "options/option_exception.h"
 #include "options/printer_options.h"
 #include "options/proof_options.h"
-#include "options/resource_manager_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
@@ -1811,16 +1810,16 @@ void SmtEngine::setResourceLimit(uint64_t units, bool cumulative)
 {
   if (cumulative)
   {
-    d_env->d_options.resman.cumulativeResourceLimit = units;
+    d_env->d_options.base.cumulativeResourceLimit = units;
   }
   else
   {
-    d_env->d_options.resman.perCallResourceLimit = units;
+    d_env->d_options.base.perCallResourceLimit = units;
   }
 }
 void SmtEngine::setTimeLimit(uint64_t millis)
 {
-  d_env->d_options.resman.perCallMillisecondLimit = millis;
+  d_env->d_options.base.perCallMillisecondLimit = millis;
 }
 
 unsigned long SmtEngine::getResourceUsage() const
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 4afa15a3b..cb0a94123 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -16,6 +16,7 @@
 #include "smt/smt_engine_state.h"
 
 #include "base/modal_exception.h"
+#include "options/base_options.h"
 #include "options/option_exception.h"
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
index 417d345cb..c76a8a2e7 100644
--- a/src/smt/smt_engine_stats.cpp
+++ b/src/smt/smt_engine_stats.cpp
@@ -25,8 +25,6 @@ SmtEngineStatistics::SmtEngineStatistics(const std::string& name)
         name + "definitionExpansionTime")),
       d_numConstantProps(
           smtStatisticsRegistry().registerInt(name + "numConstantProps")),
-      d_cnfConversionTime(
-          smtStatisticsRegistry().registerTimer(name + "cnfConversionTime")),
       d_numAssertionsPre(smtStatisticsRegistry().registerInt(
           name + "numAssertionsPreITERemoval")),
       d_numAssertionsPost(smtStatisticsRegistry().registerInt(
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
index 441721a54..db914b560 100644
--- a/src/smt/smt_engine_stats.h
+++ b/src/smt/smt_engine_stats.h
@@ -30,8 +30,6 @@ struct SmtEngineStatistics
   TimerStat d_definitionExpansionTime;
   /** number of constant propagations found during nonclausal simp */
   IntStat d_numConstantProps;
-  /** time spent converting to CNF */
-  TimerStat d_cnfConversionTime;
   /** Number of assertions before ite removal */
   IntStat d_numAssertionsPre;
   /** Number of assertions after ite removal */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index d7b70f501..f5783ab6b 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -239,7 +239,6 @@ void SmtSolver::processAssertions(Assertions& as)
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
-    TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
     const std::vector<Node>& assertions = ap.ref();
     // It is important to distinguish the input assertions from the skolem
     // definitions, as the decision justification heuristic treates the latter
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 8fa610cda..98278ef9e 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -20,6 +20,7 @@
 #include "base/modal_exception.h"
 #include "expr/dtype.h"
 #include "expr/skolem_manager.h"
+#include "options/base_options.h"
 #include "options/option_exception.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"