diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_explain.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.h | 222 |
1 files changed, 222 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h new file mode 100644 index 000000000..ad26f29e4 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -0,0 +1,222 @@ +/********************* */ +/*! \file sygus_explain.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief sygus explanations + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H + +#include <vector> + +#include "expr/node.h" +#include "theory/quantifiers/sygus/sygus_invariance.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Recursive term builder + * + * This is a utility used to generate variants + * of a term n, where subterms of n can be replaced + * by others via calls to replaceChild(...). + * + * This class maintains a "context", which indicates + * a position in term n. Below, we call the subterm of + * the initial term n at this position the "active term". + * + */ +class TermRecBuild +{ + public: + TermRecBuild() {} + /** set the initial term to n + * + * The context initially empty, that is, + * the active term is initially n. + */ + void init(Node n); + + /** push the context + * + * This updates the context so that the + * active term is updated to curr[p], where + * curr is the previously active term. + */ + void push(unsigned p); + + /** pop the context */ + void pop(); + /** indicates that the i^th child of the active + * term should be replaced by r in calls to build(). + */ + void replaceChild(unsigned i, Node r); + /** get the i^th child of the active term */ + Node getChild(unsigned i); + /** build the (modified) version of the term + * we intialized via the call to init(). + */ + Node build(unsigned p = 0); + + private: + /** stack of active terms */ + std::vector<Node> d_term; + /** stack of children of active terms + * Notice that these may be modified with calls to replaceChild(...). + */ + std::vector<std::vector<Node> > d_children; + /** stack the kind of active terms */ + std::vector<Kind> d_kind; + /** stack of whether the active terms had an operator */ + std::vector<bool> d_has_op; + /** stack of positions that were pushed via calls to push(...) */ + std::vector<unsigned> d_pos; + /** add term to the context stack */ + void addTerm(Node n); +}; + +/*The SygusExplain utility + * + * This class is used to produce explanations for refinement lemmas + * in the counterexample-guided inductive synthesis (CEGIS) loop. + * + * When given an invariance test T traverses the AST of a given term, + * uses TermRecBuild to replace various subterms by fresh variables and + * recheck whether the invariant, as specified by T still holds. + * If it does, then we may exclude the explanation for that subterm. + * + * For example, say we have that the current value of + * (datatype) sygus term n is: + * (if (gt x 0) 0 0) + * where if, gt, x, 0 are datatype constructors. + * The explanation returned by getExplanationForConstantEquality + * below for n and the above term is: + * { ((_ is if) n), ((_ is geq) n.0), + * ((_ is x) n.0.0), ((_ is 0) n.0.1), + * ((_ is 0) n.1), ((_ is 0) n.2) } + * + * This class can also return more precise + * explanations based on a property that holds for + * variants of n. For instance, + * say we find that n's builtin analog rewrites to 0: + * ite( x>0, 0, 0 ) ----> 0 + * and we would like to find the minimal explanation for + * why the builtin analog of n rewrites to 0. + * We use the invariance test EquivSygusInvarianceTest + * (see sygus_invariance.h) for doing this. + * Using the SygusExplain::getExplanationFor method below, + * this will invoke the invariant test to check, e.g. + * ite( x>0, 0, y1 ) ----> 0 ? fail + * ite( x>0, y2, 0 ) ----> 0 ? fail + * ite( y3, 0, 0 ) ----> 0 ? success + * where y1, y2, y3 are fresh variables. + * Hence the explanation for the condition x>0 is irrelevant. + * This gives us the explanation: + * { ((_ is if) n), ((_ is 0) n.1), ((_ is 0) n.2) } + * indicating that all terms of the form: + * (if _ 0 0) have a builtin equivalent that rewrites to 0. + * + * For details, see Reynolds et al SYNT 2017. + * + * Below, we let [[exp]]_n denote the term induced by + * the explanation exp for n. + * For example: + * exp = { ((_ is plus) n), ((_ is y) n.1) } + * is such that: + * [[exp]]_n = (plus w y) + * where w is a fresh variable. + */ +class SygusExplain +{ + public: + SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {} + ~SygusExplain() {} + /** get explanation for constant equality + * + * This function constructs an explanation, stored in exp, such that: + * - All formulas in exp are of the form ((_ is C) ns), where ns + * is a chain of selectors applied to n, and + * - exp => ( n = vn ) + */ + void getExplanationForConstantEquality(Node n, + Node vn, + std::vector<Node>& exp); + /** returns the conjunction of exp computed in the above function */ + Node getExplanationForConstantEquality(Node n, Node vn); + + /** get explanation for constant equality + * This is identical to the above function except that we + * take an additional argument cexc, which says which + * children of vn should be excluded from the explanation. + * + * For example, if vn = plus( plus( x, x ), y ) and cexc is { 0 -> true }, + * then the following is appended to exp : + * { ((_ is plus) n), ((_ is y) n.1) } + * where notice that the 0^th argument of vn is excluded. + */ + void getExplanationForConstantEquality(Node n, + Node vn, + std::vector<Node>& exp, + std::map<unsigned, bool>& cexc); + /** returns the conjunction of exp computed in the above function */ + Node getExplanationForConstantEquality(Node n, + Node vn, + std::map<unsigned, bool>& cexc); + + /** get explanation for + * + * This function constructs an explanation, stored in exp, such that: + * - All formulas in exp are of the form ((_ is C) ns), where ns + * is a chain of selectors applied to n, and + * - The test et holds for [[exp]]_n, and + * - (if applicable) exp => ( n != vnr ). + * + * This function updates sz to be the term size of [[exp]]_n. + */ + void getExplanationFor(Node n, + Node vn, + std::vector<Node>& exp, + SygusInvarianceTest& et, + Node vnr, + unsigned& sz); + void getExplanationFor(Node n, + Node vn, + std::vector<Node>& exp, + SygusInvarianceTest& et); + + private: + /** sygus term database associated with this utility */ + TermDbSygus* d_tdb; + /** Helper function for getExplanationFor + * var_count is the number of free variables we have introduced, + * per type, for the purposes of generalizing subterms of n. + * vnr_exp stores the explanation, if one exists, for + * n != vnr. It is only non-null if vnr is non-null. + */ + void getExplanationFor(TermRecBuild& trb, + Node n, + Node vn, + std::vector<Node>& exp, + std::map<TypeNode, int>& var_count, + SygusInvarianceTest& et, + Node vnr, + Node& vnr_exp, + int& sz); +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ |