case kind::STRING_LENGTH:
out << "LENGTH";
break;
+ case kind::STRING_SUBSTR: out << "SUBSTR"; break;
default:
Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;
#include <memory>
#include <stack>
+#include "expr/node.h"
#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
+#include "theory/arith/constraint_forward.h"
#include "theory/arith/theory_arith.h"
+#define CVC4_ARITH_VAR_TERM_PREFIX "term."
+
namespace CVC4 {
inline static Node eqNode(TNode n1, TNode n2) {
// !d_realMode <--> term.getType().isInteger()
Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
- switch (term.getKind()) {
+ switch (term.getKind())
+ {
+ case kind::CONST_RATIONAL:
+ {
+ Assert(term.getNumChildren() == 0);
+ Assert(term.getType().isInteger() || term.getType().isReal());
- case kind::CONST_RATIONAL: {
- Assert (term.getNumChildren() == 0);
- Assert (term.getType().isInteger() || term.getType().isReal());
+ const Rational& r = term.getConst<Rational>();
+ bool neg = (r < 0);
- const Rational& r = term.getConst<Rational>();
- bool neg = (r < 0);
+ os << (!d_realMode ? "(a_int " : "(a_real ");
- os << (!d_realMode ? "(a_int " : "(a_real ");
+ if (neg)
+ {
+ os << "(~ ";
+ }
- if (neg) {
- os << "(~ ";
- }
+ if (!d_realMode)
+ {
+ os << r.abs();
+ }
+ else
+ {
+ printRational(os, r.abs());
+ }
- if (!d_realMode) {
- os << r.abs();
- } else {
- os << r.abs().getNumerator();
- os << "/";
- os << r.getDenominator();
+ if (neg)
+ {
+ os << ") ";
+ }
+
+ os << ") ";
+ return;
}
- if (neg) {
+ case kind::UMINUS:
+ {
+ Assert(term.getNumChildren() == 1);
+ Assert(term.getType().isInteger() || term.getType().isReal());
+ os << (!d_realMode ? "(u-_Int " : "(u-_Real ");
+ d_proofEngine->printBoundTerm(term[0], os, map);
os << ") ";
+ return;
}
- os << ") ";
- return;
- }
+ case kind::PLUS:
+ {
+ Assert(term.getNumChildren() >= 2);
- case kind::UMINUS: {
- Assert (term.getNumChildren() == 1);
- Assert (term.getType().isInteger() || term.getType().isReal());
- os << (!d_realMode ? "(u-_Int " : "(u-_Real ");
- d_proofEngine->printBoundTerm(term[0], os, map);
- os << ") ";
- return;
- }
+ std::stringstream paren;
+ for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+ {
+ os << (!d_realMode ? "(+_Int " : "(+_Real ");
+ d_proofEngine->printBoundTerm(term[i], os, map);
+ os << " ";
+ paren << ") ";
+ }
- case kind::PLUS: {
- Assert (term.getNumChildren() >= 2);
+ d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+ os << paren.str();
+ return;
+ }
- std::stringstream paren;
- for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
- os << (!d_realMode ? "(+_Int " : "(+_Real ");
- d_proofEngine->printBoundTerm(term[i], os, map);
- os << " ";
- paren << ") ";
+ case kind::MINUS:
+ {
+ Assert(term.getNumChildren() >= 2);
+
+ std::stringstream paren;
+ for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+ {
+ os << (!d_realMode ? "(-_Int " : "(-_Real ");
+ d_proofEngine->printBoundTerm(term[i], os, map);
+ os << " ";
+ paren << ") ";
+ }
+
+ d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+ os << paren.str();
+ return;
}
- d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
- os << paren.str();
- return;
- }
+ case kind::MULT:
+ {
+ Assert(term.getNumChildren() >= 2);
- case kind::MINUS: {
- Assert (term.getNumChildren() >= 2);
+ std::stringstream paren;
+ for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+ {
+ os << (!d_realMode ? "(*_Int " : "(*_Real ");
+ d_proofEngine->printBoundTerm(term[i], os, map);
+ os << " ";
+ paren << ") ";
+ }
- std::stringstream paren;
- for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
- os << (!d_realMode ? "(-_Int " : "(-_Real ");
- d_proofEngine->printBoundTerm(term[i], os, map);
- os << " ";
- paren << ") ";
+ d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+ os << paren.str();
+ return;
}
- d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
- os << paren.str();
- return;
- }
+ case kind::DIVISION:
+ case kind::DIVISION_TOTAL:
+ {
+ Assert(term.getNumChildren() >= 2);
- case kind::MULT: {
- Assert (term.getNumChildren() >= 2);
+ std::stringstream paren;
+ for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+ {
+ os << (!d_realMode ? "(/_Int " : "(/_Real ");
+ d_proofEngine->printBoundTerm(term[i], os, map);
+ os << " ";
+ paren << ") ";
+ }
- std::stringstream paren;
- for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
- os << (!d_realMode ? "(*_Int " : "(*_Real ");
- d_proofEngine->printBoundTerm(term[i], os, map);
- os << " ";
- paren << ") ";
+ d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+ os << paren.str();
+ return;
}
- d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
- os << paren.str();
- return;
- }
+ case kind::GT:
+ Assert(term.getNumChildren() == 2);
+ os << (!d_realMode ? "(>_Int " : "(>_Real ");
+ d_proofEngine->printBoundTerm(term[0], os, map);
+ os << " ";
+ d_proofEngine->printBoundTerm(term[1], os, map);
+ os << ") ";
+ return;
- case kind::DIVISION:
- case kind::DIVISION_TOTAL: {
- Assert (term.getNumChildren() >= 2);
+ case kind::GEQ:
+ Assert(term.getNumChildren() == 2);
+ os << (!d_realMode ? "(>=_Int " : "(>=_Real ");
+ d_proofEngine->printBoundTerm(term[0], os, map);
+ os << " ";
+ d_proofEngine->printBoundTerm(term[1], os, map);
+ os << ") ";
+ return;
- std::stringstream paren;
- for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
- os << (!d_realMode ? "(/_Int " : "(/_Real ");
- d_proofEngine->printBoundTerm(term[i], os, map);
+ case kind::LT:
+ Assert(term.getNumChildren() == 2);
+ os << (!d_realMode ? "(<_Int " : "(<_Real ");
+ d_proofEngine->printBoundTerm(term[0], os, map);
os << " ";
- paren << ") ";
- }
+ d_proofEngine->printBoundTerm(term[1], os, map);
+ os << ") ";
+ return;
- d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
- os << paren.str();
- return;
- }
+ case kind::LEQ:
+ Assert(term.getNumChildren() == 2);
+ os << (!d_realMode ? "(<=_Int " : "(<=_Real ");
+ d_proofEngine->printBoundTerm(term[0], os, map);
+ os << " ";
+ d_proofEngine->printBoundTerm(term[1], os, map);
+ os << ") ";
+ return;
- case kind::GT:
- Assert (term.getNumChildren() == 2);
- os << (!d_realMode ? "(>_Int " : "(>_Real ");
- d_proofEngine->printBoundTerm(term[0], os, map);
- os << " ";
- d_proofEngine->printBoundTerm(term[1], os, map);
- os << ") ";
- return;
-
- case kind::GEQ:
- Assert (term.getNumChildren() == 2);
- os << (!d_realMode ? "(>=_Int " : "(>=_Real ");
- d_proofEngine->printBoundTerm(term[0], os, map);
- os << " ";
- d_proofEngine->printBoundTerm(term[1], os, map);
- os << ") ";
- return;
-
- case kind::LT:
- Assert (term.getNumChildren() == 2);
- os << (!d_realMode ? "(<_Int " : "(<_Real ");
- d_proofEngine->printBoundTerm(term[0], os, map);
- os << " ";
- d_proofEngine->printBoundTerm(term[1], os, map);
- os << ") ";
- return;
-
- case kind::LEQ:
- Assert (term.getNumChildren() == 2);
- os << (!d_realMode ? "(<=_Int " : "(<=_Real ");
- d_proofEngine->printBoundTerm(term[0], os, map);
- os << " ";
- d_proofEngine->printBoundTerm(term[1], os, map);
- os << ") ";
- return;
+ case kind::VARIABLE:
+ case kind::SKOLEM:
+ os << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term);
+ return;
- default:
- Debug("pf::arith") << "Default printing of term: " << term << std::endl;
- os << term;
- return;
+ default:
+ Debug("pf::arith") << "Default printing of term: " << term << std::endl;
+ os << term;
+ return;
}
}
}
}
-void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
- os << " ;; Arith Theory Lemma \n;;";
- for (unsigned i = 0; i < lemma.size(); ++i) {
- os << lemma[i] <<" ";
+void LFSCArithProof::printRational(std::ostream& o, const Rational& r)
+{
+ if (r.sgn() < 0)
+ {
+ o << "(~ " << r.getNumerator().abs() << "/" << r.getDenominator().abs()
+ << ")";
+ }
+ else
+ {
+ o << r.getNumerator() << "/" << r.getDenominator();
+ }
+}
+
+void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o,
+ const Node& n)
+{
+ switch (n.getKind())
+ {
+ case kind::PLUS:
+ {
+ // Since our axioms are binary, but n may be n-ary, we rig up
+ // a right-associative tree.
+ size_t nchildren = n.getNumChildren();
+ for (size_t i = 0; i < nchildren; ++i)
+ {
+ if (i < nchildren - 1)
+ {
+ o << "\n (pn_+ _ _ _ _ _ ";
+ }
+ printLinearMonomialNormalizer(o, n[i]);
+ }
+ std::fill_n(std::ostream_iterator<char>(o), nchildren - 1, ')');
+ break;
+ }
+ case kind::MULT:
+ case kind::VARIABLE:
+ case kind::CONST_RATIONAL:
+ case kind::SKOLEM:
+ {
+ printLinearMonomialNormalizer(o, n);
+ break;
+ }
+ default:
+#ifdef CVC4_ASSERTIONS
+ std::ostringstream msg;
+ msg << "Invalid operation " << n.getKind() << " in linear polynomial";
+ Unreachable(msg.str().c_str());
+#endif // CVC4_ASSERTIONS
+ break;
+ }
+}
+
+void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
+ const Node& n)
+{
+ switch (n.getKind())
+ {
+ case kind::MULT: {
+#ifdef CVC4_ASSERTIONS
+ std::ostringstream s;
+ s << "node " << n << " is not a linear monomial";
+ s << " " << n[0].getKind() << " " << n[1].getKind();
+ Assert((n[0].getKind() == kind::CONST_RATIONAL
+ && (n[1].getKind() == kind::VARIABLE
+ || n[1].getKind() == kind::SKOLEM)),
+ s.str().c_str());
+#endif // CVC4_ASSERTIONS
+
+ o << "\n (pn_mul_c_L _ _ _ ";
+ printConstRational(o, n[0]);
+ o << " ";
+ printVariableNormalizer(o, n[1]);
+ o << ")";
+ break;
+ }
+ case kind::CONST_RATIONAL:
+ {
+ o << "\n (pn_const ";
+ printConstRational(o, n);
+ o << ")";
+ break;
+ }
+ case kind::VARIABLE:
+ case kind::SKOLEM:
+ {
+ o << "\n ";
+ printVariableNormalizer(o, n);
+ break;
+ }
+ default:
+#ifdef CVC4_ASSERTIONS
+ std::ostringstream msg;
+ msg << "Invalid operation " << n.getKind() << " in linear monomial";
+ Unreachable(msg.str().c_str());
+#endif // CVC4_ASSERTIONS
+ break;
+ }
+}
+
+void LFSCArithProof::printConstRational(std::ostream& o, const Node& n)
+{
+ Assert(n.getKind() == kind::CONST_RATIONAL);
+ const Rational value = n.getConst<Rational>();
+ printRational(o, value);
+}
+
+void LFSCArithProof::printVariableNormalizer(std::ostream& o, const Node& n)
+{
+ std::ostringstream msg;
+ msg << "Invalid variable kind " << n.getKind() << " in linear monomial";
+ Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM,
+ msg.str().c_str());
+ o << "(pn_var " << n << ")";
+}
+
+void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o,
+ const Node& n)
+{
+ Assert(n.getKind() == kind::GEQ,
+ "can only print normalization witnesses for (>=) nodes");
+ Assert(n[1].getKind() == kind::CONST_RATIONAL);
+ o << "(poly_formula_norm_>= _ _ _ ";
+ o << "\n (pn_- _ _ _ _ _ ";
+ printLinearPolynomialNormalizer(o, n[0]);
+ o << "\n (pn_const ";
+ printConstRational(o, n[1]);
+ o << ")))";
+}
+
+void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map)
+{
+ Debug("pf::arith") << "Printing proof for lemma " << lemma << std::endl;
+ // Prefixes for the names of linearity witnesses
+ const char* linearityWitnessPrefix = "lp";
+ const char* linearizedProofPrefix = "pf_lp";
+ std::ostringstream lemmaParen;
+
+ // Construct the set of conflicting literals
+ std::set<Node> conflictSet;
+ std::transform(lemma.begin(),
+ lemma.end(),
+ std::inserter(conflictSet, conflictSet.begin()),
+ [](const Expr& e) {
+ return NodeManager::currentNM()->fromExpr(e).negate();
+ });
+
+ // If we have Farkas coefficients stored for this lemma, use them to write a
+ // proof. Otherwise, just `trust` the lemma.
+ if (d_recorder.hasFarkasCoefficients(conflictSet))
+ {
+ // Get farkas coefficients & literal order
+ const auto& farkasInfo = d_recorder.getFarkasCoefficients(conflictSet);
+ const Node& conflict = farkasInfo.first;
+ theory::arith::RationalVectorCP farkasCoefficients = farkasInfo.second;
+ Assert(farkasCoefficients != theory::arith::RationalVectorCPSentinel);
+ Assert(conflict.getNumChildren() == farkasCoefficients->size());
+ const size_t nAntecedents = conflict.getNumChildren();
+
+ // Print proof
+ os << "\n;; Farkas Proof" << std::endl;
+
+ // Construct witness that the literals are linear polynomials
+ os << "; Linear Polynomial Normalization Witnesses" << std::endl;
+ for (size_t i = 0; i != nAntecedents; ++i)
+ {
+ const Node& antecedent = conflict[i];
+ const Rational farkasC = (*farkasCoefficients)[i];
+ os << "\n; " << antecedent << " w/ farkas c = " << farkasC << std::endl;
+ os << " (@ "
+ << ProofManager::getLitName(antecedent.negate(),
+ linearityWitnessPrefix)
+ << " ";
+ const Node& nonneg =
+ antecedent.getKind() == kind::NOT ? antecedent[0] : antecedent;
+ printLinearPolynomialPredicateNormalizer(os, nonneg);
+ lemmaParen << ")";
+ }
+
+ // Prove linear polynomial constraints
+ os << "\n; Linear Polynomial Proof Conversions";
+ for (size_t i = 0; i != nAntecedents; ++i)
+ {
+ const Node& antecedent = conflict[i];
+ os << "\n (@ "
+ << ProofManager::getLitName(antecedent.negate(), linearizedProofPrefix)
+ << " ";
+ lemmaParen << ")";
+ switch (conflict[i].getKind())
+ {
+ case kind::NOT:
+ {
+ Assert(conflict[i][0].getKind() == kind::GEQ);
+ os << "(poly_flip_not_>= _ _ "
+ << "(poly_form_not _ _ "
+ << ProofManager::getLitName(antecedent.negate(),
+ linearityWitnessPrefix)
+ << " " << ProofManager::getLitName(antecedent.negate(), "")
+ << "))";
+ break;
+ }
+ case kind::GEQ:
+ {
+ os << "(poly_form _ _ "
+ << ProofManager::getLitName(antecedent.negate(),
+ linearityWitnessPrefix)
+ << " " << ProofManager::getLitName(antecedent.negate(), "") << ")";
+ break;
+ }
+ default: Unreachable();
+ }
+ }
+
+ /* Combine linear polynomial constraints to derive a contradiction.
+ *
+ * The linear polynomial constraints are refered to as **antecedents**,
+ * since they are antecedents to the contradiction.
+ *
+ * The structure of the combination is a tree
+ *
+ * (=> <=)
+ * |
+ * + 0
+ * / \
+ * * + 1
+ * / \
+ * * + 2
+ * / \
+ * * ... i
+ * \
+ * + n-1
+ * / \
+ * * (0 >= 0)
+ *
+ * Where each * is a linearized antecedant being scaled by a farkas
+ * coefficient and each + is the sum of inequalities. The tricky bit is that
+ * each antecedent can be strict (>) or relaxed (>=) and the axiom used for
+ * each * and + depends on this... The axiom for * depends on the
+ * strictness of its linear polynomial input, and the axiom for + depends
+ * on the strictness of **both** its inputs. The contradiction axiom is
+ * also a function of the strictness of its input.
+ *
+ * There are n *s and +s and we precompute
+ * 1. The strictness of the ith antecedant (`ith_antecedent_is_strict`)
+ * 2. The strictness of the right argument of the ith sum
+ * (`ith_acc_is_strict`)
+ * 3. The strictness of the final result (`strict_contradiction`)
+ *
+ * Precomupation is helpful since
+ * the computation is post-order,
+ * but printing is pre-order.
+ */
+ std::vector<bool> ith_antecedent_is_strict(nAntecedents, false);
+ std::vector<bool> ith_acc_is_strict(nAntecedents, false);
+ for (int i = nAntecedents - 1; i >= 0; --i)
+ {
+ ith_antecedent_is_strict[i] = conflict[i].getKind() == kind::NOT;
+ if (i == (int)nAntecedents - 1)
+ {
+ ith_acc_is_strict[i] = false;
+ }
+ else
+ {
+ ith_acc_is_strict[i] =
+ ith_acc_is_strict[i + 1] || ith_antecedent_is_strict[i + 1];
+ }
+ }
+ bool strict_contradiction =
+ ith_acc_is_strict[0] || ith_antecedent_is_strict[0];
+
+ // Now, print the proof
+ os << "\n; Farkas Combination";
+ // Choose the appropriate contradiction axiom
+ os << "\n (lra_contra_" << (strict_contradiction ? ">" : ">=") << " _ ";
+ for (size_t i = 0; i != nAntecedents; ++i)
+ {
+ const Node& lit = conflict[i];
+ const char* ante_op = ith_antecedent_is_strict[i] ? ">" : ">=";
+ const char* acc_op = ith_acc_is_strict[i] ? ">" : ">=";
+ os << "\n (lra_add_" << ante_op << "_" << acc_op << " _ _ _ ";
+ os << "\n (lra_mul_c_" << ante_op << " _ _ ";
+ printRational(os, (*farkasCoefficients)[i].abs());
+ os << " " << ProofManager::getLitName(lit.negate(), linearizedProofPrefix)
+ << ")"
+ << " ; " << lit;
+ }
+
+ // The basis, at least, is always the same...
+ os << "\n (lra_axiom_>= 0/1)";
+ std::fill_n(std::ostream_iterator<char>(os),
+ nAntecedents,
+ ')'); // close lra_add_*_*
+ os << ")"; // close lra_contra_*
+
+ os << lemmaParen.str(); // close normalizers and proof-normalizers
+ }
+ else
+ {
+ os << "\n; Arithmetic proofs which use reasoning more complex than Farkas "
+ "proofs are currently unsupported\n(clausify_false trust)\n";
}
- os <<"\n";
- //os << " (clausify_false trust)";
- ArithProof::printTheoryLemmaProof(lemma, os, paren, map);
}
void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
}
void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
- for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
+ for (ExprSet::const_iterator it = d_declarations.begin();
+ it != d_declarations.end();
+ ++it)
+ {
Expr term = *it;
Assert(term.isVariable());
- os << "(% " << ProofManager::sanitize(term) << " ";
- os << "(term ";
- os << term.getType() << ")\n";
+ os << "(% " << ProofManager::sanitize(term) << " var_real\n";
+ os << "(@ " << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term)
+ << " ";
+ os << "(a_var_real " << ProofManager::sanitize(term) << ")\n";
+ paren << ")";
paren << ")";
}
}
ExprSet d_declarations; // all the variable/function declarations
/**
- * @brief Where farkas proofs of lemmas are stored.
+ * Where farkas proofs of lemmas are stored.
*/
proof::ArithProofRecorder d_recorder;
std::ostream& os,
const ProofLetMap& map) override;
void printOwnedSort(Type type, std::ostream& os) override;
+
+ /**
+ * Print a rational number in LFSC format.
+ * e.g. 5/8 or (~ 1/1)
+ *
+ * @param o ostream to print to.
+ * @param r the rational to print
+ */
+ static void printRational(std::ostream& o, const Rational& r);
+
+ /**
+ * Print a value of type poly_formula_norm
+ *
+ * @param o ostream to print to
+ * @param n node (asserted to be of the form [linear polynomial >= constant])
+ */
+ static void printLinearPolynomialPredicateNormalizer(std::ostream& o,
+ const Node& n);
+
+ /**
+ * Print a value of type poly_norm
+ *
+ * @param o ostream to print to
+ * @param n node (asserted to be a linear polynomial)
+ */
+ static void printLinearPolynomialNormalizer(std::ostream& o, const Node& n);
+
+ /**
+ * Print a value of type poly_norm
+ *
+ * @param o ostream to print to
+ * @param n node (asserted to be a linear monomial)
+ */
+ static void printLinearMonomialNormalizer(std::ostream& o, const Node& n);
+
+ /**
+ * Print a LFSC rational
+ *
+ * @param o ostream to print to
+ * @param n node (asserted to be a const rational)
+ */
+ static void printConstRational(std::ostream& o, const Node& n);
+
+ /**
+ * print the pn_var normalizer for n (type poly_norm)
+ *
+ * @param o the ostream to print to
+ * @param n the node to print (asserted to be a variable)
+ */
+ static void printVariableNormalizer(std::ostream& o, const Node& n);
+ /**
+ * print a proof of the lemma
+ *
+ * First, we print linearity witnesses, i.e. witnesses that each literal has
+ * the form:
+ * [linear polynomial] >= 0 OR
+ * [linear polynomial] > 0
+ *
+ * Then we use those witnesses to prove that the above linearized constraints
+ * hold.
+ *
+ * Then we use the farkas coefficients to combine the literals into a
+ * variable-free contradiction. The literals may be a mix of strict and
+ * relaxed inequalities.
+ *
+ * @param lemma the set of literals disjoined in the lemma
+ * @param os stream to print the proof to
+ * @param paren global closing stream (unused)
+ * @param map let map (unused)
+ */
void printTheoryLemmaProof(std::vector<Expr>& lemma,
std::ostream& os,
std::ostream& paren,
void ArithProofRecorder::saveFarkasCoefficients(
Node conflict, theory::arith::RationalVectorCP farkasCoefficients)
{
+ // Verify that the conflict is a conjuction of (possibly negated) real bounds
+ // Verify that the conflict is a conjunciton ...
Assert(conflict.getKind() == kind::AND);
Assert(conflict.getNumChildren() == farkasCoefficients->size());
- for (size_t i = 0; i < conflict.getNumChildren(); ++i)
+ for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren; ++i)
{
const Node& child = conflict[i];
- Assert(child.getType().isBoolean() && child[0].getType().isReal());
+ // ... of possibly negated ...
+ const Node& nonNegativeChild =
+ child.getKind() == kind::NOT ? child[0] : child;
+ // ... real bounds
+ Assert(nonNegativeChild.getType().isBoolean()
+ && nonNegativeChild[0].getType().isReal());
}
Debug("pf::arith") << "Saved Farkas Coefficients:" << std::endl;
if (Debug.isOn("pf::arith"))
{
- for (size_t i = 0; i < conflict.getNumChildren(); ++i)
+ for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren;
+ ++i)
{
const Node& child = conflict[i];
const Rational& r = (*farkasCoefficients)[i];
return getProofType() == FarkasAP;
}
+bool Constraint::hasSimpleFarkasProof() const
+{
+ Debug("constraints::hsfp") << "hasSimpleFarkasProof " << this << std::endl;
+ if (!hasFarkasProof())
+ {
+ Debug("constraints::hsfp") << "There is no simple Farkas proof because "
+ "there is no farkas proof."
+ << std::endl;
+ return false;
+ }
+ const ConstraintRule& rule = getConstraintRule();
+ AntecedentId antId = rule.d_antecedentEnd;
+ ConstraintCP antecdent = d_database->getAntecedent(antId);
+ while (antecdent != NullConstraint)
+ {
+ if (antecdent->getProofType() != AssumeAP)
+ {
+ Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there "
+ "is an antecdent w/ rule ";
+ antecdent->getConstraintRule().print(Debug("constraints::hsfp"));
+ Debug("constraints::hsfp") << std::endl;
+ return false;
+ }
+ --antId;
+ antecdent = d_database->getAntecedent(antId);
+ }
+ return true;
+}
+
bool Constraint::hasIntHoleProof() const {
return getProofType() == IntHoleAP;
}
out << d_constraint << std::endl;
out << "d_proofType= " << d_proofType << ", " << std::endl;
out << "d_antecedentEnd= "<< d_antecedentEnd << std::endl;
-
- if(d_constraint != NullConstraint){
+
+ if (d_constraint != NullConstraint && d_antecedentEnd != AntecedentIdSentinel)
+ {
const ConstraintDatabase& database = d_constraint->getDatabase();
size_t coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffs->size()-1 : 0;
out << " * (" << *(d_constraint->getNegation()) << ")";
out << " [not d_constraint] " << endl;
}
- out << "}";
+ out << "}";
}
bool Constraint::wellFormedFarkasProof() const {
Assert(!hasProof());
Assert(negationHasProof() == nowInConflict);
Assert(a->hasProof());
+ Debug("pf::arith") << "impliedByIntHole(" << this << ", " << a << ")"
+ << std::endl;
d_database->d_antecedents.push_back(NullConstraint);
d_database->d_antecedents.push_back(a);
}
Node Constraint::externalExplainConflict() const{
+ Debug("pf::arith") << this << std::endl;
Assert(inConflict());
NodeBuilder<> nb(kind::AND);
externalExplainByAssertions(nb);
Assert(!isAssumption() || assertedToTheTheory());
Assert(!isInternalAssumption());
+ if (Debug.isOn("pf::arith"))
+ {
+ Debug("pf::arith") << "Explaining: " << this << " with rule ";
+ getConstraintRule().print(Debug("pf::arith"));
+ Debug("pf::arith") << std::endl;
+ }
+
if(assertedBefore(order)){
nb << getWitness();
}else if(hasEqualityEngineProof()){
ConstraintCP antecedent = d_database->d_antecedents[p];
while(antecedent != NullConstraint){
+ Debug("pf::arith") << "Explain " << antecedent << std::endl;
antecedent->externalExplain(nb, order);
--p;
antecedent = d_database->d_antecedents[p];
struct ConstraintRule {
ConstraintP d_constraint;
ArithProofType d_proofType;
- AntecedentId d_antecedentEnd;
+ AntecedentId d_antecedentEnd;
/**
* In this comment, we abbreviate ConstraintDatabase::d_antecedents
*
* This list is always empty if proofs are not enabled.
*
- * If proofs are enabled, the proof of constraint c at p in ans[p] of length n is
- * (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
- *
- * Farkas' proofs show a contradiction with the negation of c, c_not = c->getNegation().
+ * If proofs are enabled, the proof of constraint c at p in ans[p] of length n
+ * is (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
+ *
+ * Farkas' proofs show a contradiction with the negation of c, c_not =
+ * c->getNegation().
*
- * We treat the position for NullConstraint (p-n) as the position for the farkas
- * coefficient for so we pretend c_not is ans[p-n].
- * So this correlation for the constraints we are going to use:
- * (c_not, ans[p-(n-1)], ... , ans[p-1], ans[p])
- * With the coefficients at positions:
- * (fc[0], fc[1)], ... fc[n])
+ * We treat the position for NullConstraint (p-n) as the position for the
+ * farkas coefficient for so we pretend c_not is ans[p-n]. So this correlation
+ * for the constraints we are going to use: (c_not, ans[p-n+(1)], ... ,
+ * ans[p-n+(n-1)], ans[p-n+(n)]) With the coefficients at positions: (fc[0],
+ * fc[1)], ... fc[n])
*
- * The index of the constraints in the proof are {i | i <= 0 <= n] } (with c_not being p-n).
- * Partition the indices into L, U, and E, the lower bounds, the upper bounds and equalities.
+ * The index of the constraints in the proof are {i | i <= 0 <= n] } (with
+ * c_not being p-n). Partition the indices into L, U, and E, the lower bounds,
+ * the upper bounds and equalities.
*
- * We standardize the proofs to be upper bound oriented following the convention:
- * A x <= b
- * with the proof witness of the form
- * (lambda) Ax <= (lambda) b and lambda >= 0.
+ * We standardize the proofs to be upper bound oriented following the
+ * convention: A x <= b with the proof witness of the form (lambda) Ax <=
+ * (lambda) b and lambda >= 0.
*
- * To accomplish this cleanly, the fc coefficients must be negative for lower bounds.
- * The signs of equalities can be either positive or negative.
+ * To accomplish this cleanly, the fc coefficients must be negative for lower
+ * bounds. The signs of equalities can be either positive or negative.
*
* Thus the proof corresponds to (with multiplication over inequalities):
* \sum_{u in U} fc[u] ans[p-n+u] + \sum_{e in E} fc[e] ans[p-n+e]
* + \sum_{l in L} fc[l] ans[p-n+l]
* |= 0 < 0
* where fc[u] > 0, fc[l] < 0, and fc[e] != 0 (i.e. it can be either +/-).
- *
+ *
* There is no requirement that the proof is minimal.
- * We do however use all of the constraints by requiring non-zero coefficients.
+ * We do however use all of the constraints by requiring non-zero
+ * coefficients.
*/
#if IS_PROOFS_BUILD
RationalVectorCP d_farkasCoefficients;
}; /* class ConstraintRule */
class Constraint {
-private:
- /** The ArithVar associated with the constraint. */
- const ArithVar d_variable;
-
- /** The type of the Constraint. */
- const ConstraintType d_type;
-
- /** The DeltaRational value with the constraint. */
- const DeltaRational d_value;
-
- /** A pointer to the associated database for the Constraint. */
- ConstraintDatabase* d_database;
-
- /**
- * The node to be communicated with the TheoryEngine.
- *
- * This is not context dependent, but may be set once.
- *
- * This must be set if the constraint canBePropagated().
- * This must be set if the constraint assertedToTheTheory().
- * Otherwise, this may be null().
- */
- Node d_literal;
-
- /** Pointer to the negation of the Constraint. */
- ConstraintP d_negation;
-
- /**
- * This is true if the associated node can be propagated.
- *
- * This should be enabled if the node has been preregistered.
- *
- * Sat Context Dependent.
- * This is initially false.
- */
- bool d_canBePropagated;
-
- /**
- * This is the order the constraint was asserted to the theory.
- * If this has been set, the node can be used in conflicts.
- * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the
- * explanation of d.
- *
- * This should be set after the literal is dequeued by Theory::get().
- *
- * Sat Context Dependent.
- * This is initially AssertionOrderSentinel.
- */
- AssertionOrder d_assertionOrder;
-
- /**
- * This is guaranteed to be on the fact queue.
- * For example if x + y = x + 1 is on the fact queue, then use this
- */
- TNode d_witness;
-
- /**
- * The position of the constraint in the constraint rule id.
- *
- * Sat Context Dependent.
- * This is initially
- */
- ConstraintRuleID d_crid;
-
-
- /**
- * True if the equality has been split.
- * Only meaningful if ConstraintType == Equality.
- *
- * User Context Dependent.
- * This is initially false.
- */
- bool d_split;
-
- /**
- * Position in sorted constraint set for the variable.
- * Unset if d_type is Disequality.
- */
- SortedConstraintMapIterator d_variablePosition;
friend class ConstraintDatabase;
+ public:
/**
* This begins construction of a minimal constraint.
*
*/
~Constraint();
- /** Returns true if the constraint has been initialized. */
- bool initialized() const;
-
- /**
- * This initializes the fields that cannot be set in the constructor due to
- * circular dependencies.
- */
- void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation);
-
-
-
- class ConstraintRuleCleanup {
- public:
- inline void operator()(ConstraintRule* crp){
- Assert(crp != NULL);
- ConstraintP constraint = crp->d_constraint;
- Assert(constraint->d_crid != ConstraintRuleIdSentinel);
- constraint->d_crid = ConstraintRuleIdSentinel;
-
- PROOF(if(crp->d_farkasCoefficients != RationalVectorCPSentinel){
- delete crp->d_farkasCoefficients;
- });
- }
- };
-
- class CanBePropagatedCleanup {
- public:
- inline void operator()(ConstraintP* p){
- ConstraintP constraint = *p;
- Assert(constraint->d_canBePropagated);
- constraint->d_canBePropagated = false;
- }
- };
-
- class AssertionOrderCleanup {
- public:
- inline void operator()(ConstraintP* p){
- ConstraintP constraint = *p;
- Assert(constraint->assertedToTheTheory());
- constraint->d_assertionOrder = AssertionOrderSentinel;
- constraint->d_witness = TNode::null();
- Assert(!constraint->assertedToTheTheory());
- }
- };
-
- class SplitCleanup {
- public:
- inline void operator()(ConstraintP* p){
- ConstraintP constraint = *p;
- Assert(constraint->d_split);
- constraint->d_split = false;
- }
- };
-
- /**
- * Returns true if the node is safe to garbage collect.
- * Both it and its negation must have no context dependent data set.
- */
- bool safeToGarbageCollect() const;
-
- /**
- * Returns true if the constraint has no context dependent data set.
- */
- bool contextDependentDataIsSet() const;
-
- /**
- * Returns true if the node correctly corresponds to the constraint that is
- * being set.
- */
- bool sanityChecking(Node n) const;
-
- /** Returns a reference to the map for d_variable. */
- SortedConstraintMap& constraintSet() const;
-
- /** Returns coefficients for the proofs for farkas cancellation. */
- static std::pair<int, int> unateFarkasSigns(ConstraintCP a, ConstraintCP b);
-
-
-public:
-
static ConstraintType constraintTypeOfComparison(const Comparison& cmp);
inline ConstraintType getType() const {
/** Returns true if the node has a Farkas' proof. */
bool hasFarkasProof() const;
+ /**
+ * @brief Returns whether this constraint is provable using a Farkas
+ * proof that has input assertions as its antecedents.
+ *
+ * An example of a constraint that has a simple Farkas proof:
+ * x <= 0 proven from x + y <= 0 and x - y <= 0.
+ *
+ * An example of a constraint that does not have a simple Farkas proof:
+ * x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y
+ * (since integer reasoning is also required!).
+ * Another example of a constraint that might be proven without a simple
+ * Farkas proof:
+ * x < 0 proven from not(x == 0) and not(x > 0).
+ *
+ * This could be proven internally by the arithmetic theory using
+ * `TrichotomyAP` as the proof type.
+ *
+ */
+ bool hasSimpleFarkasProof() const;
+
/** Returns true if the node has a int hole proof. */
bool hasIntHoleProof() const;
*/
Node externalExplainConflict() const;
-private:
- Node externalExplain(AssertionOrder order) const;
-
- /**
- * Returns an explanation of that was assertedBefore(order).
- * The constraint must have a proof.
- * The constraint cannot be selfExplaining().
- *
- * This is the minimum fringe of the implication tree
- * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
- */
- void externalExplain(NodeBuilder<>& nb, AssertionOrder order) const;
-
- static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
-
-public:
/** The constraint is known to be true. */
inline bool hasProof() const {
*/
ConstraintP getFloor();
-
static ConstraintP makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r);
const ValueCollection& getValueCollection() const;
*/
const ConstraintDatabase& getDatabase() const;
-private:
-
/** Returns the constraint rule at the position. */
const ConstraintRule& getConstraintRule() const;
-
+
+ private:
+ /** Returns true if the constraint has been initialized. */
+ bool initialized() const;
+
+ /**
+ * This initializes the fields that cannot be set in the constructor due to
+ * circular dependencies.
+ */
+ void initialize(ConstraintDatabase* db,
+ SortedConstraintMapIterator v,
+ ConstraintP negation);
+
+ class ConstraintRuleCleanup
+ {
+ public:
+ inline void operator()(ConstraintRule* crp)
+ {
+ Assert(crp != NULL);
+ ConstraintP constraint = crp->d_constraint;
+ Assert(constraint->d_crid != ConstraintRuleIdSentinel);
+ constraint->d_crid = ConstraintRuleIdSentinel;
+
+ PROOF(if (crp->d_farkasCoefficients != RationalVectorCPSentinel) {
+ delete crp->d_farkasCoefficients;
+ });
+ }
+ };
+
+ class CanBePropagatedCleanup
+ {
+ public:
+ inline void operator()(ConstraintP* p)
+ {
+ ConstraintP constraint = *p;
+ Assert(constraint->d_canBePropagated);
+ constraint->d_canBePropagated = false;
+ }
+ };
+
+ class AssertionOrderCleanup
+ {
+ public:
+ inline void operator()(ConstraintP* p)
+ {
+ ConstraintP constraint = *p;
+ Assert(constraint->assertedToTheTheory());
+ constraint->d_assertionOrder = AssertionOrderSentinel;
+ constraint->d_witness = TNode::null();
+ Assert(!constraint->assertedToTheTheory());
+ }
+ };
+
+ class SplitCleanup
+ {
+ public:
+ inline void operator()(ConstraintP* p)
+ {
+ ConstraintP constraint = *p;
+ Assert(constraint->d_split);
+ constraint->d_split = false;
+ }
+ };
+
+ /**
+ * Returns true if the node is safe to garbage collect.
+ * Both it and its negation must have no context dependent data set.
+ */
+ bool safeToGarbageCollect() const;
+
+ /**
+ * Returns true if the constraint has no context dependent data set.
+ */
+ bool contextDependentDataIsSet() const;
+
+ /**
+ * Returns true if the node correctly corresponds to the constraint that is
+ * being set.
+ */
+ bool sanityChecking(Node n) const;
+
+ /** Returns a reference to the map for d_variable. */
+ SortedConstraintMap& constraintSet() const;
+
+ /** Returns coefficients for the proofs for farkas cancellation. */
+ static std::pair<int, int> unateFarkasSigns(ConstraintCP a, ConstraintCP b);
+
+ Node externalExplain(AssertionOrder order) const;
+
+ /**
+ * Returns an explanation of that was assertedBefore(order).
+ * The constraint must have a proof.
+ * The constraint cannot be selfExplaining().
+ *
+ * This is the minimum fringe of the implication tree
+ * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
+ */
+ void externalExplain(NodeBuilder<>& nb, AssertionOrder order) const;
+
+ static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
+
inline ArithProofType getProofType() const {
return getConstraintRule().d_proofType;
}
*/
bool wellFormedFarkasProof() const;
-
+
+ /** The ArithVar associated with the constraint. */
+ const ArithVar d_variable;
+
+ /** The type of the Constraint. */
+ const ConstraintType d_type;
+
+ /** The DeltaRational value with the constraint. */
+ const DeltaRational d_value;
+
+ /** A pointer to the associated database for the Constraint. */
+ ConstraintDatabase* d_database;
+
+ /**
+ * The node to be communicated with the TheoryEngine.
+ *
+ * This is not context dependent, but may be set once.
+ *
+ * This must be set if the constraint canBePropagated().
+ * This must be set if the constraint assertedToTheTheory().
+ * Otherwise, this may be null().
+ */
+ Node d_literal;
+
+ /** Pointer to the negation of the Constraint. */
+ ConstraintP d_negation;
+
+ /**
+ * This is true if the associated node can be propagated.
+ *
+ * This should be enabled if the node has been preregistered.
+ *
+ * Sat Context Dependent.
+ * This is initially false.
+ */
+ bool d_canBePropagated;
+
+ /**
+ * This is the order the constraint was asserted to the theory.
+ * If this has been set, the node can be used in conflicts.
+ * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the
+ * explanation of d.
+ *
+ * This should be set after the literal is dequeued by Theory::get().
+ *
+ * Sat Context Dependent.
+ * This is initially AssertionOrderSentinel.
+ */
+ AssertionOrder d_assertionOrder;
+
+ /**
+ * This is guaranteed to be on the fact queue.
+ * For example if x + y = x + 1 is on the fact queue, then use this
+ */
+ TNode d_witness;
+
+ /**
+ * The position of the constraint in the constraint rule id.
+ *
+ * Sat Context Dependent.
+ * This is initially
+ */
+ ConstraintRuleID d_crid;
+
+ /**
+ * True if the equality has been split.
+ * Only meaningful if ConstraintType == Equality.
+ *
+ * User Context Dependent.
+ * This is initially false.
+ */
+ bool d_split;
+
+ /**
+ * Position in sorted constraint set for the variable.
+ * Unset if d_type is Disequality.
+ */
+ SortedConstraintMapIterator d_variablePosition;
+
}; /* class ConstraintValue */
std::ostream& operator<<(std::ostream& o, const Constraint& c);
/** Outputs conflicts to the output channel. */
void TheoryArithPrivate::outputConflicts(){
+ Debug("arith::conflict") << "outputting conflicts" << std::endl;
Assert(anyConflict());
static unsigned int conflicts = 0;
Assert(!d_conflicts.empty());
for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
ConstraintCP confConstraint = d_conflicts[i];
+ bool hasProof = confConstraint->hasProof();
Assert(confConstraint->inConflict());
+ const ConstraintRule& pf = confConstraint->getConstraintRule();
+ if (Debug.isOn("arith::conflict"))
+ {
+ pf.print(std::cout);
+ std::cout << std::endl;
+ }
Node conflict = confConstraint->externalExplainConflict();
++conflicts;
Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
- // << "("<<conflicts<<")"
- << endl;
+ << " has proof: " << hasProof << endl;
+ PROOF(if (d_containing.d_proofRecorder && confConstraint->hasFarkasProof()
+ && pf.d_farkasCoefficients->size()
+ == conflict.getNumChildren()) {
+ // The Farkas coefficients and the children of `conflict` seem to be in
+ // opposite orders... There is some relevant documentation in the
+ // comment for the d_farkasCoefficients field in "constraint.h"
+ //
+ // Anyways, we reverse the children in `conflict` here.
+ NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND);
+ for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren;
+ ++i)
+ {
+ conflictInFarkasCoefficientOrder
+ << conflict[conflict.getNumChildren() - i - 1];
+ }
+
+ Assert(conflict.getNumChildren() == pf.d_farkasCoefficients->size());
+ d_containing.d_proofRecorder->saveFarkasCoefficients(
+ conflictInFarkasCoefficientOrder, pf.d_farkasCoefficients);
+ })
if(Debug.isOn("arith::normalize::external")){
conflict = flattenAndSort(conflict);
Debug("arith::conflict") << "(normalized to) " << conflict << endl;
(d_containing.d_out)->conflict(bb);
}
}
+
void TheoryArithPrivate::outputLemma(TNode lem) {
+ Debug("arith::lemma") << "Arith Lemma: " << lem << std::endl;
(d_containing.d_out)->lemma(lem);
}
PROOF(d_farkasBuffer.clear());
RationalVectorP coeffs = NULLPROOF(&d_farkasBuffer);
-
+
+ // After invoking `propegateRow`:
+ // * coeffs[0] is for implied
+ // * coeffs[i+1] is for explain[i]
d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs);
if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
Node implication = implied->externalImplication(explain);
Node clause = flattenImplication(implication);
+ PROOF(if (d_containing.d_proofRecorder
+ && coeffs != RationalVectorCPSentinel
+ && coeffs->size() == clause.getNumChildren()) {
+ Debug("arith::prop") << "implied : " << implied << std::endl;
+ Debug("arith::prop") << "implication: " << implication << std::endl;
+ Debug("arith::prop") << "coeff len: " << coeffs->size() << std::endl;
+ Debug("arith::prop") << "exp : " << explain << std::endl;
+ Debug("arith::prop") << "clause : " << clause << std::endl;
+ Debug("arith::prop")
+ << "clause len: " << clause.getNumChildren() << std::endl;
+ Debug("arith::prop") << "exp len: " << explain.size() << std::endl;
+ // Using the information from the above comment we assemble a conflict
+ // AND in coefficient order
+ NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND);
+ conflictInFarkasCoefficientOrder << implication[1].negate();
+ for (const Node& antecedent : implication[0])
+ {
+ Debug("arith::prop") << " ante: " << antecedent << std::endl;
+ conflictInFarkasCoefficientOrder << antecedent;
+ }
+
+ Assert(coeffs != RationalVectorPSentinel);
+ Assert(conflictInFarkasCoefficientOrder.getNumChildren()
+ == coeffs->size());
+ d_containing.d_proofRecorder->saveFarkasCoefficients(
+ conflictInFarkasCoefficientOrder, coeffs);
+ })
outputLemma(clause);
}else{
Assert(!implied->negationHasProof());
projects / cvc5.git / commitdiff