1 /********************* */
2 /*! \file local_theory_ext.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief local theory extensions util
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H
18 #define __CVC4__THEORY__LOCAL_THEORY_EXT_H
20 #include "theory/quantifiers_engine.h"
21 #include "context/cdo.h"
25 namespace quantifiers
{
29 class LtePartialInst
: public QuantifiersModule
{
31 // was this module invoked
35 //representatives per type
36 std::map
< TypeNode
, std::vector
< Node
> > d_reps
;
37 // should we instantiate quantifier
38 std::map
< Node
, bool > d_do_inst
;
39 // have we instantiated quantifier
40 std::map
< Node
, bool > d_inst
;
41 std::map
< Node
, std::vector
< Node
> > d_vars
;
42 std::map
< Node
, std::vector
< int > > d_pat_var_order
;
43 /** list of relevant quantifiers asserted in the current context */
44 std::vector
< Node
> d_lte_asserts
;
47 /** get instantiations */
48 void getInstantiations( std::vector
< Node
>& lemmas
);
49 void getPartialInstantiations( std::vector
< Node
>& conj
, Node q
, Node bvl
,
50 std::vector
< Node
>& vars
, std::vector
< Node
>& inst
, std::vector
< TypeNode
>& types
, TermArgTrie
* curr
,
51 unsigned pindex
, unsigned paindex
, unsigned iindex
);
52 /** get eligible inst variables */
53 void getEligibleInstVars( Node n
, std::map
< Node
, bool >& vars
);
55 bool addVariableToPatternList( Node v
, std::vector
< int >& pat_var_order
, std::map
< Node
, int >& var_order
);
57 LtePartialInst( QuantifiersEngine
* qe
, context::Context
* c
);
58 /** determine whether this quantified formula will be reduced */
59 void preRegisterQuantifier( Node q
);
61 bool wasInvoked() { return d_wasInvoked
; }
63 /* whether this module needs to check this round */
64 bool needsCheck( Theory::Effort e
);
65 /* Call during quantifier engine's check */
66 void check( Theory::Effort e
, unsigned quant_e
);
67 /* Called for new quantifiers */
68 void registerQuantifier( Node q
) {}
70 bool checkComplete() { return !d_wasInvoked
; }
71 void assertNode( Node n
) {}
72 /** Identify this module (for debugging, dynamic configuration, etc..) */
73 std::string
identify() const { return "LtePartialInst"; }