diff options
Diffstat (limited to 'src/theory/quantifiers/full_model_check.h')
-rwxr-xr-x | src/theory/quantifiers/full_model_check.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 92c866ffd..00a910567 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -65,8 +65,8 @@ public: d_has_simplified = false;
}
bool addEntry( FullModelChecker * m, Node c, Node v);
- Node evaluate( FullModelChecker * m, std::vector<Node> inst );
- int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );
+ Node evaluate( FullModelChecker * m, std::vector<Node>& inst );
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );
void simplify( FullModelChecker * m );
void debugPrint(const char * tr, Node op, FullModelChecker * m);
};
@@ -141,6 +141,8 @@ public: /** process build model */
void processBuildModel(TheoryModel* m, bool fullModel);
+ /** get current model value */
+ Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );
};
}
|