diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:30 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:36 -0500 |
commit | f65b945119341ae8afa69bd0b7dc005c9fcc768b (patch) | |
tree | c264125578d3b8edd752740701789f7b1e4e26bb /src/theory/quantifiers/model_builder.h | |
parent | 53c301aa808218abe725014e01bddc19fe11a116 (diff) |
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 906673903..e4f9529a8 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -57,15 +57,6 @@ public: -/** Attribute true for nodes that should not be used when considered for inst-gen basis */ -struct BasisNoMatchAttributeId {}; -/** use the special for boolean flag */ -typedef expr::Attribute< BasisNoMatchAttributeId, - bool, - expr::attr::NullCleanupStrategy, - true // context dependent - > BasisNoMatchAttribute; - class TermArgBasisTrie { private: bool addTerm2( FirstOrderModel* fm, Node n, int argIndex ); @@ -85,7 +76,9 @@ public: */ class QModelBuilderIG : public QModelBuilder { + typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; protected: + BoolMap d_basisNoMatch; //map from operators to model preference data std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; //built model uf |