diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-12 07:33:16 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-12 07:33:16 +0200 |
| commit | a582fa3ea1de3b6419797bbebdcb415ff4d0c0d0 (patch) | |
| tree | a81ebb13ad391082ce781c885b9302fe27a30997 /src/theory/quantifiers/macros.h | |
| parent | 86ad2ca93048844eedcafd2a2dadc43ef85dfb32 (diff) | |
Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
Diffstat (limited to 'src/theory/quantifiers/macros.h')
| -rw-r--r-- | src/theory/quantifiers/macros.h | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index 57f4abe4e..74fb0f47b 100644 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -30,11 +30,12 @@ namespace quantifiers { class QuantifierMacros{ private: - void processAssertion( Node n ); + bool d_ground_macros; + bool processAssertion( Node n ); bool isBoundVarApplyUf( Node n ); - void process( Node n, bool pol, std::vector< Node >& args, Node f ); + bool process( Node n, bool pol, std::vector< Node >& args, Node f ); bool contains( Node n, Node n_s ); - bool containsBadOp( Node n, Node op ); + bool containsBadOp( Node n, Node op, std::vector< Node >& opc ); bool isMacroLiteral( Node n, bool pol ); void getMacroCandidates( Node n, std::vector< Node >& candidates ); Node solveInEquality( Node n, Node lit ); @@ -45,13 +46,21 @@ private: std::map< Node, std::vector< Node > > d_macro_basis; //map from operators to macro definition std::map< Node, Node > d_macro_defs; + std::map< Node, Node > d_macro_defs_new; + //operators to macro ops that contain them + std::map< Node, std::vector< Node > > d_macro_def_contains; + //simplify cache + std::map< Node, Node > d_simplify_cache; private: Node simplify( Node n ); + void addMacro( Node op, Node n, std::vector< Node >& opc ); + void debugMacroDefinition( Node oo, Node n ); public: QuantifierMacros(){} ~QuantifierMacros(){} bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); + void finalizeDefinitions(); }; } |