diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_inference.h')
| -rw-r--r-- | src/theory/quantifiers/sygus_inference.h | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus_inference.h b/src/theory/quantifiers/sygus_inference.h index a61cebcc0..cdd5a1008 100644 --- a/src/theory/quantifiers/sygus_inference.h +++ b/src/theory/quantifiers/sygus_inference.h @@ -26,8 +26,12 @@ namespace quantifiers { /** SygusInference * - * A preprocessing utility to turn a set of (quantified) assertions into a - * single SyGuS conjecture. + * A preprocessing utility that turns a set of (quantified) assertions into a + * single SyGuS conjecture. If this is possible, we solve for this single Sygus + * conjecture using a separate copy of the SMT engine. If sygus successfully + * solves the conjecture, we plug the synthesis solutions back into the original + * problem, thus obtaining a set of model substitutions under which the + * assertions should simplify to true. */ class SygusInference { @@ -36,8 +40,12 @@ class SygusInference ~SygusInference() {} /** simplify assertions * - * Either replaces assertions with the negation of an equivalent SyGuS - * conjecture and returns true, or otherwise returns false. + * Either replaces all uninterpreted functions in assertions by their + * interpretation in the solution found by a separate call to an SMT engine + * and returns true, or leaves the assertions unmodified and returns false. + * + * We fail if either a sygus conjecture that corresponds to assertions cannot + * be inferred, or the sygus conjecture we infer is infeasible. */ bool simplify(std::vector<Node>& assertions); }; |