diff options
Diffstat (limited to 'src/proof/arith_proof.h')
-rw-r--r-- | src/proof/arith_proof.h | 217 |
1 files changed, 0 insertions, 217 deletions
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h deleted file mode 100644 index 832afcae0..000000000 --- a/src/proof/arith_proof.h +++ /dev/null @@ -1,217 +0,0 @@ -/********************* */ -/*! \file arith_proof.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Guy Katz, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Arith proof - ** - ** Arith proof - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__ARITH__PROOF_H -#define CVC4__ARITH__PROOF_H - -#include <memory> -#include <unordered_set> - -#include "expr/expr.h" -#include "proof/arith_proof_recorder.h" -#include "proof/proof_manager.h" -#include "proof/theory_proof.h" -#include "theory/uf/equality_engine.h" - -namespace CVC4 { - -//proof object outputted by TheoryArith -class ProofArith : public Proof { - public: - ProofArith(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {} - void toStream(std::ostream& out) const override; - - private: - static void toStreamLFSC(std::ostream& out, TheoryProof* tp, - const theory::eq::EqProof& pf, - const ProofLetMap& map); - static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - const theory::eq::EqProof& pf, - unsigned tb, const ProofLetMap& map); - // it is simply an equality engine proof - std::shared_ptr<theory::eq::EqProof> d_proof; -}; - -namespace theory { -namespace arith { -class TheoryArith; -} -} - -typedef std::unordered_set<Type, TypeHashFunction > TypeSet; - - -class ArithProof : public TheoryProof { -protected: - // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations - - // TypeSet d_sorts; // all the uninterpreted sorts in this theory - ExprSet d_declarations; // all the variable/function declarations - - /** - * Where farkas proofs of lemmas are stored. - */ - proof::ArithProofRecorder d_recorder; - - theory::TheoryId getTheoryId() override; - - public: - ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine); - - void registerTerm(Expr term) override; -}; - -class LFSCArithProof : public ArithProof { -public: - LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine) - : ArithProof(arith, proofEngine) - {} - void printOwnedTermAsType(Expr term, - std::ostream& os, - const ProofLetMap& map, - TypeNode expectedType) override; - 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) - * - * @param o ostream to print to. - * @param r the rational to print - */ - 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 - * @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, - const ProofLetMap& map) override; - void printSortDeclarations(std::ostream& os, std::ostream& paren) override; - void printTermDeclarations(std::ostream& os, std::ostream& paren) override; - void printDeferredDeclarations(std::ostream& os, - std::ostream& paren) override; - void printAliasingDeclarations(std::ostream& os, - std::ostream& paren, - const ProofLetMap& globalLetMap) override; - - /** - * Given a node that is an arith literal (an arith comparison or negation - * thereof), prints a proof of that literal. - * - * If the node represents a tightenable bound (e.g. [Int] < 3) then it prints - * a proof of the tightening instead. (e.g. [Int] <= 2). - * - * @return a pair comprising: - * * the new node (after tightening) and - * * a string proving it. - */ - std::pair<Node, std::string> printProofAndMaybeTighten(const Node& bound); - - /** - * Return whether this node, when serialized to LFSC, has sort `Bool`. Otherwise, the sort is `formula`. - */ - bool printsAsBool(const Node& n) override; - - TypeNode equalityType(const Expr& left, const Expr& right) override; -}; - - -}/* CVC4 namespace */ - -#endif /* CVC4__ARITH__PROOF_H */ |