diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/theory/quantifiers/anti_skolem.h | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/theory/quantifiers/anti_skolem.h')
-rw-r--r-- | src/theory/quantifiers/anti_skolem.h | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h new file mode 100644 index 000000000..721371159 --- /dev/null +++ b/src/theory/quantifiers/anti_skolem.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \file anti_skolem.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief dynamic quantifiers splitting + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANT_ANTI_SKOLEM_H +#define __CVC4__THEORY__QUANT_ANTI_SKOLEM_H + +#include "theory/quantifiers_engine.h" +#include "context/cdo.h" +#include "theory/quantifiers/ce_guided_single_inv.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class QuantAntiSkolem : public QuantifiersModule { + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; +private: + std::map< Node, bool > d_quant_processed; + std::map< Node, SingleInvocationPartition > d_quant_sip; + std::map< Node, std::vector< TypeNode > > d_ask_types; + std::map< Node, std::vector< unsigned > > d_ask_types_index; + + class SkQuantTypeCache { + public: + std::map< TypeNode, SkQuantTypeCache > d_children; + std::vector< Node > d_quants; + void add( std::vector< TypeNode >& typs, Node q, unsigned index = 0 ); + void clear() { + d_children.clear(); + d_quants.clear(); + } + void sendLemmas( QuantAntiSkolem * ask ); + }; + SkQuantTypeCache d_sqtc; + + class CDSkQuantCache { + public: + CDSkQuantCache( context::Context* c ) : d_valid( c, false ){} + std::map< Node, CDSkQuantCache* > d_data; + context::CDO< bool > d_valid; + bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 ); + }; + CDSkQuantCache * d_sqc; +public: + bool sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected = true ); +public: + QuantAntiSkolem( QuantifiersEngine * qe ); + + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ) {} + void assertNode( Node n ) {} + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "QuantAntiSkolem"; } +}; + +} +} +} + +#endif |