diff options
| -rw-r--r-- | src/options/smt_options | 24 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 26 |
2 files changed, 27 insertions, 23 deletions
diff --git a/src/options/smt_options b/src/options/smt_options index 394e2382a..5f50ed202 100644 --- 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 fd7753511..98993dba5 100644 --- 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{ |