blob: 600c09a58284cdea3d8a9ee3a53a4e50f6382a9f (
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
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
|
/********************* */
/*! \file sygus_process_conj.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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 Implementation of techniqures for static preprocessing and analysis
** of sygus conjectures.
**/
#include "theory/quantifiers/sygus_process_conj.h"
#include <stack>
#include "expr/datatype.h"
#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
using namespace CVC4::kind;
using namespace std;
namespace CVC4 {
namespace theory {
namespace quantifiers {
CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) : d_qe(qe) {}
CegConjectureProcess::~CegConjectureProcess() {}
Node CegConjectureProcess::simplify(Node q)
{
Trace("sygus-process") << "Simplify conjecture : " << q << std::endl;
return q;
}
void CegConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
{
if (Trace.isOn("sygus-process"))
{
Trace("sygus-process") << "Process conjecture : " << n
<< " with candidates: " << std::endl;
for (unsigned i = 0; i < candidates.size(); i++)
{
Trace("sygus-process") << " " << candidates[i] << std::endl;
}
}
Node base;
if (n.getKind() == NOT && n[0].getKind() == FORALL)
{
base = n[0][1];
}
else
{
base = n;
}
std::vector<Node> conj;
if (base.getKind() == AND)
{
for (unsigned i = 0; i < base.getNumChildren(); i++)
{
conj.push_back(base[i]);
}
}
else
{
conj.push_back(base);
}
// initialize the information for synth funs
for (unsigned i = 0; i < candidates.size(); i++)
{
Node e = candidates[i];
// d_sf_info[e].d_arg_independent
}
// process the conjunctions
for (unsigned i = 0; i < conj.size(); i++)
{
processConjunct(conj[i]);
}
}
void CegConjectureProcess::processConjunct(Node c) {}
Node CegConjectureProcess::getSymmetryBreakingPredicate(
Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
{
return Node::null();
}
void CegConjectureProcess::debugPrint(const char* c) {}
} /* namespace CVC4::theory::quantifiers */
} /* namespace CVC4::theory */
} /* namespace CVC4 */
|
