diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-06-01 09:39:16 +0200 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-01 00:39:16 -0700 |
| commit | 9b6985b4427aff888f07ecc84079452c11113cb6 (patch) | |
| tree | e693faec20af263356c78ee7daa7bb5340b307f7 /src/theory/quantifiers/term_database.h | |
| parent | 9d93595783e350969ad428ab277614a3250e59a0 (diff) | |
Require that FMF model basis terms are variables (#3031)
The commit fixes an issue where FMF could theoretically chose interpreted function applications as "model basis terms". This triggered an incorrect model (caught by an AlwaysAssert) when the interpreted function later did not appear in a model and was chosen by FMF to be equal to a wrong value.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index cd5c27f0d..d58d33673 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -108,10 +108,11 @@ class TermDb : public QuantifiersUtil { */ Node getTypeGroundTerm(TypeNode tn, unsigned i) const; /** get or make ground term - * Returns the first ground term of type tn, - * or makes one if none exist. - */ - Node getOrMakeTypeGroundTerm(TypeNode tn); + * + * Returns the first ground term of type tn, or makes one if none exist. If + * reqVar is true, then the ground term must be a variable. + */ + Node getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar = false); /** make fresh variable * Returns a fresh variable of type tn. * This will return only a single fresh |