1 /********************* */
2 /*! \file sygus_inference.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Mathias Preiner, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Sygus inference module
15 #include "preprocessing/passes/sygus_inference.h"
17 #include "smt/smt_engine.h"
18 #include "smt/smt_engine_scope.h"
19 #include "smt/smt_statistics_registry.h"
20 #include "theory/quantifiers/quantifiers_attributes.h"
21 #include "theory/quantifiers/quantifiers_rewriter.h"
22 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
23 #include "theory/smt_engine_subsolver.h"
26 using namespace CVC4::kind
;
27 using namespace CVC4::theory
;
30 namespace preprocessing
{
33 SygusInference::SygusInference(PreprocessingPassContext
* preprocContext
)
34 : PreprocessingPass(preprocContext
, "sygus-infer"){};
36 PreprocessingPassResult
SygusInference::applyInternal(
37 AssertionPipeline
* assertionsToPreprocess
)
39 Trace("sygus-infer") << "Run sygus inference..." << std::endl
;
40 std::vector
<Node
> funs
;
41 std::vector
<Node
> sols
;
42 // see if we can succesfully solve the input as a sygus problem
43 if (solveSygus(assertionsToPreprocess
->ref(), funs
, sols
))
45 Assert(funs
.size() == sols
.size());
46 // if so, sygus gives us function definitions
47 SmtEngine
* master_smte
= d_preprocContext
->getSmt();
48 for (unsigned i
= 0, size
= funs
.size(); i
< size
; i
++)
50 std::vector
<Node
> args
;
52 // if it is a non-constant function
53 if (sol
.getKind() == LAMBDA
)
55 for (const Node
& v
: sol
[0])
61 master_smte
->defineFunction(funs
[i
], args
, sol
);
64 // apply substitution to everything, should result in SAT
65 for (unsigned i
= 0, size
= assertionsToPreprocess
->ref().size(); i
< size
;
68 Node prev
= (*assertionsToPreprocess
)[i
];
70 prev
.substitute(funs
.begin(), funs
.end(), sols
.begin(), sols
.end());
73 curr
= theory::Rewriter::rewrite(curr
);
74 Trace("sygus-infer-debug")
75 << "...rewrote " << prev
<< " to " << curr
<< std::endl
;
76 assertionsToPreprocess
->replace(i
, curr
);
80 return PreprocessingPassResult::NO_CONFLICT
;
83 bool SygusInference::solveSygus(const std::vector
<Node
>& assertions
,
84 std::vector
<Node
>& funs
,
85 std::vector
<Node
>& sols
)
87 if (assertions
.empty())
89 Trace("sygus-infer") << "...fail: empty assertions." << std::endl
;
93 NodeManager
* nm
= NodeManager::currentNM();
95 // collect free variables in all assertions
96 std::vector
<Node
> qvars
;
97 std::map
<TypeNode
, std::vector
<Node
> > qtvars
;
98 std::vector
<Node
> free_functions
;
100 std::vector
<TNode
> visit
;
101 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
103 // add top-level conjuncts to eassertions
104 std::vector
<Node
> assertions_proc
= assertions
;
105 std::vector
<Node
> eassertions
;
107 while (index
< assertions_proc
.size())
109 Node ca
= assertions_proc
[index
];
110 if (ca
.getKind() == AND
)
112 for (const Node
& ai
: ca
)
114 assertions_proc
.push_back(ai
);
119 eassertions
.push_back(ca
);
124 // process eassertions
125 std::vector
<Node
> processed_assertions
;
126 for (const Node
& as
: eassertions
)
128 // substitution for this assertion
129 std::vector
<Node
> vars
;
130 std::vector
<Node
> subs
;
131 std::map
<TypeNode
, unsigned> type_count
;
134 pas
= theory::Rewriter::rewrite(pas
);
135 Trace("sygus-infer") << "assertion : " << pas
<< std::endl
;
136 if (pas
.getKind() == FORALL
)
138 // preprocess the quantified formula
139 TrustNode trn
= quantifiers::QuantifiersRewriter::preprocess(pas
);
144 Trace("sygus-infer-debug") << " ...preprocessed to " << pas
<< std::endl
;
146 if (pas
.getKind() == FORALL
)
148 // it must be a standard quantifier
149 theory::quantifiers::QAttributes qa
;
150 theory::quantifiers::QuantAttributes::computeQuantAttributes(pas
, qa
);
151 if (!qa
.isStandard())
154 << "...fail: non-standard top-level quantifier." << std::endl
;
158 for (const Node
& v
: pas
[0])
160 TypeNode tnv
= v
.getType();
161 unsigned vnum
= type_count
[tnv
];
164 if (vnum
< qtvars
[tnv
].size())
166 subs
.push_back(qtvars
[tnv
][vnum
]);
170 Assert(vnum
== qtvars
[tnv
].size());
171 Node bv
= nm
->mkBoundVar(tnv
);
172 qtvars
[tnv
].push_back(bv
);
181 pas
.substitute(vars
.begin(), vars
.end(), subs
.begin(), subs
.end());
184 Trace("sygus-infer-debug") << " ...substituted to " << pas
<< std::endl
;
186 // collect free functions, ensure no quantified formulas
188 // compute free variables
189 visit
.push_back(cur
);
194 if (visited
.find(cur
) == visited
.end())
197 if (cur
.getKind() == APPLY_UF
)
199 Node op
= cur
.getOperator();
200 // visit the operator, which might not be a variable
203 else if (cur
.isVar() && cur
.getKind() != BOUND_VARIABLE
)
205 // We are either in the case of a free first-order constant or a
206 // function in a higher-order context. We add to free_functions
207 // in either case. Note that a free constant that is not in a
208 // higher-order context is a 0-argument function-to-synthesize.
209 // We should not have traversed here before due to our visited cache.
210 Assert(std::find(free_functions
.begin(), free_functions
.end(), cur
)
211 == free_functions
.end());
212 free_functions
.push_back(cur
);
214 else if (cur
.isClosure())
217 << "...fail: non-top-level quantifier." << std::endl
;
220 for (const TNode
& cn
: cur
)
225 } while (!visit
.empty());
226 processed_assertions
.push_back(pas
);
229 // no functions to synthesize
230 if (free_functions
.empty())
232 Trace("sygus-infer") << "...fail: no free function symbols." << std::endl
;
236 // Ensure the type of all free functions is handled by the sygus grammar
237 // constructor utility.
238 bool typeSuccess
= true;
239 for (const Node
& f
: free_functions
)
241 TypeNode tn
= f
.getType();
242 if (!theory::quantifiers::CegGrammarConstructor::isHandledType(tn
))
244 Trace("sygus-infer") << "...fail: unhandled type " << tn
<< std::endl
;
254 Assert(!processed_assertions
.empty());
255 // conjunction of the assertions
256 Trace("sygus-infer") << "Construct body..." << std::endl
;
258 if (processed_assertions
.size() == 1)
260 body
= processed_assertions
[0];
264 body
= nm
->mkNode(AND
, processed_assertions
);
267 // for each free function symbol, make a bound variable of the same type
268 Trace("sygus-infer") << "Do free function substitution..." << std::endl
;
269 std::vector
<Node
> ff_vars
;
270 std::map
<Node
, Node
> ff_var_to_ff
;
271 for (const Node
& ff
: free_functions
)
273 Node ffv
= nm
->mkBoundVar(ff
.getType());
274 ff_vars
.push_back(ffv
);
275 Trace("sygus-infer") << " synth-fun: " << ff
<< " as " << ffv
<< std::endl
;
276 ff_var_to_ff
[ffv
] = ff
;
278 // substitute free functions -> variables
279 body
= body
.substitute(free_functions
.begin(),
280 free_functions
.end(),
283 Trace("sygus-infer-debug") << "...got : " << body
<< std::endl
;
286 Trace("sygus-infer") << "Make inner sygus conjecture..." << std::endl
;
287 body
= body
.negate();
290 Node bvl
= nm
->mkNode(BOUND_VAR_LIST
, qvars
);
291 body
= nm
->mkNode(EXISTS
, bvl
, body
);
294 // sygus attribute to mark the conjecture as a sygus conjecture
295 Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl
;
296 Node sygusVar
= nm
->mkSkolem("sygus", nm
->booleanType());
297 theory::SygusAttribute ca
;
298 sygusVar
.setAttribute(ca
, true);
299 Node instAttr
= nm
->mkNode(INST_ATTRIBUTE
, sygusVar
);
300 Node instAttrList
= nm
->mkNode(INST_PATTERN_LIST
, instAttr
);
302 Node fbvl
= nm
->mkNode(BOUND_VAR_LIST
, ff_vars
);
304 body
= nm
->mkNode(FORALL
, fbvl
, body
, instAttrList
);
306 Trace("sygus-infer") << "*** Return sygus inference : " << body
<< std::endl
;
308 // make a separate smt call
309 std::unique_ptr
<SmtEngine
> rrSygus
;
310 theory::initializeSubsolver(rrSygus
);
311 rrSygus
->assertFormula(body
);
312 Trace("sygus-infer") << "*** Check sat..." << std::endl
;
313 Result r
= rrSygus
->checkSat();
314 Trace("sygus-infer") << "...result : " << r
<< std::endl
;
315 if (r
.asSatisfiabilityResult().isSat() != Result::UNSAT
)
317 // failed, conjecture was infeasible
320 // get the synthesis solutions
321 std::map
<Node
, Node
> synth_sols
;
322 rrSygus
->getSynthSolutions(synth_sols
);
324 std::vector
<Node
> final_ff
;
325 std::vector
<Node
> final_ff_sol
;
326 for (std::map
<Node
, Node
>::iterator it
= synth_sols
.begin();
327 it
!= synth_sols
.end();
330 Trace("sygus-infer") << " synth sol : " << it
->first
<< " -> "
331 << it
->second
<< std::endl
;
332 Node ffv
= it
->first
;
333 std::map
<Node
, Node
>::iterator itffv
= ff_var_to_ff
.find(ffv
);
334 // all synthesis solutions should correspond to a variable we introduced
335 Assert(itffv
!= ff_var_to_ff
.end());
336 if (itffv
!= ff_var_to_ff
.end())
338 Node ff
= itffv
->second
;
339 Node body2
= it
->second
;
340 Trace("sygus-infer") << "Define " << ff
<< " as " << body2
<< std::endl
;
342 sols
.push_back(body2
);
349 } // namespace passes
350 } // namespace preprocessing