diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/options | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 12 |
2 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options index d250bee74..1daa30981 100644 --- a/src/theory/datatypes/options +++ b/src/theory/datatypes/options @@ -11,7 +11,7 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory # cdr( nil ) has no set value. expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true disable rewriting incorrectly applied selectors to arbitrary ground term -expert-option dtForceAssignment /--dt-force-assignment bool :default false :read-write +option dtForceAssignment /--dt-force-assignment bool :default false :read-write force the datatypes solver to give specific values to all datatypes terms before answering sat endmodule diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 2e33c7c4a..d1dbae90c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -93,11 +93,13 @@ Node TheoryQuantifiers::getValue(TNode n) { } void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){ - for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { - if((*i).assertion.getKind() == kind::NOT) { - m->assertPredicate((*i).assertion[0], false); - } else { - m->assertPredicate(*i, true); + if( fullModel ){ + for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { + if((*i).assertion.getKind() == kind::NOT) { + m->assertPredicate((*i).assertion[0], false); + } else { + m->assertPredicate(*i, true); + } } } } |