diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-28 14:28:31 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-28 14:28:31 +0100 |
commit | 55323fd7283d758caf31e637be237d2416b86167 (patch) | |
tree | 250940ce676196591ddc35bed7291991545e6271 /src/theory/quantifiers/fun_def_process.h | |
parent | 3ff5a32a45f2830acc4600b38332a287db4cf60a (diff) |
Initial infrastructure for function definition quantifiers, internal parsing format for Smt2.
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.h')
-rw-r--r-- | src/theory/quantifiers/fun_def_process.h | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h new file mode 100644 index 000000000..c2d8aeb65 --- /dev/null +++ b/src/theory/quantifiers/fun_def_process.h @@ -0,0 +1,45 @@ +/********************* */ +/*! \file fun_def_process.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process steps for well-defined functions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H +#define __CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +//find finite models for well-defined functions +class FunDefFmf { +public: + FunDefFmf(){} + ~FunDefFmf(){} + + void simplify( std::vector< Node >& assertions, bool doRewrite = false ); +}; + + +} +} +} + +#endif |