diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
commit | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (patch) | |
tree | a79f142c5b6fbeaec34978f8da2b2db308a33e79 /src/theory/quantifiers/model_builder.h | |
parent | 5b4c416608bda1df62e1ffe7131648a89882ddc7 (diff) |
cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index d0348dff8..7331daf8e 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -23,6 +23,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { /** Attribute true for nodes that should not be used when considered for inst-gen basis */ struct BasisNoMatchAttributeId {}; @@ -35,17 +36,14 @@ typedef expr::Attribute< BasisNoMatchAttributeId, class TermArgBasisTrie { private: - bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex ); + bool addTerm2( FirstOrderModel* fm, Node n, int argIndex ); public: /** the data */ std::map< Node, TermArgBasisTrie > d_data; public: - bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } + bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); } };/* class TermArgBasisTrie */ - -namespace quantifiers { - /** model builder class * This class is capable of building candidate models based on the current quantified formulas * that are asserted. Use: |