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