1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
/********************* */
/*! \file inst_strategy_cbqi.h
** \verbatim
** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com>
** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief instantiator_arith_instantiator
**/
#include "cvc4_private.h"
#ifndef __CVC4__INST_STRATEGT_CBQI_H
#define __CVC4__INST_STRATEGT_CBQI_H
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/arith/arithvar_node_map.h"
#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
namespace arith {
class TheoryArith;
}
namespace datatypes {
class TheoryDatatypes;
}
namespace quantifiers {
class InstStrategySimplex : public InstStrategy{
protected:
/** calculate if we should process this quantifier */
bool calculateShouldProcess( Node f );
private:
/** reference to theory arithmetic */
arith::TheoryArith* d_th;
/** delta */
std::map< TypeNode, Node > d_deltas;
/** for each quantifier, simplex rows */
std::map< Node, std::vector< arith::ArithVar > > d_instRows;
/** tableaux */
std::map< arith::ArithVar, Node > d_tableaux_term;
std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;
/** ce tableaux */
std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;
/** get value */
Node getTableauxValue( Node n, bool minus_delta = false );
Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );
/** do instantiation */
bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );
bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
/** add term to row */
void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );
/** print debug */
void debugPrint( const char* c );
private:
/** */
int d_counter;
/** negative one */
Node d_negOne;
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
int process( Node f, Theory::Effort effort, int e );
public:
InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
~InstStrategySimplex(){}
/** identify */
std::string identify() const { return std::string("Simplex"); }
};
class InstStrategyDatatypesValue : public InstStrategy
{
protected:
/** calculate if we should process this quantifier */
bool calculateShouldProcess( Node f );
private:
/** reference to theory datatypes */
datatypes::TheoryDatatypes* d_th;
/** get value function */
Node getValueFor( Node n );
public:
//constructor
InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );
~InstStrategyDatatypesValue(){}
/** reset instantiation */
void processResetInstantiationRound( Theory::Effort effort );
/** process method, returns a status */
int process( Node f, Theory::Effort effort, int e );
/** identify */
std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
};/* class InstStrategy */
}
}
}
#endif
|
