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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
/********************* */
/*! \file expr_manager_public.h
** \verbatim
** Top contributors (to current version):
** Christopher L. Conway, Tim King, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 Public black-box testing of CVC4::ExprManager.
**
** Public black-box testing of CVC4::ExprManager.
**/
#include <cxxtest/TestSuite.h>
#include <sstream>
#include <string>
#include "expr/expr_manager.h"
#include "expr/expr.h"
#include "base/exception.h"
using namespace CVC4;
using namespace CVC4::kind;
using namespace std;
class ExprManagerPublic : public CxxTest::TestSuite {
private:
ExprManager* d_exprManager;
void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) {
std::vector<Expr> worklist;
worklist.push_back(expr);
unsigned int childrenFound = 0;
while( !worklist.empty() ) {
Expr current = worklist.back();
worklist.pop_back();
if( current.getKind() == kind ) {
for( unsigned int i = 0; i < current.getNumChildren(); ++i ) {
worklist.push_back( current[i] );
}
} else {
childrenFound++;
}
}
TS_ASSERT_EQUALS( childrenFound, numChildren );
}
std::vector<Expr> mkVars(Type type, unsigned int n) {
std::vector<Expr> vars;
for( unsigned int i = 0; i < n; ++i ) {
vars.push_back( d_exprManager->mkVar(type) );
}
return vars;
}
public:
void setUp() override { d_exprManager = new ExprManager; }
void tearDown() override
{
try
{
delete d_exprManager;
}
catch (Exception e)
{
cerr << "Exception during tearDown():" << endl << e;
throw;
}
}
void testMkAssociative() {
try {
std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 294821);
Expr n = d_exprManager->mkAssociative(AND,vars);
checkAssociative(n,AND,vars.size());
vars = mkVars(d_exprManager->booleanType(), 2);
n = d_exprManager->mkAssociative(OR,vars);
checkAssociative(n,OR,2);
} catch( Exception& e ) {
cerr << "Exception in testMkAssociative(): " << endl << e;
throw;
}
}
void testMkAssociative2() {
try {
std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 2);
Expr n = d_exprManager->mkAssociative(OR,vars);
checkAssociative(n,OR,2);
} catch( Exception& e ) {
cerr << "Exception in testMkAssociative2(): " << endl << e;
throw;
}
}
void testMkAssociative3() {
try {
//unsigned int numVars = d_exprManager->maxArity(AND) + 1;
unsigned int numVars = (1<<16) + 1;
std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), numVars);
Expr n = d_exprManager->mkAssociative(AND,vars);
checkAssociative(n,AND,numVars);
} catch( Exception& e ) {
cerr << "Exception in testMkAssociative3(): " << endl << e;
throw;
}
}
void testMkAssociativeTooFew() {
std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 1);
TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), IllegalArgumentException);
}
void testMkAssociativeBadKind() {
std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10);
TS_ASSERT_THROWS( d_exprManager->mkAssociative(LEQ,vars), IllegalArgumentException);
}
};
|
