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.cpp | |
parent | 3ff5a32a45f2830acc4600b38332a287db4cf60a (diff) |
Initial infrastructure for function definition quantifiers, internal parsing format for Smt2.
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.cpp')
-rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp new file mode 100644 index 000000000..c9dbb8d4b --- /dev/null +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -0,0 +1,31 @@ +/********************* */ +/*! \file fun_def_process.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): Kshitij Bansal + ** 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 Sort inference module + ** + ** This class implements pre-process steps for well-defined functions + **/ + +#include <vector> + +#include "theory/quantifiers/fun_def_process.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + + +void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { + +} |