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.
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
#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"
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 */
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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#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 {
#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"
projects / cvc5.git / commitdiff