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