diff options
| author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-05-08 18:18:53 +0200 |
|---|---|---|
| committer | ajreynol <reynolds@larapc05.epfl.ch> | 2014-05-08 18:18:53 +0200 |
| commit | 88907b94e858b701e83bbee67f542ad0ee5ae626 (patch) | |
| tree | cb2e45ef27519ab90d038a77367823498311d54b /src/theory/quantifiers/macros.h | |
| parent | ce831651caf58c1005fd3ebfdd2b75923d594328 (diff) | |
Major simplifications to macros module.
Diffstat (limited to 'src/theory/quantifiers/macros.h')
| -rw-r--r-- | src/theory/quantifiers/macros.h | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index ad5cd2e55..682e47930 100644 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -30,20 +30,19 @@ namespace quantifiers { class QuantifierMacros{ private: + void processAssertion( Node n ); + bool isBoundVarApplyUf( Node n ); void process( Node n, bool pol, std::vector< Node >& args, Node f ); bool contains( Node n, Node n_s ); bool containsBadOp( Node n, Node n_op ); bool isMacroLiteral( Node n, bool pol ); void getMacroCandidates( Node n, std::vector< Node >& candidates ); Node solveInEquality( Node n, Node lit ); - bool isConsistentDefinition( Node op, Node cond, Node def ); bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ); bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ); //map from operators to macro basis terms std::map< Node, std::vector< Node > > d_macro_basis; - //map from operators to map from conditions to definition cases - std::map< Node, std::vector< std::pair< Node, Node > > > d_macro_def_cases; //map from operators to macro definition std::map< Node, Node > d_macro_defs; private: |