print only labeled assertions as part of the unsat core

added the option dump-unsat-cores-full for printing the entire core, as before

diff --git a/src/options/smt_options b/src/options/smt_options
index 394e2382a778b5a382d7d570019c4cdedef09add..5f50ed202738b93c7521d71dc17fc731ed1723cd 100644 (file)
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -47,6 +47,8 @@ option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produc
  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 :notify notifyBeforeSearch
  output unsat cores after every UNSAT/VALID response
+option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch
+ dump the full unsat core, including unlabeled assertions
 
 option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch
  support the get-assignment command
@@ -115,35 +117,35 @@ expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :de
 
 expert-option decisionStep decision-step --decision-step unsigned :default 1
  amount of getNext decision calls in the decision engine
- 
+
 expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1
  amount of resources spent for each bitblast step
- 
+
 expert-option parseStep parse-step --parse-step unsigned :default 1
  amount of resources spent for each command/expression parsing
- 
+
 expert-option lemmaStep lemma-step --lemma-step unsigned :default 1
  amount of resources spent when adding lemmas
- 
+
 expert-option restartStep restart-step --restart-step unsigned :default 1
  amount of resources spent for each theory restart
- 
+
 expert-option cnfStep cnf-step --cnf-step unsigned :default 1
  amount of resources spent for each call to cnf conversion
- 
+
 expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1
  amount of resources spent for each preprocessing step in SmtEngine
- 
+
 expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1
  amount of resources spent for quantifier instantiations
- 
+
 expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1
  amount of resources spent for each sat conflict (main sat solver)
- 
+
 expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1
  amount of resources spent for each sat conflict (bitvectors)
- 
- 
+
+
 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
  eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
 

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index fd77535116a437f4889a6e99c301134b16bcb541..98993dba524ca8b410f28d6ab7cae1134ef883ec 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -294,7 +294,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::EMPTYSET:
       out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
       break;
-  
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
@@ -321,7 +321,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     }
     return;
   }
-  
+
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   // operator
@@ -510,10 +510,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::SUBSET:
   case kind::MEMBER:
   case kind::SET_TYPE:
-  case kind::SINGLETON: 
+  case kind::SINGLETON:
   case kind::COMPLEMENT:out << smtKindString(k) << " "; break;
   case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
-  
+
     // fp theory
   case kind::FLOATINGPOINT_FP:
   case kind::FLOATINGPOINT_EQ:
@@ -586,7 +586,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE:
     break;
-    
+
   //separation logic
   case kind::SEP_EMP:
   case kind::SEP_PTO:
@@ -667,7 +667,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
            tmp.replace(pos, 8, "::");
         }
         out << tmp;
-      }else if( n.getKind()==kind::APPLY_TESTER ){ 
+      }else if( n.getKind()==kind::APPLY_TESTER ){
         unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
         const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
         if( d_variant==smt2_6_variant ){
@@ -877,13 +877,13 @@ static string smtKindString(Kind k) throw() {
   case kind::REGEXP_OPT: return "re.opt";
   case kind::REGEXP_RANGE: return "re.range";
   case kind::REGEXP_LOOP: return "re.loop";
-  
+
   //sep theory
   case kind::SEP_STAR: return "sep";
   case kind::SEP_PTO: return "pto";
   case kind::SEP_WAND: return "wand";
   case kind::SEP_EMP: return "emp";
-    
+
   default:
     ; /* fall through */
   }
@@ -1064,10 +1064,12 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::
   out << "(" << std::endl;
   for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
     map<Expr, string>::const_iterator j = names.find(*i);
-    if(j == names.end()) {
-      out << *i << endl;
-    } else {
+    if (j != names.end()) {
+      // Named assertions always get printed
       out << maybeQuoteSymbol((*j).second) << endl;
+    } else if (options::dumpUnsatCoresFull()) {
+      // Unnamed assertions only get printed if the option is set
+      out << *i << endl;
     }
   }
   out << ")" << endl;
@@ -1105,7 +1107,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
     const std::map< TypeNode, std::vector< Node > >& type_reps = tm.d_rep_set.d_type_reps;
 
     std::map< TypeNode, std::vector< Node > >::const_iterator tn_iterator = type_reps.find( tn );
-    if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){  
+    if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){
       if(d_variant == smt2_6_variant) {
         out << "(declare-datatypes ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " 0)) (";
       }else{