diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-06 14:22:43 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-06 14:22:43 -0600 |
commit | e0909efd64c96311c69dec223411ab6b7988d01d (patch) | |
tree | 5eff4e624d8714f6343905e8cc3d40710871c0f3 /src/theory/quantifiers/sygus/sygus_explain.h | |
parent | 3de3716f7196a5f34963d85c882837c449ecf676 (diff) |
Refactor symmetry breaking in datatypes sygus (#1640)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_explain.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.h | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index ad26f29e4..818f51438 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -100,7 +100,7 @@ class TermRecBuild * (datatype) sygus term n is: * (if (gt x 0) 0 0) * where if, gt, x, 0 are datatype constructors. - * The explanation returned by getExplanationForConstantEquality + * The explanation returned by getExplanationForEquality * 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), @@ -142,20 +142,19 @@ class SygusExplain public: SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {} ~SygusExplain() {} - /** get explanation for constant equality + /** get explanation for 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); + void getExplanationForEquality(Node n, Node vn, std::vector<Node>& exp); /** returns the conjunction of exp computed in the above function */ - Node getExplanationForConstantEquality(Node n, Node vn); + Node getExplanationForEquality(Node n, Node vn); - /** get explanation for constant equality + /** get explanation for 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. @@ -165,14 +164,14 @@ class SygusExplain * { ((_ 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); + void getExplanationForEquality(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); + Node getExplanationForEquality(Node n, + Node vn, + std::map<unsigned, bool>& cexc); /** get explanation for * |