From: Andrew Reynolds Date: Thu, 30 Nov 2017 15:57:06 +0000 (-0600) Subject: Fixes for issue 1404 (#1409) X-Git-Tag: cvc5-1.0.0~5441 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=89b6c052e96cc907800650de93d2f238e19acd38;p=cvc5.git Fixes for issue 1404 (#1409) --- diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 15b96d2a0..4da23ea96 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/full_model_check.h" #include "options/quantifiers_options.h" +#include "options/uf_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" @@ -556,11 +557,15 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){ if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){ d_preinitialized_types[tn] = true; - Node mb = fm->getModelBasisTerm(tn); - if( !mb.isConst() ){ - Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl; - fm->d_equalityEngine->addTerm( mb ); - fm->addTerm( mb ); + if (!tn.isFunction() || options::ufHo()) + { + Node mb = fm->getModelBasisTerm(tn); + if (!mb.isConst()) + { + Trace("fmc") << "...add model basis term to EE of model " << mb << " " + << tn << std::endl; + fm->d_equalityEngine->addTerm(mb); + } } } } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8be3b5460..9b259bf97 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -275,9 +275,14 @@ void TheoryStrings::explain(TNode literal, std::vector& assumptions) { assumptions.push_back( tassumptions[i] ); } } - Debug("strings-explain-debug") << "Explanation for " << literal << " was " << std::endl; - for( unsigned i=ps; i& exp, std::vector< Node > eq_exp = NodeManager::currentNM()->mkNode( kind::AND, ev ); } } + // if we have unexplained literals, this lemma is not a conflict + if (eq == d_false && !exp_n.empty()) + { + eq = eq_exp.negate(); + eq_exp = d_true; + } sendLemma( eq_exp, eq, c ); }else{ sendInfer( mkAnd( exp ), eq, c ); @@ -3338,7 +3349,6 @@ void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) { d_pending_exp[eq] = eq_exp; d_infer.push_back( eq ); d_infer_exp.push_back( eq_exp ); - } void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 65810109c..02dd92ad7 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -302,7 +302,8 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ } /** add term */ -void TheoryModel::addTerm(TNode n ){ +void TheoryModel::addTermInternal(TNode n) +{ Assert(d_equalityEngine->hasTerm(n)); Trace("model-builder-debug2") << "TheoryModel::addTerm : " << n << std::endl; //must collect UF terms @@ -512,6 +513,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { if( options::ufHo() ){ Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl; + Assert(d_equalityEngine->hasTerm(f)); // assign to representative if higher-order Node r = d_equalityEngine->getRepresentative( f ); //always replace the representative, since it is initially assigned to itself diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index a8726f490..600f511c8 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -91,12 +91,6 @@ public: //---------------------------- for building the model /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); - /** add term - * This will do any model-specific processing necessary for n, - * such as constraining the interpretation of uninterpreted functions, - * and adding n to the equality engine of this model. - */ - virtual void addTerm(TNode n); /** assert equality holds in the model */ void assertEquality(TNode a, TNode b, bool polarity); /** assert predicate holds in the model */ @@ -204,6 +198,14 @@ public: Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const; + /** add term internal + * + * This will do any model-specific processing necessary for n, + * such as constraining the interpretation of uninterpreted functions. + * This is called once for all terms in the equality engine, just before + * a model builder constructs this model. + */ + virtual void addTermInternal(TNode n); private: /** cache for getModelValue */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index b08c8f1ca..ac12b37e3 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -350,11 +350,10 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) } // AJR: build ordered list of types that ensures that base types are // enumerated first. - // (I think) this is only strictly necessary for finite model finding + - // parametric types - // instantiated with uninterpreted sorts, but is probably a good idea to do - // in general - // since it leads to models with smaller term sizes. + // (I think) this is only strictly necessary for finite model finding + + // parametric types instantiated with uninterpreted sorts, but is probably + // a good idea to do in general since it leads to models with smaller term + // sizes. std::vector type_list; eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); for (; !eqcs_i.isFinished(); ++eqcs_i) @@ -396,7 +395,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) << std::endl; } // model-specific processing of the term - tm->addTerm(n); + tm->addTermInternal(n); } // Assign representative for this EC