diff options
Diffstat (limited to 'src/proof/theory_proof.cpp')
-rw-r--r-- | src/proof/theory_proof.cpp | 34 |
1 files changed, 23 insertions, 11 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index ecd9f9810..5b5a2ae15 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -65,19 +65,17 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { os << term; return; } - std::ostringstream paren; + Assert (term.getKind() == kind::APPLY_UF); Expr func = term.getOperator(); - os << "(apply _ _ " << func << " "; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os<< "(apply _ _ "; + } + os << func << " "; for (unsigned i = 0; i < term.getNumChildren(); ++i) { printTerm(term[i], os); - if (i < term.getNumChildren() - 1) { - os << "(apply _ _ " << func << " "; - paren << ")"; - } - os << ")" ; + os << ")"; } - os << paren.str(); } std::string toLFSCKind(Kind kind) { @@ -95,7 +93,7 @@ std::string toLFSCKind(Kind kind) { void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { // should make this more general and overall sane - Assert (atom.getType().isBoolean()); + Assert (atom.getType().isBoolean() && "Only printing booleans." ); Kind kind = atom.getKind(); // this is the only predicate we have if (kind == kind::EQUAL) { @@ -106,6 +104,13 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { os <<" "; printTerm(atom[1], os); os <<")"; + } else if ( kind == kind::DISTINCT) { + os <<"(not (= "; + os << atom[0].getType() <<" "; + printTerm(atom[0], os); + os <<" "; + printTerm(atom[1], os); + os <<"))"; } else if ( kind == kind::OR || kind == kind::AND || kind == kind::XOR || @@ -134,8 +139,15 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { } os <<")"; } - } else { - Assert (false); + } else if (kind == kind::CONST_BOOLEAN) { + if (atom.getConst<bool>()) + os << "true"; + else + os << "false"; + } + else { + std::cout << kind << "\n"; + Assert (false && "Unsupported kind"); } } |