Fixes for issue 1404 (#1409)

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 15b96d2a049c29a1b09549d7525438f2275a6380..4da23ea96a1506306b51c4b4435ae70af9b772ce 100644 (file)
--- 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 8be3b5460837c1ce9403d5aeffa4b7536b8c8164..9b259bf971289155748abff0bd7c862a3e1bb9b9 100644 (file)
--- 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<TNode>& assumptions) {
       assumptions.push_back( tassumptions[i] );
     }
   }
-  Debug("strings-explain-debug") << "Explanation for " << literal << " was " << std::endl;
-  for( unsigned i=ps; i<assumptions.size(); i++ ){
-    Debug("strings-explain-debug") << "   " << assumptions[i] << std::endl;
+  if (Debug.isOn("strings-explain-debug"))
+  {
+    Debug("strings-explain-debug") << "Explanation for " << literal << " was "
+                                   << std::endl;
+    for (unsigned i = ps; i < assumptions.size(); i++)
+    {
+      Debug("strings-explain-debug") << "   " << assumptions[i] << std::endl;
+    }
   }
 }
 
@@ -3279,6 +3284,12 @@ void TheoryStrings::sendInference( std::vector< Node >& 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 65810109c94520f8a33b5ffcced7389d31729830..02dd92ad7273919b78d0be8697cf5b8be39542a2 100644 (file)
--- 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 a8726f4901bd8577fdbea82fae7c216f3e8b4ede..600f511c8c3d2c22e79ac579fd3c829e6c1ad26e 100644 (file)
--- 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 b08c8f1ca38e1c2b012d5c37f59440f98c939222..ac12b37e30594f9546b8aa034ba6b34cba08d9ba 100644 (file)
--- 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<TypeNode> 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