From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 18 Feb 2021 02:41:19 +0000 (-0600)
Subject: Move first order model for full model check to own file (#5918)
X-Git-Tag: cvc5-1.0.0~2268
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ca17deba3b0f0308bda304ac739caf43e9536c0;p=cvc5.git

Move first order model for full model check to own file (#5918)

This moves the derived model class used in finite model finding to its own file, in the src/theory/quantifiers/fmf directory.

Updates the code to meet guidelines, no behavior changes.
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 654ccb40c..96f98bd4c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -694,6 +694,8 @@ libcvc4_add_sources(
   theory/quantifiers/first_order_model.h
   theory/quantifiers/fmf/bounded_integers.cpp
   theory/quantifiers/fmf/bounded_integers.h
+  theory/quantifiers/fmf/first_order_model_fmc.cpp
+  theory/quantifiers/fmf/first_order_model_fmc.h
   theory/quantifiers/fmf/full_model_check.cpp
   theory/quantifiers/fmf/full_model_check.h
   theory/quantifiers/fmf/model_builder.cpp
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 593ec98f9..571acbda6 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -16,7 +16,6 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
-#include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
@@ -336,123 +335,6 @@ unsigned FirstOrderModel::getModelBasisArg(Node n)
   return n.getAttribute(ModelBasisArgAttribute());
 }
 
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe,
-                                       QuantifiersState& qs,
-                                       QuantifiersRegistry& qr,
-                                       std::string name)
-    : FirstOrderModel(qe, qs, qr, name)
-{
-}
-
-FirstOrderModelFmc::~FirstOrderModelFmc()
-{
-  for(std::map<Node, Def*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
-    delete (*i).second;
-  }
-}
-
-void FirstOrderModelFmc::processInitialize( bool ispre ) {
-  if( ispre ){
-    for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
-      it->second->reset();
-    }
-  }
-}
-
-void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
-  if( n.getKind()==APPLY_UF ){
-    // cannot be a bound variable
-    Node op = n.getOperator();
-    if (op.getKind() != BOUND_VARIABLE)
-    {
-      if (d_models.find(op) == d_models.end())
-      {
-        d_models[op] = new Def;
-      }
-    }
-  }
-}
-
-
-bool FirstOrderModelFmc::isStar(Node n) {
-  //return n==getStar(n.getType());
-  return n.getAttribute(IsStarAttribute());
-}
-
-Node FirstOrderModelFmc::getStar(TypeNode tn) {
-  std::map<TypeNode, Node >::iterator it = d_type_star.find( tn );
-  if( it==d_type_star.end() ){
-    Node st = NodeManager::currentNM()->mkSkolem( "star", tn, "skolem created for full-model checking" );
-    d_type_star[tn] = st;
-    st.setAttribute(IsStarAttribute(), true );
-    return st;
-  }
-  return it->second;
-}
-
-Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
-  Trace("fmc-model") << "Get function value for " << op << std::endl;
-  TypeNode type = op.getType();
-  std::vector< Node > vars;
-  for( size_t i=0; i<type.getNumChildren()-1; i++ ){
-    std::stringstream ss;
-    ss << argPrefix << (i+1);
-    Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] );
-    vars.push_back( b );
-  }
-  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
-  Node curr;
-  for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
-    Node v = d_models[op]->d_value[i];
-    Trace("fmc-model-func") << "Value is : " << v << std::endl;
-    Assert(v.isConst());
-    /*
-    if( !hasTerm( v ) ){
-      //can happen when the model basis term does not exist in ground assignment
-      TypeNode tn = v.getType();
-      //check if it is a constant introduced as a representative not existing in the model's equality engine
-      if( !d_rep_set.hasRep( tn, v ) ){
-        if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){
-          v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ];
-        }else{
-          //can happen for types not involved in quantified formulas
-          Trace("fmc-model-func") << "No type rep for " << tn << std::endl;
-          v = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 );
-        }
-        Trace("fmc-model-func") << "No term, assign " << v << std::endl;
-      }
-    }
-    v = getRepresentative( v );
-    */
-    if( curr.isNull() ){
-      Trace("fmc-model-func") << "base : " << v << std::endl;
-      curr = v;
-    }else{
-      //make the condition
-      Node cond = d_models[op]->d_cond[i];
-      Trace("fmc-model-func") << "...cond : " << cond << std::endl;
-      std::vector< Node > children;
-      for( unsigned j=0; j<cond.getNumChildren(); j++) {
-        TypeNode tn = vars[j].getType();
-        if (!isStar(cond[j]))
-        {
-          Node c = getRepresentative( cond[j] );
-          c = getRepresentative( c );
-          children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
-        }
-      }
-      Assert(!children.empty());
-      Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
-
-      Trace("fmc-model-func") << "condition : " << cc << ", value : " << v << std::endl;
-      curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
-    }
-  }
-  Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
-  curr = Rewriter::rewrite( curr );
-  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
-}
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index ebc68ca53..a868d02ef 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -189,38 +189,6 @@ class FirstOrderModel : public TheoryModel
   void computeModelBasisArgAttribute(Node n);
 };/* class FirstOrderModel */
 
-namespace fmcheck {
-
-class Def;
-
-class FirstOrderModelFmc : public FirstOrderModel
-{
-  friend class FullModelChecker;
-
- private:
-  /** models for UF */
-  std::map<Node, Def * > d_models;
-  std::map<TypeNode, Node > d_type_star;
-  /** get current model value */
-  void processInitializeModelForTerm(Node n) override;
-
- public:
-  FirstOrderModelFmc(QuantifiersEngine* qe,
-                     QuantifiersState& qs,
-                     QuantifiersRegistry& qr,
-                     std::string name);
-  ~FirstOrderModelFmc() override;
-  FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
-  // initialize the model
-  void processInitialize(bool ispre) override;
-  Node getFunctionValue(Node op, const char* argPrefix );
-
-  bool isStar(Node n);
-  Node getStar(TypeNode tn);
-};/* class FirstOrderModelFmc */
-
-}/* CVC4::theory::quantifiers::fmcheck namespace */
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
new file mode 100644
index 000000000..c2d61e7c2
--- /dev/null
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -0,0 +1,149 @@
+/*********************                                                        */
+/*! \file first_order_model_fmc.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of first order model for full model check
+ **/
+
+#include "theory/quantifiers/fmf/first_order_model_fmc.h"
+
+#include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+namespace fmcheck {
+
+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe,
+                                       QuantifiersState& qs,
+                                       QuantifiersRegistry& qr,
+                                       std::string name)
+    : FirstOrderModel(qe, qs, qr, name)
+{
+}
+
+FirstOrderModelFmc::~FirstOrderModelFmc()
+{
+  for (std::pair<const Node, Def*>& d : d_models)
+  {
+    delete d.second;
+  }
+}
+
+void FirstOrderModelFmc::processInitialize(bool ispre)
+{
+  if (!ispre)
+  {
+    return;
+  }
+  for (std::pair<const Node, Def*>& d : d_models)
+  {
+    d.second->reset();
+  }
+}
+
+void FirstOrderModelFmc::processInitializeModelForTerm(Node n)
+{
+  if (n.getKind() == APPLY_UF)
+  {
+    // cannot be a bound variable
+    Node op = n.getOperator();
+    if (op.getKind() != BOUND_VARIABLE)
+    {
+      if (d_models.find(op) == d_models.end())
+      {
+        d_models[op] = new Def;
+      }
+    }
+  }
+}
+
+bool FirstOrderModelFmc::isStar(Node n)
+{
+  return n.getAttribute(IsStarAttribute());
+}
+
+Node FirstOrderModelFmc::getStar(TypeNode tn)
+{
+  std::map<TypeNode, Node>::iterator it = d_type_star.find(tn);
+  if (it != d_type_star.end())
+  {
+    return it->second;
+  }
+  Node st = NodeManager::currentNM()->mkSkolem(
+      "star", tn, "skolem created for full-model checking");
+  d_type_star[tn] = st;
+  st.setAttribute(IsStarAttribute(), true);
+  return st;
+}
+
+Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix)
+{
+  Trace("fmc-model") << "Get function value for " << op << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  TypeNode type = op.getType();
+  std::vector<Node> vars;
+  for (size_t i = 0, nargs = type.getNumChildren() - 1; i < nargs; i++)
+  {
+    std::stringstream ss;
+    ss << argPrefix << (i + 1);
+    Node b = nm->mkBoundVar(ss.str(), type[i]);
+    vars.push_back(b);
+  }
+  Node boundVarList = nm->mkNode(BOUND_VAR_LIST, vars);
+  Node curr;
+  Def* odef = d_models[op];
+  for (size_t i = 0, ncond = odef->d_cond.size(); i < ncond; i++)
+  {
+    size_t ii = (ncond - 1) - i;
+    Node v = odef->d_value[ii];
+    Trace("fmc-model-func") << "Value is : " << v << std::endl;
+    Assert(v.isConst());
+    if (curr.isNull())
+    {
+      Trace("fmc-model-func") << "base : " << v << std::endl;
+      curr = v;
+    }
+    else
+    {
+      // make the condition
+      Node cond = odef->d_cond[ii];
+      Trace("fmc-model-func") << "...cond : " << cond << std::endl;
+      std::vector<Node> children;
+      for (size_t j = 0, nchild = cond.getNumChildren(); j < nchild; j++)
+      {
+        TypeNode tn = vars[j].getType();
+        if (!isStar(cond[j]))
+        {
+          Node c = getRepresentative(cond[j]);
+          c = getRepresentative(c);
+          children.push_back(nm->mkNode(EQUAL, vars[j], c));
+        }
+      }
+      Assert(!children.empty());
+      Node cc = nm->mkAnd(children);
+
+      Trace("fmc-model-func")
+          << "condition : " << cc << ", value : " << v << std::endl;
+      curr = nm->mkNode(ITE, cc, v, curr);
+    }
+  }
+  Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
+  curr = Rewriter::rewrite(curr);
+  return nm->mkNode(LAMBDA, boundVarList, curr);
+}
+
+}  // namespace fmcheck
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h
new file mode 100644
index 000000000..1b9bb7f23
--- /dev/null
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file first_order_model_fmc.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Paul Meng, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief First order model for full model check
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
+#define CVC4__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
+
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+namespace fmcheck {
+
+class Def;
+
+class FirstOrderModelFmc : public FirstOrderModel
+{
+  friend class FullModelChecker;
+
+ private:
+  /** models for UF */
+  std::map<Node, Def*> d_models;
+  std::map<TypeNode, Node> d_type_star;
+  /** get current model value */
+  void processInitializeModelForTerm(Node n) override;
+
+ public:
+  FirstOrderModelFmc(QuantifiersEngine* qe,
+                     QuantifiersState& qs,
+                     QuantifiersRegistry& qr,
+                     std::string name);
+  ~FirstOrderModelFmc() override;
+  FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
+  // initialize the model
+  void processInitialize(bool ispre) override;
+  Node getFunctionValue(Node op, const char* argPrefix);
+
+  bool isStar(Node n);
+  Node getStar(TypeNode tn);
+}; /* class FirstOrderModelFmc */
+
+}  // namespace fmcheck
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__FIRST_ORDER_MODEL_H */
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 76c131369..07a8f3d60 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -17,8 +17,8 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
 #define CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
 
+#include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/fmf/model_builder.h"
-#include "theory/quantifiers/first_order_model.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9c56c1ba5..ebec7a110 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -20,6 +20,7 @@
 #include "options/uf_options.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/quantifiers_modules.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"