1 /********************* */
2 /*! \file instantiation_engine.h
4 ** Original author: ajreynol
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Instantiation Engine classes
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
20 #define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
22 #include "theory/quantifiers_engine.h"
23 #include "theory/quantifiers/theory_quantifiers.h"
27 namespace quantifiers
{
29 class InstantiationEngine
: public QuantifiersModule
32 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
33 /** status of instantiation round (one of InstStrategy::STATUS_*) */
34 int d_inst_round_status
;
35 /** map from universal quantifiers to their counterexample literals */
36 std::map
< Node
, Node
> d_ce_lit
;
37 /** whether the instantiation engine should set incomplete if it cannot answer SAT */
40 bool hasAddedCbqiLemma( Node f
);
41 void addCbqiLemma( Node f
);
43 /** helper functions */
44 bool hasNonArithmeticVariable( Node f
);
45 bool hasApplyUf( Node f
);
46 /** whether to do CBQI for quantifier f */
47 bool doCbqi( Node f
);
49 /** do instantiation round */
50 bool doInstantiationRound( Theory::Effort effort
);
51 /** register literals of n, f is the quantifier it belongs to */
52 //void registerLiterals( Node n, Node f );
59 void debugSat( int reason
);
61 InstantiationEngine( QuantifiersEngine
* qe
, bool setIncomplete
= true );
62 ~InstantiationEngine(){}
64 void check( Theory::Effort e
);
65 void registerQuantifier( Node f
);
66 void assertNode( Node f
);
67 Node
explain(TNode n
){ return Node::null(); }
68 void propagate( Theory::Effort level
);
70 /** get the corresponding counterexample literal for quantified formula node n */
71 Node
getCounterexampleLiteralFor( Node f
) { return d_ce_lit
.find( f
)==d_ce_lit
.end() ? Node::null() : d_ce_lit
[ f
]; }
72 };/* class InstantiationEngine */
74 }/* CVC4::theory::quantifiers namespace */
75 }/* CVC4::theory namespace */
78 #endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */