diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-10-07 22:49:45 -0400 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-10-07 22:54:01 -0400 |
commit | 867e79e0823c689889224078dfaebec03aee9730 (patch) | |
tree | b4c8281beda8f5263e32145e22dc58c7b1b8209a /src/proof/theory_proof.h | |
parent | 1a56238b7ed75c6127293cb7c52d5b6b85245c64 (diff) |
first draft implementation of uf proofs with holes
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h new file mode 100644 index 000000000..ac8f9f7b8 --- /dev/null +++ b/src/proof/theory_proof.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \file theory_proof.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A manager for UfProofs. + ** + ** A manager for UfProofs. + ** + ** + **/ + + +#ifndef __CVC4__THEORY_PROOF_H +#define __CVC4__THEORY_PROOF_H + +#include "cvc4_private.h" +#include "util/proof.h" +#include "expr/expr.h" +#include <ext/hash_set> +#include <iostream> + +namespace CVC4 { + + typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > AtomSet; + typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > TermSet; + typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; + + class TheoryProof { + protected: + AtomSet d_atomSet; + TermSet d_termDeclarations; + SortSet d_sortDeclarations; + void addDeclaration(Expr atom); + public: + TheoryProof(); + void addAtom(Expr atom); + virtual void printFormula(Expr atom, std::ostream& os) = 0; + virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; + }; + + class LFSCTheoryProof: public TheoryProof { + void printTerm(Expr term, std::ostream& os); + public: + virtual void printFormula(Expr atom, std::ostream& os); + virtual void printDeclarations(std::ostream& os, std::ostream& paren); + }; +} /* CVC4 namespace */ +#endif /* __CVC4__THEORY_PROOF_H */ |