diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-02-07 09:08:09 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-07 11:08:09 -0600 |
commit | d86c84462b937830d754ab4d8d6202bab868bf42 (patch) | |
tree | 36c3df552ea246452a457391d102afee43ed949d | |
parent | bcbddbc8264c095da435c51b9bff3306b565aee7 (diff) |
Add `ArithProof::{printInteger,getLfscFunction}` (#3716)
-rw-r--r-- | src/proof/arith_proof.cpp | 62 | ||||
-rw-r--r-- | src/proof/arith_proof.h | 22 |
2 files changed, 84 insertions, 0 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 9ee5f2143..3ff0ff539 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -870,6 +870,56 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) { } } +std::string LFSCArithProof::getLfscFunction(const Node & n) { + Assert(n.getType().isInteger() || n.getType().isReal() || n.getType().isBoolean()); + std::string opString; + switch (n.getKind()) { + case kind::UMINUS: + opString = "u-_"; + break; + case kind::PLUS: + opString = "+_"; + break; + case kind::MINUS: + opString = "-_"; + break; + case kind::MULT: + opString = "*_"; + break; + case kind::DIVISION: + case kind::DIVISION_TOTAL: + opString = "/_"; + break; + case kind::GT: + opString = ">_"; + break; + case kind::GEQ: + opString = ">=_"; + break; + case kind::LT: + opString = "<_"; + break; + case kind::LEQ: + opString = "<=_"; + break; + default: + Unreachable() << "Tried to get the operator for a non-operator kind: " << n.getKind(); + } + std::string typeString; + if (n.getType().isInteger()) { + typeString = "Int"; + } else if (n.getType().isReal()) { + typeString = "Real"; + } else { // Boolean + if (n[0].getType().isInteger()) { + typeString = "IntReal"; + } else { + typeString = "Real"; + } + } + return opString + typeString; +} + void LFSCArithProof::printRational(std::ostream& o, const Rational& r) { if (r.sgn() < 0) @@ -883,6 +933,18 @@ void LFSCArithProof::printRational(std::ostream& o, const Rational& r) } } +void LFSCArithProof::printInteger(std::ostream& o, const Integer& i) +{ + if (i.sgn() < 0) + { + o << "(~ " << i.abs() << ")"; + } + else + { + o << i; + } +} + void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o, const Node& n) { diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index ac96ad1f3..5522b4eb4 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -89,6 +89,19 @@ public: void printOwnedSort(Type type, std::ostream& os) override; /** + * Returns the LFSC identifier for the operator of this node. + * + * e.g. "+_Real". + * + * Does not include any parens. + * + * Even if the operator is a comparison (e.g. >=) on integers, will not + * return a purely `Int` predicate like ">=_Int". Instead this treats the + * right hand side as a real. + */ + static std::string getLfscFunction(const Node& n); + + /** * Print a rational number in LFSC format. * e.g. 5/8 or (~ 1/1) * @@ -98,6 +111,15 @@ public: static void printRational(std::ostream& o, const Rational& r); /** + * Print an integer in LFSC format. + * e.g. 5 or (~ 1) + * + * @param o ostream to print to. + * @param i the integer to print + */ + static void printInteger(std::ostream& o, const Integer& i); + + /** * Print a value of type poly_formula_norm * * @param o ostream to print to |