if (type.isInteger() && d_realMode) {
// If in "real mode", don't use type Int for, e.g., equality.
- os << "Real ";
+ os << "Real";
} else {
- os << type << " ";
+ os << type;
}
}
printSort(array_type.getConstituentType(), os);
os << ")";
} else {
- os << type <<" ";
+ os << type;
}
}
Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl;
Assert (type.isBitVector());
unsigned width = utils::getSize(type);
- os << "(BitVec "<<width<<")";
+ os << "(BitVec " << width << ")";
}
void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
template <class Solver>
void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out,
std::ostream& paren) {
- out << "(satlem_simplify _ _ _ ";
+ out << "(satlem_simplify _ _ _";
paren << ")";
const ResChain<Solver>& res = this->getResolutionChain(id);
const typename ResChain<Solver>::ResSteps& steps = res.getSteps();
for (int i = steps.size() - 1; i >= 0; i--) {
- out << "(";
- out << (steps[i].sign ? "R" : "Q") << " _ _ ";
+ out << " (";
+ out << (steps[i].sign ? "R" : "Q") << " _ _";
}
ClauseId start_id = res.getStart();
- out << this->clauseName(start_id) << " ";
+ out << " " << this->clauseName(start_id);
for (unsigned i = 0; i < steps.size(); i++) {
prop::SatVariable v =
prop::MinisatSatSolver::toSatVariable(var(steps[i].lit));
- out << this->clauseName(steps[i].id) << " "
+ out << " " << this->clauseName(steps[i].id) << " "
<< ProofManager::getVarName(v, this->d_name) << ")";
}
if (id == this->d_emptyClauseId) {
- out <<"(\\ empty empty)";
+ out <<" (\\ empty empty)";
return;
}
- out << "(\\ " << this->clauseName(id) << "\n"; // bind to lemma name
+ out << " (\\ " << this->clauseName(id) << "\n"; // bind to lemma name
paren << ")";
}
os << "(";
os << "= ";
printSort(term[0].getType(), os);
+ os << " ";
printBoundTerm(term[0], os, map);
os << " ";
printBoundTerm(term[1], os, map);
if (term.getNumChildren() == 2) {
os << "(not (= ";
printSort(term[0].getType(), os);
+ os << " ";
printBoundTerm(term[0], os, map);
os << " ";
printBoundTerm(term[1], os, map);
if ((i != 0) || (j != 1)) {
os << "(not (= ";
printSort(term[0].getType(), os);
+ os << " ";
printBoundTerm(term[i], os, map);
os << " ";
printBoundTerm(term[j], os, map);
} else {
os << "(not (= ";
printSort(term[0].getType(), os);
+ os << " ";
printBoundTerm(term[0], os, map);
os << " ";
printBoundTerm(term[1], os, map);
Debug("pf::uf") << std::endl << "(pf::uf) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
Assert (type.isSort());
- os << type <<" ";
+ os << type;
}
void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {