array_info.h \
array_info.cpp \
static_fact_manager.h \
- static_fact_manager.cpp \
- theory_arrays_model.h \
- theory_arrays_model.cpp
+ static_fact_manager.cpp
EXTRA_DIST = \
kinds
#include <map>
#include "theory/rewriter.h"
#include "expr/command.h"
-#include "theory/arrays/theory_arrays_model.h"
#include "theory/model.h"
#include "theory/arrays/options.h"
#include "smt/logic_exception.h"
}
case kind::STORE_ALL: {
throw LogicException("Array theory solver does not yet support assertions using constant array value");
- }
+ }
default:
// Variables etc
if (node.getType().isArray()) {
if (constraintIdx == d_modelConstraints.size()) {
break;
}
-
+
if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) {
assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false);
if (assertionToCheck.getKind() == kind::AND &&
}
++d_numGetModelValConflicts;
getSatContext()->pop();
- }
+ }
++te;
if (te.isFinished()) {
Assert(false);
return true;
}
}
-
+
return false;
}
+++ /dev/null
-/********************* */
-/*! \file theory_arrays_model.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_arrays_model class
- **/
-
-#include "theory/theory_engine.h"
-#include "theory/arrays/theory_arrays_model.h"
-#include "theory/model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-
-ArrayModel::ArrayModel( Node arr, TheoryModel* m ) : d_arr( arr ){
- d_base_arr = arr;
- while( d_base_arr.getKind()==STORE ){
- Node ri = m->getRepresentative( d_base_arr[1] );
- if( d_values.find( ri )==d_values.end() ){
- d_values[ ri ] = m->getRepresentative( d_base_arr[2] );
- }
- d_base_arr = d_base_arr[0];
- }
-}
-
-Node ArrayModel::getValue( TheoryModel* m, Node i ){
- i = m->getRepresentative( i );
- std::map< Node, Node >::iterator it = d_values.find( i );
- if( it!=d_values.end() ){
- return it->second;
- }else{
- return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i );
- //return d_default_value; //TODO: guarantee I can return this here
- }
-}
-
-void ArrayModel::setValue( TheoryModel* m, Node i, Node e ){
- Node ri = m->getRepresentative( i );
- if( d_values.find( ri )==d_values.end() ){
- d_values[ ri ] = m->getRepresentative( e );
- }
-}
-
-void ArrayModel::setDefaultArray( Node arr ){
- d_base_arr = arr;
-}
-
-Node ArrayModel::getArrayValue(){
- Node curr = d_base_arr;
- for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){
- curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );
- }
- return curr;
-}
+++ /dev/null
-/********************* */
-/*! \file theory_arrays_model.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief MODEL for theory of arrays
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_ARRAYS_MODEL_H
-#define __CVC4__THEORY_ARRAYS_MODEL_H
-
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class TheoryModel;
-
-namespace arrays {
-
-class ArrayModel{
-protected:
- /** the array this model is for */
- Node d_arr;
-public:
- ArrayModel(){}
- ArrayModel( Node arr, TheoryModel* m );
- ~ArrayModel() {}
-public:
- /** pre-defined values */
- std::map< Node, Node > d_values;
- /** base array */
- Node d_base_arr;
- /** get value, return arguments that the value depends on */
- Node getValue( TheoryModel* m, Node i );
- /** set value */
- void setValue( TheoryModel* m, Node i, Node e );
- /** set default */
- void setDefaultArray( Node arr );
-public:
- /** get array value */
- Node getArrayValue();
-};/* class ArrayModel */
-
-}
-}
-}
-
-#endif
\ No newline at end of file
model_engine.cpp \
modes.cpp \
modes.h \
- relevant_domain.h \
- relevant_domain.cpp \
term_database.h \
term_database.cpp \
first_order_model.h \
}\r
}\r
Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;\r
- l = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), l );\r
- u = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), u );\r
+ l = d_quantEngine->getModel()->getCurrentModelValue( l );\r
+ u = d_quantEngine->getModel()->getCurrentModelValue( u );\r
Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;\r
return;\r
}\r
}
}
-void FirstOrderModel::reset(){
- TheoryModel::reset();
+Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
+ std::vector< Node > children;
+ if( n.getNumChildren()>0 ){
+ if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ for (unsigned i=0; i<n.getNumChildren(); i++) {
+ Node nc = getCurrentModelValue( n[i], partial );
+ if (nc.isNull()) {
+ return Node::null();
+ }else{
+ children.push_back( nc );
+ }
+ }
+ if( n.getKind()==APPLY_UF ){
+ return getCurrentUfModelValue( n, children, partial );
+ }else{
+ Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ nn = Rewriter::rewrite( nn );
+ return nn;
+ }
+ }else{
+ return getRepresentative(n);
+ }
}
-void FirstOrderModel::initialize( bool considerAxioms ){
- //rebuild models
- d_uf_model_tree.clear();
- d_uf_model_gen.clear();
- d_array_model.clear();
+void FirstOrderModel::initialize( bool considerAxioms ) {
+ processInitialize();
//this is called after representatives have been chosen and the equality engine has been built
//for each quantifier, collect all operators we care about
for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
}
void FirstOrderModel::initializeModelForTerm( Node n ){
+ processInitializeModelForTerm( n );
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ initializeModelForTerm( n[i] );
+ }
+}
+
+FirstOrderModelIG::FirstOrderModelIG(context::Context* c, std::string name) : FirstOrderModel(c,name) {
+
+}
+
+void FirstOrderModelIG::processInitialize(){
+ //rebuild models
+ d_uf_model_tree.clear();
+ d_uf_model_gen.clear();
+}
+
+void FirstOrderModelIG::processInitializeModelForTerm( Node n ){
if( n.getKind()==APPLY_UF ){
Node op = n.getOperator();
if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){
}
}
*/
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- initializeModelForTerm( n[i] );
- }
}
//for evaluation of quantifier bodies
-void FirstOrderModel::resetEvaluate(){
+void FirstOrderModelIG::resetEvaluate(){
d_eval_uf_use_default.clear();
d_eval_uf_model.clear();
d_eval_term_index_order.clear();
// if eVal = 0, then n' cannot be proven to be equal to phaseReq
// if eVal is not 0, then
// each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
-int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
+int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
++d_eval_formulas;
//Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
//Notice() << "Eval " << n << std::endl;
}
}
-Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
+Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
//Message() << "Eval term " << n << std::endl;
Node val;
depIndex = ri->getNumTerms()-1;
return val;
}
-Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){
+Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){
depIndex = -1;
if( n.getNumChildren()==0 ){
return n;
}
}
-void FirstOrderModel::clearEvalFailed( int index ){
+void FirstOrderModelIG::clearEvalFailed( int index ){
for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
}
d_eval_failed_lits[index].clear();
}
-void FirstOrderModel::makeEvalUfModel( Node n ){
+void FirstOrderModelIG::makeEvalUfModel( Node n ){
if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){
makeEvalUfIndexOrder( n );
if( !d_eval_uf_use_default[n] ){
bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
};
-void FirstOrderModel::makeEvalUfIndexOrder( Node n ){
+void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){
if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
#ifdef USE_INDEX_ORDERING
//sort arguments in order of least significant vs. most significant variable in default ordering
#endif
}
}
+
+Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
+ std::vector< Node > children;
+ children.push_back(n.getOperator());
+ children.insert(children.end(), args.begin(), args.end());
+ Node nv = NodeManager::currentNM()->mkNode(APPLY_UF, children);
+ //make the term model specifically for nv
+ makeEvalUfModel( nv );
+ int argDepIndex;
+ if( d_eval_uf_use_default[nv] ){
+ return d_uf_model_tree[ n.getOperator() ].getValue( this, nv, argDepIndex );
+ }else{
+ return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex );
+ }
+}
\ No newline at end of file
#include "theory/model.h"
#include "theory/uf/theory_uf_model.h"
-#include "theory/arrays/theory_arrays_model.h"
namespace CVC4 {
namespace theory {
class TermDb;
+class FirstOrderModelIG;
+namespace fmcheck {
+ class FirstOrderModelFmc;
+}
+
class FirstOrderModel : public TheoryModel
{
private:
- //for initialize model
- void initializeModelForTerm( Node n );
/** whether an axiom is asserted */
context::CDO< bool > d_axiom_asserted;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
/** is model set */
context::CDO< bool > d_isModelSet;
-public: //for Theory UF:
- //models for each UF operator
- std::map< Node, uf::UfModelTree > d_uf_model_tree;
- //model generators
- std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
-private:
- //map from terms to the models used to calculate their value
- std::map< Node, bool > d_eval_uf_use_default;
- std::map< Node, uf::UfModelTree > d_eval_uf_model;
- void makeEvalUfModel( Node n );
- //index ordering to use for each term
- std::map< Node, std::vector< int > > d_eval_term_index_order;
- void makeEvalUfIndexOrder( Node n );
-public: //for Theory Arrays:
- //default value for each non-store array
- std::map< Node, arrays::ArrayModel > d_array_model;
+ /** get current model value */
+ virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
public: //for Theory Quantifiers:
/** assert quantifier */
void assertQuantifier( Node n );
Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
/** bool axiom asserted */
bool isAxiomAsserted() { return d_axiom_asserted; }
+ /** initialize model for term */
+ void initializeModelForTerm( Node n );
+ virtual void processInitializeModelForTerm( Node n ) = 0;
public:
FirstOrderModel( context::Context* c, std::string name );
virtual ~FirstOrderModel(){}
- // reset the model
- void reset();
+ virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
+ virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
// initialize the model
void initialize( bool considerAxioms = true );
+ virtual void processInitialize() = 0;
/** mark model set */
void markModelSet() { d_isModelSet = true; }
/** is model set */
bool isModelSet() { return d_isModelSet; }
+ /** get current model value */
+ Node getCurrentModelValue( Node n, bool partial = false );
+};/* class FirstOrderModel */
+
+
+class FirstOrderModelIG : public FirstOrderModel
+{
+public: //for Theory UF:
+ //models for each UF operator
+ std::map< Node, uf::UfModelTree > d_uf_model_tree;
+ //model generators
+ std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
+private:
+ //map from terms to the models used to calculate their value
+ std::map< Node, bool > d_eval_uf_use_default;
+ std::map< Node, uf::UfModelTree > d_eval_uf_model;
+ void makeEvalUfModel( Node n );
+ //index ordering to use for each term
+ std::map< Node, std::vector< int > > d_eval_term_index_order;
+ void makeEvalUfIndexOrder( Node n );
+ /** get current model value */
+ Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
//the following functions are for evaluating quantifier bodies
public:
+ FirstOrderModelIG(context::Context* c, std::string name);
+ FirstOrderModelIG * asFirstOrderModelIG() { return this; }
+ // initialize the model
+ void processInitialize();
+ //for initialize model
+ void processInitializeModelForTerm( Node n );
/** reset evaluation */
void resetEvaluate();
/** evaluate functions */
void clearEvalFailed( int index );
std::map< Node, bool > d_eval_failed;
std::map< int, std::vector< Node > > d_eval_failed_lits;
-};/* class FirstOrderModel */
+};
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
using namespace CVC4::theory::inst;\r
using namespace CVC4::theory::quantifiers::fmcheck;\r
\r
+struct ModelBasisArgSort\r
+{\r
+ std::vector< Node > d_terms;\r
+ bool operator() (int i,int j) {\r
+ return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <\r
+ d_terms[j].getAttribute(ModelBasisArgAttribute()) );\r
+ }\r
+};\r
\r
-bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {\r
+\r
+bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {\r
if (index==(int)c.getNumChildren()) {\r
return d_data!=-1;\r
}else{\r
}\r
}\r
\r
-int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index ) {\r
+int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {\r
if (index==(int)inst.size()) {\r
return d_data;\r
}else{\r
}\r
}\r
\r
-void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int index ) {\r
+void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) {\r
if (index==(int)c.getNumChildren()) {\r
if(d_data==-1) {\r
d_data = data;\r
}\r
}\r
\r
-void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {\r
+void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {\r
if (index==(int)c.getNumChildren()) {\r
if( d_data!=-1) {\r
if( is_gen ){\r
}\r
}\r
\r
-bool EntryTrie::getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index) {\r
-\r
- return false;\r
-}\r
-\r
\r
-bool Def::addEntry( FullModelChecker * m, Node c, Node v) {\r
+bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {\r
if (!d_et.hasGeneralization(m, c)) {\r
int newIndex = (int)d_cond.size();\r
if (!d_has_simplified) {\r
}\r
}\r
\r
-Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) {\r
+Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {\r
int gindex = d_et.getGeneralizationIndex(m, inst);\r
if (gindex!=-1) {\r
return d_value[gindex];\r
}\r
}\r
\r
-int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst ) {\r
+int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) {\r
return d_et.getGeneralizationIndex(m, inst);\r
}\r
\r
-void Def::simplify(FullModelChecker * m) {\r
+void Def::simplify(FirstOrderModelFmc * m) {\r
d_has_simplified = true;\r
std::vector< Node > cond;\r
cond.insert( cond.end(), d_cond.begin(), d_cond.end() );\r
}\r
\r
\r
+\r
+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :\r
+FirstOrderModel(c, name), d_qe(qe){\r
+\r
+}\r
+\r
+Node FirstOrderModelFmc::getUsedRepresentative(Node n) {\r
+ //Assert( fm->hasTerm(n) );\r
+ TypeNode tn = n.getType();\r
+ if( tn.isBoolean() ){\r
+ return areEqual(n, d_true) ? d_true : d_false;\r
+ }else{\r
+ Node r = getRepresentative(n);\r
+ if (r==d_model_basis_rep[tn]) {\r
+ r = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+ }\r
+ return r;\r
+ }\r
+}\r
+\r
+Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {\r
+ Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;\r
+ for(unsigned i=0; i<args.size(); i++) {\r
+ args[i] = getUsedRepresentative(args[i]);\r
+ }\r
+ Assert( n.getKind()==APPLY_UF );\r
+ return d_models[n.getOperator()]->evaluate(this, args);\r
+}\r
+\r
+void FirstOrderModelFmc::processInitialize() {\r
+ for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){\r
+ it->second->reset();\r
+ }\r
+ d_model_basis_rep.clear();\r
+}\r
+\r
+void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {\r
+ if( n.getKind()==APPLY_UF ){\r
+ if( d_models.find(n.getOperator())==d_models.end()) {\r
+ d_models[n.getOperator()] = new Def;\r
+ }\r
+ }\r
+}\r
+\r
+Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){\r
+ //check if there is even any domain elements at all\r
+ if (!d_rep_set.hasType(tn)) {\r
+ Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;\r
+ Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+ d_rep_set.d_type_reps[tn].push_back(mbt);\r
+ }else if( d_rep_set.d_type_reps[tn].size()==0 ){\r
+ Message() << "empty reps" << std::endl;\r
+ exit(0);\r
+ }\r
+ return d_rep_set.d_type_reps[tn][0];\r
+}\r
+\r
+\r
+bool FirstOrderModelFmc::isStar(Node n) {\r
+ return n==getStar(n.getType());\r
+}\r
+\r
+Node FirstOrderModelFmc::getStar(TypeNode tn) {\r
+ if( d_type_star.find(tn)==d_type_star.end() ){\r
+ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );\r
+ d_type_star[tn] = st;\r
+ }\r
+ return d_type_star[tn];\r
+}\r
+\r
+bool FirstOrderModelFmc::isModelBasisTerm(Node n) {\r
+ return n==getModelBasisTerm(n.getType());\r
+}\r
+\r
+Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) {\r
+ return d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+}\r
+\r
+Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {\r
+ TypeNode type = op.getType();\r
+ std::vector< Node > vars;\r
+ for( size_t i=0; i<type.getNumChildren()-1; i++ ){\r
+ std::stringstream ss;\r
+ ss << argPrefix << (i+1);\r
+ vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );\r
+ }\r
+ Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);\r
+ Node curr;\r
+ for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {\r
+ Node v = getUsedRepresentative( d_models[op]->d_value[i] );\r
+ if( curr.isNull() ){\r
+ curr = v;\r
+ }else{\r
+ //make the condition\r
+ Node cond = d_models[op]->d_cond[i];\r
+ std::vector< Node > children;\r
+ for( unsigned j=0; j<cond.getNumChildren(); j++) {\r
+ if (!isStar(cond[j])){\r
+ Node c = getUsedRepresentative( cond[j] );\r
+ children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );\r
+ }\r
+ }\r
+ Assert( !children.empty() );\r
+ Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );\r
+ curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );\r
+ }\r
+ }\r
+ curr = Rewriter::rewrite( curr );\r
+ return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);\r
+}\r
+\r
+\r
+\r
FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :\r
QModelBuilder( c, qe ){\r
d_true = NodeManager::currentNM()->mkConst(true);\r
d_false = NodeManager::currentNM()->mkConst(false);\r
}\r
\r
-\r
void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){\r
d_addedLemmas = 0;\r
- FirstOrderModel* fm = (FirstOrderModel*)m;\r
+ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();\r
if( fullModel ){\r
//make function values\r
for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){\r
TheoryEngineModelBuilder::processBuildModel( m, fullModel );\r
//mark that the model has been set\r
fm->markModelSet();\r
+ //debug the model\r
+ debugModel( fm );\r
}else{\r
Trace("fmc") << "---Full Model Check reset() " << std::endl;\r
- for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){\r
- it->second->reset();\r
- }\r
+ fm->initialize( d_considerAxioms );\r
d_quant_models.clear();\r
- d_models_init.clear();\r
d_rep_ids.clear();\r
- d_model_basis_rep.clear();\r
d_star_insts.clear();\r
//process representatives\r
for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();\r
if( it->first.isSort() ){\r
Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;\r
Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);\r
- Node rmbt = fm->getRepresentative(mbt);\r
+ Node rmbt = fm->getUsedRepresentative( mbt);\r
int mbt_index = -1;\r
Trace("fmc") << " Model basis term : " << mbt << std::endl;\r
for( size_t a=0; a<it->second.size(); a++ ){\r
- //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );\r
- //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );\r
- Node r = fm->getRepresentative( it->second[a] );\r
+ Node r = fm->getUsedRepresentative( it->second[a] );\r
std::vector< Node > eqc;\r
((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );\r
Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);\r
\r
//if this is the model basis eqc, replace with actual model basis term\r
if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {\r
- d_model_basis_rep[it->first] = r;\r
+ fm->d_model_basis_rep[it->first] = r;\r
r = mbt;\r
mbt_index = a;\r
}\r
}\r
}\r
}\r
- }\r
-}\r
-\r
-Node FullModelChecker::getRepresentative(FirstOrderModel * fm, Node n) {\r
- //Assert( fm->hasTerm(n) );\r
- TypeNode tn = n.getType();\r
- if( tn.isBoolean() ){\r
- return fm->areEqual(n, d_true) ? d_true : d_false;\r
- }else{\r
- Node r = fm->getRepresentative(n);\r
- if (r==d_model_basis_rep[tn]) {\r
- r = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
- }\r
- return r;\r
- }\r
-}\r
-\r
-struct ModelBasisArgSort\r
-{\r
- std::vector< Node > d_terms;\r
- bool operator() (int i,int j) {\r
- return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <\r
- d_terms[j].getAttribute(ModelBasisArgAttribute()) );\r
- }\r
-};\r
-\r
-void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v,\r
- std::vector< Node > & conds,\r
- std::vector< Node > & values,\r
- std::vector< Node > & entry_conds ) {\r
- std::vector< Node > children;\r
- std::vector< Node > entry_children;\r
- children.push_back(op);\r
- entry_children.push_back(op);\r
- bool hasNonStar = false;\r
- for( unsigned i=0; i<c.getNumChildren(); i++) {\r
- Node ri = getRepresentative(fm, c[i]);\r
- children.push_back(ri);\r
- if (isModelBasisTerm(ri)) {\r
- ri = getStar( ri.getType() );\r
- }else{\r
- hasNonStar = true;\r
- }\r
- entry_children.push_back(ri);\r
- }\r
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
- Node nv = getRepresentative(fm, v);\r
- Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );\r
- if( std::find(conds.begin(), conds.end(), n )==conds.end() ){\r
- Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
- conds.push_back(n);\r
- values.push_back(nv);\r
- entry_conds.push_back(en);\r
- }\r
-}\r
-\r
-Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {\r
- if( d_models_init.find(op)==d_models_init.end() ){\r
- if( d_models.find(op)==d_models.end() ){\r
- d_models[op] = new Def;\r
- }\r
- //reset the model\r
- d_models[op]->reset();\r
-\r
- std::vector< Node > conds;\r
- std::vector< Node > values;\r
- std::vector< Node > entry_conds;\r
- Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;\r
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
- Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);\r
- Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;\r
- }\r
- Trace("fmc-model-debug") << std::endl;\r
- //initialize the model\r
- /*\r
- for( int j=0; j<2; j++ ){\r
- for( int k=1; k>=0; k-- ){\r
- Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;\r
- for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[j][k].begin();\r
- it != fm->d_uf_model_gen[op].d_set_values[j][k].end(); ++it ){\r
- Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl;\r
- if( j==1 ){\r
- addEntry(fm, op, it->first, it->second, conds, values, entry_conds);\r
- }\r
+ //now, make models\r
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
+ Node op = it->first;\r
+ //reset the model\r
+ fm->d_models[op]->reset();\r
+\r
+ std::vector< Node > conds;\r
+ std::vector< Node > values;\r
+ std::vector< Node > entry_conds;\r
+ Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;\r
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
+ Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]);\r
+ Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;\r
+ }\r
+ Trace("fmc-model-debug") << std::endl;\r
+ //initialize the model\r
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
+ Node n = fm->d_uf_terms[op][i];\r
+ if( !n.getAttribute(NoMatchAttribute()) ){\r
+ addEntry(fm, op, n, n, conds, values, entry_conds);\r
}\r
}\r
- }\r
- */\r
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
- Node n = fm->d_uf_terms[op][i];\r
- if( !n.getAttribute(NoMatchAttribute()) ){\r
- addEntry(fm, op, n, n, conds, values, entry_conds);\r
+ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
+ //add default value\r
+ if( fm->hasTerm( nmb ) ){\r
+ Trace("fmc-model-debug") << "Add default " << nmb << std::endl;\r
+ addEntry(fm, op, nmb, nmb, conds, values, entry_conds);\r
+ }else{\r
+ Node vmb = fm->getSomeDomainElement(nmb.getType());\r
+ Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";\r
+ Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;\r
+ addEntry(fm, op, nmb, vmb, conds, values, entry_conds);\r
}\r
- }\r
- Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
- //add default value\r
- if( fm->hasTerm( nmb ) ){\r
- Trace("fmc-model-debug") << "Add default " << nmb << std::endl;\r
- addEntry(fm, op, nmb, nmb, conds, values, entry_conds);\r
- }else{\r
- Node vmb = getSomeDomainElement( fm, nmb.getType() );\r
- Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";\r
- Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;\r
- addEntry(fm, op, nmb, vmb, conds, values, entry_conds);\r
- }\r
-\r
- //sort based on # default arguments\r
- std::vector< int > indices;\r
- ModelBasisArgSort mbas;\r
- for (int i=0; i<(int)conds.size(); i++) {\r
- d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );\r
- mbas.d_terms.push_back(conds[i]);\r
- indices.push_back(i);\r
- }\r
- std::sort( indices.begin(), indices.end(), mbas );\r
\r
+ //sort based on # default arguments\r
+ std::vector< int > indices;\r
+ ModelBasisArgSort mbas;\r
+ for (int i=0; i<(int)conds.size(); i++) {\r
+ d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );\r
+ mbas.d_terms.push_back(conds[i]);\r
+ indices.push_back(i);\r
+ }\r
+ std::sort( indices.begin(), indices.end(), mbas );\r
\r
- for (int i=0; i<(int)indices.size(); i++) {\r
- d_models[op]->addEntry(this, entry_conds[indices[i]], values[indices[i]]);\r
- }\r
- d_models[op]->debugPrint("fmc-model", op, this);\r
- Trace("fmc-model") << std::endl;\r
\r
- d_models[op]->simplify( this );\r
- Trace("fmc-model-simplify") << "After simplification : " << std::endl;\r
- d_models[op]->debugPrint("fmc-model-simplify", op, this);\r
- Trace("fmc-model-simplify") << std::endl;\r
+ for (int i=0; i<(int)indices.size(); i++) {\r
+ fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);\r
+ }\r
+ fm->d_models[op]->debugPrint("fmc-model", op, this);\r
+ Trace("fmc-model") << std::endl;\r
\r
- d_models_init[op] = true;\r
+ fm->d_models[op]->simplify( fm );\r
+ Trace("fmc-model-simplify") << "After simplification : " << std::endl;\r
+ fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);\r
+ Trace("fmc-model-simplify") << std::endl;\r
+ }\r
}\r
- return d_models[op];\r
-}\r
-\r
-\r
-bool FullModelChecker::isStar(Node n) {\r
- return n==getStar(n.getType());\r
-}\r
-\r
-bool FullModelChecker::isModelBasisTerm(Node n) {\r
- return n==getModelBasisTerm(n.getType());\r
-}\r
-\r
-Node FullModelChecker::getModelBasisTerm(TypeNode tn) {\r
- return d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
}\r
\r
void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {\r
}\r
\r
void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {\r
+ FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();\r
if( n.isNull() ){\r
Trace(tr) << "null";\r
}\r
- else if(isStar(n) && dispStar) {\r
+ else if(fm->isStar(n) && dispStar) {\r
Trace(tr) << "*";\r
}else{\r
TypeNode tn = n.getType();\r
if (!options::fmfModelBasedInst()) {\r
return false;\r
}else{\r
+ FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();\r
if (effort==0) {\r
//register the quantifier\r
if (d_quant_cond.find(f)==d_quant_cond.end()) {\r
}\r
\r
//model check the quantifier\r
- doCheck(fm, f, d_quant_models[f], f[1]);\r
+ doCheck(fmfmc, f, d_quant_models[f], f[1]);\r
Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;\r
d_quant_models[f].debugPrint("fmc", Node::null(), this);\r
Trace("fmc") << std::endl;\r
bool hasStar = false;\r
std::vector< Node > inst;\r
for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {\r
- if (isStar(d_quant_models[f].d_cond[i][j])) {\r
+ if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {\r
hasStar = true;\r
- inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));\r
+ inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));\r
}else{\r
inst.push_back(d_quant_models[f].d_cond[i][j]);\r
}\r
bool addInst = true;\r
if( hasStar ){\r
//try obvious (specified by inst)\r
- Node ev = d_quant_models[f].evaluate(this, inst);\r
+ Node ev = d_quant_models[f].evaluate(fmfmc, inst);\r
if (ev==d_true) {\r
addInst = false;\r
}\r
}else{\r
//for debugging\r
if (Trace.isOn("fmc-test-inst")) {\r
- Node ev = d_quant_models[f].evaluate(this, inst);\r
+ Node ev = d_quant_models[f].evaluate(fmfmc, inst);\r
if( ev==d_true ){\r
std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;\r
exit(0);\r
for( int i=(d_star_insts[f].size()-1); i>=0; i--) {\r
//get witness for d_star_insts[f][i]\r
int j = d_star_insts[f][i];\r
- if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
- int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );\r
+ if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
+ int lem = exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j );\r
if( lem==-1 ){\r
//something went wrong, resort to exhaustive instantiation\r
return false;\r
}\r
}\r
\r
-int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {\r
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {\r
int addedLemmas = 0;\r
RepSetIterator riter( d_qe, &(fm->d_rep_set) );\r
Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";\r
TypeNode tn = c[i].getType();\r
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
//RepDomain rd;\r
- if( isStar(c[i]) ){\r
+ if( fm->isStar(c[i]) ){\r
//add the full range\r
//for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();\r
// it != d_rep_ids[tn].end(); ++it ){\r
std::vector< Node > inst;\r
for( int i=0; i<riter.getNumTerms(); i++ ){\r
//m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );\r
- Node r = getRepresentative( fm, riter.getTerm( i ) );\r
+ Node r = fm->getUsedRepresentative( riter.getTerm( i ) );\r
debugPrint("fmc-exh-debug", r);\r
Trace("fmc-exh-debug") << " ";\r
inst.push_back(r);\r
}\r
\r
- int ev_index = d_quant_models[f].getGeneralizationIndex(this, inst);\r
+ int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);\r
Trace("fmc-exh-debug") << ", index = " << ev_index;\r
Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];\r
if (ev!=d_true) {\r
return addedLemmas;\r
}\r
\r
-void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {\r
+void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {\r
Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;\r
if( n.getKind() == kind::BOUND_VARIABLE ){\r
- d.addEntry(this, mkCondDefault(f), n);\r
+ d.addEntry(fm, mkCondDefault(fm, f), n);\r
Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;\r
}\r
else if( n.getNumChildren()==0 ){\r
Node r = n;\r
if( !fm->hasTerm(n) ){\r
- r = getSomeDomainElement( fm, n.getType() );\r
+ r = fm->getSomeDomainElement(n.getType() );\r
}\r
- r = getRepresentative(fm, r);\r
- d.addEntry(this, mkCondDefault(f), r);\r
+ r = fm->getUsedRepresentative( r);\r
+ d.addEntry(fm, mkCondDefault(fm, f), r);\r
}\r
else if( n.getKind() == kind::NOT ){\r
//just do directly\r
doNegate( d );\r
}\r
else if( n.getKind() == kind::FORALL ){\r
- d.addEntry(this, mkCondDefault(f), Node::null());\r
+ d.addEntry(fm, mkCondDefault(fm, f), Node::null());\r
}\r
else{\r
std::vector< int > var_ch;\r
}else{\r
Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;\r
std::vector< Node > cond;\r
- mkCondDefaultVec(f, cond);\r
+ mkCondDefaultVec(fm, f, cond);\r
std::vector< Node > val;\r
//interpreted compose\r
doInterpretedCompose( fm, f, d, n, children, 0, cond, val );\r
}\r
}\r
- d.simplify(this);\r
+ d.simplify(fm);\r
}\r
Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;\r
d.debugPrint("fmc-debug", Node::null(), this);\r
}\r
}\r
\r
-void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ) {\r
+void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) {\r
std::vector<Node> cond;\r
- mkCondDefaultVec(f, cond);\r
+ mkCondDefaultVec(fm, f, cond);\r
if (eq[0]==eq[1]){\r
- d.addEntry(this, mkCond(cond), d_true);\r
+ d.addEntry(fm, mkCond(cond), d_true);\r
}else{\r
int j = getVariableId(f, eq[0]);\r
int k = getVariableId(f, eq[1]);\r
TypeNode tn = eq[0].getType();\r
if( !fm->d_rep_set.hasType( tn ) ){\r
- getSomeDomainElement( fm, tn ); //to verify the type is initialized\r
+ fm->getSomeDomainElement( tn ); //to verify the type is initialized\r
}\r
for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {\r
- Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );\r
+ Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );\r
cond[j+1] = r;\r
cond[k+1] = r;\r
- d.addEntry( this, mkCond(cond), d_true);\r
+ d.addEntry( fm, mkCond(cond), d_true);\r
}\r
- d.addEntry(this, mkCondDefault(f), d_false);\r
+ d.addEntry( fm, mkCondDefault(fm, f), d_false);\r
}\r
}\r
\r
-void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v) {\r
+void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {\r
int j = getVariableId(f, v);\r
for (unsigned i=0; i<dc.d_cond.size(); i++) {\r
Node val = dc.d_value[i];\r
if( dc.d_cond[i][j]!=val ){\r
- if (isStar(dc.d_cond[i][j])) {\r
+ if (fm->isStar(dc.d_cond[i][j])) {\r
std::vector<Node> cond;\r
mkCondVec(dc.d_cond[i],cond);\r
cond[j+1] = val;\r
- d.addEntry(this, mkCond(cond), d_true);\r
- cond[j+1] = getStar(val.getType());\r
- d.addEntry(this, mkCond(cond), d_false);\r
+ d.addEntry(fm, mkCond(cond), d_true);\r
+ cond[j+1] = fm->getStar(val.getType());\r
+ d.addEntry(fm, mkCond(cond), d_false);\r
}else{\r
- d.addEntry( this, dc.d_cond[i], d_false);\r
+ d.addEntry( fm, dc.d_cond[i], d_false);\r
}\r
}else{\r
- d.addEntry( this, dc.d_cond[i], d_true);\r
+ d.addEntry( fm, dc.d_cond[i], d_true);\r
}\r
}\r
}\r
\r
-void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {\r
- getModel(fm, op);\r
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {\r
Trace("fmc-uf-debug") << "Definition : " << std::endl;\r
- d_models[op]->debugPrint("fmc-uf-debug", op, this);\r
+ fm->d_models[op]->debugPrint("fmc-uf-debug", op, this);\r
Trace("fmc-uf-debug") << std::endl;\r
\r
std::vector< Node > cond;\r
- mkCondDefaultVec(f, cond);\r
+ mkCondDefaultVec(fm, f, cond);\r
std::vector< Node > val;\r
doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);\r
}\r
\r
-void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,\r
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,\r
std::vector< Def > & dc, int index,\r
std::vector< Node > & cond, std::vector<Node> & val ) {\r
Trace("fmc-uf-process") << "process at " << index << std::endl;\r
if (index==(int)dc.size()) {\r
//we have an entry, now do actual compose\r
std::map< int, Node > entries;\r
- doUninterpretedCompose2( fm, f, entries, 0, cond, val, d_models[op]->d_et);\r
+ doUninterpretedCompose2( fm, f, entries, 0, cond, val, fm->d_models[op]->d_et);\r
//add them to the definition\r
- for( unsigned e=0; e<d_models[op]->d_cond.size(); e++ ){\r
+ for( unsigned e=0; e<fm->d_models[op]->d_cond.size(); e++ ){\r
if ( entries.find(e)!=entries.end() ){\r
- d.addEntry(this, entries[e], d_models[op]->d_value[e] );\r
+ d.addEntry(fm, entries[e], fm->d_models[op]->d_value[e] );\r
}\r
}\r
}else{\r
for (unsigned i=0; i<dc[index].d_cond.size(); i++) {\r
- if (isCompat(cond, dc[index].d_cond[i])!=0) {\r
+ if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {\r
std::vector< Node > new_cond;\r
new_cond.insert(new_cond.end(), cond.begin(), cond.end());\r
- if( doMeet(new_cond, dc[index].d_cond[i]) ){\r
+ if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){\r
Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;\r
val.push_back(dc[index].d_value[i]);\r
doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);\r
}\r
}\r
\r
-void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,\r
+void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,\r
std::map< int, Node > & entries, int index,\r
std::vector< Node > & cond, std::vector< Node > & val,\r
EntryTrie & curr ) {\r
if( v.getKind()==kind::BOUND_VARIABLE ){\r
int j = getVariableId(f, v);\r
Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;\r
- if (!isStar(cond[j+1])) {\r
+ if (!fm->isStar(cond[j+1])) {\r
v = cond[j+1];\r
}else{\r
bind_var = true;\r
cond[j+1] = it->first;\r
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
}\r
- cond[j+1] = getStar(v.getType());\r
+ cond[j+1] = fm->getStar(v.getType());\r
}else{\r
if (curr.d_child.find(v)!=curr.d_child.end()) {\r
Trace("fmc-uf-process") << "follow value..." << std::endl;\r
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);\r
}\r
- Node st = getStar(v.getType());\r
+ Node st = fm->getStar(v.getType());\r
if (curr.d_child.find(st)!=curr.d_child.end()) {\r
Trace("fmc-uf-process") << "follow star..." << std::endl;\r
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);\r
}\r
}\r
\r
-void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,\r
+void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,\r
std::vector< Def > & dc, int index,\r
std::vector< Node > & cond, std::vector<Node> & val ) {\r
if ( index==(int)dc.size() ){\r
Node c = mkCond(cond);\r
Node v = evaluateInterpreted(n, val);\r
- d.addEntry(this, c, v);\r
+ d.addEntry(fm, c, v);\r
}\r
else {\r
TypeNode vtn = n.getType();\r
for (unsigned i=0; i<dc[index].d_cond.size(); i++) {\r
- if (isCompat(cond, dc[index].d_cond[i])!=0) {\r
+ if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {\r
std::vector< Node > new_cond;\r
new_cond.insert(new_cond.end(), cond.begin(), cond.end());\r
- if( doMeet(new_cond, dc[index].d_cond[i]) ){\r
+ if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){\r
bool process = true;\r
if (vtn.isBoolean()) {\r
//short circuit\r
if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||\r
(n.getKind()==AND && dc[index].d_value[i]==d_false) ){\r
Node c = mkCond(new_cond);\r
- d.addEntry(this, c, dc[index].d_value[i]);\r
+ d.addEntry(fm, c, dc[index].d_value[i]);\r
process = false;\r
}\r
}\r
}\r
}\r
\r
-int FullModelChecker::isCompat( std::vector< Node > & cond, Node c ) {\r
+int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {\r
Assert(cond.size()==c.getNumChildren()+1);\r
for (unsigned i=1; i<cond.size(); i++) {\r
- if( cond[i]!=c[i-1] && !isStar(cond[i]) && !isStar(c[i-1]) ) {\r
+ if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {\r
return 0;\r
}\r
}\r
return 1;\r
}\r
\r
-bool FullModelChecker::doMeet( std::vector< Node > & cond, Node c ) {\r
+bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {\r
Assert(cond.size()==c.getNumChildren()+1);\r
for (unsigned i=1; i<cond.size(); i++) {\r
if( cond[i]!=c[i-1] ) {\r
- if( isStar(cond[i]) ){\r
+ if( fm->isStar(cond[i]) ){\r
cond[i] = c[i-1];\r
- }else if( !isStar(c[i-1]) ){\r
+ }else if( !fm->isStar(c[i-1]) ){\r
return false;\r
}\r
}\r
return NodeManager::currentNM()->mkNode(APPLY_UF, cond);\r
}\r
\r
-Node FullModelChecker::mkCondDefault( Node f) {\r
+Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {\r
std::vector< Node > cond;\r
- mkCondDefaultVec(f, cond);\r
+ mkCondDefaultVec(fm, f, cond);\r
return mkCond(cond);\r
}\r
\r
-Node FullModelChecker::getStar(TypeNode tn) {\r
- if( d_type_star.find(tn)==d_type_star.end() ){\r
- Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );\r
- d_type_star[tn] = st;\r
- }\r
- return d_type_star[tn];\r
-}\r
-\r
-Node FullModelChecker::getSomeDomainElement(FirstOrderModel * fm, TypeNode tn){\r
- //check if there is even any domain elements at all\r
- if (!fm->d_rep_set.hasType(tn)) {\r
- Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;\r
- Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
- fm->d_rep_set.d_type_reps[tn].push_back(mbt);\r
- }else if( fm->d_rep_set.d_type_reps[tn].size()==0 ){\r
- Message() << "empty reps" << std::endl;\r
- exit(0);\r
- }\r
- return fm->d_rep_set.d_type_reps[tn][0];\r
-}\r
-\r
-void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {\r
+void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {\r
//get function symbol for f\r
cond.push_back(d_quant_cond[f]);\r
for (unsigned i=0; i<f[0].getNumChildren(); i++) {\r
- Node ts = getStar( f[0][i].getType() );\r
+ Node ts = fm->getStar( f[0][i].getType() );\r
cond.push_back(ts);\r
}\r
}\r
}\r
}\r
\r
-bool FullModelChecker::useSimpleModels() {\r
- return options::fmfFullModelCheckSimple();\r
+Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {\r
+ return fm->getFunctionValue(op, argPrefix);\r
}\r
\r
-Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {\r
- getModel( fm, op );\r
- TypeNode type = op.getType();\r
- std::vector< Node > vars;\r
- for( size_t i=0; i<type.getNumChildren()-1; i++ ){\r
- std::stringstream ss;\r
- ss << argPrefix << (i+1);\r
- vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );\r
- }\r
- Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);\r
- Node curr;\r
- for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {\r
- Node v = fm->getRepresentative( d_models[op]->d_value[i] );\r
- if( curr.isNull() ){\r
- curr = v;\r
+\r
+\r
+void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,\r
+ std::vector< Node > & conds,\r
+ std::vector< Node > & values,\r
+ std::vector< Node > & entry_conds ) {\r
+ std::vector< Node > children;\r
+ std::vector< Node > entry_children;\r
+ children.push_back(op);\r
+ entry_children.push_back(op);\r
+ bool hasNonStar = false;\r
+ for( unsigned i=0; i<c.getNumChildren(); i++) {\r
+ Node ri = fm->getUsedRepresentative( c[i]);\r
+ children.push_back(ri);\r
+ if (fm->isModelBasisTerm(ri)) {\r
+ ri = fm->getStar( ri.getType() );\r
}else{\r
- //make the condition\r
- Node cond = d_models[op]->d_cond[i];\r
- std::vector< Node > children;\r
- for( unsigned j=0; j<cond.getNumChildren(); j++) {\r
- if (!isStar(cond[j])){\r
- Node c = fm->getRepresentative( cond[j] );\r
- children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );\r
- }\r
- }\r
- Assert( !children.empty() );\r
- Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );\r
- curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );\r
+ hasNonStar = true;\r
}\r
+ entry_children.push_back(ri);\r
+ }\r
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
+ Node nv = fm->getUsedRepresentative( v);\r
+ Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );\r
+ if( std::find(conds.begin(), conds.end(), n )==conds.end() ){\r
+ Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
+ conds.push_back(n);\r
+ values.push_back(nv);\r
+ entry_conds.push_back(en);\r
}\r
- curr = Rewriter::rewrite( curr );\r
- return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);\r
}\r
\r
-Node FullModelChecker::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {\r
- Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;\r
- for(unsigned i=0; i<args.size(); i++) {\r
- args[i] = getRepresentative(fm, args[i]);\r
- }\r
- if( n.getKind()==VARIABLE ){\r
- Node r = getRepresentative(fm, n);\r
- return r;\r
- }else if( n.getKind()==APPLY_UF ){\r
- getModel(fm, n.getOperator());\r
- return d_models[n.getOperator()]->evaluate(this, args);\r
- }else{\r
- return Node::null();\r
- }\r
-}
\ No newline at end of file
+bool FullModelChecker::useSimpleModels() {\r
+ return options::fmfFullModelCheckSimple();\r
+}\r
#define FULL_MODEL_CHECK\r
\r
#include "theory/quantifiers/model_builder.h"\r
+#include "theory/quantifiers/first_order_model.h"\r
\r
namespace CVC4 {\r
namespace theory {\r
namespace fmcheck {\r
\r
\r
+class FirstOrderModelFmc;\r
class FullModelChecker;\r
\r
class EntryTrie\r
std::map<Node,EntryTrie> d_child;\r
int d_data;\r
void reset() { d_data = -1; d_child.clear(); }\r
- void addEntry( FullModelChecker * m, Node c, Node v, int data, int index = 0 );\r
- bool hasGeneralization( FullModelChecker * m, Node c, int index = 0 );\r
- int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index = 0 );\r
- void getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );\r
- //if possible, get ground instance of c that evaluates to the entry\r
- bool getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index = 0 );\r
+ void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 );\r
+ bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );\r
+ int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );\r
+ void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );\r
};\r
\r
\r
d_status.clear();\r
d_has_simplified = false;\r
}\r
- bool addEntry( FullModelChecker * m, Node c, Node v);\r
- Node evaluate( FullModelChecker * m, std::vector<Node>& inst );\r
- int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );\r
- void simplify( FullModelChecker * m );\r
+ bool addEntry( FirstOrderModelFmc * m, Node c, Node v);\r
+ Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst );\r
+ int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );\r
+ void simplify( FirstOrderModelFmc * m );\r
void debugPrint(const char * tr, Node op, FullModelChecker * m);\r
};\r
\r
+class FirstOrderModelFmc : public FirstOrderModel\r
+{\r
+ friend class FullModelChecker;\r
+private:\r
+ /** quant engine */\r
+ QuantifiersEngine * d_qe;\r
+ /** models for UF */\r
+ std::map<Node, Def * > d_models;\r
+ std::map<TypeNode, Node > d_model_basis_rep;\r
+ std::map<TypeNode, Node > d_type_star;\r
+ Node getUsedRepresentative(Node n);\r
+ /** get current model value */\r
+ Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );\r
+ void processInitializeModelForTerm(Node n);\r
+public:\r
+ FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);\r
+ FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }\r
+ // initialize the model\r
+ void processInitialize();\r
+\r
+ Node getFunctionValue(Node op, const char* argPrefix );\r
+\r
+ bool isStar(Node n);\r
+ Node getStar(TypeNode tn);\r
+ bool isModelBasisTerm(Node n);\r
+ Node getModelBasisTerm(TypeNode tn);\r
+ Node getSomeDomainElement(TypeNode tn);\r
+};\r
+\r
\r
class FullModelChecker : public QModelBuilder\r
{\r
Node d_true;\r
Node d_false;\r
std::map<TypeNode, std::map< Node, int > > d_rep_ids;\r
- std::map<TypeNode, Node > d_model_basis_rep;\r
- std::map<Node, Def * > d_models;\r
std::map<Node, Def > d_quant_models;\r
- std::map<Node, bool > d_models_init;\r
std::map<Node, Node > d_quant_cond;\r
- std::map<TypeNode, Node > d_type_star;\r
std::map<Node, std::map< Node, int > > d_quant_var_id;\r
std::map<Node, std::vector< int > > d_star_insts;\r
- Node getRepresentative(FirstOrderModel * fm, Node n);\r
- Node normalizeArgReps(FirstOrderModel * fm, Node op, Node n);\r
- void addEntry( FirstOrderModel * fm, Node op, Node c, Node v,\r
+ Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);\r
+ int exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);\r
+protected:\r
+ void addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,\r
std::vector< Node > & conds,\r
std::vector< Node > & values,\r
std::vector< Node > & entry_conds );\r
- int exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index);\r
private:\r
- void doCheck(FirstOrderModel * fm, Node f, Def & d, Node n );\r
+ void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );\r
\r
void doNegate( Def & dc );\r
- void doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq );\r
- void doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v);\r
- void doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, std::vector< Def > & dc );\r
+ void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq );\r
+ void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);\r
+ void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );\r
\r
- void doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,\r
+ void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,\r
std::vector< Def > & dc, int index,\r
std::vector< Node > & cond, std::vector<Node> & val );\r
- void doUninterpretedCompose2( FirstOrderModel * fm, Node f,\r
+ void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,\r
std::map< int, Node > & entries, int index,\r
std::vector< Node > & cond, std::vector< Node > & val,\r
EntryTrie & curr);\r
\r
- void doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,\r
+ void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,\r
std::vector< Def > & dc, int index,\r
std::vector< Node > & cond, std::vector<Node> & val );\r
- int isCompat( std::vector< Node > & cond, Node c );\r
- bool doMeet( std::vector< Node > & cond, Node c );\r
+ int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );\r
+ bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );\r
Node mkCond( std::vector< Node > & cond );\r
- Node mkCondDefault( Node f );\r
- void mkCondDefaultVec( Node f, std::vector< Node > & cond );\r
+ Node mkCondDefault( FirstOrderModelFmc * fm, Node f );\r
+ void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );\r
void mkCondVec( Node n, std::vector< Node > & cond );\r
Node evaluateInterpreted( Node n, std::vector< Node > & vals );\r
public:\r
~FullModelChecker(){}\r
\r
int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }\r
- bool isStar(Node n);\r
- Node getStar(TypeNode tn);\r
- Node getSomeDomainElement(FirstOrderModel * fm, TypeNode tn);\r
- bool isModelBasisTerm(Node n);\r
- Node getModelBasisTerm(TypeNode tn);\r
- Def * getModel(FirstOrderModel * fm, Node op);\r
\r
void debugPrintCond(const char * tr, Node n, bool dispStar = false);\r
void debugPrint(const char * tr, Node n, bool dispStar = false);\r
\r
bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );\r
\r
- bool useSimpleModels();\r
- Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix );\r
+ Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );\r
\r
/** process build model */\r
void processBuildModel(TheoryModel* m, bool fullModel);\r
/** get current model value */\r
- Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );\r
+ Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );\r
+\r
+ bool useSimpleModels();\r
};\r
\r
}\r
#include "theory/uf/theory_uf.h"
#include "theory/uf/theory_uf_model.h"
#include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/arrays/theory_arrays_model.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/model_builder.h"
return options::fmfModelBasedInst();
}
-
-Node QModelBuilder::getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial ) {
- std::vector< Node > children;
- if( n.getNumChildren()>0 ){
- if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- for (unsigned i=0; i<n.getNumChildren(); i++) {
- Node nc = getCurrentModelValue( fm, n[i] );
- if (nc.isNull()) {
- return Node::null();
- }else{
- children.push_back( nc );
+void QModelBuilder::debugModel( FirstOrderModel* fm ){
+ //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
+ if( Trace.isOn("quant-model-warn") ){
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ std::vector< Node > vars;
+ for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+ vars.push_back( f[0][j] );
+ }
+ RepSetIterator riter( d_qe, &(fm->d_rep_set) );
+ riter.setQuantifier( f );
+ while( !riter.isFinished() ){
+ std::vector< Node > terms;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ terms.push_back( riter.getTerm( i ) );
+ }
+ Node n = d_qe->getInstantiation( f, vars, terms );
+ Node val = fm->getValue( n );
+ if( val!=fm->d_true ){
+ Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl;
+ Trace("quant-model-warn") << " " << f << std::endl;
+ Trace("quant-model-warn") << " Evaluates to " << val << std::endl;
+ }
+ riter.increment();
}
- }
- if( n.getKind()==APPLY_UF ){
- return getCurrentUfModelValue( fm, n, children, partial );
- }else{
- Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
- nn = Rewriter::rewrite( nn );
- return nn;
- }
- }else{
- if( n.getKind()==VARIABLE ){
- return getCurrentUfModelValue( fm, n, children, partial );
- }else{
- return n;
}
}
}
+
bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
if( argIndex<(int)n.getNumChildren() ){
Node r;
}
}
+
QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) :
QModelBuilder( c, qe ) {
return n;
}
-void QModelBuilderIG::debugModel( FirstOrderModel* fm ){
- //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
- if( Trace.isOn("quant-model-warn") ){
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- std::vector< Node > vars;
- for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
- vars.push_back( f[0][j] );
- }
- RepSetIterator riter( d_qe, &(fm->d_rep_set) );
- riter.setQuantifier( f );
- while( !riter.isFinished() ){
- std::vector< Node > terms;
- for( int i=0; i<riter.getNumTerms(); i++ ){
- terms.push_back( riter.getTerm( i ) );
- }
- Node n = d_qe->getInstantiation( f, vars, terms );
- Node val = fm->getValue( n );
- if( val!=fm->d_true ){
- Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl;
- Trace("quant-model-warn") << " " << f << std::endl;
- Trace("quant-model-warn") << " Evaluates to " << val << std::endl;
- }
- riter.increment();
- }
- }
- }
-}
-
void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
- FirstOrderModel* fm = (FirstOrderModel*)m;
+ FirstOrderModel* f = (FirstOrderModel*)m;
+ FirstOrderModelIG* fm = f->asFirstOrderModelIG();
if( fullModel ){
Assert( d_curr_model==fm );
//update models
}
void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
+ FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
d_uf_model_constructed.clear();
//determine if any functions are constant
- for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+ for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
Node op = it->first;
TermArgBasisTrie tabt;
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node n = fm->d_uf_terms[op][i];
+ for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
+ Node n = fmig->d_uf_terms[op][i];
//for calculating if op is constant
if( !n.getAttribute(NoMatchAttribute()) ){
- Node v = fm->getRepresentative( n );
+ Node v = fmig->getRepresentative( n );
if( i==0 ){
d_uf_prefs[op].d_const_val = v;
}else if( v!=d_uf_prefs[op].d_const_val ){
if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
if( !n.getAttribute(BasisNoMatchAttribute()) ){
//need to consider if it is not congruent modulo model basis
- if( !tabt.addTerm( fm, n ) ){
+ if( !tabt.addTerm( fmig, n ) ){
BasisNoMatchAttribute bnma;
n.setAttribute(bnma,true);
}
}
}
if( !d_uf_prefs[op].d_const_val.isNull() ){
- fm->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
- fm->d_uf_model_gen[op].makeModel( fm, it->second );
+ fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
+ fmig->d_uf_model_gen[op].makeModel( fmig, it->second );
Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
- fm->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
+ fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
Debug("fmf-model-cons") << std::endl;
d_uf_model_constructed[op] = true;
}else{
}
void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+ FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
//the pro/con preferences for this quantifier
std::vector< Node > pro_con[2];
for( int j=0; j<2; j++ ){
if( TermDb::hasInstConstAttr(n[j]) ){
if( n[j].getKind()==APPLY_UF &&
- fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
+ fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){
uf_terms.push_back( gn[j] );
isConst = isConst && hasConstantDefinition( gn[j] );
}else{
for( int k=0; k<2; k++ ){
for( int j=0; j<(int)pro_con[k].size(); j++ ){
Node op = pro_con[k][j].getOperator();
- Node r = fm->getRepresentative( pro_con[k][j] );
+ Node r = fmig->getRepresentative( pro_con[k][j] );
d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
}
}
}
void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
+ FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
if( optReconsiderFuncConstants() ){
//reconsider constant functions that weren't necessary
if( d_uf_model_constructed[op] ){
Node v = d_uf_prefs[op].d_const_val;
if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
- fm->d_uf_model_tree[op].clear();
- fm->d_uf_model_gen[op].clear();
+ fmig->d_uf_model_tree[op].clear();
+ fmig->d_uf_model_gen[op].clear();
d_uf_model_constructed[op] = false;
}
}
Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
//set the values in the model
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node n = fm->d_uf_terms[op][i];
+ for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
+ Node n = fmig->d_uf_terms[op][i];
if( isTermActive( n ) ){
- Node v = fm->getRepresentative( n );
- Trace("fmf-model-cons") << "Set term " << n << " : " << fm->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
+ Node v = fmig->getRepresentative( n );
+ Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
//if this assertion did not help the model, just consider it ground
//set n = v in the model tree
//set it as ground value
- fm->d_uf_model_gen[op].setValue( fm, n, v );
- if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){
+ fmig->d_uf_model_gen[op].setValue( fm, n, v );
+ if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
//also set as default value if necessary
if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
Trace("fmf-model-cons") << " Set as default." << std::endl;
- fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+ fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
if( n==defaultTerm ){
//incidentally already set, we will not need to find a default value
setDefaultVal = false;
}
}else{
if( n==defaultTerm ){
- fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+ fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
//incidentally already set, we will not need to find a default value
setDefaultVal = false;
}
//chose defaultVal based on heuristic, currently the best ratio of "pro" responses
Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
if( defaultVal.isNull() ){
- if (!fm->d_rep_set.hasType(defaultTerm.getType())) {
+ if (!fmig->d_rep_set.hasType(defaultTerm.getType())) {
Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType());
- fm->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt);
+ fmig->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt);
}
- defaultVal = fm->d_rep_set.d_type_reps[defaultTerm.getType()][0];
+ defaultVal = fmig->d_rep_set.d_type_reps[defaultTerm.getType()][0];
}
Assert( !defaultVal.isNull() );
- Trace("fmf-model-cons") << "Set default term : " << fm->d_rep_set.getIndexFor( defaultVal ) << std::endl;
- fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
+ Trace("fmf-model-cons") << "Set default term : " << fmig->d_rep_set.getIndexFor( defaultVal ) << std::endl;
+ fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
}
Debug("fmf-model-cons") << " Making model...";
- fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] );
+ fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] );
d_uf_model_constructed[op] = true;
Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl;
}
}
void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
+ FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
bool setDefaultVal = true;
Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
//set the values in the model
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node n = fm->d_uf_terms[op][i];
+ for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
+ Node n = fmig->d_uf_terms[op][i];
if( isTermActive( n ) ){
- Node v = fm->getRepresentative( n );
- fm->d_uf_model_gen[op].setValue( fm, n, v );
+ Node v = fmig->getRepresentative( n );
+ fmig->d_uf_model_gen[op].setValue( fm, n, v );
}
//also possible set as default
if( d_term_selected.find( n )!=d_term_selected.end() || n==defaultTerm ){
- Node v = fm->getRepresentative( n );
- fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+ Node v = fmig->getRepresentative( n );
+ fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
if( n==defaultTerm ){
setDefaultVal = false;
}
//set the overall default value if not set already (is this necessary??)
if( setDefaultVal ){
Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
- fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
+ fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
}
- fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] );
+ fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] );
d_uf_model_constructed[op] = true;
}
context::CDO< FirstOrderModel* > d_curr_model;
//quantifiers engine
QuantifiersEngine* d_qe;
- /** get current model value */
- virtual Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) = 0;
public:
QModelBuilder( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilder(){}
bool d_considerAxioms;
/** exist instantiation ? */
virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
- /** get current model value */
- Node getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial = false );
+ //debug model
+ void debugModel( FirstOrderModel* fm );
};
public:
QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilderIG(){}
- //debug model
- void debugModel( FirstOrderModel* fm );
public:
//whether to add inst-gen lemmas
virtual bool optInstGen();
#include "theory/uf/theory_uf.h"
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/quantifiers/options.h"
-#include "theory/arrays/theory_arrays_model.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/quantifiers_attributes.h"
//Model Engine constructor
ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
-QuantifiersModule( qe ),
-d_rel_domain( qe, qe->getModel() ){
+QuantifiersModule( qe ){
if( options::fmfFullModelCheck() ){
d_builder = new fmcheck::FullModelChecker( c, qe );
}
*/
//compute the relevant domain if necessary
- if( optUseRelevantDomain() ){
- d_rel_domain.compute();
- }
+ //if( optUseRelevantDomain() ){
+ //}
d_triedLemmas = 0;
d_testLemmas = 0;
d_relevantLemmas = 0;
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
if( riter.setQuantifier( f ) ){
- Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
- d_quantEngine->getModel()->resetEvaluate();
+ FirstOrderModelIG * fmig = NULL;
+ if( !options::fmfFullModelCheck() ){
+ fmig = (FirstOrderModelIG*)d_quantEngine->getModel();
+ Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+ fmig->resetEvaluate();
+ }
Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
int tests = 0;
int triedLemmas = 0;
d_testLemmas++;
int eval = 0;
int depIndex;
- if( d_builder->optUseModel() ){
+ if( d_builder->optUseModel() && fmig ){
//see if instantiation is already true in current model
Debug("fmf-model-eval") << "Evaluating ";
riter.debugPrintSmall("fmf-model-eval");
//if evaluate(...)==1, then the instantiation is already true in the model
// depIndex is the index of the least significant variable that this evaluation relies upon
depIndex = riter.getNumTerms()-1;
- eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
+ eval = fmig->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
if( eval==1 ){
Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
}else{
}
}
//print debugging information
- d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
- d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
- d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
- d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
+ if( fmig ){
+ d_statistics.d_eval_formulas += fmig->d_eval_formulas;
+ d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
+ d_statistics.d_eval_lits += fmig->d_eval_lits;
+ d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
+ }
int relevantInst = 1;
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
relevantInst = relevantInst * (int)riter.d_domain[i].size();
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/model_builder.h"
#include "theory/model.h"
-#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/full_model_check.h"
namespace CVC4 {
/** builder class */
QModelBuilder* d_builder;
private: //analysis of current model:
- //relevant domain
- RelevantDomain d_rel_domain;
//is the exhaustive instantiation incomplete?
bool d_incomplete_check;
private:
+++ /dev/null
-/********************* */
-/*! \file relevant_domain.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of relevant domain class
- **/
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/relevant_domain.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){
-
-}
-
-void RelevantDomain::compute(){
- Trace("rel-dom") << "compute relevant domain" << std::endl;
- d_quant_inst_domain.clear();
- for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
- Node f = d_model->getAssertedQuantifier( i );
- d_quant_inst_domain[f].resize( f[0].getNumChildren() );
- }
- Trace("rel-dom") << "account for ground terms" << std::endl;
- //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)
- for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin();
- it != d_model->d_uf_model_tree.end(); ++it ){
- Node op = it->first;
- for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){
- Node n = d_model->d_uf_terms[op][i];
- //add arguments to domain
- for( int j=0; j<(int)n.getNumChildren(); j++ ){
- if( d_model->d_rep_set.hasType( n[j].getType() ) ){
- Node ra = d_model->getRepresentative( n[j] );
- int raIndex = d_model->d_rep_set.getIndexFor( ra );
- if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground domain: rep set does not contain : " << ra << std::endl;
- Assert( raIndex!=-1 );
- if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){
- d_active_domain[op][j].push_back( raIndex );
- }
- }
- }
- //add to range
- Node r = d_model->getRepresentative( n );
- int raIndex = d_model->d_rep_set.getIndexFor( r );
- if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground range: rep set does not contain : " << r << std::endl;
- Assert( raIndex!=-1 );
- if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){
- d_active_range[op].push_back( raIndex );
- }
- }
- }
- Trace("rel-dom") << "do quantifiers" << std::endl;
- //find fixed point for relevant domain computation
- bool success;
- do{
- success = true;
- for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
- Node f = d_model->getAssertedQuantifier( i );
- //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)
- if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getInstConstantBody( f ), Node::null(), -1, f ) ){
- success = false;
- }
- //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)
- RepDomain range;
- if( extendFunctionDomains( d_qe->getTermDatabase()->getInstConstantBody( f ), range ) ){
- success = false;
- }
- }
- }while( !success );
- Trace("rel-dom") << "done compute relevant domain" << std::endl;
- /*
- //debug printing
- Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl;
- if( useRelInstDomain ){
- Trace("rel-dom") << "Relevant domain : " << std::endl;
- for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){
- Trace("rel-dom") << " " << i << " : ";
- for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){
- Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " ";
- }
- Trace("rel-dom") << std::endl;
- }
- }
- */
-}
-
-bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){
- bool domainChanged = false;
- if( n.getKind()==INST_CONSTANT ){
- bool domainSet = false;
- int vi = n.getAttribute(InstVarNumAttribute());
- Assert( !parent.isNull() );
- if( parent.getKind()==APPLY_UF ){
- //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument
- Node op = parent.getOperator();
- if( d_active_domain.find( op )!=d_active_domain.end() ){
- for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){
- int d = d_active_domain[op][arg][i];
- if( std::find( d_quant_inst_domain[f][vi].begin(), d_quant_inst_domain[f][vi].end(), d )==
- d_quant_inst_domain[f][vi].end() ){
- d_quant_inst_domain[f][vi].push_back( d );
- domainChanged = true;
- }
- }
- domainSet = true;
- }
- }
- if( !domainSet ){
- //otherwise, we must consider the entire domain
- TypeNode tn = n.getType();
- if( d_quant_inst_domain_complete[f].find( vi )==d_quant_inst_domain_complete[f].end() ){
- if( d_model->d_rep_set.hasType( tn ) ){
- //it is the complete domain
- d_quant_inst_domain[f][vi].clear();
- for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){
- d_quant_inst_domain[f][vi].push_back( i );
- }
- domainChanged = true;
- }
- d_quant_inst_domain_complete[f][vi] = true;
- }
- }
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( computeRelevantInstantiationDomain( n[i], n, i, f ) ){
- domainChanged = true;
- }
- }
- }
- return domainChanged;
-}
-
-bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
- if( n.getKind()==INST_CONSTANT ){
- Node f = TermDb::getInstConstAttr(n);
- int var = n.getAttribute(InstVarNumAttribute());
- range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );
- return false;
- }else{
- Node op;
- if( n.getKind()==APPLY_UF ){
- op = n.getOperator();
- }
- bool domainChanged = false;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- RepDomain childRange;
- if( extendFunctionDomains( n[i], childRange ) ){
- domainChanged = true;
- }
- if( n.getKind()==APPLY_UF ){
- if( d_active_domain.find( op )!=d_active_domain.end() ){
- for( int j=0; j<(int)childRange.size(); j++ ){
- int v = childRange[j];
- if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){
- d_active_domain[op][i].push_back( v );
- domainChanged = true;
- }
- }
- }else{
- //do this?
- }
- }
- }
- //get the range
- if( TermDb::hasInstConstAttr(n) ){
- if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){
- range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );
- }else{
- //infinite range?
- }
- }else{
- Node r = d_model->getRepresentative( n );
- int index = d_model->d_rep_set.getIndexFor( r );
- if( index==-1 ){
- //we consider all ground terms in bodies of quantifiers to be the first ground representative
- range.push_back( 0 );
- }else{
- range.push_back( index );
- }
- }
- return domainChanged;
- }
-}
\ No newline at end of file
+++ /dev/null
-/********************* */
-/*! \file relevant_domain.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief relevant domain class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class RelevantDomain
-{
-private:
- QuantifiersEngine* d_qe;
- FirstOrderModel* d_model;
-
- //the domain of the arguments for each operator
- std::map< Node, std::map< int, RepDomain > > d_active_domain;
- //the range for each operator
- std::map< Node, RepDomain > d_active_range;
- //for computing relevant instantiation domain, return true if changed
- bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f );
- //for computing extended
- bool extendFunctionDomains( Node n, RepDomain& range );
-public:
- RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
- virtual ~RelevantDomain(){}
- //compute the relevant domain
- void compute();
- //relevant instantiation domain for each quantifier
- std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
- std::map< Node, std::map< int, bool > > d_quant_inst_domain_complete;
-};/* class RelevantDomain */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
d_hasAddedLemma = false;
//the model object
- d_model = new quantifiers::FirstOrderModel( c, "FirstOrderModel" );
+ if( options::fmfFullModelCheck() ){
+ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
+ }else{
+ d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" );
+ }
//add quantifiers modules
if( !options::finiteModelFind() || options::fmfInstEngine() ){
}
int RepSetIterator::domainSize( int i ) {
+ Assert(i>=0);
if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){
return d_domain[i].size();
}else{
counter = (int)d_index.size()-1;
#endif
//increment d_index
- Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+ if( counter>=0){
+ Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+ }
while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){
counter--;
if( counter>=0){
regress/regress0/preprocess \
regress/regress0/unconstrained \
regress/regress0/decision \
+ regress/regress0/fmf \
regress/regress1 \
regress/regress2 \
regress/regress3
projects / cvc5.git / commitdiff