blob: 334d70eea8d405bd7281723138db998a749a8a01 (
plain)
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
|
/********************* */
/*! \file theory_arrays_instantiator.cpp
** \verbatim
** Original author: ajreynol
** Major contributors: none
** 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 Implementation of theory_arrays_instantiator class
**/
#include "theory/theory_engine.h"
#include "theory/arrays/theory_arrays_instantiator.h"
#include "theory/arrays/theory_arrays.h"
using namespace std;
using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::arrays;
InstantiatorTheoryArrays::InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th) :
Instantiator( c, ie, th ){
}
void InstantiatorTheoryArrays::preRegisterTerm( Node t ){
}
void InstantiatorTheoryArrays::assertNode( Node assertion ){
Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl;
d_quantEngine->addTermToDatabase( assertion );
if( Options::current()->cbqi ){
if( assertion.hasAttribute(InstConstantAttribute()) ){
setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
}else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
}
}
}
void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort effort ){
}
int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e, int limitInst ){
return InstStrategy::STATUS_SAT;
}
|
