diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-25 18:19:57 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-25 18:20:15 +0100 |
commit | 7f43bd304b3d6bede36a777ee85ab68fab35d742 (patch) | |
tree | 7b3f35a95f7af95ad2a67f502317ef177096f95a /src/theory/quantifiers/term_database.h | |
parent | 4262723336d82944ffed768604fcd175cdc749a9 (diff) |
Infrastructure for partially single invocation properties. Bug fix for unconstrained functions in sygus solver.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 8ce6aeaf0..86b0efbf3 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -267,7 +267,19 @@ public: static bool hasInstConstAttr( Node n ); static Node getBoundVarAttr( Node n ); static bool hasBoundVarAttr( Node n ); - + +private: + /** get bound vars */ + static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); + /** get bound vars */ + static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ); +public: + //get the bound variables in this node + static void getBoundVars( Node n, std::vector< Node >& vars ); + //remove quantifiers + static Node getRemoveQuantifiers( Node n ); + //quantified simplify (treat free variables in n as quantified and run rewriter) + static Node getQuantSimplify( Node n ); //for skolem private: @@ -387,7 +399,7 @@ private: static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); //general utilities public: - /** simple check for contains term */ + /** simple check for whether n contains t as subterm */ static bool containsTerm( Node n, Node t ); /** simple check for contains term, true if contains at least one term in t */ static bool containsTerms( Node n, std::vector< Node >& t ); |