From 610c3e111c4bca484d94e21df46a35c55fdd6882 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 28 Jan 2013 23:19:12 -0600 Subject: [PATCH] fix for finite model finding caused by new collectModelInfo code --- src/theory/datatypes/options | 2 +- 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); + } } } } -- 2.30.2