diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/quantifiers/quantifiers_rewriter.h | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h new file mode 100644 index 000000000..8c037d30b --- /dev/null +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -0,0 +1,88 @@ +/********************* */ +/*! \file quantifiers_rewriter.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Rewriter for the theory of inductive quantifiers + ** + ** Rewriter for the theory of inductive quantifiers. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H + +#include "theory/rewriter.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +// attribute for "contains instantiation constants from" +struct NestedQuantAttributeId {}; +typedef expr::Attribute<NestedQuantAttributeId, Node> NestedQuantAttribute; + +class QuantifiersRewriter { +public: + static bool isClause( Node n ); + static bool isLiteral( Node n ); + static bool isCube( Node n ); +private: + static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); + static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); + static void computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); + static bool hasArg( std::vector< Node >& args, Node n ); + static void setNestedQuantifiers( Node n, Node q ); + static void computeArgs( std::map< Node, bool >& active, Node n ); + static Node computeClause( Node n ); +private: + static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); + static Node computeNNF( Node body ); + static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); + static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); + static Node computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq ); +private: + enum{ + COMPUTE_NNF = 0, + COMPUTE_PRE_SKOLEM, + COMPUTE_PRENEX, + COMPUTE_VAR_ELIMINATION, + //COMPUTE_FLATTEN_ARGS_UF, + COMPUTE_CNF, + COMPUTE_LAST + }; + static Node computeOperation( Node f, int computeOption ); +public: + static RewriteResponse preRewrite(TNode in); + static RewriteResponse postRewrite(TNode in); + static Node rewriteEquality(TNode equality) { + return postRewrite(equality).node; + } + static inline void init() {} + static inline void shutdown() {} +private: + /** options */ + static bool doMiniscopingNoFreeVar(); + static bool doMiniscopingAnd(); + static bool doOperation( Node f, bool isNested, int computeOption, bool duringRewrite = true ); +public: + static Node rewriteQuants( Node n, bool isNested = false, bool duringRewrite = true ); + static Node rewriteQuant( Node n, bool isNested = false, bool duringRewrite = true ); +};/* class QuantifiersRewriter */ + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ + |