From fbc81b67ac1cfeb3afe37f3299180177faaa1ca6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 23 May 2013 16:45:47 -0500 Subject: [PATCH] Refactoring to prepare for MBQI with integer quantification. Minor bug fixes. --- src/theory/arrays/Makefile.am | 4 +- src/theory/arrays/theory_arrays.cpp | 9 +- src/theory/arrays/theory_arrays_model.cpp | 65 --- src/theory/arrays/theory_arrays_model.h | 58 -- src/theory/quantifiers/Makefile.am | 2 - src/theory/quantifiers/bounded_integers.cpp | 4 +- src/theory/quantifiers/first_order_model.cpp | 82 ++- src/theory/quantifiers/first_order_model.h | 65 ++- src/theory/quantifiers/full_model_check.cpp | 571 +++++++++---------- src/theory/quantifiers/full_model_check.h | 96 ++-- src/theory/quantifiers/model_builder.cpp | 157 +++-- src/theory/quantifiers/model_builder.h | 8 +- src/theory/quantifiers/model_engine.cpp | 31 +- src/theory/quantifiers/model_engine.h | 3 - src/theory/quantifiers/relevant_domain.cpp | 198 ------- src/theory/quantifiers/relevant_domain.h | 54 -- src/theory/quantifiers_engine.cpp | 6 +- src/theory/rep_set.cpp | 5 +- test/Makefile.am | 1 + 19 files changed, 549 insertions(+), 870 deletions(-) delete mode 100644 src/theory/arrays/theory_arrays_model.cpp delete mode 100644 src/theory/arrays/theory_arrays_model.h delete mode 100644 src/theory/quantifiers/relevant_domain.cpp delete mode 100644 src/theory/quantifiers/relevant_domain.h diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index ec834522f..77f102cf8 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -16,9 +16,7 @@ libarrays_la_SOURCES = \ 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 diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 89f1dbf2c..98346d0e3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -21,7 +21,6 @@ #include #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" @@ -495,7 +494,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) } 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()) { @@ -1082,7 +1081,7 @@ void TheoryArrays::checkModel(Effort e) 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 && @@ -1429,7 +1428,7 @@ Node TheoryArrays::getModelValRec(TNode node) } ++d_numGetModelValConflicts; getSatContext()->pop(); - } + } ++te; if (te.isFinished()) { Assert(false); @@ -1466,7 +1465,7 @@ bool TheoryArrays::hasLoop(TNode node, TNode target) return true; } } - + return false; } diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp deleted file mode 100644 index b5c81ef69..000000000 --- a/src/theory/arrays/theory_arrays_model.cpp +++ /dev/null @@ -1,65 +0,0 @@ -/********************* */ -/*! \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; -} diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h deleted file mode 100644 index 66dc80568..000000000 --- a/src/theory/arrays/theory_arrays_model.h +++ /dev/null @@ -1,58 +0,0 @@ -/********************* */ -/*! \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 diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 92d780be4..60f2ee7f7 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -23,8 +23,6 @@ libquantifiers_la_SOURCES = \ model_engine.cpp \ modes.cpp \ modes.h \ - relevant_domain.h \ - relevant_domain.cpp \ term_database.h \ term_database.cpp \ first_order_model.h \ diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 4492e6d2d..e33cd2131 100755 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -355,8 +355,8 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node } } Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl; - l = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), l ); - u = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), u ); + l = d_quantEngine->getModel()->getCurrentModelValue( l ); + u = d_quantEngine->getModel()->getCurrentModelValue( u ); Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl; return; } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index a11729519..cf4381c02 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -38,15 +38,34 @@ void FirstOrderModel::assertQuantifier( Node n ){ } } -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; imkNode( 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; id_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; @@ -226,7 +259,7 @@ int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ } } -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; @@ -342,7 +375,7 @@ Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ 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; @@ -372,14 +405,14 @@ Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< i } } -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] ){ @@ -423,7 +456,7 @@ struct sortGetMaxVariableNum { bool operator() (Node i,Node j) { return (getMaxVariableNum(i) & 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 diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 76f21e19c..491e97097 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -19,7 +19,6 @@ #include "theory/model.h" #include "theory/uf/theory_uf_model.h" -#include "theory/arrays/theory_arrays_model.h" namespace CVC4 { namespace theory { @@ -30,33 +29,22 @@ namespace quantifiers{ 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 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 ); @@ -66,19 +54,51 @@ public: //for Theory Quantifiers: 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 */ @@ -97,7 +117,8 @@ private: 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 */ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index b5d4648a1..2513cb08e 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -24,8 +24,17 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; using namespace CVC4::theory::quantifiers::fmcheck; +struct ModelBasisArgSort +{ + std::vector< Node > d_terms; + bool operator() (int i,int j) { + return (d_terms[i].getAttribute(ModelBasisArgAttribute()) < + d_terms[j].getAttribute(ModelBasisArgAttribute()) ); + } +}; -bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) { + +bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { if (index==(int)c.getNumChildren()) { return d_data!=-1; }else{ @@ -44,7 +53,7 @@ bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) { } } -int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector & inst, int index ) { +int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector & inst, int index ) { if (index==(int)inst.size()) { return d_data; }else{ @@ -64,7 +73,7 @@ int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector & } } -void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int index ) { +void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) { if (index==(int)c.getNumChildren()) { if(d_data==-1) { d_data = data; @@ -75,7 +84,7 @@ void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int in } } -void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector & compat, std::vector & gen, int index, bool is_gen ) { +void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector & compat, std::vector & gen, int index, bool is_gen ) { if (index==(int)c.getNumChildren()) { if( d_data!=-1) { if( is_gen ){ @@ -101,13 +110,8 @@ void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector & com } } -bool EntryTrie::getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector & inst, int index) { - - return false; -} - -bool Def::addEntry( FullModelChecker * m, Node c, Node v) { +bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) { if (!d_et.hasGeneralization(m, c)) { int newIndex = (int)d_cond.size(); if (!d_has_simplified) { @@ -139,7 +143,7 @@ bool Def::addEntry( FullModelChecker * m, Node c, Node v) { } } -Node Def::evaluate( FullModelChecker * m, std::vector& inst ) { +Node Def::evaluate( FirstOrderModelFmc * m, std::vector& inst ) { int gindex = d_et.getGeneralizationIndex(m, inst); if (gindex!=-1) { return d_value[gindex]; @@ -148,11 +152,11 @@ Node Def::evaluate( FullModelChecker * m, std::vector& inst ) { } } -int Def::getGeneralizationIndex( FullModelChecker * m, std::vector& inst ) { +int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector& inst ) { return d_et.getGeneralizationIndex(m, inst); } -void Def::simplify(FullModelChecker * m) { +void Def::simplify(FirstOrderModelFmc * m) { d_has_simplified = true; std::vector< Node > cond; cond.insert( cond.end(), d_cond.begin(), d_cond.end() ); @@ -186,16 +190,128 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } + +FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : +FirstOrderModel(c, name), d_qe(qe){ + +} + +Node FirstOrderModelFmc::getUsedRepresentative(Node n) { + //Assert( fm->hasTerm(n) ); + TypeNode tn = n.getType(); + if( tn.isBoolean() ){ + return areEqual(n, d_true) ? d_true : d_false; + }else{ + Node r = getRepresentative(n); + if (r==d_model_basis_rep[tn]) { + r = d_qe->getTermDatabase()->getModelBasisTerm(tn); + } + return r; + } +} + +Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { + Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl; + for(unsigned i=0; ievaluate(this, args); +} + +void FirstOrderModelFmc::processInitialize() { + for( std::map::iterator it = d_models.begin(); it != d_models.end(); ++it ){ + it->second->reset(); + } + d_model_basis_rep.clear(); +} + +void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { + if( n.getKind()==APPLY_UF ){ + if( d_models.find(n.getOperator())==d_models.end()) { + d_models[n.getOperator()] = new Def; + } + } +} + +Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){ + //check if there is even any domain elements at all + if (!d_rep_set.hasType(tn)) { + Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); + d_rep_set.d_type_reps[tn].push_back(mbt); + }else if( d_rep_set.d_type_reps[tn].size()==0 ){ + Message() << "empty reps" << std::endl; + exit(0); + } + return d_rep_set.d_type_reps[tn][0]; +} + + +bool FirstOrderModelFmc::isStar(Node n) { + return n==getStar(n.getType()); +} + +Node FirstOrderModelFmc::getStar(TypeNode tn) { + if( d_type_star.find(tn)==d_type_star.end() ){ + Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" ); + d_type_star[tn] = st; + } + return d_type_star[tn]; +} + +bool FirstOrderModelFmc::isModelBasisTerm(Node n) { + return n==getModelBasisTerm(n.getType()); +} + +Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) { + return d_qe->getTermDatabase()->getModelBasisTerm(tn); +} + +Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { + TypeNode type = op.getType(); + std::vector< Node > vars; + for( size_t i=0; imkBoundVar( ss.str(), type[i] ) ); + } + 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 = getUsedRepresentative( d_models[op]->d_value[i] ); + if( curr.isNull() ){ + curr = v; + }else{ + //make the condition + Node cond = d_models[op]->d_cond[i]; + std::vector< Node > children; + for( unsigned j=0; jmkNode( EQUAL, vars[j], c ) ); + } + } + Assert( !children.empty() ); + Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); + curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); + } + } + curr = Rewriter::rewrite( curr ); + return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); +} + + + FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) : QModelBuilder( c, qe ){ d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } - void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ d_addedLemmas = 0; - FirstOrderModel* fm = (FirstOrderModel*)m; + FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); if( fullModel ){ //make function values for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){ @@ -204,15 +320,13 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ TheoryEngineModelBuilder::processBuildModel( m, fullModel ); //mark that the model has been set fm->markModelSet(); + //debug the model + debugModel( fm ); }else{ Trace("fmc") << "---Full Model Check reset() " << std::endl; - for( std::map::iterator it = d_models.begin(); it != d_models.end(); ++it ){ - it->second->reset(); - } + fm->initialize( d_considerAxioms ); d_quant_models.clear(); - d_models_init.clear(); d_rep_ids.clear(); - d_model_basis_rep.clear(); d_star_insts.clear(); //process representatives for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); @@ -220,13 +334,11 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ if( it->first.isSort() ){ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first); - Node rmbt = fm->getRepresentative(mbt); + Node rmbt = fm->getUsedRepresentative( mbt); int mbt_index = -1; Trace("fmc") << " Model basis term : " << mbt << std::endl; for( size_t a=0; asecond.size(); a++ ){ - //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] ); - //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 ); - Node r = fm->getRepresentative( it->second[a] ); + Node r = fm->getUsedRepresentative( it->second[a] ); std::vector< Node > eqc; ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt); @@ -241,7 +353,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ //if this is the model basis eqc, replace with actual model basis term if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) { - d_model_basis_rep[it->first] = r; + fm->d_model_basis_rep[it->first] = r; r = mbt; mbt_index = a; } @@ -257,150 +369,63 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } } - } -} - -Node FullModelChecker::getRepresentative(FirstOrderModel * fm, Node n) { - //Assert( fm->hasTerm(n) ); - TypeNode tn = n.getType(); - if( tn.isBoolean() ){ - return fm->areEqual(n, d_true) ? d_true : d_false; - }else{ - Node r = fm->getRepresentative(n); - if (r==d_model_basis_rep[tn]) { - r = d_qe->getTermDatabase()->getModelBasisTerm(tn); - } - return r; - } -} - -struct ModelBasisArgSort -{ - std::vector< Node > d_terms; - bool operator() (int i,int j) { - return (d_terms[i].getAttribute(ModelBasisArgAttribute()) < - d_terms[j].getAttribute(ModelBasisArgAttribute()) ); - } -}; - -void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v, - std::vector< Node > & conds, - std::vector< Node > & values, - std::vector< Node > & entry_conds ) { - std::vector< Node > children; - std::vector< Node > entry_children; - children.push_back(op); - entry_children.push_back(op); - bool hasNonStar = false; - for( unsigned i=0; imkNode( APPLY_UF, children ); - Node nv = getRepresentative(fm, v); - Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); - if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ - Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; - conds.push_back(n); - values.push_back(nv); - entry_conds.push_back(en); - } -} - -Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) { - if( d_models_init.find(op)==d_models_init.end() ){ - if( d_models.find(op)==d_models.end() ){ - d_models[op] = new Def; - } - //reset the model - d_models[op]->reset(); - - std::vector< Node > conds; - std::vector< Node > values; - std::vector< Node > entry_conds; - Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl; - for( size_t i=0; id_uf_terms[op].size(); i++ ){ - Node r = getRepresentative(fm, fm->d_uf_terms[op][i]); - Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl; - } - Trace("fmc-model-debug") << std::endl; - //initialize the model - /* - for( int j=0; j<2; j++ ){ - for( int k=1; k>=0; k-- ){ - Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl; - for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[j][k].begin(); - it != fm->d_uf_model_gen[op].d_set_values[j][k].end(); ++it ){ - Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl; - if( j==1 ){ - addEntry(fm, op, it->first, it->second, conds, values, entry_conds); - } + //now, make models + for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + //reset the model + fm->d_models[op]->reset(); + + std::vector< Node > conds; + std::vector< Node > values; + std::vector< Node > entry_conds; + Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl; + for( size_t i=0; id_uf_terms[op].size(); i++ ){ + Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]); + Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl; + } + Trace("fmc-model-debug") << std::endl; + //initialize the model + for( size_t i=0; id_uf_terms[op].size(); i++ ){ + Node n = fm->d_uf_terms[op][i]; + if( !n.getAttribute(NoMatchAttribute()) ){ + addEntry(fm, op, n, n, conds, values, entry_conds); } } - } - */ - for( size_t i=0; id_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; - if( !n.getAttribute(NoMatchAttribute()) ){ - addEntry(fm, op, n, n, conds, values, entry_conds); + Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op); + //add default value + if( fm->hasTerm( nmb ) ){ + Trace("fmc-model-debug") << "Add default " << nmb << std::endl; + addEntry(fm, op, nmb, nmb, conds, values, entry_conds); + }else{ + Node vmb = fm->getSomeDomainElement(nmb.getType()); + Trace("fmc-model-debug") << "Add default to default representative " << nmb << " "; + Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl; + addEntry(fm, op, nmb, vmb, conds, values, entry_conds); } - } - Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op); - //add default value - if( fm->hasTerm( nmb ) ){ - Trace("fmc-model-debug") << "Add default " << nmb << std::endl; - addEntry(fm, op, nmb, nmb, conds, values, entry_conds); - }else{ - Node vmb = getSomeDomainElement( fm, nmb.getType() ); - Trace("fmc-model-debug") << "Add default to default representative " << nmb << " "; - Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl; - addEntry(fm, op, nmb, vmb, conds, values, entry_conds); - } - - //sort based on # default arguments - std::vector< int > indices; - ModelBasisArgSort mbas; - for (int i=0; i<(int)conds.size(); i++) { - d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] ); - mbas.d_terms.push_back(conds[i]); - indices.push_back(i); - } - std::sort( indices.begin(), indices.end(), mbas ); + //sort based on # default arguments + std::vector< int > indices; + ModelBasisArgSort mbas; + for (int i=0; i<(int)conds.size(); i++) { + d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] ); + mbas.d_terms.push_back(conds[i]); + indices.push_back(i); + } + std::sort( indices.begin(), indices.end(), mbas ); - for (int i=0; i<(int)indices.size(); i++) { - d_models[op]->addEntry(this, entry_conds[indices[i]], values[indices[i]]); - } - d_models[op]->debugPrint("fmc-model", op, this); - Trace("fmc-model") << std::endl; - d_models[op]->simplify( this ); - Trace("fmc-model-simplify") << "After simplification : " << std::endl; - d_models[op]->debugPrint("fmc-model-simplify", op, this); - Trace("fmc-model-simplify") << std::endl; + for (int i=0; i<(int)indices.size(); i++) { + fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]); + } + fm->d_models[op]->debugPrint("fmc-model", op, this); + Trace("fmc-model") << std::endl; - d_models_init[op] = true; + fm->d_models[op]->simplify( fm ); + Trace("fmc-model-simplify") << "After simplification : " << std::endl; + fm->d_models[op]->debugPrint("fmc-model-simplify", op, this); + Trace("fmc-model-simplify") << std::endl; + } } - return d_models[op]; -} - - -bool FullModelChecker::isStar(Node n) { - return n==getStar(n.getType()); -} - -bool FullModelChecker::isModelBasisTerm(Node n) { - return n==getModelBasisTerm(n.getType()); -} - -Node FullModelChecker::getModelBasisTerm(TypeNode tn) { - return d_qe->getTermDatabase()->getModelBasisTerm(tn); } void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) { @@ -413,10 +438,11 @@ void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) { } void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { + FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel(); if( n.isNull() ){ Trace(tr) << "null"; } - else if(isStar(n) && dispStar) { + else if(fm->isStar(n) && dispStar) { Trace(tr) << "*"; }else{ TypeNode tn = n.getType(); @@ -438,6 +464,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if (!options::fmfModelBasedInst()) { return false; }else{ + FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc(); if (effort==0) { //register the quantifier if (d_quant_cond.find(f)==d_quant_cond.end()) { @@ -452,7 +479,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, } //model check the quantifier - doCheck(fm, f, d_quant_models[f], f[1]); + doCheck(fmfmc, f, d_quant_models[f], f[1]); Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; d_quant_models[f].debugPrint("fmc", Node::null(), this); Trace("fmc") << std::endl; @@ -463,9 +490,9 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, bool hasStar = false; std::vector< Node > inst; for (unsigned j=0; jisStar(d_quant_models[f].d_cond[i][j])) { hasStar = true; - inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType())); + inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType())); }else{ inst.push_back(d_quant_models[f].d_cond[i][j]); } @@ -473,14 +500,14 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, bool addInst = true; if( hasStar ){ //try obvious (specified by inst) - Node ev = d_quant_models[f].evaluate(this, inst); + Node ev = d_quant_models[f].evaluate(fmfmc, inst); if (ev==d_true) { addInst = false; } }else{ //for debugging if (Trace.isOn("fmc-test-inst")) { - Node ev = d_quant_models[f].evaluate(this, inst); + Node ev = d_quant_models[f].evaluate(fmfmc, inst); if( ev==d_true ){ std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl; exit(0); @@ -518,8 +545,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, for( int i=(d_star_insts[f].size()-1); i>=0; i--) { //get witness for d_star_insts[f][i] int j = d_star_insts[f][i]; - if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ - int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j ); + if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ + int lem = exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ); if( lem==-1 ){ //something went wrong, resort to exhaustive instantiation return false; @@ -534,7 +561,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, } } -int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) { +int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) { int addedLemmas = 0; RepSetIterator riter( d_qe, &(fm->d_rep_set) ); Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " "; @@ -546,7 +573,7 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c TypeNode tn = c[i].getType(); if( d_rep_ids.find(tn)!=d_rep_ids.end() ){ //RepDomain rd; - if( isStar(c[i]) ){ + if( fm->isStar(c[i]) ){ //add the full range //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin(); // it != d_rep_ids[tn].end(); ++it ){ @@ -573,13 +600,13 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c std::vector< Node > inst; for( int i=0; igetUsedRepresentative( riter.getTerm( i ) ); debugPrint("fmc-exh-debug", r); Trace("fmc-exh-debug") << " "; inst.push_back(r); } - int ev_index = d_quant_models[f].getGeneralizationIndex(this, inst); + int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst); Trace("fmc-exh-debug") << ", index = " << ev_index; Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index]; if (ev!=d_true) { @@ -600,19 +627,19 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c return addedLemmas; } -void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) { +void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) { Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl; if( n.getKind() == kind::BOUND_VARIABLE ){ - d.addEntry(this, mkCondDefault(f), n); + d.addEntry(fm, mkCondDefault(fm, f), n); Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl; } else if( n.getNumChildren()==0 ){ Node r = n; if( !fm->hasTerm(n) ){ - r = getSomeDomainElement( fm, n.getType() ); + r = fm->getSomeDomainElement(n.getType() ); } - r = getRepresentative(fm, r); - d.addEntry(this, mkCondDefault(f), r); + r = fm->getUsedRepresentative( r); + d.addEntry(fm, mkCondDefault(fm, f), r); } else if( n.getKind() == kind::NOT ){ //just do directly @@ -620,7 +647,7 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) { doNegate( d ); } else if( n.getKind() == kind::FORALL ){ - d.addEntry(this, mkCondDefault(f), Node::null()); + d.addEntry(fm, mkCondDefault(fm, f), Node::null()); } else{ std::vector< int > var_ch; @@ -655,13 +682,13 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) { }else{ Trace("fmc-debug") << "Do interpreted compose " << n << std::endl; std::vector< Node > cond; - mkCondDefaultVec(f, cond); + mkCondDefaultVec(fm, f, cond); std::vector< Node > val; //interpreted compose doInterpretedCompose( fm, f, d, n, children, 0, cond, val ); } } - d.simplify(this); + d.simplify(fm); } Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl; d.debugPrint("fmc-debug", Node::null(), this); @@ -676,62 +703,61 @@ void FullModelChecker::doNegate( Def & dc ) { } } -void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ) { +void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) { std::vector cond; - mkCondDefaultVec(f, cond); + mkCondDefaultVec(fm, f, cond); if (eq[0]==eq[1]){ - d.addEntry(this, mkCond(cond), d_true); + d.addEntry(fm, mkCond(cond), d_true); }else{ int j = getVariableId(f, eq[0]); int k = getVariableId(f, eq[1]); TypeNode tn = eq[0].getType(); if( !fm->d_rep_set.hasType( tn ) ){ - getSomeDomainElement( fm, tn ); //to verify the type is initialized + fm->getSomeDomainElement( tn ); //to verify the type is initialized } for (unsigned i=0; id_rep_set.d_type_reps[tn].size(); i++) { - Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] ); + Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] ); cond[j+1] = r; cond[k+1] = r; - d.addEntry( this, mkCond(cond), d_true); + d.addEntry( fm, mkCond(cond), d_true); } - d.addEntry(this, mkCondDefault(f), d_false); + d.addEntry( fm, mkCondDefault(fm, f), d_false); } } -void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v) { +void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) { int j = getVariableId(f, v); for (unsigned i=0; iisStar(dc.d_cond[i][j])) { std::vector cond; mkCondVec(dc.d_cond[i],cond); cond[j+1] = val; - d.addEntry(this, mkCond(cond), d_true); - cond[j+1] = getStar(val.getType()); - d.addEntry(this, mkCond(cond), d_false); + d.addEntry(fm, mkCond(cond), d_true); + cond[j+1] = fm->getStar(val.getType()); + d.addEntry(fm, mkCond(cond), d_false); }else{ - d.addEntry( this, dc.d_cond[i], d_false); + d.addEntry( fm, dc.d_cond[i], d_false); } }else{ - d.addEntry( this, dc.d_cond[i], d_true); + d.addEntry( fm, dc.d_cond[i], d_true); } } } -void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) { - getModel(fm, op); +void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) { Trace("fmc-uf-debug") << "Definition : " << std::endl; - d_models[op]->debugPrint("fmc-uf-debug", op, this); + fm->d_models[op]->debugPrint("fmc-uf-debug", op, this); Trace("fmc-uf-debug") << std::endl; std::vector< Node > cond; - mkCondDefaultVec(f, cond); + mkCondDefaultVec(fm, f, cond); std::vector< Node > val; doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val); } -void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d, +void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d, std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector & val ) { Trace("fmc-uf-process") << "process at " << index << std::endl; @@ -743,19 +769,19 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Nod if (index==(int)dc.size()) { //we have an entry, now do actual compose std::map< int, Node > entries; - doUninterpretedCompose2( fm, f, entries, 0, cond, val, d_models[op]->d_et); + doUninterpretedCompose2( fm, f, entries, 0, cond, val, fm->d_models[op]->d_et); //add them to the definition - for( unsigned e=0; ed_cond.size(); e++ ){ + for( unsigned e=0; ed_models[op]->d_cond.size(); e++ ){ if ( entries.find(e)!=entries.end() ){ - d.addEntry(this, entries[e], d_models[op]->d_value[e] ); + d.addEntry(fm, entries[e], fm->d_models[op]->d_value[e] ); } } }else{ for (unsigned i=0; i new_cond; new_cond.insert(new_cond.end(), cond.begin(), cond.end()); - if( doMeet(new_cond, dc[index].d_cond[i]) ){ + if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){ Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl; val.push_back(dc[index].d_value[i]); doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val); @@ -768,7 +794,7 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Nod } } -void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, +void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, std::map< int, Node > & entries, int index, std::vector< Node > & cond, std::vector< Node > & val, EntryTrie & curr ) { @@ -788,7 +814,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, if( v.getKind()==kind::BOUND_VARIABLE ){ int j = getVariableId(f, v); Trace("fmc-uf-process") << v << " is variable #" << j << std::endl; - if (!isStar(cond[j+1])) { + if (!fm->isStar(cond[j+1])) { v = cond[j+1]; }else{ bind_var = true; @@ -801,13 +827,13 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, cond[j+1] = it->first; doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); } - cond[j+1] = getStar(v.getType()); + cond[j+1] = fm->getStar(v.getType()); }else{ if (curr.d_child.find(v)!=curr.d_child.end()) { Trace("fmc-uf-process") << "follow value..." << std::endl; doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]); } - Node st = getStar(v.getType()); + Node st = fm->getStar(v.getType()); if (curr.d_child.find(st)!=curr.d_child.end()) { Trace("fmc-uf-process") << "follow star..." << std::endl; doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]); @@ -816,28 +842,28 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, } } -void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, +void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector & val ) { if ( index==(int)dc.size() ){ Node c = mkCond(cond); Node v = evaluateInterpreted(n, val); - d.addEntry(this, c, v); + d.addEntry(fm, c, v); } else { TypeNode vtn = n.getType(); for (unsigned i=0; i new_cond; new_cond.insert(new_cond.end(), cond.begin(), cond.end()); - if( doMeet(new_cond, dc[index].d_cond[i]) ){ + if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){ bool process = true; if (vtn.isBoolean()) { //short circuit if( (n.getKind()==OR && dc[index].d_value[i]==d_true) || (n.getKind()==AND && dc[index].d_value[i]==d_false) ){ Node c = mkCond(new_cond); - d.addEntry(this, c, dc[index].d_value[i]); + d.addEntry(fm, c, dc[index].d_value[i]); process = false; } } @@ -852,23 +878,23 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & } } -int FullModelChecker::isCompat( std::vector< Node > & cond, Node c ) { +int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) { Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; iisStar(cond[i]) && !fm->isStar(c[i-1]) ) { return 0; } } return 1; } -bool FullModelChecker::doMeet( std::vector< Node > & cond, Node c ) { +bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) { Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; iisStar(cond[i]) ){ cond[i] = c[i-1]; - }else if( !isStar(c[i-1]) ){ + }else if( !fm->isStar(c[i-1]) ){ return false; } } @@ -880,38 +906,17 @@ Node FullModelChecker::mkCond( std::vector< Node > & cond ) { return NodeManager::currentNM()->mkNode(APPLY_UF, cond); } -Node FullModelChecker::mkCondDefault( Node f) { +Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) { std::vector< Node > cond; - mkCondDefaultVec(f, cond); + mkCondDefaultVec(fm, f, cond); return mkCond(cond); } -Node FullModelChecker::getStar(TypeNode tn) { - if( d_type_star.find(tn)==d_type_star.end() ){ - Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" ); - d_type_star[tn] = st; - } - return d_type_star[tn]; -} - -Node FullModelChecker::getSomeDomainElement(FirstOrderModel * fm, TypeNode tn){ - //check if there is even any domain elements at all - if (!fm->d_rep_set.hasType(tn)) { - Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); - fm->d_rep_set.d_type_reps[tn].push_back(mbt); - }else if( fm->d_rep_set.d_type_reps[tn].size()==0 ){ - Message() << "empty reps" << std::endl; - exit(0); - } - return fm->d_rep_set.d_type_reps[tn][0]; -} - -void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) { +void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) { //get function symbol for f cond.push_back(d_quant_cond[f]); for (unsigned i=0; igetStar( f[0][i].getType() ); cond.push_back(ts); } } @@ -964,56 +969,42 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) } } -bool FullModelChecker::useSimpleModels() { - return options::fmfFullModelCheckSimple(); +Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) { + return fm->getFunctionValue(op, argPrefix); } -Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) { - getModel( fm, op ); - TypeNode type = op.getType(); - std::vector< Node > vars; - for( size_t i=0; imkBoundVar( ss.str(), type[i] ) ); - } - 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 = fm->getRepresentative( d_models[op]->d_value[i] ); - if( curr.isNull() ){ - curr = v; + + +void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v, + std::vector< Node > & conds, + std::vector< Node > & values, + std::vector< Node > & entry_conds ) { + std::vector< Node > children; + std::vector< Node > entry_children; + children.push_back(op); + entry_children.push_back(op); + bool hasNonStar = false; + for( unsigned i=0; igetUsedRepresentative( c[i]); + children.push_back(ri); + if (fm->isModelBasisTerm(ri)) { + ri = fm->getStar( ri.getType() ); }else{ - //make the condition - Node cond = d_models[op]->d_cond[i]; - std::vector< Node > children; - for( unsigned j=0; jgetRepresentative( cond[j] ); - 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 ); - curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); + hasNonStar = true; } + entry_children.push_back(ri); + } + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + Node nv = fm->getUsedRepresentative( v); + Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); + if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ + Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; + conds.push_back(n); + values.push_back(nv); + entry_conds.push_back(en); } - curr = Rewriter::rewrite( curr ); - return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); } -Node FullModelChecker::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) { - Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl; - for(unsigned i=0; ievaluate(this, args); - }else{ - return Node::null(); - } -} \ No newline at end of file +bool FullModelChecker::useSimpleModels() { + return options::fmfFullModelCheckSimple(); +} diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 00a910567..ddf298006 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -14,6 +14,7 @@ #define FULL_MODEL_CHECK #include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/first_order_model.h" namespace CVC4 { namespace theory { @@ -21,6 +22,7 @@ namespace quantifiers { namespace fmcheck { +class FirstOrderModelFmc; class FullModelChecker; class EntryTrie @@ -30,12 +32,10 @@ public: std::map d_child; int d_data; void reset() { d_data = -1; d_child.clear(); } - void addEntry( FullModelChecker * m, Node c, Node v, int data, int index = 0 ); - bool hasGeneralization( FullModelChecker * m, Node c, int index = 0 ); - int getGeneralizationIndex( FullModelChecker * m, std::vector & inst, int index = 0 ); - void getEntries( FullModelChecker * m, Node c, std::vector & compat, std::vector & gen, int index = 0, bool is_gen = true ); - //if possible, get ground instance of c that evaluates to the entry - bool getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector & inst, int index = 0 ); + void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 ); + bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 ); + int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector & inst, int index = 0 ); + void getEntries( FirstOrderModelFmc * m, Node c, std::vector & compat, std::vector & gen, int index = 0, bool is_gen = true ); }; @@ -64,13 +64,42 @@ public: d_status.clear(); d_has_simplified = false; } - bool addEntry( FullModelChecker * m, Node c, Node v); - Node evaluate( FullModelChecker * m, std::vector& inst ); - int getGeneralizationIndex( FullModelChecker * m, std::vector& inst ); - void simplify( FullModelChecker * m ); + bool addEntry( FirstOrderModelFmc * m, Node c, Node v); + Node evaluate( FirstOrderModelFmc * m, std::vector& inst ); + int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector& inst ); + void simplify( FirstOrderModelFmc * m ); void debugPrint(const char * tr, Node op, FullModelChecker * m); }; +class FirstOrderModelFmc : public FirstOrderModel +{ + friend class FullModelChecker; +private: + /** quant engine */ + QuantifiersEngine * d_qe; + /** models for UF */ + std::map d_models; + std::map d_model_basis_rep; + std::map d_type_star; + Node getUsedRepresentative(Node n); + /** get current model value */ + Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); + void processInitializeModelForTerm(Node n); +public: + FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); + FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } + // initialize the model + void processInitialize(); + + Node getFunctionValue(Node op, const char* argPrefix ); + + bool isStar(Node n); + Node getStar(TypeNode tn); + bool isModelBasisTerm(Node n); + Node getModelBasisTerm(TypeNode tn); + Node getSomeDomainElement(TypeNode tn); +}; + class FullModelChecker : public QModelBuilder { @@ -78,45 +107,41 @@ protected: Node d_true; Node d_false; std::map > d_rep_ids; - std::map d_model_basis_rep; - std::map d_models; std::map d_quant_models; - std::map d_models_init; std::map d_quant_cond; - std::map d_type_star; std::map > d_quant_var_id; std::map > d_star_insts; - Node getRepresentative(FirstOrderModel * fm, Node n); - Node normalizeArgReps(FirstOrderModel * fm, Node op, Node n); - void addEntry( FirstOrderModel * fm, Node op, Node c, Node v, + Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); + int exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); +protected: + void addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v, std::vector< Node > & conds, std::vector< Node > & values, std::vector< Node > & entry_conds ); - int exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index); private: - void doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ); + void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ); void doNegate( Def & dc ); - void doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ); - void doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v); - void doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, std::vector< Def > & dc ); + void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ); + void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v); + void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc ); - void doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d, + void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d, std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector & val ); - void doUninterpretedCompose2( FirstOrderModel * fm, Node f, + void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, std::map< int, Node > & entries, int index, std::vector< Node > & cond, std::vector< Node > & val, EntryTrie & curr); - void doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, + void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector & val ); - int isCompat( std::vector< Node > & cond, Node c ); - bool doMeet( std::vector< Node > & cond, Node c ); + int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); + bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); Node mkCond( std::vector< Node > & cond ); - Node mkCondDefault( Node f ); - void mkCondDefaultVec( Node f, std::vector< Node > & cond ); + Node mkCondDefault( FirstOrderModelFmc * fm, Node f ); + void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ); void mkCondVec( Node n, std::vector< Node > & cond ); Node evaluateInterpreted( Node n, std::vector< Node > & vals ); public: @@ -124,25 +149,20 @@ public: ~FullModelChecker(){} int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; } - bool isStar(Node n); - Node getStar(TypeNode tn); - Node getSomeDomainElement(FirstOrderModel * fm, TypeNode tn); - bool isModelBasisTerm(Node n); - Node getModelBasisTerm(TypeNode tn); - Def * getModel(FirstOrderModel * fm, Node op); void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ); - bool useSimpleModels(); - Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ); + Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); /** process build model */ void processBuildModel(TheoryModel* m, bool fullModel); /** get current model value */ - Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ); + Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial ); + + bool useSimpleModels(); }; } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 76e61707e..88fb7cd8f 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -18,7 +18,6 @@ #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" @@ -45,38 +44,37 @@ bool QModelBuilder::optUseModel() { 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; igetNumAssertedQuantifiers(); 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; igetInstantiation( 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; @@ -97,6 +95,7 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ } } + QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) : QModelBuilder( c, qe ) { @@ -106,37 +105,9 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std:: 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; igetNumAssertedQuantifiers(); 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; igetInstantiation( 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 @@ -303,16 +274,17 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ } 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; id_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; id_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 ){ @@ -324,7 +296,7 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ 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); } @@ -332,10 +304,10 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ } } 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{ @@ -420,6 +392,7 @@ int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { } 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]; @@ -454,7 +427,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ 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{ @@ -542,7 +515,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ 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 ); } } @@ -600,6 +573,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ } 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] ){ @@ -608,8 +582,8 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node 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; } } @@ -621,20 +595,20 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ 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; id_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; id_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; @@ -642,7 +616,7 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ } }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; } @@ -655,18 +629,18 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ //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; } @@ -1030,19 +1004,20 @@ void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, Ins } 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; id_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; id_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; } @@ -1051,9 +1026,9 @@ void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ //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; } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index f41392eee..715612975 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -33,8 +33,6 @@ protected: 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(){} @@ -50,8 +48,8 @@ public: 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 ); }; @@ -123,8 +121,6 @@ protected: //helper functions 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(); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index c91d9d3ab..32deb9e47 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -18,7 +18,6 @@ #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" @@ -35,8 +34,7 @@ using namespace CVC4::theory::inst; //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 ); @@ -179,9 +177,8 @@ int ModelEngine::checkModel(){ } */ //compute the relevant domain if necessary - if( optUseRelevantDomain() ){ - d_rel_domain.compute(); - } + //if( optUseRelevantDomain() ){ + //} d_triedLemmas = 0; d_testLemmas = 0; d_relevantLemmas = 0; @@ -240,8 +237,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //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; @@ -252,7 +253,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ 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"); @@ -261,7 +262,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //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{ @@ -296,10 +297,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } } //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; igetNumAssertedQuantifiers(); 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; id_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; id_rep_set.hasType( tn ) ){ - //it is the complete domain - d_quant_inst_domain[f][vi].clear(); - for( size_t i=0; id_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 diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h deleted file mode 100644 index 6fc035e8a..000000000 --- a/src/theory/quantifiers/relevant_domain.h +++ /dev/null @@ -1,54 +0,0 @@ -/********************* */ -/*! \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 */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 89d1ad55a..c663e1aa2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -48,7 +48,11 @@ d_lemmas_produced_c(u){ 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() ){ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 6903adda5..99e28714f 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -100,6 +100,7 @@ RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), } int RepSetIterator::domainSize( int i ) { + Assert(i>=0); if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){ return d_domain[i].size(); }else{ @@ -281,7 +282,9 @@ void RepSetIterator::increment2( int counter ){ 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){ diff --git a/test/Makefile.am b/test/Makefile.am index 6cccca05c..0fdc69e03 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -53,6 +53,7 @@ subdirs_to_check = \ regress/regress0/preprocess \ regress/regress0/unconstrained \ regress/regress0/decision \ + regress/regress0/fmf \ regress/regress1 \ regress/regress2 \ regress/regress3 -- 2.30.2