Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of sygus abduction utility, which transforms an arbitrary
14 : : * input into an abduction problem.
15 : : */
16 : :
17 : : #include "theory/quantifiers/sygus/sygus_abduct.h"
18 : :
19 : : #include <sstream>
20 : :
21 : : #include "expr/dtype.h"
22 : : #include "expr/node_algorithm.h"
23 : : #include "expr/skolem_manager.h"
24 : : #include "theory/datatypes/sygus_datatype_utils.h"
25 : : #include "theory/quantifiers/quantifiers_attributes.h"
26 : : #include "theory/quantifiers/quantifiers_rewriter.h"
27 : : #include "theory/quantifiers/sygus/sygus_utils.h"
28 : : #include "theory/quantifiers/term_util.h"
29 : :
30 : : using namespace std;
31 : : using namespace cvc5::internal::kind;
32 : :
33 : : namespace cvc5::internal {
34 : : namespace theory {
35 : : namespace quantifiers {
36 : :
37 : 0 : SygusAbduct::SygusAbduct() {}
38 : :
39 : 601 : Node SygusAbduct::mkAbductionConjecture(const std::string& name,
40 : : const std::vector<Node>& asserts,
41 : : const std::vector<Node>& axioms,
42 : : TypeNode abdGType)
43 : : {
44 : 601 : NodeManager* nm = NodeManager::currentNM();
45 : 601 : SkolemManager* sm = nm->getSkolemManager();
46 : 1202 : std::unordered_set<Node> symset;
47 [ + + ]: 1918 : for (size_t i = 0, size = asserts.size(); i < size; i++)
48 : : {
49 : 1317 : expr::getSymbols(asserts[i], symset);
50 : : }
51 [ + - ]: 1202 : Trace("sygus-abduct-debug")
52 : 601 : << "...finish, got " << symset.size() << " symbols." << std::endl;
53 : :
54 [ + - ]: 601 : Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl;
55 : 1202 : std::vector<Node> syms;
56 : 1202 : std::vector<Node> vars;
57 : 1202 : std::vector<Node> varlist;
58 : 1202 : std::vector<TypeNode> varlistTypes;
59 [ + + ]: 1886 : for (const Node& s : symset)
60 : : {
61 : 1285 : TypeNode tn = s.getType();
62 [ + + ]: 2564 : if (tn.isDatatypeConstructor() || tn.isDatatypeSelector()
63 [ + + ][ + + ]: 2564 : || tn.isDatatypeTester() || tn.isDatatypeUpdater())
[ - + ][ + + ]
64 : : {
65 : : // datatype symbols should be considered interpreted symbols here, not
66 : : // (higher-order) variables.
67 : 12 : continue;
68 : : }
69 : : // Notice that we allow for non-first class (e.g. function) variables here.
70 : : // This is applicable to the case where we are doing get-abduct in a logic
71 : : // with UF.
72 : 2546 : std::stringstream ss;
73 : 1273 : ss << s;
74 : 2546 : Node var = nm->mkBoundVar(tn);
75 : 1273 : syms.push_back(s);
76 : 1273 : vars.push_back(var);
77 : 2546 : Node vlv = nm->mkBoundVar(ss.str(), tn);
78 : 1273 : varlist.push_back(vlv);
79 : 1273 : varlistTypes.push_back(tn);
80 : : // set that this variable encodes the term s
81 : : SygusVarToTermAttribute sta;
82 : 1273 : vlv.setAttribute(sta, s);
83 : : }
84 [ + - ]: 601 : Trace("sygus-abduct-debug") << "...finish" << std::endl;
85 : :
86 [ + - ]: 601 : Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl;
87 : : // make the abduction predicate to synthesize
88 : 601 : TypeNode abdType = varlistTypes.empty() ? nm->booleanType()
89 [ + + ]: 1202 : : nm->mkPredicateType(varlistTypes);
90 : 1803 : Node abd = nm->mkBoundVar(name.c_str(), abdType);
91 [ + - ]: 601 : Trace("sygus-abduct-debug") << "...finish" << std::endl;
92 : :
93 : : // the sygus variable list
94 : 1202 : Node abvl;
95 : : // if provided, we will associate the provide sygus datatype type with the
96 : : // function-to-synthesize. However, we must convert it so that its
97 : : // free symbols are universally quantified.
98 [ + + ]: 601 : if (!abdGType.isNull())
99 : : {
100 [ + - ][ + - ]: 622 : Assert(abdGType.isDatatype() && abdGType.getDType().isSygus());
[ - + ][ - - ]
101 [ + - ]: 311 : Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl;
102 [ + - ][ - + ]: 311 : Trace("sygus-abduct-debug") << abdGType.getDType().getName() << std::endl;
[ - - ]
103 : :
104 : : // substitute the free symbols of the grammar with variables corresponding
105 : : // to the formal argument list of the new sygus datatype type.
106 : : TypeNode abdGTypeS = datatypes::utils::substituteAndGeneralizeSygusType(
107 : 311 : abdGType, syms, varlist);
108 : :
109 [ + - ][ + - ]: 622 : Assert(abdGTypeS.isDatatype() && abdGTypeS.getDType().isSygus());
[ - + ][ - - ]
110 : :
111 [ + - ]: 622 : Trace("sygus-abduct-debug")
112 : 311 : << "Make sygus grammar attribute..." << std::endl;
113 : : // Set the sygus grammar attribute to indicate that abdGTypeS encodes the
114 : : // grammar for abd.
115 : 311 : SygusUtils::setSygusType(abd, abdGTypeS);
116 [ + - ]: 311 : Trace("sygus-abduct-debug") << "Finished setting up grammar." << std::endl;
117 : :
118 : : // use the bound variable list from the new substituted grammar type
119 : 311 : const DType& agtsd = abdGTypeS.getDType();
120 : 311 : abvl = agtsd.getSygusVarList();
121 [ + - ][ + - ]: 622 : Assert(!abvl.isNull() && abvl.getKind() == Kind::BOUND_VAR_LIST);
[ - + ][ - - ]
122 : : }
123 [ + + ]: 290 : else if (!varlist.empty())
124 : : {
125 : : // the bound variable list of the abduct-to-synthesize is determined by
126 : : // the variable list above
127 : 280 : abvl = nm->mkNode(Kind::BOUND_VAR_LIST, varlist);
128 : : // We do not set a grammar type for abd (SygusSynthGrammarAttribute).
129 : : // Its grammar will be constructed internally in the default way
130 : : }
131 : :
132 [ + - ]: 601 : Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl;
133 : 1202 : std::vector<Node> achildren;
134 : 601 : achildren.push_back(abd);
135 : 601 : achildren.insert(achildren.end(), vars.begin(), vars.end());
136 [ + + ]: 1202 : Node abdApp = vars.empty() ? abd : nm->mkNode(Kind::APPLY_UF, achildren);
137 [ + - ]: 601 : Trace("sygus-abduct-debug") << "...finish" << std::endl;
138 : :
139 [ + - ]: 601 : Trace("sygus-abduct-debug") << "Set attributes..." << std::endl;
140 : : // set the sygus bound variable list
141 : 601 : SygusUtils::setSygusArgumentList(abd, abvl);
142 [ + - ]: 601 : Trace("sygus-abduct-debug") << "...finish" << std::endl;
143 : :
144 [ + - ]: 601 : Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl;
145 : : Node input =
146 [ + + ]: 1202 : asserts.size() == 1 ? asserts[0] : nm->mkNode(Kind::AND, asserts);
147 : 601 : input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
148 : : // A(x) => ~input( x )
149 : 601 : input = nm->mkNode(Kind::OR, abdApp.negate(), input.negate());
150 [ + - ]: 601 : Trace("sygus-abduct-debug") << "...finish" << std::endl;
151 : :
152 [ + - ]: 601 : Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl;
153 : 601 : Node res = input.negate();
154 [ + + ]: 601 : if (!vars.empty())
155 : : {
156 : 591 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, vars);
157 : : // exists x. ~( A( x ) => ~input( x ) )
158 : 591 : res = nm->mkNode(Kind::EXISTS, bvl, res);
159 : : }
160 : : // sygus attribute
161 : : Node aconj =
162 : 601 : axioms.size() == 0
163 : 0 : ? nm->mkConst(true)
164 [ + + ][ + + ]: 1202 : : (axioms.size() == 1 ? axioms[0] : nm->mkNode(Kind::AND, axioms));
165 : 601 : aconj = aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
166 [ + - ]: 601 : Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl;
167 : 1803 : Node sc = nm->mkNode(Kind::AND, aconj, abdApp);
168 [ + + ]: 601 : if (!vars.empty())
169 : : {
170 : 591 : Node vbvl = nm->mkNode(Kind::BOUND_VAR_LIST, vars);
171 : 591 : sc = nm->mkNode(Kind::EXISTS, vbvl, sc);
172 : : }
173 : 1803 : Node sygusScVar = sm->mkDummySkolem("sygus_sc", nm->booleanType());
174 : 601 : sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
175 : 1202 : Node instAttr = nm->mkNode(Kind::INST_ATTRIBUTE, sygusScVar);
176 : : // build in the side condition
177 : : // exists x. A( x ) ^ input_axioms( x )
178 : : // as an additional annotation on the sygus conjecture. In other words,
179 : : // the abducts A we procedure must be consistent with our axioms.
180 : :
181 : : // forall A. exists x. ~( A( x ) => ~input( x ) )
182 : 1803 : res = SygusUtils::mkSygusConjecture({abd}, res, {instAttr});
183 [ + - ]: 601 : Trace("sygus-abduct-debug") << "...finish" << std::endl;
184 : :
185 [ + - ]: 601 : Trace("sygus-abduct") << "Generate: " << res << std::endl;
186 : :
187 : 1202 : return res;
188 : : }
189 : :
190 : : } // namespace quantifiers
191 : : } // namespace theory
192 : : } // namespace cvc5::internal
|
