summaryrefslogtreecommitdiff
path: root/src/theory/theory_model.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r--src/theory/theory_model.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index a161f02f4..092b5e8c7 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -262,6 +262,9 @@ protected:
bool isAssignable(TNode n);
void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel );
+ /** is v an excluded codatatype value */
+ bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
+ bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
public:
TheoryEngineModelBuilder(TheoryEngine* te);
virtual ~TheoryEngineModelBuilder(){}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback