From 7ca17deba3b0f0308bda304ac739caf43e9536c0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Feb 2021 20:41:19 -0600 Subject: [PATCH] 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. --- src/CMakeLists.txt | 2 + src/theory/quantifiers/first_order_model.cpp | 118 -------------- src/theory/quantifiers/first_order_model.h | 32 ---- .../quantifiers/fmf/first_order_model_fmc.cpp | 149 ++++++++++++++++++ .../quantifiers/fmf/first_order_model_fmc.h | 60 +++++++ src/theory/quantifiers/fmf/full_model_check.h | 2 +- src/theory/quantifiers_engine.cpp | 1 + 7 files changed, 213 insertions(+), 151 deletions(-) create mode 100644 src/theory/quantifiers/fmf/first_order_model_fmc.cpp create mode 100644 src/theory/quantifiers/fmf/first_order_model_fmc.h 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::iterator i = d_models.begin(); i != d_models.end(); ++i) { - delete (*i).second; - } -} - -void FirstOrderModelFmc::processInitialize( bool ispre ) { - if( ispre ){ - for( std::map::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::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; imkBoundVar( 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; jmkNode( 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 d_models; - std::map 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& d : d_models) + { + delete d.second; + } +} + +void FirstOrderModelFmc::processInitialize(bool ispre) +{ + if (!ispre) + { + return; + } + for (std::pair& 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::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 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 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 d_models; + std::map 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" -- 2.30.2