Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).

9 files changed, 150 insertions, 21 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index def9308bb..bf0e57eca 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -228,6 +228,7 @@ void Smt2::addTheory(Theory theory) {
 
   case THEORY_STRINGS:
     defineType("String", getExprManager()->stringType());
+    defineType("Int", getExprManager()->integerType());
     addStringOperators();
     break;
 
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 0f9cfa710..2d8c4178a 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -204,7 +204,7 @@ void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
   Debug("cores") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);
   d_deps[Node::fromExpr(formula)]; // empty vector of deps
-  if(inUnsatCore || options::dumpUnsatCores()) {
+  if(inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) {
     Debug("cores") << "adding to input core forms: " << formula << std::endl;
     d_inputCoreFormulas.insert(formula);
   }
@@ -221,6 +221,11 @@ void ProofManager::addDependence(TNode n, TNode dep) {
   }
 }
 
+void ProofManager::addUnsatCore(Expr formula) {
+  Assert (d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
+  d_outputCoreFormulas.insert(formula);
+}
+
 void ProofManager::setLogic(const LogicInfo& logic) {
   d_logic = logic;
 }
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 43d6723fa..ee99b0159 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -171,6 +171,7 @@ public:
   void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
   // note that n depends on dep (for cores)
   void addDependence(TNode n, TNode dep);
+  void addUnsatCore(Expr formula);
 
   assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
   assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
diff --git a/src/smt/options b/src/smt/options
index 593fc4887..b23d73943 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -31,7 +31,7 @@ option dumpModels --dump-models bool :default false :link --produce-models
  output models after every SAT/INVALID/UNKNOWN response
 option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on proof generation
-option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
  after UNSAT/VALID, machine-check the generated proof
 option dumpProofs --dump-proofs bool :default false :link --proof
  output proofs after every UNSAT/VALID response
@@ -41,6 +41,8 @@ option dumpSynth --dump-synth bool :default false
  output solution for synthesis conjectures after every UNSAT/VALID response
 option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on unsat core generation
+option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write
+ after UNSAT/VALID, produce and check an unsat core (expensive)
 option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  output unsat cores after every UNSAT/VALID response
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 229cc7c7c..b2bdea13f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -199,6 +199,8 @@ struct SmtEngineStatistics {
   TimerStat d_checkModelTime;
   /** time spent in checkProof() */
   TimerStat d_checkProofTime;
+  /** time spent in checkUnsatCore() */
+  TimerStat d_checkUnsatCoreTime;
   /** time spent in PropEngine::checkSat() */
   TimerStat d_solveTime;
   /** time spent in pushing/popping */
@@ -229,6 +231,7 @@ struct SmtEngineStatistics {
     d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
     d_checkModelTime("smt::SmtEngine::checkModelTime"),
     d_checkProofTime("smt::SmtEngine::checkProofTime"),
+    d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
     d_solveTime("smt::SmtEngine::solveTime"),
     d_pushPopTime("smt::SmtEngine::pushPopTime"),
     d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
@@ -253,6 +256,7 @@ struct SmtEngineStatistics {
     StatisticsRegistry::registerStat(&d_numAssertionsPost);
     StatisticsRegistry::registerStat(&d_checkModelTime);
     StatisticsRegistry::registerStat(&d_checkProofTime);
+    StatisticsRegistry::registerStat(&d_checkUnsatCoreTime);
     StatisticsRegistry::registerStat(&d_solveTime);
     StatisticsRegistry::registerStat(&d_pushPopTime);
     StatisticsRegistry::registerStat(&d_processAssertionsTime);
@@ -278,6 +282,7 @@ struct SmtEngineStatistics {
     StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
     StatisticsRegistry::unregisterStat(&d_checkModelTime);
     StatisticsRegistry::unregisterStat(&d_checkProofTime);
+    StatisticsRegistry::unregisterStat(&d_checkUnsatCoreTime);
     StatisticsRegistry::unregisterStat(&d_solveTime);
     StatisticsRegistry::unregisterStat(&d_pushPopTime);
     StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
@@ -695,6 +700,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_modelGlobalCommands(),
   d_modelCommands(NULL),
   d_dumpCommands(),
+#ifdef CVC4_PROOF  
+  d_defineCommands(),
+#endif  
   d_logic(),
   d_originalOptions(em->getOptions()),
   d_pendingPops(0),
@@ -1029,6 +1037,14 @@ void SmtEngine::setDefaults() {
       Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl;
       setOption("bv-intro-pow2", false);
     }
+    if(options::repeatSimp()) {
+      if(options::repeatSimp.wasSetByUser()) {
+        throw OptionException("repeat-simp not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl;
+      setOption("repeat-simp", false);
+    }
+
   }
 
   if(options::produceAssignments() && !options::produceModels()) {
@@ -1047,6 +1063,24 @@ void SmtEngine::setDefaults() {
     }
   }
 
+  // strings require LIA, UF; widen the logic
+  if(d_logic.isTheoryEnabled(THEORY_STRINGS)) {
+    LogicInfo log(d_logic.getUnlockedCopy());
+    // Strings requires arith for length constraints, and also UF
+    if(!d_logic.isTheoryEnabled(THEORY_UF)) {
+      Trace("smt") << "because strings are enabled, also enabling UF" << endl;
+      log.enableTheory(THEORY_UF);
+    }
+    if(!d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isDifferenceLogic() || !d_logic.areIntegersUsed()) {
+      Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl;
+      log.enableTheory(THEORY_ARITH);
+      log.enableIntegers();
+      log.arithOnlyLinear();
+    }
+    d_logic = log;
+    d_logic.lock();
+  }
+
   // by default, symmetry breaker is on only for QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
     bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
@@ -1133,16 +1167,25 @@ void SmtEngine::setDefaults() {
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
-      (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV));
+                      (d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+		       d_logic.isTheoryEnabled(THEORY_UF) &&
+		       d_logic.isTheoryEnabled(THEORY_BV)) &&
+                      !options::unsatCores();
     Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
     options::repeatSimp.set(repeatSimp);
   }
   // Turn on unconstrained simplification for QF_AUFBV
-  if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) {
+  if(!options::unconstrainedSimp.wasSetByUser() ||
+      options::incrementalSolving()) {
     //    bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
     //    bool uncSimp = false && !qf_sat && !options::incrementalSolving();
-    bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::produceAssignments() && !options::checkModels() &&
-      (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
+    bool uncSimp = !options::incrementalSolving() &&
+                   !d_logic.isQuantified() &&
+                   !options::produceModels() &&
+                   !options::produceAssignments() &&
+                   !options::checkModels() &&
+                   !options::unsatCores() &&
+                   (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl;
     options::unconstrainedSimp.set(uncSimp);
   }
@@ -1660,6 +1703,11 @@ void SmtEngine::defineFunction(Expr func,
 
   SmtScope smts(this);
 
+  PROOF( if (options::checkUnsatCores()) {
+      d_defineCommands.push_back(c.clone());
+    });
+
+  
   // Substitute out any abstract values in formula
   Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
 
@@ -3033,7 +3081,7 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
+  
   if (d_assertions.size() == 0) {
     // nothing to do
     return;
@@ -3331,8 +3379,7 @@ void SmtEnginePrivate::processAssertions() {
           d_iteSkolemMap.erase(toErase.back());
           toErase.pop_back();
         }
-        d_assertions[d_realAssertionsEnd - 1] =
-          Rewriter::rewrite(Node(builder));
+	d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
       }
       // For some reason this is needed for some benchmarks, such as
       // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
@@ -3442,6 +3489,12 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
       // n is the result of an unknown preprocessing step, add it to dependency map to null
       ProofManager::currentPM()->addDependence(n, Node::null());
     }
+    // rewrite rules are by default in the unsat core because
+    // they need to be applied until saturation
+    if(options::unsatCores() && 
+       n.getKind() == kind::REWRITE_RULE ){
+      ProofManager::currentPM()->addUnsatCore(n.toExpr());
+    }
   );
 
   // Add the normalized formula to the queue
@@ -3512,7 +3565,7 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
     // Dump the query if requested
     if(Dump.isOn("benchmark")) {
       // the expr already got dumped out if assertion-dumping is on
-      Dump("benchmark") << CheckSatCommand();
+      Dump("benchmark") << CheckSatCommand(ex);
     }
 
     // Pop the context
@@ -3539,6 +3592,13 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
         checkProof();
       }
     }
+    // Check that UNSAT results generate an unsat core correctly.
+    if(options::checkUnsatCores()) {
+      if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+        TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
+        checkUnsatCore();
+      }
+    }
 
     return r;
   } catch (UnsafeInterruptException& e) {
@@ -3596,7 +3656,7 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
   // Dump the query if requested
   if(Dump.isOn("benchmark")) {
     // the expr already got dumped out if assertion-dumping is on
-    Dump("benchmark") << CheckSatCommand();
+    Dump("benchmark") << QueryCommand(ex);
   }
 
   // Pop the context
@@ -3623,6 +3683,13 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
       checkProof();
     }
   }
+  // Check that UNSAT results generate an unsat core correctly.
+  if(options::checkUnsatCores()) {
+    if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
+      checkUnsatCore();
+    }
+  }
 
   return r;
   } catch (UnsafeInterruptException& e) {
@@ -3943,6 +4010,47 @@ Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) {
   return m;
 }
 
+void SmtEngine::checkUnsatCore() {
+  Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
+
+  Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
+  UnsatCore core = getUnsatCore();
+
+  SmtEngine coreChecker(d_exprManager);
+  coreChecker.setLogic(getLogicInfo());
+
+  PROOF(
+  std::vector<Command*>::const_iterator itg = d_defineCommands.begin();
+  for (; itg != d_defineCommands.end();  ++itg) {
+    (*itg)->invoke(&coreChecker);
+  }
+	);
+  
+  Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
+  for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
+    Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;
+    coreChecker.assertFormula(*i);
+  }
+  const bool checkUnsatCores = options::checkUnsatCores();
+  Result r;
+  try {
+    options::checkUnsatCores.set(false);
+    options::checkProofs.set(false);
+    r = coreChecker.checkSat();
+  } catch(...) {
+    options::checkUnsatCores.set(checkUnsatCores);
+    throw;
+  }
+  Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
+  if(r.asSatisfiabilityResult().isUnknown()) {
+    InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
+  }
+
+  if(r.asSatisfiabilityResult().isSat()) {
+    InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
+  }
+}
+
 void SmtEngine::checkModel(bool hardFailure) {
   // --check-model implies --produce-assertions, which enables the
   // assertion list, so we should be ok.
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7c5c45e42..de9b8127d 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -186,6 +186,13 @@ class CVC4_PUBLIC SmtEngine {
   std::vector<Command*> d_dumpCommands;
 
   /**
+   *A vector of command definitions to be imported in the new
+   *SmtEngine when checking unsat-cores.
+   */
+#ifdef CVC4_PROOF  
+  std::vector<Command*> d_defineCommands;
+#endif   
+  /**
    * The logic we're in.
    */
   LogicInfo d_logic;
@@ -261,6 +268,11 @@ class CVC4_PUBLIC SmtEngine {
   void checkProof();
 
   /**
+   * Check that an unsatisfiable core is indeed unsatisfiable.
+   */
+  void checkUnsatCore();
+
+  /**
    * Check that a generated Model (via getModel()) actually satisfies
    * all user assertions.
    */
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 2080c772a..4c35bd863 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -57,9 +57,10 @@ void SmtEngine::checkProof() {
 
   Chat() << "checking proof..." << endl;
 
-  if( ! ( d_logic.isPure(theory::THEORY_BOOL) ||
-          ( d_logic.isPure(theory::THEORY_UF) &&
-            ! d_logic.hasCardinalityConstraints() ) ) ) {
+  if( !(d_logic.isPure(theory::THEORY_BOOL) ||
+	(d_logic.isPure(theory::THEORY_UF) &&
+	 ! d_logic.hasCardinalityConstraints())) ||
+      d_logic.isQuantified()) {
     // no checking for these yet
     Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl;
     return;
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 635262a1e..1df304061 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -223,13 +223,7 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         p += 2;
       }
       if(*p == 'S') {
-        // Strings requires arith for length constraints,
-        // and UF for equality (?)
         enableTheory(THEORY_STRINGS);
-        enableTheory(THEORY_UF);
-        enableTheory(THEORY_ARITH);
-        enableIntegers();
-        arithOnlyLinear();
         ++p;
       }
       if(!strncmp(p, "IDL", 3)) {
diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h
index 27cf86488..8f497688a 100644
--- a/src/util/unsat_core.h
+++ b/src/util/unsat_core.h
@@ -23,6 +23,7 @@
 #include <iostream>
 #include <vector>
 #include "expr/expr.h"
+#include "util/output.h"
 
 namespace CVC4 {
 
@@ -43,13 +44,17 @@ public:
   UnsatCore() : d_smt(NULL) {}
 
   template <class T>
-  UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {}
+  UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {
+    Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
+  }
 
   ~UnsatCore() {}
 
   /** get the smt engine that this unsat core is hooked up to */
   SmtEngine* getSmtEngine() { return d_smt; }
 
+  size_t size() const { return d_core.size(); }
+
   typedef std::vector<Expr>::const_iterator iterator;
   typedef std::vector<Expr>::const_iterator const_iterator;