diff options
Diffstat (limited to 'src/theory/quantifiers/fun_def_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/fun_def_engine.cpp | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp new file mode 100644 index 000000000..56214f540 --- /dev/null +++ b/src/theory/quantifiers/fun_def_engine.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file fun_def_process.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** 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 + ** + ** This class implements specialized techniques for (recursively) defined functions + **/ + +#include <vector> + +#include "theory/quantifiers/fun_def_engine.h" +#include "theory/rewriter.h" +#include "theory/quantifiers/term_database.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) { + +} + +/* whether this module needs to check this round */ +bool FunDefEngine::needsCheck( Theory::Effort e ) { + return e>=Theory::EFFORT_LAST_CALL; +} + +/* reset at a round */ +void FunDefEngine::reset_round( Theory::Effort e ){ + //TODO +} + +/* Call during quantifier engine's check */ +void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) { + //TODO +} + +/* Called for new quantifiers */ +void FunDefEngine::registerQuantifier( Node q ) { + //TODO +} + +/** called for everything that gets asserted */ +void FunDefEngine::assertNode( Node n ) { + //TODO +} |